This commit is contained in:
crumbtoo
2024-03-28 11:32:34 -06:00
parent ba7ee8bc2c
commit b9634e5530
2 changed files with 11 additions and 2 deletions

View File

@@ -364,7 +364,7 @@ inferProg p = do
(p',csroot) <- annotateProg (etaExpandAll p) (p',csroot) <- annotateProg (etaExpandAll p)
traceM $ "p' : " <> show p' traceM $ "p' : " <> show p'
let (cs,as) = foldMap finalJudgement p' ^. lensProduct constraints assumptions let (cs,as) = foldMap finalJudgement p' ^. lensProduct constraints assumptions
cs' <- (\a -> csroot <> cs <> a) <$> elimAssumptionsG g0 as cs' <- (\a -> cs <> csroot <> a) <$> elimAssumptionsG g0 as
traceM $ "cs' : " <> show cs' traceM $ "cs' : " <> show cs'
sub <- solve cs' sub <- solve cs'
pure $ p' & programDecls . traversed . _FunD . _3 pure $ p' & programDecls . traversed . _FunD . _3
@@ -388,8 +388,12 @@ annotateProg p = do
-- we only wipe the memo here as a temporary solution to the memo shadowing -- we only wipe the memo here as a temporary solution to the memo shadowing
-- problem -- problem
p' <- (thenWipeMemo . annotate) `traverse` p p' <- (thenWipeMemo . annotate) `traverse` p
p'' <- forOf (traversed . traversed . _2) p' \ j -> do
c <- elimWithBinds (ks `zip` txs) (j ^. assumptions)
pure $ j & constraints <>~ c
& assumptions %~ deleteKeys ks
-- TODO: any remaining assumptions should be errors at this point -- TODO: any remaining assumptions should be errors at this point
pure (p',cs) pure (p'',cs)
where where
thenWipeMemo a = (hmMemo .= mempty) *> a thenWipeMemo a = (hmMemo .= mempty) *> a

View File

@@ -100,6 +100,9 @@
" in " " in "
(Expr colours 0 e)]) (Expr colours 0 e)])
(defn LitExpr [_ l]
[:code (str l)])
(defn Expr [[c & colours] p {e :e t :type}] (defn Expr [[c & colours] p {e :e t :type}]
(match e (match e
{:InL {:tag "LamF" :contents [bs body & _]}} {:InL {:tag "LamF" :contents [bs body & _]}}
@@ -113,6 +116,8 @@
{:InR {:tag "LetEF" :contents [r bs body]}} {:InR {:tag "LetEF" :contents [r bs body]}}
(maybe-parens (< ppr/app-prec1 p) (maybe-parens (< ppr/app-prec1 p)
[Typed c t [LetExpr colours r bs body]]) [Typed c t [LetExpr colours r bs body]])
{:InL {:tag "LitF" :contents l}}
[Typed c t [LitExpr colours l]]
:else [:code "<expr>"])) :else [:code "<expr>"]))
(def rainbow-cycle (cycle ["red" (def rainbow-cycle (cycle ["red"