Correct the De Bruijn indices when inferring (and printing) the types…

… and values of partially-applied 'mu' combinators
lih · Apr 30, 2019 · 677b5fb · 677b5fb
1 parent 597d6d6
commit 677b5fb
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 8 deletions.
diff --git a/capricon/capricon.cabal b/capricon/capricon.cabal
@@ -2,7 +2,7 @@
 -- see http://haskell.org/cabal/users-guide/
 
 name:                capricon
-version:             0.13.1.1
+version:             0.13.1.2
 -- synopsis:            
 -- description:         
 license:             GPL-3

diff --git a/capricon/exe/CaPriCon_Engine.hs b/capricon/exe/CaPriCon_Engine.hs
@@ -160,7 +160,7 @@ runWordsState ws st = ($st) $ from (stateT.concatT) $^ do
 runWithFS :: JS.JSString -> FSIO a -> JS.CIO a
 runWithFS fsname (FSIO r) = newFS fsname >>= r^..readerT
 
-hasteDict = cocDict ("0.13.1.1-js" :: String) getString getBytes setString setBytes
+hasteDict = cocDict ("0.13.1.2-js" :: String) getString getBytes setString setBytes
 
 main :: IO ()
 main = do

diff --git a/capricon/src/Data/CaPriCon.hs b/capricon/src/Data/CaPriCon.hs
@@ -483,16 +483,16 @@ showNode' dir = go 0
                                                     [DocSpace,DocAssoc x' (go 0 env' tx)] + bind_tail ((x',tx):env') e
                   where x' = fresh (map fst env') x
                 bind_tail env' x = [bind_sep t,DocSpace,go 0 env' x]
-        go d env (Cons a) = showA d a
-          where showA _ (Ap h xs) =
+        go d env (Cons a) = showA d env a
+          where showA _ envA (Ap h xs) =
                   let ni = case h of
-                             Sym i -> DocVarName $ case drop i env of
+                             Sym i -> DocVarName $ case drop i envA of
                                (h',_):_ -> h'
                                _ -> "#"+fromString (show i)
-                             Mu _ _ a' -> DocMu (showA 0 a')
+                             Mu envD _ a' -> DocMu (showA 0 (map (\(x,tx,_) -> (x,tx)) envD + envA) a')
                              Axiom _ ax -> DocText (fromString $ show ax)
                       lvl = if empty xs then 1000 else 1
-                  in par lvl d $ DocSeq $ intercalate [DocSpace] $ map pure (ni:map (go 2 env) xs)
+                  in par lvl d $ DocSeq $ intercalate [DocSpace] $ map pure (ni:map (go 2 envA) xs)
 
         toPat d env x
           | (pats,(_,k)):_ <- findPattern dir x =
@@ -534,7 +534,7 @@ type_of = yb maybeT . go
                 go' (Ap (Mu env _ a') subs) = do
                   ta <- local (map (\(x,tx,_) -> (x,tx)) env +) (go' a')
                   preret <- maybeT $^ mu_type $ foldl' (\e (x,tx,_) -> Bind Prod x tx e) ta env
-                  rec_subst subs (subst (Cons a') preret)
+                  rec_subst subs (subst (foldl' (\e (x,tx,_) -> Bind Lambda x tx e) (Cons a') env) preret)
                 go' (Ap (Axiom t _) subs) = rec_subst subs t
 
                 rec_subst (y:t) (Bind Prod _ tx e) = do