From 32f6e5a3b17bf565368a7b77dcdde2be69eb20fc Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Mon, 28 Aug 2023 19:57:02 +0200 Subject: [PATCH] make displace total (with a few asserts) --- lib/Quox/Displace.idr | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/lib/Quox/Displace.idr b/lib/Quox/Displace.idr index c7d5e02..1945936 100644 --- a/lib/Quox/Displace.idr +++ b/lib/Quox/Displace.idr @@ -2,6 +2,8 @@ module Quox.Displace import Quox.Syntax +%default total + parameters (k : Universe) namespace Term @@ -31,7 +33,7 @@ parameters (k : Universe) doDisplace (Box val loc) = Box (doDisplace val) loc doDisplace (E e) = E (doDisplace e) 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)) = DCloT (Sub (doDisplace t) th) @@ -48,7 +50,8 @@ parameters (k : Universe) doDisplace (CasePair qty pair ret body loc) = CasePair qty (doDisplace pair) (doDisplaceS ret) (doDisplaceS body) 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) = CaseNat qty qtyIH (doDisplace nat) (doDisplaceS ret) (doDisplace zero) (doDisplaceS succ) loc @@ -65,9 +68,9 @@ parameters (k : Universe) (doDisplaceDS zero) (doDisplaceDS one) loc doDisplace (TypeCase ty ret arms def loc) = TypeCase (doDisplace ty) (doDisplace ret) - (map doDisplaceS arms) (doDisplace def) loc + (assert_total $ map doDisplaceS arms) (doDisplace def) loc 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)) = DCloE (Sub (doDisplace e) th)