mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-10-06 04:17:14 +03:00
Rebuild
This commit is contained in:
Victor Maia
parent
b5ad5d4e7f
commit
5d504fc14d
@ -1,61 +0,0 @@
|
||||
Bench
|
||||
=====
|
||||
|
||||
Benchmarks of Kind2 vs other proof assistants. These benchmarks measure the time
|
||||
each assistant takes to verify a given file. Replicate as follows:
|
||||
|
||||
### Agda
|
||||
|
||||
```
|
||||
time agda -i src file.agda
|
||||
```
|
||||
|
||||
### Coq
|
||||
|
||||
```
|
||||
time coqtop -l file.v -batch -type-in-type
|
||||
```
|
||||
|
||||
### Idris2
|
||||
|
||||
```
|
||||
time idris2 --check file.idr
|
||||
```
|
||||
|
||||
### Lean
|
||||
|
||||
```
|
||||
time lean file.lean
|
||||
```
|
||||
|
||||
### Kind2
|
||||
|
||||
```
|
||||
time kind2 check file.kind2
|
||||
```
|
||||
|
||||
### Kind2-C
|
||||
|
||||
```
|
||||
kind2 gen-checker file.kind2
|
||||
hvm compile file.check.hvm
|
||||
clang file.check.c -O3 -o check
|
||||
time ./check
|
||||
```
|
||||
|
||||
Results
|
||||
=======
|
||||
|
||||
### nat_exp
|
||||
|
||||
Computes `3 ^ 8`, using the Nat type, on the type level.
|
||||
|
||||
```
|
||||
language | time
|
||||
-------- | --------
|
||||
Kind2-C | 0.17 s
|
||||
Kind2 | 0.58 s
|
||||
Agda | 15.55 s
|
||||
Idris2 | 67.40 s
|
||||
Lean | timeout
|
||||
```
|
||||
@ -13,8 +13,10 @@ echo "Building Kind2 type checker"
|
||||
|
||||
# Probably we should just use git clone in Wikind?
|
||||
cd ../Wikind
|
||||
$KIND2 check Kind/TypeChecker.kind2
|
||||
#$KIND2 check Kind/TypeChecker.kind2
|
||||
$KIND2 to-hvm Kind/TypeChecker.kind2 > ../Kind2/src/checker.hvm
|
||||
|
||||
cd $CURRENT
|
||||
cargo build --release
|
||||
cargo install --path $CURRENT
|
||||
|
||||
#cd $CURRENT
|
||||
#cargo build --release
|
||||
|
||||
629
src/checker.hvm
629
src/checker.hvm
@ -62,6 +62,17 @@
|
||||
// Kind.API.output.error.details (fnid: U60) (ctx: (Kind.Context)) (sub: (Kind.Subst)) (origin: U60) : (String)
|
||||
(Kind.API.output.error.details fnid ctx sub orig) = (Kind.Printer.text (List.cons (Bool.if (Kind.Context.is_empty ctx) "" (Kind.Printer.text (List.cons (Kind.Printer.color "4") (List.cons "Kind.Context:" (List.cons (Kind.Printer.color "0") (List.cons (String.new_line) (List.cons (Kind.Context.show ctx sub) (List.nil)))))))) (List.cons (Kind.Printer.color "4") (List.cons (String.cons 79 (String.cons 110 (String.cons 32 (String.cons 39 "{{#F")))) (List.cons (Show.to_string (U60.show (>> orig 48))) (List.cons (String.cons 70 (String.cons 35 (String.cons 125 (String.cons 125 (String.cons 39 ":"))))) (List.cons (Kind.Printer.color "0") (List.cons (String.new_line) (List.cons "{{#R" (List.cons (Show.to_string (U60.show (>> orig 48))) (List.cons ":" (List.cons (Show.to_string (U60.show (& orig 16777215))) (List.cons ":" (List.cons (Show.to_string (U60.show (& (>> orig 24) 16777215))) (List.cons "R#}}" (List.cons (String.new_line) (List.nil)))))))))))))))))
|
||||
|
||||
// Kind.Printer.color (color_code: (String)) : (String)
|
||||
(Kind.Printer.color color_code) = (Kind.Printer.text (List.cons (String.cons 27 "") (List.cons "[" (List.cons color_code (List.cons "m" (List.nil))))))
|
||||
|
||||
// Kind.Printer.text (ls: (List (String))) : (String)
|
||||
(Kind.Printer.text (List.nil)) = ""
|
||||
(Kind.Printer.text (List.cons x xs)) = (String.concat x (Kind.Printer.text xs))
|
||||
|
||||
// String.concat (xs: (String)) (ys: (String)) : (String)
|
||||
(String.concat (String.cons x xs) ys) = (String.cons x (String.concat xs ys))
|
||||
(String.concat "" ys) = ys
|
||||
|
||||
// Kind.Term.fill (term: (Kind.Term)) (subst: (Kind.Subst)) : (Kind.Term)
|
||||
(Kind.Term.fill term (Kind.Subst.end)) = term
|
||||
(Kind.Term.fill (Kind.Term.typ orig) sub) = (Kind.Term.typ orig)
|
||||
@ -104,10 +115,6 @@
|
||||
(Maybe.match (Maybe.none) none some) = none
|
||||
(Maybe.match (Maybe.some value_) none some) = (some value_)
|
||||
|
||||
// Kind.Term.eval_app (orig: U60) (left: (Kind.Term)) (right: (Kind.Term)) : (Kind.Term)
|
||||
(Kind.Term.eval_app orig (Kind.Term.lam orig1 name body) arg) = (body arg)
|
||||
(Kind.Term.eval_app orig func arg) = (Kind.Term.app orig func arg)
|
||||
|
||||
// Kind.Term.eval_ann (orig: U60) (expr: (Kind.Term)) (type: (Kind.Term)) : (Kind.Term)
|
||||
(Kind.Term.eval_ann orig expr type) = expr
|
||||
|
||||
@ -119,13 +126,9 @@
|
||||
(Kind.Subst.look (Kind.Subst.unfilled rest) n) = (Kind.Subst.look rest (- n 1))
|
||||
(Kind.Subst.look (Kind.Subst.sub term rest) n) = (Kind.Subst.look rest (- n 1))
|
||||
|
||||
// Kind.Printer.text (ls: (List (String))) : (String)
|
||||
(Kind.Printer.text (List.nil)) = ""
|
||||
(Kind.Printer.text (List.cons x xs)) = (String.concat x (Kind.Printer.text xs))
|
||||
|
||||
// String.concat (xs: (String)) (ys: (String)) : (String)
|
||||
(String.concat (String.cons x xs) ys) = (String.cons x (String.concat xs ys))
|
||||
(String.concat "" ys) = ys
|
||||
// Kind.Term.eval_app (orig: U60) (left: (Kind.Term)) (right: (Kind.Term)) : (Kind.Term)
|
||||
(Kind.Term.eval_app orig (Kind.Term.lam orig1 name body) arg) = (body arg)
|
||||
(Kind.Term.eval_app orig func arg) = (Kind.Term.app orig func arg)
|
||||
|
||||
// Kind.Context.show.type (name: U60) (type: (Kind.Term)) (sub: (Kind.Subst)) (pad: U60) : (String)
|
||||
(Kind.Context.show.type name type sub pad) = (Kind.Printer.text (List.cons "- " (List.cons (String.pad_right (U60.to_nat pad) 32 (Kind.Name.show name)) (List.cons " : " (List.cons (String.cut (Kind.Term.show (Kind.Term.fill type sub))) (List.cons (String.new_line) (List.nil)))))))
|
||||
@ -141,31 +144,6 @@
|
||||
// Kind.Context.show (ctx: (Kind.Context)) (subst: (Kind.Subst)) : (String)
|
||||
(Kind.Context.show ctx subst) = (Kind.Context.show.go ctx subst (Kind.Context.max_name_length ctx))
|
||||
|
||||
// U60.to_nat (x: U60) : (Nat)
|
||||
(U60.to_nat 0) = (Nat.zero)
|
||||
(U60.to_nat n) = (Nat.succ (U60.to_nat (- n 1)))
|
||||
|
||||
// Kind.Name.show.go (name: U60) (chrs: (String)) : (String)
|
||||
(Kind.Name.show.go name chrs) = (U60.if (== name 0) chrs let val = (% name 64); let chr = (U60.if (== val 0) 46 (U60.if (& (<= 1 val) (<= val 10)) (+ (- val 1) 48) (U60.if (& (<= 11 val) (<= val 36)) (+ (- val 11) 65) (U60.if (& (<= 37 val) (<= val 62)) (+ (- val 37) 97) (U60.if (== val 63) 95 63))))); (Kind.Name.show.go (/ name 64) (String.cons chr chrs)))
|
||||
|
||||
// Kind.Name.show (name: U60) : (String)
|
||||
(Kind.Name.show name) = (Kind.Name.show.go name "")
|
||||
|
||||
// U60.if -(r: Type) (n: U60) (t: r) (f: r) : r
|
||||
(U60.if 0 t f) = f
|
||||
(U60.if x t f) = t
|
||||
|
||||
// String.pad_right (size: (Nat)) (chr: (Char)) (str: (String)) : (String)
|
||||
(String.pad_right (Nat.zero) chr str) = str
|
||||
(String.pad_right (Nat.succ sp) chr "") = (String.cons chr (String.pad_right sp chr ""))
|
||||
(String.pad_right (Nat.succ sp) chr (String.cons x xs)) = (String.cons x (String.pad_right sp chr xs))
|
||||
|
||||
// Char : Type
|
||||
(Char) = 0
|
||||
|
||||
// Kind.Printer.color (color_code: (String)) : (String)
|
||||
(Kind.Printer.color color_code) = (Kind.Printer.text (List.cons (String.cons 27 "") (List.cons "[" (List.cons color_code (List.cons "m" (List.nil))))))
|
||||
|
||||
// Kind.Term.show.forall (orig: U60) (name: U60) (type: (Kind.Term)) (body: (_: (Kind.Term)) (Kind.Term)) : (String)
|
||||
(Kind.Term.show.forall orig name type body) = (U60.if (== name 63) (Kind.Printer.text (List.cons "(" (List.cons (Kind.Term.show type) (List.cons " -> " (List.cons (Kind.Term.show (body (Kind.Term.var orig name 0))) (List.cons ")" (List.nil))))))) (Kind.Printer.text (List.cons "((" (List.cons (Kind.Name.show name) (List.cons ": " (List.cons (Kind.Term.show type) (List.cons ") -> " (List.cons (Kind.Term.show (body (Kind.Term.var orig name 0))) (List.cons ")" (List.nil))))))))))
|
||||
|
||||
@ -206,38 +184,19 @@
|
||||
(Kind.Term.show.go (Kind.Term.num orig numb)) = (Show.to_string (U60.show numb))
|
||||
(Kind.Term.show.go (Kind.Term.op2 orig operator left right)) = (Kind.Printer.text (List.cons "(" (List.cons (Kind.Operator.show operator) (List.cons " " (List.cons (Kind.Term.show left) (List.cons " " (List.cons (Kind.Term.show right) (List.cons ")" (List.nil)))))))))
|
||||
|
||||
// Maybe.try -(a: Type) (ls: (List (Maybe a))) (alt: a) : a
|
||||
(Maybe.try (List.nil) alt) = alt
|
||||
(Maybe.try (List.cons maybe xs) alt) = (Maybe.match maybe (Maybe.try xs alt) @maybe.value maybe.value)
|
||||
|
||||
// Show.to_string (show: (Show)) : (String)
|
||||
(Show.to_string show) = (show "")
|
||||
|
||||
// Show : Type
|
||||
(Show) = 0
|
||||
|
||||
// Kind.Term.show.sugar.string.go (term: (Kind.Term)) : (Maybe (String))
|
||||
(Kind.Term.show.sugar.string.go (Kind.Term.ct0 (String.nil.) orig)) = (Maybe.some "")
|
||||
(Kind.Term.show.sugar.string.go (Kind.Term.ct2 (String.cons.) orig (Kind.Term.num orig1 x0) x1)) = (Maybe.bind (Kind.Term.show.sugar.string.go x1) @tail (Maybe.pure (String.cons x0 tail)))
|
||||
(Kind.Term.show.sugar.string.go other) = (Maybe.none)
|
||||
|
||||
// Kind.Term.show.sugar.string (term: (Kind.Term)) : (Maybe (String))
|
||||
(Kind.Term.show.sugar.string term) = (Maybe.bind (Kind.Term.show.sugar.string.go term) @res let quot = (String.cons 39 ""); (Maybe.pure (Kind.Printer.text (List.cons quot (List.cons res (List.cons quot (List.nil)))))))
|
||||
|
||||
// Maybe.bind -(a: Type) -(b: Type) (ma: (Maybe a)) (mb: (_: a) (Maybe b)) : (Maybe b)
|
||||
(Maybe.bind (Maybe.none) mb) = (Maybe.none)
|
||||
(Maybe.bind (Maybe.some val) mb) = (mb val)
|
||||
|
||||
// Maybe.pure -(a: Type) (x: a) : (Maybe a)
|
||||
(Maybe.pure x) = (Maybe.some x)
|
||||
|
||||
// Kind.Term.show.sugar.sigma (term: (Kind.Term)) : (Maybe (String))
|
||||
(Kind.Term.show.sugar.sigma (Kind.Term.ct2 (Sigma.) orig typ (Kind.Term.lam orig_ name body))) = (Maybe.some (Kind.Printer.text (List.cons "([" (List.cons (Kind.Name.show name) (List.cons ": " (List.cons (Kind.Term.show typ) (List.cons "] -> " (List.cons (Kind.Term.show (body (Kind.Term.var orig_ name 0))) (List.cons ")" (List.nil))))))))))
|
||||
(Kind.Term.show.sugar.sigma term) = (Maybe.none)
|
||||
|
||||
// U60.show (n: U60) : (Show)
|
||||
(U60.show 0) = @str (String.cons 48 str)
|
||||
(U60.show n) = @str let next = (String.cons (+ 48 (% n 10)) str); let func = (U60.if (< n 10) @h h @h ((U60.show (/ n 10)) h)); (func next)
|
||||
// Kind.Name.show.go (name: U60) (chrs: (String)) : (String)
|
||||
(Kind.Name.show.go name chrs) = (U60.if (== name 0) chrs let val = (% name 64); let chr = (U60.if (== val 0) 46 (U60.if (& (<= 1 val) (<= val 10)) (+ (- val 1) 48) (U60.if (& (<= 11 val) (<= val 36)) (+ (- val 11) 65) (U60.if (& (<= 37 val) (<= val 62)) (+ (- val 37) 97) (U60.if (== val 63) 95 63))))); (Kind.Name.show.go (/ name 64) (String.cons chr chrs)))
|
||||
|
||||
// Kind.Name.show (name: U60) : (String)
|
||||
(Kind.Name.show name) = (Kind.Name.show.go name "")
|
||||
|
||||
// U60.if -(r: Type) (n: U60) (t: r) (f: r) : r
|
||||
(U60.if 0 t f) = f
|
||||
(U60.if x t f) = t
|
||||
|
||||
// Kind.Operator.show (op: (Kind.Operator)) : (String)
|
||||
(Kind.Operator.show (Kind.Operator.add)) = "+"
|
||||
@ -257,6 +216,34 @@
|
||||
(Kind.Operator.show (Kind.Operator.gtn)) = ">"
|
||||
(Kind.Operator.show (Kind.Operator.neq)) = "!="
|
||||
|
||||
// Show.to_string (show: (Show)) : (String)
|
||||
(Show.to_string show) = (show "")
|
||||
|
||||
// Show : Type
|
||||
(Show) = 0
|
||||
|
||||
// Show : Type
|
||||
(Show) = 0
|
||||
|
||||
// Maybe.try -(a: Type) (ls: (List (Maybe a))) (alt: a) : a
|
||||
(Maybe.try (List.nil) alt) = alt
|
||||
(Maybe.try (List.cons maybe xs) alt) = (Maybe.match maybe (Maybe.try xs alt) @maybe.value maybe.value)
|
||||
|
||||
// Kind.Term.show.sugar.string.go (term: (Kind.Term)) : (Maybe (String))
|
||||
(Kind.Term.show.sugar.string.go (Kind.Term.ct0 (String.nil.) orig)) = (Maybe.some "")
|
||||
(Kind.Term.show.sugar.string.go (Kind.Term.ct2 (String.cons.) orig (Kind.Term.num orig1 x0) x1)) = (Maybe.bind (Kind.Term.show.sugar.string.go x1) @tail (Maybe.pure (String.cons x0 tail)))
|
||||
(Kind.Term.show.sugar.string.go other) = (Maybe.none)
|
||||
|
||||
// Kind.Term.show.sugar.string (term: (Kind.Term)) : (Maybe (String))
|
||||
(Kind.Term.show.sugar.string term) = (Maybe.bind (Kind.Term.show.sugar.string.go term) @res let quot = (String.cons 39 ""); (Maybe.pure (Kind.Printer.text (List.cons quot (List.cons res (List.cons quot (List.nil)))))))
|
||||
|
||||
// Maybe.pure -(a: Type) (x: a) : (Maybe a)
|
||||
(Maybe.pure x) = (Maybe.some x)
|
||||
|
||||
// Maybe.bind -(a: Type) -(b: Type) (ma: (Maybe a)) (mb: (_: a) (Maybe b)) : (Maybe b)
|
||||
(Maybe.bind (Maybe.none) mb) = (Maybe.none)
|
||||
(Maybe.bind (Maybe.some val) mb) = (mb val)
|
||||
|
||||
// Kind.Term.show.sugar.list.go (term: (Kind.Term)) : (Maybe (List (String)))
|
||||
(Kind.Term.show.sugar.list.go (Kind.Term.ct0 (List.nil.) orig)) = (Maybe.some (List.nil))
|
||||
(Kind.Term.show.sugar.list.go (Kind.Term.ct2 (List.cons.) orig x0 x1)) = (Maybe.bind (Kind.Term.show.sugar.list.go x1) @tail (Maybe.pure (List.cons (Kind.Term.show x0) tail)))
|
||||
@ -271,10 +258,6 @@
|
||||
// String.intercalate (sep: (String)) (xs: (List (String))) : (String)
|
||||
(String.intercalate sep xs) = (String.flatten (List.intersperse sep xs))
|
||||
|
||||
// String.flatten (xs: (List (String))) : (String)
|
||||
(String.flatten (List.nil)) = ""
|
||||
(String.flatten (List.cons head tail)) = (String.concat head (String.flatten tail))
|
||||
|
||||
// List.intersperse -(a: Type) (sep: a) (xs: (List a)) : (List a)
|
||||
(List.intersperse sep (List.nil)) = (List.nil)
|
||||
(List.intersperse sep (List.cons xh (List.nil))) = (List.pure xh)
|
||||
@ -283,6 +266,35 @@
|
||||
// List.pure -(t: Type) (x: t) : (List t)
|
||||
(List.pure x) = (List.cons x (List.nil))
|
||||
|
||||
// String.flatten (xs: (List (String))) : (String)
|
||||
(String.flatten (List.nil)) = ""
|
||||
(String.flatten (List.cons head tail)) = (String.concat head (String.flatten tail))
|
||||
|
||||
// U60.show (n: U60) : (Show)
|
||||
(U60.show 0) = @str (String.cons 48 str)
|
||||
(U60.show n) = @str let next = (String.cons (+ 48 (% n 10)) str); let func = (U60.if (< n 10) @h h @h ((U60.show (/ n 10)) h)); (func next)
|
||||
|
||||
// String.new_line : (String)
|
||||
(String.new_line) = (String.pure (Char.newline))
|
||||
|
||||
// String.pure (x: (Char)) : (String)
|
||||
(String.pure x) = (String.cons x "")
|
||||
|
||||
// Char : Type
|
||||
(Char) = 0
|
||||
|
||||
// Char.newline : (Char)
|
||||
(Char.newline) = 10
|
||||
|
||||
// U60.to_nat (x: U60) : (Nat)
|
||||
(U60.to_nat 0) = (Nat.zero)
|
||||
(U60.to_nat n) = (Nat.succ (U60.to_nat (- n 1)))
|
||||
|
||||
// String.pad_right (size: (Nat)) (chr: (Char)) (str: (String)) : (String)
|
||||
(String.pad_right (Nat.zero) chr str) = str
|
||||
(String.pad_right (Nat.succ sp) chr "") = (String.cons chr (String.pad_right sp chr ""))
|
||||
(String.pad_right (Nat.succ sp) chr (String.cons x xs)) = (String.cons x (String.pad_right sp chr xs))
|
||||
|
||||
// Kind.Context.max_name_length.aux (ctx: (Kind.Context)) (acc: U60) : U60
|
||||
(Kind.Context.max_name_length.aux (Kind.Context.empty) acc) = acc
|
||||
(Kind.Context.max_name_length.aux (Kind.Context.entry name type vals rest) acc) = (Kind.Context.max_name_length.aux rest (U60.max (Nat.to_u60 (String.length (Kind.Name.show name))) acc))
|
||||
@ -290,6 +302,10 @@
|
||||
// Kind.Context.max_name_length (ctx: (Kind.Context)) : U60
|
||||
(Kind.Context.max_name_length ctx) = (Kind.Context.max_name_length.aux ctx 0)
|
||||
|
||||
// Nat.to_u60 (n: (Nat)) : U60
|
||||
(Nat.to_u60 (Nat.zero)) = 0
|
||||
(Nat.to_u60 (Nat.succ n)) = (+ 1 (Nat.to_u60 n))
|
||||
|
||||
// String.length (xs: (String)) : (Nat)
|
||||
(String.length "") = (Nat.zero)
|
||||
(String.length (String.cons x xs)) = (Nat.succ (String.length xs))
|
||||
@ -297,19 +313,6 @@
|
||||
// U60.max (fst: U60) (snd: U60) : U60
|
||||
(U60.max fst snd) = (U60.if (> fst snd) fst snd)
|
||||
|
||||
// Nat.to_u60 (n: (Nat)) : U60
|
||||
(Nat.to_u60 (Nat.zero)) = 0
|
||||
(Nat.to_u60 (Nat.succ n)) = (+ 1 (Nat.to_u60 n))
|
||||
|
||||
// String.new_line : (String)
|
||||
(String.new_line) = (String.pure (Char.newline))
|
||||
|
||||
// Char.newline : (Char)
|
||||
(Char.newline) = 10
|
||||
|
||||
// String.pure (x: (Char)) : (String)
|
||||
(String.pure x) = (String.cons x "")
|
||||
|
||||
// String.cut.go (str: (String)) (df: (String)) (n: U60) : (String)
|
||||
(String.cut.go "" df n) = ""
|
||||
(String.cut.go (String.cons x xs) df 0) = df
|
||||
@ -325,16 +328,16 @@
|
||||
// Pair.match -(a: Type) -(b: Type) (x: (Pair a b)) -(p: (x: (Pair a b)) Type) (new: (fst: a) (snd: b) (p (Pair.new a b fst snd))) : (p x)
|
||||
(Pair.match (Pair.new fst_ snd_) new) = ((new fst_) snd_)
|
||||
|
||||
// Kind.Context.is_empty (ctx: (Kind.Context)) : (Bool)
|
||||
(Kind.Context.is_empty (Kind.Context.empty)) = (Bool.true)
|
||||
(Kind.Context.is_empty (Kind.Context.entry name type vals rest)) = (Bool.false)
|
||||
|
||||
// Pair.fst -(a: Type) -(b: Type) (pair: (Pair a b)) : a
|
||||
(Pair.fst (Pair.new fst snd)) = fst
|
||||
|
||||
// Pair.snd -(a: Type) -(b: Type) (pair: (Pair a b)) : b
|
||||
(Pair.snd (Pair.new fst snd)) = snd
|
||||
|
||||
// Kind.Context.is_empty (ctx: (Kind.Context)) : (Bool)
|
||||
(Kind.Context.is_empty (Kind.Context.empty)) = (Bool.true)
|
||||
(Kind.Context.is_empty (Kind.Context.entry name type vals rest)) = (Bool.false)
|
||||
|
||||
// List.reverse -(a: Type) (xs: (List a)) : (List a)
|
||||
(List.reverse xs) = (List.reverse.go xs (List.nil))
|
||||
|
||||
@ -357,232 +360,6 @@
|
||||
(Kind.API.check_function.rules (List.nil) type) = (List.nil)
|
||||
(Kind.API.check_function.rules (List.cons rule rules) type) = let head = (Kind.Checker.run (Kind.Checker.unify (Kind.Checker.rule rule type)) (Bool.false)); let tail = (Kind.API.check_function.rules rules type); (List.cons head tail)
|
||||
|
||||
// Kind.Checker.rule (rule: (Kind.Rule)) (term: (Kind.Term)) : (Kind.Checker (Unit))
|
||||
(Kind.Checker.rule (Kind.Rule.lhs arg args) (Kind.Term.all orig name type body)) = (Kind.Checker.bind (Kind.Checker.check arg type) @_ (Kind.Checker.bind (Kind.Checker.rule args (body arg)) @_ (Kind.Checker.pure (Unit.new))))
|
||||
(Kind.Checker.rule (Kind.Rule.lhs arg args) other) = (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.fail (Kind.Error.too_many_arguments ctx (Kind.Term.get_origin arg @orig @term orig))))
|
||||
(Kind.Checker.rule (Kind.Rule.rhs expr) type) = (Kind.Checker.bind (Kind.Checker.set_right_hand_side (Bool.true)) @_ (Kind.Checker.bind (Kind.Checker.check expr type) @_ (Kind.Checker.pure (Unit.new))))
|
||||
|
||||
// Kind.Checker.check (term: (Kind.Term)) (type: (Kind.Term)) : (Kind.Checker (Unit))
|
||||
(Kind.Checker.check (Kind.Term.lam orig name body) type) = (Kind.Checker.bind (Kind.Checker.get_subst) @subst let fun = (Kind.Term.if_all type @t_orig @t_name @t_type @t_body @orig @name @body (Kind.Checker.bind (Kind.Checker.get_depth) @dep (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.check (body (Kind.Term.var orig name dep)) (t_body (Kind.Term.var t_orig t_name dep))) name t_type (List.nil)) @chk (Kind.Checker.pure (Unit.new)))) @orig @name @body (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.fail (Kind.Error.cant_infer_lambda ctx orig)))); (((fun orig) name) body))
|
||||
(Kind.Checker.check (Kind.Term.let orig name expr body) type) = (Kind.Checker.bind (Kind.Checker.get_depth) @dep (Kind.Checker.bind (Kind.Checker.infer expr) @expr_typ (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.check (body (Kind.Term.var orig name dep)) type) name expr_typ (List.cons (Kind.Term.eval expr) (List.nil))) @body_chk (Kind.Checker.pure (Unit.new)))))
|
||||
(Kind.Checker.check (Kind.Term.hlp orig) type) = (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.bind (Kind.Checker.error (Kind.Error.inspection ctx orig type) (Unit.new)) @_ (Kind.Checker.pure (Unit.new))))
|
||||
(Kind.Checker.check (Kind.Term.var orig name idx) type) = (Kind.Checker.bind (Kind.Checker.get_right_hand_side) @rhs (Bool.if rhs (Kind.Checker.compare rhs (Kind.Term.var orig name idx) type) (Kind.Checker.extend name type (List.nil))))
|
||||
(Kind.Checker.check (Kind.Term.hol orig numb) type) = (Kind.Checker.pure (Unit.new))
|
||||
(Kind.Checker.check term type) = (Kind.Checker.bind (Kind.Checker.get_right_hand_side) @rhs (Kind.Checker.compare rhs term type))
|
||||
|
||||
// Kind.Checker.compare (rhs: (Bool)) (term: (Kind.Term)) (type: (Kind.Term)) : (Kind.Checker (Unit))
|
||||
(Kind.Checker.compare rhs term type) = (Kind.Term.get_origin term @orig @term (Kind.Checker.bind (Kind.Checker.infer term) @term_typ let fun = (Bool.if rhs @term_typ @type (Kind.Checker.new_equation orig type term_typ) @term_typ @type (Kind.Checker.bind (Kind.Checker.equal (Kind.Term.eval term_typ) (Kind.Term.eval type)) @is_equal (Bool.if is_equal (Kind.Checker.pure (Unit.new)) (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.fail (Kind.Error.impossible_case ctx orig type term_typ)))))); ((fun term_typ) type)))
|
||||
|
||||
// Kind.Checker.extended -(a: Type) (checker: (Kind.Checker a)) (name: U60) (type: (Kind.Term)) (vals: (List (Kind.Term))) : (Kind.Checker a)
|
||||
(Kind.Checker.extended checker name type vals) = (Kind.Checker.bind (Kind.Checker.extend name type vals) @_ (Kind.Checker.bind checker @got (Kind.Checker.bind (Kind.Checker.shrink) @_ (Kind.Checker.pure got))))
|
||||
|
||||
// Kind.Checker.extend (name: U60) (type: (Kind.Term)) (vals: (List (Kind.Term))) : (Kind.Checker (Unit))
|
||||
(Kind.Checker.extend name type vals) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked (Kind.Context.extend context name type vals) (+ depth 1) rhs subst eqts errs (Unit.new))
|
||||
|
||||
// Kind.Context.extend (prev: (Kind.Context)) (name: U60) (term: (Kind.Term)) (ls: (List (Kind.Term))) : (Kind.Context)
|
||||
(Kind.Context.extend (Kind.Context.empty) name type values) = (Kind.Context.entry name type values (Kind.Context.empty))
|
||||
(Kind.Context.extend (Kind.Context.entry n t v rest) name type values) = (Kind.Context.entry n t v (Kind.Context.extend rest name type values))
|
||||
|
||||
// Kind.Checker (a: Type) : Type
|
||||
(Kind.Checker a) = 0
|
||||
|
||||
// Kind.Checker.bind.result -(a: Type) -(b: Type) (result: (Kind.Result a)) (then: (_: a) (Kind.Checker b)) : (Kind.Result b)
|
||||
(Kind.Checker.bind.result (Kind.Result.checked context depth rhs sub equations errs ret) then) = (((((((then ret) context) depth) rhs) sub) equations) errs)
|
||||
(Kind.Checker.bind.result (Kind.Result.errored context sub errs) then) = (Kind.Result.errored context sub errs)
|
||||
|
||||
// Kind.Checker.bind -(a: Type) -(b: Type) (checker: (Kind.Checker a)) (then: (_: a) (Kind.Checker b)) : (Kind.Checker b)
|
||||
(Kind.Checker.bind checker then) = @context @depth @rhs @subst @eqts @errs (Kind.Checker.bind.result ((((((checker context) depth) rhs) subst) eqts) errs) then)
|
||||
|
||||
// Kind.Checker.shrink : (Kind.Checker (Unit))
|
||||
(Kind.Checker.shrink) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked (Kind.Context.shrink context) (- depth 1) rhs subst eqts errs (Unit.new))
|
||||
|
||||
// Kind.Context.shrink (ctx: (Kind.Context)) : (Kind.Context)
|
||||
(Kind.Context.shrink (Kind.Context.empty)) = (Kind.Context.empty)
|
||||
(Kind.Context.shrink (Kind.Context.entry name type vals (Kind.Context.empty))) = (Kind.Context.empty)
|
||||
(Kind.Context.shrink (Kind.Context.entry name type vals rest)) = (Kind.Context.entry name type vals (Kind.Context.shrink rest))
|
||||
|
||||
// Kind.Checker.pure -(t: Type) (a: t) : (Kind.Checker t)
|
||||
(Kind.Checker.pure res) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs res)
|
||||
|
||||
// Kind.Checker.get_subst : (Kind.Checker (Kind.Subst))
|
||||
(Kind.Checker.get_subst) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs subst)
|
||||
|
||||
// Kind.Checker.equal (left: (Kind.Term)) (right: (Kind.Term)) : (Kind.Checker (Bool))
|
||||
(Kind.Checker.equal (Kind.Term.typ orig) (Kind.Term.typ orig1)) = (Kind.Checker.pure (Bool.true))
|
||||
(Kind.Checker.equal (Kind.Term.all a.orig a.name a.type a.body) (Kind.Term.all b.orig b.name b.type b.body)) = (Kind.Checker.bind (Kind.Checker.get_depth) @dep (Kind.Checker.bind (Kind.Checker.equal a.type b.type) @type (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.equal (a.body (Kind.Term.var a.orig a.name dep)) (b.body (Kind.Term.var b.orig b.name dep))) (Null) (Null) (List.nil)) @body (Kind.Checker.pure (Bool.and type body)))))
|
||||
(Kind.Checker.equal (Kind.Term.lam a.orig a.name a.body) (Kind.Term.lam b.orig b.name b.body)) = (Kind.Checker.bind (Kind.Checker.get_depth) @dep (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.equal (a.body (Kind.Term.var a.orig a.name dep)) (b.body (Kind.Term.var b.orig b.name dep))) (Null) (Null) (List.nil)) @body (Kind.Checker.pure body)))
|
||||
(Kind.Checker.equal (Kind.Term.app a.orig a.func a.argm) (Kind.Term.app b.orig b.func b.argm)) = (Kind.Checker.bind (Kind.Checker.equal a.func b.func) @func (Kind.Checker.bind (Kind.Checker.equal a.argm b.argm) @argm (Kind.Checker.pure (Bool.and func argm))))
|
||||
(Kind.Checker.equal (Kind.Term.let a.orig a.name a.expr a.body) (Kind.Term.let b.orig b.name b.expr b.body)) = (Kind.Checker.bind (Kind.Checker.get_depth) @dep (Kind.Checker.bind (Kind.Checker.equal a.expr b.expr) @expr (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.equal (a.body (Kind.Term.var a.orig a.name dep)) (b.body (Kind.Term.var b.orig b.name dep))) (Null) (Null) (List.nil)) @body (Kind.Checker.pure (Bool.and expr body)))))
|
||||
(Kind.Checker.equal (Kind.Term.ann a.orig a.expr a.type) (Kind.Term.ann b.orig b.expr b.type)) = (Kind.Checker.bind (Kind.Checker.equal a.expr b.expr) @func (Kind.Checker.bind (Kind.Checker.equal a.type b.type) @arg (Kind.Checker.pure (Bool.and func arg))))
|
||||
(Kind.Checker.equal (Kind.Term.u60 a.orig) (Kind.Term.u60 b.orig)) = (Kind.Checker.pure (Bool.true))
|
||||
(Kind.Checker.equal (Kind.Term.num a.orig a.num) (Kind.Term.num b.orig b.num)) = (Kind.Checker.pure (U60.equal a.num b.num))
|
||||
(Kind.Checker.equal (Kind.Term.op2 a.orig a.op a.val0 a.val1) (Kind.Term.op2 b.orig b.op b.val0 b.val1)) = let op = (Kind.Operator.equal a.op b.op); (Kind.Checker.bind (Kind.Checker.equal a.val0 b.val0) @val0 (Kind.Checker.bind (Kind.Checker.equal a.val1 b.val1) @val1 (Kind.Checker.pure (Bool.and op (Bool.and val0 val1)))))
|
||||
(Kind.Checker.equal (Kind.Term.hol a.orig a.numb) (Kind.Term.hol b.orig b.numb)) = (Bool.if (U60.equal a.numb b.numb) (Kind.Checker.pure (Bool.true)) (Kind.Checker.equal.hol a.orig a.numb (Kind.Term.hol b.orig b.numb)))
|
||||
(Kind.Checker.equal (Kind.Term.hol a.orig a.numb) b) = (Kind.Checker.equal.hol a.orig a.numb b)
|
||||
(Kind.Checker.equal b (Kind.Term.hol a.orig a.numb)) = (Kind.Checker.equal.hol a.orig a.numb b)
|
||||
(Kind.Checker.equal (Kind.Term.var a.orig a.name a.idx) b) = (Kind.Checker.bind (Kind.Checker.get_right_hand_side) @rhs (Kind.Checker.equal.var rhs a.orig a.name a.idx b))
|
||||
(Kind.Checker.equal b (Kind.Term.var a.orig a.name a.idx)) = (Kind.Checker.bind (Kind.Checker.get_right_hand_side) @rhs (Kind.Checker.equal.var rhs a.orig a.name a.idx b))
|
||||
(Kind.Checker.equal (Kind.Term.ct0 a.ctid a.orig) (Kind.Term.ct0 b.ctid b.orig)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.pure ctid)
|
||||
(Kind.Checker.equal (Kind.Term.ct1 a.ctid a.orig a.x0) (Kind.Term.ct1 b.ctid b.orig b.x0)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.pure (Bool.and ctid x0)))
|
||||
(Kind.Checker.equal (Kind.Term.ct2 a.ctid a.orig a.x0 a.x1) (Kind.Term.ct2 b.ctid b.orig b.x0 b.x1)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 x1)))))
|
||||
(Kind.Checker.equal (Kind.Term.ct3 a.ctid a.orig a.x0 a.x1 a.x2) (Kind.Term.ct3 b.ctid b.orig b.x0 b.x1 b.x2)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 x2)))))))
|
||||
(Kind.Checker.equal (Kind.Term.ct4 a.ctid a.orig a.x0 a.x1 a.x2 a.x3) (Kind.Term.ct4 b.ctid b.orig b.x0 b.x1 b.x2 b.x3)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 x3)))))))))
|
||||
(Kind.Checker.equal (Kind.Term.ct5 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4) (Kind.Term.ct5 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.bind (Kind.Checker.equal a.x4 b.x4) @x4 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 x4)))))))))))
|
||||
(Kind.Checker.equal (Kind.Term.ct6 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5) (Kind.Term.ct6 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.bind (Kind.Checker.equal a.x4 b.x4) @x4 (Kind.Checker.bind (Kind.Checker.equal a.x5 b.x5) @x5 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 x5)))))))))))))
|
||||
(Kind.Checker.equal (Kind.Term.ct7 a.ctid a.orig a.args) (Kind.Term.ct7 b.ctid b.orig b.args)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.args b.args) @xargs (Kind.Checker.pure (Bool.and ctid xargs)))
|
||||
(Kind.Checker.equal (Kind.Term.ct8 a.ctid a.orig a.args) (Kind.Term.ct8 b.ctid b.orig b.args)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.args b.args) @xargs (Kind.Checker.pure (Bool.and ctid xargs)))
|
||||
(Kind.Checker.equal (Kind.Term.args7 a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6) (Kind.Term.args7 b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6)) = (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.bind (Kind.Checker.equal a.x4 b.x4) @x4 (Kind.Checker.bind (Kind.Checker.equal a.x5 b.x5) @x5 (Kind.Checker.bind (Kind.Checker.equal a.x6 b.x6) @x6 (Kind.Checker.pure (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 x6))))))))))))))
|
||||
(Kind.Checker.equal (Kind.Term.args8 a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7) (Kind.Term.args8 b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7)) = (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.bind (Kind.Checker.equal a.x4 b.x4) @x4 (Kind.Checker.bind (Kind.Checker.equal a.x5 b.x5) @x5 (Kind.Checker.bind (Kind.Checker.equal a.x6 b.x6) @x6 (Kind.Checker.bind (Kind.Checker.equal a.x7 b.x7) @x7 (Kind.Checker.pure (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 x7))))))))))))))))
|
||||
(Kind.Checker.equal (Kind.Term.fn0 a.ctid a.orig) (Kind.Term.fn0 b.ctid b.orig)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.pure ctid)
|
||||
(Kind.Checker.equal (Kind.Term.fn1 a.ctid a.orig a.x0) (Kind.Term.fn1 b.ctid b.orig b.x0)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.pure (Bool.and ctid x0)))
|
||||
(Kind.Checker.equal (Kind.Term.fn2 a.ctid a.orig a.x0 a.x1) (Kind.Term.fn2 b.ctid b.orig b.x0 b.x1)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 x1)))))
|
||||
(Kind.Checker.equal (Kind.Term.fn3 a.ctid a.orig a.x0 a.x1 a.x2) (Kind.Term.fn3 b.ctid b.orig b.x0 b.x1 b.x2)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 x2)))))))
|
||||
(Kind.Checker.equal (Kind.Term.fn4 a.ctid a.orig a.x0 a.x1 a.x2 a.x3) (Kind.Term.fn4 b.ctid b.orig b.x0 b.x1 b.x2 b.x3)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 x3)))))))))
|
||||
(Kind.Checker.equal (Kind.Term.fn5 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4) (Kind.Term.fn5 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.bind (Kind.Checker.equal a.x4 b.x4) @x4 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 x4)))))))))))
|
||||
(Kind.Checker.equal (Kind.Term.fn6 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5) (Kind.Term.fn6 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.bind (Kind.Checker.equal a.x4 b.x4) @x4 (Kind.Checker.bind (Kind.Checker.equal a.x5 b.x5) @x5 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 x5)))))))))))))
|
||||
(Kind.Checker.equal (Kind.Term.fn7 a.ctid a.orig a.args) (Kind.Term.fn7 b.ctid b.orig b.args)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.args b.args) @xargs (Kind.Checker.pure (Bool.and ctid xargs)))
|
||||
(Kind.Checker.equal (Kind.Term.fn8 a.ctid a.orig a.args) (Kind.Term.fn8 b.ctid b.orig b.args)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.args b.args) @xargs (Kind.Checker.pure (Bool.and ctid xargs)))
|
||||
(Kind.Checker.equal a b) = (Kind.Checker.bind (Kind.Checker.get_subst) @sub (Bool.if (Bool.or (Kind.Term.fillable a sub) (Kind.Term.fillable b sub)) (Kind.Checker.equal (Kind.Term.fill a sub) (Kind.Term.fill b sub)) (Kind.Checker.pure (Bool.false))))
|
||||
|
||||
// Kind.Checker.equal.var (rhs: (Bool)) (orig: U60) (name: U60) (idx: U60) (b: (Kind.Term)) : (Kind.Checker (Bool))
|
||||
(Kind.Checker.equal.var (Bool.false) orig name idx b) = (Kind.Checker.bind (Kind.Checker.add_value idx b) @_ (Kind.Checker.pure (Bool.true)))
|
||||
(Kind.Checker.equal.var (Bool.true) a.orig a.name a.idx (Kind.Term.var b.orig b.name b.idx)) = (Bool.if (U60.equal a.idx b.idx) (Kind.Checker.pure (Bool.true)) (Kind.Checker.bind (Kind.Checker.find a.idx (List.nil) @n @t @v v) @a.val (Kind.Checker.bind (Kind.Checker.find b.idx (List.nil) @n @t @v v) @b.val (Kind.Checker.bind (Kind.Checker.equal.var.try_values a.val (Kind.Term.var b.orig b.name b.idx)) @a.chk (Kind.Checker.bind (Kind.Checker.equal.var.try_values b.val (Kind.Term.var a.orig a.name a.idx)) @b.chk (Kind.Checker.pure (Bool.or a.chk b.chk)))))))
|
||||
(Kind.Checker.equal.var (Bool.true) a.orig a.name a.idx b) = (Kind.Checker.bind (Kind.Checker.get_subst) @sub (Bool.if (Kind.Term.fillable b sub) (Kind.Checker.equal (Kind.Term.var a.orig a.name a.idx) (Kind.Term.fill b sub)) (Kind.Checker.bind (Kind.Checker.find a.idx (List.nil) @n @t @v v) @a.val (Kind.Checker.bind (Kind.Checker.equal.var.try_values a.val b) @res (Kind.Checker.pure res)))))
|
||||
|
||||
// Kind.Checker.equal.var.try_values (ls: (List (Kind.Term))) (term: (Kind.Term)) : (Kind.Checker (Bool))
|
||||
(Kind.Checker.equal.var.try_values (List.nil) term) = (Kind.Checker.pure (Bool.false))
|
||||
(Kind.Checker.equal.var.try_values (List.cons x xs) term) = (Kind.Checker.bind (Kind.Checker.equal x term) @head (Bool.if head (Kind.Checker.pure (Bool.true)) (Kind.Checker.equal.var.try_values xs term)))
|
||||
|
||||
// Kind.Checker.equal.hol (orig: U60) (numb: U60) (b: (Kind.Term)) : (Kind.Checker (Bool))
|
||||
(Kind.Checker.equal.hol a.orig a.numb b) = (Kind.Checker.bind (Kind.Checker.look a.numb) @got (Kind.Checker.bind (Kind.Checker.equal.hol.val got a.orig a.numb b) @res (Kind.Checker.pure res)))
|
||||
|
||||
// Kind.Checker.equal.hol.val (val: (Maybe (Kind.Term))) (orig: U60) (numb: U60) (b: (Kind.Term)) : (Kind.Checker (Bool))
|
||||
(Kind.Checker.equal.hol.val (Maybe.none) orig numb b) = (Kind.Checker.bind (Kind.Checker.fill numb b) @_ (Kind.Checker.pure (Bool.true)))
|
||||
(Kind.Checker.equal.hol.val (Maybe.some val) orig numb b) = (Kind.Checker.equal val b)
|
||||
|
||||
// Kind.Checker.get_right_hand_side : (Kind.Checker (Bool))
|
||||
(Kind.Checker.get_right_hand_side) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs rhs)
|
||||
|
||||
// Kind.Checker.find -(r: Type) (index: U60) (alt: r) (fun: (_: U60) (_: (Kind.Term)) (_: (List (Kind.Term))) r) : (Kind.Checker r)
|
||||
(Kind.Checker.find index alt fun) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs (Kind.Context.find context index alt fun))
|
||||
|
||||
// Kind.Context.find -(res: Type) (ctx: (Kind.Context)) (name: U60) (alt: res) (fun: (_: U60) (_: (Kind.Term)) (_: (List (Kind.Term))) res) : res
|
||||
(Kind.Context.find (Kind.Context.entry name type vals rest) 0 alt fun) = (((fun name) type) vals)
|
||||
(Kind.Context.find (Kind.Context.entry name type vals rest) n alt fun) = (Kind.Context.find rest (- n 1) alt fun)
|
||||
(Kind.Context.find (Kind.Context.empty) n alt fun) = alt
|
||||
|
||||
// Kind.Checker.fill (index: U60) (val: (Kind.Term)) : (Kind.Checker (Unit))
|
||||
(Kind.Checker.fill index val) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs (Kind.Subst.fill subst index val) eqts errs (Unit.new))
|
||||
|
||||
// Kind.Subst.fill (subst: (Kind.Subst)) (depth: U60) (term: (Kind.Term)) : (Kind.Subst)
|
||||
(Kind.Subst.fill (Kind.Subst.end) 0 term) = (Kind.Subst.sub term (Kind.Subst.end))
|
||||
(Kind.Subst.fill (Kind.Subst.unfilled rest) 0 term) = (Kind.Subst.sub term rest)
|
||||
(Kind.Subst.fill (Kind.Subst.sub lost rest) 0 term) = (Kind.Subst.sub term rest)
|
||||
(Kind.Subst.fill (Kind.Subst.end) n term) = (Kind.Subst.unfilled (Kind.Subst.fill (Kind.Subst.end) (- n 1) term))
|
||||
(Kind.Subst.fill (Kind.Subst.unfilled rest) n term) = (Kind.Subst.unfilled (Kind.Subst.fill rest (- n 1) term))
|
||||
(Kind.Subst.fill (Kind.Subst.sub keep rest) n term) = (Kind.Subst.sub keep (Kind.Subst.fill rest (- n 1) term))
|
||||
|
||||
// Bool.or (a: (Bool)) (b: (Bool)) : (Bool)
|
||||
(Bool.or (Bool.true) b) = (Bool.true)
|
||||
(Bool.or (Bool.false) b) = b
|
||||
|
||||
// Kind.Term.fillable (term: (Kind.Term)) (sub: (Kind.Subst)) : (Bool)
|
||||
(Kind.Term.fillable term (Kind.Subst.end)) = (Bool.false)
|
||||
(Kind.Term.fillable (Kind.Term.typ orig) sub) = (Bool.false)
|
||||
(Kind.Term.fillable (Kind.Term.var orig name index) sub) = (Bool.false)
|
||||
(Kind.Term.fillable (Kind.Term.hlp orig) sub) = (Bool.false)
|
||||
(Kind.Term.fillable (Kind.Term.u60 orig) sub) = (Bool.false)
|
||||
(Kind.Term.fillable (Kind.Term.num orig num) sub) = (Bool.false)
|
||||
(Kind.Term.fillable (Kind.Term.all orig name typ body) sub) = (Bool.or (Kind.Term.fillable typ sub) (Kind.Term.fillable (body (Kind.Term.hlp 0)) sub))
|
||||
(Kind.Term.fillable (Kind.Term.lam orig name body) sub) = (Kind.Term.fillable (body (Kind.Term.hlp 0)) sub)
|
||||
(Kind.Term.fillable (Kind.Term.app orig expr typ) sub) = (Bool.or (Kind.Term.fillable expr sub) (Kind.Term.fillable typ sub))
|
||||
(Kind.Term.fillable (Kind.Term.let orig name expr body) sub) = (Bool.or (Kind.Term.fillable expr sub) (Kind.Term.fillable (body (Kind.Term.hlp 0)) sub))
|
||||
(Kind.Term.fillable (Kind.Term.ann orig expr typ) sub) = (Bool.or (Kind.Term.fillable expr sub) (Kind.Term.fillable typ sub))
|
||||
(Kind.Term.fillable (Kind.Term.op2 orig op left right) sub) = (Bool.or (Kind.Term.fillable left sub) (Kind.Term.fillable right sub))
|
||||
(Kind.Term.fillable (Kind.Term.hol orig numb) sub) = (Maybe.is_some (Kind.Subst.look sub numb))
|
||||
(Kind.Term.fillable (Kind.Term.ct0 ctid orig) sub) = (Bool.false)
|
||||
(Kind.Term.fillable (Kind.Term.ct1 ctid orig x0) sub) = (Kind.Term.fillable x0 sub)
|
||||
(Kind.Term.fillable (Kind.Term.ct2 ctid orig x0 x1) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Kind.Term.fillable x1 sub))
|
||||
(Kind.Term.fillable (Kind.Term.ct3 ctid orig x0 x1 x2) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Kind.Term.fillable x2 sub)))
|
||||
(Kind.Term.fillable (Kind.Term.ct4 ctid orig x0 x1 x2 x3) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Bool.or (Kind.Term.fillable x2 sub) (Kind.Term.fillable x3 sub))))
|
||||
(Kind.Term.fillable (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Bool.or (Kind.Term.fillable x2 sub) (Bool.or (Kind.Term.fillable x3 sub) (Kind.Term.fillable x4 sub)))))
|
||||
(Kind.Term.fillable (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Bool.or (Kind.Term.fillable x2 sub) (Bool.or (Kind.Term.fillable x3 sub) (Bool.or (Kind.Term.fillable x4 sub) (Kind.Term.fillable x5 sub))))))
|
||||
(Kind.Term.fillable (Kind.Term.ct7 fnid orig args) sub) = (Kind.Term.fillable args sub)
|
||||
(Kind.Term.fillable (Kind.Term.ct8 fnid orig args) sub) = (Kind.Term.fillable args sub)
|
||||
(Kind.Term.fillable (Kind.Term.fn0 fnid orig) sub) = (Bool.false)
|
||||
(Kind.Term.fillable (Kind.Term.fn1 fnid orig x0) sub) = (Kind.Term.fillable x0 sub)
|
||||
(Kind.Term.fillable (Kind.Term.fn2 fnid orig x0 x1) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Kind.Term.fillable x1 sub))
|
||||
(Kind.Term.fillable (Kind.Term.fn3 fnid orig x0 x1 x2) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Kind.Term.fillable x2 sub)))
|
||||
(Kind.Term.fillable (Kind.Term.fn4 fnid orig x0 x1 x2 x3) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Bool.or (Kind.Term.fillable x2 sub) (Kind.Term.fillable x3 sub))))
|
||||
(Kind.Term.fillable (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Bool.or (Kind.Term.fillable x2 sub) (Bool.or (Kind.Term.fillable x3 sub) (Kind.Term.fillable x4 sub)))))
|
||||
(Kind.Term.fillable (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Bool.or (Kind.Term.fillable x2 sub) (Bool.or (Kind.Term.fillable x3 sub) (Bool.or (Kind.Term.fillable x4 sub) (Kind.Term.fillable x5 sub))))))
|
||||
(Kind.Term.fillable (Kind.Term.fn7 fnid orig args) sub) = (Kind.Term.fillable args sub)
|
||||
(Kind.Term.fillable (Kind.Term.fn8 fnid orig args) sub) = (Kind.Term.fillable args sub)
|
||||
(Kind.Term.fillable (Kind.Term.args7 x0 x1 x2 x3 x4 x5 x6) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Bool.or (Kind.Term.fillable x2 sub) (Bool.or (Kind.Term.fillable x3 sub) (Bool.or (Kind.Term.fillable x4 sub) (Bool.or (Kind.Term.fillable x5 sub) (Kind.Term.fillable x6 sub)))))))
|
||||
(Kind.Term.fillable (Kind.Term.args8 x0 x1 x2 x3 x4 x5 x6 x7) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Bool.or (Kind.Term.fillable x2 sub) (Bool.or (Kind.Term.fillable x3 sub) (Bool.or (Kind.Term.fillable x4 sub) (Bool.or (Kind.Term.fillable x5 sub) (Bool.or (Kind.Term.fillable x6 sub) (Kind.Term.fillable x7 sub))))))))
|
||||
|
||||
// Maybe.is_some -(a: Type) (m: (Maybe a)) : (Bool)
|
||||
(Maybe.is_some (Maybe.none)) = (Bool.false)
|
||||
(Maybe.is_some (Maybe.some v)) = (Bool.true)
|
||||
|
||||
// Kind.Checker.look (index: U60) : (Kind.Checker (Maybe (Kind.Term)))
|
||||
(Kind.Checker.look index) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs (Kind.Subst.look subst index))
|
||||
|
||||
// Kind.Operator.equal (left: (Kind.Operator)) (right: (Kind.Operator)) : (Bool)
|
||||
(Kind.Operator.equal (Kind.Operator.and) (Kind.Operator.and)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.sub) (Kind.Operator.sub)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.mul) (Kind.Operator.mul)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.div) (Kind.Operator.div)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.mod) (Kind.Operator.mod)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.and) (Kind.Operator.and)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.or) (Kind.Operator.or)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.xor) (Kind.Operator.xor)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.shl) (Kind.Operator.shl)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.shr) (Kind.Operator.shr)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.ltn) (Kind.Operator.ltn)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.lte) (Kind.Operator.lte)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.eql) (Kind.Operator.eql)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.gte) (Kind.Operator.gte)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.gtn) (Kind.Operator.gtn)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.neq) (Kind.Operator.neq)) = (Bool.true)
|
||||
(Kind.Operator.equal a b) = (Bool.false)
|
||||
|
||||
// U60.equal (a: U60) (b: U60) : (Bool)
|
||||
(U60.equal a b) = (U60.to_bool (== a b))
|
||||
|
||||
// U60.to_bool (n: U60) : (Bool)
|
||||
(U60.to_bool 0) = (Bool.false)
|
||||
(U60.to_bool n) = (Bool.true)
|
||||
|
||||
// Kind.Checker.get_depth : (Kind.Checker U60)
|
||||
(Kind.Checker.get_depth) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs depth)
|
||||
|
||||
// Kind.Checker.add_value (idx: U60) (val: (Kind.Term)) : (Kind.Checker (Unit))
|
||||
(Kind.Checker.add_value idx val) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked (Kind.Context.add_value context idx val) depth rhs subst eqts errs (Unit.new))
|
||||
|
||||
// Kind.Context.add_value (prev: (Kind.Context)) (name: U60) (term: (Kind.Term)) : (Kind.Context)
|
||||
(Kind.Context.add_value (Kind.Context.entry name type vals rest) 0 val) = (Kind.Context.entry name type (List.cons val vals) rest)
|
||||
(Kind.Context.add_value (Kind.Context.entry name type vals rest) n val) = (Kind.Context.entry name type vals (Kind.Context.add_value rest (- n 1) val))
|
||||
(Kind.Context.add_value (Kind.Context.empty) n val) = (Kind.Context.empty)
|
||||
|
||||
// Bool.and (a: (Bool)) (b: (Bool)) : (Bool)
|
||||
(Bool.and (Bool.true) b) = b
|
||||
(Bool.and (Bool.false) b) = (Bool.false)
|
||||
|
||||
// Kind.Checker.new_equation (orig: U60) (left: (Kind.Term)) (right: (Kind.Term)) : (Kind.Checker (Unit))
|
||||
(Kind.Checker.new_equation orig left right) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst (List.append eqts (Kind.Equation.new context orig left right)) errs (Unit.new))
|
||||
|
||||
// List.append -(a: Type) (xs: (List a)) (x: a) : (List a)
|
||||
(List.append (List.nil) x) = (List.pure x)
|
||||
(List.append (List.cons xs.h xs.t) x) = (List.cons xs.h (List.append xs.t x))
|
||||
|
||||
// Kind.Checker.fail -(t: Type) (err: (Kind.Error)) : (Kind.Checker t)
|
||||
(Kind.Checker.fail err) = @context @depth @rhs @subst @eqts @errs (Kind.Result.errored context subst (List.cons err errs))
|
||||
|
||||
// Kind.Term.if_all -(res: Type) (term: (Kind.Term)) (if: (_: U60) (_: U60) (_: (Kind.Term)) (_: (_: (Kind.Term)) (Kind.Term)) res) (else: res) : res
|
||||
(Kind.Term.if_all (Kind.Term.all orig name typ body) func_if else) = ((((func_if orig) name) typ) body)
|
||||
(Kind.Term.if_all other func_if else) = else
|
||||
|
||||
// Kind.Term.eval (term: (Kind.Term)) : (Kind.Term)
|
||||
(Kind.Term.eval (Kind.Term.typ orig)) = (Kind.Term.typ orig)
|
||||
(Kind.Term.eval (Kind.Term.var orig name index)) = (Kind.Term.var orig name index)
|
||||
@ -636,6 +413,27 @@
|
||||
(Kind.Term.eval_op orig (Kind.Operator.neq) (Kind.Term.num a.orig a.num) (Kind.Term.num b.orig b.num)) = (Kind.Term.num 0 (!= a.num b.num))
|
||||
(Kind.Term.eval_op orig op left right) = (Kind.Term.op2 orig op left right)
|
||||
|
||||
// Kind.Checker.rule (rule: (Kind.Rule)) (term: (Kind.Term)) : (Kind.Checker (Unit))
|
||||
(Kind.Checker.rule (Kind.Rule.lhs arg args) (Kind.Term.all orig name type body)) = (Kind.Checker.bind (Kind.Checker.check arg type) @_ (Kind.Checker.bind (Kind.Checker.rule args (body arg)) @_ (Kind.Checker.pure (Unit.new))))
|
||||
(Kind.Checker.rule (Kind.Rule.lhs arg args) other) = (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.fail (Kind.Error.too_many_arguments ctx (Kind.Term.get_origin arg @orig @term orig))))
|
||||
(Kind.Checker.rule (Kind.Rule.rhs expr) type) = (Kind.Checker.bind (Kind.Checker.set_right_hand_side (Bool.true)) @_ (Kind.Checker.bind (Kind.Checker.check expr type) @_ (Kind.Checker.pure (Unit.new))))
|
||||
|
||||
// Kind.Checker.bind.result -(a: Type) -(b: Type) (result: (Kind.Result a)) (then: (_: a) (Kind.Checker b)) : (Kind.Result b)
|
||||
(Kind.Checker.bind.result (Kind.Result.checked context depth rhs sub equations errs ret) then) = (((((((then ret) context) depth) rhs) sub) equations) errs)
|
||||
(Kind.Checker.bind.result (Kind.Result.errored context sub errs) then) = (Kind.Result.errored context sub errs)
|
||||
|
||||
// Kind.Checker.bind -(a: Type) -(b: Type) (checker: (Kind.Checker a)) (then: (_: a) (Kind.Checker b)) : (Kind.Checker b)
|
||||
(Kind.Checker.bind checker then) = @context @depth @rhs @subst @eqts @errs (Kind.Checker.bind.result ((((((checker context) depth) rhs) subst) eqts) errs) then)
|
||||
|
||||
// Kind.Checker (a: Type) : Type
|
||||
(Kind.Checker a) = 0
|
||||
|
||||
// Kind.Checker.fail -(t: Type) (err: (Kind.Error)) : (Kind.Checker t)
|
||||
(Kind.Checker.fail err) = @context @depth @rhs @subst @eqts @errs (Kind.Result.errored context subst (List.cons err errs))
|
||||
|
||||
// Kind.Checker.pure -(t: Type) (a: t) : (Kind.Checker t)
|
||||
(Kind.Checker.pure res) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs res)
|
||||
|
||||
// Kind.Term.get_origin -(r: Type) (term: (Kind.Term)) (got: (_: U60) (_: (Kind.Term)) r) : r
|
||||
(Kind.Term.get_origin (Kind.Term.typ orig) got) = ((got orig) (Kind.Term.typ orig))
|
||||
(Kind.Term.get_origin (Kind.Term.var orig name index) got) = ((got orig) (Kind.Term.var orig name index))
|
||||
@ -668,12 +466,61 @@
|
||||
(Kind.Term.get_origin (Kind.Term.fn7 fnid orig args) got) = ((got orig) (Kind.Term.fn7 fnid orig args))
|
||||
(Kind.Term.get_origin (Kind.Term.fn8 fnid orig args) got) = ((got orig) (Kind.Term.fn8 fnid orig args))
|
||||
|
||||
// Kind.Checker.set_right_hand_side (rhs: (Bool)) : (Kind.Checker (Unit))
|
||||
(Kind.Checker.set_right_hand_side to_rhs) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth to_rhs subst eqts errs (Unit.new))
|
||||
|
||||
// Kind.Checker.get_context : (Kind.Checker (Kind.Context))
|
||||
(Kind.Checker.get_context) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs context)
|
||||
|
||||
// Kind.Checker.check (term: (Kind.Term)) (type: (Kind.Term)) : (Kind.Checker (Unit))
|
||||
(Kind.Checker.check (Kind.Term.lam orig name body) type) = (Kind.Checker.bind (Kind.Checker.get_subst) @subst let fun = (Kind.Term.if_all type @t_orig @t_name @t_type @t_body @orig @name @body (Kind.Checker.bind (Kind.Checker.get_depth) @dep (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.check (body (Kind.Term.var orig name dep)) (t_body (Kind.Term.var t_orig t_name dep))) name t_type (List.nil)) @chk (Kind.Checker.pure (Unit.new)))) @orig @name @body (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.fail (Kind.Error.cant_infer_lambda ctx orig)))); (((fun orig) name) body))
|
||||
(Kind.Checker.check (Kind.Term.let orig name expr body) type) = (Kind.Checker.bind (Kind.Checker.get_depth) @dep (Kind.Checker.bind (Kind.Checker.infer expr) @expr_typ (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.check (body (Kind.Term.var orig name dep)) type) name expr_typ (List.cons (Kind.Term.eval expr) (List.nil))) @body_chk (Kind.Checker.pure (Unit.new)))))
|
||||
(Kind.Checker.check (Kind.Term.hlp orig) type) = (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.bind (Kind.Checker.error (Kind.Error.inspection ctx orig type) (Unit.new)) @_ (Kind.Checker.pure (Unit.new))))
|
||||
(Kind.Checker.check (Kind.Term.var orig name idx) type) = (Kind.Checker.bind (Kind.Checker.get_right_hand_side) @rhs (Bool.if rhs (Kind.Checker.compare rhs (Kind.Term.var orig name idx) type) (Kind.Checker.extend name type (List.nil))))
|
||||
(Kind.Checker.check (Kind.Term.hol orig numb) type) = (Kind.Checker.pure (Unit.new))
|
||||
(Kind.Checker.check term type) = (Kind.Checker.bind (Kind.Checker.get_right_hand_side) @rhs (Kind.Checker.compare rhs term type))
|
||||
|
||||
// Kind.Checker.compare (rhs: (Bool)) (term: (Kind.Term)) (type: (Kind.Term)) : (Kind.Checker (Unit))
|
||||
(Kind.Checker.compare rhs term type) = (Kind.Term.get_origin term @orig @term (Kind.Checker.bind (Kind.Checker.infer term) @term_typ let fun = (Bool.if rhs @term_typ @type (Kind.Checker.new_equation orig type term_typ) @term_typ @type (Kind.Checker.bind (Kind.Checker.equal (Kind.Term.eval term_typ) (Kind.Term.eval type)) @is_equal (Bool.if is_equal (Kind.Checker.pure (Unit.new)) (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.fail (Kind.Error.impossible_case ctx orig type term_typ)))))); ((fun term_typ) type)))
|
||||
|
||||
// Kind.Checker.get_right_hand_side : (Kind.Checker (Bool))
|
||||
(Kind.Checker.get_right_hand_side) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs rhs)
|
||||
|
||||
// Kind.Checker.new_equation (orig: U60) (left: (Kind.Term)) (right: (Kind.Term)) : (Kind.Checker (Unit))
|
||||
(Kind.Checker.new_equation orig left right) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst (List.append eqts (Kind.Equation.new context orig left right)) errs (Unit.new))
|
||||
|
||||
// List.append -(a: Type) (xs: (List a)) (x: a) : (List a)
|
||||
(List.append (List.nil) x) = (List.pure x)
|
||||
(List.append (List.cons xs.h xs.t) x) = (List.cons xs.h (List.append xs.t x))
|
||||
|
||||
// Kind.Checker.extend (name: U60) (type: (Kind.Term)) (vals: (List (Kind.Term))) : (Kind.Checker (Unit))
|
||||
(Kind.Checker.extend name type vals) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked (Kind.Context.extend context name type vals) (+ depth 1) rhs subst eqts errs (Unit.new))
|
||||
|
||||
// Kind.Context.extend (prev: (Kind.Context)) (name: U60) (term: (Kind.Term)) (ls: (List (Kind.Term))) : (Kind.Context)
|
||||
(Kind.Context.extend (Kind.Context.empty) name type values) = (Kind.Context.entry name type values (Kind.Context.empty))
|
||||
(Kind.Context.extend (Kind.Context.entry n t v rest) name type values) = (Kind.Context.entry n t v (Kind.Context.extend rest name type values))
|
||||
|
||||
// Kind.Checker.extended -(a: Type) (checker: (Kind.Checker a)) (name: U60) (type: (Kind.Term)) (vals: (List (Kind.Term))) : (Kind.Checker a)
|
||||
(Kind.Checker.extended checker name type vals) = (Kind.Checker.bind (Kind.Checker.extend name type vals) @_ (Kind.Checker.bind checker @got (Kind.Checker.bind (Kind.Checker.shrink) @_ (Kind.Checker.pure got))))
|
||||
|
||||
// Kind.Checker.shrink : (Kind.Checker (Unit))
|
||||
(Kind.Checker.shrink) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked (Kind.Context.shrink context) (- depth 1) rhs subst eqts errs (Unit.new))
|
||||
|
||||
// Kind.Context.shrink (ctx: (Kind.Context)) : (Kind.Context)
|
||||
(Kind.Context.shrink (Kind.Context.empty)) = (Kind.Context.empty)
|
||||
(Kind.Context.shrink (Kind.Context.entry name type vals (Kind.Context.empty))) = (Kind.Context.empty)
|
||||
(Kind.Context.shrink (Kind.Context.entry name type vals rest)) = (Kind.Context.entry name type vals (Kind.Context.shrink rest))
|
||||
|
||||
// Kind.Checker.error -(t: Type) (err: (Kind.Error)) (ret: t) : (Kind.Checker t)
|
||||
(Kind.Checker.error err ret) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts (List.cons err errs) ret)
|
||||
|
||||
// Kind.Term.if_all -(res: Type) (term: (Kind.Term)) (if: (_: U60) (_: U60) (_: (Kind.Term)) (_: (_: (Kind.Term)) (Kind.Term)) res) (else: res) : res
|
||||
(Kind.Term.if_all (Kind.Term.all orig name typ body) func_if else) = ((((func_if orig) name) typ) body)
|
||||
(Kind.Term.if_all other func_if else) = else
|
||||
|
||||
// Kind.Checker.get_subst : (Kind.Checker (Kind.Subst))
|
||||
(Kind.Checker.get_subst) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs subst)
|
||||
|
||||
// Kind.Checker.infer_args (args: (Kind.Term)) : (_: U60) (_: U60) (Kind.Term)
|
||||
(Kind.Checker.infer_args (Kind.Term.args7 x0 x1 x2 x3 x4 x5 x6)) = @ctid @orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 ctid orig) x0) x1) x2) x3) x4) x5) x6)
|
||||
(Kind.Checker.infer_args (Kind.Term.args8 x0 x1 x2 x3 x4 x5 x6 x7)) = @ctid @orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4) x5) x6) x7)
|
||||
@ -710,8 +557,164 @@
|
||||
(Kind.Checker.infer (Kind.Term.num orig numb)) = (Kind.Checker.pure (Kind.Term.u60 0))
|
||||
(Kind.Checker.infer (Kind.Term.op2 orig oper left right)) = (Kind.Checker.bind (Kind.Checker.check left (Kind.Term.u60 0)) @_ (Kind.Checker.bind (Kind.Checker.check right (Kind.Term.u60 0)) @_ (Kind.Checker.pure (Kind.Term.u60 0))))
|
||||
|
||||
// Kind.Checker.set_right_hand_side (rhs: (Bool)) : (Kind.Checker (Unit))
|
||||
(Kind.Checker.set_right_hand_side to_rhs) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth to_rhs subst eqts errs (Unit.new))
|
||||
// Kind.Checker.get_depth : (Kind.Checker U60)
|
||||
(Kind.Checker.get_depth) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs depth)
|
||||
|
||||
// Kind.Checker.find -(r: Type) (index: U60) (alt: r) (fun: (_: U60) (_: (Kind.Term)) (_: (List (Kind.Term))) r) : (Kind.Checker r)
|
||||
(Kind.Checker.find index alt fun) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs (Kind.Context.find context index alt fun))
|
||||
|
||||
// Kind.Context.find -(res: Type) (ctx: (Kind.Context)) (name: U60) (alt: res) (fun: (_: U60) (_: (Kind.Term)) (_: (List (Kind.Term))) res) : res
|
||||
(Kind.Context.find (Kind.Context.entry name type vals rest) 0 alt fun) = (((fun name) type) vals)
|
||||
(Kind.Context.find (Kind.Context.entry name type vals rest) n alt fun) = (Kind.Context.find rest (- n 1) alt fun)
|
||||
(Kind.Context.find (Kind.Context.empty) n alt fun) = alt
|
||||
|
||||
// Kind.Checker.equal (left: (Kind.Term)) (right: (Kind.Term)) : (Kind.Checker (Bool))
|
||||
(Kind.Checker.equal (Kind.Term.typ orig) (Kind.Term.typ orig1)) = (Kind.Checker.pure (Bool.true))
|
||||
(Kind.Checker.equal (Kind.Term.all a.orig a.name a.type a.body) (Kind.Term.all b.orig b.name b.type b.body)) = (Kind.Checker.bind (Kind.Checker.get_depth) @dep (Kind.Checker.bind (Kind.Checker.equal a.type b.type) @type (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.equal (a.body (Kind.Term.var a.orig a.name dep)) (b.body (Kind.Term.var b.orig b.name dep))) (Null) (Null) (List.nil)) @body (Kind.Checker.pure (Bool.and type body)))))
|
||||
(Kind.Checker.equal (Kind.Term.lam a.orig a.name a.body) (Kind.Term.lam b.orig b.name b.body)) = (Kind.Checker.bind (Kind.Checker.get_depth) @dep (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.equal (a.body (Kind.Term.var a.orig a.name dep)) (b.body (Kind.Term.var b.orig b.name dep))) (Null) (Null) (List.nil)) @body (Kind.Checker.pure body)))
|
||||
(Kind.Checker.equal (Kind.Term.app a.orig a.func a.argm) (Kind.Term.app b.orig b.func b.argm)) = (Kind.Checker.bind (Kind.Checker.equal a.func b.func) @func (Kind.Checker.bind (Kind.Checker.equal a.argm b.argm) @argm (Kind.Checker.pure (Bool.and func argm))))
|
||||
(Kind.Checker.equal (Kind.Term.let a.orig a.name a.expr a.body) (Kind.Term.let b.orig b.name b.expr b.body)) = (Kind.Checker.bind (Kind.Checker.get_depth) @dep (Kind.Checker.bind (Kind.Checker.equal a.expr b.expr) @expr (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.equal (a.body (Kind.Term.var a.orig a.name dep)) (b.body (Kind.Term.var b.orig b.name dep))) (Null) (Null) (List.nil)) @body (Kind.Checker.pure (Bool.and expr body)))))
|
||||
(Kind.Checker.equal (Kind.Term.ann a.orig a.expr a.type) (Kind.Term.ann b.orig b.expr b.type)) = (Kind.Checker.bind (Kind.Checker.equal a.expr b.expr) @func (Kind.Checker.bind (Kind.Checker.equal a.type b.type) @arg (Kind.Checker.pure (Bool.and func arg))))
|
||||
(Kind.Checker.equal (Kind.Term.u60 a.orig) (Kind.Term.u60 b.orig)) = (Kind.Checker.pure (Bool.true))
|
||||
(Kind.Checker.equal (Kind.Term.num a.orig a.num) (Kind.Term.num b.orig b.num)) = (Kind.Checker.pure (U60.equal a.num b.num))
|
||||
(Kind.Checker.equal (Kind.Term.op2 a.orig a.op a.val0 a.val1) (Kind.Term.op2 b.orig b.op b.val0 b.val1)) = let op = (Kind.Operator.equal a.op b.op); (Kind.Checker.bind (Kind.Checker.equal a.val0 b.val0) @val0 (Kind.Checker.bind (Kind.Checker.equal a.val1 b.val1) @val1 (Kind.Checker.pure (Bool.and op (Bool.and val0 val1)))))
|
||||
(Kind.Checker.equal (Kind.Term.hol a.orig a.numb) (Kind.Term.hol b.orig b.numb)) = (Bool.if (U60.equal a.numb b.numb) (Kind.Checker.pure (Bool.true)) (Kind.Checker.equal.hol a.orig a.numb (Kind.Term.hol b.orig b.numb)))
|
||||
(Kind.Checker.equal (Kind.Term.hol a.orig a.numb) b) = (Kind.Checker.equal.hol a.orig a.numb b)
|
||||
(Kind.Checker.equal b (Kind.Term.hol a.orig a.numb)) = (Kind.Checker.equal.hol a.orig a.numb b)
|
||||
(Kind.Checker.equal (Kind.Term.var a.orig a.name a.idx) b) = (Kind.Checker.bind (Kind.Checker.get_right_hand_side) @rhs (Kind.Checker.equal.var rhs a.orig a.name a.idx b))
|
||||
(Kind.Checker.equal b (Kind.Term.var a.orig a.name a.idx)) = (Kind.Checker.bind (Kind.Checker.get_right_hand_side) @rhs (Kind.Checker.equal.var rhs a.orig a.name a.idx b))
|
||||
(Kind.Checker.equal (Kind.Term.ct0 a.ctid a.orig) (Kind.Term.ct0 b.ctid b.orig)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.pure ctid)
|
||||
(Kind.Checker.equal (Kind.Term.ct1 a.ctid a.orig a.x0) (Kind.Term.ct1 b.ctid b.orig b.x0)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.pure (Bool.and ctid x0)))
|
||||
(Kind.Checker.equal (Kind.Term.ct2 a.ctid a.orig a.x0 a.x1) (Kind.Term.ct2 b.ctid b.orig b.x0 b.x1)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 x1)))))
|
||||
(Kind.Checker.equal (Kind.Term.ct3 a.ctid a.orig a.x0 a.x1 a.x2) (Kind.Term.ct3 b.ctid b.orig b.x0 b.x1 b.x2)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 x2)))))))
|
||||
(Kind.Checker.equal (Kind.Term.ct4 a.ctid a.orig a.x0 a.x1 a.x2 a.x3) (Kind.Term.ct4 b.ctid b.orig b.x0 b.x1 b.x2 b.x3)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 x3)))))))))
|
||||
(Kind.Checker.equal (Kind.Term.ct5 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4) (Kind.Term.ct5 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.bind (Kind.Checker.equal a.x4 b.x4) @x4 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 x4)))))))))))
|
||||
(Kind.Checker.equal (Kind.Term.ct6 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5) (Kind.Term.ct6 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.bind (Kind.Checker.equal a.x4 b.x4) @x4 (Kind.Checker.bind (Kind.Checker.equal a.x5 b.x5) @x5 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 x5)))))))))))))
|
||||
(Kind.Checker.equal (Kind.Term.ct7 a.ctid a.orig a.args) (Kind.Term.ct7 b.ctid b.orig b.args)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.args b.args) @xargs (Kind.Checker.pure (Bool.and ctid xargs)))
|
||||
(Kind.Checker.equal (Kind.Term.ct8 a.ctid a.orig a.args) (Kind.Term.ct8 b.ctid b.orig b.args)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.args b.args) @xargs (Kind.Checker.pure (Bool.and ctid xargs)))
|
||||
(Kind.Checker.equal (Kind.Term.args7 a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6) (Kind.Term.args7 b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6)) = (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.bind (Kind.Checker.equal a.x4 b.x4) @x4 (Kind.Checker.bind (Kind.Checker.equal a.x5 b.x5) @x5 (Kind.Checker.bind (Kind.Checker.equal a.x6 b.x6) @x6 (Kind.Checker.pure (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 x6))))))))))))))
|
||||
(Kind.Checker.equal (Kind.Term.args8 a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7) (Kind.Term.args8 b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7)) = (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.bind (Kind.Checker.equal a.x4 b.x4) @x4 (Kind.Checker.bind (Kind.Checker.equal a.x5 b.x5) @x5 (Kind.Checker.bind (Kind.Checker.equal a.x6 b.x6) @x6 (Kind.Checker.bind (Kind.Checker.equal a.x7 b.x7) @x7 (Kind.Checker.pure (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 x7))))))))))))))))
|
||||
(Kind.Checker.equal (Kind.Term.fn0 a.ctid a.orig) (Kind.Term.fn0 b.ctid b.orig)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.pure ctid)
|
||||
(Kind.Checker.equal (Kind.Term.fn1 a.ctid a.orig a.x0) (Kind.Term.fn1 b.ctid b.orig b.x0)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.pure (Bool.and ctid x0)))
|
||||
(Kind.Checker.equal (Kind.Term.fn2 a.ctid a.orig a.x0 a.x1) (Kind.Term.fn2 b.ctid b.orig b.x0 b.x1)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 x1)))))
|
||||
(Kind.Checker.equal (Kind.Term.fn3 a.ctid a.orig a.x0 a.x1 a.x2) (Kind.Term.fn3 b.ctid b.orig b.x0 b.x1 b.x2)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 x2)))))))
|
||||
(Kind.Checker.equal (Kind.Term.fn4 a.ctid a.orig a.x0 a.x1 a.x2 a.x3) (Kind.Term.fn4 b.ctid b.orig b.x0 b.x1 b.x2 b.x3)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 x3)))))))))
|
||||
(Kind.Checker.equal (Kind.Term.fn5 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4) (Kind.Term.fn5 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.bind (Kind.Checker.equal a.x4 b.x4) @x4 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 x4)))))))))))
|
||||
(Kind.Checker.equal (Kind.Term.fn6 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5) (Kind.Term.fn6 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.bind (Kind.Checker.equal a.x4 b.x4) @x4 (Kind.Checker.bind (Kind.Checker.equal a.x5 b.x5) @x5 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 x5)))))))))))))
|
||||
(Kind.Checker.equal (Kind.Term.fn7 a.ctid a.orig a.args) (Kind.Term.fn7 b.ctid b.orig b.args)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.args b.args) @xargs (Kind.Checker.pure (Bool.and ctid xargs)))
|
||||
(Kind.Checker.equal (Kind.Term.fn8 a.ctid a.orig a.args) (Kind.Term.fn8 b.ctid b.orig b.args)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.args b.args) @xargs (Kind.Checker.pure (Bool.and ctid xargs)))
|
||||
(Kind.Checker.equal a b) = (Kind.Checker.bind (Kind.Checker.get_subst) @sub (Bool.if (Bool.or (Kind.Term.fillable a sub) (Kind.Term.fillable b sub)) (Kind.Checker.equal (Kind.Term.fill a sub) (Kind.Term.fill b sub)) (Kind.Checker.pure (Bool.false))))
|
||||
|
||||
// Kind.Checker.equal.var (rhs: (Bool)) (orig: U60) (name: U60) (idx: U60) (b: (Kind.Term)) : (Kind.Checker (Bool))
|
||||
(Kind.Checker.equal.var (Bool.false) orig name idx b) = (Kind.Checker.bind (Kind.Checker.add_value idx b) @_ (Kind.Checker.pure (Bool.true)))
|
||||
(Kind.Checker.equal.var (Bool.true) a.orig a.name a.idx (Kind.Term.var b.orig b.name b.idx)) = (Bool.if (U60.equal a.idx b.idx) (Kind.Checker.pure (Bool.true)) (Kind.Checker.bind (Kind.Checker.find a.idx (List.nil) @n @t @v v) @a.val (Kind.Checker.bind (Kind.Checker.find b.idx (List.nil) @n @t @v v) @b.val (Kind.Checker.bind (Kind.Checker.equal.var.try_values a.val (Kind.Term.var b.orig b.name b.idx)) @a.chk (Kind.Checker.bind (Kind.Checker.equal.var.try_values b.val (Kind.Term.var a.orig a.name a.idx)) @b.chk (Kind.Checker.pure (Bool.or a.chk b.chk)))))))
|
||||
(Kind.Checker.equal.var (Bool.true) a.orig a.name a.idx b) = (Kind.Checker.bind (Kind.Checker.get_subst) @sub (Bool.if (Kind.Term.fillable b sub) (Kind.Checker.equal (Kind.Term.var a.orig a.name a.idx) (Kind.Term.fill b sub)) (Kind.Checker.bind (Kind.Checker.find a.idx (List.nil) @n @t @v v) @a.val (Kind.Checker.bind (Kind.Checker.equal.var.try_values a.val b) @res (Kind.Checker.pure res)))))
|
||||
|
||||
// Kind.Checker.equal.var.try_values (ls: (List (Kind.Term))) (term: (Kind.Term)) : (Kind.Checker (Bool))
|
||||
(Kind.Checker.equal.var.try_values (List.nil) term) = (Kind.Checker.pure (Bool.false))
|
||||
(Kind.Checker.equal.var.try_values (List.cons x xs) term) = (Kind.Checker.bind (Kind.Checker.equal x term) @head (Bool.if head (Kind.Checker.pure (Bool.true)) (Kind.Checker.equal.var.try_values xs term)))
|
||||
|
||||
// Kind.Checker.equal.hol (orig: U60) (numb: U60) (b: (Kind.Term)) : (Kind.Checker (Bool))
|
||||
(Kind.Checker.equal.hol a.orig a.numb b) = (Kind.Checker.bind (Kind.Checker.look a.numb) @got (Kind.Checker.bind (Kind.Checker.equal.hol.val got a.orig a.numb b) @res (Kind.Checker.pure res)))
|
||||
|
||||
// Kind.Checker.equal.hol.val (val: (Maybe (Kind.Term))) (orig: U60) (numb: U60) (b: (Kind.Term)) : (Kind.Checker (Bool))
|
||||
(Kind.Checker.equal.hol.val (Maybe.none) orig numb b) = (Kind.Checker.bind (Kind.Checker.fill numb b) @_ (Kind.Checker.pure (Bool.true)))
|
||||
(Kind.Checker.equal.hol.val (Maybe.some val) orig numb b) = (Kind.Checker.equal val b)
|
||||
|
||||
// Kind.Checker.look (index: U60) : (Kind.Checker (Maybe (Kind.Term)))
|
||||
(Kind.Checker.look index) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs (Kind.Subst.look subst index))
|
||||
|
||||
// Bool.and (a: (Bool)) (b: (Bool)) : (Bool)
|
||||
(Bool.and (Bool.true) b) = b
|
||||
(Bool.and (Bool.false) b) = (Bool.false)
|
||||
|
||||
// Kind.Term.fillable (term: (Kind.Term)) (sub: (Kind.Subst)) : (Bool)
|
||||
(Kind.Term.fillable term (Kind.Subst.end)) = (Bool.false)
|
||||
(Kind.Term.fillable (Kind.Term.typ orig) sub) = (Bool.false)
|
||||
(Kind.Term.fillable (Kind.Term.var orig name index) sub) = (Bool.false)
|
||||
(Kind.Term.fillable (Kind.Term.hlp orig) sub) = (Bool.false)
|
||||
(Kind.Term.fillable (Kind.Term.u60 orig) sub) = (Bool.false)
|
||||
(Kind.Term.fillable (Kind.Term.num orig num) sub) = (Bool.false)
|
||||
(Kind.Term.fillable (Kind.Term.all orig name typ body) sub) = (Bool.or (Kind.Term.fillable typ sub) (Kind.Term.fillable (body (Kind.Term.hlp 0)) sub))
|
||||
(Kind.Term.fillable (Kind.Term.lam orig name body) sub) = (Kind.Term.fillable (body (Kind.Term.hlp 0)) sub)
|
||||
(Kind.Term.fillable (Kind.Term.app orig expr typ) sub) = (Bool.or (Kind.Term.fillable expr sub) (Kind.Term.fillable typ sub))
|
||||
(Kind.Term.fillable (Kind.Term.let orig name expr body) sub) = (Bool.or (Kind.Term.fillable expr sub) (Kind.Term.fillable (body (Kind.Term.hlp 0)) sub))
|
||||
(Kind.Term.fillable (Kind.Term.ann orig expr typ) sub) = (Bool.or (Kind.Term.fillable expr sub) (Kind.Term.fillable typ sub))
|
||||
(Kind.Term.fillable (Kind.Term.op2 orig op left right) sub) = (Bool.or (Kind.Term.fillable left sub) (Kind.Term.fillable right sub))
|
||||
(Kind.Term.fillable (Kind.Term.hol orig numb) sub) = (Maybe.is_some (Kind.Subst.look sub numb))
|
||||
(Kind.Term.fillable (Kind.Term.ct0 ctid orig) sub) = (Bool.false)
|
||||
(Kind.Term.fillable (Kind.Term.ct1 ctid orig x0) sub) = (Kind.Term.fillable x0 sub)
|
||||
(Kind.Term.fillable (Kind.Term.ct2 ctid orig x0 x1) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Kind.Term.fillable x1 sub))
|
||||
(Kind.Term.fillable (Kind.Term.ct3 ctid orig x0 x1 x2) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Kind.Term.fillable x2 sub)))
|
||||
(Kind.Term.fillable (Kind.Term.ct4 ctid orig x0 x1 x2 x3) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Bool.or (Kind.Term.fillable x2 sub) (Kind.Term.fillable x3 sub))))
|
||||
(Kind.Term.fillable (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Bool.or (Kind.Term.fillable x2 sub) (Bool.or (Kind.Term.fillable x3 sub) (Kind.Term.fillable x4 sub)))))
|
||||
(Kind.Term.fillable (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Bool.or (Kind.Term.fillable x2 sub) (Bool.or (Kind.Term.fillable x3 sub) (Bool.or (Kind.Term.fillable x4 sub) (Kind.Term.fillable x5 sub))))))
|
||||
(Kind.Term.fillable (Kind.Term.ct7 fnid orig args) sub) = (Kind.Term.fillable args sub)
|
||||
(Kind.Term.fillable (Kind.Term.ct8 fnid orig args) sub) = (Kind.Term.fillable args sub)
|
||||
(Kind.Term.fillable (Kind.Term.fn0 fnid orig) sub) = (Bool.false)
|
||||
(Kind.Term.fillable (Kind.Term.fn1 fnid orig x0) sub) = (Kind.Term.fillable x0 sub)
|
||||
(Kind.Term.fillable (Kind.Term.fn2 fnid orig x0 x1) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Kind.Term.fillable x1 sub))
|
||||
(Kind.Term.fillable (Kind.Term.fn3 fnid orig x0 x1 x2) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Kind.Term.fillable x2 sub)))
|
||||
(Kind.Term.fillable (Kind.Term.fn4 fnid orig x0 x1 x2 x3) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Bool.or (Kind.Term.fillable x2 sub) (Kind.Term.fillable x3 sub))))
|
||||
(Kind.Term.fillable (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Bool.or (Kind.Term.fillable x2 sub) (Bool.or (Kind.Term.fillable x3 sub) (Kind.Term.fillable x4 sub)))))
|
||||
(Kind.Term.fillable (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Bool.or (Kind.Term.fillable x2 sub) (Bool.or (Kind.Term.fillable x3 sub) (Bool.or (Kind.Term.fillable x4 sub) (Kind.Term.fillable x5 sub))))))
|
||||
(Kind.Term.fillable (Kind.Term.fn7 fnid orig args) sub) = (Kind.Term.fillable args sub)
|
||||
(Kind.Term.fillable (Kind.Term.fn8 fnid orig args) sub) = (Kind.Term.fillable args sub)
|
||||
(Kind.Term.fillable (Kind.Term.args7 x0 x1 x2 x3 x4 x5 x6) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Bool.or (Kind.Term.fillable x2 sub) (Bool.or (Kind.Term.fillable x3 sub) (Bool.or (Kind.Term.fillable x4 sub) (Bool.or (Kind.Term.fillable x5 sub) (Kind.Term.fillable x6 sub)))))))
|
||||
(Kind.Term.fillable (Kind.Term.args8 x0 x1 x2 x3 x4 x5 x6 x7) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Bool.or (Kind.Term.fillable x2 sub) (Bool.or (Kind.Term.fillable x3 sub) (Bool.or (Kind.Term.fillable x4 sub) (Bool.or (Kind.Term.fillable x5 sub) (Bool.or (Kind.Term.fillable x6 sub) (Kind.Term.fillable x7 sub))))))))
|
||||
|
||||
// Bool.or (a: (Bool)) (b: (Bool)) : (Bool)
|
||||
(Bool.or (Bool.true) b) = (Bool.true)
|
||||
(Bool.or (Bool.false) b) = b
|
||||
|
||||
// Maybe.is_some -(a: Type) (m: (Maybe a)) : (Bool)
|
||||
(Maybe.is_some (Maybe.none)) = (Bool.false)
|
||||
(Maybe.is_some (Maybe.some v)) = (Bool.true)
|
||||
|
||||
// U60.equal (a: U60) (b: U60) : (Bool)
|
||||
(U60.equal a b) = (U60.to_bool (== a b))
|
||||
|
||||
// U60.to_bool (n: U60) : (Bool)
|
||||
(U60.to_bool 0) = (Bool.false)
|
||||
(U60.to_bool n) = (Bool.true)
|
||||
|
||||
// Kind.Checker.add_value (idx: U60) (val: (Kind.Term)) : (Kind.Checker (Unit))
|
||||
(Kind.Checker.add_value idx val) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked (Kind.Context.add_value context idx val) depth rhs subst eqts errs (Unit.new))
|
||||
|
||||
// Kind.Context.add_value (prev: (Kind.Context)) (name: U60) (term: (Kind.Term)) : (Kind.Context)
|
||||
(Kind.Context.add_value (Kind.Context.entry name type vals rest) 0 val) = (Kind.Context.entry name type (List.cons val vals) rest)
|
||||
(Kind.Context.add_value (Kind.Context.entry name type vals rest) n val) = (Kind.Context.entry name type vals (Kind.Context.add_value rest (- n 1) val))
|
||||
(Kind.Context.add_value (Kind.Context.empty) n val) = (Kind.Context.empty)
|
||||
|
||||
// Kind.Operator.equal (left: (Kind.Operator)) (right: (Kind.Operator)) : (Bool)
|
||||
(Kind.Operator.equal (Kind.Operator.and) (Kind.Operator.and)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.sub) (Kind.Operator.sub)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.mul) (Kind.Operator.mul)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.div) (Kind.Operator.div)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.mod) (Kind.Operator.mod)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.and) (Kind.Operator.and)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.or) (Kind.Operator.or)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.xor) (Kind.Operator.xor)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.shl) (Kind.Operator.shl)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.shr) (Kind.Operator.shr)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.ltn) (Kind.Operator.ltn)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.lte) (Kind.Operator.lte)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.eql) (Kind.Operator.eql)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.gte) (Kind.Operator.gte)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.gtn) (Kind.Operator.gtn)) = (Bool.true)
|
||||
(Kind.Operator.equal (Kind.Operator.neq) (Kind.Operator.neq)) = (Bool.true)
|
||||
(Kind.Operator.equal a b) = (Bool.false)
|
||||
|
||||
// Kind.Checker.fill (index: U60) (val: (Kind.Term)) : (Kind.Checker (Unit))
|
||||
(Kind.Checker.fill index val) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs (Kind.Subst.fill subst index val) eqts errs (Unit.new))
|
||||
|
||||
// Kind.Subst.fill (subst: (Kind.Subst)) (depth: U60) (term: (Kind.Term)) : (Kind.Subst)
|
||||
(Kind.Subst.fill (Kind.Subst.end) 0 term) = (Kind.Subst.sub term (Kind.Subst.end))
|
||||
(Kind.Subst.fill (Kind.Subst.unfilled rest) 0 term) = (Kind.Subst.sub term rest)
|
||||
(Kind.Subst.fill (Kind.Subst.sub lost rest) 0 term) = (Kind.Subst.sub term rest)
|
||||
(Kind.Subst.fill (Kind.Subst.end) n term) = (Kind.Subst.unfilled (Kind.Subst.fill (Kind.Subst.end) (- n 1) term))
|
||||
(Kind.Subst.fill (Kind.Subst.unfilled rest) n term) = (Kind.Subst.unfilled (Kind.Subst.fill rest (- n 1) term))
|
||||
(Kind.Subst.fill (Kind.Subst.sub keep rest) n term) = (Kind.Subst.sub keep (Kind.Subst.fill rest (- n 1) term))
|
||||
|
||||
// Kind.Checker.unify (checker: (Kind.Checker (Unit))) : (Kind.Checker (Unit))
|
||||
(Kind.Checker.unify checker) = (Kind.Checker.bind checker @_ (Kind.Checker.bind (Kind.Checker.get_equations) @equations (Kind.Checker.unify.go equations (List.nil) (Bool.false))))
|
||||
|
||||
Loading…
Reference in New Issue
Block a user