From 8c675d01d5d5c23f194f83329a34db2f9f2cada0 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 9 Sep 2021 23:54:18 +0200
Subject: [PATCH] make (//) lazier

---
 src/Quox/Syntax/Subst.idr |  2 +-
 src/Quox/Syntax/Term.idr  | 22 ++++++++++++----------
 2 files changed, 13 insertions(+), 11 deletions(-)

diff --git a/src/Quox/Syntax/Subst.idr b/src/Quox/Syntax/Subst.idr
index f776e86..f80dc6b 100644
--- a/src/Quox/Syntax/Subst.idr
+++ b/src/Quox/Syntax/Subst.idr
@@ -35,7 +35,7 @@ export Ord (f to) => Ord (Subst f from to) where compare = compare `on` repr
 infixl 8 //
 public export
 interface FromVar env => CanSubst env term where
-  (//) : term from -> Subst env from to -> term to
+  (//) : term from -> Lazy (Subst env from to) -> term to
 
 public export
 CanSubst1 : (Nat -> Type) -> Type
diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index fd0f162..e5bba64 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -187,11 +187,12 @@ export FromVar (Term d) where fromVar = E . fromVar
 ||| - otherwise, wraps in a new closure
 export
 CanSubst (Elim d) (Elim d) where
-  F x       // _        = F x
-  B i       // th       = th !! i
-  CloE e ph // th       = CloE e $ assert_total $ ph . th
-  e         // Shift SZ = e
-  e         // th       = CloE e th
+  F x       // _  = F x
+  B i       // th = th !! i
+  CloE e ph // th = assert_total CloE e $ ph . th
+  e         // th = case force th of
+                         Shift SZ => e
+                         th       => CloE e th
 
 ||| does the minimal reasonable work:
 ||| - deletes the closure around an atomic constant like `TYPE`
@@ -201,11 +202,12 @@ CanSubst (Elim d) (Elim d) where
 ||| - otherwise, wraps in a new closure
 export
 CanSubst (Elim d) (Term d) where
-  TYPE l    // _        = TYPE l
-  E e       // th       = E $ e // th
-  CloT s ph // th       = CloT s $ ph . th
-  s         // Shift SZ = s
-  s         // th       = CloT s th
+  TYPE l    // _  = TYPE l
+  E e       // th = E $ e // th
+  CloT s ph // th = CloT s $ ph . th
+  s         // th = case force th of
+                         Shift SZ => s
+                         th       => CloT s th
 
 export CanShift (Term d) where i // by = i // Shift by {env=(Elim d)}
 export CanShift (Elim d) where i // by = i // Shift by {env=(Elim d)}