fix subtyping on custom types

ElaraLang · Aug 23, 2023 · c790d2f · c790d2f
1 parent a1c6bd9
commit c790d2f
Show file tree

Hide file tree

Showing 18 changed files with 82 additions and 69 deletions.
diff --git a/app/Main.hs b/app/Main.hs
@@ -91,24 +91,24 @@ runElara dumpShunted dumpTyped dumpCore = fmap fst <$> finalisePipeline $ do
     source <- loadModule "source.elr"
     prelude <- loadModule "prelude.elr"
 
-    let graph = createGraph [source]
+    let graph = createGraph [source, prelude]
     coreGraph <- processModules graph (dumpShunted, dumpTyped)
 
     when dumpCore $ do
         liftIO $ dumpGraph coreGraph (view (field' @"name" . to nameText)) ".core.elr"
 
-    -- classes <- runReader java8 (emitGraph coreGraph)
-    -- for_ classes $ \(mn, class') -> do
-    --     putTextLn ("Compiling " <> showPretty mn <> "...")
-    --     let converted = convert class'
-    --     let bs = runPut (writeBinary converted)
-    --     liftIO $ writeFileLBS ("build/" <> suitableFilePath (ClassFile.name class')) bs
-    --     putTextLn ("Compiled " <> showPretty mn <> "!")
+    classes <- runReader java8 (emitGraph coreGraph)
+    for_ classes $ \(mn, class') -> do
+        putTextLn ("Compiling " <> showPretty mn <> "...")
+        let converted = convert class'
+        let bs = runPut (writeBinary converted)
+        liftIO $ writeFileLBS ("build/" <> suitableFilePath (ClassFile.name class')) bs
+        putTextLn ("Compiled " <> showPretty mn <> "!")
 
     end <- liftIO getCPUTime
     let t :: Double
         t = fromIntegral (end - start) * 1e-9
-    putTextLn ("Successfully compiled " <> show 0 <> " classes in " <> fromString (printf "%.2f" t) <> "ms!")
+    putTextLn ("Successfully compiled " <> show (length classes) <> " classes in " <> fromString (printf "%.2f" t) <> "ms!")
 
 -- typedGraph <- inferModules shuntedGraph
 
@@ -183,7 +183,7 @@ processModules graph (dumpShunted, dumpTyped) =
                     ( traverseGraph rename
                         >=> traverseGraph shunt
                         >=> dumpIf dumpShunted (view (_Unwrapped . unlocated . field' @"name" . to nameText)) ".shunted.elr"
-                        >=> traverseGraph inferModule
+                        >=> traverseGraphRevTopologically inferModule
                         >=> dumpIf dumpTyped (view (_Unwrapped . unlocated . field' @"name" . to nameText)) ".typed.elr"
                         >=> traverseGraph moduleToCore
                         $ graph

diff --git a/build/Main.class b/build/Main.class
diff --git a/build/Main.core.elr b/build/Main.core.elr
@@ -1,9 +1,6 @@
 module Main
-{ Main.add : forall (a_1 : Type). forall (b_2 : Type). forall (c_3 : Type). a_1 -> b_2 -> c_3
-    = Elara.Prim.elaraPrimitive @(a_1 -> b_2 -> c_3) "undefined"
+{ Main.add2 : Int -> String
+    = Elara.Prim.elaraPrimitive @(Int -> String) "undefined"
 ; 
-Main.add2 : String -> Char -> Int
-    = Elara.Prim.elaraPrimitive @(String -> Char -> Int) "undefined"
-; 
-Main.main : Int
-    = Main.add @String @Char @Int "1" 'c' }
+Main.main : IO ()
+    = Prelude.println (Main.add2 1) }
diff --git a/build/Main.shunted.elr b/build/Main.shunted.elr
@@ -1,15 +1,11 @@
 module Main exposing (..)
 
+import Prelude exposing (..)
 
-
-def Main.add : (a_1 -> (b_2 -> c_3))
-let Main.add =
-    (Elara.Prim.elaraPrimitive  "undefined" ) 
-
-def Main.add2 : (Elara.Prim.String -> (Elara.Prim.Char -> Elara.Prim.Int))
+def Main.add2 : (Elara.Prim.Int -> Elara.Prim.String)
 let Main.add2 =
     (Elara.Prim.elaraPrimitive  "undefined" ) 
 
-def Main.main : Elara.Prim.Int
+def Main.main : Elara.Prim.IO ()
 let Main.main =
-    ((Main.add  "1" )  'c' ) 
+    (Prelude.println  (Main.add2  1 ) ) 
diff --git a/build/Main.typed.elr b/build/Main.typed.elr
@@ -1,38 +1,16 @@
 module Main exposing (..)
 
+import Prelude exposing (..)
 
-
-def Main.add : forall (a_1 : Type) (b_2 : Type) (c_3 : Type) . a_1 -> b_2 -> c_3
-let Main.add =
-    ((Elara.Prim.elaraPrimitive : forall (a_0 : Type) . Text -> a_0 @a_1 ->
-                                                                     b_2 ->
-                                                                       c_3) : forall (a_1 : Type) .
-                                                                              forall (b_2 : Type) .
-                                                                              forall (c_3 : Type) .
-                                                                                a_1 ->
-                                                                                b_2 ->
-                                                                                  c_3 "undefined" : Text) : forall (a_1 : Type) .
-                                                                                                            forall (b_2 : Type) .
-                                                                                                            forall (c_3 : Type) .
-                                                                                                              a_1 ->
-                                                                                                              b_2 ->
-                                                                                                                c_3
-
-def Main.add2 : Text -> Char -> Integer
+def Main.add2 : Integer -> Text
 let Main.add2 =
-    ((Elara.Prim.elaraPrimitive : forall (a_0 : Type) . Text -> a_0 @Text ->
-                                                                     Char ->
-                                                                       Integer) : Text ->
-                                                                                  Char ->
-                                                                                    Integer "undefined" : Text) : Text ->
-                                                                                                                  Char ->
-                                                                                                                    Integer
+    ((Elara.Prim.elaraPrimitive : forall (a_0 : Type) . Text -> a_0 @Integer ->
+                                                                       Text) : Integer ->
+                                                                                 Text "undefined" : Text) : Integer ->
+                                                                                                              Text
 
-def Main.main : Integer
+def Main.main : IO Unit 
 let Main.main =
-    (((((Main.add : forall (a_1 : Type) .
-                    forall (b_2 : Type) .
-                    forall (c_3 : Type) .
-                      a_1 -> b_2 -> c_3 @Text) : Char ->
-                                                   Integer "1" : Text) : Char ->
-                                                                           Integer @Char) : Integer @Integer) : Integer 'c' : Char) : Integer
+    (Prelude.println : Text -> IO Unit  (Main.add2 : Integer ->
+                                                       Text 1 : Integer) : Text) : IO Unit
+
diff --git a/build/Prelude.class b/build/Prelude.class
diff --git a/build/Prelude.typed.elr b/build/Prelude.typed.elr
@@ -0,0 +1,13 @@
+module Prelude exposing (..)
+
+
+
+def Prelude.println : Text -> IO Unit 
+let Prelude.println =
+    ((Elara.Prim.elaraPrimitive : forall (a_0 : Type) . Text -> a_0 @Text ->
+                                                                       IO Unit
+                                                                          ) : Text ->
+                                                                                IO Unit
+                                                                                    "println" : Text) : Text ->
+                                                                                                          IO Unit
+
diff --git a/jvm-stdlib/elara/Error.class b/jvm-stdlib/elara/Error.class
diff --git a/jvm-stdlib/elara/Error.java b/jvm-stdlib/elara/Error.java
@@ -0,0 +1,7 @@
+package elara;
+
+public class Error {
+    public static Throwable undefined() {
+        return new RuntimeException("undefined");
+    }
+}
diff --git a/jvm-stdlib/elara/Func.class b/jvm-stdlib/elara/Func.class
diff --git a/prelude.elr b/prelude.elr
@@ -1 +1,4 @@
 module Prelude
+
+def println : String -> IO ()
+let println = elaraPrimitive "println"
diff --git a/source.elr b/source.elr
@@ -1,8 +1,7 @@
-def add : a -> b -> c
-let add = elaraPrimitive "undefined"
+import Prelude 
 
-def add2 : String -> Char -> Int
+def add2 : Int -> String
 let add2 = elaraPrimitive "undefined"
 
-def main : Int
-let main = add "1" 'c'
+def main : IO ()
+let main = println (add2 1 )
diff --git a/src/Elara/AST/Module.hs b/src/Elara/AST/Module.hs
@@ -21,6 +21,7 @@ import Elara.AST.Region (Located, unlocated)
 import Elara.Data.Pretty
 import Elara.Data.Pretty.Styles qualified as Style
 import Elara.Data.TopologicalGraph
+import Print (debugPretty)
 import Unsafe.Coerce
 
 newtype Module ast = Module (ASTLocate ast (Module' ast))

diff --git a/src/Elara/Emit.hs b/src/Elara/Emit.hs
@@ -28,7 +28,7 @@ import JVM.Data.JVMVersion
 import Polysemy
 import Polysemy.Reader
 import Polysemy.Writer
-import Print (showPretty)
+import Print (showColored, showPretty)
 
 type Emit r = Members '[Reader JVMVersion] r
 
@@ -156,12 +156,18 @@ createModuleName (ModuleName name) = QualifiedClassName (PackageName $ init name
 generateCode :: JVMExpr -> Maybe Type -> InnerEmit [Instruction]
 generateCode (Var (JVMLocal 0)) _ = pure [ALoad0]
 -- Hardcode elaraPrimitive "println"
-generateCode (App (Var (Normal (Id (Global (Identity v)) _))) (Lit (String "println"))) _
+generateCode ((App (TyApp (Var (Normal (Id (Global (Identity v)) _))) as) (Lit (String "println")))) _
     | v == fetchPrimitiveName =
         pure
             [ ALoad0
             , InvokeStatic (ClassInfoType "elara.IO") "println" (MethodDescriptor [ObjectFieldType "java.lang.String"] (TypeReturn (ObjectFieldType "elara.IO")))
             ]
+generateCode ((App (TyApp (Var (Normal (Id (Global (Identity v)) _))) as) (Lit (String "undefined")))) (Just t)
+    | v == fetchPrimitiveName =
+        pure
+            [ InvokeStatic (ClassInfoType "elara.Error") "undefined" (MethodDescriptor [] (TypeReturn (ObjectFieldType "java.lang.Throwable")))
+            , AThrow
+            ]
 generateCode ((Var (Normal (Id{idVarName = Global (Identity (Qualified vn mn)), idVarType = idVarType})))) _ = do
     -- load static var
     let invokeStaticVars = (ClassInfoType $ createModuleName mn, vn, generateFieldType idVarType)
@@ -179,6 +185,7 @@ generateCode (App (Var (Normal (Id{idVarName = Global (Identity (Qualified vn mn
             )
 
     pure $ x' <> [uncurry3 InvokeStatic invokeStaticVars] <> castInstrs
+generateCode (TyApp a t) _ = generateCode a (Just t)
 generateCode (Lit (String s)) _ =
     pure
         [ LDC (LDCString s)
@@ -188,7 +195,7 @@ generateCode (Lit (Int i)) _ =
         [ LDC (LDCInt (fromIntegral i))
         , InvokeStatic (ClassInfoType "java.lang.Integer") "valueOf" (MethodDescriptor [ObjectFieldType "java.lang.String"] (TypeReturn (ObjectFieldType "java.lang.Integer")))
         ]
-generateCode e t = error (showPretty (e, t))
+generateCode e t = error (showPretty e)
 
 {- | Determines if a type is a value type.
  That is, a type that can be compiled to a field rather than a method.
@@ -205,6 +212,7 @@ generateFieldType c | c == stringCon = ObjectFieldType "java.lang.String"
 generateFieldType (AppTy l _) | l == listCon = ObjectFieldType "elara.EList"
 generateFieldType (TyVarTy _) = ObjectFieldType "java.lang.Object"
 generateFieldType (AppTy l _) | l == ioCon = ObjectFieldType "elara.IO"
+generateFieldType (FuncTy _ _) = ObjectFieldType "elara.Func"
 generateFieldType o = error $ "generateFieldType: " <> show o
 
 generateMethodDescriptor :: HasCallStack => Type -> MethodDescriptor

diff --git a/src/Elara/TypeInfer.hs b/src/Elara/TypeInfer.hs
@@ -63,9 +63,7 @@ inferModule ::
     Module 'Shunted ->
     Sem r (Module 'Typed)
 inferModule m = do
-    m' <- traverseModuleRevTopologically inferDeclaration m
-    y <- Infer.getAll
-    pure m'
+    traverseModuleRevTopologically inferDeclaration m
 
 inferDeclaration ::
     forall r.

diff --git a/src/Elara/TypeInfer/Error.hs b/src/Elara/TypeInfer/Error.hs
@@ -58,6 +58,7 @@ data TypeInferenceError
     | --
       RecordTypeMismatch (Type SourceRegion) (Type SourceRegion) (Map.Map UniqueTyVar (Type SourceRegion)) (Map.Map UniqueTyVar (Type SourceRegion))
     | UnionTypeMismatch (Type SourceRegion) (Type SourceRegion) (Map.Map UniqueTyVar (Type SourceRegion)) (Map.Map UniqueTyVar (Type SourceRegion))
+    | CustomTypeMismatch (Type SourceRegion) (Type SourceRegion) Text Text
     | --
       UserDefinedTypeNotInContext SourceRegion ShuntedType (Context SourceRegion)
     | KindInferError KindInferError

diff --git a/src/Elara/TypeInfer/Infer.hs b/src/Elara/TypeInfer/Infer.hs
@@ -660,6 +660,18 @@ subtype _A0 _B0 = do
                         )
                         p1
                 (_, _) -> throw (NotUnionSubtype (Type.location _A0) _A (Type.location _B0) _B)
+        (_A@Type.Custom{conName, typeArguments = kAs0}, _B@Type.Custom{conName = conName2, typeArguments = kBs0}) -> do
+            when (conName /= conName2) do
+                throw (CustomTypeMismatch _A0 _B0 conName conName2)
+
+            let process (_A1, _B1) = do
+                    _Θ <- get
+
+                    subtype
+                        (Context.solveType _Θ _A1)
+                        (Context.solveType _Θ _B1)
+
+            traverse_ process (zip kAs0 kBs0)
 
         -- Unfortunately, we need to have this wildcard match at the end,
         -- otherwise we'd have to specify a number of cases that is quadratic

diff --git a/stack.yaml b/stack.yaml
@@ -11,7 +11,7 @@ flags:
 
 extra-deps:
 - git: git@github.com:ElaraLang/h2jvm.git
-  commit: 6f7ba6c9a5f4e2d11661b2852505912bd8c74775
+  commit: 533ea177137ec737ba4ce7f22fab44a1fd60b44a
 - git: git@github.com:knightzmc/diagnose.git
   commit: 59730d9207319d7cae13fb93f21062f2b40a823f
 - OneTuple-0.4.1.1@sha256:be0324c77a0eaf1d48b771b7e86f2b19d53a9f5ecc6ab2c914dab7dad309c671,2539