Skip to content

Commit

Permalink
Merge pull request #25 from msp-strath/sketchy
Browse files Browse the repository at this point in the history
prop was generating rules with scope errors; have patched some
  • Loading branch information
pigworker authored Mar 23, 2021
2 parents 0e5b663 + 57aeba4 commit be426f5
Show file tree
Hide file tree
Showing 2 changed files with 30 additions and 2 deletions.
12 changes: 10 additions & 2 deletions Src/ChkRaw.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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])
Expand All @@ -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)])
Expand Down
20 changes: 20 additions & 0 deletions Src/Context.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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!
Expand Down

0 comments on commit be426f5

Please sign in to comment.