From ccabfc6a5e41650788199cb8fd5d87731f094bcd Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Wed, 11 Oct 2017 17:11:18 -0400 Subject: - Small refactorings. --- stdlib/source/lux/type.lux | 6 +++ stdlib/source/lux/type/auto.lux | 4 +- stdlib/source/lux/type/check.lux | 84 ++++++++++++++++++++-------------------- 3 files changed, 50 insertions(+), 44 deletions(-) diff --git a/stdlib/source/lux/type.lux b/stdlib/source/lux/type.lux index acdbab38d..117d77043 100644 --- a/stdlib/source/lux/type.lux +++ b/stdlib/source/lux/type.lux @@ -346,3 +346,9 @@ _ false)) + +(def: #export (array level elem-type) + (-> Nat Type Type) + (case level + +0 elem-type + _ (#;Host "#Array" (list (array (n.dec level) elem-type))))) diff --git a/stdlib/source/lux/type/auto.lux b/stdlib/source/lux/type/auto.lux index 9bb8a5657..67d1455a1 100644 --- a/stdlib/source/lux/type/auto.lux +++ b/stdlib/source/lux/type/auto.lux @@ -156,7 +156,7 @@ (#;UnivQ _) (do Monad - [[id var] tc;create-var] + [[id var] tc;create] (apply-function-type (maybe;assume (type;apply (list var) func)) arg)) @@ -173,7 +173,7 @@ (case type (#;UnivQ _) (do Monad - [[id var] tc;create-var + [[id var] tc;create [ids final-output] (concrete-type (maybe;assume (type;apply (list var) type)))] (wrap [(#;Cons id ids) final-output])) diff --git a/stdlib/source/lux/type/check.lux b/stdlib/source/lux/type/check.lux index b3ae0a04d..769b45391 100644 --- a/stdlib/source/lux/type/check.lux +++ b/stdlib/source/lux/type/check.lux @@ -160,7 +160,7 @@ #;None (#R;Error ($_ text/compose "Unknown type-var: " (nat/encode id)))))) -(def: #export (read-var id) +(def: #export (read id) (-> Nat (Check Type)) (function [context] (case (|> context (get@ #;var-bindings) (var::get id)) @@ -173,7 +173,7 @@ #;None (#R;Error ($_ text/compose "Unknown type-var: " (nat/encode id)))))) -(def: #export (write-var id type) +(def: #export (write id type) (-> Nat Type (Check Unit)) (function [context] (case (|> context (get@ #;var-bindings) (var::get id)) @@ -187,7 +187,7 @@ #;None (#R;Error ($_ text/compose "Unknown type-var: " (nat/encode id)))))) -(def: (rewrite-var id type) +(def: (update id type) (-> Nat Type (Check Unit)) (function [context] (case (|> context (get@ #;var-bindings) (var::get id)) @@ -198,7 +198,7 @@ #;None (#R;Error ($_ text/compose "Unknown type-var: " (nat/encode id)))))) -(def: #export (clear-var id) +(def: #export (clear id) (-> Nat (Check Unit)) (function [context] (case (|> context (get@ #;var-bindings) (var::get id)) @@ -217,27 +217,27 @@ (do Monad [? (bound? id)] (if ? - (read-var id) + (read id) (wrap type))) (do Monad [? (bound? id)] (if ? (do Monad - [=type (read-var id) + [=type (read id) ==type (clean t-id =type)] (case ==type (#;Var =id) (if (n.= t-id =id) (do Monad - [_ (clear-var id)] + [_ (clear id)] (wrap type)) (do Monad - [_ (rewrite-var id ==type)] + [_ (update id ==type)] (wrap type))) _ (do Monad - [_ (rewrite-var id ==type)] + [_ (update id ==type)] (wrap type)))) (wrap type)))) @@ -270,7 +270,7 @@ (:: Monad wrap type) )) -(def: #export create-var +(def: #export create (Check [Nat Type]) (function [context] (let [id (get@ #;var-counter context)] @@ -291,18 +291,18 @@ (#R;Success [(set@ #;var-bindings value context) []]))) -(def: #export (delete-var id) +(def: #export (delete id) (-> Nat (Check Unit)) (function [context] (#R;Success [(update@ #;var-bindings (var::remove id) context) []]))) -(def: #export (with-var k) +(def: #export (with k) (All [a] (-> (-> [Nat Type] (Check a)) (Check a))) (do Monad - [[id var] create-var + [[id var] create output (k [id var]) - _ (delete-var id)] + _ (delete id)] (wrap output))) (def: #export fresh-context @@ -355,15 +355,15 @@ (-> [Type Type] Bool Assumptions Assumptions) (#;Cons [ea status] assumptions)) -(def: (on-var id type then else) +(def: (on id type then else) (All [a] (-> Nat Type (Check a) (-> Type (Check a)) (Check a))) (either (do Monad - [_ (write-var id type)] + [_ (write id type)] then) (do Monad - [bound (read-var id)] + [bound (read id)] (else bound)))) (def: #export (check' expected actual assumptions) @@ -376,12 +376,12 @@ (if (n.= e-id a-id) (Check/wrap assumptions) (do Monad - [ebound (attempt (read-var e-id)) - abound (attempt (read-var a-id))] + [ebound (attempt (read e-id)) + abound (attempt (read a-id))] (case [ebound abound] [#;None #;None] (do @ - [_ (write-var e-id actual)] + [_ (write e-id actual)] (wrap assumptions)) [(#;Some etype) #;None] @@ -394,14 +394,14 @@ (check' etype atype assumptions)))) [(#;Var id) _] - (on-var id actual (Check/wrap assumptions) - (function [bound] - (check' bound actual assumptions))) + (on id actual (Check/wrap assumptions) + (function [bound] + (check' bound actual assumptions))) [_ (#;Var id)] - (on-var id expected (Check/wrap assumptions) - (function [bound] - (check' expected bound assumptions))) + (on id expected (Check/wrap assumptions) + (function [bound] + (check' expected bound assumptions))) [(#;Apply eA (#;Ex eid)) (#;Apply aA (#;Ex aid))] (if (n.= eid aid) @@ -410,7 +410,7 @@ [(#;Apply A1 (#;Var id)) (#;Apply A2 F2)] (either (do Monad - [F1 (read-var id)] + [F1 (read id)] (check' (#;Apply A1 F1) actual assumptions)) (do Monad [assumptions (check' (#;Var id) F2 assumptions) @@ -420,7 +420,7 @@ [(#;Apply A1 F1) (#;Apply A2 (#;Var id))] (either (do Monad - [F2 (read-var id)] + [F2 (read id)] (check' expected (#;Apply A2 F2) assumptions)) (do Monad [assumptions (check' F1 (#;Var id) assumptions) @@ -453,22 +453,22 @@ (check' expected' actual assumptions)) [_ (#;UnivQ _)] - (with-var - (function [[var-id var]] - (do Monad - [actual' (apply-type! actual var) - assumptions (check' expected actual' assumptions) - _ (clean var-id expected)] - (Check/wrap assumptions)))) + (with + (function [[var-id var]] + (do Monad + [actual' (apply-type! actual var) + assumptions (check' expected actual' assumptions) + _ (clean var-id expected)] + (Check/wrap assumptions)))) [(#;ExQ e!env e!def) _] - (with-var - (function [[var-id var]] - (do Monad - [expected' (apply-type! expected var) - assumptions (check' expected' actual assumptions) - _ (clean var-id actual)] - (Check/wrap assumptions)))) + (with + (function [[var-id var]] + (do Monad + [expected' (apply-type! expected var) + assumptions (check' expected' actual assumptions) + _ (clean var-id actual)] + (Check/wrap assumptions)))) [_ (#;ExQ a!env a!def)] (do Monad -- cgit v1.2.3