diff options
Diffstat (limited to '')
| -rw-r--r-- | source/lux.lux | 323 | ||||
| -rw-r--r-- | src/lux.clj | 6 | ||||
| -rw-r--r-- | src/lux/analyser.clj | 15 | ||||
| -rw-r--r-- | src/lux/analyser/base.clj | 18 | ||||
| -rw-r--r-- | src/lux/analyser/case.clj | 236 | ||||
| -rw-r--r-- | src/lux/analyser/lambda.clj | 2 | ||||
| -rw-r--r-- | src/lux/analyser/lux.clj | 104 | ||||
| -rw-r--r-- | src/lux/base.clj | 12 | ||||
| -rw-r--r-- | src/lux/type.clj | 413 |
9 files changed, 634 insertions, 495 deletions
diff --git a/source/lux.lux b/source/lux.lux index 357366d58..ca6a1925c 100644 --- a/source/lux.lux +++ b/source/lux.lux @@ -74,173 +74,170 @@ #Nil])])])])])])])])])])]))]) #NothingT])))) -## ## (deftype (Maybe a) -## ## (| #None -## ## (#Some a))) -## (def' Maybe -## (#AllT [#Nil "Maybe" "a" -## (#VariantT (#Cons [["lux;None" (#TupleT #Nil)] -## (#Cons [["lux;Some" (#BoundT "a")] -## #Nil])]))])) - -## ## (deftype (Bindings k v) -## ## (& #counter Int -## ## #mappings (List (, k v)))) -## (def' Bindings -## (#AllT [#Nil "Bindings" "k" -## (#AllT [#Nil "" "v" -## (#RecordT (#Cons [["lux;counter" Int] -## (#Cons [["lux;mappings" (#AppT [List -## (#TupleT (#Cons [(#BoundT "k") -## (#Cons [(#BoundT "v") -## #Nil])]))])] -## #Nil])]))])])) - -## ## (deftype (Env k v) -## ## (& #name Text -## ## #inner-closures Int -## ## #locals (Bindings k v) -## ## #closure (Bindings k v))) -## (def' Env -## (#AllT [#Nil "Env" "k" -## (#AllT [#Nil "" "v" -## (#RecordT (#Cons [["lux;name" Text] -## (#Cons [["lux;inner-closures" Int] -## (#Cons [["lux;locals" (#AppT [(#AppT [Bindings (#BoundT "k")]) -## (#BoundT "v")])] -## (#Cons [["lux;closure" (#AppT [(#AppT [Bindings (#BoundT "k")]) -## (#BoundT "v")])] -## #Nil])])])]))])])) - -## ## (deftype Cursor -## ## (, Text Int Int)) -## (def' Cursor -## (#TupleT (#Cons [Text (#Cons [Int (#Cons [Int #Nil])])]))) - -## ## (deftype (Meta m v) -## ## (| (#Meta (, m v)))) -## (def' Meta -## (#AllT [#Nil "Meta" "m" -## (#AllT [#Nil "" "v" -## (#VariantT (#Cons [["lux;Meta" (#TupleT (#Cons [(#BoundT "m") -## (#Cons [(#BoundT "v") -## #Nil])]))] -## #Nil]))])])) - -## ## (def' Reader -## ## (List (Meta Cursor Text))) -## (def' Reader -## (#AppT [List -## (#AppT [(#AppT [Meta Cursor]) -## Text])])) - -## ## (deftype Compiler_State -## ## (& #source (Maybe Reader) -## ## #modules (List Any) -## ## #module-aliases (List Any) -## ## #global-env (Maybe (Env Text Any)) -## ## #local-envs (List (Env Text Any)) -## ## #types (Bindings Int Type) -## ## #writer (^ org.objectweb.asm.ClassWriter) -## ## #loader (^ java.net.URLClassLoader) -## ## #eval-ctor Int)) -## (def' Compiler_State -## (#RecordT (#Cons [["lux;source" (#AppT [Maybe Reader])] -## (#Cons [["lux;modules" (#AppT [List Any])] -## (#Cons [["lux;module-aliases" (#AppT [List Any])] -## (#Cons [["lux;global-env" (#AppT [Maybe (#AppT [(#AppT [Env Text]) Any])])] -## (#Cons [["lux;local-envs" (#AppT [List (#AppT [(#AppT [Env Text]) Any])])] -## (#Cons [["lux;types" (#AppT [(#AppT [Bindings Int]) Type])] -## (#Cons [["lux;writer" (#DataT "org.objectweb.asm.ClassWriter")] -## (#Cons [["lux;loader" (#DataT "java.lang.ClassLoader")] -## (#Cons [["lux;eval-ctor" Int] -## #Nil])])])])])])])])]))) +## (deftype (Maybe a) +## (| #None +## (#Some a))) +(def' Maybe + (#AllT [#Nil "Maybe" "a" + (#VariantT (#Cons [["lux;None" (#TupleT #Nil)] + (#Cons [["lux;Some" (#BoundT "a")] + #Nil])]))])) -## ## (deftype #rec Syntax -## ## (Meta Cursor (| (#Bool Bool) -## ## (#Int Int) -## ## (#Real Real) -## ## (#Char Char) -## ## (#Text Text) -## ## (#Form (List Syntax)) -## ## (#Tuple (List Syntax)) -## ## (#Record (List (, Text Syntax)))))) -## (def' Syntax -## (case' (#AppT [(#BoundT "Syntax") (#BoundT "")]) -## Syntax -## (case' (#AppT [List Syntax]) -## SyntaxList -## (#AppT [(#AllT [#Nil "Syntax" "" -## (#VariantT (#Cons [["lux;Bool" Bool] -## (#Cons [["lux;Int" Int] -## (#Cons [["lux;Real" Real] -## (#Cons [["lux;Char" Char] -## (#Cons [["lux;Text" Text] -## (#Cons [["lux;Form" SyntaxList] -## (#Cons [["lux;Tuple" SyntaxList] -## (#Cons [["lux;Record" (#AppT [List (#TupleT (#Cons [Text (#Cons [Syntax #Nil])]))])] -## #Nil])])])])])])])]))]) -## #NothingT])))) +## (deftype (Bindings k v) +## (& #counter Int +## #mappings (List (, k v)))) +(def' Bindings + (#AllT [#Nil "Bindings" "k" + (#AllT [#Nil "" "v" + (#RecordT (#Cons [["lux;counter" Int] + (#Cons [["lux;mappings" (#AppT [List + (#TupleT (#Cons [(#BoundT "k") + (#Cons [(#BoundT "v") + #Nil])]))])] + #Nil])]))])])) + +## (deftype (Env k v) +## (& #name Text +## #inner-closures Int +## #locals (Bindings k v) +## #closure (Bindings k v))) +(def' Env + (#AllT [#Nil "Env" "k" + (#AllT [#Nil "" "v" + (#RecordT (#Cons [["lux;name" Text] + (#Cons [["lux;inner-closures" Int] + (#Cons [["lux;locals" (#AppT [(#AppT [Bindings (#BoundT "k")]) + (#BoundT "v")])] + (#Cons [["lux;closure" (#AppT [(#AppT [Bindings (#BoundT "k")]) + (#BoundT "v")])] + #Nil])])])]))])])) + +## (deftype Cursor +## (, Text Int Int)) +(def' Cursor + (#TupleT (#Cons [Text (#Cons [Int (#Cons [Int #Nil])])]))) + +## (deftype (Meta m v) +## (| (#Meta (, m v)))) +(def' Meta + (#AllT [#Nil "Meta" "m" + (#AllT [#Nil "" "v" + (#VariantT (#Cons [["lux;Meta" (#TupleT (#Cons [(#BoundT "m") + (#Cons [(#BoundT "v") + #Nil])]))] + #Nil]))])])) -## ## (deftype (Either l r) -## ## (| (#Left l) -## ## (#Right r))) -## (def' Either -## (#AllT [#Nil "_" "l" -## (#AllT [#Nil "" "r" -## (#VariantT (#Cons [["lux;Left" (#BoundT "l")] -## (#Cons [["lux;Right" (#BoundT "r")] -## #Nil])]))])])) +## (def' Reader +## (List (Meta Cursor Text))) +(def' Reader + (#AppT [List + (#AppT [(#AppT [Meta Cursor]) + Text])])) + +## (deftype Compiler_State +## (& #source (Maybe Reader) +## #modules (List Any) +## #module-aliases (List Any) +## #global-env (Maybe (Env Text Any)) +## #local-envs (List (Env Text Any)) +## #types (Bindings Int Type) +## #writer (^ org.objectweb.asm.ClassWriter) +## #loader (^ java.net.URLClassLoader) +## #eval-ctor Int)) +(def' Compiler_State + (#RecordT (#Cons [["lux;source" (#AppT [Maybe Reader])] + (#Cons [["lux;modules" (#AppT [List Any])] + (#Cons [["lux;module-aliases" (#AppT [List Any])] + (#Cons [["lux;global-env" (#AppT [Maybe (#AppT [(#AppT [Env Text]) Any])])] + (#Cons [["lux;local-envs" (#AppT [List (#AppT [(#AppT [Env Text]) Any])])] + (#Cons [["lux;types" (#AppT [(#AppT [Bindings Int]) Type])] + (#Cons [["lux;writer" (#DataT "org.objectweb.asm.ClassWriter")] + (#Cons [["lux;loader" (#DataT "java.lang.ClassLoader")] + (#Cons [["lux;eval-ctor" Int] + #Nil])])])])])])])])]))) + +## (deftype #rec Syntax +## (Meta Cursor (| (#Bool Bool) +## (#Int Int) +## (#Real Real) +## (#Char Char) +## (#Text Text) +## (#Form (List Syntax)) +## (#Tuple (List Syntax)) +## (#Record (List (, Text Syntax)))))) +(def' Syntax + (case' (#AppT [(#BoundT "Syntax") (#BoundT "")]) + Syntax + (case' (#AppT [List Syntax]) + SyntaxList + (#AppT [(#AllT [#Nil "Syntax" "" + (#AppT [(#AppT [Meta Cursor]) + (#VariantT (#Cons [["lux;Bool" Bool] + (#Cons [["lux;Int" Int] + (#Cons [["lux;Real" Real] + (#Cons [["lux;Char" Char] + (#Cons [["lux;Text" Text] + (#Cons [["lux;Form" SyntaxList] + (#Cons [["lux;Tuple" SyntaxList] + (#Cons [["lux;Record" (#AppT [List (#TupleT (#Cons [Text (#Cons [Syntax #Nil])]))])] + #Nil])])])])])])])]))])]) + #NothingT])))) + +## (deftype (Either l r) +## (| (#Left l) +## (#Right r))) +(def' Either + (#AllT [#Nil "_" "l" + (#AllT [#Nil "" "r" + (#VariantT (#Cons [["lux;Left" (#BoundT "l")] + (#Cons [["lux;Right" (#BoundT "r")] + #Nil])]))])])) + +## (deftype Macro +## (-> (List Syntax) Compiler_State +## (Either Text [Compiler_State (List Syntax)]))) +(def' Macro + (case' (#AppT [List Syntax]) + SyntaxList + (#LambdaT [SyntaxList + (#LambdaT [Compiler_State + (#AppT [(#AppT [Either Text]) + (#TupleT (#Cons [Compiler_State + (#Cons [SyntaxList #Nil])]))])])]))) + +## Base functions & macros +## (def (_meta data) +## (All [a] (-> a (Meta Cursor a))) +## (#Meta [["" -1 -1] data])) +(def' _meta + (check' (#AllT [#Nil "_" "a" + (#LambdaT [(#BoundT "a") + (#AppT [(#AppT [Meta Cursor]) + (#BoundT "a")])])]) + (lambda' _ data + (#Meta [["" -1 -1] data])))) + +(def' let' + (check' Macro + (lambda' _ tokens + (lambda' _ state + (case' tokens + (#Cons [lhs (#Cons [rhs (#Cons [body #Nil])])]) + (#Right [state + (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "case'"])) + (#Cons [rhs (#Cons [lhs (#Cons [body #Nil])])])]))) + #Nil])]) + + _ + (#Left "Wrong syntax for let'")) + )))) -## ## (deftype Macro -## ## (-> (List Syntax) Compiler_State -## ## (Either Text [Compiler_State (List Syntax)]))) -## (def' Macro -## (case' (#AppT [List Syntax]) -## SyntaxList -## (#LambdaT [SyntaxList -## (#LambdaT [CompilerState -## (#AppT [(#AppT [Either Text]) -## (#TupleT (#Cons [CompilerState -## (#Cons [SyntaxList #Nil])]))])])]))) - -## ## Base functions & macros -## ## (def (_meta data) -## ## (All [a] (-> a (Meta Cursor a))) -## ## (#Meta [["" -1 -1] data])) -## (def' _meta -## (check' (#AllT [#Nil "_" "a" -## (#LambdaT [(#BoundT "a") -## (#AppT [(#AppT [Meta Cursor]) -## (#BoundT "a")])])]) -## (lambda' _ data -## (#Meta [["" -1 -1] data])))) - -## ## (def' let' -## ## (check' Macro -## ## (lambda' _ tokens -## ## (lambda' _ state -## ## (case' tokens -## ## (#Cons [lhs (#Cons [rhs (#Cons [body #Nil])])]) -## ## (#Right [state -## ## (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "case'"])) -## ## (#Cons [rhs (#Cons [lhs (#Cons [body #Nil])])])]))) -## ## #Nil])]) - -## ## _ -## ## (#Left "Wrong syntax for let'")) -## ## )))) -## ## (def' let' -## ## (check' Macro -## ## (lambda' _ tokens -## ## (lambda' _ state -## ## (#Left "Wrong syntax for let'") -## ## )))) ## (def' let' -## (check' (#AppT [(#AppT [Either Text]) -## (#TupleT (#Cons [CompilerState -## (#Cons [(#AppT [List Syntax]) #Nil])]))]) -## (#Left "Wrong syntax for let'"))) +## (check' Macro +## (lambda' _ tokens +## (lambda' _ state +## (#Left "Wrong syntax for let'") +## )))) ## (def' let' ## (lambda' _ tokens diff --git a/src/lux.clj b/src/lux.clj index 7bee8df16..e035e92c8 100644 --- a/src/lux.clj +++ b/src/lux.clj @@ -11,8 +11,12 @@ ;; TODO: All optimizations ;; TODO: Anonymous classes ;; TODO: - + ;; Finish total-locals + + ;; TODO: Change &type/check to it returns a tuple with the new expected & actual types + ;; TODO: Stop passing-along the exo-types and instead pass-along endo-types where possible + ;; TODO: Optimize analyser to avoid redundant checks when dealing with type-checking (making sure check* is being handed a type) (time (&compiler/compile-all (&/|list "lux"))) (System/gc) diff --git a/src/lux/analyser.clj b/src/lux/analyser.clj index 39eaf9e16..14d5599e4 100644 --- a/src/lux/analyser.clj +++ b/src/lux/analyser.clj @@ -38,19 +38,24 @@ (matchv ::M/objects [token] ;; Standard special forms [["lux;Meta" [meta ["lux;Bool" ?value]]]] - (return (&/|list (&/V "Expression" (&/T (&/V "bool" ?value) &type/Bool)))) + (|do [_ (&type/check exo-type &type/Bool)] + (return (&/|list (&/V "Expression" (&/T (&/V "bool" ?value) exo-type))))) [["lux;Meta" [meta ["lux;Int" ?value]]]] - (return (&/|list (&/V "Expression" (&/T (&/V "int" ?value) &type/Int)))) + (|do [_ (&type/check exo-type &type/Int)] + (return (&/|list (&/V "Expression" (&/T (&/V "int" ?value) exo-type))))) [["lux;Meta" [meta ["lux;Real" ?value]]]] - (return (&/|list (&/V "Expression" (&/T (&/V "real" ?value) &type/Real)))) + (|do [_ (&type/check exo-type &type/Real)] + (return (&/|list (&/V "Expression" (&/T (&/V "real" ?value) exo-type))))) [["lux;Meta" [meta ["lux;Char" ?value]]]] - (return (&/|list (&/V "Expression" (&/T (&/V "char" ?value) &type/Char)))) + (|do [_ (&type/check exo-type &type/Char)] + (return (&/|list (&/V "Expression" (&/T (&/V "char" ?value) exo-type))))) [["lux;Meta" [meta ["lux;Text" ?value]]]] - (return (&/|list (&/V "Expression" (&/T (&/V "text" ?value) &type/Text)))) + (|do [_ (&type/check exo-type &type/Text)] + (return (&/|list (&/V "Expression" (&/T (&/V "text" ?value) exo-type))))) [["lux;Meta" [meta ["lux;Tuple" ?elems]]]] (&&lux/analyse-tuple analyse exo-type ?elems) diff --git a/src/lux/analyser/base.clj b/src/lux/analyser/base.clj index 0d2d8304a..35c12c3e0 100644 --- a/src/lux/analyser/base.clj +++ b/src/lux/analyser/base.clj @@ -37,9 +37,21 @@ (fail "[Analyser Error] Can't expand to other than 2 elements."))))) (defn with-var [k] - (|do [=var &type/fresh-var + (|do [=var &type/create-var =ret (k =var)] (matchv ::M/objects [=ret] [["Expression" [?expr ?type]]] - (|do [=type (&type/clean =var ?type)] - (return (&/V "Expression" (&/T ?expr =type))))))) + (|do [id (&type/var-id =var) + =type (&type/clean id ?type) + :let [_ (prn 'with-var/CLEANING id)] + _ (&type/delete-var id)] + (return (&/V "Expression" (&/T ?expr =type)))) + + [_] + (assert false (pr-str '&&/with-var (aget =ret 0)))))) + +(defmacro with-vars [vars body] + (reduce (fn [b v] + `(with-var (fn [~v] ~b))) + body + (reverse vars))) diff --git a/src/lux/analyser/case.clj b/src/lux/analyser/case.clj index 6b2fe7a03..74d5ea5a3 100644 --- a/src/lux/analyser/case.clj +++ b/src/lux/analyser/case.clj @@ -8,93 +8,116 @@ [env :as &env]))) ;; [Utils] +(defn ^:private resolve-type [type] + (matchv ::M/objects [type] + [["lux;VarT" ?idx]] + (|do [type* (&type/deref ?idx)] + (resolve-type type*)) + + [_] + (&type/actual-type type))) + +(defn ^:private variant-case [case type] + (matchv ::M/objects [type] + [["lux;VariantT" ?cases]] + (if-let [case-type (&/|get case ?cases)] + (return case-type) + (fail (str "[Pattern-maching error] Variant lacks case: " case))) + + [_] + (fail "[Pattern-maching error] Type is not a variant."))) + (defn ^:private analyse-variant [analyse-pattern idx value-type tag value] (|do [[idx* test] (analyse-pattern idx value-type value)] (return (&/T idx* (&/V "VariantTestAC" (&/T tag test)))))) (defn ^:private analyse-pattern [idx value-type pattern] - (prn 'analyse-pattern/pattern (aget pattern 0) (aget pattern 1) (alength (aget pattern 1))) + ;; (prn 'analyse-pattern/pattern (aget pattern 0) (aget pattern 1) (alength (aget pattern 1))) (matchv ::M/objects [pattern] [["lux;Meta" [_ pattern*]]] ;; (assert false) (do ;; (prn 'analyse-pattern/pattern* (aget pattern* 0)) - ;; (when (= "lux;Form" (aget pattern* 0)) - ;; (prn 'analyse-pattern/_2 (aget pattern* 1 0)) ;; "lux;Cons" - ;; (prn 'analyse-pattern/_2 (aget pattern* 1 1 0 0)) ;; "lux;Meta" - ;; (prn 'analyse-pattern/_2 (alength (aget pattern* 1 1 0 1))) - ;; (prn 'analyse-pattern/_2 (aget pattern* 1 1 0 1 1 0)) ;; "lux;Tag" - ;; (prn 'analyse-pattern/_2 [(aget pattern* 1 1 0 1 1 1 0) (aget pattern* 1 1 0 1 1 1 1)]) ;; ["" "Cons"] - ;; (prn 'analyse-pattern/_2 (aget pattern* 1 1 1 0)) ;; "lux;Cons" - ;; (prn 'analyse-pattern/_2 (aget pattern* 1 1 1 1 0)) ;; #<Object[] [Ljava.lang.Object;@63c7c38b> - ;; (prn 'analyse-pattern/_2 (aget pattern* 1 1 1 1 1 0)) ;; "lux;Nil" - ;; ) - ;; ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Tag" [?module ?name]]]] - ;; ["lux;Cons" [?value - ;; ["lux;Nil" _]]]]]] - (matchv ::M/objects [pattern*] - [["lux;Symbol" [?module ?name]]] - (return (&/T (inc idx) (&/V "StoreTestAC" (&/T idx (str ?module ";" ?name) value-type)))) - - [["lux;Bool" ?value]] - (|do [_ (&type/check value-type &type/Bool)] - (return (&/T idx (&/V "BoolTestAC" ?value)))) - - [["lux;Int" ?value]] - (|do [_ (&type/check value-type &type/Int)] - (return (&/T idx (&/V "IntTestAC" ?value)))) - - [["lux;Real" ?value]] - (|do [_ (&type/check value-type &type/Real)] - (return (&/T idx (&/V "RealTestAC" ?value)))) - - [["lux;Char" ?value]] - (|do [_ (&type/check value-type &type/Char)] - (return (&/T idx (&/V "CharTestAC" ?value)))) - - [["lux;Text" ?value]] - (|do [_ (&type/check value-type &type/Text)] - (return (&/T idx (&/V "TextTestAC" ?value)))) - - [["lux;Tuple" ?members]] - (|do [=vars (&/map% (fn [_] &type/fresh-var) - (&/|range (&/|length ?members))) - _ (&type/check value-type (&/V "lux;TupleT" =vars)) - [idx* tests] (&/fold% (fn [idx+subs mv] - (|let [[_idx subs] idx+subs - [?member ?var] mv] - (|do [[idx* test] (analyse-pattern _idx ?var ?member)] - (return (&/T idx* (&/|cons test subs)))))) - (&/T idx (&/|list)) - (&/zip2 ?members =vars))] - (return (&/T idx* (&/V "TupleTestAC" (&/|reverse tests))))) - - [["lux;Record" ?fields]] - (|do [=vars (&/map% (fn [_] &type/fresh-var) - (&/|range (&/|length ?fields))) - _ (&type/check value-type (&/V "lux;RecordT" (&/zip2 (&/|keys ?fields) =vars))) - tests (&/fold% (fn [idx+subs mv] - (|let [[_idx subs] idx+subs - [[slot value] ?var] mv] - (|do [[idx* test] (analyse-pattern _idx ?var value)] - (return (&/T idx* (&/|cons (&/T slot test) subs)))))) - (&/T idx (&/|list)) (&/zip2 ?fields =vars))] - (return (&/V "RecordTestAC" tests))) - - [["lux;Tag" [?module ?name]]] - (|do [module* (if (= "" ?module) - &/get-module-name - (return ?module))] - (analyse-variant analyse-pattern idx value-type (str module* ";" ?name) (&/V "lux;Meta" (&/T (&/T "" -1 -1) - (&/V "lux;Tuple" (&/|list)))))) - - [["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Tag" [?module ?name]]]] - ["lux;Cons" [?value - ["lux;Nil" _]]]]]]] - (|do [module* (if (= "" ?module) - &/get-module-name - (return ?module))] - (analyse-variant analyse-pattern idx value-type (str module* ";" ?name) ?value)) - )) + ;; (when (= "lux;Form" (aget pattern* 0)) + ;; (prn 'analyse-pattern/_2 (aget pattern* 1 0)) ;; "lux;Cons" + ;; (prn 'analyse-pattern/_2 (aget pattern* 1 1 0 0)) ;; "lux;Meta" + ;; (prn 'analyse-pattern/_2 (alength (aget pattern* 1 1 0 1))) + ;; (prn 'analyse-pattern/_2 (aget pattern* 1 1 0 1 1 0)) ;; "lux;Tag" + ;; (prn 'analyse-pattern/_2 [(aget pattern* 1 1 0 1 1 1 0) (aget pattern* 1 1 0 1 1 1 1)]) ;; ["" "Cons"] + ;; (prn 'analyse-pattern/_2 (aget pattern* 1 1 1 0)) ;; "lux;Cons" + ;; (prn 'analyse-pattern/_2 (aget pattern* 1 1 1 1 0)) ;; #<Object[] [Ljava.lang.Object;@63c7c38b> + ;; (prn 'analyse-pattern/_2 (aget pattern* 1 1 1 1 1 0)) ;; "lux;Nil" + ;; ) + ;; ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Tag" [?module ?name]]]] + ;; ["lux;Cons" [?value + ;; ["lux;Nil" _]]]]]] + (matchv ::M/objects [pattern*] + [["lux;Symbol" [?module ?name]]] + (return (&/T (inc idx) (&/V "StoreTestAC" (&/T idx (str ?module ";" ?name) value-type)))) + + [["lux;Bool" ?value]] + (|do [_ (&type/check value-type &type/Bool)] + (return (&/T idx (&/V "BoolTestAC" ?value)))) + + [["lux;Int" ?value]] + (|do [_ (&type/check value-type &type/Int)] + (return (&/T idx (&/V "IntTestAC" ?value)))) + + [["lux;Real" ?value]] + (|do [_ (&type/check value-type &type/Real)] + (return (&/T idx (&/V "RealTestAC" ?value)))) + + [["lux;Char" ?value]] + (|do [_ (&type/check value-type &type/Char)] + (return (&/T idx (&/V "CharTestAC" ?value)))) + + [["lux;Text" ?value]] + (|do [_ (&type/check value-type &type/Text)] + (return (&/T idx (&/V "TextTestAC" ?value)))) + + [["lux;Tuple" ?members]] + (|do [=vars (&/map% (constantly &type/create-var) ?members) + _ (&type/check value-type (&/V "lux;TupleT" =vars)) + [idx* tests] (&/fold% (fn [idx+subs mv] + (|let [[_idx subs] idx+subs + [?member ?var] mv] + (|do [[idx* test] (analyse-pattern _idx ?var ?member)] + (return (&/T idx* (&/|cons test subs)))))) + (&/T idx (&/|list)) + (&/zip2 ?members =vars))] + (return (&/T idx* (&/V "TupleTestAC" (&/|reverse tests))))) + + [["lux;Record" ?fields]] + (|do [=vars (&/map% (constantly &type/create-var) ?fields) + _ (&type/check value-type (&/V "lux;RecordT" (&/zip2 (&/|keys ?fields) =vars))) + tests (&/fold% (fn [idx+subs mv] + (|let [[_idx subs] idx+subs + [[slot value] ?var] mv] + (|do [[idx* test] (analyse-pattern _idx ?var value)] + (return (&/T idx* (&/|cons (&/T slot test) subs)))))) + (&/T idx (&/|list)) (&/zip2 ?fields =vars))] + (return (&/V "RecordTestAC" tests))) + + [["lux;Tag" [?module ?name]]] + (|do [module* (if (= "" ?module) + &/get-module-name + (return ?module)) + :let [=tag (str module* ";" ?name)] + value-type* (resolve-type value-type) + case-type (variant-case =tag value-type*)] + (analyse-variant analyse-pattern idx case-type =tag (&/V "lux;Meta" (&/T (&/T "" -1 -1) + (&/V "lux;Tuple" (&/|list)))))) + + [["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Tag" [?module ?name]]]] + ["lux;Cons" [?value + ["lux;Nil" _]]]]]]] + (|do [module* (if (= "" ?module) + &/get-module-name + (return ?module)) + :let [=tag (str module* ";" ?name)] + value-type* (resolve-type value-type) + case-type (variant-case =tag value-type*)] + (analyse-variant analyse-pattern idx case-type =tag ?value)) + )) )) (defn ^:private with-test [test body] @@ -127,9 +150,9 @@ (let [compare-kv #(compare (aget %1 0) (aget %2 0))] (defn ^:private merge-total [struct test+body] - (prn 'merge-total (aget struct 0) (class test+body)) - (prn 'merge-total (aget struct 0) (aget test+body 0)) - (prn 'merge-total (aget struct 0) (aget test+body 0 0)) + ;; (prn 'merge-total (aget struct 0) (class test+body)) + ;; (prn 'merge-total (aget struct 0) (aget test+body 0)) + ;; (prn 'merge-total (aget struct 0) (aget test+body 0 0)) (matchv ::M/objects [test+body] [[test ?body]] (matchv ::M/objects [struct test] @@ -222,49 +245,41 @@ [["MatchAC" ?tests]] (&/fold% merge-total (&/V "DefaultTotal" false) ?tests)))) -(defn ^:private resolve-type [type] - (matchv ::M/objects [type] - [["lux;VarT" ?idx]] - (&type/deref ?idx) - - [_] - (return type))) - (defn ^:private check-totality [value-type struct] (prn 'check-totality (aget value-type 0) (aget struct 0) (&type/show-type value-type)) - (matchv ::M/objects [value-type struct] - [_ ["BoolTotal" [?total _]]] + (matchv ::M/objects [struct] + [["BoolTotal" [?total _]]] (|do [_ (&type/check value-type &type/Bool)] (return ?total)) - [_ ["IntTotal" [?total _]]] + [["IntTotal" [?total _]]] (|do [_ (&type/check value-type &type/Int)] (return ?total)) - [_ ["RealTotal" [?total _]]] + [["RealTotal" [?total _]]] (|do [_ (&type/check value-type &type/Real)] (return ?total)) - [_ ["CharTotal" [?total _]]] + [["CharTotal" [?total _]]] (|do [_ (&type/check value-type &type/Char)] (return ?total)) - [_ ["TextTotal" [?total _]]] + [["TextTotal" [?total _]]] (|do [_ (&type/check value-type &type/Text)] (return ?total)) - [_ ["TupleTotal" [?total ?structs]]] - (|do [elems-vars (&/map% (constantly &type/fresh-var) (&/|range (&/|length ?structs))) + [["TupleTotal" [?total ?structs]]] + (|do [elems-vars (&/map% (constantly &type/create-var) ?structs) _ (&type/check value-type (&/V "lux;TupleT" elems-vars)) totals (&/map% (fn [sv] - (|let [[struct tvar] sv] - (check-totality tvar struct))) + (|let [[sub-struct tvar] sv] + (check-totality tvar sub-struct))) (&/zip2 ?structs elems-vars))] (return (or ?total (every? true? totals)))) - [_ ["RecordTotal" [?total ?structs]]] - (|do [elems-vars (&/map% (constantly &type/fresh-var) (&/|range (&/|length ?structs))) + [["RecordTotal" [?total ?structs]]] + (|do [elems-vars (&/map% (constantly &type/create-var) ?structs) :let [structs+vars (&/zip2 ?structs elems-vars) record-type (&/V "lux;RecordT" (&/|map (fn [sv] (|let [[[k v] tvar] sv] @@ -278,13 +293,24 @@ (return (or ?total (every? true? totals)))) - [_ ["VariantTotal" [?total ?structs]]] + [["VariantTotal" [?total ?structs]]] (&/try-all% (&/|list (|do [real-type (resolve-type value-type) - :let [_ (prn 'real-type (&type/show-type real-type))]] - (assert false)) + :let [_ (prn 'real-type/_1 (&type/show-type real-type))] + veredicts (matchv ::M/objects [real-type] + [["lux;VariantT" ?cases]] + (&/map% (fn [case] + (|let [[ctag ctype] case] + (if-let [sub-struct (&/|get ctag ?structs)] + (check-totality ctype sub-struct) + (return ?total)))) + ?cases) + + [_] + (fail "[Pattern-maching error] Value is not a variant."))] + (return (&/fold #(and %1 %2) ?total veredicts))) (fail "[Pattern-maching error] Can't pattern-match on an unknown variant type."))) - [_ ["DefaultTotal" true]] + [["DefaultTotal" true]] (return true) )) diff --git a/src/lux/analyser/lambda.clj b/src/lux/analyser/lambda.clj index 619c39766..ae049f50f 100644 --- a/src/lux/analyser/lambda.clj +++ b/src/lux/analyser/lambda.clj @@ -8,7 +8,7 @@ ;; [Resource] (defn with-lambda [self self-type arg arg-type body] ;; (prn 'with-lambda (&/|length self) (&/|length arg)) - (prn 'with-lambda [(aget self 0) (aget self 1)] [(aget arg 0) (aget arg 1)] (alength self) (alength arg)) + ;; (prn 'with-lambda [(aget self 0) (aget self 1)] [(aget arg 0) (aget arg 1)] (alength self) (alength arg)) (|let [[?module1 ?name1] self [?module2 ?name2] arg] (&/with-closure diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj index a9a42ffe3..32f65320a 100644 --- a/src/lux/analyser/lux.clj +++ b/src/lux/analyser/lux.clj @@ -19,9 +19,9 @@ ;; [Exports] (defn analyse-tuple [analyse exo-type ?elems] - (prn 'analyse-tuple (str "[" (->> ?elems (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")) "]") - (&type/show-type exo-type)) - (|do [members-vars (&/map% (constantly &type/fresh-var) ?elems) + ;; (prn 'analyse-tuple (str "[" (->> ?elems (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")) "]") + ;; (&type/show-type exo-type)) + (|do [members-vars (&/map% (constantly &type/create-var) ?elems) _ (&type/check exo-type (&/V "lux;TupleT" members-vars)) =elems (&/map% (fn [ve] (|let [[=var elem] ve] @@ -36,8 +36,8 @@ (defn analyse-variant [analyse exo-type ident ?value] (|let [[?module ?name] ident] - (do (prn 'analyse-variant (str ?module ";" ?name) (&/show-ast ?value)) - (|do [:let [_ (prn 'analyse-variant/exo-type (&type/show-type exo-type))] + (do ;; (prn 'analyse-variant (str ?module ";" ?name) (&/show-ast ?value)) + (|do [;; :let [_ (prn 'analyse-variant/exo-type (&type/show-type exo-type))] module (if (= "" ?module) &/get-module-name (return ?module)) @@ -53,13 +53,15 @@ [_] (&type/actual-type exo-type)) - :let [_ (prn 'exo-type* (&type/show-type exo-type*))]] + ;; :let [_ (prn 'analyse-variant/exo-type* (&type/show-type exo-type*))] + ] (matchv ::M/objects [exo-type*] [["lux;VariantT" ?cases]] (if-let [vtype (&/|get ?tag ?cases)] - (|do [:let [_ (prn 'VARIANT_BODY ?tag (&/show-ast ?value) (&type/show-type vtype))] + (|do [;; :let [_ (prn 'VARIANT_BODY ?tag (&/show-ast ?value) (&type/show-type vtype))] =value (&&/analyse-1 analyse vtype ?value) - :let [_ (prn 'GOT_VALUE =value)]] + ;; :let [_ (prn 'GOT_VALUE =value)] + ] (return (&/|list (&/V "Expression" (&/T (&/V "variant" (&/T ?tag =value)) exo-type))))) (fail (str "[Analyser Error] There is no case " ?tag " for variant type " (&type/show-type exo-type*)))) @@ -178,47 +180,79 @@ _ (&/assert! (> num-branches 0) "[Analyser Error] Can't have empty branches in \"case'\" expression.") _ (&/assert! (even? num-branches) "[Analyser Error] Unbalanced branches in \"case'\" expression.") =value ((analyse-1+ analyse) ?value) + :let [_ (prn 'analyse-case/GOT_VALUE)] =value-type (&&/expr-type =value) - =match (&&case/analyse-branches analyse exo-type =value-type (&/|as-pairs ?branches))] + =match (&&case/analyse-branches analyse exo-type =value-type (&/|as-pairs ?branches)) + :let [_ (prn 'analyse-case/GOT_MATCH)]] (return (&/|list (&/V "Expression" (&/T (&/V "case" (&/T =value =match)) exo-type)))))) -(defn analyse-lambda [analyse exo-type ?self ?arg ?body] +(defn analyse-lambda* [analyse exo-type ?self ?arg ?body] ;; (prn 'analyse-lambda ?self ?arg ?body) - (|do [=lambda-type* &type/fresh-lambda - _ (&type/check exo-type =lambda-type*)] - (matchv ::M/objects [=lambda-type*] - [["lux;LambdaT" [=arg =return]]] - (|do [[=scope =captured =body] (&&lambda/with-lambda ?self =lambda-type* - ?arg =arg - (&&/analyse-1 analyse =return ?body)) - =lambda-type** (&type/clean =return =lambda-type*) - =lambda-type (matchv ::M/objects [=arg] - [["lux;VarT" ?id]] - (&/try-all% (&/|list (|do [bound (&type/deref ?id)] - (&type/clean =arg =lambda-type**)) - (let [var-name (str (gensym ""))] - (|do [_ (&type/set-var ?id (&/V "lux;BoundT" var-name)) - lambda-type (&type/clean =arg =lambda-type**)] - (return (&/V "lux;AllT" (&/T (&/|list) "" var-name lambda-type))))))) + (|do [lambda-expr (&&/with-vars [=arg =return] + (|do [:let [_ (prn 'analyse-lambda/_-1 (&type/show-type =arg) (&type/show-type =return))] + :let [=lambda-type* (&/V "lux;LambdaT" (&/T =arg =return))] + :let [_ (prn 'analyse-lambda/_0)] + _ (&type/check exo-type =lambda-type*) + :let [_ (prn 'analyse-lambda/_0.5 (&type/show-type exo-type))] + :let [_ (prn 'analyse-lambda/_1 (&type/show-type =lambda-type*))] + _ (|do [aid (&type/var-id =arg) + atype (&type/deref aid) + rid (&type/var-id =return) + rtype (&type/deref rid) + :let [_ (prn 'analyse-lambda/_1.5 (&type/show-type atype) (&type/show-type rtype))]] + (return nil)) + [=scope =captured =body] (&&lambda/with-lambda ?self =lambda-type* + ?arg =arg + (&&/analyse-1 analyse =return ?body)) + :let [_ (prn 'analyse-lambda/_2)] + =lambda-type (matchv ::M/objects [=arg] + [["lux;VarT" ?id]] + (|do [? (&type/bound? ?id)] + (if ? + (return =lambda-type*) + (let [var-name (str (gensym ""))] + (|do [_ (&type/set-var ?id (&/V "lux;BoundT" var-name))] + (return (&/V "lux;AllT" (&/T (&/|list) "" var-name =lambda-type*))))))) + + [_] + (fail "")) + :let [_ (prn 'analyse-lambda/_3 (&type/show-type =lambda-type))]] + (return (&/V "Expression" (&/T (&/V "lambda" (&/T =scope =captured =body)) =lambda-type))))) + :let [_ (prn 'analyse-lambda/_4)]] + (return lambda-expr))) - [_] - (fail ""))] - (return (&/|list (&/V "Expression" (&/T (&/V "lambda" (&/T =scope =captured =body)) =lambda-type)))))))) +(defn analyse-lambda [analyse exo-type ?self ?arg ?body] + (prn 'analyse-lambda/&& (aget exo-type 0)) + (|do [output (matchv ::M/objects [exo-type] + [["lux;AllT" _]] + (&&/with-var + (fn [$arg] + (|do [exo-type* (&type/apply-type exo-type $arg) + outputs (analyse-lambda analyse exo-type* ?self ?arg ?body)] + (return (&/|head outputs))))) + + [_] + (analyse-lambda* analyse exo-type ?self ?arg ?body))] + (return (&/|list output)))) (defn analyse-def [analyse exo-type ?name ?value] - (prn 'analyse-def ?name (&/show-ast ?value)) + ;; (prn 'analyse-def/CODE ?name (&/show-ast ?value)) (|do [_ (&type/check exo-type &type/Nothing) module-name &/get-module-name ? (&&def/defined? module-name ?name)] (if ? (fail (str "[Analyser Error] Can't redefine " ?name)) - (|do [=value (&/with-scope ?name + (|do [:let [_ (prn 'analyse-def/_0)] + =value (&/with-scope ?name (&&/with-var #(&&/analyse-1 analyse % ?value))) + :let [_ (prn 'analyse-def/_1)] =value-type (&&/expr-type =value) - :let [_ (prn 'analyse-def ?name (&type/show-type =value-type))] - _ (&&def/define module-name ?name =value-type)] + :let [_ (prn 'analyse-def/_2)] + ;; :let [_ (prn 'analyse-def/TYPE ?name (&type/show-type =value-type))] + _ (&&def/define module-name ?name =value-type) + :let [_ (prn 'analyse-def/_3)]] (return (&/|list (&/V "Statement" (&/V "def" (&/T ?name =value))))))))) (defn analyse-declare-macro [exo-type ident] @@ -241,12 +275,12 @@ ==type (eval! =type) _ (&type/check exo-type ==type) :let [_ (println "analyse-check#4" (&type/show-type ==type))] - =value (&&/analyse-1 analyse exo-type ?value) + =value (&&/analyse-1 analyse ==type ?value) :let [_ (println "analyse-check#5")]] (matchv ::M/objects [=value] [["Expression" [?expr ?expr-type]]] (|do [:let [_ (println "analyse-check#6" (&type/show-type ?expr-type))] - _ (&type/check ==type ?expr-type) + ;; _ (&type/check ==type ?expr-type) :let [_ (println "analyse-check#7")]] (return (&/|list (&/V "Expression" (&/T ?expr ==type)))))))) diff --git a/src/lux/base.clj b/src/lux/base.clj index 91519eb0c..f9d3c9c23 100644 --- a/src/lux/base.clj +++ b/src/lux/base.clj @@ -87,6 +87,16 @@ (V "lux;Cons" (T (T slot value) table*)) (V "lux;Cons" (T (T k v) (|put slot value table*)))))) +(defn |remove [slot table] + (matchv ::M/objects [table] + [["lux;Nil" _]] + table + + [["lux;Cons" [[k v] table*]]] + (if (= k slot) + table* + (V "lux;Cons" (T (T k v) (|remove slot table*)))))) + (defn |merge [table1 table2] ;; (prn '|merge (aget table1 0) (aget table2 0)) (matchv ::M/objects [table2] @@ -125,7 +135,7 @@ ;; [Resources/Monads] (defn fail [message] (fn [_] - (prn 'FAIL message) + ;; (prn 'FAIL message) (V "lux;Left" message))) (defn return [value] diff --git a/src/lux/type.clj b/src/lux/type.clj index 0cd839cf2..4eeea30aa 100644 --- a/src/lux/type.clj +++ b/src/lux/type.clj @@ -7,6 +7,42 @@ (declare show-type) ;; [Util] +(def Any (&/V "lux;AnyT" nil)) +(def Nothing (&/V "lux;NothingT" nil)) +(def Bool (&/V "lux;DataT" "java.lang.Boolean")) +(def Int (&/V "lux;DataT" "java.lang.Long")) +(def Real (&/V "lux;DataT" "java.lang.Double")) +(def Char (&/V "lux;DataT" "java.lang.Character")) +(def Text (&/V "lux;DataT" "java.lang.String")) +(def Unit (&/V "lux;TupleT" (&/|list))) + +(def List + (&/V "lux;AllT" (&/T (&/|table) "List" "a" + (&/V "lux;VariantT" (&/|list (&/T "lux;Nil" (&/V "lux;TupleT" (&/|list))) + (&/T "lux;Cons" (&/V "lux;TupleT" (&/|list (&/V "lux;BoundT" "a") + (&/V "lux;AppT" (&/T (&/V "lux;BoundT" "List") + (&/V "lux;BoundT" "a"))))))))))) + +(def Type + (let [Type (&/V "lux;AppT" (&/T (&/V "lux;BoundT" "Type") (&/V "lux;BoundT" "_"))) + TypeEnv (&/V "lux;AppT" (&/T List (&/V "lux;TupleT" (&/|list Text Type)))) + Unit (&/V "lux;TupleT" (&/|list)) + TypePair (&/V "lux;TupleT" (&/|list Type Type))] + (&/V "lux;AppT" (&/T (&/V "lux;AllT" (&/T (&/|list) "Type" "_" + (&/V "lux;VariantT" (&/|list (&/T "lux;AnyT" Unit) + (&/T "lux;NothingT" Unit) + (&/T "lux;DataT" Text) + (&/T "lux;TupleT" (&/V "lux;AppT" (&/T List Type))) + (&/T "lux;VariantT" TypeEnv) + (&/T "lux;RecordT" TypeEnv) + (&/T "lux;LambdaT" TypePair) + (&/T "lux;BoundT" Text) + (&/T "lux;VarT" Int) + (&/T "lux;AllT" (&/V "lux;TupleT" (&/|list TypeEnv Text Text Type))) + (&/T "lux;AppT" TypePair) + )))) + (&/V "lux;NothingT" nil))))) + (defn bound? [id] (fn [state] (if-let [type* (->> state (&/get$ "lux;types") (&/get$ "lux;mappings") (&/|get id))] @@ -16,21 +52,21 @@ [["lux;None" _]] (return* state false)) - (fail* (str "Unknown type-var: " id))))) + (fail* (str "[Type Error] Unknown type-var: " id))))) (defn deref [id] (fn [state] (let [mappings (->> state (&/get$ "lux;types") (&/get$ "lux;mappings"))] (do (prn 'deref/mappings (&/->seq (&/|keys mappings))) (if-let [type* (->> mappings (&/|get id))] - (do (prn 'deref/type* (aget type* 0)) + (do ;; (prn 'deref/type* (aget type* 0)) (matchv ::M/objects [type*] [["lux;Some" type]] (return* state type) [["lux;None" _]] - (fail* (str "Unbound type-var: " id)))) - (fail* (str "Unknown type-var: " id))))))) + (fail* (str "[Type Error] Unbound type-var: " id)))) + (fail* (str "[Type Error] Unknown type-var: " id))))))) (defn set-var [id type] (fn [state] @@ -38,17 +74,17 @@ (do ;; (prn 'set-var (aget tvar 0)) (matchv ::M/objects [tvar] [["lux;Some" bound]] - (fail* (str "Can't rebind type var: " id " | Current type: " (show-type bound))) + (fail* (str "[Type Error] Can't rebind type var: " id " | Current type: " (show-type bound))) [["lux;None" _]] (return* (&/update$ "lux;types" (fn [ts] (&/update$ "lux;mappings" #(&/|put id (&/V "lux;Some" type) %) ts)) state) nil))) - (fail* (str "Unknown type-var: " id))))) + (fail* (str "[Type Error] Unknown type-var: " id))))) ;; [Exports] -(def fresh-var +(def create-var (fn [state] (let [id (->> state (&/get$ "lux;types") (&/get$ "lux;counter"))] (return* (&/update$ "lux;types" #(->> % @@ -57,59 +93,79 @@ state) (&/V "lux;VarT" id))))) -(def fresh-lambda - (|do [=arg fresh-var - =return fresh-var] - (return (&/V "lux;LambdaT" (&/T =arg =return))))) - -(defn clean [tvar type] - (matchv ::M/objects [tvar] - [["lux;VarT" ?tid]] - (matchv ::M/objects [type] - [["lux;VarT" ?id]] - (if (= ?tid ?id) - (|do [=type (deref ?id)] - (clean tvar =type)) - (return type)) - - [["lux;LambdaT" [?arg ?return]]] - (|do [=arg (clean tvar ?arg) - =return (clean tvar ?return)] - (return (&/V "lux;LambdaT" (&/T =arg =return)))) - - [["lux;AppT" [?lambda ?param]]] - (|do [=lambda (clean tvar ?lambda) - =param (clean tvar ?param)] - (return (&/V "lux;AppT" (&/T =lambda =param)))) - - [["lux;TupleT" ?members]] - (|do [=members (&/map% (partial clean tvar) ?members)] - (return (&/V "lux;TupleT" =members))) - - [["lux;VariantT" ?members]] - (|do [=members (&/map% (fn [[k v]] - (|do [=v (clean tvar v)] - (return (&/T k =v)))) - ?members)] - (return (&/V "lux;VariantT" =members))) - - [["lux;RecordT" ?members]] - (|do [=members (&/map% (fn [[k v]] - (|do [=v (clean tvar v)] - (return (&/T k =v)))) - ?members)] - (return (&/V "lux;RecordT" =members))) - - [["lux;AllT" [?env ?name ?arg ?body]]] - (|do [=env (&/map% (fn [[k v]] - (|do [=v (clean tvar v)] - (return (&/T k =v)))) - ?env)] - (return (&/V "lux;AllT" (&/T =env ?name ?arg ?body)))) - - [_] - (return type) - ))) +(defn delete-var [id] + (fn [state] + (prn 'delete-var id) + (if-let [tvar (->> state (&/get$ "lux;types") (&/get$ "lux;mappings") (&/|get id))] + (return* (&/update$ "lux;types" (fn [ts] (&/update$ "lux;mappings" #(&/|remove id %) + ts)) + state) + nil) + (fail* (str "[Type Error] Unknown type-var: " id))))) + +(defn var-id [type] + (matchv ::M/objects [type] + [["lux;VarT" ?id]] + (return ?id) + + [_] + (fail (str "[Type Error] Not type-var: " (show-type type))))) + +(defn clean [?tid type] + (matchv ::M/objects [type] + [["lux;VarT" ?id]] + (if (= ?tid ?id) + (|do [=type (deref ?id)] + (clean ?tid =type)) + (return type)) + + [["lux;LambdaT" [?arg ?return]]] + (|do [=arg (clean ?tid ?arg) + =return (clean ?tid ?return)] + (return (&/V "lux;LambdaT" (&/T =arg =return)))) + + [["lux;AppT" [?lambda ?param]]] + (|do [=lambda (clean ?tid ?lambda) + =param (clean ?tid ?param)] + (return (&/V "lux;AppT" (&/T =lambda =param)))) + + [["lux;TupleT" ?members]] + (|do [=members (&/map% (partial clean ?tid) ?members)] + (return (&/V "lux;TupleT" =members))) + + [["lux;VariantT" ?members]] + (|do [=members (&/map% (fn [[k v]] + (|do [=v (clean ?tid v)] + (return (&/T k =v)))) + ?members)] + (return (&/V "lux;VariantT" =members))) + + [["lux;RecordT" ?members]] + (|do [=members (&/map% (fn [[k v]] + (|do [=v (clean ?tid v)] + (return (&/T k =v)))) + ?members)] + (return (&/V "lux;RecordT" =members))) + + [["lux;AllT" [?env ?name ?arg ?body]]] + (|do [=env (&/map% (fn [[k v]] + (|do [=v (clean ?tid v)] + (return (&/T k =v)))) + ?env) + body* (clean ?tid ?body)] + (return (&/V "lux;AllT" (&/T =env ?name ?arg body*)))) + + [_] + (return type) + )) + +(defn with-var [k] + (|do [=var create-var + id (var-id =var) + type (k =var)] + (|do [type* (clean id type) + _ (delete-var id)] + (return type*)))) (defn show-type [type] ;; (prn 'show-type (aget type 0)) @@ -167,80 +223,88 @@ )) (defn type= [x y] - (matchv ::M/objects [x y] - [["lux;AnyT" _] ["lux;AnyT" _]] - true - - [["lux;NothingT" _] ["lux;NothingT" _]] - true - - [["lux;DataT" xname] ["lux;DataT" yname]] - (= xname yname) - - [["lux;TupleT" xelems] ["lux;TupleT" yelems]] - (&/fold (fn [old xy] (and old (type= (aget xy 0) (aget xy 1)))) - true - (&/zip2 xelems yelems)) - - [["lux;VariantT" xcases] ["lux;VariantT" ycases]] - (&/fold (fn [old cases] - (matchv ::M/objects [cases] - [[[xtag xtype] [ytag ytype]]] - (and (= xtag ytag) - (type= xtype ytype)))) - true (&/zip2 xcases ycases)) - - - [["lux;RecordT" xfields] ["lux;RecordT" yfields]] - (&/fold (fn [old cases] - (matchv ::M/objects [cases] - [[[xtag xtype] [ytag ytype]]] - (and (= xtag ytag) - (type= xtype ytype)))) - true (&/zip2 xfields yfields)) - - [["lux;LambdaT" [xinput xoutput]] ["lux;LambdaT" [yinput youtput]]] - (and (type= xinput yinput) - (type= xoutput youtput)) - - [["lux;VarT" xid] ["lux;VarT" yid]] - (= xid yid) - - [["lux;BoundT" xname] ["lux;BoundT" yname]] - (= xname yname) - - [["lux;AppT" [xlambda xparam]] ["lux;AppT" [ylambda yparam]]] - (and (type= xlambda ylambda) - (type= xparam yparam)) - - [["lux;AllT" [xenv xname xarg xbody]] ["lux;AllT" [yenv yname yarg ybody]]] - (and (&/fold (fn [old cases] - (matchv ::M/objects [cases] - [[[xtag xtype] [ytag ytype]]] - (and (= xtag ytag) - (type= xtype ytype)))) - true (&/zip2 xenv yenv)) - (= xname yname) - (= xarg yarg) - (type= xbody ybody)) - - [_ _] - (do ;; (prn 'type= (show-type x) (show-type y)) - false) - )) - -(defn ^:private fp-get [k xs] - (matchv ::M/objects [k] - [[e a]] - (matchv ::M/objects [xs] + (let [output (matchv ::M/objects [x y] + [["lux;AnyT" _] ["lux;AnyT" _]] + true + + [["lux;NothingT" _] ["lux;NothingT" _]] + true + + [["lux;DataT" xname] ["lux;DataT" yname]] + (= xname yname) + + [["lux;TupleT" xelems] ["lux;TupleT" yelems]] + (&/fold (fn [old xy] + (|let [[x* y*] xy] + (and old + (type= x* y*)))) + true + (&/zip2 xelems yelems)) + + [["lux;VariantT" xcases] ["lux;VariantT" ycases]] + (and (= (&/|length xcases) (&/|length ycases)) + (&/fold (fn [old case] + (and old + (type= (&/|get case xcases) (&/|get case ycases)))) + true + (&/|keys xcases))) + + [["lux;RecordT" xfields] ["lux;RecordT" yfields]] + (and (= (&/|length xfields) (&/|length yfields)) + (&/fold (fn [old field] + (and old + (type= (&/|get field xfields) (&/|get field yfields)))) + true + (&/|keys xfields))) + + [["lux;LambdaT" [xinput xoutput]] ["lux;LambdaT" [yinput youtput]]] + (and (type= xinput yinput) + (type= xoutput youtput)) + + [["lux;VarT" xid] ["lux;VarT" yid]] + (= xid yid) + + [["lux;BoundT" xname] ["lux;BoundT" yname]] + (= xname yname) + + [["lux;AppT" [xlambda xparam]] ["lux;AppT" [ylambda yparam]]] + (and (type= xlambda ylambda) + (type= xparam yparam)) + + [["lux;AllT" [xenv xname xarg xbody]] ["lux;AllT" [yenv yname yarg ybody]]] + (do ;; (prn 'TESTING_ALLT + ;; 'NAME [xname yname] (= xname yname) + ;; 'ARG (= xarg yarg) + ;; 'LENGTH [(&/|length xenv) (&/|length yenv)] (= (&/|length xenv) (&/|length yenv))) + (and (= xname yname) + (= xarg yarg) + (type= xbody ybody) + ;; (= (&/|length xenv) (&/|length yenv)) + ;; (&/fold (fn [old bname] + ;; (and old + ;; (type= (&/|get bname xenv) (&/|get bname yenv)))) + ;; true + ;; (&/|keys xenv)) + )) + + [_ _] + (do (prn 'type= (show-type x) (show-type y)) + false) + )] + ;; (prn 'type= output (show-type x) (show-type y)) + output)) + +(defn ^:private fp-get [k fixpoints] + (|let [[e a] k] + (matchv ::M/objects [fixpoints] [["lux;Nil" _]] (&/V "lux;None" nil) - [["lux;Cons" [[[e* a*] v*] xs*]]] + [["lux;Cons" [[[e* a*] v*] fixpoints*]]] (if (and (type= e e*) (type= a a*)) (&/V "lux;Some" v*) - (fp-get k xs*)) + (fp-get k fixpoints*)) ))) (defn ^:private fp-put [k v fixpoints] @@ -315,7 +379,7 @@ (def init-fixpoints (&/|list)) (defn ^:private check* [fixpoints expected actual] - (prn 'check* (aget expected 0) (aget actual 0)) + ;; (prn 'check* (aget expected 0) (aget actual 0)) ;; (prn 'check* (show-type expected) (show-type actual)) (matchv ::M/objects [expected actual] [["lux;AnyT" _] _] @@ -347,8 +411,17 @@ (check* fixpoints expected bound)))) [["lux;AppT" [F A]] _] - (|do [expected* (apply-type F A) - :let [fp-pair (&/T expected actual)]] + (let [fp-pair (&/T expected actual) + _ (prn 'LEFT_APP (&/|length fixpoints)) + _ (when (> (&/|length fixpoints) 10) + (println 'FIXPOINTS (->> (&/|keys fixpoints) + (&/|map (fn [pair] + (|let [[e a] pair] + (str (show-type e) ":+:" + (show-type a))))) + (&/|interpose "\n\n") + (&/fold str ""))) + (assert false))] (matchv ::M/objects [(fp-get fp-pair fixpoints)] [["lux;Some" ?]] (if ? @@ -356,21 +429,34 @@ (fail (check-error expected actual))) [["lux;None" _]] - (check* (fp-put fp-pair true fixpoints) expected* actual))) + (|do [expected* (apply-type F A)] + (check* (fp-put fp-pair true fixpoints) expected* actual)))) [_ ["lux;AppT" [F A]]] (|do [actual* (apply-type F A)] (check* fixpoints expected actual*)) [["lux;AllT" _] _] - (|do [$var fresh-var - expected* (apply-type expected $var)] - (check* fixpoints expected* actual)) + (with-var + (fn [$arg] + (|do [expected* (apply-type expected $arg)] + (check* fixpoints expected* actual)))) [_ ["lux;AllT" _]] - (|do [$var fresh-var - actual* (apply-type actual $var)] - (check* fixpoints expected actual*)) + (with-var + (fn [$arg] + (|do [actual* (apply-type actual $arg)] + (check* fixpoints expected actual*)))) + + ;; [["lux;AllT" _] _] + ;; (|do [$arg create-var + ;; expected* (apply-type expected $arg)] + ;; (check* fixpoints expected* actual)) + + ;; [_ ["lux;AllT" _]] + ;; (|do [$arg create-var + ;; actual* (apply-type actual $arg)] + ;; (check* fixpoints expected actual*)) [["lux;DataT" e!name] ["lux;DataT" a!name]] (if (= e!name a!name) @@ -382,8 +468,8 @@ (check* fixpoints* eO aO)) [["lux;TupleT" e!members] ["lux;TupleT" a!members]] - (do (do (prn 'e!members (&/|length e!members)) - (prn 'a!members (&/|length a!members))) + (do ;; (do (prn 'e!members (&/|length e!members)) + ;; (prn 'a!members (&/|length a!members))) (if (= (&/|length e!members) (&/|length a!members)) (|do [fixpoints* (&/fold% (fn [fixp ea] (|let [[e a] ea] @@ -405,7 +491,7 @@ [["lux;VariantT" e!cases] ["lux;VariantT" a!cases]] (if (= (&/|length e!cases) (&/|length a!cases)) (|do [fixpoints* (&/fold% (fn [fixp slot] - (prn "lux;VariantT" slot) + (prn 'VARIANT_CASE slot) (if-let [e!type (&/|get slot e!cases)] (if-let [a!type (&/|get slot a!cases)] (|do [[fixp* _] (check* fixp e!type a!type)] @@ -420,7 +506,7 @@ [["lux;RecordT" e!fields] ["lux;RecordT" a!fields]] (if (= (&/|length e!fields) (&/|length a!fields)) (|do [fixpoints* (&/fold% (fn [fixp slot] - (prn "lux;RecordT" slot) + (prn 'RECORD_FIELD slot) (if-let [e!type (&/|get slot e!fields)] (if-let [a!type (&/|get slot a!fields)] (|do [[fixp* _] (check* fixp e!type a!type)] @@ -456,9 +542,10 @@ (return output)) [["lux;AllT" [local-env local-name local-arg local-def]]] - (|do [$var fresh-var - func* (apply-type func $var)] - (apply-lambda func* param)) + (with-var + (fn [$arg] + (|do [func* (apply-type func $arg)] + (apply-lambda func* param)))) [_] (fail (str "[Type System] Can't apply type " (show-type func) " to type " (show-type param))) @@ -473,39 +560,3 @@ [_] (return type) )) - -(def Any (&/V "lux;AnyT" nil)) -(def Nothing (&/V "lux;NothingT" nil)) -(def Bool (&/V "lux;DataT" "java.lang.Boolean")) -(def Int (&/V "lux;DataT" "java.lang.Long")) -(def Real (&/V "lux;DataT" "java.lang.Double")) -(def Char (&/V "lux;DataT" "java.lang.Character")) -(def Text (&/V "lux;DataT" "java.lang.String")) -(def Unit (&/V "lux;TupleT" (&/|list))) - -(def List - (&/V "lux;AllT" (&/T (&/|table) "List" "a" - (&/V "lux;VariantT" (&/|list (&/T "lux;Nil" (&/V "lux;TupleT" (&/|list))) - (&/T "lux;Cons" (&/V "lux;TupleT" (&/|list (&/V "lux;BoundT" "a") - (&/V "lux;AppT" (&/T (&/V "lux;BoundT" "List") - (&/V "lux;BoundT" "a"))))))))))) - -(def Type - (let [Type (&/V "lux;AppT" (&/T (&/V "lux;BoundT" "Type") (&/V "lux;BoundT" "_"))) - TypeEnv (&/V "lux;AppT" (&/T List (&/V "lux;TupleT" (&/|list Text Type)))) - Unit (&/V "lux;TupleT" (&/|list)) - TypePair (&/V "lux;TupleT" (&/|list Type Type))] - (&/V "lux;AppT" (&/T (&/V "lux;AllT" (&/T (&/|list) "Type" "_" - (&/V "lux;VariantT" (&/|list (&/T "lux;AnyT" Unit) - (&/T "lux;NothingT" Unit) - (&/T "lux;DataT" Text) - (&/T "lux;TupleT" (&/V "lux;AppT" (&/T List Type))) - (&/T "lux;VariantT" TypeEnv) - (&/T "lux;RecordT" TypeEnv) - (&/T "lux;LambdaT" TypePair) - (&/T "lux;BoundT" Text) - (&/T "lux;VarT" Int) - (&/T "lux;AllT" (&/V "lux;TupleT" (&/|list TypeEnv Text Text Type))) - (&/T "lux;AppT" TypePair) - )))) - (&/V "lux;NothingT" nil))))) |