Initial commit for nbe elaborator

No error messages, no import resolution yet
dhall-lang · Apr 20, 2019 · 627a6cd · 627a6cd
1 parent f462dcc
commit 627a6cd
Show file tree

Hide file tree

Showing 14 changed files with 3,825 additions and 1,609 deletions.
diff --git a/dhall/dhall.cabal b/dhall/dhall.cabal
@@ -392,6 +392,7 @@ Library
         directory                   >= 1.2.2.0  && < 1.4 ,
         dotgen                      >= 0.4.2    && < 0.5 ,
         exceptions                  >= 0.8.3    && < 0.11,
+        ghc-prim                    >= 0.3.1.0  && < 0.6,
         filepath                    >= 1.4      && < 1.5 ,
         haskeline                   >= 0.7.2.1  && < 0.8 ,
         lens-family-core            >= 1.0.0    && < 1.3 ,
@@ -450,6 +451,8 @@ Library
         Dhall.Parser.Token,
         Dhall.Import.Types,
         Dhall.Eval,
+        Dhall.Elaboration,
+        Dhall.TypeErrors,
         Dhall.Util,
         Paths_dhall
     if flag(with-http)

diff --git a/dhall/src/Dhall/Binary.hs b/dhall/src/Dhall/Binary.hs
@@ -131,11 +131,11 @@ class ToTerm a where
 
 instance ToTerm a => ToTerm (Expr s a) where
     encode (Var (V "_" n)) =
-        TInteger n
+        TInt n
     encode (Var (V x 0)) =
         TString x
     encode (Var (V x n)) =
-        TList [ TString x, TInteger n ]
+        TList [ TString x, TInt n ]
     encode NaturalBuild =
         TString "Natural/build"
     encode NaturalFold =
@@ -499,9 +499,9 @@ class FromTerm a where
 
 instance FromTerm a => FromTerm (Expr s a) where
     decode (TInt n) =
-        return (Var (V "_" (fromIntegral n)))
-    decode (TInteger n) =
         return (Var (V "_" n))
+    decode (TInteger n) =
+        return (Var (V "_" (fromIntegral n)))
     decode (TString "Natural/build") =
         return NaturalBuild
     decode (TString "Natural/fold") =
@@ -571,7 +571,7 @@ instance FromTerm a => FromTerm (Expr s a) where
     decode (TList [ TString x, TInt n ]) =
         return (Var (V x (fromIntegral n)))
     decode (TList [ TString x, TInteger n ]) =
-        return (Var (V x n))
+        return (Var (V x (fromIntegral n)))
     decode (TList (TInt 0 : f₁ : xs₁)) = do
         f₀  <- decode f₁
         xs₀ <- traverse decode xs₁

diff --git a/dhall/src/Dhall/Binary.hs-boot b/dhall/src/Dhall/Binary.hs-boot
@@ -8,3 +8,6 @@ class ToTerm a where
     encode :: a -> Term
 
 instance ToTerm a => ToTerm (Expr s a)
+
+class FromTerm a where
+    decode :: Term -> Maybe a