From b78279c3e079e5d0f3a44a4ae976e6fff882af96 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Wed, 14 Aug 2024 16:15:49 +0200 Subject: [PATCH] Fix inference of let and letrec in core (#2953) * Closes #2949 --------- Co-authored-by: Paul Cadman --- src/Juvix/Compiler/Core/Data/BinderList.hs | 4 +-- .../Core/Transformation/ComputeTypeInfo.hs | 8 +++-- test/Compilation/Positive.hs | 7 ++++- test/Core/Eval/Positive.hs | 7 ++++- tests/Compilation/positive/out/test079.out | 1 + tests/Compilation/positive/test079.juvix | 30 +++++++++++++++++++ tests/Core/positive/out/test065.out | 1 + tests/Core/positive/test065.jvc | 27 +++++++++++++++++ 8 files changed, 79 insertions(+), 6 deletions(-) create mode 100644 tests/Compilation/positive/out/test079.out create mode 100644 tests/Compilation/positive/test079.juvix create mode 100644 tests/Core/positive/out/test065.out create mode 100644 tests/Core/positive/test065.jvc diff --git a/src/Juvix/Compiler/Core/Data/BinderList.hs b/src/Juvix/Compiler/Core/Data/BinderList.hs index 53e856d982..6e217b6d2b 100644 --- a/src/Juvix/Compiler/Core/Data/BinderList.hs +++ b/src/Juvix/Compiler/Core/Data/BinderList.hs @@ -78,7 +78,7 @@ lookupMay idx bl | idx < bl ^. blLength = Just $ (bl ^. blMap) !! idx | otherwise = Nothing --- | lookup de Bruijn Index +-- | lookup de Bruijn index lookup :: Index -> BinderList a -> a lookup idx bl = fromMaybe err (lookupMay idx bl) where @@ -93,7 +93,7 @@ lookup idx bl = fromMaybe err (lookupMay idx bl) <> show (length (bl ^. blMap)) ) --- | lookup de Bruijn Level +-- | lookup de Bruijn level lookupLevel :: Level -> BinderList a -> a lookupLevel lvl bl | target < bl ^. blLength = (bl ^. blMap) !! target diff --git a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs index e2622cf50a..b180ad5763 100644 --- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs +++ b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs @@ -99,9 +99,13 @@ computeNodeTypeInfo md = umapL go NLam Lambda {..} -> mkPi mempty _lambdaBinder (Info.getNodeType _lambdaBody) NLet Let {..} -> - Info.getNodeType _letBody + shift + (-1) + (Info.getNodeType _letBody) NRec LetRec {..} -> - Info.getNodeType _letRecBody + shift + (-(length _letRecValues)) + (Info.getNodeType _letRecBody) NCase Case {..} -> case _caseDefault of Just nd -> Info.getNodeType nd Nothing -> case _caseBranches of diff --git a/test/Compilation/Positive.hs b/test/Compilation/Positive.hs index 3a65505b66..51fc1fb284 100644 --- a/test/Compilation/Positive.hs +++ b/test/Compilation/Positive.hs @@ -465,5 +465,10 @@ tests = "Test078: Builtin Byte" $(mkRelDir ".") $(mkRelFile "test078.juvix") - $(mkRelFile "out/test078.out") + $(mkRelFile "out/test078.out"), + posTestEval + "Test079: Let / LetRec type inference (during lambda lifting) in Core" + $(mkRelDir ".") + $(mkRelFile "test079.juvix") + $(mkRelFile "out/test079.out") ] diff --git a/test/Core/Eval/Positive.hs b/test/Core/Eval/Positive.hs index a8451a1884..ade2bec210 100644 --- a/test/Core/Eval/Positive.hs +++ b/test/Core/Eval/Positive.hs @@ -362,5 +362,10 @@ tests = "Test064: ByteArray" $(mkRelDir ".") $(mkRelFile "test064.jvc") - $(mkRelFile "out/test064.out") + $(mkRelFile "out/test064.out"), + PosTest + "Test065: Let / LetRec type inference" + $(mkRelDir ".") + $(mkRelFile "test065.jvc") + $(mkRelFile "out/test065.out") ] diff --git a/tests/Compilation/positive/out/test079.out b/tests/Compilation/positive/out/test079.out new file mode 100644 index 0000000000..26af6a865b --- /dev/null +++ b/tests/Compilation/positive/out/test079.out @@ -0,0 +1 @@ +zero diff --git a/tests/Compilation/positive/test079.juvix b/tests/Compilation/positive/test079.juvix new file mode 100644 index 0000000000..0c09c285da --- /dev/null +++ b/tests/Compilation/positive/test079.juvix @@ -0,0 +1,30 @@ +module test079; + ++ : Nat -> Nat -> Nat + | _ _ := zero; + +type Nat := + | zero + | suc Nat; + +type Foldable := mkFoldable {for : {B : Type} -> (B -> Nat -> B) -> B -> Box -> B}; + +type Box := mkBox {unbox : Nat}; + +one : Nat := zero; + +open Foldable public; + +foldableBoxNatI : Foldable := + mkFoldable@{ + for {B : Type} (f : B -> Nat -> B) (ini : B) : Box -> B + | (mkBox x) := + let + terminating + go : Nat -> B + | zero := ini + | _ := go x; + in go x + }; + +main : Nat := for foldableBoxNatI λ {_ y := y} one (mkBox zero); diff --git a/tests/Core/positive/out/test065.out b/tests/Core/positive/out/test065.out new file mode 100644 index 0000000000..63e34bbb68 --- /dev/null +++ b/tests/Core/positive/out/test065.out @@ -0,0 +1 @@ +Zero diff --git a/tests/Core/positive/test065.jvc b/tests/Core/positive/test065.jvc new file mode 100644 index 0000000000..39e5af8a2b --- /dev/null +++ b/tests/Core/positive/test065.jvc @@ -0,0 +1,27 @@ +type nat { + Zero : nat; + Suc : nat -> nat; +}; + +type Box { + mkBox : nat -> Box; +}; + +def id := λ(x : Any) x; + +def f := λ(x : nat) λ(y : nat) x; + +def topGo : Π B : Type, B → nat → B := λ(B : Type) λ(b : B) λ(x' : nat) b; + +def const : Π A : Type, A -> A -> A := λ(A : Type) λ(x : A) λ(y : A) x; + +def lam := id (λ(B : Type) + λ(f : B → nat → B) + λ(ini : B) + λ(_X : Box) + case _X of { + mkBox (x : nat) := let go : nat → B := topGo B ini in + const B (go x) (go x) + }); + +lam nat f Zero (mkBox (Suc Zero))