rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

make displace total (with a few asserts)

Browse source
This commit is contained in:
rhiannon morris 2023-08-28 19:57:02 +02:00
parent 72609bc12f
commit 32f6e5a3b1
1 changed files with 7 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
lib/Quox/Displace.idr
View file

@ -2,6 +2,8 @@ module Quox.Displace
import Quox.Syntax import Quox.Syntax
%default total
parameters (k : Universe) parameters (k : Universe)
namespace Term namespace Term
@ -31,7 +33,7 @@ parameters (k : Universe)
doDisplace (Box val loc) = Box (doDisplace val) loc doDisplace (Box val loc) = Box (doDisplace val) loc
doDisplace (E e) = E (doDisplace e) doDisplace (E e) = E (doDisplace e)
doDisplace (CloT (Sub t th)) = doDisplace (CloT (Sub t th)) =
CloT (Sub (doDisplace t) (map doDisplace th)) CloT (Sub (doDisplace t) (assert_total $ map doDisplace th))
doDisplace (DCloT (Sub t th)) = doDisplace (DCloT (Sub t th)) =
DCloT (Sub (doDisplace t) th) DCloT (Sub (doDisplace t) th)
@ -48,7 +50,8 @@ parameters (k : Universe)
doDisplace (CasePair qty pair ret body loc) = doDisplace (CasePair qty pair ret body loc) =
CasePair qty (doDisplace pair) (doDisplaceS ret) (doDisplaceS body) loc CasePair qty (doDisplace pair) (doDisplaceS ret) (doDisplaceS body) loc
doDisplace (CaseEnum qty tag ret arms loc) = doDisplace (CaseEnum qty tag ret arms loc) =
CaseEnum qty (doDisplace tag) (doDisplaceS ret) (map doDisplace arms) loc CaseEnum qty (doDisplace tag) (doDisplaceS ret)
(assert_total $ map doDisplace arms) loc
doDisplace (CaseNat qty qtyIH nat ret zero succ loc) = doDisplace (CaseNat qty qtyIH nat ret zero succ loc) =
CaseNat qty qtyIH (doDisplace nat) (doDisplaceS ret) CaseNat qty qtyIH (doDisplace nat) (doDisplaceS ret)
(doDisplace zero) (doDisplaceS succ) loc (doDisplace zero) (doDisplaceS succ) loc
@ -65,9 +68,9 @@ parameters (k : Universe)
(doDisplaceDS zero) (doDisplaceDS one) loc (doDisplaceDS zero) (doDisplaceDS one) loc
doDisplace (TypeCase ty ret arms def loc) = doDisplace (TypeCase ty ret arms def loc) =
TypeCase (doDisplace ty) (doDisplace ret) TypeCase (doDisplace ty) (doDisplace ret)
(map doDisplaceS arms) (doDisplace def) loc (assert_total $ map doDisplaceS arms) (doDisplace def) loc
doDisplace (CloE (Sub e th)) = doDisplace (CloE (Sub e th)) =
CloE (Sub (doDisplace e) (map doDisplace th)) CloE (Sub (doDisplace e) (assert_total $ map doDisplace th))
doDisplace (DCloE (Sub e th)) = doDisplace (DCloE (Sub e th)) =
DCloE (Sub (doDisplace e) th) DCloE (Sub (doDisplace e) th)