aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--luxc/src/lux/base.clj20
-rw-r--r--luxc/src/lux/type.clj57
-rw-r--r--stdlib/source/lux.lux52
-rw-r--r--stdlib/source/lux/macro.lux5
-rw-r--r--stdlib/source/lux/math/simple.lux6
-rw-r--r--stdlib/source/lux/type/auto.lux77
-rw-r--r--stdlib/source/lux/type/check.lux259
7 files changed, 276 insertions, 200 deletions
diff --git a/luxc/src/lux/base.clj b/luxc/src/lux/base.clj
index 2fe9952ee..bdbffdf35 100644
--- a/luxc/src/lux/base.clj
+++ b/luxc/src/lux/base.clj
@@ -110,6 +110,12 @@
["counter"
"mappings"])
+;; Type-Context
+(deftuple
+ ["ex-counter"
+ "var-counter"
+ "var-bindings"])
+
;; Env
(deftuple
["name"
@@ -148,7 +154,7 @@
"cursor"
"modules"
"scopes"
- "type-vars"
+ "type-context"
"expected"
"seed"
"scope-type-vars"
@@ -711,6 +717,14 @@
;; "lux;mappings"
(|table)]))
+(def +init-type-context+
+ (T [;; ex-counter
+ 0
+ ;; var-counter
+ 0
+ ;; var-bindings
+ (|table)]))
+
(defn env [name old-name]
(T [;; "lux;name"
($Cons name old-name)
@@ -821,8 +835,8 @@
(|table)
;; "lux;scopes"
$Nil
- ;; "lux;types"
- +init-bindings+
+ ;; "lux;type-context"
+ +init-type-context+
;; "lux;expected"
$None
;; "lux;seed"
diff --git a/luxc/src/lux/type.clj b/luxc/src/lux/type.clj
index 561d81795..f69542442 100644
--- a/luxc/src/lux/type.clj
+++ b/luxc/src/lux/type.clj
@@ -171,7 +171,7 @@
(defn bound? [id]
(fn [state]
- (if-let [type (->> state (&/get$ &/$type-vars) (&/get$ &/$mappings) (&/|get id))]
+ (if-let [type (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings) (&/|get id))]
(|case type
(&/$Some type*)
(return* state true)
@@ -183,7 +183,7 @@
(defn deref [id]
(fn [state]
- (if-let [type* (->> state (&/get$ &/$type-vars) (&/get$ &/$mappings) (&/|get id))]
+ (if-let [type* (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings) (&/|get id))]
(|case type*
(&/$Some type)
(return* state type)
@@ -205,7 +205,7 @@
(defn set-var [id type]
(fn [state]
- (if-let [tvar (->> state (&/get$ &/$type-vars) (&/get$ &/$mappings) (&/|get id))]
+ (if-let [tvar (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings) (&/|get id))]
(|case tvar
(&/$Some bound)
(if (type= type bound)
@@ -214,56 +214,63 @@
state))
(&/$None)
- (return* (&/update$ &/$type-vars (fn [ts] (&/update$ &/$mappings #(&/|put id (&/$Some type) %)
- ts))
+ (return* (&/update$ &/$type-context (fn [ts] (&/update$ &/$var-bindings #(&/|put id (&/$Some type) %)
+ ts))
state)
nil))
- ((&/fail-with-loc (str "[Type Error] Unknown type-var: " id " | " (->> state (&/get$ &/$type-vars) (&/get$ &/$mappings) &/|length)))
+ ((&/fail-with-loc (str "[Type Error] Unknown type-var: " id " | " (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings) &/|length)))
state))))
(defn reset-var [id type]
(fn [state]
- (if-let [tvar (->> state (&/get$ &/$type-vars) (&/get$ &/$mappings) (&/|get id))]
- (return* (&/update$ &/$type-vars (fn [ts] (&/update$ &/$mappings #(&/|put id (&/$Some type) %)
- ts))
+ (if-let [tvar (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings) (&/|get id))]
+ (return* (&/update$ &/$type-context (fn [ts] (&/update$ &/$var-bindings #(&/|put id (&/$Some type) %)
+ ts))
state)
nil)
- ((&/fail-with-loc (str "[Type Error] Unknown type-var: " id " | " (->> state (&/get$ &/$type-vars) (&/get$ &/$mappings) &/|length)))
+ ((&/fail-with-loc (str "[Type Error] Unknown type-var: " id " | " (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings) &/|length)))
state))))
(defn unset-var [id]
(fn [state]
- (if-let [tvar (->> state (&/get$ &/$type-vars) (&/get$ &/$mappings) (&/|get id))]
- (return* (&/update$ &/$type-vars (fn [ts] (&/update$ &/$mappings #(&/|put id &/$None %)
- ts))
+ (if-let [tvar (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings) (&/|get id))]
+ (return* (&/update$ &/$type-context (fn [ts] (&/update$ &/$var-bindings #(&/|put id &/$None %)
+ ts))
state)
nil)
- ((&/fail-with-loc (str "[Type Error] Unknown type-var: " id " | " (->> state (&/get$ &/$type-vars) (&/get$ &/$mappings) &/|length)))
+ ((&/fail-with-loc (str "[Type Error] Unknown type-var: " id " | " (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings) &/|length)))
state))))
;; [Exports]
;; Type vars
(def reset-mappings
(fn [state]
- (return* (&/update$ &/$type-vars #(->> %
- ;; (&/set$ &/$counter 0)
- (&/set$ &/$mappings (&/|table)))
+ (return* (&/update$ &/$type-context #(->> %
+ ;; (&/set$ &/$var-counter 0)
+ (&/set$ &/$var-bindings (&/|table)))
state)
nil)))
(def create-var
(fn [state]
- (let [id (->> state (&/get$ &/$type-vars) (&/get$ &/$counter))]
- (return* (&/update$ &/$type-vars #(->> %
- (&/update$ &/$counter inc)
- (&/update$ &/$mappings (fn [ms] (&/|put id &/$None ms))))
+ (let [id (->> state (&/get$ &/$type-context) (&/get$ &/$var-counter))]
+ (return* (&/update$ &/$type-context #(->> %
+ (&/update$ &/$var-counter inc)
+ (&/update$ &/$var-bindings (fn [ms] (&/|put id &/$None ms))))
state)
id))))
(def existential
;; (Lux Type)
- (|do [seed &/gen-id]
- (return (&/$ExT seed))))
+ (fn [compiler]
+ (return* (&/update$ &/$type-context
+ (fn [context]
+ (&/update$ &/$ex-counter inc context))
+ compiler)
+ (->> compiler
+ (&/get$ &/$type-context)
+ (&/get$ &/$ex-counter)
+ &/$ExT))))
(declare clean*)
(defn delete-var [id]
@@ -292,9 +299,9 @@
(|do [?type** (clean* id ?type*)]
(return (&/T [?id (&/$Some ?type**)]))))
))))
- (->> state (&/get$ &/$type-vars) (&/get$ &/$mappings)))]
+ (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings)))]
(fn [state]
- (return* (&/update$ &/$type-vars #(&/set$ &/$mappings (&/|remove id mappings*) %)
+ (return* (&/update$ &/$type-context #(&/set$ &/$var-bindings (&/|remove id mappings*) %)
state)
nil)))
state))))
diff --git a/stdlib/source/lux.lux b/stdlib/source/lux.lux
index 8be7f8d26..e1244d970 100644
--- a/stdlib/source/lux.lux
+++ b/stdlib/source/lux.lux
@@ -548,6 +548,26 @@
(#Cons [["lux" "doc"] (#TextA "All the information contained within a Lux module.")]
default-def-meta-exported)))
+## (type: Type-Context
+## {#ex-counter Nat
+## #var-counter Nat
+## #var-bindings (List [Nat (Maybe Type)])})
+(_lux_def Type-Context
+ (#NamedT ["lux" "Type-Context"]
+ (#ProdT ## ex-counter
+ Nat
+ (#ProdT ## var-counter
+ Nat
+ ## var-bindings
+ (#AppT List
+ (#ProdT Nat
+ (#AppT Maybe Type))))))
+ (#Cons [["lux" "tags"] (#ListA (#Cons (#TextA "ex-counter")
+ (#Cons (#TextA "var-counter")
+ (#Cons (#TextA "var-bindings")
+ #Nil))))]
+ default-def-meta-exported))
+
## (type: Compiler-Mode
## #Release
## #Debug
@@ -592,7 +612,7 @@
## #cursor Cursor
## #modules (List [Text Module])
## #scopes (List Scope)
-## #type-vars (Bindings Nat (Maybe Type))
+## #type-context Type-Context
## #expected (Maybe Type)
## #seed Nat
## #scope-type-vars (List Nat)
@@ -610,8 +630,8 @@
Module))
(#ProdT ## "lux;scopes"
(#AppT List Scope)
- (#ProdT ## "lux;type-vars"
- (#AppT (#AppT Bindings Nat) (#AppT Maybe Type))
+ (#ProdT ## "lux;type-context"
+ Type-Context
(#ProdT ## "lux;expected"
(#AppT Maybe Type)
(#ProdT ## "lux;seed"
@@ -625,7 +645,7 @@
(#Cons (#TextA "cursor")
(#Cons (#TextA "modules")
(#Cons (#TextA "scopes")
- (#Cons (#TextA "type-vars")
+ (#Cons (#TextA "type-context")
(#Cons (#TextA "expected")
(#Cons (#TextA "seed")
(#Cons (#TextA "scope-type-vars")
@@ -1695,7 +1715,7 @@
(-> Ident ($' Lux Ident))
(let' [[module name] ident
{#info info #source source #modules modules
- #scopes scopes #type-vars types #host host
+ #scopes scopes #type-context types #host host
#seed seed #expected expected #cursor cursor
#scope-type-vars scope-type-vars} state]
(_lux_case (get module modules)
@@ -1854,7 +1874,7 @@
($' Lux Text)
(_lux_case state
{#info info #source source #modules modules
- #scopes scopes #type-vars types #host host
+ #scopes scopes #type-context types #host host
#seed seed #expected expected #cursor cursor
#scope-type-vars scope-type-vars}
(_lux_case (reverse scopes)
@@ -2336,7 +2356,7 @@
(function' [state]
(_lux_case state
{#info info #source source #modules modules
- #scopes scopes #type-vars types #host host
+ #scopes scopes #type-context types #host host
#seed seed #expected expected
#cursor cursor
#scope-type-vars scope-type-vars}
@@ -2591,12 +2611,12 @@
(-> Text ($' Lux AST))
(_lux_case state
{#info info #source source #modules modules
- #scopes scopes #type-vars types #host host
+ #scopes scopes #type-context types #host host
#seed seed #expected expected
#cursor cursor
#scope-type-vars scope-type-vars}
(#Right {#info info #source source #modules modules
- #scopes scopes #type-vars types #host host
+ #scopes scopes #type-context types #host host
#seed (n.+ +1 seed) #expected expected
#cursor cursor
#scope-type-vars scope-type-vars}
@@ -3462,7 +3482,7 @@
(-> Text (Lux Module))
(function [state]
(let [{#info info #source source #modules modules
- #scopes scopes #type-vars types #host host
+ #scopes scopes #type-context types #host host
#seed seed #expected expected #cursor cursor
#scope-type-vars scope-type-vars} state]
(case (get name modules)
@@ -3525,7 +3545,7 @@
(Lux Type)
(function [state]
(let [{#info info #source source #modules modules
- #scopes scopes #type-vars types #host host
+ #scopes scopes #type-context types #host host
#seed seed #expected expected #cursor cursor
#scope-type-vars scope-type-vars} state]
(case expected
@@ -4049,7 +4069,7 @@
(-> Text (Lux (List Text)))
(let [modules (case state
{#info info #source source #modules modules
- #scopes scopes #type-vars types #host host
+ #scopes scopes #type-context types #host host
#seed seed #expected expected #cursor cursor
#scope-type-vars scope-type-vars}
modules)]
@@ -4104,7 +4124,7 @@
(-> Text Compiler (Maybe Type))
(case state
{#info info #source source #modules modules
- #scopes scopes #type-vars types #host host
+ #scopes scopes #type-context types #host host
#seed seed #expected expected #cursor cursor
#scope-type-vars scope-type-vars}
(find (: (-> Scope (Maybe Type))
@@ -4126,7 +4146,7 @@
(-> Ident Compiler (Maybe Type))
(let [[v-prefix v-name] name
{#info info #source source #modules modules
- #scopes scopes #type-vars types #host host
+ #scopes scopes #type-context types #host host
#seed seed #expected expected #cursor cursor
#scope-type-vars scope-type-vars} state]
(case (get v-prefix modules)
@@ -4145,7 +4165,7 @@
(-> Ident (Lux [Type Void]))
(let [[v-prefix v-name] name
{#info info #source source #modules modules
- #scopes scopes #type-vars types #host host
+ #scopes scopes #type-context types #host host
#seed seed #expected expected #cursor cursor
#scope-type-vars scope-type-vars} state]
(case (get v-prefix modules)
@@ -5504,7 +5524,7 @@
(Lux (List Nat))
(case state
{#info info #source source #modules modules
- #scopes scopes #type-vars types #host host
+ #scopes scopes #type-context types #host host
#seed seed #expected expected #cursor cursor
#scope-type-vars scope-type-vars}
(#Right state scope-type-vars)
diff --git a/stdlib/source/lux/macro.lux b/stdlib/source/lux/macro.lux
index 5a3d3829d..93920c67b 100644
--- a/stdlib/source/lux/macro.lux
+++ b/stdlib/source/lux/macro.lux
@@ -614,6 +614,11 @@
(function [compiler]
(#;Right [compiler compiler])))
+(def: #export type-context
+ (Lux Type-Context)
+ (function [compiler]
+ (#;Right [compiler (get@ #;type-context compiler)])))
+
(do-template [<macro> <func> <desc>]
[(macro: #export (<macro> tokens)
{#;doc (doc "Performs a macro-expansion and logs the resulting ASTs."
diff --git a/stdlib/source/lux/math/simple.lux b/stdlib/source/lux/math/simple.lux
index 6a2f2f710..6e6e23592 100644
--- a/stdlib/source/lux/math/simple.lux
+++ b/stdlib/source/lux/math/simple.lux
@@ -11,9 +11,9 @@
(type [check])))
(def: (find-type-var id env)
- (-> Nat (Bindings Nat (Maybe Type)) (Lux Type))
+ (-> Nat Type-Context (Lux Type))
(case (list;find (|>. product;left (n.= id))
- (get@ #;mappings env))
+ (get@ #;var-bindings env))
(#;Some [_ (#;Some type)])
(case type
(#;VarT id')
@@ -36,7 +36,7 @@
compiler macro;get-compiler]
(case raw-type
(#;VarT id)
- (find-type-var id (get@ #;type-vars compiler))
+ (find-type-var id (get@ #;type-context compiler))
_
(wrap raw-type))))
diff --git a/stdlib/source/lux/type/auto.lux b/stdlib/source/lux/type/auto.lux
index 95e422b13..bb1ecc1c6 100644
--- a/stdlib/source/lux/type/auto.lux
+++ b/stdlib/source/lux/type/auto.lux
@@ -17,9 +17,9 @@
))
(def: (find-type-var id env)
- (-> Nat (Bindings Nat (Maybe Type)) (Lux Type))
+ (-> Nat Type-Context (Lux Type))
(case (list;find (|>. product;left (n.= id))
- (get@ #;mappings env))
+ (get@ #;var-bindings env))
(#;Some [_ (#;Some type)])
(case type
(#;VarT id')
@@ -42,7 +42,7 @@
compiler macro;get-compiler]
(case raw-type
(#;VarT id)
- (find-type-var id (get@ #;type-vars compiler))
+ (find-type-var id (get@ #;type-context compiler))
_
(wrap raw-type))))
@@ -76,25 +76,25 @@
(case member
["" simple-name]
(macro;either (do Monad<Lux>
- [member (macro;normalize member)
- _ (macro;resolve-tag member)]
- (wrap member))
- (do Monad<Lux>
- [this-module-name macro;current-module-name
- imp-mods (macro;imported-modules this-module-name)
- tag-lists (mapM @ macro;tag-lists imp-mods)
- #let [tag-lists (|> tag-lists List/join (List/map product;left) List/join)
- candidates (list;filter (. (Text/= simple-name) product;right)
- tag-lists)]]
- (case candidates
- #;Nil
- (macro;fail (format "Unknown tag: " (%ident member)))
-
- (#;Cons winner #;Nil)
- (wrap winner)
-
- _
- (macro;fail (format "Too many candidate tags: " (%list %ident candidates))))))
+ [member (macro;normalize member)
+ _ (macro;resolve-tag member)]
+ (wrap member))
+ (do Monad<Lux>
+ [this-module-name macro;current-module-name
+ imp-mods (macro;imported-modules this-module-name)
+ tag-lists (mapM @ macro;tag-lists imp-mods)
+ #let [tag-lists (|> tag-lists List/join (List/map product;left) List/join)
+ candidates (list;filter (. (Text/= simple-name) product;right)
+ tag-lists)]]
+ (case candidates
+ #;Nil
+ (macro;fail (format "Unknown tag: " (%ident member)))
+
+ (#;Cons winner #;Nil)
+ (wrap winner)
+
+ _
+ (macro;fail (format "Too many candidate tags: " (%list %ident candidates))))))
_
(:: Monad<Lux> wrap member)))
@@ -191,22 +191,13 @@
input-types)]
(tc;check output-type member-type')))
-(def: compiler-type-context
- (Lux tc;Context)
- (function [compiler]
- (let [type-vars (get@ #;type-vars compiler)
- context (|> tc;fresh-context
- (set@ #tc;var-counter (get@ #;counter type-vars))
- (set@ #tc;bindings (dict;from-list number;Hash<Nat> (get@ #;mappings type-vars))))]
- (#;Right [compiler context]))))
-
(type: #rec Instance
{#constructor Ident
#dependencies (List Instance)})
(def: (test-provision provision context dep alts)
- (-> (-> Compiler tc;Context Type (Check Instance))
- tc;Context Type (List [Ident Type])
+ (-> (-> Compiler Type-Context Type (Check Instance))
+ Type-Context Type (List [Ident Type])
(Lux (List Instance)))
(do Monad<Lux>
[compiler macro;get-compiler]
@@ -233,12 +224,12 @@
(wrap found))))
(def: (provision compiler context dep)
- (-> Compiler tc;Context Type (Check Instance))
+ (-> Compiler Type-Context Type (Check Instance))
(case (macro;run compiler
- ($_ macro;either
- (do Monad<Lux> [alts local-env] (test-provision provision context dep alts))
- (do Monad<Lux> [alts local-structs] (test-provision provision context dep alts))
- (do Monad<Lux> [alts import-structs] (test-provision provision context dep alts))))
+ ($_ macro;either
+ (do Monad<Lux> [alts local-env] (test-provision provision context dep alts))
+ (do Monad<Lux> [alts local-structs] (test-provision provision context dep alts))
+ (do Monad<Lux> [alts import-structs] (test-provision provision context dep alts))))
(#;Left error)
(tc;fail error)
@@ -258,7 +249,7 @@
(-> Type Nat (List Type) Type (List [Ident Type]) (Lux (List Instance)))
(do Monad<Lux>
[compiler macro;get-compiler
- context compiler-type-context]
+ context macro;type-context]
(case (|> alts
(List/map (function [[alt-name alt-type]]
(case (tc;run context
@@ -357,10 +348,10 @@
_
(macro;fail (format "Too many options available: "
- (|> chosen-ones
- (List/map (. %ident product;left))
- (text;join-with ", "))
- " --- for type: " (%type sig-type)))))
+ (|> chosen-ones
+ (List/map (. %ident product;left))
+ (text;join-with ", "))
+ " --- for type: " (%type sig-type)))))
(#;Right [args _])
(do @
diff --git a/stdlib/source/lux/type/check.lux b/stdlib/source/lux/type/check.lux
index 4d93c9024..1fec0891a 100644
--- a/stdlib/source/lux/type/check.lux
+++ b/stdlib/source/lux/type/check.lux
@@ -7,28 +7,20 @@
monad)
(data [text "Text/" Monoid<Text> Eq<Text>]
text/format
- [number]
maybe
[product]
- (coll [list]
- [dict])
+ (coll [list])
[error #- fail])
[type "Type/" Eq<Type>]
))
-(type: #export Id Nat)
-
(type: #export Fixed (List [[Type Type] Bool]))
-(type: #export Context
- {#var-counter Id
- #ex-counter Id
- #bindings (dict;Dict Id (Maybe Type))
- #fixed Fixed
- })
-
(type: #export (Check a)
- (-> Context (Error [Context a])))
+ (-> Type-Context (Error [Type-Context a])))
+
+(type: #export Type-Vars
+ (List [Nat (Maybe Type)]))
(struct: #export _ (Functor Check)
(def: (map f fa)
@@ -85,9 +77,51 @@
(open Monad<Check> "Check/")
+(def: (var::get id plist)
+ (-> Nat Type-Vars (Maybe (Maybe Type)))
+ (case plist
+ #;Nil
+ #;None
+
+ (#;Cons [var-id var-type]
+ plist')
+ (if (n.= id var-id)
+ (#;Some var-type)
+ (var::get id plist'))
+ ))
+
+(def: (var::put id value plist)
+ (-> Nat (Maybe Type) Type-Vars Type-Vars)
+ (case plist
+ #;Nil
+ (list [id value])
+
+ (#;Cons [var-id var-type]
+ plist')
+ (if (n.= id var-id)
+ (#;Cons [var-id value]
+ plist')
+ (#;Cons [var-id var-type]
+ (var::put id value plist')))
+ ))
+
+(def: (var::remove id plist)
+ (-> Nat Type-Vars Type-Vars)
+ (case plist
+ #;Nil
+ #;Nil
+
+ (#;Cons [var-id var-type]
+ plist')
+ (if (n.= id var-id)
+ plist'
+ (#;Cons [var-id var-type]
+ (var::remove id plist')))
+ ))
+
## [[Logic]]
(def: #export (run context proc)
- (All [a] (-> Context (Check a) (Error a)))
+ (All [a] (-> Type-Context (Check a) (Error a)))
(case (proc context)
(#;Left error)
(#;Left error)
@@ -107,16 +141,16 @@
(def: #export existential
{#;doc "A producer of existential types."}
- (Check [Id Type])
+ (Check [Nat Type])
(function [context]
- (let [id (get@ #ex-counter context)]
- (#;Right [(update@ #ex-counter n.inc context)
+ (let [id (get@ #;ex-counter context)]
+ (#;Right [(update@ #;ex-counter n.inc context)
[id (#;ExT id)]]))))
(def: #export (bound? id)
- (-> Id (Check Bool))
+ (-> Nat (Check Bool))
(function [context]
- (case (|> context (get@ #bindings) (dict;get id))
+ (case (|> context (get@ #;var-bindings) (var::get id))
(#;Some (#;Some _))
(#;Right [context true])
@@ -127,9 +161,9 @@
(#;Left (format "Unknown type-var: " (%n id))))))
(def: #export (read-var id)
- (-> Id (Check Type))
+ (-> Nat (Check Type))
(function [context]
- (case (|> context (get@ #bindings) (dict;get id))
+ (case (|> context (get@ #;var-bindings) (var::get id))
(#;Some (#;Some type))
(#;Right [context type])
@@ -140,43 +174,43 @@
(#;Left (format "Unknown type-var: " (%n id))))))
(def: #export (write-var id type)
- (-> Id Type (Check Unit))
+ (-> Nat Type (Check Unit))
(function [context]
- (case (|> context (get@ #bindings) (dict;get id))
+ (case (|> context (get@ #;var-bindings) (var::get id))
(#;Some (#;Some bound))
(#;Left (format "Cannot rebind type-var: " (%n id) " | Current type: " (%type bound)))
(#;Some #;None)
- (#;Right [(update@ #bindings (dict;put id (#;Some type)) context)
+ (#;Right [(update@ #;var-bindings (var::put id (#;Some type)) context)
[]])
#;None
(#;Left (format "Unknown type-var: " (%n id))))))
(def: (rewrite-var id type)
- (-> Id Type (Check Unit))
+ (-> Nat Type (Check Unit))
(function [context]
- (case (|> context (get@ #bindings) (dict;get id))
+ (case (|> context (get@ #;var-bindings) (var::get id))
(#;Some _)
- (#;Right [(update@ #bindings (dict;put id (#;Some type)) context)
+ (#;Right [(update@ #;var-bindings (var::put id (#;Some type)) context)
[]])
#;None
(#;Left (format "Unknown type-var: " (%n id))))))
(def: #export (clear-var id)
- (-> Id (Check Unit))
+ (-> Nat (Check Unit))
(function [context]
- (case (|> context (get@ #bindings) (dict;get id))
+ (case (|> context (get@ #;var-bindings) (var::get id))
(#;Some _)
- (#;Right [(update@ #bindings (dict;put id #;None) context)
+ (#;Right [(update@ #;var-bindings (var::put id #;None) context)
[]])
#;None
(#;Left (format "Unknown type-var: " (%n id))))))
(def: #export (clean t-id type)
- (-> Id Type (Check Type))
+ (-> Nat Type (Check Type))
(case type
(#;VarT id)
(if (n.= t-id id)
@@ -237,33 +271,28 @@
))
(def: #export create-var
- (Check [Id Type])
+ (Check [Nat Type])
(function [context]
- (let [id (get@ #var-counter context)]
+ (let [id (get@ #;var-counter context)]
(#;Right [(|> context
- (update@ #var-counter n.inc)
- (update@ #bindings (dict;put id #;None)))
+ (update@ #;var-counter n.inc)
+ (update@ #;var-bindings (var::put id #;None)))
[id (#;VarT id)]]))))
-(do-template [<get> <set> <tag> <type>]
- [(def: <get>
- (Check <type>)
- (function [context]
- (#;Right [context
- (get@ <tag> context)])))
-
- (def: (<set> value)
- (-> <type> (Check Unit))
- (function [context]
- (#;Right [(set@ <tag> value context)
- []])))]
-
- [get-bindings set-bindings #bindings (dict;Dict Id (Maybe Type))]
- [get-fixed set-fixed #fixed Fixed]
- )
+(def: get-bindings
+ (Check (List [Nat (Maybe Type)]))
+ (function [context]
+ (#;Right [context
+ (get@ #;var-bindings context)])))
+
+(def: (set-bindings value)
+ (-> (List [Nat (Maybe Type)]) (Check Unit))
+ (function [context]
+ (#;Right [(set@ #;var-bindings value context)
+ []])))
(def: #export (delete-var id)
- (-> Id (Check Unit))
+ (-> Nat (Check Unit))
(do Monad<Check>
[? (bound? id)
_ (if ?
@@ -292,11 +321,11 @@
[b-type'' (clean id b-type')]
(wrap [b-id (#;Some b-type'')])))
)))
- (dict;entries bindings))]
- (set-bindings (|> bindings' (dict;from-list number;Hash<Nat>) (dict;remove id)))))
+ bindings)]
+ (set-bindings (var::remove id bindings'))))
(def: #export (with-var k)
- (All [a] (-> (-> [Id Type] (Check a)) (Check a)))
+ (All [a] (-> (-> [Nat Type] (Check a)) (Check a)))
(do Monad<Check>
[[id var] create-var
output (k [id var])
@@ -304,11 +333,10 @@
(wrap output)))
(def: #export fresh-context
- Context
- {#var-counter +0
- #ex-counter +0
- #bindings (dict;new number;Hash<Nat>)
- #fixed (list)
+ Type-Context
+ {#;var-counter +0
+ #;ex-counter +0
+ #;var-bindings (list)
})
(def: (attempt op)
@@ -327,12 +355,10 @@
(#;Left message)))
(def: (fail-check expected actual)
- (-> Type Type (Check Unit))
+ (All [a] (-> Type Type (Check a)))
(fail (format "Expected: " (%type expected) "\n\n"
"Actual: " (%type actual))))
-(def: success (Check Unit) (Check/wrap []))
-
(def: (either left right)
(All [a] (-> (Check a) (Check a) (Check a)))
(function [context]
@@ -355,158 +381,171 @@
(-> [Type Type] Bool Fixed Fixed)
(#;Cons [ea status] fixed))
-(def: #export (check expected actual)
+(def: #export (check' expected actual fixed)
{#;doc "Type-check to ensure that the 'expected' type subsumes the 'actual' type."}
- (-> Type Type (Check Unit))
+ (-> Type Type Fixed (Check Fixed))
(if (is expected actual)
- success
+ (Check/wrap fixed)
(case [expected actual]
[(#;VarT e-id) (#;VarT a-id)]
(if (n.= e-id a-id)
- success
+ (Check/wrap fixed)
(do Monad<Check>
[ebound (attempt (read-var e-id))
abound (attempt (read-var a-id))]
(case [ebound abound]
[#;None #;None]
- (write-var e-id actual)
+ (do @
+ [_ (write-var e-id actual)]
+ (wrap fixed))
[(#;Some etype) #;None]
- (check etype actual)
+ (check' etype actual fixed)
[#;None (#;Some atype)]
- (check expected atype)
+ (check' expected atype fixed)
[(#;Some etype) (#;Some atype)]
- (check etype atype))))
+ (check' etype atype fixed))))
[(#;VarT id) _]
- (either (write-var id actual)
+ (either (do Monad<Check>
+ [_ (write-var id actual)]
+ (wrap fixed))
(do Monad<Check>
[bound (read-var id)]
- (check bound actual)))
+ (check' bound actual fixed)))
[_ (#;VarT id)]
- (either (write-var id expected)
+ (either (do Monad<Check>
+ [_ (write-var id expected)]
+ (wrap fixed))
(do Monad<Check>
[bound (read-var id)]
- (check expected bound)))
+ (check' expected bound fixed)))
[(#;AppT (#;ExT eid) eA) (#;AppT (#;ExT aid) aA)]
(if (n.= eid aid)
- (check eA aA)
+ (check' eA aA fixed)
(fail-check expected actual))
[(#;AppT (#;VarT id) A1) (#;AppT F2 A2)]
(either (do Monad<Check>
[F1 (read-var id)]
- (check (#;AppT F1 A1) actual))
+ (check' (#;AppT F1 A1) actual fixed))
(do Monad<Check>
- [_ (check (#;VarT id) F2)
+ [fixed (check' (#;VarT id) F2 fixed)
e' (apply-type! F2 A1)
a' (apply-type! F2 A2)]
- (check e' a')))
+ (check' e' a' fixed)))
[(#;AppT F1 A1) (#;AppT (#;VarT id) A2)]
(either (do Monad<Check>
[F2 (read-var id)]
- (check expected (#;AppT F2 A2)))
+ (check' expected (#;AppT F2 A2) fixed))
(do Monad<Check>
- [_ (check F1 (#;VarT id))
+ [fixed (check' F1 (#;VarT id) fixed)
e' (apply-type! F1 A1)
a' (apply-type! F1 A2)]
- (check e' a')))
+ (check' e' a' fixed)))
[(#;AppT F A) _]
- (do Monad<Check>
- [#let [fx-pair [expected actual]]
- fixed get-fixed]
+ (let [fx-pair [expected actual]]
(case (fx-get fx-pair fixed)
(#;Some ?)
(if ?
- success
+ (Check/wrap fixed)
(fail-check expected actual))
#;None
(do Monad<Check>
- [expected' (apply-type! F A)
- _ (set-fixed (fx-put fx-pair true fixed))]
- (check expected' actual))))
+ [expected' (apply-type! F A)]
+ (check' expected' actual (fx-put fx-pair true fixed)))))
[_ (#;AppT F A)]
(do Monad<Check>
[actual' (apply-type! F A)]
- (check expected actual'))
+ (check' expected actual' fixed))
[(#;UnivQ _) _]
(do Monad<Check>
[[ex-id ex] existential
expected' (apply-type! expected ex)]
- (check expected' actual))
+ (check' expected' actual fixed))
[_ (#;UnivQ _)]
(with-var
(function [[var-id var]]
(do Monad<Check>
[actual' (apply-type! actual var)
- =output (check expected actual')
+ fixed (check' expected actual' fixed)
_ (clean var-id expected)]
- success)))
+ (Check/wrap fixed))))
[(#;ExQ e!env e!def) _]
(with-var
(function [[var-id var]]
(do Monad<Check>
[expected' (apply-type! expected var)
- =output (check expected' actual)
+ fixed (check' expected' actual fixed)
_ (clean var-id actual)]
- success)))
+ (Check/wrap fixed))))
[_ (#;ExQ a!env a!def)]
(do Monad<Check>
[[ex-id ex] existential
actual' (apply-type! actual ex)]
- (check expected actual'))
+ (check' expected actual' fixed))
[(#;HostT e-name e-params) (#;HostT a-name a-params)]
- (if (Text/= e-name a-name)
+ (if (and (Text/= e-name a-name)
+ (n.= (list;size e-params)
+ (list;size a-params)))
(do Monad<Check>
- [_ (mapM Monad<Check>
- (function [[e a]] (check e a))
- (list;zip2 e-params a-params))]
- success)
+ [fixed (foldM Monad<Check>
+ (function [[e a] fixed] (check' e a fixed))
+ fixed
+ (list;zip2 e-params a-params))]
+ (Check/wrap fixed))
(fail-check expected actual))
(^template [<unit> <append>]
[<unit> <unit>]
- success
+ (Check/wrap fixed)
[(<append> eL eR) (<append> aL aR)]
(do Monad<Check>
- [_ (check eL aL)]
- (check eR aR)))
+ [fixed (check' eL aL fixed)]
+ (check' eR aR fixed)))
([#;VoidT #;SumT]
[#;UnitT #;ProdT])
[(#;FunctionT eI eO) (#;FunctionT aI aO)]
(do Monad<Check>
- [_ (check aI eI)]
- (check eO aO))
+ [fixed (check' aI eI fixed)]
+ (check' eO aO fixed))
[(#;ExT e!id) (#;ExT a!id)]
(if (n.= e!id a!id)
- success
+ (Check/wrap fixed)
(fail-check expected actual))
[(#;NamedT _ ?etype) _]
- (check ?etype actual)
+ (check' ?etype actual fixed)
[_ (#;NamedT _ ?atype)]
- (check expected ?atype)
+ (check' expected ?atype fixed)
_
(fail-check expected actual))))
+(def: #export (check expected actual)
+ {#;doc "Type-check to ensure that the 'expected' type subsumes the 'actual' type."}
+ (-> Type Type (Check Unit))
+ (do Monad<Check>
+ [fixed (check' expected actual (list))]
+ (wrap [])))
+
(def: #export (checks? expected actual)
{#;doc "A simple type-checking function that just returns a yes/no answer."}
(-> Type Type Bool)
@@ -518,6 +557,6 @@
true))
(def: #export get-context
- (Check Context)
+ (Check Type-Context)
(function [context]
(#;Right [context context])))
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-16 07:26:23 +0000