HigherOrderCO/Kind1
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind1.git synced 2024-09-19 04:37:28 +03:00
Code Issues Packages Projects Releases Wiki Activity

Fixes

Browse Source
This commit is contained in:
Felipe g 2022-09-21 11:53:55 -03:00
parent e6d79950d9
commit 6c3be451b9
9 changed files with 349 additions and 331 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/book.rs
View File

@ -118,7 +118,7 @@ impl Display for Entry {
write!(f, "\n{}", rule)?
}
Ok(())
writeln!(f, "")
}
}

4
src/book/term.rs
View File

@ -80,7 +80,7 @@ impl Display for Operator {
use Operator::*;
match self {
Add => write!(f, "*"),
Add => write!(f, "+"),
Sub => write!(f, "-"),
Mul => write!(f, "*"),
Div => write!(f, "/"),
@ -116,7 +116,7 @@ impl Display for Term {
Lam { orig: _, name, body } => write!(f, "({} => {})", name, body),
Ann { orig: _, expr, tipo } => write!(f, "({} :: {})", expr, tipo),
Op2 { orig: _, oper, val0, val1 } => write!(f, "({} {} {})", oper, val0, val1),
All { orig: _, name, tipo, body } => write!(f, "(({}: {}) {})", name, tipo, body),
All { orig: _, name, tipo, body } => write!(f, "({}: {}) {}", name, tipo, body),
Let { orig: _, name, expr, body } => write!(f, "(let {} = {}; {})", name, expr, body),
Sub { name, redx, expr, .. } => write!(f, "({} ## {}/{})", expr, name, redx),
Ctr { orig: _, name, args } => write!(f, "({}{})", name, args.iter().map(|x| format!(" {}", x)).collect::<String>()),

575
src/checker.hvm
View File

@ -4,14 +4,6 @@
// Kind.API.eval_main : (String)
(Kind.API.eval_main) = (Kind.Printer.text (List.cons (Kind.Term.show (Kind.Term.FN0 (Main.) 0)) (List.cons (String.new_line) (List.cons (String.new_line) (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.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))))))))))
@ -69,43 +61,28 @@
(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)))))))))
// 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.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)
// 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)))))))
// 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))
// 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)
// 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
// Maybe.pure -(a: Type) (x: a) : (Maybe a)
(Maybe.pure x) = (Maybe.some x)
// 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)))
// Show.to_string (show: (Show)) : (String)
(Show.to_string show) = (show "")
// Show : Type
(Show) = 0
// 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 (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
// 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)
// Maybe.match -(t: Type) (x: (Maybe t)) -(p: (x: (Maybe t)) Type) (none: (p (Maybe.none t))) (some: (value: t) (p (Maybe.some t value))) : (p x)
(Maybe.match (Maybe.none) none some) = none
(Maybe.match (Maybe.some value_) none some) = (some value_)
// 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)))
@ -114,16 +91,19 @@
// Kind.Term.show.sugar.list (term: (Kind.Term)) : (Maybe (String))
(Kind.Term.show.sugar.list term) = (Maybe.bind (Kind.Term.show.sugar.list.go term) @res (Maybe.pure (Kind.Printer.text (List.cons "[" (List.cons (String.join " " res) (List.cons "]" (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)
// String.join (sep: (String)) (list: (List (String))) : (String)
(String.join sep list) = (String.intercalate sep list)
// 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)
@ -132,15 +112,31 @@
// List.pure -(t: Type) (x: t) : (List t)
(List.pure x) = (List.cons x (List.nil))
// 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)
// String.flatten (xs: (List (String))) : (String)
(String.flatten (List.nil)) = ""
(String.flatten (List.cons head tail)) = (String.concat head (String.flatten tail))
// 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)))
// 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.Name.show (name: U60) : (String)
(Kind.Name.show name) = (Kind.Name.show.go name "")
// Maybe.match -(t: Type) (x: (Maybe t)) -(p: (x: (Maybe t)) Type) (none: (p (Maybe.none t))) (some: (value: t) (p (Maybe.some t value))) : (p x)
(Maybe.match (Maybe.none) none some) = none
(Maybe.match (Maybe.some value_) none some) = (some 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)))))))
// Kind.Operator.show (op: (Kind.Operator)) : (String)
(Kind.Operator.show (Kind.Operator.add)) = "+"
@ -160,70 +156,29 @@
(Kind.Operator.show (Kind.Operator.gtn)) = ">"
(Kind.Operator.show (Kind.Operator.neq)) = "!="
// 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
// Kind.Term.set_origin (new_origin: U60) (term: (Kind.Term)) : (Kind.Term)
(Kind.Term.set_origin new_origin (Kind.Term.typ old_orig)) = (Kind.Term.typ new_origin)
(Kind.Term.set_origin new_origin (Kind.Term.var old_orig name idx)) = (Kind.Term.var new_origin name idx)
(Kind.Term.set_origin new_origin (Kind.Term.hol old_orig numb)) = (Kind.Term.hol new_origin numb)
(Kind.Term.set_origin new_origin (Kind.Term.all old_orig name typ body)) = (Kind.Term.all new_origin name typ body)
(Kind.Term.set_origin new_origin (Kind.Term.lam old_orig name body)) = (Kind.Term.lam new_origin name body)
(Kind.Term.set_origin new_origin (Kind.Term.let old_orig name expr body)) = (Kind.Term.let new_origin name expr body)
(Kind.Term.set_origin new_origin (Kind.Term.ann old_orig expr typ)) = (Kind.Term.ann new_origin expr typ)
(Kind.Term.set_origin new_origin (Kind.Term.sub old_orig name indx redx expr)) = (Kind.Term.sub new_origin name indx redx expr)
(Kind.Term.set_origin new_origin (Kind.Term.app old_orig func arg)) = (Kind.Term.app new_origin func arg)
(Kind.Term.set_origin new_origin (Kind.Term.hlp old_orig)) = (Kind.Term.hlp new_origin)
(Kind.Term.set_origin new_origin (Kind.Term.u60 old_orig)) = (Kind.Term.u60 new_origin)
(Kind.Term.set_origin new_origin (Kind.Term.num old_orig num)) = (Kind.Term.num new_origin num)
(Kind.Term.set_origin new_origin (Kind.Term.op2 old_orig op left right)) = (Kind.Term.op2 new_origin op left right)
(Kind.Term.set_origin new_origin (Kind.Term.ct0 ctid old_orig)) = (Kind.Term.ct0 ctid new_origin)
(Kind.Term.set_origin new_origin (Kind.Term.ct1 ctid old_orig x0)) = (Kind.Term.ct1 ctid new_origin x0)
(Kind.Term.set_origin new_origin (Kind.Term.ct2 ctid old_orig x0 x1)) = (Kind.Term.ct2 ctid new_origin x0 x1)
(Kind.Term.set_origin new_origin (Kind.Term.ct3 ctid old_orig x0 x1 x2)) = (Kind.Term.ct3 ctid new_origin x0 x1 x2)
(Kind.Term.set_origin new_origin (Kind.Term.ct4 ctid old_orig x0 x1 x2 x3)) = (Kind.Term.ct4 ctid new_origin x0 x1 x2 x3)
(Kind.Term.set_origin new_origin (Kind.Term.ct5 ctid old_orig x0 x1 x2 x3 x4)) = (Kind.Term.ct5 ctid new_origin x0 x1 x2 x3 x4)
(Kind.Term.set_origin new_origin (Kind.Term.ct6 ctid old_orig x0 x1 x2 x3 x4 x5)) = (Kind.Term.ct6 ctid new_origin x0 x1 x2 x3 x4 x5)
(Kind.Term.set_origin new_origin (Kind.Term.ct7 ctid old_orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Term.ct7 ctid new_origin x0 x1 x2 x3 x4 x5 x6)
(Kind.Term.set_origin new_origin (Kind.Term.ct8 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Term.ct8 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7)
(Kind.Term.set_origin new_origin (Kind.Term.ct9 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Term.ct9 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8)
(Kind.Term.set_origin new_origin (Kind.Term.ct10 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Term.ct10 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)
(Kind.Term.set_origin new_origin (Kind.Term.ct11 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Term.ct11 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)
(Kind.Term.set_origin new_origin (Kind.Term.ct12 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Term.ct12 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)
(Kind.Term.set_origin new_origin (Kind.Term.ct13 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Term.ct13 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)
(Kind.Term.set_origin new_origin (Kind.Term.ct14 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Term.ct14 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)
(Kind.Term.set_origin new_origin (Kind.Term.ct15 ctid old_orig args)) = (Kind.Term.ct15 ctid new_origin args)
(Kind.Term.set_origin new_origin (Kind.Term.ct16 ctid old_orig args)) = (Kind.Term.ct16 ctid new_origin args)
(Kind.Term.set_origin new_origin (Kind.Term.fn0 fnid old_orig)) = (Kind.Term.fn0 fnid new_origin)
(Kind.Term.set_origin new_origin (Kind.Term.fn1 fnid old_orig x0)) = (Kind.Term.fn1 fnid new_origin x0)
(Kind.Term.set_origin new_origin (Kind.Term.fn2 fnid old_orig x0 x1)) = (Kind.Term.fn2 fnid new_origin x0 x1)
(Kind.Term.set_origin new_origin (Kind.Term.fn3 fnid old_orig x0 x1 x2)) = (Kind.Term.fn3 fnid new_origin x0 x1 x2)
(Kind.Term.set_origin new_origin (Kind.Term.fn4 fnid old_orig x0 x1 x2 x3)) = (Kind.Term.fn4 fnid new_origin x0 x1 x2 x3)
(Kind.Term.set_origin new_origin (Kind.Term.fn5 fnid old_orig x0 x1 x2 x3 x4)) = (Kind.Term.fn5 fnid new_origin x0 x1 x2 x3 x4)
(Kind.Term.set_origin new_origin (Kind.Term.fn6 fnid old_orig x0 x1 x2 x3 x4 x5)) = (Kind.Term.fn6 fnid new_origin x0 x1 x2 x3 x4 x5)
(Kind.Term.set_origin new_origin (Kind.Term.fn7 fnid old_orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Term.fn7 fnid new_origin x0 x1 x2 x3 x4 x5 x6)
(Kind.Term.set_origin new_origin (Kind.Term.fn8 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Term.fn8 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7)
(Kind.Term.set_origin new_origin (Kind.Term.fn9 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Term.fn9 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8)
(Kind.Term.set_origin new_origin (Kind.Term.fn10 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Term.fn10 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)
(Kind.Term.set_origin new_origin (Kind.Term.fn11 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Term.fn11 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)
(Kind.Term.set_origin new_origin (Kind.Term.fn12 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Term.fn12 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)
(Kind.Term.set_origin new_origin (Kind.Term.fn13 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Term.fn13 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)
(Kind.Term.set_origin new_origin (Kind.Term.fn14 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Term.fn14 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)
(Kind.Term.set_origin new_origin (Kind.Term.fn15 ctid old_orig args)) = (Kind.Term.fn15 ctid new_origin args)
(Kind.Term.set_origin new_origin (Kind.Term.fn16 ctid old_orig args)) = (Kind.Term.fn16 ctid new_origin args)
// Char : Type
(Char) = 0
// String.pure (x: (Char)) : (String)
(String.pure x) = (String.cons x "")
// Kind.API.check_all : (String)
(Kind.API.check_all) = let output = (Kind.API.output (List.reverse (Kind.API.check_functions (Functions)))); (Bool.if (String.is_nil output) (Kind.Printer.text (List.cons "All terms check." (List.cons (String.new_line) (List.cons (String.new_line) (List.nil))))) output)
// String.is_nil (xs: (String)) : (Bool)
(String.is_nil "") = (Bool.true)
(String.is_nil (String.cons x xs)) = (Bool.false)
// Kind.API.check_functions (fnid: (List U60)) : (List (Pair U60 (List (Kind.Result (Unit)))))
(Kind.API.check_functions (List.nil)) = (List.nil)
(Kind.API.check_functions (List.cons f fs)) = let head = (Pair.new f (Kind.API.check_function f)); let tail = (Kind.API.check_functions fs); (List.cons head tail)
@ -235,89 +190,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.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)
(Kind.Term.eval (Kind.Term.hol orig numb)) = (Kind.Term.hol orig numb)
(Kind.Term.eval (Kind.Term.all orig name typ body)) = (Kind.Term.all orig name (Kind.Term.eval typ) @x (Kind.Term.eval (body x)))
(Kind.Term.eval (Kind.Term.lam orig name body)) = (Kind.Term.lam orig name @x (Kind.Term.eval (body x)))
(Kind.Term.eval (Kind.Term.let orig name expr body)) = (Kind.Term.eval_let orig name (Kind.Term.eval expr) @x (Kind.Term.eval (body x)))
(Kind.Term.eval (Kind.Term.ann orig expr typ)) = (Kind.Term.eval_ann orig (Kind.Term.eval expr) (Kind.Term.eval typ))
(Kind.Term.eval (Kind.Term.sub orig name indx redx expr)) = (Kind.Term.eval_sub orig name indx redx (Kind.Term.eval expr))
(Kind.Term.eval (Kind.Term.app orig expr typ)) = (Kind.Term.eval_app orig (Kind.Term.eval expr) (Kind.Term.eval typ))
(Kind.Term.eval (Kind.Term.hlp orig)) = (Kind.Term.hlp orig)
(Kind.Term.eval (Kind.Term.u60 orig)) = (Kind.Term.u60 orig)
(Kind.Term.eval (Kind.Term.num orig num)) = (Kind.Term.num orig num)
(Kind.Term.eval (Kind.Term.op2 orig op left right)) = (Kind.Term.eval_op orig op (Kind.Term.eval left) (Kind.Term.eval right))
(Kind.Term.eval (Kind.Term.ct0 ctid orig)) = (Kind.Term.ct0 ctid orig)
(Kind.Term.eval (Kind.Term.ct1 ctid orig x0)) = (Kind.Term.ct1 ctid orig (Kind.Term.eval x0))
(Kind.Term.eval (Kind.Term.ct2 ctid orig x0 x1)) = (Kind.Term.ct2 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1))
(Kind.Term.eval (Kind.Term.ct3 ctid orig x0 x1 x2)) = (Kind.Term.ct3 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2))
(Kind.Term.eval (Kind.Term.ct4 ctid orig x0 x1 x2 x3)) = (Kind.Term.ct4 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3))
(Kind.Term.eval (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4)) = (Kind.Term.ct5 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4))
(Kind.Term.eval (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5)) = (Kind.Term.ct6 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5))
(Kind.Term.eval (Kind.Term.ct7 ctid orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Term.ct7 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6))
(Kind.Term.eval (Kind.Term.ct8 ctid orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Term.ct8 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7))
(Kind.Term.eval (Kind.Term.ct9 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Term.ct9 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8))
(Kind.Term.eval (Kind.Term.ct10 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Term.ct10 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9))
(Kind.Term.eval (Kind.Term.ct11 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Term.ct11 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10))
(Kind.Term.eval (Kind.Term.ct12 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Term.ct12 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11))
(Kind.Term.eval (Kind.Term.ct13 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Term.ct13 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11) (Kind.Term.eval x12))
(Kind.Term.eval (Kind.Term.ct14 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Term.ct14 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11) (Kind.Term.eval x12) (Kind.Term.eval x13))
(Kind.Term.eval (Kind.Term.ct15 fnid orig x0)) = (Kind.Term.ct15 fnid orig (Kind.Term.eval x0))
(Kind.Term.eval (Kind.Term.ct16 fnid orig x0)) = (Kind.Term.ct16 fnid orig (Kind.Term.eval x0))
(Kind.Term.eval (Kind.Term.fn0 fnid orig)) = (Kind.Term.FN0 fnid orig)
(Kind.Term.eval (Kind.Term.fn1 fnid orig x0)) = (Kind.Term.FN1 fnid orig (Kind.Term.eval x0))
(Kind.Term.eval (Kind.Term.fn2 fnid orig x0 x1)) = (Kind.Term.FN2 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1))
(Kind.Term.eval (Kind.Term.fn3 fnid orig x0 x1 x2)) = (Kind.Term.FN3 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2))
(Kind.Term.eval (Kind.Term.fn4 fnid orig x0 x1 x2 x3)) = (Kind.Term.FN4 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3))
(Kind.Term.eval (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4)) = (Kind.Term.FN5 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4))
(Kind.Term.eval (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5)) = (Kind.Term.FN6 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5))
(Kind.Term.eval (Kind.Term.fn7 fnid orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Term.FN7 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6))
(Kind.Term.eval (Kind.Term.fn8 fnid orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Term.FN8 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7))
(Kind.Term.eval (Kind.Term.fn9 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Term.FN9 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8))
(Kind.Term.eval (Kind.Term.fn10 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Term.FN10 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9))
(Kind.Term.eval (Kind.Term.fn11 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Term.FN11 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10))
(Kind.Term.eval (Kind.Term.fn12 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Term.FN12 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11))
(Kind.Term.eval (Kind.Term.fn13 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Term.FN13 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11) (Kind.Term.eval x12))
(Kind.Term.eval (Kind.Term.fn14 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Term.FN14 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11) (Kind.Term.eval x12) (Kind.Term.eval x13))
(Kind.Term.eval (Kind.Term.fn15 fnid orig x0)) = (Kind.Term.FN15 fnid orig (Kind.Term.eval x0))
(Kind.Term.eval (Kind.Term.fn16 fnid orig x0)) = (Kind.Term.FN16 fnid orig (Kind.Term.eval x0))
(Kind.Term.eval (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)) = (Kind.Term.args15 (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11) (Kind.Term.eval x12) (Kind.Term.eval x13) (Kind.Term.eval x14))
(Kind.Term.eval (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)) = (Kind.Term.args16 (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11) (Kind.Term.eval x12) (Kind.Term.eval x13) (Kind.Term.eval x14) (Kind.Term.eval x15))
// Kind.Term.eval_sub (orig: U60) (name: U60) (indx: U60) (redx: U60) (expr: (Kind.Term)) : (Kind.Term)
(Kind.Term.eval_sub orig name indx redx expr) = expr
// 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
// Kind.Term.eval_let (orig: U60) (name: U60) (expr: (Kind.Term)) (body: (_: (Kind.Term)) (Kind.Term)) : (Kind.Term)
(Kind.Term.eval_let orig name expr body) = (body expr)
// Kind.Term.eval_op (orig: U60) (op: (Kind.Operator)) (left: (Kind.Term)) (right: (Kind.Term)) : (Kind.Term)
(Kind.Term.eval_op orig (Kind.Operator.add) (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 (Kind.Operator.sub) (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 (Kind.Operator.mul) (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 (Kind.Operator.div) (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 (Kind.Operator.mod) (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 (Kind.Operator.and) (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 (Kind.Operator.or) (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 (Kind.Operator.xor) (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 (Kind.Operator.shl) (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 (Kind.Operator.shr) (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 (Kind.Operator.ltn) (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 (Kind.Operator.lte) (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 (Kind.Operator.eql) (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 (Kind.Operator.gte) (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 (Kind.Operator.gtn) (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 (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.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))))
@ -334,21 +206,18 @@
// Kind.Checker (a: Type) : Type
(Kind.Checker a) = 0
// Kind.Checker.with_context -(a: Type) (checker: (Kind.Checker a)) (context: (Kind.Context)) : (Kind.Checker a)
(Kind.Checker.with_context checker new_context) = (Kind.Checker.bind (Kind.Checker.set_context new_context) @old_context (Kind.Checker.bind checker @got (Kind.Checker.bind (Kind.Checker.set_context old_context) @_ (Kind.Checker.pure got))))
// 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.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.set_context (new_context: (Kind.Context)) : (Kind.Checker (Kind.Context))
(Kind.Checker.set_context new_context) = @old_context @depth @rhs @subst @eqts @errs (Kind.Result.checked new_context depth rhs subst eqts errs old_context)
// Bool.if -(a: Type) (b: (Bool)) (t: a) (f: a) : a
(Bool.if (Bool.true) t f) = t
(Bool.if (Bool.false) t f) = f
// 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.get_equations : (Kind.Checker (List (Kind.Equation)))
(Kind.Checker.get_equations) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs eqts)
// 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))
@ -420,24 +289,6 @@
(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.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.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.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))
@ -446,8 +297,17 @@
(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.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.or (a: (Bool)) (b: (Bool)) : (Bool)
(Bool.or (Bool.true) b) = (Bool.true)
(Bool.or (Bool.false) b) = 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))
@ -460,18 +320,6 @@
(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))
// Bool.and (a: (Bool)) (b: (Bool)) : (Bool)
(Bool.and (Bool.true) b) = b
(Bool.and (Bool.false) b) = (Bool.false)
// 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.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)
@ -528,21 +376,6 @@
(Maybe.is_some (Maybe.none)) = (Bool.false)
(Maybe.is_some (Maybe.some v)) = (Bool.true)
// Bool.or (a: (Bool)) (b: (Bool)) : (Bool)
(Bool.or (Bool.true) b) = (Bool.true)
(Bool.or (Bool.false) b) = b
// Bool.if -(a: Type) (b: (Bool)) (t: a) (f: a) : a
(Bool.if (Bool.true) t f) = t
(Bool.if (Bool.false) t f) = f
// 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.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))
@ -554,8 +387,8 @@
(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.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.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.Term.fill (term: (Kind.Term)) (subst: (Kind.Subst)) : (Kind.Term)
(Kind.Term.fill term (Kind.Subst.end)) = term
@ -609,6 +442,26 @@
(Kind.Term.fill (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) sub) = (Kind.Term.args16 (Kind.Term.fill x0 sub) (Kind.Term.fill x1 sub) (Kind.Term.fill x2 sub) (Kind.Term.fill x3 sub) (Kind.Term.fill x4 sub) (Kind.Term.fill x5 sub) (Kind.Term.fill x6 sub) (Kind.Term.fill x7 sub) (Kind.Term.fill x8 sub) (Kind.Term.fill x9 sub) (Kind.Term.fill x10 sub) (Kind.Term.fill x11 sub) (Kind.Term.fill x12 sub) (Kind.Term.fill x13 sub) (Kind.Term.fill x14 sub) (Kind.Term.fill x15 sub))
(Kind.Term.fill (Kind.Term.hol orig numb) sub) = let substRes = (Kind.Subst.look sub numb); (Maybe.match substRes (Kind.Term.hol orig numb) @substRes.value (Kind.Term.fill substRes.value sub))
// Kind.Term.eval_let (orig: U60) (name: U60) (expr: (Kind.Term)) (body: (_: (Kind.Term)) (Kind.Term)) : (Kind.Term)
(Kind.Term.eval_let orig name expr body) = (body expr)
// Kind.Term.eval_sub (orig: U60) (name: U60) (indx: U60) (redx: U60) (expr: (Kind.Term)) : (Kind.Term)
(Kind.Term.eval_sub orig name indx redx expr) = expr
// Kind.Term.eval_ann (orig: U60) (expr: (Kind.Term)) (type: (Kind.Term)) : (Kind.Term)
(Kind.Term.eval_ann orig expr type) = expr
// 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)
// Bool.and (a: (Bool)) (b: (Bool)) : (Bool)
(Bool.and (Bool.true) b) = b
(Bool.and (Bool.false) b) = (Bool.false)
// 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.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)
@ -628,26 +481,125 @@
(Kind.Operator.equal (Kind.Operator.neq) (Kind.Operator.neq)) = (Bool.true)
(Kind.Operator.equal a b) = (Bool.false)
// 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.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.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.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.Checker.get_equations : (Kind.Checker (List (Kind.Equation)))
(Kind.Checker.get_equations) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs eqts)
// 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.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.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)
// 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.with_context -(a: Type) (checker: (Kind.Checker a)) (context: (Kind.Context)) : (Kind.Checker a)
(Kind.Checker.with_context checker new_context) = (Kind.Checker.bind (Kind.Checker.set_context new_context) @old_context (Kind.Checker.bind checker @got (Kind.Checker.bind (Kind.Checker.set_context old_context) @_ (Kind.Checker.pure got))))
// Kind.Checker.set_context (new_context: (Kind.Context)) : (Kind.Checker (Kind.Context))
(Kind.Checker.set_context new_context) = @old_context @depth @rhs @subst @eqts @errs (Kind.Result.checked new_context depth rhs subst eqts errs old_context)
// 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)
(Kind.Term.eval (Kind.Term.hol orig numb)) = (Kind.Term.hol orig numb)
(Kind.Term.eval (Kind.Term.all orig name typ body)) = (Kind.Term.all orig name (Kind.Term.eval typ) @x (Kind.Term.eval (body x)))
(Kind.Term.eval (Kind.Term.lam orig name body)) = (Kind.Term.lam orig name @x (Kind.Term.eval (body x)))
(Kind.Term.eval (Kind.Term.let orig name expr body)) = (Kind.Term.eval_let orig name (Kind.Term.eval expr) @x (Kind.Term.eval (body x)))
(Kind.Term.eval (Kind.Term.ann orig expr typ)) = (Kind.Term.eval_ann orig (Kind.Term.eval expr) (Kind.Term.eval typ))
(Kind.Term.eval (Kind.Term.sub orig name indx redx expr)) = (Kind.Term.eval_sub orig name indx redx (Kind.Term.eval expr))
(Kind.Term.eval (Kind.Term.app orig expr typ)) = (Kind.Term.eval_app orig (Kind.Term.eval expr) (Kind.Term.eval typ))
(Kind.Term.eval (Kind.Term.hlp orig)) = (Kind.Term.hlp orig)
(Kind.Term.eval (Kind.Term.u60 orig)) = (Kind.Term.u60 orig)
(Kind.Term.eval (Kind.Term.num orig num)) = (Kind.Term.num orig num)
(Kind.Term.eval (Kind.Term.op2 orig op left right)) = (Kind.Term.eval_op orig op (Kind.Term.eval left) (Kind.Term.eval right))
(Kind.Term.eval (Kind.Term.ct0 ctid orig)) = (Kind.Term.ct0 ctid orig)
(Kind.Term.eval (Kind.Term.ct1 ctid orig x0)) = (Kind.Term.ct1 ctid orig (Kind.Term.eval x0))
(Kind.Term.eval (Kind.Term.ct2 ctid orig x0 x1)) = (Kind.Term.ct2 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1))
(Kind.Term.eval (Kind.Term.ct3 ctid orig x0 x1 x2)) = (Kind.Term.ct3 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2))
(Kind.Term.eval (Kind.Term.ct4 ctid orig x0 x1 x2 x3)) = (Kind.Term.ct4 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3))
(Kind.Term.eval (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4)) = (Kind.Term.ct5 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4))
(Kind.Term.eval (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5)) = (Kind.Term.ct6 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5))
(Kind.Term.eval (Kind.Term.ct7 ctid orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Term.ct7 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6))
(Kind.Term.eval (Kind.Term.ct8 ctid orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Term.ct8 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7))
(Kind.Term.eval (Kind.Term.ct9 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Term.ct9 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8))
(Kind.Term.eval (Kind.Term.ct10 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Term.ct10 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9))
(Kind.Term.eval (Kind.Term.ct11 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Term.ct11 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10))
(Kind.Term.eval (Kind.Term.ct12 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Term.ct12 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11))
(Kind.Term.eval (Kind.Term.ct13 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Term.ct13 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11) (Kind.Term.eval x12))
(Kind.Term.eval (Kind.Term.ct14 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Term.ct14 ctid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11) (Kind.Term.eval x12) (Kind.Term.eval x13))
(Kind.Term.eval (Kind.Term.ct15 fnid orig x0)) = (Kind.Term.ct15 fnid orig (Kind.Term.eval x0))
(Kind.Term.eval (Kind.Term.ct16 fnid orig x0)) = (Kind.Term.ct16 fnid orig (Kind.Term.eval x0))
(Kind.Term.eval (Kind.Term.fn0 fnid orig)) = (Kind.Term.FN0 fnid orig)
(Kind.Term.eval (Kind.Term.fn1 fnid orig x0)) = (Kind.Term.FN1 fnid orig (Kind.Term.eval x0))
(Kind.Term.eval (Kind.Term.fn2 fnid orig x0 x1)) = (Kind.Term.FN2 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1))
(Kind.Term.eval (Kind.Term.fn3 fnid orig x0 x1 x2)) = (Kind.Term.FN3 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2))
(Kind.Term.eval (Kind.Term.fn4 fnid orig x0 x1 x2 x3)) = (Kind.Term.FN4 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3))
(Kind.Term.eval (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4)) = (Kind.Term.FN5 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4))
(Kind.Term.eval (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5)) = (Kind.Term.FN6 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5))
(Kind.Term.eval (Kind.Term.fn7 fnid orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Term.FN7 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6))
(Kind.Term.eval (Kind.Term.fn8 fnid orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Term.FN8 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7))
(Kind.Term.eval (Kind.Term.fn9 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Term.FN9 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8))
(Kind.Term.eval (Kind.Term.fn10 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Term.FN10 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9))
(Kind.Term.eval (Kind.Term.fn11 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Term.FN11 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10))
(Kind.Term.eval (Kind.Term.fn12 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Term.FN12 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11))
(Kind.Term.eval (Kind.Term.fn13 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Term.FN13 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11) (Kind.Term.eval x12))
(Kind.Term.eval (Kind.Term.fn14 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Term.FN14 fnid orig (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11) (Kind.Term.eval x12) (Kind.Term.eval x13))
(Kind.Term.eval (Kind.Term.fn15 fnid orig x0)) = (Kind.Term.FN15 fnid orig (Kind.Term.eval x0))
(Kind.Term.eval (Kind.Term.fn16 fnid orig x0)) = (Kind.Term.FN16 fnid orig (Kind.Term.eval x0))
(Kind.Term.eval (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)) = (Kind.Term.args15 (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11) (Kind.Term.eval x12) (Kind.Term.eval x13) (Kind.Term.eval x14))
(Kind.Term.eval (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)) = (Kind.Term.args16 (Kind.Term.eval x0) (Kind.Term.eval x1) (Kind.Term.eval x2) (Kind.Term.eval x3) (Kind.Term.eval x4) (Kind.Term.eval x5) (Kind.Term.eval x6) (Kind.Term.eval x7) (Kind.Term.eval x8) (Kind.Term.eval x9) (Kind.Term.eval x10) (Kind.Term.eval x11) (Kind.Term.eval x12) (Kind.Term.eval x13) (Kind.Term.eval x14) (Kind.Term.eval x15))
// Kind.Term.eval_op (orig: U60) (op: (Kind.Operator)) (left: (Kind.Term)) (right: (Kind.Term)) : (Kind.Term)
(Kind.Term.eval_op orig (Kind.Operator.add) (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 (Kind.Operator.sub) (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 (Kind.Operator.mul) (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 (Kind.Operator.div) (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 (Kind.Operator.mod) (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 (Kind.Operator.and) (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 (Kind.Operator.or) (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 (Kind.Operator.xor) (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 (Kind.Operator.shl) (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 (Kind.Operator.shr) (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 (Kind.Operator.ltn) (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 (Kind.Operator.lte) (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 (Kind.Operator.eql) (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 (Kind.Operator.gte) (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 (Kind.Operator.gtn) (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 (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.run -(t: Type) (checker: (Kind.Checker t)) (rhs: (Bool)) : (Kind.Result t)
(Kind.Checker.run checker rhs) = ((((((checker (Kind.Context.empty)) 0) rhs) (Kind.Subst.end)) (List.nil)) (List.nil))
// 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.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.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.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))
@ -697,6 +649,9 @@
(Kind.Term.get_origin (Kind.Term.fn15 fnid orig args) got) = ((got orig) (Kind.Term.fn15 fnid orig args))
(Kind.Term.get_origin (Kind.Term.fn16 fnid orig args) got) = ((got orig) (Kind.Term.fn16 fnid orig args))
// 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.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)))))
@ -708,6 +663,9 @@
// 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_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.infer_args (args: (Kind.Term)) : (_: (Kind.Term)) (_: U60) (Kind.Term)
(Kind.Checker.infer_args (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)) = @term @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.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 term x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12) x13) x14)
(Kind.Checker.infer_args (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)) = @term @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.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 term x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12) x13) x14) x15)
@ -779,9 +737,6 @@
(List.at.u60 (List.cons head tail) 0) = (Maybe.some head)
(List.at.u60 (List.cons head tail) idx) = (List.at.u60 tail (- idx 1))
// 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.replace (term: (Kind.Term)) (index: U60) (value: (Kind.Term)) : (Kind.Term)
(Kind.Term.replace (Kind.Term.typ orig) idx val) = (Kind.Term.typ orig)
(Kind.Term.replace (Kind.Term.var orig name index) idx val) = (Bool.if (U60.equal idx index) val (Kind.Term.var orig name index))
@ -829,10 +784,6 @@
(Kind.Term.replace (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) idx val) = (Kind.Term.args16 (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val) (Kind.Term.replace x8 idx val) (Kind.Term.replace x9 idx val) (Kind.Term.replace x10 idx val) (Kind.Term.replace x11 idx val) (Kind.Term.replace x12 idx val) (Kind.Term.replace x13 idx val) (Kind.Term.replace x14 idx val) (Kind.Term.replace x15 idx val))
(Kind.Term.replace (Kind.Term.hol orig numb) idx val) = (Kind.Term.hol orig numb)
// 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.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))
@ -840,12 +791,19 @@
(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.run -(t: Type) (checker: (Kind.Checker t)) (rhs: (Bool)) : (Kind.Result t)
(Kind.Checker.run checker rhs) = ((((((checker (Kind.Context.empty)) 0) rhs) (Kind.Subst.end)) (List.nil)) (List.nil))
// 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
// String.is_nil (xs: (String)) : (Bool)
(String.is_nil "") = (Bool.true)
(String.is_nil (String.cons x xs)) = (Bool.false)
// 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))
// List.reverse -(a: Type) (xs: (List a)) : (List a)
(List.reverse xs) = (List.reverse.go xs (List.nil))
// List.reverse.go -(a: Type) (xs: (List a)) (ys: (List a)) : (List a)
(List.reverse.go (List.nil) ys) = ys
(List.reverse.go (List.cons x xs) ys) = (List.reverse.go xs (List.cons x ys))
// Kind.API.output (res: (List (Pair U60 (List (Kind.Result (Unit)))))) : (String)
(Kind.API.output (List.nil)) = ""
@ -873,13 +831,6 @@
// 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.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)
// 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
@ -888,6 +839,10 @@
// String.cut (str: (String)) : (String)
(String.cut str) = (String.cut.go str "(...)" 2048)
// 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)
// 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)))))))
@ -902,6 +857,10 @@
// 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.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))
@ -909,10 +868,6 @@
// 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))
// U60.max (fst: U60) (snd: U60) : U60
(U60.max fst snd) = (U60.if (> fst snd) fst snd)
@ -920,19 +875,63 @@
(String.length "") = (Nat.zero)
(String.length (String.cons x xs)) = (Nat.succ (String.length xs))
// Nat.to_u60 (n: (Nat)) : U60
(Nat.to_u60 (Nat.zero)) = 0
(Nat.to_u60 (Nat.succ n)) = (+ 1 (Nat.to_u60 n))
// 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))
// U60.to_nat (x: U60) : (Nat)
(U60.to_nat 0) = (Nat.zero)
(U60.to_nat n) = (Nat.succ (U60.to_nat (- n 1)))
// List.reverse -(a: Type) (xs: (List a)) : (List a)
(List.reverse xs) = (List.reverse.go xs (List.nil))
// List.reverse.go -(a: Type) (xs: (List a)) (ys: (List a)) : (List a)
(List.reverse.go (List.nil) ys) = ys
(List.reverse.go (List.cons x xs) ys) = (List.reverse.go xs (List.cons x ys))
// 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.set_origin (new_origin: U60) (term: (Kind.Term)) : (Kind.Term)
(Kind.Term.set_origin new_origin (Kind.Term.typ old_orig)) = (Kind.Term.typ new_origin)
(Kind.Term.set_origin new_origin (Kind.Term.var old_orig name idx)) = (Kind.Term.var new_origin name idx)
(Kind.Term.set_origin new_origin (Kind.Term.hol old_orig numb)) = (Kind.Term.hol new_origin numb)
(Kind.Term.set_origin new_origin (Kind.Term.all old_orig name typ body)) = (Kind.Term.all new_origin name typ body)
(Kind.Term.set_origin new_origin (Kind.Term.lam old_orig name body)) = (Kind.Term.lam new_origin name body)
(Kind.Term.set_origin new_origin (Kind.Term.let old_orig name expr body)) = (Kind.Term.let new_origin name expr body)
(Kind.Term.set_origin new_origin (Kind.Term.ann old_orig expr typ)) = (Kind.Term.ann new_origin expr typ)
(Kind.Term.set_origin new_origin (Kind.Term.sub old_orig name indx redx expr)) = (Kind.Term.sub new_origin name indx redx expr)
(Kind.Term.set_origin new_origin (Kind.Term.app old_orig func arg)) = (Kind.Term.app new_origin func arg)
(Kind.Term.set_origin new_origin (Kind.Term.hlp old_orig)) = (Kind.Term.hlp new_origin)
(Kind.Term.set_origin new_origin (Kind.Term.u60 old_orig)) = (Kind.Term.u60 new_origin)
(Kind.Term.set_origin new_origin (Kind.Term.num old_orig num)) = (Kind.Term.num new_origin num)
(Kind.Term.set_origin new_origin (Kind.Term.op2 old_orig op left right)) = (Kind.Term.op2 new_origin op left right)
(Kind.Term.set_origin new_origin (Kind.Term.ct0 ctid old_orig)) = (Kind.Term.ct0 ctid new_origin)
(Kind.Term.set_origin new_origin (Kind.Term.ct1 ctid old_orig x0)) = (Kind.Term.ct1 ctid new_origin x0)
(Kind.Term.set_origin new_origin (Kind.Term.ct2 ctid old_orig x0 x1)) = (Kind.Term.ct2 ctid new_origin x0 x1)
(Kind.Term.set_origin new_origin (Kind.Term.ct3 ctid old_orig x0 x1 x2)) = (Kind.Term.ct3 ctid new_origin x0 x1 x2)
(Kind.Term.set_origin new_origin (Kind.Term.ct4 ctid old_orig x0 x1 x2 x3)) = (Kind.Term.ct4 ctid new_origin x0 x1 x2 x3)
(Kind.Term.set_origin new_origin (Kind.Term.ct5 ctid old_orig x0 x1 x2 x3 x4)) = (Kind.Term.ct5 ctid new_origin x0 x1 x2 x3 x4)
(Kind.Term.set_origin new_origin (Kind.Term.ct6 ctid old_orig x0 x1 x2 x3 x4 x5)) = (Kind.Term.ct6 ctid new_origin x0 x1 x2 x3 x4 x5)
(Kind.Term.set_origin new_origin (Kind.Term.ct7 ctid old_orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Term.ct7 ctid new_origin x0 x1 x2 x3 x4 x5 x6)
(Kind.Term.set_origin new_origin (Kind.Term.ct8 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Term.ct8 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7)
(Kind.Term.set_origin new_origin (Kind.Term.ct9 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Term.ct9 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8)
(Kind.Term.set_origin new_origin (Kind.Term.ct10 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Term.ct10 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)
(Kind.Term.set_origin new_origin (Kind.Term.ct11 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Term.ct11 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)
(Kind.Term.set_origin new_origin (Kind.Term.ct12 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Term.ct12 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)
(Kind.Term.set_origin new_origin (Kind.Term.ct13 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Term.ct13 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)
(Kind.Term.set_origin new_origin (Kind.Term.ct14 ctid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Term.ct14 ctid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)
(Kind.Term.set_origin new_origin (Kind.Term.ct15 ctid old_orig args)) = (Kind.Term.ct15 ctid new_origin args)
(Kind.Term.set_origin new_origin (Kind.Term.ct16 ctid old_orig args)) = (Kind.Term.ct16 ctid new_origin args)
(Kind.Term.set_origin new_origin (Kind.Term.fn0 fnid old_orig)) = (Kind.Term.fn0 fnid new_origin)
(Kind.Term.set_origin new_origin (Kind.Term.fn1 fnid old_orig x0)) = (Kind.Term.fn1 fnid new_origin x0)
(Kind.Term.set_origin new_origin (Kind.Term.fn2 fnid old_orig x0 x1)) = (Kind.Term.fn2 fnid new_origin x0 x1)
(Kind.Term.set_origin new_origin (Kind.Term.fn3 fnid old_orig x0 x1 x2)) = (Kind.Term.fn3 fnid new_origin x0 x1 x2)
(Kind.Term.set_origin new_origin (Kind.Term.fn4 fnid old_orig x0 x1 x2 x3)) = (Kind.Term.fn4 fnid new_origin x0 x1 x2 x3)
(Kind.Term.set_origin new_origin (Kind.Term.fn5 fnid old_orig x0 x1 x2 x3 x4)) = (Kind.Term.fn5 fnid new_origin x0 x1 x2 x3 x4)
(Kind.Term.set_origin new_origin (Kind.Term.fn6 fnid old_orig x0 x1 x2 x3 x4 x5)) = (Kind.Term.fn6 fnid new_origin x0 x1 x2 x3 x4 x5)
(Kind.Term.set_origin new_origin (Kind.Term.fn7 fnid old_orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Term.fn7 fnid new_origin x0 x1 x2 x3 x4 x5 x6)
(Kind.Term.set_origin new_origin (Kind.Term.fn8 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Term.fn8 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7)
(Kind.Term.set_origin new_origin (Kind.Term.fn9 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Term.fn9 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8)
(Kind.Term.set_origin new_origin (Kind.Term.fn10 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Term.fn10 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)
(Kind.Term.set_origin new_origin (Kind.Term.fn11 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Term.fn11 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)
(Kind.Term.set_origin new_origin (Kind.Term.fn12 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Term.fn12 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)
(Kind.Term.set_origin new_origin (Kind.Term.fn13 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Term.fn13 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)
(Kind.Term.set_origin new_origin (Kind.Term.fn14 fnid old_orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Term.fn14 fnid new_origin x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)
(Kind.Term.set_origin new_origin (Kind.Term.fn15 ctid old_orig args)) = (Kind.Term.fn15 ctid new_origin args)
(Kind.Term.set_origin new_origin (Kind.Term.fn16 ctid old_orig args)) = (Kind.Term.fn16 ctid new_origin args)

18
src/driver.rs
View File

@ -106,20 +106,20 @@ pub fn run_with_hvm(code: &str, main: &str, read_string: bool) -> Result<RunResu
})
}
pub fn cmd_to_hvm(config: Config, path: &str) -> Result<(), String> {
pub fn cmd_to_hvm(config: &Config, path: &str) -> Result<(), String> {
let loaded = load(config, path)?;
let result = codegen::hvm::to_hvm_book(&loaded.book);
print!("{}", result);
Ok(())
}
pub fn cmd_show(config: Config, path: &str) -> Result<(), String> {
pub fn cmd_show(config: &Config, path: &str) -> Result<(), String> {
let loaded = load(config, path)?;
println!("{}", loaded.book);
Ok(())
}
pub fn cmd_gen_checker(config: Config, path: &str) -> Result<(), String> {
pub fn cmd_gen_checker(config: &Config, path: &str) -> Result<(), String> {
let loaded = load(config, path)?;
let gen_path = format!("{}.hvm", path.replace(".kind2", ".check"));
println!("Generated '{}'.", gen_path);
@ -127,7 +127,7 @@ pub fn cmd_gen_checker(config: Config, path: &str) -> Result<(), String> {
Ok(())
}
pub fn cmd_derive(config: Config, path: &str) -> Result<(), String> {
pub fn cmd_derive(config: &Config, path: &str) -> Result<(), String> {
let color = config.color_output;
let newcode = match std::fs::read_to_string(&path) {
Err(_) => {
@ -149,7 +149,7 @@ pub fn cmd_derive(config: Config, path: &str) -> Result<(), String> {
std::fs::create_dir_all(dir.parent().unwrap()).unwrap();
std::fs::write(dir, txt).ok();
}
save_derived(color, path, &new_type::derive_type(&newtype));
save_derived(color, path, &new_type::derive_type(&config.kind2_path, &newtype));
for i in 0..newtype.ctrs.len() {
save_derived(color, path, &new_type::derive_ctr(&newtype, i));
}
@ -157,7 +157,7 @@ pub fn cmd_derive(config: Config, path: &str) -> Result<(), String> {
Ok(())
}
pub fn cmd_check_all(config: Config, path: &str) -> Result<(), String> {
pub fn cmd_check_all(config: &Config, path: &str) -> Result<(), String> {
let loaded = load(config, path)?;
let result = run_with_hvm(&gen_checker(&loaded.book), "Kind.API.check_all", true)?;
print!("{}", inject_highlights(&loaded.file, &result.output));
@ -166,7 +166,7 @@ pub fn cmd_check_all(config: Config, path: &str) -> Result<(), String> {
}
// Evaluates Main on Kind2
pub fn cmd_eval_main(config: Config, path: &str) -> Result<(), String> {
pub fn cmd_eval_main(config: &Config, path: &str) -> Result<(), String> {
let loaded = load(config, path)?;
if loaded.book.entrs.contains_key(&Ident("Main".to_string())) {
let result = run_with_hvm(&gen_checker(&loaded.book), "Kind.API.eval_main", true)?;
@ -178,7 +178,7 @@ pub fn cmd_eval_main(config: Config, path: &str) -> Result<(), String> {
}
}
pub fn cmd_run_main(config: Config, path: &str) -> Result<(), String> {
pub fn cmd_run_main(config: &Config, path: &str) -> Result<(), String> {
let loaded = load(config, path)?;
if loaded.book.entrs.contains_key(&Ident("Main".to_string())) {
let result = codegen::hvm::to_hvm_book(&loaded.book);
@ -191,7 +191,7 @@ pub fn cmd_run_main(config: Config, path: &str) -> Result<(), String> {
}
}
pub fn cmd_to_kdl(config: Config, path: &str) -> Result<(), String> {
pub fn cmd_to_kdl(config: &Config, path: &str) -> Result<(), String> {
let loaded = load(config, path)?;
let comp_book = codegen::kdl::compile_book(&loaded.book)?;
let kdl_names = codegen::kdl::get_kdl_names(&comp_book)?;

3
src/driver/config.rs
View File

@ -1,7 +1,8 @@
// The configuration needed to customize
// the compiler experience
#[derive(Clone, Copy)]
#[derive(Clone)]
pub struct Config {
pub no_high_line: bool,
pub color_output: bool,
pub kind2_path: String
}

31
src/driver/loader.rs
View File

@ -1,3 +1,5 @@
use std::path::{Path, PathBuf};
use crate::book::name::Ident;
use crate::book::span::{FileOffset, Span, SpanData};
use crate::book::Book;
@ -26,19 +28,22 @@ impl Load {
}
}
pub fn load_entry(name: &str, load: &mut Load) -> Result<(), String> {
pub fn load_entry(config: &Config, name: &str, load: &mut Load) -> Result<(), String> {
if !load.book.entrs.contains_key(&Ident(name.to_string())) {
let path: String;
let path: PathBuf;
if name.ends_with(".kind2") {
path = name.to_string();
path = PathBuf::from(&name.to_string());
} else {
let inside_path = format!("{}/_.kind2", &name.replace('.', "/")); // path ending with 'Name/_.kind'
let normal_path = format!("{}.kind2", &name.replace('.', "/")); // path ending with 'Name.kind'
if std::path::Path::new(&inside_path).is_file() {
if std::path::Path::new(&normal_path).is_file() {
let root = Path::new(&config.kind2_path).join(&name.replace('.', "/"));
let inside_path = root.clone().join("_.kind2"); // path ending with 'Name/_.kind'
let mut normal_path = root.clone(); // path ending with 'Name.kind'
normal_path.set_extension("kind2");
if inside_path.is_file() {
if normal_path.is_file() {
return Err(format!(
"The following files can't exist simultaneously:\n- {}\n- {}\nPlease delete one and try again.",
inside_path, normal_path
inside_path.display(), normal_path.display()
));
}
path = inside_path;
@ -56,34 +61,34 @@ pub fn load_entry(name: &str, load: &mut Load) -> Result<(), String> {
let mut new_book = match read_book(&newcode) {
Err(err) => {
return Err(format!("\x1b[1m[{}]\x1b[0m\n{}", path, err));
return Err(format!("\x1b[1m[{}]\x1b[0m\n{}", path.display(), err));
}
Ok(book) => book,
};
new_book.set_origin_file(FileOffset(load.file.len() as u32));
load.file.push(File { path, code: newcode });
load.file.push(File { path: path.to_str().unwrap().into(), code: newcode });
for name in &new_book.names {
load.book.names.push(name.clone());
load.book.entrs.insert(Ident(name.clone()), new_book.entrs.get(&Ident(name.to_string())).unwrap().clone());
}
for unbound in &new_book.get_unbounds() {
load_entry(&unbound.0, load)?;
load_entry(config, &unbound.0, load)?;
}
}
Ok(())
}
pub fn load(config: Config, name: &str) -> Result<Load, String> {
pub fn load(config: &Config, name: &str) -> Result<Load, String> {
let mut load = Load::new_empty();
if !std::path::Path::new(name).is_file() {
return Err(format!("File not found: '{}'", name));
}
load_entry(name, &mut load)?;
load_entry(config, name, &mut load)?;
match load.book.adjust() {
Ok(book) => {

12
src/lowering/load.rs
View File

@ -3,21 +3,27 @@ use crate::book::new_type::NewType;
use crate::parser::new_type::read_newtype;
use std::collections::HashMap;
use std::path::Path;
use std::rc::Rc;
use std::env;
// TODO: Remove this from the adjust layer. I think that we need to move it
// to the driver.
fn load_newtype(name: &Ident) -> Result<Box<NewType>, String> {
let path = format!("{}/_.type", name.to_string().replace('.', "/"));
let path = env::var_os("KIND2_PATH").map(|x| x.into_string().unwrap()).unwrap_or("".to_string());
let root = Path::new(&path).join(name.to_string().replace('.', "/"));
let path = root.clone().join("_.type");
let newcode = match std::fs::read_to_string(&path) {
Err(_) => {
return Err(format!("File not found: '{}'.", path));
return Err(format!("File not found: '{}'.", path.display()));
}
Ok(code) => code,
};
let newtype = match read_newtype(&newcode) {
Err(err) => {
return Err(format!("\x1b[1m[{}]\x1b[0m\n{}", path, err));
return Err(format!("\x1b[1m[{}]\x1b[0m\n{}", path.display(), err));
}
Ok(book) => book,
};

26
src/main.rs
View File

@ -5,6 +5,8 @@ pub mod lowering;
pub mod parser;
pub mod codegen;
use std::env;
use crate::driver::*;
use crate::driver::config::Config;
@ -17,10 +19,10 @@ pub struct Cli {
#[clap(subcommand)]
pub command: Command,
#[clap(short, long, value_parser, default_value_t = false)]
#[clap(aliases=&["nhl"], long, value_parser, default_value_t = false)]
pub no_high_line: bool,
#[clap(short, long, value_parser, default_value_t = true)]
#[clap(aliases=&["co"], long, value_parser, default_value_t = true)]
pub color_output: bool
}
@ -62,20 +64,22 @@ pub enum Command {
fn run_cli() -> Result<(), String> {
let cli_matches = Cli::parse();
let config = Config {
no_high_line: cli_matches.no_high_line,
color_output: cli_matches.color_output
color_output: cli_matches.color_output,
kind2_path: env::var_os("KIND2_PATH").map(|x| x.into_string().unwrap()).unwrap_or("".to_string())
};
match cli_matches.command {
Command::Eval { file: path } => cmd_eval_main(config, &path),
Command::Run { file: path } => cmd_run_main(config, &path),
Command::Check { file: path } => cmd_check_all(config, &path),
Command::Derive { file: path } => cmd_derive(config, &path),
Command::GenChecker { file: path } => cmd_gen_checker(config, &path),
Command::Show { file: path } => cmd_show(config, &path),
Command::ToKDL { file: path } => cmd_to_kdl(config, &path),
Command::ToHVM { file: path } => cmd_to_hvm(config, &path),
Command::Eval { file: path } => cmd_eval_main(&config, &path),
Command::Run { file: path } => cmd_run_main(&config, &path),
Command::Check { file: path } => cmd_check_all(&config, &path),
Command::Derive { file: path } => cmd_derive(&config, &path),
Command::GenChecker { file: path } => cmd_gen_checker(&config, &path),
Command::Show { file: path } => cmd_show(&config, &path),
Command::ToKDL { file: path } => cmd_to_kdl(&config, &path),
Command::ToHVM { file: path } => cmd_to_hvm(&config, &path),
}
}

9
src/parser/new_type.rs
View File

@ -1,3 +1,5 @@
use std::path::Path;
use crate::book::new_type::{Constructor, Derived, NewType};
use crate::book::{Argument, Entry, Rule};
use crate::book::name::Ident;
@ -5,8 +7,9 @@ use crate::book::span::Span;
use crate::book::term::Term;
use crate::parser::*;
pub fn derive_type(tipo: &NewType) -> Derived {
let path = format!("{}/_.kind2", tipo.name.to_path());
pub fn derive_type(path: &str, tipo: &NewType) -> Derived {
let root = Path::new(path).join(tipo.name.to_path());
let path = root.clone().join("_.kind2");
let name = format!("{}", tipo.name);
let kdln = None;
let mut args = vec![];
@ -29,7 +32,7 @@ pub fn derive_type(tipo: &NewType) -> Derived {
tipo,
rules,
};
Derived { path: Ident(path), entr }
Derived { path: Ident(path.to_str().unwrap().to_string()), entr }
}
pub fn derive_ctr(tipo: &NewType, index: usize) -> Derived {