diff options
-rw-r--r-- | stdlib/source/lux/math/constructive.lux | 199 | ||||
-rw-r--r-- | stdlib/test/test/lux/math/constructive.lux | 58 |
2 files changed, 0 insertions, 257 deletions
diff --git a/stdlib/source/lux/math/constructive.lux b/stdlib/source/lux/math/constructive.lux deleted file mode 100644 index 2a904f7cb..000000000 --- a/stdlib/source/lux/math/constructive.lux +++ /dev/null @@ -1,199 +0,0 @@ -(.module: - [lux #+ ->] - (lux (control [monad #+ do] - ["p" parser "parser/" Monad<Parser>] - ["ex" exception #+ exception:]) - (data [product] - ["e" error] - text/format - (coll [list "list/" Functor<List>])) - (lang [type]) - (type abstract) - [macro] - (macro [code] - ["s" syntax #+ syntax:] - (syntax (common ["scr" reader] - ["scw" writer])) - [poly]))) - -(abstract: #export (Witness t w) - {} - - t - - (.def: #export ! - (.All [t] - (.Ex [w] - (-> t (Witness t w)))) - (.|>> :abstraction)) - - (.def: #export ? - (.All [t w] - (-> (Witness t w) t)) - (.|>> :representation)) - ) - -(syntax: #export (@ {name s.symbol}) - (do @ - [witnessT (macro.find-type name)] - (.case (.<| (poly.run witnessT) - poly.apply - (p.after (poly.this Witness)) - (p.after poly.any) - poly.any) - (#e.Success identityT) - (wrap (.list (type.to-code identityT))) - - (#e.Error error) - (macro.fail error)))) - -(syntax: #export (proof: - {export? scr.export} - {name s.local-symbol} - type - proof) - (do @ - [g!w (macro.gensym "w")] - (wrap (.list (.` (.def: (~+ (scw.export export?)) - (~ (code.local-symbol name)) - (..! (.: (~ type) - (~ proof))))))))) - -(.def: type-vars - (s.Syntax (.List .Text)) - (p.default (.list) - (s.tuple (p.some s.local-symbol)))) - -(.type: Input' - {#input-name .Text - #input-type .Code}) - -(.type: Input - (#Identified Input') - (#Anonymous Input')) - -(.do-template [<name> <tag> <type>] - [(.def: (<name> input) - (-> Input <type>) - (.case input - (#Identified input') - (.get@ <tag> input') - - (#Anonymous input') - (.get@ <tag> input')))] - - [input-name #input-name .Text] - [input-type #input-type .Code] - ) - -(.def: (identified? input) - (-> Input .Bool) - (.case input - (#Identified input') - true - - (#Anonymous input') - false)) - -(.def: input - (s.Syntax Input) - (p.alt (s.record (p.seq s.local-symbol s.any)) - (s.tuple (p.seq s.local-symbol s.any)))) - -(.def: theorem-declaration - (s.Syntax [.Text (.List Input)]) - (s.form (p.seq s.local-symbol (p.some input)))) - -(.def: proposition-declaration - (s.Syntax [.Text (.List .Text)]) - (s.form (p.seq s.local-symbol (p.many s.local-symbol)))) - -(syntax: #export (proposition: - {export? scr.export} - {[name elements] proposition-declaration} - {meaning (p.maybe s.any)}) - (.case meaning - #.None - (wrap (.list (.` ((~! abstract:) (~+ (scw.export export?)) - ((~ (code.local-symbol name)) - (~+ (list/map code.local-symbol elements))) - - {} - - .Any)))) - - (#.Some meaning) - (wrap (.list (.` (.type: (~+ (scw.export export?)) - ((~ (code.local-symbol name)) - (~+ (list/map code.local-symbol elements))) - (~ meaning))))))) - -(.def: (theorem-type type-vars inputs meaning) - (-> (.List .Text) (.List Input) .Code .Code) - (.let [g!universals (list/map code.local-symbol - type-vars) - g!identities (.|> inputs - (list.filter identified?) - (list/map (.|>> input-name code.local-symbol))) - g!requisites (list/map (.function (_ input) - (.case input - (#Identified input') - (.` (..Witness (~ (.get@ #input-type input')) - (~ (code.local-symbol (input-name input))))) - - (#Anonymous input') - (.get@ #input-type input'))) - inputs)] - (.` (.All [(~+ g!universals)] - (.Ex [(~+ g!identities)] - (-> (~+ g!requisites) (~ meaning))))))) - -(syntax: #export (axiom {description (p.default "" s.text)}) - (wrap (.list (.` (.:assume []))))) - -(syntax: #export (theorem {type-vars type-vars} - {[name inputs] theorem-declaration} - outputT - meaning) - (.let [inputs-names (list/map (.|>> input-name code.local-symbol) - inputs)] - (wrap (.list (.` (.: (~ (theorem-type type-vars inputs outputT)) - (.function ((~ (code.local-symbol name)) (~+ inputs-names)) - (~ meaning)))))))) - -(.def: (input-code input) - (-> Input .Code) - (.case input - (#Identified [name type]) - (.` {(~ (code.local-symbol name)) (~ type)}) - - (#Anonymous [name type]) - (.` [(~ (code.local-symbol name)) (~ type)]))) - -(syntax: #export (theorem: - {export? scr.export} - {type-vars type-vars} - {[name inputs] theorem-declaration} - outputT - meaning) - (wrap (.list (.` (..proof: (~+ (scw.export export?)) - (~ (code.local-symbol name)) - (~ (theorem-type type-vars inputs outputT)) - (..theorem [(~+ (list/map code.local-symbol type-vars))] - ((~ (code.local-symbol name)) (~+ (list/map input-code inputs))) - (~ outputT) - (~ meaning))))))) - -(.type: #export (not p) - (-> p .Nothing)) - -(.type: #export (Test p) - (#True p) - (#False (not p))) - -(exception: #export absurd) - -(.def: #export absurdity - (.All [p] (-> p .Nothing)) - (.function (_ proof) - (.error! (ex.construct absurd [])))) diff --git a/stdlib/test/test/lux/math/constructive.lux b/stdlib/test/test/lux/math/constructive.lux deleted file mode 100644 index 86f8b7360..000000000 --- a/stdlib/test/test/lux/math/constructive.lux +++ /dev/null @@ -1,58 +0,0 @@ -(.module: - [lux #+ ->] - (lux (data text/format) - (math ["_" constructive #*]))) - -(theorem: #export (n/+ [param .Nat] [subject .Nat]) - .Nat - (.n/+ param subject)) - -(proposition: #export (apply2 f input0 input1 output)) - -(proposition: #export (commutativity f left right output) - (-> (apply2 f left right output) - (apply2 f right left output))) - -(proof: #export n/+|commutativity - (commutativity (~ (@ n/+))) - (theorem [@left @right @output] - (_ [normal (apply2 (~ (@ n/+)) @left @right @output)]) - (apply2 (~ (@ n/+)) @right @left @output) - - (axiom "n/+|commutativity"))) - -(proposition: #export (equality reference sample)) - -(theorem: #export [t] (is {reference t} {sample t}) - (Test (equality reference sample)) - (.if (.is? reference sample) - (#_.True (.let [the-axiom (axiom "is")] - the-axiom)) - (#_.False absurdity))) - -(proposition: #export (relation2 rel reference sample)) - -(proposition: #export (reflexivity rel value) - (relation2 rel value value)) - -(proposition: #export (symmetry rel left right) - (-> (relation2 rel left right) - (relation2 rel right left))) - -(proposition: #export (transitivity rel left mid right) - (-> [(relation2 rel left mid) - (relation2 rel mid right)] - (relation2 rel left right))) - -(theorem: #export [t0 t1 t2] ($2 {f (-> t0 t1 t2)} - {input0 t0} - {input1 t1}) - [t2 (apply2 f input0 input1 t2)] - (.let [output ((? f) (? input0) (? input1))] - [output (axiom)])) - -(theorem: (can-commute-n/+ {param .Nat} {subject .Nat}) - .Nat - (.let [[output apply2] ((? $2) n/+ param subject) - output|commutes! ((? n/+|commutativity) apply2)] - output)) |