diff options
| -rw-r--r-- | source/lux.lux | 58 | ||||
| -rw-r--r-- | src/lux/type.clj | 85 |
2 files changed, 86 insertions, 57 deletions
diff --git a/source/lux.lux b/source/lux.lux index a005da3da..aab80ed7e 100644 --- a/source/lux.lux +++ b/source/lux.lux @@ -22,11 +22,14 @@ (def' Text (#DataT "java.lang.String")) (export' Text) +(def' Void (#VariantT #Nil)) +(export' Void) + ## (deftype (List a) ## (| #Nil ## (#Cons (, a (List a))))) (def' List - (#AllT [#Nil "List" "a" + (#AllT [#None "List" "a" (#VariantT (#Cons [["lux;Nil" (#TupleT #Nil)] (#Cons [["lux;Cons" (#TupleT (#Cons [(#BoundT "a") (#Cons [(#AppT [(#BoundT "List") (#BoundT "a")]) @@ -34,6 +37,16 @@ #Nil])]))])) (export' List) +## (deftype (Maybe a) +## (| #None +## (#Some a))) +(def' Maybe + (#AllT [#None "Maybe" "a" + (#VariantT (#Cons [["lux;None" (#TupleT #Nil)] + (#Cons [["lux;Some" (#BoundT "a")] + #Nil])]))])) +(export' Maybe) + ## (deftype #rec Type ## (| #AnyT ## #NothingT @@ -44,47 +57,36 @@ ## (#LambdaT (, Type Type)) ## (#BoundT Text) ## (#VarT Int) -## (#AllT (, (List (, Text Type)) Text Text Type)) +## (#AllT (, (Maybe (List (, Text Type))) Text Text Type)) ## (#AppT (, Type Type)))) (def' Type (case' (#AppT [(#BoundT "Type") (#BoundT "")]) Type (case' (#AppT [List (#TupleT (#Cons [Text (#Cons [Type #Nil])]))]) TypeEnv - (#AppT [(#AllT [#Nil "Type" "" + (#AppT [(#AllT [#None "Type" "" (#VariantT (#Cons [["lux;AnyT" (#TupleT #Nil)] (#Cons [["lux;NothingT" (#TupleT #Nil)] (#Cons [["lux;DataT" Text] - (#Cons [["lux;TupleT" (#AppT [List (#AppT [(#BoundT "Type") (#BoundT "")])])] + (#Cons [["lux;TupleT" (#AppT [List Type])] (#Cons [["lux;VariantT" TypeEnv] (#Cons [["lux;RecordT" TypeEnv] (#Cons [["lux;LambdaT" (#TupleT (#Cons [Type (#Cons [Type #Nil])]))] (#Cons [["lux;BoundT" Text] (#Cons [["lux;VarT" Int] - (#Cons [["lux;AllT" (#TupleT (#Cons [TypeEnv (#Cons [Text (#Cons [Text (#Cons [Type #Nil])])])]))] + (#Cons [["lux;AllT" (#TupleT (#Cons [(#AppT [Maybe TypeEnv]) (#Cons [Text (#Cons [Text (#Cons [Type #Nil])])])]))] (#Cons [["lux;AppT" (#TupleT (#Cons [Type (#Cons [Type #Nil])]))] #Nil])])])])])])])])])])]))]) #NothingT])))) (export' Type) -## (deftype (Maybe a) -## (| #None -## (#Some a))) -(def' Maybe - (:' Type - (#AllT [#Nil "Maybe" "a" - (#VariantT (#Cons [["lux;None" (#TupleT #Nil)] - (#Cons [["lux;Some" (#BoundT "a")] - #Nil])]))]))) -(export' Maybe) - ## (deftype (Bindings k v) ## (& #counter Int ## #mappings (List (, k v)))) (def' Bindings (:' Type - (#AllT [#Nil "Bindings" "k" - (#AllT [#Nil "" "v" + (#AllT [#None "Bindings" "k" + (#AllT [#None "" "v" (#RecordT (#Cons [["lux;counter" Int] (#Cons [["lux;mappings" (#AppT [List (#TupleT (#Cons [(#BoundT "k") @@ -99,8 +101,8 @@ ## #closure (Bindings k v))) (def' Env (:' Type - (#AllT [#Nil "Env" "k" - (#AllT [#Nil "" "v" + (#AllT [#None "Env" "k" + (#AllT [#None "" "v" (#RecordT (#Cons [["lux;name" Text] (#Cons [["lux;inner-closures" Int] (#Cons [["lux;locals" (#AppT [(#AppT [Bindings (#BoundT "k")]) @@ -119,8 +121,8 @@ ## (| (#Meta (, m v)))) (def' Meta (:' Type - (#AllT [#Nil "Meta" "m" - (#AllT [#Nil "" "v" + (#AllT [#None "Meta" "m" + (#AllT [#None "" "v" (#VariantT (#Cons [["lux;Meta" (#TupleT (#Cons [(#BoundT "m") (#Cons [(#BoundT "v") #Nil])]))] @@ -186,7 +188,7 @@ Syntax'List (case' (#TupleT (#Cons [Text (#Cons [Text #Nil])])) Ident - (#AllT [#Nil "Syntax'" "w" + (#AllT [#None "Syntax'" "w" (#VariantT (#Cons [["lux;Bool" Bool] (#Cons [["lux;Int" Int] (#Cons [["lux;Real" Real] @@ -217,8 +219,8 @@ ## (#Right r))) (def' Either (:' Type - (#AllT [#Nil "_" "l" - (#AllT [#Nil "" "r" + (#AllT [#None "_" "l" + (#AllT [#None "" "r" (#VariantT (#Cons [["lux;Left" (#BoundT "l")] (#Cons [["lux;Right" (#BoundT "r")] #Nil])]))])]))) @@ -452,7 +454,7 @@ (#Cons [(#Meta [_ (#Tuple (#Cons [(#Meta [_ (#Symbol ["" arg-name])]) other-args]))]) (#Cons [body #Nil])]) (return' (#Cons [(_meta (#Form (#Cons [(_meta (#Tag ["lux" "AllT"])) - (#Cons [(_meta (#Tuple (#Cons [(_meta (#Tag ["lux" "Nil"])) + (#Cons [(_meta (#Tuple (#Cons [(_meta (#Tag ["lux" "None"])) (#Cons [(_meta (#Text "")) (#Cons [(_meta (#Text arg-name)) (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["lux" "All'"])) @@ -760,7 +762,7 @@ ## (lambda [body arg] ## (case' arg ## (#Meta [_ (#Symbol [arg-module arg-name])]) -## (` (#AllT (list) "" (~ (_meta (#Text arg-name))) (~ (replace-ident [arg-module arg-name] +## (` (#AllT #None "" (~ (_meta (#Text arg-name))) (~ (replace-ident [arg-module arg-name] ## (` (#BoundT (~ (#Text ($ text:++ arg-module ";" arg-name))))) ## body))))))) ## body @@ -1596,7 +1598,7 @@ ## (#Symbol ["" arg])) ## args) ## body' (replace-syntax arg-replacements body)] -## (return (list (` (#AllT [#Nil (~ name') (#Tuple (list (~@ args'))) +## (return (list (` (#AllT [#None (~ name') (#Tuple (list (~@ args'))) ## (~ body')])))))) ## (def (walk-syntax type) diff --git a/src/lux/type.clj b/src/lux/type.clj index 35190da27..17db11b43 100644 --- a/src/lux/type.clj +++ b/src/lux/type.clj @@ -17,18 +17,22 @@ (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))) + (&/V "lux;AllT" (&/T (&/V "lux;None" nil) "List" "a" + (&/V "lux;VariantT" (&/|list (&/T "lux;Nil" Unit) (&/T "lux;Cons" (&/V "lux;TupleT" (&/|list (&/V "lux;BoundT" "a") (&/V "lux;AppT" (&/T (&/V "lux;BoundT" "List") (&/V "lux;BoundT" "a"))))))))))) +(def Maybe + (&/V "lux;AllT" (&/T (&/V "lux;None" nil) "Maybe" "a" + (&/V "lux;VariantT" (&/|list (&/T "lux;None" Unit) + (&/T "lux;Some" (&/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;AppT" (&/T (&/V "lux;AllT" (&/T (&/V "lux;None" nil) "Type" "_" (&/V "lux;VariantT" (&/|list (&/T "lux;AnyT" Unit) (&/T "lux;NothingT" Unit) (&/T "lux;DataT" Text) @@ -38,7 +42,7 @@ (&/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;AllT" (&/V "lux;TupleT" (&/|list (&/V "lux;AppT" (&/T Maybe TypeEnv)) Text Text Type))) (&/T "lux;AppT" TypePair) )))) (&/V "lux;NothingT" nil))))) @@ -154,10 +158,16 @@ (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) + (|do [=env (matchv ::M/objects [?env] + [["lux;None" _]] + (return ?env) + + [["lux;Some" ?env*]] + (|do [clean-env (&/map% (fn [[k v]] + (|do [=v (clean* ?tid v)] + (return (&/T k =v)))) + ?env*)] + (return (&/V "lux;Some" clean-env)))) body* (clean* ?tid ?body)] (return (&/V "lux;AllT" (&/T =env ?name ?arg body*)))) @@ -284,20 +294,27 @@ ;; '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)) - )) + (and (= xname yname) + (= xarg yarg) + ;; (matchv ::M/objects [xenv yenv] + ;; [["lux;None" _] ["lux;None" _]] + ;; true + + ;; [["lux;Some" xenv*] ["lux;Some" yenv*]] + ;; (&/fold (fn [old bname] + ;; (and old + ;; (type= (&/|get bname xenv*) (&/|get bname yenv*)))) + ;; (= (&/|length xenv*) (&/|length yenv*)) + ;; (&/|keys xenv*)) + + ;; [_ _] + ;; false) + (type= xbody ybody) + )) [_ _] (do ;; (prn 'type= (show-type x) (show-type y)) - false) + false) )] ;; (prn 'type= output (show-type x) (show-type y)) output)) @@ -343,16 +360,19 @@ (&/V "lux;AppT" (&/T (beta-reduce env ?type-fn) (beta-reduce env ?type-arg))) [["lux;AllT" [?local-env ?local-name ?local-arg ?local-def]]] - (&/V "lux;AllT" (&/T (&/|merge ?local-env env) ?local-name ?local-arg ?local-def)) + (matchv ::M/objects [?local-env] + [["lux;None" _]] + (&/V "lux;AllT" (&/T (&/V "lux;Some" env) ?local-name ?local-arg ?local-def)) + + [["lux;Some" _]] + type) [["lux;LambdaT" [?input ?output]]] (&/V "lux;LambdaT" (&/T (beta-reduce env ?input) (beta-reduce env ?output))) [["lux;BoundT" ?name]] (if-let [bound (&/|get ?name env)] - (do ;; (prn 'beta-reduce "lux;BoundT" ?name (->> (&/|keys env) (&/|interpose " ") (&/fold str "")) - ;; (show-type bound)) - (beta-reduce env bound)) + (beta-reduce env bound) type) [_] @@ -372,10 +392,17 @@ ;; (prn 'apply-type (aget type-fn 0) (aget param 0)) (matchv ::M/objects [type-fn] [["lux;AllT" [local-env local-name local-arg local-def]]] - (return (beta-reduce (->> local-env - (&/|put local-name type-fn) - (&/|put local-arg param)) - local-def)) + (let [;; _ (prn 'apply-type/local-env (aget local-env 0) (show-type type-fn)) + local-env* (matchv ::M/objects [local-env] + [["lux;None" _]] + (&/|table) + + [["lux;Some" local-env*]] + local-env*)] + (return (beta-reduce (->> local-env* + (&/|put local-name type-fn) + (&/|put local-arg param)) + local-def))) [["lux;AppT" [F A]]] (|do [type-fn* (apply-type F A)] @@ -552,7 +579,7 @@ (|do [_ (check* init-fixpoints input param)] (return output)) - [["lux;AllT" [local-env local-name local-arg local-def]]] + [["lux;AllT" _]] (with-var (fn [$var] (|do [func* (apply-type func $var) |