aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/lux/type
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--stdlib/source/lux/type.lux136
-rw-r--r--stdlib/source/lux/type/abstract.lux134
-rw-r--r--stdlib/source/lux/type/check.lux242
-rw-r--r--stdlib/source/lux/type/dynamic.lux10
-rw-r--r--stdlib/source/lux/type/implicit.lux222
-rw-r--r--stdlib/source/lux/type/refinement.lux14
-rw-r--r--stdlib/source/lux/type/resource.lux68
-rw-r--r--stdlib/source/lux/type/unit.lux34
8 files changed, 430 insertions, 430 deletions
diff --git a/stdlib/source/lux/type.lux b/stdlib/source/lux/type.lux
index 1d390b8b6..bfdfd94f9 100644
--- a/stdlib/source/lux/type.lux
+++ b/stdlib/source/lux/type.lux
@@ -26,34 +26,34 @@
(template [<name> <tag>]
[(def: #export (<name> type)
(-> Type [Nat Type])
- (loop [num-args 0
+ (loop [num_args 0
type type]
(case type
- (<tag> env sub-type)
- (recur (inc num-args) sub-type)
+ (<tag> env sub_type)
+ (recur (inc num_args) sub_type)
_
- [num-args type])))]
+ [num_args type])))]
- [flatten-univ-q #.UnivQ]
- [flatten-ex-q #.ExQ]
+ [flatten_univ_q #.UnivQ]
+ [flatten_ex_q #.ExQ]
)
-(def: #export (flatten-function type)
+(def: #export (flatten_function type)
(-> Type [(List Type) Type])
(case type
(#.Function in out')
- (let [[ins out] (flatten-function out')]
+ (let [[ins out] (flatten_function out')]
[(list& in ins) out])
_
[(list) type]))
-(def: #export (flatten-application type)
+(def: #export (flatten_application type)
(-> Type [Type (List Type)])
(case type
(#.Apply arg func')
- (let [[func args] (flatten-application func')]
+ (let [[func args] (flatten_application func')]
[func (list\compose args (list arg))])
_
@@ -69,8 +69,8 @@
_
(list type)))]
- [flatten-variant #.Sum]
- [flatten-tuple #.Product]
+ [flatten_variant #.Sum]
+ [flatten_tuple #.Product]
)
(def: #export (format type)
@@ -79,7 +79,7 @@
(#.Primitive name params)
($_ text\compose
"(primitive "
- (text.enclose' text.double-quote name)
+ (text.enclose' text.double_quote name)
(|> params
(list\map (|>> format (text\compose " ")))
(list\fold (function.flip text\compose) ""))
@@ -94,11 +94,11 @@
(list.interpose " ")
(list\fold text\compose ""))
<close>)])
- ([#.Sum "(| " ")" flatten-variant]
- [#.Product "[" "]" flatten-tuple])
+ ([#.Sum "(| " ")" flatten_variant]
+ [#.Product "[" "]" flatten_tuple])
(#.Function input output)
- (let [[ins out] (flatten-function type)]
+ (let [[ins out] (flatten_function type)]
($_ text\compose "(-> "
(|> ins
(list\map format)
@@ -117,12 +117,12 @@
($_ text\compose "⟨e:" (n\encode id) "⟩")
(#.Apply param fun)
- (let [[type-func type-args] (flatten-application type)]
- ($_ text\compose "(" (format type-func) " " (|> type-args (list\map format) list.reverse (list.interpose " ") (list\fold text\compose "")) ")"))
+ (let [[type_func type_args] (flatten_application type)]
+ ($_ text\compose "(" (format type_func) " " (|> type_args (list\map format) list.reverse (list.interpose " ") (list\fold text\compose "")) ")"))
(^template [<tag> <desc>]
[(<tag> env body)
- ($_ text\compose "(" <desc> " {" (|> env (list\map format) (text.join-with " ")) "} " (format body) ")")])
+ ($_ text\compose "(" <desc> " {" (|> env (list\map format) (text.join_with " ")) "} " (format body) ")")])
([#.UnivQ "All"]
[#.ExQ "Ex"])
@@ -130,40 +130,40 @@
($_ text\compose module "." name)
))
-(def: (beta-reduce env type)
+(def: (beta_reduce env type)
(-> (List Type) Type Type)
(case type
(#.Primitive name params)
- (#.Primitive name (list\map (beta-reduce env) params))
+ (#.Primitive name (list\map (beta_reduce env) params))
(^template [<tag>]
[(<tag> left right)
- (<tag> (beta-reduce env left) (beta-reduce env right))])
+ (<tag> (beta_reduce env left) (beta_reduce env right))])
([#.Sum] [#.Product]
[#.Function] [#.Apply])
(^template [<tag>]
- [(<tag> old-env def)
- (case old-env
+ [(<tag> old_env def)
+ (case old_env
#.Nil
(<tag> env def)
_
- (<tag> (list\map (beta-reduce env) old-env) def))])
+ (<tag> (list\map (beta_reduce env) old_env) def))])
([#.UnivQ]
[#.ExQ])
(#.Parameter idx)
(maybe.default (error! ($_ text\compose
- "Unknown type parameter" text.new-line
- " Index: " (n\encode idx) text.new-line
+ "Unknown type parameter" text.new_line
+ " Index: " (n\encode idx) text.new_line
"Environment: " (|> env
list.enumeration
(list\map (.function (_ [index type])
($_ text\compose
(n\encode index)
" " (..format type))))
- (text.join-with (text\compose text.new-line " ")))))
+ (text.join_with (text\compose text.new_line " ")))))
(list.nth idx env))
_
@@ -225,7 +225,7 @@
(^template [<tag>]
[(<tag> env body)
(|> body
- (beta-reduce (list& func param env))
+ (beta_reduce (list& func param env))
(apply params'))])
([#.UnivQ] [#.ExQ])
@@ -238,12 +238,12 @@
_
#.None)))
-(def: #export (to-code type)
+(def: #export (to_code type)
(-> Type Code)
(case type
(#.Primitive name params)
(` (#.Primitive (~ (code.text name))
- (.list (~+ (list\map to-code params)))))
+ (.list (~+ (list\map to_code params)))))
(^template [<tag>]
[(<tag> idx)
@@ -252,34 +252,34 @@
(^template [<tag>]
[(<tag> left right)
- (` (<tag> (~ (to-code left))
- (~ (to-code right))))])
+ (` (<tag> (~ (to_code left))
+ (~ (to_code right))))])
([#.Sum] [#.Product] [#.Function] [#.Apply])
- (#.Named name sub-type)
+ (#.Named name sub_type)
(code.identifier name)
(^template [<tag>]
[(<tag> env body)
- (` (<tag> (.list (~+ (list\map to-code env)))
- (~ (to-code body))))])
+ (` (<tag> (.list (~+ (list\map to_code env)))
+ (~ (to_code body))))])
([#.UnivQ] [#.ExQ])
))
-(def: #export (un-alias type)
+(def: #export (un_alias type)
(-> Type Type)
(case type
(#.Named _ (#.Named name type'))
- (un-alias (#.Named name type'))
+ (un_alias (#.Named name type'))
_
type))
-(def: #export (un-name type)
+(def: #export (un_name type)
(-> Type Type)
(case type
(#.Named name type')
- (un-name type')
+ (un_name type')
_
type))
@@ -326,8 +326,8 @@
0 body
_ (|> body (<name> (dec size)) (<tag> (list)))))]
- [univ-q #.UnivQ]
- [ex-q #.ExQ]
+ [univ_q #.UnivQ]
+ [ex_q #.ExQ]
)
(def: #export (quantified? type)
@@ -348,53 +348,53 @@
_
#0))
-(def: #export (array depth elem-type)
+(def: #export (array depth elem_type)
(-> Nat Type Type)
(case depth
- 0 elem-type
- _ (|> elem-type (array (dec depth)) (list) (#.Primitive array.type-name))))
+ 0 elem_type
+ _ (|> elem_type (array (dec depth)) (list) (#.Primitive array.type_name))))
-(syntax: (new-secret-marker)
- (meta.with-gensyms [g!_secret-marker_]
- (wrap (list g!_secret-marker_))))
+(syntax: (new_secret_marker)
+ (meta.with_gensyms [g!_secret_marker_]
+ (wrap (list g!_secret_marker_))))
-(def: secret-marker
- (`` (name-of (~~ (new-secret-marker)))))
+(def: secret_marker
+ (`` (name_of (~~ (new_secret_marker)))))
(syntax: #export (:log! {input (<>.or (<>.and <c>.identifier
- (<>.maybe (<>.after (<c>.identifier! ..secret-marker) <c>.any)))
+ (<>.maybe (<>.after (<c>.identifier! ..secret_marker) <c>.any)))
<c>.any)})
(case input
(#.Left [valueN valueC])
(do meta.monad
[location meta.location
- valueT (meta.find-type valueN)
+ valueT (meta.find_type valueN)
#let [_ (log! ($_ text\compose
- (name\encode (name-of ..:log!)) " " (location.format location) text.new-line
+ (name\encode (name_of ..:log!)) " " (location.format location) text.new_line
"Expression: " (case valueC
(#.Some valueC)
(code.format valueC)
#.None
(name\encode valueN))
- text.new-line
+ text.new_line
" Type: " (..format valueT)))]]
(wrap (list (code.identifier valueN))))
(#.Right valueC)
- (meta.with-gensyms [g!value]
+ (meta.with_gensyms [g!value]
(wrap (list (` (.let [(~ g!value) (~ valueC)]
- (..:log! (~ valueC) (~ (code.identifier ..secret-marker)) (~ g!value)))))))))
+ (..:log! (~ valueC) (~ (code.identifier ..secret_marker)) (~ g!value)))))))))
-(def: type-parameters
+(def: type_parameters
(Parser (List Text))
- (<c>.tuple (<>.some <c>.local-identifier)))
+ (<c>.tuple (<>.some <c>.local_identifier)))
-(syntax: #export (:cast {type-vars type-parameters}
+(syntax: #export (:cast {type_vars type_parameters}
input
output
{value (<>.maybe <c>.any)})
- (let [casterC (` (: (All [(~+ (list\map code.local-identifier type-vars))]
+ (let [casterC (` (: (All [(~+ (list\map code.local_identifier type_vars))]
(-> (~ input) (~ output)))
(|>> :assume)))]
(case value
@@ -413,28 +413,28 @@
(<c>.record (<>.and <c>.any <c>.any)))
## TODO: Make sure the generated code always gets optimized away.
-(syntax: #export (:share {type-vars type-parameters}
+(syntax: #export (:share {type_vars type_parameters}
{exemplar typed}
{computation typed})
- (meta.with-gensyms [g!_]
- (let [shareC (` (: (All [(~+ (list\map code.local-identifier type-vars))]
+ (meta.with_gensyms [g!_]
+ (let [shareC (` (: (All [(~+ (list\map code.local_identifier type_vars))]
(-> (~ (get@ #type exemplar))
(~ (get@ #type computation))))
(.function ((~ g!_) (~ g!_))
(~ (get@ #expression computation)))))]
(wrap (list (` ((~ shareC) (~ (get@ #expression exemplar)))))))))
-(syntax: #export (:by-example {type-vars type-parameters}
+(syntax: #export (:by_example {type_vars type_parameters}
{exemplar typed}
{extraction <c>.any})
(wrap (list (` (:of ((~! :share)
- [(~+ (list\map code.local-identifier type-vars))]
+ [(~+ (list\map code.local_identifier type_vars))]
{(~ (get@ #type exemplar))
(~ (get@ #expression exemplar))}
{(~ extraction)
(:assume [])}))))))
-(exception: #export (hole-type {location Location} {type Type})
+(exception: #export (hole_type {location Location} {type Type})
(exception.report
["Location" (location.format location)]
["Type" (..format type)]))
@@ -442,5 +442,5 @@
(syntax: #export (:hole)
(do meta.monad
[location meta.location
- expectedT meta.expected-type]
- (meta.fail (exception.construct ..hole-type [location expectedT]))))
+ expectedT meta.expected_type]
+ (meta.fail (exception.construct ..hole_type [location expectedT]))))
diff --git a/stdlib/source/lux/type/abstract.lux b/stdlib/source/lux/type/abstract.lux
index 604984c10..1aa673f41 100644
--- a/stdlib/source/lux/type/abstract.lux
+++ b/stdlib/source/lux/type/abstract.lux
@@ -37,7 +37,7 @@
(type: #export Frame
{#name Text
- #type-vars (List Code)
+ #type_vars (List Code)
#abstraction Code
#representation Code})
@@ -48,49 +48,49 @@
(template: (!peek <source> <reference> <then>)
(loop [entries <source>]
(case entries
- (#.Cons [head-name head] tail)
- (if (text\= <reference> head-name)
+ (#.Cons [head_name head] tail)
+ (if (text\= <reference> head_name)
<then>
(recur tail))
#.Nil
(undefined))))
-(def: (peek-frames-definition reference source)
+(def: (peek_frames_definition reference source)
(-> Text (List [Text Global]) (Stack Frame))
(!peek source reference
(case head
(#.Left _)
(undefined)
- (#.Right [exported? frame-type frame-anns frame-value])
- (:coerce (Stack Frame) frame-value))))
+ (#.Right [exported? frame_type frame_anns frame_value])
+ (:coerce (Stack Frame) frame_value))))
-(def: (peek-frames reference definition-reference source)
+(def: (peek_frames reference definition_reference source)
(-> Text Text (List [Text Module]) (Stack Frame))
(!peek source reference
- (peek-frames-definition definition-reference (get@ #.definitions head))))
+ (peek_frames_definition definition_reference (get@ #.definitions head))))
-(exception: #export no-active-frames)
+(exception: #export no_active_frames)
(def: (peek! frame)
(-> (Maybe Text) (Meta Frame))
(function (_ compiler)
- (let [[reference definition-reference] (name-of ..frames)
- current-frames (peek-frames reference definition-reference (get@ #.modules compiler))]
+ (let [[reference definition_reference] (name_of ..frames)
+ current_frames (peek_frames reference definition_reference (get@ #.modules compiler))]
(case (case frame
(#.Some frame)
(list.find (function (_ [actual _])
(text\= frame actual))
- current-frames)
+ current_frames)
#.None
- (..peek current-frames))
+ (..peek current_frames))
(#.Some frame)
(#.Right [compiler frame])
#.None
- (exception.throw ..no-active-frames [])))))
+ (exception.throw ..no_active_frames [])))))
(def: #export current
(Meta Frame)
@@ -103,131 +103,131 @@
(template: (!push <source> <reference> <then>)
(loop [entries <source>]
(case entries
- (#.Cons [head-name head] tail)
- (if (text\= <reference> head-name)
- (#.Cons [head-name <then>]
+ (#.Cons [head_name head] tail)
+ (if (text\= <reference> head_name)
+ (#.Cons [head_name <then>]
tail)
- (#.Cons [head-name head]
+ (#.Cons [head_name head]
(recur tail)))
#.Nil
(undefined))))
-(def: (push-frame-definition reference frame source)
+(def: (push_frame_definition reference frame source)
(-> Text Frame (List [Text Global]) (List [Text Global]))
(!push source reference
(case head
(#.Left _)
(undefined)
- (#.Right [exported? frames-type frames-anns frames-value])
+ (#.Right [exported? frames_type frames_anns frames_value])
(#.Right [exported?
- frames-type
- frames-anns
- (..push frame (:coerce (Stack Frame) frames-value))]))))
+ frames_type
+ frames_anns
+ (..push frame (:coerce (Stack Frame) frames_value))]))))
-(def: (push-frame [module-reference definition-reference] frame source)
+(def: (push_frame [module_reference definition_reference] frame source)
(-> Name Frame (List [Text Module]) (List [Text Module]))
- (!push source module-reference
- (update@ #.definitions (push-frame-definition definition-reference frame) head)))
+ (!push source module_reference
+ (update@ #.definitions (push_frame_definition definition_reference frame) head)))
(def: (push! frame)
(-> Frame (Meta Any))
(function (_ compiler)
(#.Right [(update@ #.modules
- (..push-frame (name-of ..frames) frame)
+ (..push_frame (name_of ..frames) frame)
compiler)
[]])))
-(def: (pop-frame-definition reference source)
+(def: (pop_frame_definition reference source)
(-> Text (List [Text Global]) (List [Text Global]))
(!push source reference
(case head
(#.Left _)
(undefined)
- (#.Right [exported? frames-type frames-anns frames-value])
+ (#.Right [exported? frames_type frames_anns frames_value])
(#.Right [exported?
- frames-type
- frames-anns
- (let [current-frames (:coerce (Stack Frame) frames-value)]
- (case (..pop current-frames)
- (#.Some current-frames')
- current-frames'
+ frames_type
+ frames_anns
+ (let [current_frames (:coerce (Stack Frame) frames_value)]
+ (case (..pop current_frames)
+ (#.Some current_frames')
+ current_frames'
#.None
- current-frames))]))))
+ current_frames))]))))
-(def: (pop-frame [module-reference definition-reference] source)
+(def: (pop_frame [module_reference definition_reference] source)
(-> Name (List [Text Module]) (List [Text Module]))
- (!push source module-reference
- (|> head (update@ #.definitions (pop-frame-definition definition-reference)))))
+ (!push source module_reference
+ (|> head (update@ #.definitions (pop_frame_definition definition_reference)))))
(syntax: (pop!)
(function (_ compiler)
(#.Right [(update@ #.modules
- (..pop-frame (name-of ..frames))
+ (..pop_frame (name_of ..frames))
compiler)
(list)])))
(def: cast
(Parser [(Maybe Text) Code])
- (<>.either (<>.and (<>.maybe <c>.local-identifier) <c>.any)
+ (<>.either (<>.and (<>.maybe <c>.local_identifier) <c>.any)
(<>.and (<>\wrap #.None) <c>.any)))
(template [<name> <from> <to>]
[(syntax: #export (<name> {[frame value] ..cast})
(do meta.monad
- [[name type-vars abstraction representation] (peek! frame)]
- (wrap (list (` ((~! :cast) [(~+ type-vars)] (~ <from>) (~ <to>)
+ [[name type_vars abstraction representation] (peek! frame)]
+ (wrap (list (` ((~! :cast) [(~+ type_vars)] (~ <from>) (~ <to>)
(~ value)))))))]
[:abstraction representation abstraction]
[:representation abstraction representation]
)
-(def: abstraction-type-name
+(def: abstraction_type_name
(-> Name Text)
(|>> name\encode
($_ text\compose
- (name\encode (name-of #..Abstraction))
+ (name\encode (name_of #..Abstraction))
" ")))
-(def: representation-definition-name
+(def: representation_definition_name
(-> Text Text)
(|>> ($_ text\compose
- (name\encode (name-of #Representation))
+ (name\encode (name_of #Representation))
" ")))
(def: declaration
(Parser [Text (List Text)])
- (<>.either (<c>.form (<>.and <c>.local-identifier (<>.some <c>.local-identifier)))
- (<>.and <c>.local-identifier (\ <>.monad wrap (list)))))
+ (<>.either (<c>.form (<>.and <c>.local_identifier (<>.some <c>.local_identifier)))
+ (<>.and <c>.local_identifier (\ <>.monad wrap (list)))))
## TODO: Make sure the generated code always gets optimized away.
## (This applies to uses of ":abstraction" and ":representation")
(syntax: #export (abstract:
{export |export|.parser}
- {[name type-vars] declaration}
- representation-type
- {annotations (<>.default cs.empty-annotations csr.annotations)}
+ {[name type_vars] declaration}
+ representation_type
+ {annotations (<>.default cs.empty_annotations csr.annotations)}
{primitives (<>.some <c>.any)})
(do meta.monad
- [current-module meta.current-module-name
- #let [type-varsC (list\map code.local-identifier type-vars)
- abstraction-declaration (` ((~ (code.local-identifier name)) (~+ type-varsC)))
- representation-declaration (` ((~ (code.local-identifier (representation-definition-name name)))
- (~+ type-varsC)))]
+ [current_module meta.current_module_name
+ #let [type_varsC (list\map code.local_identifier type_vars)
+ abstraction_declaration (` ((~ (code.local_identifier name)) (~+ type_varsC)))
+ representation_declaration (` ((~ (code.local_identifier (representation_definition_name name)))
+ (~+ type_varsC)))]
_ (..push! [name
- type-varsC
- abstraction-declaration
- representation-declaration])]
- (wrap (list& (` (type: (~+ (|export|.write export)) (~ abstraction-declaration)
+ type_varsC
+ abstraction_declaration
+ representation_declaration])]
+ (wrap (list& (` (type: (~+ (|export|.write export)) (~ abstraction_declaration)
(~ (csw.annotations annotations))
- (primitive (~ (code.text (abstraction-type-name [current-module name])))
- [(~+ type-varsC)])))
- (` (type: (~ representation-declaration)
- (~ representation-type)))
+ (primitive (~ (code.text (abstraction_type_name [current_module name])))
+ [(~+ type_varsC)])))
+ (` (type: (~ representation_declaration)
+ (~ representation_type)))
($_ list\compose
primitives
(list (` ((~! ..pop!)))))))))
@@ -235,10 +235,10 @@
(syntax: #export (:transmutation value)
(wrap (list (` (..:abstraction (..:representation (~ value)))))))
-(syntax: #export (^:representation {name (<c>.form <c>.local-identifier)}
+(syntax: #export (^:representation {name (<c>.form <c>.local_identifier)}
body
{branches (<>.some <c>.any)})
- (let [g!var (code.local-identifier name)]
+ (let [g!var (code.local_identifier name)]
(wrap (list& g!var
(` (.let [(~ g!var) (..:representation (~ g!var))]
(~ body)))
diff --git a/stdlib/source/lux/type/check.lux b/stdlib/source/lux/type/check.lux
index 13a1e1381..d8d358010 100644
--- a/stdlib/source/lux/type/check.lux
+++ b/stdlib/source/lux/type/check.lux
@@ -24,26 +24,26 @@
(template: (!text\= reference subject)
("lux text =" reference subject))
-(exception: #export (unknown-type-var {id Nat})
+(exception: #export (unknown_type_var {id Nat})
(exception.report
["ID" (n\encode id)]))
-(exception: #export (unbound-type-var {id Nat})
+(exception: #export (unbound_type_var {id Nat})
(exception.report
["ID" (n\encode id)]))
-(exception: #export (invalid-type-application {funcT Type} {argT Type})
+(exception: #export (invalid_type_application {funcT Type} {argT Type})
(exception.report
["Type function" (//.format funcT)]
["Type argument" (//.format argT)]))
-(exception: #export (cannot-rebind-var {id Nat} {type Type} {bound Type})
+(exception: #export (cannot_rebind_var {id Nat} {type Type} {bound Type})
(exception.report
["Var" (n\encode id)]
["Wanted Type" (//.format type)]
["Current Type" (//.format bound)]))
-(exception: #export (type-check-failed {expected Type} {actual Type})
+(exception: #export (type_check_failed {expected Type} {actual Type})
(exception.report
["Expected" (//.format expected)]
["Actual" (//.format actual)]))
@@ -53,12 +53,12 @@
(type: #export Assumption [Type Type])
(type: #export (Check a)
- (-> Type-Context (Try [Type-Context a])))
+ (-> Type_Context (Try [Type_Context a])))
(type: #export (Checker a)
(-> (List Assumption) a a (Check (List Assumption))))
-(type: #export Type-Vars
+(type: #export Type_Vars
(List [Var (Maybe Type)]))
(structure: #export functor
@@ -122,37 +122,37 @@
(open: "check\." ..monad)
(def: (var::new id plist)
- (-> Var Type-Vars Type-Vars)
+ (-> Var Type_Vars Type_Vars)
(#.Cons [id #.None] plist))
(def: (var::get id plist)
- (-> Var Type-Vars (Maybe (Maybe Type)))
+ (-> Var Type_Vars (Maybe (Maybe Type)))
(case plist
- (#.Cons [var-id var-type]
+ (#.Cons [var_id var_type]
plist')
- (if (!n/= id var-id)
- (#.Some var-type)
+ (if (!n/= id var_id)
+ (#.Some var_type)
(var::get id plist'))
#.Nil
#.None))
(def: (var::put id value plist)
- (-> Var (Maybe Type) Type-Vars Type-Vars)
+ (-> Var (Maybe Type) Type_Vars Type_Vars)
(case plist
#.Nil
(list [id value])
- (#.Cons [var-id var-type]
+ (#.Cons [var_id var_type]
plist')
- (if (!n/= id var-id)
- (#.Cons [var-id value]
+ (if (!n/= id var_id)
+ (#.Cons [var_id value]
plist')
- (#.Cons [var-id var-type]
+ (#.Cons [var_id var_type]
(var::put id value plist')))))
(def: #export (run context proc)
- (All [a] (-> Type-Context (Check a) (Try a)))
+ (All [a] (-> Type_Context (Check a) (Try a)))
(case (proc context)
(#try.Success [context' output])
(#try.Success output)
@@ -180,15 +180,15 @@
{#.doc "A producer of existential types."}
(Check [Nat Type])
(function (_ context)
- (let [id (get@ #.ex-counter context)]
- (#try.Success [(update@ #.ex-counter inc context)
+ (let [id (get@ #.ex_counter context)]
+ (#try.Success [(update@ #.ex_counter inc context)
[id (#.Ex id)]]))))
(template [<name> <outputT> <fail> <succeed>]
[(def: #export (<name> id)
(-> Var (Check <outputT>))
(function (_ context)
- (case (|> context (get@ #.var-bindings) (var::get id))
+ (case (|> context (get@ #.var_bindings) (var::get id))
(^or (#.Some (#.Some (#.Var _)))
(#.Some #.None))
(#try.Success [context <fail>])
@@ -197,7 +197,7 @@
(#try.Success [context <succeed>])
#.None
- (exception.throw unknown-type-var id))))]
+ (exception.throw ..unknown_type_var id))))]
[bound? Bit false true]
[read (Maybe Type) #.None (#.Some bound)]
@@ -212,72 +212,72 @@
(wrap type)
#.None
- (..throw unbound-type-var id))))
+ (..throw ..unbound_type_var id))))
(def: (peek id)
(-> Var (Check Type))
(function (_ context)
- (case (|> context (get@ #.var-bindings) (var::get id))
+ (case (|> context (get@ #.var_bindings) (var::get id))
(#.Some (#.Some bound))
(#try.Success [context bound])
(#.Some _)
- (exception.throw unbound-type-var id)
+ (exception.throw ..unbound_type_var id)
_
- (exception.throw unknown-type-var id))))
+ (exception.throw ..unknown_type_var id))))
(def: #export (bind type id)
(-> Type Var (Check Any))
(function (_ context)
- (case (|> context (get@ #.var-bindings) (var::get id))
+ (case (|> context (get@ #.var_bindings) (var::get id))
(#.Some #.None)
- (#try.Success [(update@ #.var-bindings (var::put id (#.Some type)) context)
+ (#try.Success [(update@ #.var_bindings (var::put id (#.Some type)) context)
[]])
(#.Some (#.Some bound))
- (exception.throw cannot-rebind-var [id type bound])
+ (exception.throw ..cannot_rebind_var [id type bound])
_
- (exception.throw unknown-type-var id))))
+ (exception.throw ..unknown_type_var id))))
(def: (update type id)
(-> Type Var (Check Any))
(function (_ context)
- (case (|> context (get@ #.var-bindings) (var::get id))
+ (case (|> context (get@ #.var_bindings) (var::get id))
(#.Some _)
- (#try.Success [(update@ #.var-bindings (var::put id (#.Some type)) context)
+ (#try.Success [(update@ #.var_bindings (var::put id (#.Some type)) context)
[]])
_
- (exception.throw unknown-type-var id))))
+ (exception.throw ..unknown_type_var id))))
(def: #export var
(Check [Var Type])
(function (_ context)
- (let [id (get@ #.var-counter context)]
+ (let [id (get@ #.var_counter context)]
(#try.Success [(|> context
- (update@ #.var-counter inc)
- (update@ #.var-bindings (var::new id)))
+ (update@ #.var_counter inc)
+ (update@ #.var_bindings (var::new id)))
[id (#.Var id)]]))))
-(def: (apply-type! funcT argT)
+(def: (apply_type! funcT argT)
(-> Type Type (Check Type))
(case funcT
- (#.Var func-id)
+ (#.Var func_id)
(do ..monad
- [?funcT' (read func-id)]
+ [?funcT' (read func_id)]
(case ?funcT'
(#.Some funcT')
- (apply-type! funcT' argT)
+ (apply_type! funcT' argT)
_
- (throw ..invalid-type-application [funcT argT])))
+ (throw ..invalid_type_application [funcT argT])))
(#.Apply argT' funcT')
(do ..monad
- [funcT'' (apply-type! funcT' argT')]
- (apply-type! funcT'' argT))
+ [funcT'' (apply_type! funcT' argT')]
+ (apply_type! funcT'' argT))
_
(case (//.apply (list argT) funcT)
@@ -285,19 +285,19 @@
(check\wrap output)
_
- (throw ..invalid-type-application [funcT argT]))))
+ (throw ..invalid_type_application [funcT argT]))))
(type: #export Ring (Set Var))
-(def: empty-ring Ring (set.new n.hash))
+(def: empty_ring Ring (set.new n.hash))
## TODO: Optimize this by not using sets anymore.
(def: #export (ring start)
(-> Var (Check Ring))
(function (_ context)
(loop [current start
- output (set.add start empty-ring)]
- (case (|> context (get@ #.var-bindings) (var::get current))
+ output (set.add start empty_ring)]
+ (case (|> context (get@ #.var_bindings) (var::get current))
(#.Some (#.Some type))
(case type
(#.Var post)
@@ -306,19 +306,19 @@
(recur post (set.add post output)))
_
- (#try.Success [context empty-ring]))
+ (#try.Success [context empty_ring]))
(#.Some #.None)
(#try.Success [context output])
#.None
- (exception.throw unknown-type-var current)))))
+ (exception.throw ..unknown_type_var current)))))
-(def: #export fresh-context
- Type-Context
- {#.var-counter 0
- #.ex-counter 0
- #.var-bindings (list)})
+(def: #export fresh_context
+ Type_Context
+ {#.var_counter 0
+ #.ex_counter 0
+ #.var_bindings (list)})
(def: (attempt op)
(All [a] (-> (Check a) (Check (Maybe a))))
@@ -351,8 +351,8 @@
(-> Assumption (List Assumption) (List Assumption))
(#.Cons assumption assumptions))
-## TODO: "if-bind" can be optimized...
-(def: (if-bind id type then else)
+## TODO: "if_bind" can be optimized...
+(def: (if_bind id type then else)
(All [a]
(-> Var Type (Check a) (-> Type (Check a))
(Check a)))
@@ -363,28 +363,28 @@
(do {! ..monad}
[ring (..ring id)
_ (assert "" (n.> 1 (set.size ring)))
- _ (monad.map ! (update type) (set.to-list ring))]
+ _ (monad.map ! (update type) (set.to_list ring))]
then)
(do ..monad
[?bound (read id)]
(else (maybe.default (#.Var id) ?bound)))))
-## TODO: "link-2" can be optimized...
-(def: (link-2 left right)
+## TODO: "link_2" can be optimized...
+(def: (link_2 left right)
(-> Var Var (Check Any))
(do ..monad
[_ (..bind (#.Var right) left)]
(..bind (#.Var left) right)))
-## TODO: "link-3" can be optimized...
-(def: (link-3 interpose to from)
+## TODO: "link_3" can be optimized...
+(def: (link_3 interpose to from)
(-> Var Var Var (Check Any))
(do ..monad
[_ (update (#.Var interpose) from)]
(update (#.Var to) interpose)))
-## TODO: "check-vars" can be optimized...
-(def: (check-vars check' assumptions idE idA)
+## TODO: "check_vars" can be optimized...
+(def: (check_vars check' assumptions idE idA)
(-> (Checker Type) (Checker Var))
(if (!n/= idE idA)
(check\wrap assumptions)
@@ -395,7 +395,7 @@
## Link the 2 variables circularly
[#.None #.None]
(do !
- [_ (link-2 idE idA)]
+ [_ (link_2 idE idA)]
(wrap assumptions))
## Interpose new variable between 2 existing links
@@ -403,7 +403,7 @@
(case etype
(#.Var targetE)
(do !
- [_ (link-3 idA targetE idE)]
+ [_ (link_3 idA targetE idE)]
(wrap assumptions))
_
@@ -414,7 +414,7 @@
(case atype
(#.Var targetA)
(do !
- [_ (link-3 idE targetA idA)]
+ [_ (link_3 idE targetA idA)]
(wrap assumptions))
_
@@ -432,17 +432,17 @@
(do !
[_ (monad.fold ! (function (_ interpose to)
(do !
- [_ (link-3 interpose to idE)]
+ [_ (link_3 interpose to idE)]
(wrap interpose)))
targetE
- (set.to-list ringA))]
+ (set.to_list ringA))]
(wrap assumptions))))
(^template [<pattern> <id> <type>]
[<pattern>
(do !
[ring (..ring <id>)
- _ (monad.map ! (update <type>) (set.to-list ring))]
+ _ (monad.map ! (update <type>) (set.to_list ring))]
(wrap assumptions))])
([[(#.Var _) _] idE atype]
[[_ (#.Var _)] idA etype])
@@ -450,87 +450,87 @@
_
(check' assumptions etype atype))))))
-## TODO: "check-apply" can be optimized...
-(def: (check-apply check' assumptions expected actual)
+## TODO: "check_apply" can be optimized...
+(def: (check_apply check' assumptions expected actual)
(-> (Checker Type) (Checker [Type Type]))
- (let [[expected-input expected-function] expected
- [actual-input actual-function] actual]
- (case [expected-function actual-function]
+ (let [[expected_input expected_function] expected
+ [actual_input actual_function] actual]
+ (case [expected_function actual_function]
[(#.Ex exE) (#.Ex exA)]
(if (!n/= exE exA)
- (check' assumptions expected-input actual-input)
+ (check' assumptions expected_input actual_input)
(fail ""))
[(#.UnivQ _ _) (#.Ex _)]
(do ..monad
- [expected' (apply-type! expected-function expected-input)]
+ [expected' (apply_type! expected_function expected_input)]
(check' assumptions expected' (#.Apply actual)))
[(#.Ex _) (#.UnivQ _ _)]
(do ..monad
- [actual' (apply-type! actual-function actual-input)]
+ [actual' (apply_type! actual_function actual_input)]
(check' assumptions (#.Apply expected) actual'))
- [(#.Apply [expected-input' expected-function']) (#.Ex _)]
+ [(#.Apply [expected_input' expected_function']) (#.Ex _)]
(do ..monad
- [expected-function'' (apply-type! expected-function' expected-input')]
- (check' assumptions (#.Apply [expected-input expected-function'']) (#.Apply actual)))
+ [expected_function'' (apply_type! expected_function' expected_input')]
+ (check' assumptions (#.Apply [expected_input expected_function'']) (#.Apply actual)))
- [(#.Ex _) (#.Apply [actual-input' actual-function'])]
+ [(#.Ex _) (#.Apply [actual_input' actual_function'])]
(do ..monad
- [actual-function'' (apply-type! actual-function' actual-input')]
- (check' assumptions (#.Apply expected) (#.Apply [actual-input actual-function''])))
+ [actual_function'' (apply_type! actual_function' actual_input')]
+ (check' assumptions (#.Apply expected) (#.Apply [actual_input actual_function''])))
(^or [(#.Ex _) _] [_ (#.Ex _)])
(do ..monad
- [assumptions (check' assumptions expected-function actual-function)]
- (check' assumptions expected-input actual-input))
+ [assumptions (check' assumptions expected_function actual_function)]
+ (check' assumptions expected_input actual_input))
[(#.Var id) _]
(function (_ context)
(case ((do ..monad
- [expected-function' (read! id)]
- (check' assumptions (#.Apply expected-input expected-function') (#.Apply actual)))
+ [expected_function' (read! id)]
+ (check' assumptions (#.Apply expected_input expected_function') (#.Apply actual)))
context)
(#try.Success output)
(#try.Success output)
(#try.Failure _)
- (case actual-function
+ (case actual_function
(#.UnivQ _ _)
((do ..monad
- [actual' (apply-type! actual-function actual-input)]
+ [actual' (apply_type! actual_function actual_input)]
(check' assumptions (#.Apply expected) actual'))
context)
(#.Ex exA)
((do ..monad
- [assumptions (check' assumptions expected-function actual-function)]
- (check' assumptions expected-input actual-input))
+ [assumptions (check' assumptions expected_function actual_function)]
+ (check' assumptions expected_input actual_input))
context)
_
((do ..monad
- [assumptions (check' assumptions expected-function actual-function)
- expected' (apply-type! actual-function expected-input)
- actual' (apply-type! actual-function actual-input)]
+ [assumptions (check' assumptions expected_function actual_function)
+ expected' (apply_type! actual_function expected_input)
+ actual' (apply_type! actual_function actual_input)]
(check' assumptions expected' actual'))
context))))
[_ (#.Var id)]
(function (_ context)
(case ((do ..monad
- [actual-function' (read! id)]
- (check' assumptions (#.Apply expected) (#.Apply actual-input actual-function')))
+ [actual_function' (read! id)]
+ (check' assumptions (#.Apply expected) (#.Apply actual_input actual_function')))
context)
(#try.Success output)
(#try.Success output)
_
((do ..monad
- [assumptions (check' assumptions expected-function actual-function)
- expected' (apply-type! expected-function expected-input)
- actual' (apply-type! expected-function actual-input)]
+ [assumptions (check' assumptions expected_function actual_function)
+ expected' (apply_type! expected_function expected_input)
+ actual' (apply_type! expected_function actual_input)]
(check' assumptions expected' actual'))
context)))
@@ -547,42 +547,42 @@
(Checker Type)
(if (is? expected actual)
(check\wrap assumptions)
- (with type-check-failed [expected actual]
+ (with type_check_failed [expected actual]
(case [expected actual]
[(#.Var idE) (#.Var idA)]
- (check-vars check' assumptions idE idA)
+ (check_vars check' assumptions idE idA)
[(#.Var id) _]
- (if-bind id actual
+ (if_bind id actual
(check\wrap assumptions)
(function (_ bound)
(check' assumptions bound actual)))
[_ (#.Var id)]
- (if-bind id expected
+ (if_bind id expected
(check\wrap assumptions)
(function (_ bound)
(check' assumptions expected bound)))
(^template [<fE> <fA>]
[[(#.Apply aE <fE>) (#.Apply aA <fA>)]
- (check-apply check' assumptions [aE <fE>] [aA <fA>])])
+ (check_apply check' assumptions [aE <fE>] [aA <fA>])])
([F1 (#.Ex ex)]
[(#.Ex exE) fA]
[fE (#.Var idA)]
[(#.Var idE) fA])
[(#.Apply A F) _]
- (let [new-assumption [expected actual]]
- (if (assumed? new-assumption assumptions)
+ (let [new_assumption [expected actual]]
+ (if (assumed? new_assumption assumptions)
(check\wrap assumptions)
(do ..monad
- [expected' (apply-type! F A)]
- (check' (assume! new-assumption assumptions) expected' actual))))
+ [expected' (apply_type! F A)]
+ (check' (assume! new_assumption assumptions) expected' actual))))
[_ (#.Apply A F)]
(do ..monad
- [actual' (apply-type! F A)]
+ [actual' (apply_type! F A)]
(check' assumptions expected actual'))
## TODO: Refactor-away as cold-code
@@ -590,7 +590,7 @@
[[(<tag> _) _]
(do ..monad
[[_ paramT] <instancer>
- expected' (apply-type! expected paramT)]
+ expected' (apply_type! expected paramT)]
(check' assumptions expected' actual))])
([#.UnivQ ..existential]
[#.ExQ ..var])
@@ -600,24 +600,24 @@
[[_ (<tag> _)]
(do ..monad
[[_ paramT] <instancer>
- actual' (apply-type! actual paramT)]
+ actual' (apply_type! actual paramT)]
(check' assumptions expected actual'))])
([#.UnivQ ..var]
[#.ExQ ..existential])
- [(#.Primitive e-name e-params) (#.Primitive a-name a-params)]
- (if (!text\= e-name a-name)
+ [(#.Primitive e_name e_params) (#.Primitive a_name a_params)]
+ (if (!text\= e_name a_name)
(loop [assumptions assumptions
- e-params e-params
- a-params a-params]
- (case [e-params a-params]
+ e_params e_params
+ a_params a_params]
+ (case [e_params a_params]
[#.Nil #.Nil]
(check\wrap assumptions)
- [(#.Cons e-head e-tail) (#.Cons a-head a-tail)]
+ [(#.Cons e_head e_tail) (#.Cons a_head a_tail)]
(do ..monad
- [assumptions' (check' assumptions e-head a-head)]
- (recur assumptions' e-tail a-tail))
+ [assumptions' (check' assumptions e_head a_head)]
+ (recur assumptions' e_tail a_tail))
_
(fail "")))
@@ -658,7 +658,7 @@
(def: #export (checks? expected actual)
{#.doc "A simple type-checking function that just returns a yes/no answer."}
(-> Type Type Bit)
- (case (run fresh-context (check' (list) expected actual))
+ (case (run fresh_context (check' (list) expected actual))
(#try.Failure _)
false
@@ -666,7 +666,7 @@
true))
(def: #export context
- (Check Type-Context)
+ (Check Type_Context)
(function (_ context)
(#try.Success [context context])))
diff --git a/stdlib/source/lux/type/dynamic.lux b/stdlib/source/lux/type/dynamic.lux
index 9d9027e72..21a0d6cf3 100644
--- a/stdlib/source/lux/type/dynamic.lux
+++ b/stdlib/source/lux/type/dynamic.lux
@@ -7,13 +7,13 @@
[data
[text
["%" format (#+ format)]]]
- [meta (#+ with-gensyms)]
+ [meta (#+ with_gensyms)]
[macro
["." syntax (#+ syntax:)]]
["." type
abstract]])
-(exception: #export (wrong-type {expected Type} {actual Type})
+(exception: #export (wrong_type {expected Type} {actual Type})
(exception.report
["Expected" (%.type expected)]
["Actual" (%.type actual)]))
@@ -29,20 +29,20 @@
(syntax: #export (:dynamic value)
{#.doc (doc (: Dynamic
(:dynamic 123)))}
- (with-gensyms [g!value]
+ (with_gensyms [g!value]
(wrap (list (` (let [(~ g!value) (~ value)]
((~! ..abstraction) [(:of (~ g!value)) (~ g!value)])))))))
(syntax: #export (:check type value)
{#.doc (doc (: (try.Try Nat)
(:check Nat (:dynamic 123))))}
- (with-gensyms [g!type g!value]
+ (with_gensyms [g!type g!value]
(wrap (list (` (let [[(~ g!type) (~ g!value)] ((~! ..representation) (~ value))]
(: ((~! try.Try) (~ type))
(if (\ (~! type.equivalence) (~' =)
(.type (~ type)) (~ g!type))
(#try.Success (:coerce (~ type) (~ g!value)))
- ((~! exception.throw) ..wrong-type [(.type (~ type)) (~ g!type)])))))))))
+ ((~! exception.throw) ..wrong_type [(.type (~ type)) (~ g!type)])))))))))
(def: #export (print value)
(-> Dynamic (Try Text))
diff --git a/stdlib/source/lux/type/implicit.lux b/stdlib/source/lux/type/implicit.lux
index 69890cd3e..f24a80599 100644
--- a/stdlib/source/lux/type/implicit.lux
+++ b/stdlib/source/lux/type/implicit.lux
@@ -26,14 +26,14 @@
["." type
["." check (#+ Check)]]])
-(def: (find-type-var id env)
- (-> Nat Type-Context (Meta Type))
+(def: (find_type_var id env)
+ (-> Nat Type_Context (Meta Type))
(case (list.find (|>> product.left (n.= id))
- (get@ #.var-bindings env))
+ (get@ #.var_bindings env))
(#.Some [_ (#.Some type)])
(case type
(#.Var id')
- (find-type-var id' env)
+ (find_type_var id' env)
_
(\ meta.monad wrap type))
@@ -45,57 +45,57 @@
(meta.fail (format "Unknown type-var " (%.nat id)))
))
-(def: (resolve-type var-name)
+(def: (resolve_type var_name)
(-> Name (Meta Type))
(do meta.monad
- [raw-type (meta.find-type var-name)
- compiler meta.get-compiler]
- (case raw-type
+ [raw_type (meta.find_type var_name)
+ compiler meta.get_compiler]
+ (case raw_type
(#.Var id)
- (find-type-var id (get@ #.type-context compiler))
+ (find_type_var id (get@ #.type_context compiler))
_
- (wrap raw-type))))
+ (wrap raw_type))))
-(def: (find-member-type idx sig-type)
+(def: (find_member_type idx sig_type)
(-> Nat Type (Check Type))
- (case sig-type
- (#.Named _ sig-type')
- (find-member-type idx sig-type')
+ (case sig_type
+ (#.Named _ sig_type')
+ (find_member_type idx sig_type')
(#.Apply arg func)
(case (type.apply (list arg) func)
#.None
(check.fail (format "Cannot apply type " (%.type func) " to type " (%.type arg)))
- (#.Some sig-type')
- (find-member-type idx sig-type'))
+ (#.Some sig_type')
+ (find_member_type idx sig_type'))
(#.Product left right)
(if (n.= 0 idx)
(\ check.monad wrap left)
- (find-member-type (dec idx) right))
+ (find_member_type (dec idx) right))
_
(if (n.= 0 idx)
- (\ check.monad wrap sig-type)
- (check.fail (format "Cannot find member type " (%.nat idx) " for " (%.type sig-type))))))
+ (\ check.monad wrap sig_type)
+ (check.fail (format "Cannot find member type " (%.nat idx) " for " (%.type sig_type))))))
-(def: (find-member-name member)
+(def: (find_member_name member)
(-> Name (Meta Name))
(case member
- ["" simple-name]
+ ["" simple_name]
(meta.either (do meta.monad
[member (meta.normalize member)
- _ (meta.resolve-tag member)]
+ _ (meta.resolve_tag member)]
(wrap member))
(do {! meta.monad}
- [this-module-name meta.current-module-name
- imp-mods (meta.imported-modules this-module-name)
- tag-lists (monad.map ! meta.tag-lists imp-mods)
- #let [tag-lists (|> tag-lists list\join (list\map product.left) list\join)
- candidates (list.filter (|>> product.right (text\= simple-name))
- tag-lists)]]
+ [this_module_name meta.current_module_name
+ imp_mods (meta.imported_modules this_module_name)
+ tag_lists (monad.map ! meta.tag_lists imp_mods)
+ #let [tag_lists (|> tag_lists list\join (list\map product.left) list\join)
+ candidates (list.filter (|>> product.right (text\= simple_name))
+ tag_lists)]]
(case candidates
#.Nil
(meta.fail (format "Unknown tag: " (%.name member)))
@@ -109,64 +109,64 @@
_
(\ meta.monad wrap member)))
-(def: (resolve-member member)
+(def: (resolve_member member)
(-> Name (Meta [Nat Type]))
(do meta.monad
- [member (find-member-name member)
- [idx tag-list sig-type] (meta.resolve-tag member)]
- (wrap [idx sig-type])))
+ [member (find_member_name member)
+ [idx tag_list sig_type] (meta.resolve_tag member)]
+ (wrap [idx sig_type])))
-(def: (prepare-definitions source-module target-module constants)
+(def: (prepare_definitions source_module target_module constants)
(-> Text Text (List [Text Definition]) (List [Name Type]))
(do list.monad
- [[name [exported? def-type def-anns def-value]] constants]
- (if (and (annotation.structure? def-anns)
- (or (text\= target-module source-module)
+ [[name [exported? def_type def_anns def_value]] constants]
+ (if (and (annotation.structure? def_anns)
+ (or (text\= target_module source_module)
exported?))
- (list [[source-module name] def-type])
+ (list [[source_module name] def_type])
(list))))
-(def: local-env
+(def: local_env
(Meta (List [Name Type]))
(do meta.monad
- [local-batches meta.locals
- #let [total-locals (list\fold (function (_ [name type] table)
- (try.default table (dict.try-put name type table)))
+ [local_batches meta.locals
+ #let [total_locals (list\fold (function (_ [name type] table)
+ (try.default table (dict.try_put name type table)))
(: (Dictionary Text Type)
(dict.new text.hash))
- (list\join local-batches))]]
- (wrap (|> total-locals
+ (list\join local_batches))]]
+ (wrap (|> total_locals
dict.entries
(list\map (function (_ [name type]) [["" name] type]))))))
-(def: local-structs
+(def: local_structs
(Meta (List [Name Type]))
(do {! meta.monad}
- [this-module-name meta.current-module-name]
- (\ ! map (prepare-definitions this-module-name this-module-name)
- (meta.definitions this-module-name))))
+ [this_module_name meta.current_module_name]
+ (\ ! map (prepare_definitions this_module_name this_module_name)
+ (meta.definitions this_module_name))))
-(def: import-structs
+(def: import_structs
(Meta (List [Name Type]))
(do {! meta.monad}
- [this-module-name meta.current-module-name
- imp-mods (meta.imported-modules this-module-name)
- export-batches (monad.map ! (function (_ imp-mod)
- (\ ! map (prepare-definitions imp-mod this-module-name)
- (meta.definitions imp-mod)))
- imp-mods)]
- (wrap (list\join export-batches))))
-
-(def: (apply-function-type func arg)
+ [this_module_name meta.current_module_name
+ imp_mods (meta.imported_modules this_module_name)
+ export_batches (monad.map ! (function (_ imp_mod)
+ (\ ! map (prepare_definitions imp_mod this_module_name)
+ (meta.definitions imp_mod)))
+ imp_mods)]
+ (wrap (list\join export_batches))))
+
+(def: (apply_function_type func arg)
(-> Type Type (Check Type))
(case func
(#.Named _ func')
- (apply-function-type func' arg)
+ (apply_function_type func' arg)
(#.UnivQ _)
(do check.monad
[[id var] check.var]
- (apply-function-type (maybe.assume (type.apply (list var) func))
+ (apply_function_type (maybe.assume (type.apply (list var) func))
arg))
(#.Function input output)
@@ -177,46 +177,46 @@
_
(check.fail (format "Invalid function type: " (%.type func)))))
-(def: (concrete-type type)
+(def: (concrete_type type)
(-> Type (Check [(List Nat) Type]))
(case type
(#.UnivQ _)
(do check.monad
[[id var] check.var
- [ids final-output] (concrete-type (maybe.assume (type.apply (list var) type)))]
+ [ids final_output] (concrete_type (maybe.assume (type.apply (list var) type)))]
(wrap [(#.Cons id ids)
- final-output]))
+ final_output]))
_
(\ check.monad wrap [(list) type])))
-(def: (check-apply member-type input-types output-type)
+(def: (check_apply member_type input_types output_type)
(-> Type (List Type) Type (Check []))
(do check.monad
- [member-type' (monad.fold check.monad
+ [member_type' (monad.fold check.monad
(function (_ input member)
- (apply-function-type member input))
- member-type
- input-types)]
- (check.check output-type member-type')))
+ (apply_function_type member input))
+ member_type
+ input_types)]
+ (check.check output_type member_type')))
(type: #rec Instance
{#constructor Name
#dependencies (List Instance)})
-(def: (test-provision provision context dep alts)
- (-> (-> Lux Type-Context Type (Check Instance))
- Type-Context Type (List [Name Type])
+(def: (test_provision provision context dep alts)
+ (-> (-> Lux Type_Context Type (Check Instance))
+ Type_Context Type (List [Name Type])
(Meta (List Instance)))
(do meta.monad
- [compiler meta.get-compiler]
+ [compiler meta.get_compiler]
(case (|> alts
- (list\map (function (_ [alt-name alt-type])
+ (list\map (function (_ [alt_name alt_type])
(case (check.run context
(do {! check.monad}
- [[tvars alt-type] (concrete-type alt-type)
- #let [[deps alt-type] (type.flatten-function alt-type)]
- _ (check.check dep alt-type)
+ [[tvars alt_type] (concrete_type alt_type)
+ #let [[deps alt_type] (type.flatten_function alt_type)]
+ _ (check.check dep alt_type)
context' check.context
=deps (monad.map ! (provision compiler context') deps)]
(wrap =deps)))
@@ -224,7 +224,7 @@
(list)
(#.Right =deps)
- (list [alt-name =deps]))))
+ (list [alt_name =deps]))))
list\join)
#.Nil
(meta.fail (format "No candidates for provisioning: " (%.type dep)))
@@ -233,12 +233,12 @@
(wrap found))))
(def: (provision compiler context dep)
- (-> Lux Type-Context Type (Check Instance))
+ (-> Lux Type_Context Type (Check Instance))
(case (meta.run compiler
($_ meta.either
- (do meta.monad [alts ..local-env] (..test-provision provision context dep alts))
- (do meta.monad [alts ..local-structs] (..test-provision provision context dep alts))
- (do meta.monad [alts ..import-structs] (..test-provision provision context dep alts))))
+ (do meta.monad [alts ..local_env] (..test_provision provision context dep alts))
+ (do meta.monad [alts ..local_structs] (..test_provision provision context dep alts))
+ (do meta.monad [alts ..import_structs] (..test_provision provision context dep alts))))
(#.Left error)
(check.fail error)
@@ -254,20 +254,20 @@
(check.fail (format "Too many candidates for provisioning: " (%.type dep) " --- " (%.list (|>> product.left %.name) candidates))))
))
-(def: (test-alternatives sig-type member-idx input-types output-type alts)
+(def: (test_alternatives sig_type member_idx input_types output_type alts)
(-> Type Nat (List Type) Type (List [Name Type]) (Meta (List Instance)))
(do meta.monad
- [compiler meta.get-compiler
- context meta.type-context]
+ [compiler meta.get_compiler
+ context meta.type_context]
(case (|> alts
- (list\map (function (_ [alt-name alt-type])
+ (list\map (function (_ [alt_name alt_type])
(case (check.run context
(do {! check.monad}
- [[tvars alt-type] (concrete-type alt-type)
- #let [[deps alt-type] (type.flatten-function alt-type)]
- _ (check.check alt-type sig-type)
- member-type (find-member-type member-idx alt-type)
- _ (check-apply member-type input-types output-type)
+ [[tvars alt_type] (concrete_type alt_type)
+ #let [[deps alt_type] (type.flatten_function alt_type)]
+ _ (check.check alt_type sig_type)
+ member_type (find_member_type member_idx alt_type)
+ _ (check_apply member_type input_types output_type)
context' check.context
=deps (monad.map ! (provision compiler context') deps)]
(wrap =deps)))
@@ -275,21 +275,21 @@
(list)
(#.Right =deps)
- (list [alt-name =deps]))))
+ (list [alt_name =deps]))))
list\join)
#.Nil
- (meta.fail (format "No alternatives for " (%.type (type.function input-types output-type))))
+ (meta.fail (format "No alternatives for " (%.type (type.function input_types output_type))))
found
(wrap found))))
-(def: (find-alternatives sig-type member-idx input-types output-type)
+(def: (find_alternatives sig_type member_idx input_types output_type)
(-> Type Nat (List Type) Type (Meta (List Instance)))
- (let [test (test-alternatives sig-type member-idx input-types output-type)]
+ (let [test (test_alternatives sig_type member_idx input_types output_type)]
($_ meta.either
- (do meta.monad [alts local-env] (test alts))
- (do meta.monad [alts local-structs] (test alts))
- (do meta.monad [alts import-structs] (test alts)))))
+ (do meta.monad [alts local_env] (test alts))
+ (do meta.monad [alts local_structs] (test alts))
+ (do meta.monad [alts import_structs] (test alts)))))
(def: (var? input)
(-> Code Bit)
@@ -300,7 +300,7 @@
_
#0))
-(def: (join-pair [l r])
+(def: (join_pair [l r])
(All [a] (-> [a a] (List a)))
(list l r))
@@ -343,34 +343,34 @@
(case args
(#.Left [args _])
(do {! meta.monad}
- [[member-idx sig-type] (resolve-member member)
- input-types (monad.map ! resolve-type args)
- output-type meta.expected-type
- chosen-ones (find-alternatives sig-type member-idx input-types output-type)]
- (case chosen-ones
+ [[member_idx sig_type] (resolve_member member)
+ input_types (monad.map ! resolve_type args)
+ output_type meta.expected_type
+ chosen_ones (find_alternatives sig_type member_idx input_types output_type)]
+ (case chosen_ones
#.Nil
(meta.fail (format "No structure option could be found for member: " (%.name member)))
(#.Cons chosen #.Nil)
(wrap (list (` (\ (~ (instance$ chosen))
- (~ (code.local-identifier (product.right member)))
+ (~ (code.local_identifier (product.right member)))
(~+ (list\map code.identifier args))))))
_
(meta.fail (format "Too many options available: "
- (|> chosen-ones
+ (|> chosen_ones
(list\map (|>> product.left %.name))
- (text.join-with ", "))
- " --- for type: " (%.type sig-type)))))
+ (text.join_with ", "))
+ " --- for type: " (%.type sig_type)))))
(#.Right [args _])
(do {! meta.monad}
[labels (|> (meta.gensym "") (list.repeat (list.size args)) (monad.seq !))]
- (wrap (list (` (let [(~+ (|> (list.zip/2 labels args) (list\map join-pair) list\join))]
+ (wrap (list (` (let [(~+ (|> (list.zip/2 labels args) (list\map join_pair) list\join))]
(..\\ (~ (code.identifier member)) (~+ labels)))))))
))
-(def: (implicit-bindings amount)
+(def: (implicit_bindings amount)
(-> Nat (Meta (List Code)))
(|> (meta.gensym "g!implicit")
(list.repeat amount)
@@ -382,7 +382,7 @@
(syntax: #export (implicit {structures ..implicits} body)
(do meta.monad
- [g!implicit+ (implicit-bindings (list.size structures))]
+ [g!implicit+ (implicit_bindings (list.size structures))]
(wrap (list (` (let [(~+ (|> (list.zip/2 g!implicit+ structures)
(list\map (function (_ [g!implicit structure])
(list g!implicit structure)))
@@ -391,7 +391,7 @@
(syntax: #export (implicit: {structures ..implicits})
(do meta.monad
- [g!implicit+ (implicit-bindings (list.size structures))]
+ [g!implicit+ (implicit_bindings (list.size structures))]
(wrap (|> (list.zip/2 g!implicit+ structures)
(list\map (function (_ [g!implicit structure])
(` (def: (~ g!implicit) (~ structure)))))))))
diff --git a/stdlib/source/lux/type/refinement.lux b/stdlib/source/lux/type/refinement.lux
index 1daa8ff1b..3429d28af 100644
--- a/stdlib/source/lux/type/refinement.lux
+++ b/stdlib/source/lux/type/refinement.lux
@@ -5,7 +5,7 @@
["." meta]
[macro
[syntax (#+ syntax:)]]
- [type (#+ :by-example)
+ [type (#+ :by_example)
abstract]])
(abstract: #export (Refined t r)
@@ -21,9 +21,9 @@
(All [t]
(Ex [r]
(-> (Predicate t) (Refiner t r))))
- (function (_ un-refined)
- (if (predicate un-refined)
- (#.Some (:abstraction {#value un-refined
+ (function (_ un_refined)
+ (if (predicate un_refined)
+ (#.Some (:abstraction {#value un_refined
#predicate predicate}))
#.None)))
@@ -32,7 +32,7 @@
(All [t r] (-> (Refined t r) <output>))
(|> refined :representation (get@ <slot>)))]
- [un-refine t #value]
+ [un_refine t #value]
[predicate (Predicate t) #predicate]
)
@@ -81,8 +81,8 @@
(#.Cons head no)]))))
(syntax: #export (type refiner)
- (meta.with-gensyms [g!t g!r]
- (wrap (list (` ((~! :by-example) [(~ g!t) (~ g!r)]
+ (meta.with_gensyms [g!t g!r]
+ (wrap (list (` ((~! :by_example) [(~ g!t) (~ g!r)]
{(..Refiner (~ g!t) (~ g!r))
(~ refiner)}
(..Refined (~ g!t) (~ g!r))))))))
diff --git a/stdlib/source/lux/type/resource.lux b/stdlib/source/lux/type/resource.lux
index b91f9d990..26407ba39 100644
--- a/stdlib/source/lux/type/resource.lux
+++ b/stdlib/source/lux/type/resource.lux
@@ -74,9 +74,9 @@
[output procedure]
(wrap [keys output]))))]
- [pure Identity identity.monad run-pure lift-pure]
- [sync IO io.monad run-sync lift-sync]
- [async Promise promise.monad run-async lift-async]
+ [pure Identity identity.monad run_pure lift_pure]
+ [sync IO io.monad run_sync lift_sync]
+ [async Promise promise.monad run_async lift_async]
)
(abstract: #export Ordered [])
@@ -91,8 +91,8 @@
(Ex [k] (-> [] (Key <mode> k)))
(|>> :abstraction))]
- [ordered-key Ordered]
- [commutative-key Commutative]
+ [ordered_key Ordered]
+ [commutative_key Commutative]
))
(type: #export OK (Key Ordered))
@@ -109,12 +109,12 @@
(function (_ keys)
(\ <monad> wrap [[(<key> []) keys] (:abstraction value)])))]
- [ordered-pure Identity identity.monad Ordered ordered-key]
- [ordered-sync IO io.monad Ordered ordered-key]
- [ordered-async Promise promise.monad Ordered ordered-key]
- [commutative-sync IO io.monad Commutative commutative-key]
- [commutative-pure Identity identity.monad Commutative commutative-key]
- [commutative-async Promise promise.monad Commutative commutative-key]
+ [ordered_pure Identity identity.monad Ordered ordered_key]
+ [ordered_sync IO io.monad Ordered ordered_key]
+ [ordered_async Promise promise.monad Ordered ordered_key]
+ [commutative_sync IO io.monad Commutative commutative_key]
+ [commutative_pure Identity identity.monad Commutative commutative_key]
+ [commutative_async Promise promise.monad Commutative commutative_key]
)
(template [<name> <m> <monad>]
@@ -124,16 +124,16 @@
(function (_ [key keys])
(\ <monad> wrap [keys (:representation resource)])))]
- [read-pure Identity identity.monad]
- [read-sync IO io.monad]
- [read-async Promise promise.monad]
+ [read_pure Identity identity.monad]
+ [read_sync IO io.monad]
+ [read_async Promise promise.monad]
))
-(exception: #export (index-cannot-be-repeated {index Nat})
+(exception: #export (index_cannot_be_repeated {index Nat})
(exception.report
["Index" (%.nat index)]))
-(exception: #export amount-cannot-be-zero)
+(exception: #export amount_cannot_be_zero)
(def: indices
(Parser (List Nat))
@@ -144,26 +144,26 @@
(wrap (list))
(do !
[head s.nat
- _ (p.assert (exception.construct index-cannot-be-repeated head)
+ _ (p.assert (exception.construct index_cannot_be_repeated head)
(not (set.member? seen head)))
tail (recur (set.add head seen))]
(wrap (list& head tail))))))))
-(def: (no-op Monad<m>)
+(def: (no_op Monad<m>)
(All [m] (-> (Monad m) (Linear m Any)))
(function (_ context) (\ Monad<m> wrap [context []])))
(template [<name> <m> <monad>]
[(syntax: #export (<name> {swaps ..indices})
- (meta.with-gensyms [g!_ g!context]
+ (meta.with_gensyms [g!_ g!context]
(case swaps
#.Nil
- (wrap (list (` ((~! no-op) <monad>))))
+ (wrap (list (` ((~! no_op) <monad>))))
(#.Cons head tail)
(do {! meta.monad}
- [#let [max-idx (list\fold n.max head tail)]
- g!inputs (<| (monad.seq !) (list.repeat (inc max-idx)) (meta.gensym "input"))
+ [#let [max_idx (list\fold n.max head tail)]
+ g!inputs (<| (monad.seq !) (list.repeat (inc max_idx)) (meta.gensym "input"))
#let [g!outputs (|> (monad.fold maybe.monad
(function (_ from to)
(do maybe.monad
@@ -172,7 +172,7 @@
(: (Row Code) row.empty)
swaps)
maybe.assume
- row.to-list)
+ row.to_list)
g!inputsT+ (list\map (|>> (~) ..CK (`)) g!inputs)
g!outputsT+ (list\map (|>> (~) ..CK (`)) g!outputs)]]
(wrap (list (` (: (All [(~+ g!inputs) (~ g!context)]
@@ -183,22 +183,22 @@
(function ((~ g!_) [(~+ g!inputs) (~ g!context)])
(\ (~! <monad>) (~' wrap) [[(~+ g!outputs) (~ g!context)] []]))))))))))]
- [exchange-pure Identity identity.monad]
- [exchange-sync IO io.monad]
- [exchange-async Promise promise.monad]
+ [exchange_pure Identity identity.monad]
+ [exchange_sync IO io.monad]
+ [exchange_async Promise promise.monad]
)
(def: amount
(Parser Nat)
(do p.monad
[raw s.nat
- _ (p.assert (exception.construct amount-cannot-be-zero [])
+ _ (p.assert (exception.construct ..amount_cannot_be_zero [])
(n.> 0 raw))]
(wrap raw)))
(template [<name> <m> <monad> <from> <to>]
[(syntax: #export (<name> {amount ..amount})
- (meta.with-gensyms [g!_ g!context]
+ (meta.with_gensyms [g!_ g!context]
(do {! meta.monad}
[g!keys (<| (monad.seq !) (list.repeat amount) (meta.gensym "keys"))]
(wrap (list (` (: (All [(~+ g!keys) (~ g!context)]
@@ -209,10 +209,10 @@
(function ((~ g!_) [<from> (~ g!context)])
(\ (~! <monad>) (~' wrap) [[<to> (~ g!context)] []])))))))))]
- [group-pure Identity identity.monad (~+ g!keys) [(~+ g!keys)]]
- [group-sync IO io.monad (~+ g!keys) [(~+ g!keys)]]
- [group-async Promise promise.monad (~+ g!keys) [(~+ g!keys)]]
- [un-group-pure Identity identity.monad [(~+ g!keys)] (~+ g!keys)]
- [un-group-sync IO io.monad [(~+ g!keys)] (~+ g!keys)]
- [un-group-async Promise promise.monad [(~+ g!keys)] (~+ g!keys)]
+ [group_pure Identity identity.monad (~+ g!keys) [(~+ g!keys)]]
+ [group_sync IO io.monad (~+ g!keys) [(~+ g!keys)]]
+ [group_async Promise promise.monad (~+ g!keys) [(~+ g!keys)]]
+ [un_group_pure Identity identity.monad [(~+ g!keys)] (~+ g!keys)]
+ [un_group_sync IO io.monad [(~+ g!keys)] (~+ g!keys)]
+ [un_group_async Promise promise.monad [(~+ g!keys)] (~+ g!keys)]
)
diff --git a/stdlib/source/lux/type/unit.lux b/stdlib/source/lux/type/unit.lux
index 9f5fdba78..c00b0eae4 100644
--- a/stdlib/source/lux/type/unit.lux
+++ b/stdlib/source/lux/type/unit.lux
@@ -40,7 +40,7 @@
(: (All [u] (-> (Qty u) (Qty (s u))))
scale)
(: (All [u] (-> (Qty (s u)) (Qty u)))
- de-scale)
+ de_scale)
(: Ratio
ratio))
@@ -64,21 +64,21 @@
[(def: <name>
(-> Text Text)
(|>> (format "{" kind "@" module "}")
- (let [[module kind] (name-of <tag>)])))]
+ (let [[module kind] (name_of <tag>)])))]
- [unit-name #..Unit]
- [scale-name #..Scale]
+ [unit_name #..Unit]
+ [scale_name #..Scale]
)
(syntax: #export (unit:
{export |export|.parser}
- {name s.local-identifier}
- {annotations (p.default cs.empty-annotations csr.annotations)})
- (wrap (list (` (type: (~+ (|export|.write export)) (~ (code.local-identifier name))
+ {name s.local_identifier}
+ {annotations (p.default cs.empty_annotations csr.annotations)})
+ (wrap (list (` (type: (~+ (|export|.write export)) (~ (code.local_identifier name))
(~ (csw.annotations annotations))
- (primitive (~ (code.text (unit-name name))))))
- (` (def: (~+ (|export|.write export)) (~ (code.local-identifier (format "@" name)))
- (~ (code.local-identifier name))
+ (primitive (~ (code.text (unit_name name))))))
+ (` (def: (~+ (|export|.write export)) (~ (code.local_identifier (format "@" name)))
+ (~ (code.local_identifier name))
(:assume [])))
)))
@@ -95,21 +95,21 @@
(syntax: #export (scale:
{export |export|.parser}
- {name s.local-identifier}
+ {name s.local_identifier}
{(^slots [#ratio.numerator #ratio.denominator]) ratio^}
- {annotations (p.default cs.empty-annotations csr.annotations)})
- (let [g!scale (code.local-identifier name)]
+ {annotations (p.default cs.empty_annotations csr.annotations)})
+ (let [g!scale (code.local_identifier name)]
(wrap (list (` (type: (~+ (|export|.write export)) ((~ g!scale) (~' u))
(~ (csw.annotations annotations))
- (primitive (~ (code.text (scale-name name))) [(~' u)])))
- (` (structure: (~+ (|export|.write export)) (~ (code.local-identifier (format "@" name)))
+ (primitive (~ (code.text (scale_name name))) [(~' u)])))
+ (` (structure: (~+ (|export|.write export)) (~ (code.local_identifier (format "@" name)))
(..Scale (~ g!scale))
(def: (~' scale)
(|>> ..out
(i.* (~ (code.int (.int numerator))))
(i./ (~ (code.int (.int denominator))))
..in))
- (def: (~' de-scale)
+ (def: (~' de_scale)
(|>> ..out
(i.* (~ (code.int (.int denominator))))
(i./ (~ (code.int (.int numerator))))
@@ -143,7 +143,7 @@
(i.* (out (input param)))
in)))
-(def: #export (re-scale from to quantity)
+(def: #export (re_scale from to quantity)
(All [si so u] (-> (Scale si) (Scale so) (Qty (si u)) (Qty (so u))))
(let [[numerator denominator] (ratio./ (\ from ratio)
(\ to ratio))]
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-13 11:28:07 +0000