aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source
diff options
context:
space:
mode:
authorEduardo Julian2017-12-28 23:19:37 -0400
committerEduardo Julian2017-12-28 23:19:37 -0400
commit59d674d660b4e52ec54ef046024b850b4eeb7a0f (patch)
tree7a870b0adea8003003309c7e55198c3f448cc59b /stdlib/source
parentbcb247513c80d321fcdd20e655b666a97269c54e (diff)
- A small, in-development module for doing constructive mathematics with something close to dependent types.
Diffstat (limited to 'stdlib/source')
-rw-r--r--stdlib/source/lux/math/constructive.lux196
1 files changed, 196 insertions, 0 deletions
diff --git a/stdlib/source/lux/math/constructive.lux b/stdlib/source/lux/math/constructive.lux
new file mode 100644
index 000000000..3f12d1a88
--- /dev/null
+++ b/stdlib/source/lux/math/constructive.lux
@@ -0,0 +1,196 @@
+(.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>]))
+ (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.existential)
+ (#e.Success witness-id)
+ (wrap (.list (.` (#.Ex (~ (code.nat witness-id))))))
+
+ (#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)))
+
+ {}
+
+ .Unit))))
+
+ (#.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 (.` (.:!! [])))))
+
+(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 .Bottom))
+
+(.type: #export (Test p)
+ (#True p)
+ (#False (not p)))
+
+(exception: #export Absurdity)
+
+(.def: #export absurdity
+ (.All [p] (-> p .Bottom))
+ (.function [proof]
+ (.error! (Absurdity ""))))