aboutsummaryrefslogtreecommitdiff
path: root/stdlib
diff options
context:
space:
mode:
Diffstat (limited to 'stdlib')
-rw-r--r--stdlib/source/lux/math/constructive.lux199
-rw-r--r--stdlib/test/test/lux/math/constructive.lux58
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))
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 17:29:29 +0000