From 57aeba44c2d4a71bd0d5fd1ad2fa5d3dc4a16e38 Mon Sep 17 00:00:00 2001
From: Conor McBride <conor@strictlypositive.org>
Date: Mon, 22 Mar 2021 19:39:23 +0000
Subject: [PATCH] prop was generating rules with scope errors; have patched
 some

---
 Src/ChkRaw.hs  | 12 ++++++++++--
 Src/Context.hs | 20 ++++++++++++++++++++
 2 files changed, 30 insertions(+), 2 deletions(-)

diff --git a/Src/ChkRaw.hs b/Src/ChkRaw.hs
index e519f79..7452387 100644
--- a/Src/ChkRaw.hs
+++ b/Src/ChkRaw.hs
@@ -626,7 +626,8 @@ chkProp (ls, (t, _, rel) :$$ as) intros | elem t [Uid, Sym]  = do
   (rus, cxs) <- fold <$> traverse (chkIntro tel) intros
   guard $ nodup rus
   mapM_ pushOutDoor cxs
-  doorStep
+  de <- doorStep
+  True <- tracy ("CHKPROP-KILLS: " ++ show de) $ return True
   return ()
  where
   chkIntro :: Tel -> RawIntro -> AM ([String], [CxE])
@@ -645,13 +646,20 @@ chkProp (ls, (t, _, rel) :$$ as) intros | elem t [Uid, Sym]  = do
     pop $ \case {ImplicitQuantifier -> True; _ -> False}
     ps <- traverse chkPrem prems
     lox <- doorStep
+    True <- tracy ("PROP-INTRO-KILL: " ++ show lox) $ return True
     tel <- telify vs lox
-    let (tel', ps') = rfold e4p sb (tel, toList ps)
+    let pss = subOut lox ps
+    let (tel', ps') = rfold e4p sb (tel, toList pss)
     let byr = ByRule True $ (hp, (ru, tel')) :<= ps'
+    True <- tracy ("PROP-INTRO: " ++ show byr) $ return True
     return ([ru], [byr])
   chkPrem :: ([Appl], Appl) -> AM Subgoal
   chkPrem (hs, g) =
     rfold GIVEN <$> traverse (elabTm EXP Prop) hs <*> (PROVE <$> elabTm EXP Prop g)
+  subOut [] ps = ps
+  subOut (Bind (x, Hide ty) (Defn t) : de) ps =
+    subOut (e4p (x, t ::: ty) de) (fmap (e4p (x, t ::: ty)) ps)
+  subOut (_ : de) ps = subOut de ps
 chkProp _ intros = gripe FAIL
 
 patify :: Tm -> AM (Pat, [(Nom, Syn)])
diff --git a/Src/Context.hs b/Src/Context.hs
index 9aee8ba..658fb20 100644
--- a/Src/Context.hs
+++ b/Src/Context.hs
@@ -256,6 +256,26 @@ nomBKind x = gamma >>= foldl me empty where
   me no (Bind (y, _) bk) | x == y = return bk
   me no _ = no
 
+-- wildly incomplete
+instance Stan CxE where
+  stan ms (Bind (x, Hide ty) k) =
+    Bind (x, Hide (stan ms ty)) (stan ms k)
+  stan ms z = z
+  sbst u es (Bind (x, Hide ty) k) =
+    Bind (x, Hide (sbst u es ty)) (sbst u es k)
+  sbst u es z = z
+  abst x i (Bind (n, Hide ty) k) =
+    Bind <$> ((n,) <$> (Hide <$> abst x i ty)) <*> abst x i k
+  abst x i z = pure z
+
+instance Stan BKind where
+  stan ms (Defn t) = Defn (stan ms t)
+  stan _ k = k
+  sbst u es (Defn t) = Defn (sbst u es t)
+  sbst _ _ k = k
+  abst x i (Defn t) = Defn <$> abst x i t
+  abst _ _ k = pure k
+
 
 ------------------------------------------------------------------------------
 --  Demanding!