diff options
author | Eduardo Julian | 2015-08-28 22:46:12 -0400 |
---|---|---|
committer | Eduardo Julian | 2015-08-28 22:46:12 -0400 |
commit | 8de225f98aaed212bf3b683208bff5c6ab85a835 (patch) | |
tree | f9a3e197c7bf62cffa411f5a9e768cbca6a76d9b /src | |
parent | a10d922283a9256f0f0015d9d00a0c549b1891cb (diff) |
- Changed the name of AllT (for-all type) to UnivQ (universal quantification).
- UnivQ no longer stores the environment as key-val pairs with Text names, but instead stores it as type-lists with variables accessed via an index through a (updated) BoundT.
- UnivQ no longer stores the name of the type-fun, not the name of the type-arg.
Diffstat (limited to '')
-rw-r--r-- | src/lux/analyser/case.clj | 44 | ||||
-rw-r--r-- | src/lux/analyser/env.clj | 4 | ||||
-rw-r--r-- | src/lux/analyser/host.clj | 2 | ||||
-rw-r--r-- | src/lux/analyser/lux.clj | 63 | ||||
-rw-r--r-- | src/lux/analyser/module.clj | 2 | ||||
-rw-r--r-- | src/lux/base.clj | 37 | ||||
-rw-r--r-- | src/lux/compiler/type.clj | 19 | ||||
-rw-r--r-- | src/lux/reader.clj | 4 | ||||
-rw-r--r-- | src/lux/type.clj | 445 |
9 files changed, 290 insertions, 330 deletions
diff --git a/src/lux/analyser/case.clj b/src/lux/analyser/case.clj index 5987cbdf7..829b5b6d8 100644 --- a/src/lux/analyser/case.clj +++ b/src/lux/analyser/case.clj @@ -48,7 +48,7 @@ (fail "##9##")))] (resolve-type type*)) - (&/$AllT _aenv _aname _aarg _abody) + (&/$UnivQ _) ;; (&type/actual-type _abody) (|do [$var &type/existential =type (&type/apply-type type $var)] @@ -61,42 +61,46 @@ _ (&type/actual-type type))) +(defn update-up-frame [frame] + (|let [[_env _idx _var] frame] + (&/T _env (+ 2 _idx) _var))) + (defn adjust-type* [up type] - "(-> (List (, (Maybe (Env Text Type)) Text Text Type)) Type (Lux Type))" + "(-> (List (, (Maybe (List Type)) Int Type)) Type (Lux Type))" ;; (prn 'adjust-type* (&type/show-type type)) (|case type - (&/$AllT _aenv _aname _aarg _abody) + (&/$UnivQ _aenv _abody) (&type/with-var (fn [$var] (|do [=type (&type/apply-type type $var)] - (adjust-type* (&/|cons (&/T _aenv _aname _aarg $var) up) =type)))) + (adjust-type* (&/Cons$ (&/T _aenv 1 $var) (&/|map update-up-frame up)) =type)))) (&/$TupleT ?members) (|do [(&/$TupleT ?members*) (&/fold% (fn [_abody ena] - (|let [[_aenv _aname _aarg (&/$VarT _avar)] ena] - (|do [_ (&type/set-var _avar (&/V &/$BoundT _aarg))] + (|let [[_aenv _aidx (&/$VarT _avar)] ena] + (|do [_ (&type/set-var _avar (&/V &/$BoundT _aidx))] (&type/clean* _avar _abody)))) type up)] (return (&type/Tuple$ (&/|map (fn [v] (&/fold (fn [_abody ena] - (|let [[_aenv _aname _aarg _avar] ena] - (&/V &/$AllT (&/T _aenv _aname _aarg _abody)))) + (|let [[_aenv _aidx _avar] ena] + (&/V &/$UnivQ (&/T _aenv _abody)))) v up)) ?members*)))) (&/$VariantT ?members) (|do [(&/$VariantT ?members*) (&/fold% (fn [_abody ena] - (|let [[_aenv _aname _aarg (&/$VarT _avar)] ena] - (|do [_ (&type/set-var _avar (&/V &/$BoundT _aarg))] + (|let [[_aenv _aidx (&/$VarT _avar)] ena] + (|do [_ (&type/set-var _avar (&/V &/$BoundT _aidx))] (&type/clean* _avar _abody)))) type up)] (return (&/V &/$VariantT (&/|map (fn [v] (&/fold (fn [_abody ena] - (|let [[_aenv _aname _aarg _avar] ena] - (&/V &/$AllT (&/T _aenv _aname _aarg _abody)))) + (|let [[_aenv _aidx _avar] ena] + (&/V &/$UnivQ (&/T _aenv _abody)))) v up)) ?members*)))) @@ -169,7 +173,7 @@ (|do [[=tests =kont] (&/fold (fn [kont* vm] (|let [[v m] vm] (|do [[=test [=tests =kont]] (analyse-pattern v m kont*)] - (return (&/T (&/|cons =test =tests) =kont))))) + (return (&/T (&/Cons$ =test =tests) =kont))))) (|do [=kont kont] (return (&/T (&/|list) =kont))) (&/|reverse (&/zip2 ?member-types ?members)))] @@ -192,7 +196,7 @@ (|do [[=tests =kont] (&/fold (fn [kont* vm] (|let [[v m] vm] (|do [[=test [=tests =kont]] (analyse-pattern v m kont*)] - (return (&/T (&/|cons =test =tests) =kont))))) + (return (&/T (&/Cons$ =test =tests) =kont))))) (|do [=kont kont] (return (&/T (&/|list) =kont))) (&/|reverse (&/zip2 ?member-types ?members)))] @@ -242,7 +246,7 @@ (defn ^:private analyse-branch [analyse exo-type value-type pattern body patterns] (|do [pattern+body (analyse-pattern value-type pattern (&&/analyse-1 analyse exo-type body))] - (return (&/|cons pattern+body patterns)))) + (return (&/Cons$ pattern+body patterns)))) (let [compare-kv #(.compareTo ^String (aget ^objects %1 0) ^String (aget ^objects %2 0))] (defn ^:private merge-total [struct test+body] @@ -258,31 +262,31 @@ (return (&/V $BoolTotal (&/T total? (&/|list ?value)))) [($BoolTotal total? ?values) ($BoolTestAC ?value)] - (return (&/V $BoolTotal (&/T total? (&/|cons ?value ?values)))) + (return (&/V $BoolTotal (&/T total? (&/Cons$ ?value ?values)))) [($DefaultTotal total?) ($IntTestAC ?value)] (return (&/V $IntTotal (&/T total? (&/|list ?value)))) [($IntTotal total? ?values) ($IntTestAC ?value)] - (return (&/V $IntTotal (&/T total? (&/|cons ?value ?values)))) + (return (&/V $IntTotal (&/T total? (&/Cons$ ?value ?values)))) [($DefaultTotal total?) ($RealTestAC ?value)] (return (&/V $RealTotal (&/T total? (&/|list ?value)))) [($RealTotal total? ?values) ($RealTestAC ?value)] - (return (&/V $RealTotal (&/T total? (&/|cons ?value ?values)))) + (return (&/V $RealTotal (&/T total? (&/Cons$ ?value ?values)))) [($DefaultTotal total?) ($CharTestAC ?value)] (return (&/V $CharTotal (&/T total? (&/|list ?value)))) [($CharTotal total? ?values) ($CharTestAC ?value)] - (return (&/V $CharTotal (&/T total? (&/|cons ?value ?values)))) + (return (&/V $CharTotal (&/T total? (&/Cons$ ?value ?values)))) [($DefaultTotal total?) ($TextTestAC ?value)] (return (&/V $TextTotal (&/T total? (&/|list ?value)))) [($TextTotal total? ?values) ($TextTestAC ?value)] - (return (&/V $TextTotal (&/T total? (&/|cons ?value ?values)))) + (return (&/V $TextTotal (&/T total? (&/Cons$ ?value ?values)))) [($DefaultTotal total?) ($TupleTestAC ?tests)] (|do [structs (&/map% (fn [t] diff --git a/src/lux/analyser/env.clj b/src/lux/analyser/env.clj index 666807586..66478eecc 100644 --- a/src/lux/analyser/env.clj +++ b/src/lux/analyser/env.clj @@ -22,7 +22,7 @@ =return (body (&/update$ &/$envs (fn [stack] (let [bound-unit (&/V &&/$var (&/V &/$Local (->> (&/|head stack) (&/get$ &/$locals) (&/get$ &/$counter))))] - (&/|cons (&/update$ &/$locals #(->> % + (&/Cons$ (&/update$ &/$locals #(->> % (&/update$ &/$counter inc) (&/update$ &/$mappings (fn [m] (&/|put name (&/T bound-unit type) m)))) (&/|head stack)) @@ -31,7 +31,7 @@ (|case =return (&/$Right ?state ?value) (return* (&/update$ &/$envs (fn [stack*] - (&/|cons (&/update$ &/$locals #(->> % + (&/Cons$ (&/update$ &/$locals #(->> % (&/update$ &/$counter dec) (&/set$ &/$mappings old-mappings)) (&/|head stack*)) diff --git a/src/lux/analyser/host.clj b/src/lux/analyser/host.clj index 8ccfc5ace..098dc89df 100644 --- a/src/lux/analyser/host.clj +++ b/src/lux/analyser/host.clj @@ -313,7 +313,7 @@ (&&/analyse-1 analyse (&/V &/$DataT (as-otype ?method-output)) ?method-body)) (&/|reverse (if (:static? =method-modifiers) =method-inputs - (&/|cons (&/T ";this" ?super-class) + (&/Cons$ (&/T ";this" ?super-class) =method-inputs)))))] (return {:name ?method-name :modifiers =method-modifiers diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj index 634769839..c3f7622b8 100644 --- a/src/lux/analyser/lux.clj +++ b/src/lux/analyser/lux.clj @@ -42,7 +42,7 @@ (return (&/|list (&/T (&/V &&/$tuple =elems) exo-type)))) - (&/$AllT _) + (&/$UnivQ _) (&type/with-var (fn [$var] (|do [exo-type** (&type/apply-type exo-type* $var)] @@ -90,7 +90,7 @@ (&/$None) (fail (str "[Analyser Error] There is no case " idx " for variant type " (&type/show-type exo-type*)))) - (&/$AllT _) + (&/$UnivQ _) (&type/with-var (fn [$var] (|do [exo-type** (&type/apply-type exo-type* $var)] @@ -98,41 +98,20 @@ _ (fail (str "[Analyser Error] Can't create a variant if the expected type is " (&type/show-type exo-type*)))))) -;; (defn analyse-variant [analyse exo-type ident ?values] -;; (|do [exo-type* (|case exo-type -;; (&/$VarT ?id) -;; (&/try-all% (&/|list (|do [exo-type* (&type/deref ?id)] -;; (&type/actual-type exo-type*)) -;; (|do [_ (&type/set-var ?id &type/Type)] -;; (&type/actual-type &type/Type)))) - -;; _ -;; (&type/actual-type exo-type))] -;; (|case exo-type* -;; (&/$VariantT ?cases) -;; (|do [?tag (&&/resolved-ident ident)] -;; (if-let [vtype (&/|get ?tag ?cases)] -;; (|do [=value (analyse-variant-body analyse vtype ?values)] -;; (return (&/|list (&/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*))))) - -;; (&/$AllT _) -;; (&type/with-var -;; (fn [$var] -;; (|do [exo-type** (&type/apply-type exo-type* $var)] -;; (analyse-variant analyse exo-type** ident ?values)))) - -;; _ -;; (fail (str "[Analyser Error] Can't create a variant if the expected type is " (&type/show-type exo-type*)))))) (defn analyse-record [analyse exo-type ?elems] + ;; (when @&type/!flag + ;; (prn 'analyse-record (&type/show-type exo-type) + ;; (&/->seq (&/|map (fn [pair] + ;; (|let [[k v] pair] + ;; (str (&/show-ast k) " " (&/show-ast v)))) + ;; ?elems)))) (|do [exo-type* (|case exo-type (&/$VarT ?id) (|do [exo-type* (&type/deref ?id)] (&type/actual-type exo-type*)) - (&/$AllT _) + (&/$UnivQ _) (|do [$var &type/existential =type (&type/apply-type exo-type $var)] (&type/actual-type =type)) @@ -148,7 +127,7 @@ (return ?table) _ - (fail (str "[Analyser Error] The type of a record must be a record-type:\n" (&type/show-type exo-type*)))) + (fail (str "[Analyser Error] The type of a record must be a record-type:\n" (&type/show-type exo-type*) "\n" (&type/show-type exo-type)))) _ (&/assert! (= (&/|length types) (&/|length ?elems)) (str "[Analyser Error] Record length mismatch. Expected: " (&/|length types) "; actual: " (&/|length ?elems))) members (&&record/order-record ?elems) @@ -221,13 +200,13 @@ (&/$Cons top-outer _) (do ;; (prn 'analyse-symbol/_3 ?module name) - (|let [scopes (&/|tail (&/folds #(&/|cons (&/get$ &/$name %2) %1) + (|let [scopes (&/|tail (&/folds #(&/Cons$ (&/get$ &/$name %2) %1) (&/|map #(&/get$ &/$name %) outer) (&/|reverse inner))) [=local inner*] (&/fold2 (fn [register+new-inner frame in-scope] (|let [[register new-inner] register+new-inner [register* frame*] (&&lambda/close-over (&/|reverse in-scope) name register frame)] - (&/T register* (&/|cons frame* new-inner)))) + (&/T register* (&/Cons$ frame* new-inner)))) (&/T (or (->> top-outer (&/get$ &/$locals) (&/get$ &/$mappings) (&/|get name)) (->> top-outer (&/get$ &/$closure) (&/get$ &/$mappings) (&/|get name))) (&/|list)) @@ -255,7 +234,7 @@ (&/$Cons ?arg ?args*) (|do [?fun-type* (&type/actual-type fun-type)] (|case ?fun-type* - (&/$AllT _aenv _aname _aarg _abody) + (&/$UnivQ _) ;; (|do [$var &type/existential ;; type* (&type/apply-type ?fun-type* $var)] ;; (analyse-apply* analyse exo-type type* ?args)) @@ -268,7 +247,7 @@ (|do [? (&type/bound? ?id) type** (if ? (&type/clean $var =output-t) - (|do [_ (&type/set-var ?id (&/V &/$BoundT _aarg))] + (|do [_ (&type/set-var ?id (&/V &/$BoundT 1))] (&type/clean $var =output-t)))] (return (&/T type** =args))) )))) @@ -276,7 +255,7 @@ (&/$LambdaT ?input-t ?output-t) (|do [[=output-t =args] (analyse-apply* analyse exo-type ?output-t ?args*) =arg (&&/analyse-1 analyse ?input-t ?arg)] - (return (&/T =output-t (&/|cons =arg =args)))) + (return (&/T =output-t (&/Cons$ =arg =args)))) ;; [[&/$VarT ?id-t]] ;; (|do [ (&type/deref ?id-t)]) @@ -332,7 +311,7 @@ (defn analyse-lambda* [analyse exo-type ?self ?arg ?body] (|do [exo-type* (&type/actual-type exo-type)] (|case exo-type - (&/$AllT _) + (&/$UnivQ _) (&type/with-var (fn [$var] (|do [exo-type** (&type/apply-type exo-type* $var)] @@ -353,7 +332,7 @@ (defn analyse-lambda** [analyse exo-type ?self ?arg ?body] (|case exo-type - (&/$AllT _env _self _arg _body) + (&/$UnivQ _) (&type/with-var (fn [$var] (|do [exo-type* (&type/apply-type exo-type $var) @@ -376,12 +355,12 @@ (|do [?? (&type/bound? ?_id)] ;; (return (&/T _expr exo-type)) (if ?? - (fail (str "[Analyser Error] Can't use type-var in any type-specific way inside polymorphic functions: " ?id ":" _arg " " (&type/show-type dtype))) + (fail (str "[Analyser Error] Can't use type-var in any type-specific way inside polymorphic functions: " ?id " " (&type/show-type dtype))) (return (&/T _expr exo-type))) ) _ - (fail (str "[Analyser Error] Can't use type-var in any type-specific way inside polymorphic functions: " ?id ":" _arg " " (&type/show-type dtype))))) + (fail (str "[Analyser Error] Can't use type-var in any type-specific way inside polymorphic functions: " ?id " " (&type/show-type dtype))))) (return (&/T _expr exo-type)))))))) _ @@ -395,8 +374,8 @@ (defn analyse-def [analyse compile-token ?name ?value] ;; (prn 'analyse-def/BEGIN ?name) - ;; (when (= "PList/Dict" ?name) - ;; (prn 'DEF ?name (&/show-ast ?value))) + ;; (when (= "monoid$" ?name) + ;; (reset! &type/!flag true)) (|do [module-name &/get-module-name ;; :let [_ (println 'DEF/PRE (str module-name ";" ?name))] ? (&&module/defined? module-name ?name)] diff --git a/src/lux/analyser/module.clj b/src/lux/analyser/module.clj index 77630bafe..6eca13b44 100644 --- a/src/lux/analyser/module.clj +++ b/src/lux/analyser/module.clj @@ -41,7 +41,7 @@ (return* (&/update$ &/$modules (fn [ms] (&/|update current-module - (fn [m] (&/update$ $imports (partial &/|cons module) m)) + (fn [m] (&/update$ $imports (partial &/Cons$ module) m)) ms)) state) nil)))) diff --git a/src/lux/base.clj b/src/lux/base.clj index 44459beb4..5444c6c81 100644 --- a/src/lux/base.clj +++ b/src/lux/base.clj @@ -54,7 +54,7 @@ "BoundT" "VarT" "ExT" - "AllT" + "UnivQ" "AppT" "NamedT") @@ -285,9 +285,6 @@ (reverse (partition 2 steps)))) ;; [Resources/Combinators] -(defn |cons [head tail] - (V $Cons (T head tail))) - (defn |++ [xs ys] (|case xs ($Nil) @@ -348,7 +345,7 @@ ($Cons x xs*) (if (p x) (|let [[pre post] (|split-with p xs*)] - (T (|cons x pre) post)) + (T (Cons$ x pre) post)) (T (V $Nil nil) xs)))) (defn |contains? [k table] @@ -383,7 +380,7 @@ (|list init) ($Cons x xs*) - (|cons init (folds f (f init x) xs*)))) + (Cons$ init (folds f (f init x) xs*)))) (defn |length [xs] (fold (fn [acc _] (inc acc)) 0 xs)) @@ -417,7 +414,7 @@ (|list) ($Cons [k v] plist*) - (|cons k (|keys plist*)))) + (Cons$ k (|keys plist*)))) (defn |vals [plist] (|case plist @@ -425,7 +422,7 @@ (|list) ($Cons [k v] plist*) - (|cons v (|vals plist*)))) + (Cons$ v (|vals plist*)))) (defn |interpose [sep xs] (|case xs @@ -449,7 +446,7 @@ ys (<name> f xs*)] (return (<joiner> y ys))))) - map% |cons + map% Cons$ flat-map% |++) (defn list-join [xss] @@ -465,7 +462,7 @@ (defn |reverse [xs] (fold (fn [tail head] - (|cons head tail)) + (Cons$ head tail)) (|list) xs)) @@ -501,7 +498,7 @@ (defn repeat% [monad] (try-all% (|list (|do [head monad tail (repeat% monad)] - (return (|cons head tail))) + (return (Cons$ head tail))) (return (|list))))) (defn exhaust% [step] @@ -677,11 +674,11 @@ (defn ->list [seq] (if (empty? seq) (|list) - (|cons (first seq) (->list (rest seq))))) + (Cons$ (first seq) (->list (rest seq))))) (defn |repeat [n x] (if (> n 0) - (|cons x (|repeat (dec n) x)) + (Cons$ x (|repeat (dec n) x)) (|list))) (def get-module-name @@ -707,7 +704,7 @@ (defn with-scope [name body] (fn [state] - (let [output (body (update$ $envs #(|cons (env name) %) state))] + (let [output (body (update$ $envs #(Cons$ (env name) %) state))] (|case output ($Right state* datum) (return* (update$ $envs |tail state*) datum) @@ -723,7 +720,7 @@ (return (->> top (get$ $inner-closures) str)))] (fn [state] (let [body* (with-scope closure-name body)] - (run-state body* (update$ $envs #(|cons (update$ $inner-closures inc (|head %)) + (run-state body* (update$ $envs #(Cons$ (update$ $inner-closures inc (|head %)) (|tail %)) state)))))) @@ -789,10 +786,10 @@ ($Meta _ ($TagS ?module ?tag)) (str "#" ?module ";" ?tag) - ($Meta _ ($SymbolS ?module ?ident)) + ($Meta _ ($SymbolS ?module ?name)) (if (.equals "" ?module) - ?ident - (str ?module ";" ?ident)) + ?name + (str ?module ";" ?name)) ($Meta _ ($TupleS ?elems)) (str "[" (->> ?elems (|map show-ast) (|interpose " ") (fold str "")) "]") @@ -832,7 +829,7 @@ [($Cons x xs*) ($Cons y ys*)] (|do [z (f x y) zs (map2% f xs* ys*)] - (return (|cons z zs))) + (return (Cons$ z zs))) [($Nil) ($Nil)] (return (V $Nil nil)) @@ -843,7 +840,7 @@ (defn map2 [f xs ys] (|case [xs ys] [($Cons x xs*) ($Cons y ys*)] - (|cons (f x y) (map2 f xs* ys*)) + (Cons$ (f x y) (map2 f xs* ys*)) [_ _] (V $Nil nil))) diff --git a/src/lux/compiler/type.clj b/src/lux/compiler/type.clj index 54a7c5e0c..0d0300844 100644 --- a/src/lux/compiler/type.clj +++ b/src/lux/compiler/type.clj @@ -21,6 +21,11 @@ (&/T (&/V &a/$tuple members) &type/$Void)) +(defn ^:private int$ [value] + "(-> Int Analysis)" + (&/T (&/V &a/$int value) + &type/$Void)) + (defn ^:private text$ [text] "(-> Text Analysis)" (&/T (&/V &a/$text text) @@ -58,20 +63,16 @@ (&/$LambdaT ?input ?output) (variant$ &/$LambdaT (tuple$ (&/|list (->analysis ?input) (->analysis ?output)))) - (&/$AllT ?env ?name ?arg ?body) - (variant$ &/$AllT + (&/$UnivQ ?env ?body) + (variant$ &/$UnivQ (tuple$ (&/|list (&/fold (fn [tail head] - (|let [[hlabel htype] head] - (Cons$ (tuple$ (&/|list (text$ hlabel) (->analysis htype))) - tail))) + (Cons$ (->analysis head) tail)) $Nil (&/|reverse ?env)) - (text$ ?name) - (text$ ?arg) (->analysis ?body)))) - (&/$BoundT ?name) - (variant$ &/$BoundT (text$ ?name)) + (&/$BoundT ?idx) + (variant$ &/$BoundT (int$ ?idx)) (&/$AppT ?fun ?arg) (variant$ &/$AppT (tuple$ (&/|list (->analysis ?fun) (->analysis ?arg)))) diff --git a/src/lux/reader.clj b/src/lux/reader.clj index aa845c09d..0fcb5097b 100644 --- a/src/lux/reader.clj +++ b/src/lux/reader.clj @@ -33,7 +33,7 @@ output) ($Yes output line*) - (return* (&/set$ &/$source (&/|cons line* more) state) + (return* (&/set$ &/$source (&/Cons$ line* more) state) output)) ))) @@ -117,7 +117,7 @@ column-num* (+ column-num match-length)] (if (= column-num* (.length line)) (recur (str prefix match "\n") reader**) - (&/V &/$Right (&/T (&/|cons (&/T (&/T file-name line-num column-num*) line) + (&/V &/$Right (&/T (&/Cons$ (&/T (&/T file-name line-num column-num*) line) reader**) (&/T (&/T file-name line-num column-num) (str prefix match)))))) (&/V &/$Left (str "[Reader Error] Pattern failed: " regex)))))))) diff --git a/src/lux/type.clj b/src/lux/type.clj index bcef74475..2b06553c3 100644 --- a/src/lux/type.clj +++ b/src/lux/type.clj @@ -40,8 +40,8 @@ (defn Variant$ [members] ;; (assert (|list? members)) (&/V &/$VariantT members)) -(defn All$ [env name arg body] - (&/V &/$AllT (&/T env name arg body))) +(defn Univ$ [env body] + (&/V &/$UnivQ (&/T env body))) (defn Named$ [name type] (&/V &/$NamedT (&/T name type))) @@ -57,91 +57,90 @@ (def IO (Named$ (&/T "lux/data" "IO") - (All$ empty-env "IO" "a" - (Lambda$ Unit (Bound$ "a"))))) + (Univ$ empty-env + (Lambda$ Unit (Bound$ 1))))) (def List (Named$ (&/T "lux" "List") - (All$ empty-env "lux;List" "a" - (Variant$ (&/|list - ;; lux;Nil - Unit - ;; lux;Cons - (Tuple$ (&/|list (Bound$ "a") - (App$ (Bound$ "lux;List") - (Bound$ "a")))) - ))))) + (Univ$ empty-env + (Variant$ (&/|list + ;; lux;Nil + Unit + ;; lux;Cons + (Tuple$ (&/|list (Bound$ 1) + (App$ (Bound$ 0) + (Bound$ 1)))) + ))))) (def Maybe (Named$ (&/T "lux" "Maybe") - (All$ empty-env "lux;Maybe" "a" - (Variant$ (&/|list - ;; lux;None - Unit - ;; lux;Some - (Bound$ "a") - ))))) + (Univ$ empty-env + (Variant$ (&/|list + ;; lux;None + Unit + ;; lux;Some + (Bound$ 1) + ))))) (def Type (Named$ (&/T "lux" "Type") - (let [Type (App$ (Bound$ "Type") (Bound$ "_")) + (let [Type (App$ (Bound$ 0) (Bound$ 1)) TypeList (App$ List Type) - TypeEnv (App$ List (Tuple$ (&/|list Text Type))) TypePair (Tuple$ (&/|list Type Type))] - (App$ (All$ empty-env "Type" "_" - (Variant$ (&/|list - ;; DataT - Text - ;; VariantT - TypeList - ;; TupleT - TypeList - ;; LambdaT - TypePair - ;; BoundT - Text - ;; VarT - Int - ;; ExT - Int - ;; AllT - (Tuple$ (&/|list TypeEnv Text Text Type)) - ;; AppT - TypePair - ;; NamedT - (Tuple$ (&/|list Ident Type)) - ))) + (App$ (Univ$ empty-env + (Variant$ (&/|list + ;; DataT + Text + ;; VariantT + TypeList + ;; TupleT + TypeList + ;; LambdaT + TypePair + ;; BoundT + Int + ;; VarT + Int + ;; ExT + Int + ;; UnivQ + (Tuple$ (&/|list TypeList Type)) + ;; AppT + TypePair + ;; NamedT + (Tuple$ (&/|list Ident Type)) + ))) $Void)))) (def Bindings (Named$ (&/T "lux" "Bindings") - (All$ empty-env "lux;Bindings" "k" - (All$ empty-env "" "v" - (Tuple$ (&/|list - ;; "lux;counter" - Int - ;; "lux;mappings" - (App$ List - (Tuple$ (&/|list (Bound$ "k") - (Bound$ "v")))))))))) + (Univ$ empty-env + (Univ$ empty-env + (Tuple$ (&/|list + ;; "lux;counter" + Int + ;; "lux;mappings" + (App$ List + (Tuple$ (&/|list (Bound$ 3) + (Bound$ 1)))))))))) (def Env (Named$ (&/T "lux" "Env") - (let [bindings (App$ (App$ Bindings (Bound$ "k")) - (Bound$ "v"))] - (All$ empty-env "lux;Env" "k" - (All$ empty-env "" "v" - (Tuple$ - (&/|list - ;; "lux;name" - Text - ;; "lux;inner-closures" - Int - ;; "lux;locals" - bindings - ;; "lux;closure" - bindings - ))))))) + (let [bindings (App$ (App$ Bindings (Bound$ 3)) + (Bound$ 1))] + (Univ$ empty-env + (Univ$ empty-env + (Tuple$ + (&/|list + ;; "lux;name" + Text + ;; "lux;inner-closures" + Int + ;; "lux;locals" + bindings + ;; "lux;closure" + bindings + ))))))) (def Cursor (Named$ (&/T "lux" "Cursor") @@ -149,42 +148,42 @@ (def Meta (Named$ (&/T "lux" "Meta") - (All$ empty-env "lux;Meta" "m" - (All$ empty-env "" "v" - (Variant$ (&/|list - ;; &/$Meta - (Tuple$ (&/|list (Bound$ "m") - (Bound$ "v"))))))))) + (Univ$ empty-env + (Univ$ empty-env + (Variant$ (&/|list + ;; &/$Meta + (Tuple$ (&/|list (Bound$ 3) + (Bound$ 1))))))))) (def AST* (Named$ (&/T "lux" "AST'") - (let [AST* (App$ (Bound$ "w") - (App$ (Bound$ "lux;AST'") - (Bound$ "w"))) + (let [AST* (App$ (Bound$ 1) + (App$ (Bound$ 0) + (Bound$ 1))) AST*List (App$ List AST*)] - (All$ empty-env "lux;AST'" "w" - (Variant$ (&/|list - ;; &/$BoolS - Bool - ;; &/$IntS - Int - ;; &/$RealS - Real - ;; &/$CharS - Char - ;; &/$TextS - Text - ;; &/$SymbolS - Ident - ;; &/$TagS - Ident - ;; &/$FormS - AST*List - ;; &/$TupleS - AST*List - ;; &/$RecordS - (App$ List (Tuple$ (&/|list AST* AST*)))) - ))))) + (Univ$ empty-env + (Variant$ (&/|list + ;; &/$BoolS + Bool + ;; &/$IntS + Int + ;; &/$RealS + Real + ;; &/$CharS + Char + ;; &/$TextS + Text + ;; &/$SymbolS + Ident + ;; &/$TagS + Ident + ;; &/$FormS + AST*List + ;; &/$TupleS + AST*List + ;; &/$RecordS + (App$ List (Tuple$ (&/|list AST* AST*)))) + ))))) (def AST (Named$ (&/T "lux" "AST") @@ -195,21 +194,21 @@ (def Either (Named$ (&/T "lux" "Either") - (All$ empty-env "lux;Either" "l" - (All$ empty-env "" "r" - (Variant$ (&/|list - ;; &/$Left - (Bound$ "l") - ;; &/$Right - (Bound$ "r"))))))) + (Univ$ empty-env + (Univ$ empty-env + (Variant$ (&/|list + ;; &/$Left + (Bound$ 3) + ;; &/$Right + (Bound$ 1))))))) (def StateE - (All$ empty-env "lux;StateE" "s" - (All$ empty-env "" "a" - (Lambda$ (Bound$ "s") - (App$ (App$ Either Text) - (Tuple$ (&/|list (Bound$ "s") - (Bound$ "a")))))))) + (Univ$ empty-env + (Univ$ empty-env + (Lambda$ (Bound$ 3) + (App$ (App$ Either Text) + (Tuple$ (&/|list (Bound$ 3) + (Bound$ 1)))))))) (def Source (Named$ (&/T "lux" "Source") @@ -229,17 +228,17 @@ (Data$ "clojure.lang.Atom"))))) (def DefData* - (All$ empty-env "lux;DefData'" "" - (Variant$ (&/|list - ;; "lux;ValueD" - (Tuple$ (&/|list Type Unit)) - ;; "lux;TypeD" - Type - ;; "lux;MacroD" - (Bound$ "") - ;; "lux;AliasD" - Ident - )))) + (Univ$ empty-env + (Variant$ (&/|list + ;; "lux;ValueD" + (Tuple$ (&/|list Type Unit)) + ;; "lux;TypeD" + Type + ;; "lux;MacroD" + (Bound$ 1) + ;; "lux;AliasD" + Ident + )))) (def LuxVar (Named$ (&/T "lux" "LuxVar") @@ -250,63 +249,63 @@ Ident)))) (def $Module - (All$ empty-env "lux;$Module" "Compiler" - (Tuple$ - (&/|list - ;; "lux;module-aliases" - (App$ List (Tuple$ (&/|list Text Text))) - ;; "lux;defs" - (App$ List - (Tuple$ (&/|list Text - (Tuple$ (&/|list Bool - (App$ DefData* - (Lambda$ ASTList - (App$ (App$ StateE (Bound$ "Compiler")) - ASTList)))))))) - ;; "lux;imports" - (App$ List Text) - ;; "lux;tags" - ;; (List (, Text (, Int (List Ident) Type))) - (App$ List - (Tuple$ (&/|list Text - (Tuple$ (&/|list Int - (App$ List Ident) - Type))))) - ;; "lux;types" - ;; (List (, Text (, (List Ident) Type))) - (App$ List - (Tuple$ (&/|list Text - (Tuple$ (&/|list (App$ List Ident) - Type))))) - )))) + (Univ$ empty-env + (Tuple$ + (&/|list + ;; "lux;module-aliases" + (App$ List (Tuple$ (&/|list Text Text))) + ;; "lux;defs" + (App$ List + (Tuple$ (&/|list Text + (Tuple$ (&/|list Bool + (App$ DefData* + (Lambda$ ASTList + (App$ (App$ StateE (Bound$ 1)) + ASTList)))))))) + ;; "lux;imports" + (App$ List Text) + ;; "lux;tags" + ;; (List (, Text (, Int (List Ident) Type))) + (App$ List + (Tuple$ (&/|list Text + (Tuple$ (&/|list Int + (App$ List Ident) + Type))))) + ;; "lux;types" + ;; (List (, Text (, (List Ident) Type))) + (App$ List + (Tuple$ (&/|list Text + (Tuple$ (&/|list (App$ List Ident) + Type))))) + )))) (def $Compiler (Named$ (&/T "lux" "Compiler") - (App$ (All$ empty-env "lux;Compiler" "" - (Tuple$ - (&/|list - ;; "lux;source" - Source - ;; "lux;cursor" - Cursor - ;; "lux;modules" - (App$ List (Tuple$ (&/|list Text - (App$ $Module (App$ (Bound$ "lux;Compiler") (Bound$ "")))))) - ;; "lux;envs" - (App$ List - (App$ (App$ Env Text) - (Tuple$ (&/|list LuxVar Type)))) - ;; "lux;types" - (App$ (App$ Bindings Int) Type) - ;; "lux;expected" - Type - ;; "lux;seed" - Int - ;; "lux;eval?" - Bool - ;; "lux;host" - Host - ))) + (App$ (Univ$ empty-env + (Tuple$ + (&/|list + ;; "lux;source" + Source + ;; "lux;cursor" + Cursor + ;; "lux;modules" + (App$ List (Tuple$ (&/|list Text + (App$ $Module (App$ (Bound$ 0) (Bound$ 1)))))) + ;; "lux;envs" + (App$ List + (App$ (App$ Env Text) + (Tuple$ (&/|list LuxVar Type)))) + ;; "lux;types" + (App$ (App$ Bindings Int) Type) + ;; "lux;expected" + Type + ;; "lux;seed" + Int + ;; "lux;eval?" + Bool + ;; "lux;host" + Host + ))) $Void))) (def Macro @@ -439,13 +438,10 @@ (|do [=members (&/map% (partial clean* ?tid) ?members)] (return (Variant$ =members))) - (&/$AllT ?env ?name ?arg ?body) - (|do [=env (&/map% (fn [[k v]] - (|do [=v (clean* ?tid v)] - (return (&/T k =v)))) - ?env) + (&/$UnivQ ?env ?body) + (|do [=env (&/map% (partial clean* ?tid) ?env) body* (clean* ?tid ?body)] - (return (All$ =env ?name ?arg body*))) + (return (Univ$ =env body*))) _ (return type) @@ -463,7 +459,7 @@ (|case type (&/$LambdaT ?in ?out) (|let [[??out ?args] (unravel-fun ?out)] - (&/T ??out (&/|cons ?in ?args))) + (&/T ??out (&/Cons$ ?in ?args))) _ (&/T type (&/|list)))) @@ -505,26 +501,16 @@ (&/$ExT ?id) (str "⟨" ?id "⟩") - (&/$BoundT name) - name + (&/$BoundT idx) + (str idx) (&/$AppT _ _) (|let [[?call-fun ?call-args] (unravel-app type)] (str "(" (show-type ?call-fun) " " (->> ?call-args (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")")) - (&/$AllT ?env ?name ?arg ?body) - (if (= "" ?name) - (let [[args body] (loop [args (list ?arg) - body* ?body] - (|case body* - (&/$AllT ?env* ?name* ?arg* ?body*) - (recur (cons ?arg* args) ?body*) - - _ - [args body*]))] - (str "(All " ?name " [" (->> args reverse (interpose " ") (reduce str "")) "] " (show-type body) ")")) - ?name) - + (&/$UnivQ ?env ?body) + (str "(All " (show-type ?body) ")") + (&/$NamedT ?name ?type) (&/ident->text ?name) @@ -554,8 +540,8 @@ [(&/$VarT xid) (&/$VarT yid)] (.equals ^Object xid yid) - [(&/$BoundT xname) (&/$BoundT yname)] - (.equals ^Object xname yname) + [(&/$BoundT xidx) (&/$BoundT yidx)] + (= xidx yidx) [(&/$ExT xid) (&/$ExT yid)] (.equals ^Object xid yid) @@ -563,24 +549,8 @@ [(&/$AppT xlambda xparam) (&/$AppT ylambda yparam)] (and (type= xlambda ylambda) (type= xparam yparam)) - [(&/$AllT xenv xname xarg xbody) (&/$AllT yenv yname yarg ybody)] - (and (.equals ^Object xname yname) - (.equals ^Object xarg yarg) - ;; (matchv ::M/objects [xenv yenv] - ;; [[&/$None _] [&/$None _]] - ;; true - - ;; [[&/$Some xenv*] [&/$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) - ) + [(&/$UnivQ xenv xbody) (&/$UnivQ yenv ybody)] + (type= xbody ybody) [(&/$NamedT ?xname ?xtype) _] (type= ?xtype y) @@ -607,14 +577,18 @@ ))) (defn ^:private fp-put [k v fixpoints] - (&/|cons (&/T k v) fixpoints)) + (&/Cons$ (&/T k v) fixpoints)) (defn ^:private check-error [expected actual] (str "[Type Checker]\nExpected: " (show-type expected) "\n\nActual: " (show-type actual) "\n")) +;; (def !flag (atom false)) + (defn beta-reduce [env type] + ;; (when @!flag + ;; (prn 'beta-reduce (show-type type))) (|case type (&/$VariantT ?members) (Variant$ (&/|map (partial beta-reduce env) ?members)) @@ -625,10 +599,10 @@ (&/$AppT ?type-fn ?type-arg) (App$ (beta-reduce env ?type-fn) (beta-reduce env ?type-arg)) - (&/$AllT ?local-env ?local-name ?local-arg ?local-def) + (&/$UnivQ ?local-env ?local-def) (|case ?local-env (&/$Nil) - (All$ env ?local-name ?local-arg ?local-def) + (Univ$ env ?local-def) _ type) @@ -636,21 +610,26 @@ (&/$LambdaT ?input ?output) (Lambda$ (beta-reduce env ?input) (beta-reduce env ?output)) - (&/$BoundT ?name) - (if-let [bound (&/|get ?name env)] + (&/$BoundT ?idx) + (|case (&/|at ?idx env) + (&/$Some bound) (beta-reduce env bound) - type) + + _ + (assert false (str "[Type Error] Unknown var: " ?idx " | " (&/->seq (&/|map show-type env))))) _ type )) (defn apply-type [type-fn param] + ;; (when @!flag + ;; (prn 'apply-type (show-type type-fn) (show-type param))) (|case type-fn - (&/$AllT local-env local-name local-arg local-def) + (&/$UnivQ local-env local-def) (return (beta-reduce (->> local-env - (&/|put local-name type-fn) - (&/|put local-arg param)) + (&/Cons$ param) + (&/Cons$ type-fn)) local-def)) (&/$AppT F A) @@ -839,13 +818,13 @@ (|do [actual* (apply-type F A)] (check* class-loader fixpoints expected actual*)) - [(&/$AllT _) _] + [(&/$UnivQ _) _] (with-var (fn [$arg] (|do [expected* (apply-type expected $arg)] (check* class-loader fixpoints expected* actual)))) - [_ (&/$AllT _)] + [_ (&/$UnivQ _)] (with-var (fn [$arg] (|do [actual* (apply-type actual $arg)] @@ -910,7 +889,7 @@ (|do [_ (check* init-fixpoints input param)] (return output)) - (&/$AllT _) + (&/$UnivQ _) (with-var (fn [$var] (|do [func* (apply-type func $var) |