gulp
This commit is contained in:
@@ -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
|
||||||
|
|
||||||
|
|||||||
@@ -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"
|
||||||
|
|||||||
Reference in New Issue
Block a user