|
|
|
@ -1,111 +1,4 @@
|
|
|
|
|
(Main) = let imports = [(Dynamic.new λa λb (Kind.Term.set_origin a b)), (Dynamic.new (Kind.API.check_all)), (Dynamic.new (Kind.API.eval_main))]; (Kind.API.check_all)
|
|
|
|
|
(Kind.API.eval_main) = (Kind.Printer.text [(Kind.Term.show (Kind.Term.FN0 (Main.) 0)), (String.new_line), (String.new_line)])
|
|
|
|
|
(String.new_line) = (String.pure (Char.newline))
|
|
|
|
|
(String.pure x) = (String.cons x "")
|
|
|
|
|
(Char.newline) = 10
|
|
|
|
|
(Kind.Printer.text []) = ""
|
|
|
|
|
(Kind.Printer.text (List.cons x xs)) = (String.concat x (Kind.Printer.text xs))
|
|
|
|
|
(String.concat (String.cons x xs) ys) = (String.cons x (String.concat xs ys))
|
|
|
|
|
(String.concat "" ys) = ys
|
|
|
|
|
(Kind.Term.show term) = let sugars = [(Kind.Term.show.sugar.string term), (Kind.Term.show.sugar.list term), (Kind.Term.show.sugar.sigma term)]; (Maybe.try sugars (Kind.Term.show.go term))
|
|
|
|
|
(Kind.Term.show.sugar.list term) = (Maybe.bind (Kind.Term.show.sugar.list.go term) λres (Maybe.pure (Kind.Printer.text ["[", (String.join " " res), "]"])))
|
|
|
|
|
(Kind.Term.show.sugar.list.go (Kind.Term.ct0 (List.nil.) orig)) = (Maybe.some [])
|
|
|
|
|
(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)))
|
|
|
|
|
(Kind.Term.show.sugar.list.go other) = (Maybe.none)
|
|
|
|
|
(Maybe.pure x) = (Maybe.some x)
|
|
|
|
|
(Maybe.bind (Maybe.none) mb) = (Maybe.none)
|
|
|
|
|
(Maybe.bind (Maybe.some val) mb) = (mb val)
|
|
|
|
|
(String.join sep list) = (String.intercalate sep list)
|
|
|
|
|
(String.intercalate sep xs) = (String.flatten (List.intersperse sep xs))
|
|
|
|
|
(List.intersperse sep []) = []
|
|
|
|
|
(List.intersperse sep [xh]) = (List.pure xh)
|
|
|
|
|
(List.intersperse sep (List.cons xh xt)) = (List.cons xh (List.cons sep (List.intersperse sep xt)))
|
|
|
|
|
(List.pure x) = [x]
|
|
|
|
|
(String.flatten []) = ""
|
|
|
|
|
(String.flatten (List.cons head tail)) = (String.concat head (String.flatten tail))
|
|
|
|
|
(Kind.Term.show.sugar.string term) = (Maybe.bind (Kind.Term.show.sugar.string.go term) λres let quot = (String.cons 34 ""); (Maybe.pure (Kind.Printer.text [quot, res, quot])))
|
|
|
|
|
(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.u60 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 (Kind.Term.ct2 (Sigma.) orig typ (Kind.Term.lam orig_ name body))) = (Maybe.some (Kind.Printer.text ["([", (Kind.Name.show name), ": ", (Kind.Term.show typ), "] -> ", (Kind.Term.show (body (Kind.Term.var orig_ name 0))), ")"]))
|
|
|
|
|
(Kind.Term.show.sugar.sigma term) = (Maybe.none)
|
|
|
|
|
(Kind.Name.show name) = (Kind.Name.show.go name "")
|
|
|
|
|
(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)))
|
|
|
|
|
(U60.if 0 t f) = f
|
|
|
|
|
(U60.if n t f) = t
|
|
|
|
|
(Maybe.try [] alt) = alt
|
|
|
|
|
(Maybe.try (List.cons maybe xs) alt) = (Maybe.match maybe (Maybe.try xs alt) λvalue value)
|
|
|
|
|
(Maybe.match (Maybe.none) none some) = none
|
|
|
|
|
(Maybe.match (Maybe.some value_) none some) = (some value_)
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.typ orig)) = "Type"
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.var orig name index)) = (Kind.Printer.text [(Kind.Name.show name)])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.hol orig numb)) = (Kind.Printer.text ["_"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.all orig name type body)) = (Kind.Term.show.forall orig name type body)
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.lam orig name body)) = (Kind.Printer.text ["(", (Kind.Name.show name), " => ", (Kind.Term.show (body (Kind.Term.var orig name 0))), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.let orig name exp body)) = (Kind.Printer.text ["let ", (Kind.Name.show name), " = ", (Kind.Term.show exp), "; ", (Kind.Term.show (body (Kind.Term.var orig name 0)))])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ann orig expr type)) = (Kind.Printer.text ["{", (Kind.Term.show expr), " :: ", (Kind.Term.show type), "}"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.sub orig name indx redx expr)) = (Kind.Printer.text [(Kind.Term.show expr), " ## ", (Kind.Name.show name), "/", (Show.to_string (U60.show redx))])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.app orig func argm)) = (Kind.Printer.text ["(", (Kind.Term.show func), " ", (Kind.Term.show argm), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct0 ctid orig)) = (NameOf ctid)
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct1 ctid orig x0)) = (Kind.Printer.text ["(", (NameOf ctid), " ", (Kind.Term.show x0), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct2 ctid orig x0 x1)) = (Kind.Printer.text ["(", (NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct3 ctid orig x0 x1 x2)) = (Kind.Printer.text ["(", (NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct4 ctid orig x0 x1 x2 x3)) = (Kind.Printer.text ["(", (NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4)) = (Kind.Printer.text ["(", (NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5)) = (Kind.Printer.text ["(", (NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct7 ctid orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Printer.text ["(", (NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct8 ctid orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Printer.text ["(", (NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct9 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Printer.text ["(", (NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct10 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Printer.text ["(", (NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct11 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Printer.text ["(", (NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct12 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Printer.text ["(", (NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct13 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Printer.text ["(", (NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct14 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Printer.text ["(", (NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), " ", (Kind.Term.show x13), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct15 ctid orig x0)) = (Kind.Printer.text ["(", (NameOf ctid), " ", (Kind.Term.show x0), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct16 ctid orig x0)) = (Kind.Printer.text ["(", (NameOf ctid), " ", (Kind.Term.show x0), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn0 fnid orig)) = (NameOf fnid)
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn1 fnid orig x0)) = (Kind.Printer.text ["(", (NameOf fnid), " ", (Kind.Term.show x0), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn2 fnid orig x0 x1)) = (Kind.Printer.text ["(", (NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn3 fnid orig x0 x1 x2)) = (Kind.Printer.text ["(", (NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn4 fnid orig x0 x1 x2 x3)) = (Kind.Printer.text ["(", (NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4)) = (Kind.Printer.text ["(", (NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5)) = (Kind.Printer.text ["(", (NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn7 fnid orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Printer.text ["(", (NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn8 fnid orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Printer.text ["(", (NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn9 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Printer.text ["(", (NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn10 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Printer.text ["(", (NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn11 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Printer.text ["(", (NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn12 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Printer.text ["(", (NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn13 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Printer.text ["(", (NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn14 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Printer.text ["(", (NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), " ", (Kind.Term.show x13), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn15 fnid orig x0)) = (Kind.Printer.text ["(", (NameOf fnid), " ", (Kind.Term.show x0), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn16 fnid orig x0)) = (Kind.Printer.text ["(", (NameOf fnid), " ", (Kind.Term.show x0), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)) = (Kind.Printer.text [(Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), " ", (Kind.Term.show x13), " ", (Kind.Term.show x14)])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)) = (Kind.Printer.text [(Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), " ", (Kind.Term.show x13), " ", (Kind.Term.show x14), " ", (Kind.Term.show x15)])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.hlp orig)) = "?"
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.U60 orig)) = "U60"
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.u60 orig numb)) = (Show.to_string (U60.show numb))
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.op2 orig operator left right)) = (Kind.Printer.text ["(", (Kind.Operator.show operator), " ", (Kind.Term.show left), " ", (Kind.Term.show right), ")"])
|
|
|
|
|
(Show.to_string show) = (show "")
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.add)) = "+"
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.sub)) = "-"
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.mul)) = "*"
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.div)) = "/"
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.mod)) = "%"
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.and)) = "&"
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.or)) = "|"
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.xor)) = "^"
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.shl)) = "<<"
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.shr)) = ">>"
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.ltn)) = "<"
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.lte)) = "<="
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.eql)) = "=="
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.gte)) = ">="
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.gtn)) = ">"
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.neq)) = "!="
|
|
|
|
|
(Kind.Term.show.forall orig name type body) = (U60.if (== name 63) (Kind.Printer.text ["(", (Kind.Term.show type), " -> ", (Kind.Term.show (body (Kind.Term.var orig name 0))), ")"]) (Kind.Printer.text ["((", (Kind.Name.show name), ": ", (Kind.Term.show type), ") -> ", (Kind.Term.show (body (Kind.Term.var orig name 0))), ")"]))
|
|
|
|
|
(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)
|
|
|
|
|
(Main) = let imports = [(Dynamic.new λa λb (Kind.Term.set_origin a b)), (Dynamic.new (Kind.API.check_all)), (Dynamic.new (Kind.API.eval_main)), (Dynamic.new λa (Kind.Coverage.check a))]; (Kind.API.check_all)
|
|
|
|
|
(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)
|
|
|
|
@ -153,102 +46,33 @@
|
|
|
|
|
(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)
|
|
|
|
|
(Kind.API.check_all) = let output = (Kind.API.output (List.reverse (Kind.API.check_functions (Functions)))); output
|
|
|
|
|
(Kind.API.check_all) = let output = (Kind.API.output (List.reverse (Kind.API.check_functions (Kind.Axiom.Functions)))); output
|
|
|
|
|
(List.reverse xs) = (List.reverse.go xs [])
|
|
|
|
|
(List.reverse.go [] ys) = ys
|
|
|
|
|
(List.reverse.go (List.cons x xs) ys) = (List.reverse.go xs (List.cons x ys))
|
|
|
|
|
(Kind.API.check_functions []) = []
|
|
|
|
|
(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)
|
|
|
|
|
(Kind.API.check_function fnid) = let rules = (RuleOf fnid); let type = (TypeOf fnid); let type_check = (Kind.Checker.run (Kind.Checker.unify (Kind.Checker.check type (Kind.Term.typ 0))) (Bool.true)); let rule_check = (Kind.API.check_function.rules rules (Kind.Term.eval type)); (List.cons type_check rule_check)
|
|
|
|
|
(Kind.API.check_function fnid) = let rules = (Kind.Axiom.RuleOf fnid); let type = (Kind.Axiom.TypeOf fnid); let type_check = (Kind.Checker.run (Kind.Checker.unify (Kind.Checker.check type (Kind.Term.typ 0))) (Bool.true)); let rule_check = (Kind.API.check_function.rules rules (Kind.Term.eval type)); let res = (List.cons type_check rule_check); (Bool.if (Kind.Axiom.CoverCheck fnid) let cover_check = (Kind.Checker.run (Kind.Coverage.check fnid) (Bool.true)); (List.cons cover_check res) res)
|
|
|
|
|
(Kind.Checker.unify checker) = (Kind.Checker.bind checker λx_1 (Kind.Checker.bind (Kind.Checker.get_equations) λequations (Kind.Checker.unify.go equations [] (Bool.false))))
|
|
|
|
|
(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.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.get_equations) = λcontext λdepth λrhs λsubst λeqts λerrs (Kind.Result.checked context depth rhs subst eqts errs eqts)
|
|
|
|
|
(Kind.Checker.unify.go [] [] changed) = (Kind.Checker.pure (Unit.new))
|
|
|
|
|
(Kind.Checker.unify.go [] unsolved (Bool.true)) = (Kind.Checker.unify.go unsolved [] (Bool.false))
|
|
|
|
|
(Kind.Checker.unify.go [] unsolved (Bool.false)) = (Kind.Checker.unify.go.fail unsolved)
|
|
|
|
|
(Kind.Checker.unify.go (List.cons (Kind.Equation.new ctx orig left right) equations) unsolved changed) = (Kind.Checker.bind (Kind.Checker.with_context (Kind.Checker.equal (Kind.Term.eval left) (Kind.Term.eval right)) ctx) λis_equal let unify = (Bool.if is_equal λequations λunsolved (Kind.Checker.unify.go equations unsolved (Bool.true)) λequations λunsolved let eqt = (Kind.Equation.new ctx orig left right); (Kind.Checker.unify.go equations (List.cons eqt unsolved) changed)); (unify equations unsolved))
|
|
|
|
|
(Kind.Checker.unify.go.fail []) = (Kind.Checker.pure (Unit.new))
|
|
|
|
|
(Kind.Checker.unify.go.fail (List.cons (Kind.Equation.new ctx orig left right) eqts)) = (Kind.Checker.bind (Kind.Checker.error (Kind.Error.type_mismatch ctx orig left right) (Unit.new)) λx_1 (Kind.Checker.unify.go.fail eqts))
|
|
|
|
|
(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.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.pure res) = λcontext λdepth λrhs λsubst λeqts λerrs (Kind.Result.checked context depth rhs subst eqts errs res)
|
|
|
|
|
(Kind.Checker.error err ret) = λcontext λdepth λrhs λsubst λeqts λerrs (Kind.Result.checked context depth rhs subst eqts (List.cons err errs) ret)
|
|
|
|
|
(Bool.if (Bool.true) t f) = t
|
|
|
|
|
(Bool.if (Bool.false) t f) = f
|
|
|
|
|
(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) λx_1 (Kind.Checker.pure got))))
|
|
|
|
|
(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 (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.u60 orig num)) = (Kind.Term.u60 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 name indx redx expr) = expr
|
|
|
|
|
(Kind.Term.eval_ann orig expr type) = expr
|
|
|
|
|
(Kind.Term.eval_let orig name expr body) = (body expr)
|
|
|
|
|
(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_op orig (Kind.Operator.add) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (+ a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.sub) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (- a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.mul) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (* a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.div) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (/ a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.mod) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (% a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.and) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (& a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.or) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (| a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.xor) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (^ a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.shl) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (<< a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.shr) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (>> a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.ltn) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (< a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.lte) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (<= a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.eql) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (== a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.gte) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (>= a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.gtn) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (> a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.neq) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (!= a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig op left right) = (Kind.Term.op2 orig op left right)
|
|
|
|
|
(Kind.Checker.unify.go.fail []) = (Kind.Checker.pure (Unit.new))
|
|
|
|
|
(Kind.Checker.unify.go.fail (List.cons (Kind.Equation.new ctx orig left right) eqts)) = (Kind.Checker.bind (Kind.Checker.error (Kind.Error.type_mismatch ctx orig left right) (Unit.new)) λx_1 (Kind.Checker.unify.go.fail eqts))
|
|
|
|
|
(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 res) = λcontext λdepth λrhs λsubst λeqts λerrs (Kind.Result.checked context depth rhs subst eqts errs res)
|
|
|
|
|
(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) []) λ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) []) λbody (Kind.Checker.pure body)))
|
|
|
|
|
(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))) (Kind.Axiom.Null) (Kind.Axiom.Null) []) λ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))) (Kind.Axiom.Null) (Kind.Axiom.Null) []) λ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) []) λbody (Kind.Checker.pure (Bool.and expr body)))))
|
|
|
|
|
(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))) (Kind.Axiom.Null) (Kind.Axiom.Null) []) λ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) λtype (Kind.Checker.pure (Bool.and func type))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.sub a.orig a.name a.indx a.redx a.expr) (Kind.Term.sub b.orig b.name b.indx b.redx b.expr)) = (Kind.Checker.bind (Kind.Checker.equal a.expr b.expr) λfunc (Kind.Checker.pure func))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.U60 a.orig) (Kind.Term.U60 b.orig)) = (Kind.Checker.pure (Bool.true))
|
|
|
|
@ -259,121 +83,44 @@
|
|
|
|
|
(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.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6) (Kind.Term.ct7 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6)) = 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.bind (Kind.Checker.equal a.x6 b.x6) λx6 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 x6)))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.ct8 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7) (Kind.Term.ct8 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7)) = 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.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 ctid (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.ct9 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8) (Kind.Term.ct9 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8)) = 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.bind (Kind.Checker.equal a.x6 b.x6) λx6 (Kind.Checker.bind (Kind.Checker.equal a.x7 b.x7) λx7 (Kind.Checker.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 x8)))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.ct10 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8 a.x9) (Kind.Term.ct10 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8 b.x9)) = 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.bind (Kind.Checker.equal a.x6 b.x6) λx6 (Kind.Checker.bind (Kind.Checker.equal a.x7 b.x7) λx7 (Kind.Checker.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.bind (Kind.Checker.equal a.x9 b.x9) λx9 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 (Bool.and x8 x9)))))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.ct11 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8 a.x9 a.x10) (Kind.Term.ct11 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8 b.x9 b.x10)) = 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.bind (Kind.Checker.equal a.x6 b.x6) λx6 (Kind.Checker.bind (Kind.Checker.equal a.x7 b.x7) λx7 (Kind.Checker.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.bind (Kind.Checker.equal a.x9 b.x9) λx9 (Kind.Checker.bind (Kind.Checker.equal a.x10 b.x10) λx10 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 (Bool.and x8 (Bool.and x9 x10)))))))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.ct12 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8 a.x9 a.x10 a.x11) (Kind.Term.ct12 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8 b.x9 b.x10 b.x11)) = 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.bind (Kind.Checker.equal a.x6 b.x6) λx6 (Kind.Checker.bind (Kind.Checker.equal a.x7 b.x7) λx7 (Kind.Checker.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.bind (Kind.Checker.equal a.x9 b.x9) λx9 (Kind.Checker.bind (Kind.Checker.equal a.x10 b.x10) λx10 (Kind.Checker.bind (Kind.Checker.equal a.x11 b.x11) λx11 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 (Bool.and x8 (Bool.and x9 (Bool.and x10 x11)))))))))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.ct13 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8 a.x9 a.x10 a.x11 a.x12) (Kind.Term.ct13 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8 b.x9 b.x10 b.x11 b.x12)) = 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.bind (Kind.Checker.equal a.x6 b.x6) λx6 (Kind.Checker.bind (Kind.Checker.equal a.x7 b.x7) λx7 (Kind.Checker.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.bind (Kind.Checker.equal a.x9 b.x9) λx9 (Kind.Checker.bind (Kind.Checker.equal a.x10 b.x10) λx10 (Kind.Checker.bind (Kind.Checker.equal a.x11 b.x11) λx11 (Kind.Checker.bind (Kind.Checker.equal a.x12 b.x12) λx12 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 (Bool.and x8 (Bool.and x9 (Bool.and x10 (Bool.and x11 x12)))))))))))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.ct14 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8 a.x9 a.x10 a.x11 a.x12 a.x13) (Kind.Term.ct14 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8 b.x9 b.x10 b.x11 b.x12 b.x13)) = 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.bind (Kind.Checker.equal a.x6 b.x6) λx6 (Kind.Checker.bind (Kind.Checker.equal a.x7 b.x7) λx7 (Kind.Checker.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.bind (Kind.Checker.equal a.x9 b.x9) λx9 (Kind.Checker.bind (Kind.Checker.equal a.x10 b.x10) λx10 (Kind.Checker.bind (Kind.Checker.equal a.x11 b.x11) λx11 (Kind.Checker.bind (Kind.Checker.equal a.x12 b.x12) λx12 (Kind.Checker.bind (Kind.Checker.equal a.x13 b.x13) λx13 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 (Bool.and x8 (Bool.and x9 (Bool.and x10 (Bool.and x11 (Bool.and x12 x13)))))))))))))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.ct15 a.ctid a.orig a.args) (Kind.Term.ct15 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.ct16 a.ctid a.orig a.args) (Kind.Term.ct16 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.ct0 a.ctid a.orig) (Kind.Term.ct0 b.ctid b.orig)) = let ctid = (U60.equal (Kind.Axiom.HashOf a.ctid) (Kind.Axiom.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 (Kind.Axiom.HashOf a.ctid) (Kind.Axiom.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 (Kind.Axiom.HashOf a.ctid) (Kind.Axiom.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 (Kind.Axiom.HashOf a.ctid) (Kind.Axiom.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 (Kind.Axiom.HashOf a.ctid) (Kind.Axiom.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 (Kind.Axiom.HashOf a.ctid) (Kind.Axiom.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 (Kind.Axiom.HashOf a.ctid) (Kind.Axiom.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.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6) (Kind.Term.ct7 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6)) = let ctid = (U60.equal (Kind.Axiom.HashOf a.ctid) (Kind.Axiom.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.bind (Kind.Checker.equal a.x6 b.x6) λx6 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 x6)))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.ct8 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7) (Kind.Term.ct8 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7)) = let ctid = (U60.equal (Kind.Axiom.HashOf a.ctid) (Kind.Axiom.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.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 ctid (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.ct9 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8) (Kind.Term.ct9 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8)) = let ctid = (U60.equal (Kind.Axiom.HashOf a.ctid) (Kind.Axiom.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.bind (Kind.Checker.equal a.x6 b.x6) λx6 (Kind.Checker.bind (Kind.Checker.equal a.x7 b.x7) λx7 (Kind.Checker.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 x8)))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.ct10 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8 a.x9) (Kind.Term.ct10 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8 b.x9)) = let ctid = (U60.equal (Kind.Axiom.HashOf a.ctid) (Kind.Axiom.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.bind (Kind.Checker.equal a.x6 b.x6) λx6 (Kind.Checker.bind (Kind.Checker.equal a.x7 b.x7) λx7 (Kind.Checker.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.bind (Kind.Checker.equal a.x9 b.x9) λx9 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 (Bool.and x8 x9)))))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.ct11 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8 a.x9 a.x10) (Kind.Term.ct11 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8 b.x9 b.x10)) = let ctid = (U60.equal (Kind.Axiom.HashOf a.ctid) (Kind.Axiom.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.bind (Kind.Checker.equal a.x6 b.x6) λx6 (Kind.Checker.bind (Kind.Checker.equal a.x7 b.x7) λx7 (Kind.Checker.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.bind (Kind.Checker.equal a.x9 b.x9) λx9 (Kind.Checker.bind (Kind.Checker.equal a.x10 b.x10) λx10 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 (Bool.and x8 (Bool.and x9 x10)))))))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.ct12 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8 a.x9 a.x10 a.x11) (Kind.Term.ct12 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8 b.x9 b.x10 b.x11)) = let ctid = (U60.equal (Kind.Axiom.HashOf a.ctid) (Kind.Axiom.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.bind (Kind.Checker.equal a.x6 b.x6) λx6 (Kind.Checker.bind (Kind.Checker.equal a.x7 b.x7) λx7 (Kind.Checker.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.bind (Kind.Checker.equal a.x9 b.x9) λx9 (Kind.Checker.bind (Kind.Checker.equal a.x10 b.x10) λx10 (Kind.Checker.bind (Kind.Checker.equal a.x11 b.x11) λx11 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 (Bool.and x8 (Bool.and x9 (Bool.and x10 x11)))))))))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.ct13 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8 a.x9 a.x10 a.x11 a.x12) (Kind.Term.ct13 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8 b.x9 b.x10 b.x11 b.x12)) = let ctid = (U60.equal (Kind.Axiom.HashOf a.ctid) (Kind.Axiom.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.bind (Kind.Checker.equal a.x6 b.x6) λx6 (Kind.Checker.bind (Kind.Checker.equal a.x7 b.x7) λx7 (Kind.Checker.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.bind (Kind.Checker.equal a.x9 b.x9) λx9 (Kind.Checker.bind (Kind.Checker.equal a.x10 b.x10) λx10 (Kind.Checker.bind (Kind.Checker.equal a.x11 b.x11) λx11 (Kind.Checker.bind (Kind.Checker.equal a.x12 b.x12) λx12 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 (Bool.and x8 (Bool.and x9 (Bool.and x10 (Bool.and x11 x12)))))))))))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.ct14 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8 a.x9 a.x10 a.x11 a.x12 a.x13) (Kind.Term.ct14 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8 b.x9 b.x10 b.x11 b.x12 b.x13)) = let ctid = (U60.equal (Kind.Axiom.HashOf a.ctid) (Kind.Axiom.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.bind (Kind.Checker.equal a.x6 b.x6) λx6 (Kind.Checker.bind (Kind.Checker.equal a.x7 b.x7) λx7 (Kind.Checker.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.bind (Kind.Checker.equal a.x9 b.x9) λx9 (Kind.Checker.bind (Kind.Checker.equal a.x10 b.x10) λx10 (Kind.Checker.bind (Kind.Checker.equal a.x11 b.x11) λx11 (Kind.Checker.bind (Kind.Checker.equal a.x12 b.x12) λx12 (Kind.Checker.bind (Kind.Checker.equal a.x13 b.x13) λx13 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 (Bool.and x8 (Bool.and x9 (Bool.and x10 (Bool.and x11 (Bool.and x12 x13)))))))))))))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.ct15 a.ctid a.orig a.args) (Kind.Term.ct15 b.ctid b.orig b.args)) = let ctid = (U60.equal (Kind.Axiom.HashOf a.ctid) (Kind.Axiom.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.ct16 a.ctid a.orig a.args) (Kind.Term.ct16 b.ctid b.orig b.args)) = let ctid = (U60.equal (Kind.Axiom.HashOf a.ctid) (Kind.Axiom.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.args15 a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8 a.x9 a.x10 a.x11 a.x12 a.x13 a.x14) (Kind.Term.args15 b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8 b.x9 b.x10 b.x11 b.x12 b.x13 b.x14)) = (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.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.bind (Kind.Checker.equal a.x9 b.x9) λx9 (Kind.Checker.bind (Kind.Checker.equal a.x10 b.x10) λx10 (Kind.Checker.bind (Kind.Checker.equal a.x11 b.x11) λx11 (Kind.Checker.bind (Kind.Checker.equal a.x12 b.x12) λx12 (Kind.Checker.bind (Kind.Checker.equal a.x13 b.x13) λx13 (Kind.Checker.bind (Kind.Checker.equal a.x14 b.x14) λx14 (Kind.Checker.pure (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 (Bool.and x8 (Bool.and x9 (Bool.and x10 (Bool.and x11 (Bool.and x12 (Bool.and x13 x14))))))))))))))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.args16 a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8 a.x9 a.x10 a.x11 a.x12 a.x13 a.x14 a.x15) (Kind.Term.args16 b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8 b.x9 b.x10 b.x11 b.x12 b.x13 b.x14 b.x15)) = (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.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.bind (Kind.Checker.equal a.x9 b.x9) λx9 (Kind.Checker.bind (Kind.Checker.equal a.x10 b.x10) λx10 (Kind.Checker.bind (Kind.Checker.equal a.x11 b.x11) λx11 (Kind.Checker.bind (Kind.Checker.equal a.x12 b.x12) λx12 (Kind.Checker.bind (Kind.Checker.equal a.x13 b.x13) λx13 (Kind.Checker.bind (Kind.Checker.equal a.x14 b.x14) λx14 (Kind.Checker.bind (Kind.Checker.equal a.x15 b.x15) λx15 (Kind.Checker.pure (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 (Bool.and x8 (Bool.and x9 (Bool.and x10 (Bool.and x11 (Bool.and x12 (Bool.and x13 (Bool.and x14 x15))))))))))))))))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn0 a.fnid a.orig) (Kind.Term.fn0 b.fnid b.orig)) = let fnid = (U60.equal (HashOf a.fnid) (HashOf b.fnid)); (Kind.Checker.pure fnid)
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn1 a.fnid a.orig a.x0) (Kind.Term.fn1 b.fnid b.orig b.x0)) = let fnid = (U60.equal (HashOf a.fnid) (HashOf b.fnid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) λx0 (Kind.Checker.pure (Bool.and fnid x0)))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn2 a.fnid a.orig a.x0 a.x1) (Kind.Term.fn2 b.fnid b.orig b.x0 b.x1)) = let fnid = (U60.equal (HashOf a.fnid) (HashOf b.fnid)); (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 fnid (Bool.and x0 x1)))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn3 a.fnid a.orig a.x0 a.x1 a.x2) (Kind.Term.fn3 b.fnid b.orig b.x0 b.x1 b.x2)) = let fnid = (U60.equal (HashOf a.fnid) (HashOf b.fnid)); (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 fnid (Bool.and x0 (Bool.and x1 x2)))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn4 a.fnid a.orig a.x0 a.x1 a.x2 a.x3) (Kind.Term.fn4 b.fnid b.orig b.x0 b.x1 b.x2 b.x3)) = let fnid = (U60.equal (HashOf a.fnid) (HashOf b.fnid)); (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 fnid (Bool.and x0 (Bool.and x1 (Bool.and x2 x3)))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn5 a.fnid a.orig a.x0 a.x1 a.x2 a.x3 a.x4) (Kind.Term.fn5 b.fnid b.orig b.x0 b.x1 b.x2 b.x3 b.x4)) = let fnid = (U60.equal (HashOf a.fnid) (HashOf b.fnid)); (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 fnid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 x4)))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn6 a.fnid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5) (Kind.Term.fn6 b.fnid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5)) = let fnid = (U60.equal (HashOf a.fnid) (HashOf b.fnid)); (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 fnid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 x5)))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn7 a.fnid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6) (Kind.Term.fn7 b.fnid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6)) = let fnid = (U60.equal (HashOf a.fnid) (HashOf b.fnid)); (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 fnid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 x6)))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn8 a.fnid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7) (Kind.Term.fn8 b.fnid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7)) = let fnid = (U60.equal (HashOf a.fnid) (HashOf b.fnid)); (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 fnid (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.fn9 a.fnid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8) (Kind.Term.fn9 b.fnid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8)) = let fnid = (U60.equal (HashOf a.fnid) (HashOf b.fnid)); (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.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.pure (Bool.and fnid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 x8)))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn10 a.fnid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8 a.x9) (Kind.Term.fn10 b.fnid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8 b.x9)) = let fnid = (U60.equal (HashOf a.fnid) (HashOf b.fnid)); (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.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.bind (Kind.Checker.equal a.x9 b.x9) λx9 (Kind.Checker.pure (Bool.and fnid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 (Bool.and x8 x9)))))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn11 a.fnid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8 a.x9 a.x10) (Kind.Term.fn11 b.fnid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8 b.x9 b.x10)) = let fnid = (U60.equal (HashOf a.fnid) (HashOf b.fnid)); (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.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.bind (Kind.Checker.equal a.x9 b.x9) λx9 (Kind.Checker.bind (Kind.Checker.equal a.x10 b.x10) λx10 (Kind.Checker.pure (Bool.and fnid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 (Bool.and x8 (Bool.and x9 x10)))))))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn12 a.fnid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8 a.x9 a.x10 a.x11) (Kind.Term.fn12 b.fnid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8 b.x9 b.x10 b.x11)) = let fnid = (U60.equal (HashOf a.fnid) (HashOf b.fnid)); (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.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.bind (Kind.Checker.equal a.x9 b.x9) λx9 (Kind.Checker.bind (Kind.Checker.equal a.x10 b.x10) λx10 (Kind.Checker.bind (Kind.Checker.equal a.x11 b.x11) λx11 (Kind.Checker.pure (Bool.and fnid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 (Bool.and x8 (Bool.and x9 (Bool.and x10 x11)))))))))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn13 a.fnid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8 a.x9 a.x10 a.x11 a.x12) (Kind.Term.fn13 b.fnid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8 b.x9 b.x10 b.x11 b.x12)) = let fnid = (U60.equal (HashOf a.fnid) (HashOf b.fnid)); (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.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.bind (Kind.Checker.equal a.x9 b.x9) λx9 (Kind.Checker.bind (Kind.Checker.equal a.x10 b.x10) λx10 (Kind.Checker.bind (Kind.Checker.equal a.x11 b.x11) λx11 (Kind.Checker.bind (Kind.Checker.equal a.x12 b.x12) λx12 (Kind.Checker.pure (Bool.and fnid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 (Bool.and x8 (Bool.and x9 (Bool.and x10 (Bool.and x11 x12)))))))))))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn14 a.fnid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8 a.x9 a.x10 a.x11 a.x12 a.x13) (Kind.Term.fn14 b.fnid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8 b.x9 b.x10 b.x11 b.x12 b.x13)) = let fnid = (U60.equal (HashOf a.fnid) (HashOf b.fnid)); (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.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.bind (Kind.Checker.equal a.x9 b.x9) λx9 (Kind.Checker.bind (Kind.Checker.equal a.x10 b.x10) λx10 (Kind.Checker.bind (Kind.Checker.equal a.x11 b.x11) λx11 (Kind.Checker.bind (Kind.Checker.equal a.x12 b.x12) λx12 (Kind.Checker.bind (Kind.Checker.equal a.x13 b.x13) λx13 (Kind.Checker.pure (Bool.and fnid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 (Bool.and x8 (Bool.and x9 (Bool.and x10 (Bool.and x11 (Bool.and x12 x13)))))))))))))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn15 a.fnid a.orig a.args) (Kind.Term.fn15 b.fnid b.orig b.args)) = let fnid = (U60.equal (HashOf a.fnid) (HashOf b.fnid)); (Kind.Checker.bind (Kind.Checker.equal a.args b.args) λxargs (Kind.Checker.pure (Bool.and fnid xargs)))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn16 a.fnid a.orig a.args) (Kind.Term.fn16 b.fnid b.orig b.args)) = let fnid = (U60.equal (HashOf a.fnid) (HashOf b.fnid)); (Kind.Checker.bind (Kind.Checker.equal a.args b.args) λxargs (Kind.Checker.pure (Bool.and fnid xargs)))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn0 a.fnid a.orig) (Kind.Term.fn0 b.fnid b.orig)) = let fnid = (U60.equal (Kind.Axiom.HashOf a.fnid) (Kind.Axiom.HashOf b.fnid)); (Kind.Checker.pure fnid)
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn1 a.fnid a.orig a.x0) (Kind.Term.fn1 b.fnid b.orig b.x0)) = let fnid = (U60.equal (Kind.Axiom.HashOf a.fnid) (Kind.Axiom.HashOf b.fnid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) λx0 (Kind.Checker.pure (Bool.and fnid x0)))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn2 a.fnid a.orig a.x0 a.x1) (Kind.Term.fn2 b.fnid b.orig b.x0 b.x1)) = let fnid = (U60.equal (Kind.Axiom.HashOf a.fnid) (Kind.Axiom.HashOf b.fnid)); (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 fnid (Bool.and x0 x1)))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn3 a.fnid a.orig a.x0 a.x1 a.x2) (Kind.Term.fn3 b.fnid b.orig b.x0 b.x1 b.x2)) = let fnid = (U60.equal (Kind.Axiom.HashOf a.fnid) (Kind.Axiom.HashOf b.fnid)); (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 fnid (Bool.and x0 (Bool.and x1 x2)))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn4 a.fnid a.orig a.x0 a.x1 a.x2 a.x3) (Kind.Term.fn4 b.fnid b.orig b.x0 b.x1 b.x2 b.x3)) = let fnid = (U60.equal (Kind.Axiom.HashOf a.fnid) (Kind.Axiom.HashOf b.fnid)); (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 fnid (Bool.and x0 (Bool.and x1 (Bool.and x2 x3)))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn5 a.fnid a.orig a.x0 a.x1 a.x2 a.x3 a.x4) (Kind.Term.fn5 b.fnid b.orig b.x0 b.x1 b.x2 b.x3 b.x4)) = let fnid = (U60.equal (Kind.Axiom.HashOf a.fnid) (Kind.Axiom.HashOf b.fnid)); (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 fnid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 x4)))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn6 a.fnid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5) (Kind.Term.fn6 b.fnid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5)) = let fnid = (U60.equal (Kind.Axiom.HashOf a.fnid) (Kind.Axiom.HashOf b.fnid)); (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 fnid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 x5)))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn7 a.fnid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6) (Kind.Term.fn7 b.fnid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6)) = let fnid = (U60.equal (Kind.Axiom.HashOf a.fnid) (Kind.Axiom.HashOf b.fnid)); (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 fnid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 x6)))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn8 a.fnid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7) (Kind.Term.fn8 b.fnid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7)) = let fnid = (U60.equal (Kind.Axiom.HashOf a.fnid) (Kind.Axiom.HashOf b.fnid)); (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 fnid (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.fn9 a.fnid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8) (Kind.Term.fn9 b.fnid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8)) = let fnid = (U60.equal (Kind.Axiom.HashOf a.fnid) (Kind.Axiom.HashOf b.fnid)); (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.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.pure (Bool.and fnid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 x8)))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn10 a.fnid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8 a.x9) (Kind.Term.fn10 b.fnid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8 b.x9)) = let fnid = (U60.equal (Kind.Axiom.HashOf a.fnid) (Kind.Axiom.HashOf b.fnid)); (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.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.bind (Kind.Checker.equal a.x9 b.x9) λx9 (Kind.Checker.pure (Bool.and fnid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 (Bool.and x8 x9)))))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn11 a.fnid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8 a.x9 a.x10) (Kind.Term.fn11 b.fnid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8 b.x9 b.x10)) = let fnid = (U60.equal (Kind.Axiom.HashOf a.fnid) (Kind.Axiom.HashOf b.fnid)); (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.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.bind (Kind.Checker.equal a.x9 b.x9) λx9 (Kind.Checker.bind (Kind.Checker.equal a.x10 b.x10) λx10 (Kind.Checker.pure (Bool.and fnid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 (Bool.and x8 (Bool.and x9 x10)))))))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn12 a.fnid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8 a.x9 a.x10 a.x11) (Kind.Term.fn12 b.fnid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8 b.x9 b.x10 b.x11)) = let fnid = (U60.equal (Kind.Axiom.HashOf a.fnid) (Kind.Axiom.HashOf b.fnid)); (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.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.bind (Kind.Checker.equal a.x9 b.x9) λx9 (Kind.Checker.bind (Kind.Checker.equal a.x10 b.x10) λx10 (Kind.Checker.bind (Kind.Checker.equal a.x11 b.x11) λx11 (Kind.Checker.pure (Bool.and fnid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 (Bool.and x8 (Bool.and x9 (Bool.and x10 x11)))))))))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn13 a.fnid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8 a.x9 a.x10 a.x11 a.x12) (Kind.Term.fn13 b.fnid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8 b.x9 b.x10 b.x11 b.x12)) = let fnid = (U60.equal (Kind.Axiom.HashOf a.fnid) (Kind.Axiom.HashOf b.fnid)); (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.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.bind (Kind.Checker.equal a.x9 b.x9) λx9 (Kind.Checker.bind (Kind.Checker.equal a.x10 b.x10) λx10 (Kind.Checker.bind (Kind.Checker.equal a.x11 b.x11) λx11 (Kind.Checker.bind (Kind.Checker.equal a.x12 b.x12) λx12 (Kind.Checker.pure (Bool.and fnid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 (Bool.and x8 (Bool.and x9 (Bool.and x10 (Bool.and x11 x12)))))))))))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn14 a.fnid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7 a.x8 a.x9 a.x10 a.x11 a.x12 a.x13) (Kind.Term.fn14 b.fnid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7 b.x8 b.x9 b.x10 b.x11 b.x12 b.x13)) = let fnid = (U60.equal (Kind.Axiom.HashOf a.fnid) (Kind.Axiom.HashOf b.fnid)); (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.bind (Kind.Checker.equal a.x8 b.x8) λx8 (Kind.Checker.bind (Kind.Checker.equal a.x9 b.x9) λx9 (Kind.Checker.bind (Kind.Checker.equal a.x10 b.x10) λx10 (Kind.Checker.bind (Kind.Checker.equal a.x11 b.x11) λx11 (Kind.Checker.bind (Kind.Checker.equal a.x12 b.x12) λx12 (Kind.Checker.bind (Kind.Checker.equal a.x13 b.x13) λx13 (Kind.Checker.pure (Bool.and fnid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 (Bool.and x7 (Bool.and x8 (Bool.and x9 (Bool.and x10 (Bool.and x11 (Bool.and x12 x13)))))))))))))))))))))))))))))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn15 a.fnid a.orig a.args) (Kind.Term.fn15 b.fnid b.orig b.args)) = let fnid = (U60.equal (Kind.Axiom.HashOf a.fnid) (Kind.Axiom.HashOf b.fnid)); (Kind.Checker.bind (Kind.Checker.equal a.args b.args) λxargs (Kind.Checker.pure (Bool.and fnid xargs)))
|
|
|
|
|
(Kind.Checker.equal (Kind.Term.fn16 a.fnid a.orig a.args) (Kind.Term.fn16 b.fnid b.orig b.args)) = let fnid = (U60.equal (Kind.Axiom.HashOf a.fnid) (Kind.Axiom.HashOf b.fnid)); (Kind.Checker.bind (Kind.Checker.equal a.args b.args) λxargs (Kind.Checker.pure (Bool.and fnid 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.extended checker name type vals) = (Kind.Checker.bind (Kind.Checker.extend name type vals) λx_2 (Kind.Checker.bind checker λgot (Kind.Checker.bind (Kind.Checker.shrink) λx_1 (Kind.Checker.pure got))))
|
|
|
|
|
(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 (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 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 (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.Term.fill term (Kind.Subst.end)) = term
|
|
|
|
|
(Kind.Term.fill (Kind.Term.typ orig) sub) = (Kind.Term.typ orig)
|
|
|
|
|
(Kind.Term.fill (Kind.Term.var orig name index) sub) = (Kind.Term.var orig name index)
|
|
|
|
|
(Kind.Term.fill (Kind.Term.all orig name typ body) sub) = (Kind.Term.all orig name (Kind.Term.fill typ sub) λx (Kind.Term.fill (body x) sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.lam orig name body) sub) = (Kind.Term.lam orig name λx (Kind.Term.fill (body x) sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.let orig name expr body) sub) = (Kind.Term.eval_let orig name (Kind.Term.fill expr sub) λx (Kind.Term.fill (body x) sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.ann orig expr typ) sub) = (Kind.Term.eval_ann orig (Kind.Term.fill expr sub) (Kind.Term.fill typ sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.sub orig name indx redx expr) sub) = (Kind.Term.eval_sub orig name indx redx (Kind.Term.fill expr sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.app orig expr typ) sub) = (Kind.Term.eval_app orig (Kind.Term.fill expr sub) (Kind.Term.fill typ sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.hlp orig) sub) = (Kind.Term.hlp orig)
|
|
|
|
|
(Kind.Term.fill (Kind.Term.U60 orig) sub) = (Kind.Term.U60 orig)
|
|
|
|
|
(Kind.Term.fill (Kind.Term.u60 orig num) sub) = (Kind.Term.u60 orig num)
|
|
|
|
|
(Kind.Term.fill (Kind.Term.op2 orig op left right) sub) = (Kind.Term.op2 orig op (Kind.Term.fill left sub) (Kind.Term.fill right sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.ct0 ctid orig) sub) = (Kind.Term.ct0 ctid orig)
|
|
|
|
|
(Kind.Term.fill (Kind.Term.ct1 ctid orig x0) sub) = (Kind.Term.ct1 ctid orig (Kind.Term.fill x0 sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.ct2 ctid orig x0 x1) sub) = (Kind.Term.ct2 ctid orig (Kind.Term.fill x0 sub) (Kind.Term.fill x1 sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.ct3 ctid orig x0 x1 x2) sub) = (Kind.Term.ct3 ctid orig (Kind.Term.fill x0 sub) (Kind.Term.fill x1 sub) (Kind.Term.fill x2 sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.ct4 ctid orig x0 x1 x2 x3) sub) = (Kind.Term.ct4 ctid orig (Kind.Term.fill x0 sub) (Kind.Term.fill x1 sub) (Kind.Term.fill x2 sub) (Kind.Term.fill x3 sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4) sub) = (Kind.Term.ct5 ctid orig (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 (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5) sub) = (Kind.Term.ct6 ctid orig (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 (Kind.Term.ct7 ctid orig x0 x1 x2 x3 x4 x5 x6) sub) = (Kind.Term.ct7 ctid orig (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 (Kind.Term.ct8 ctid orig x0 x1 x2 x3 x4 x5 x6 x7) sub) = (Kind.Term.ct8 ctid orig (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 (Kind.Term.ct9 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8) sub) = (Kind.Term.ct9 ctid orig (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 (Kind.Term.ct10 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) sub) = (Kind.Term.ct10 ctid orig (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 (Kind.Term.ct11 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) sub) = (Kind.Term.ct11 ctid orig (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 (Kind.Term.ct12 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) sub) = (Kind.Term.ct12 ctid orig (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 (Kind.Term.ct13 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) sub) = (Kind.Term.ct13 ctid orig (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 (Kind.Term.ct14 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) sub) = (Kind.Term.ct14 ctid orig (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 (Kind.Term.ct15 ctid orig x0) sub) = (Kind.Term.ct15 ctid orig (Kind.Term.fill x0 sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.ct16 ctid orig x0) sub) = (Kind.Term.ct16 ctid orig (Kind.Term.fill x0 sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.fn0 fnid orig) sub) = (Kind.Term.FN0 fnid orig)
|
|
|
|
|
(Kind.Term.fill (Kind.Term.fn1 fnid orig x0) sub) = (Kind.Term.FN1 fnid orig (Kind.Term.fill x0 sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.fn2 fnid orig x0 x1) sub) = (Kind.Term.FN2 fnid orig (Kind.Term.fill x0 sub) (Kind.Term.fill x1 sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.fn3 fnid orig x0 x1 x2) sub) = (Kind.Term.FN3 fnid orig (Kind.Term.fill x0 sub) (Kind.Term.fill x1 sub) (Kind.Term.fill x2 sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.fn4 fnid orig x0 x1 x2 x3) sub) = (Kind.Term.FN4 fnid orig (Kind.Term.fill x0 sub) (Kind.Term.fill x1 sub) (Kind.Term.fill x2 sub) (Kind.Term.fill x3 sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4) sub) = (Kind.Term.FN5 fnid orig (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 (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5) sub) = (Kind.Term.FN6 fnid orig (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 (Kind.Term.fn7 fnid orig x0 x1 x2 x3 x4 x5 x6) sub) = (Kind.Term.FN7 fnid orig (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 (Kind.Term.fn8 fnid orig x0 x1 x2 x3 x4 x5 x6 x7) sub) = (Kind.Term.FN8 fnid orig (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 (Kind.Term.fn9 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8) sub) = (Kind.Term.FN9 fnid orig (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 (Kind.Term.fn10 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) sub) = (Kind.Term.FN10 fnid orig (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 (Kind.Term.fn11 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) sub) = (Kind.Term.FN11 fnid orig (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 (Kind.Term.fn12 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) sub) = (Kind.Term.FN12 fnid orig (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 (Kind.Term.fn13 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) sub) = (Kind.Term.FN13 fnid orig (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 (Kind.Term.fn14 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) sub) = (Kind.Term.FN14 fnid orig (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 (Kind.Term.fn15 ctid orig x0) sub) = (Kind.Term.FN15 ctid orig (Kind.Term.fill x0 sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.fn16 ctid orig x0) sub) = (Kind.Term.FN16 ctid orig (Kind.Term.fill x0 sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) sub) = (Kind.Term.args15 (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 (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) λvalue (Kind.Term.fill value sub))
|
|
|
|
|
(Kind.Subst.look (Kind.Subst.end) 0) = (Maybe.none)
|
|
|
|
|
(Kind.Subst.look (Kind.Subst.unfilled rest) 0) = (Maybe.none)
|
|
|
|
|
(Kind.Subst.look (Kind.Subst.sub term rest) 0) = (Maybe.some term)
|
|
|
|
|
(Kind.Subst.look (Kind.Subst.end) n) = (Maybe.none)
|
|
|
|
|
(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))
|
|
|
|
|
(U60.equal a b) = (U60.to_bool (== a b))
|
|
|
|
|
(U60.to_bool 0) = (Bool.false)
|
|
|
|
|
(U60.to_bool n) = (Bool.true)
|
|
|
|
|
(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.look index) = λcontext λdepth λrhs λsubst λeqts λerrs (Kind.Result.checked context depth rhs subst eqts errs (Kind.Subst.look subst index))
|
|
|
|
|
(Kind.Checker.equal.hol.val (Maybe.none) orig numb b) = (Kind.Checker.bind (Kind.Checker.fill numb b) λx_1 (Kind.Checker.pure (Bool.true)))
|
|
|
|
|
(Kind.Checker.equal.hol.val (Maybe.some val) orig numb b) = (Kind.Checker.equal val b)
|
|
|
|
|
(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 (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.get_depth) = λcontext λdepth λrhs λsubst λeqts λerrs (Kind.Result.checked context depth rhs subst eqts errs depth)
|
|
|
|
|
(Kind.Checker.get_right_hand_side) = λcontext λdepth λrhs λsubst λeqts λerrs (Kind.Result.checked context depth rhs subst eqts errs rhs)
|
|
|
|
|
(Kind.Term.fillable term (Kind.Subst.end)) = (Bool.false)
|
|
|
|
|
(Kind.Term.fillable (Kind.Term.typ orig) sub) = (Bool.false)
|
|
|
|
@ -425,11 +172,16 @@
|
|
|
|
|
(Kind.Term.fillable (Kind.Term.fn16 fnid orig args) sub) = (Kind.Term.fillable args sub)
|
|
|
|
|
(Kind.Term.fillable (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) 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) (Bool.or (Kind.Term.fillable x7 sub) (Bool.or (Kind.Term.fillable x8 sub) (Bool.or (Kind.Term.fillable x9 sub) (Bool.or (Kind.Term.fillable x10 sub) (Bool.or (Kind.Term.fillable x11 sub) (Bool.or (Kind.Term.fillable x12 sub) (Bool.or (Kind.Term.fillable x13 sub) (Kind.Term.fillable x14 sub)))))))))))))))
|
|
|
|
|
(Kind.Term.fillable (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) 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) (Bool.or (Kind.Term.fillable x7 sub) (Bool.or (Kind.Term.fillable x8 sub) (Bool.or (Kind.Term.fillable x9 sub) (Bool.or (Kind.Term.fillable x10 sub) (Bool.or (Kind.Term.fillable x11 sub) (Bool.or (Kind.Term.fillable x12 sub) (Bool.or (Kind.Term.fillable x13 sub) (Bool.or (Kind.Term.fillable x14 sub) (Kind.Term.fillable x15 sub))))))))))))))))
|
|
|
|
|
(Maybe.is_some (Maybe.none)) = (Bool.false)
|
|
|
|
|
(Maybe.is_some (Maybe.some v)) = (Bool.true)
|
|
|
|
|
(Kind.Subst.look (Kind.Subst.end) 0) = (Maybe.none)
|
|
|
|
|
(Kind.Subst.look (Kind.Subst.unfilled rest) 0) = (Maybe.none)
|
|
|
|
|
(Kind.Subst.look (Kind.Subst.sub term rest) 0) = (Maybe.some term)
|
|
|
|
|
(Kind.Subst.look (Kind.Subst.end) n) = (Maybe.none)
|
|
|
|
|
(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.or (Bool.true) b) = (Bool.true)
|
|
|
|
|
(Bool.or (Bool.false) b) = b
|
|
|
|
|
(Kind.Checker.get_depth) = λcontext λdepth λrhs λsubst λeqts λerrs (Kind.Result.checked context depth rhs subst eqts errs depth)
|
|
|
|
|
(Maybe.is_some (Maybe.none)) = (Bool.false)
|
|
|
|
|
(Maybe.is_some (Maybe.some v)) = (Bool.true)
|
|
|
|
|
(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)
|
|
|
|
@ -448,6 +200,19 @@
|
|
|
|
|
(Kind.Operator.equal (Kind.Operator.neq) (Kind.Operator.neq)) = (Bool.true)
|
|
|
|
|
(Kind.Operator.equal a b) = (Bool.false)
|
|
|
|
|
(Kind.Checker.get_subst) = λcontext λdepth λrhs λsubst λeqts λerrs (Kind.Result.checked context depth rhs subst eqts errs subst)
|
|
|
|
|
(Bool.and (Bool.true) b) = b
|
|
|
|
|
(Bool.and (Bool.false) b) = (Bool.false)
|
|
|
|
|
(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 (Maybe.none) orig numb b) = (Kind.Checker.bind (Kind.Checker.fill numb b) λx_1 (Kind.Checker.pure (Bool.true)))
|
|
|
|
|
(Kind.Checker.equal.hol.val (Maybe.some val) orig numb b) = (Kind.Checker.equal val b)
|
|
|
|
|
(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 (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.look index) = λcontext λdepth λrhs λsubst λeqts λerrs (Kind.Result.checked context depth rhs subst eqts errs (Kind.Subst.look subst index))
|
|
|
|
|
(Kind.Checker.equal.var (Bool.false) orig name idx b) = (Kind.Checker.bind (Kind.Checker.add_value idx b) λx_1 (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 [] λn λt λv v) λa.val (Kind.Checker.bind (Kind.Checker.find b.idx [] λ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 [] λn λt λv v) λa.val (Kind.Checker.bind (Kind.Checker.equal.var.try_values a.val b) λres (Kind.Checker.pure res)))))
|
|
|
|
@ -457,22 +222,263 @@
|
|
|
|
|
(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
|
|
|
|
|
(U60.equal a b) = (U60.to_bool (== a b))
|
|
|
|
|
(U60.to_bool 0) = (Bool.false)
|
|
|
|
|
(U60.to_bool n) = (Bool.true)
|
|
|
|
|
(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 (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 (Bool.true) b) = b
|
|
|
|
|
(Bool.and (Bool.false) b) = (Bool.false)
|
|
|
|
|
(Kind.Checker.get_equations) = λcontext λdepth λrhs λsubst λeqts λerrs (Kind.Result.checked context depth rhs subst eqts errs eqts)
|
|
|
|
|
(Kind.Term.fill term (Kind.Subst.end)) = term
|
|
|
|
|
(Kind.Term.fill (Kind.Term.typ orig) sub) = (Kind.Term.typ orig)
|
|
|
|
|
(Kind.Term.fill (Kind.Term.var orig name index) sub) = (Kind.Term.var orig name index)
|
|
|
|
|
(Kind.Term.fill (Kind.Term.all orig name typ body) sub) = (Kind.Term.all orig name (Kind.Term.fill typ sub) λx (Kind.Term.fill (body x) sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.lam orig name body) sub) = (Kind.Term.lam orig name λx (Kind.Term.fill (body x) sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.let orig name expr body) sub) = (Kind.Term.eval_let orig name (Kind.Term.fill expr sub) λx (Kind.Term.fill (body x) sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.ann orig expr typ) sub) = (Kind.Term.eval_ann orig (Kind.Term.fill expr sub) (Kind.Term.fill typ sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.sub orig name indx redx expr) sub) = (Kind.Term.eval_sub orig name indx redx (Kind.Term.fill expr sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.app orig expr typ) sub) = (Kind.Term.eval_app orig (Kind.Term.fill expr sub) (Kind.Term.fill typ sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.hlp orig) sub) = (Kind.Term.hlp orig)
|
|
|
|
|
(Kind.Term.fill (Kind.Term.U60 orig) sub) = (Kind.Term.U60 orig)
|
|
|
|
|
(Kind.Term.fill (Kind.Term.u60 orig num) sub) = (Kind.Term.u60 orig num)
|
|
|
|
|
(Kind.Term.fill (Kind.Term.op2 orig op left right) sub) = (Kind.Term.op2 orig op (Kind.Term.fill left sub) (Kind.Term.fill right sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.ct0 ctid orig) sub) = (Kind.Term.ct0 ctid orig)
|
|
|
|
|
(Kind.Term.fill (Kind.Term.ct1 ctid orig x0) sub) = (Kind.Term.ct1 ctid orig (Kind.Term.fill x0 sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.ct2 ctid orig x0 x1) sub) = (Kind.Term.ct2 ctid orig (Kind.Term.fill x0 sub) (Kind.Term.fill x1 sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.ct3 ctid orig x0 x1 x2) sub) = (Kind.Term.ct3 ctid orig (Kind.Term.fill x0 sub) (Kind.Term.fill x1 sub) (Kind.Term.fill x2 sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.ct4 ctid orig x0 x1 x2 x3) sub) = (Kind.Term.ct4 ctid orig (Kind.Term.fill x0 sub) (Kind.Term.fill x1 sub) (Kind.Term.fill x2 sub) (Kind.Term.fill x3 sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4) sub) = (Kind.Term.ct5 ctid orig (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 (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5) sub) = (Kind.Term.ct6 ctid orig (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 (Kind.Term.ct7 ctid orig x0 x1 x2 x3 x4 x5 x6) sub) = (Kind.Term.ct7 ctid orig (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 (Kind.Term.ct8 ctid orig x0 x1 x2 x3 x4 x5 x6 x7) sub) = (Kind.Term.ct8 ctid orig (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 (Kind.Term.ct9 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8) sub) = (Kind.Term.ct9 ctid orig (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 (Kind.Term.ct10 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) sub) = (Kind.Term.ct10 ctid orig (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 (Kind.Term.ct11 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) sub) = (Kind.Term.ct11 ctid orig (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 (Kind.Term.ct12 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) sub) = (Kind.Term.ct12 ctid orig (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 (Kind.Term.ct13 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) sub) = (Kind.Term.ct13 ctid orig (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 (Kind.Term.ct14 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) sub) = (Kind.Term.ct14 ctid orig (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 (Kind.Term.ct15 ctid orig x0) sub) = (Kind.Term.ct15 ctid orig (Kind.Term.fill x0 sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.ct16 ctid orig x0) sub) = (Kind.Term.ct16 ctid orig (Kind.Term.fill x0 sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.fn0 fnid orig) sub) = (Kind.Term.FN0 fnid orig)
|
|
|
|
|
(Kind.Term.fill (Kind.Term.fn1 fnid orig x0) sub) = (Kind.Term.FN1 fnid orig (Kind.Term.fill x0 sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.fn2 fnid orig x0 x1) sub) = (Kind.Term.FN2 fnid orig (Kind.Term.fill x0 sub) (Kind.Term.fill x1 sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.fn3 fnid orig x0 x1 x2) sub) = (Kind.Term.FN3 fnid orig (Kind.Term.fill x0 sub) (Kind.Term.fill x1 sub) (Kind.Term.fill x2 sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.fn4 fnid orig x0 x1 x2 x3) sub) = (Kind.Term.FN4 fnid orig (Kind.Term.fill x0 sub) (Kind.Term.fill x1 sub) (Kind.Term.fill x2 sub) (Kind.Term.fill x3 sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4) sub) = (Kind.Term.FN5 fnid orig (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 (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5) sub) = (Kind.Term.FN6 fnid orig (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 (Kind.Term.fn7 fnid orig x0 x1 x2 x3 x4 x5 x6) sub) = (Kind.Term.FN7 fnid orig (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 (Kind.Term.fn8 fnid orig x0 x1 x2 x3 x4 x5 x6 x7) sub) = (Kind.Term.FN8 fnid orig (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 (Kind.Term.fn9 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8) sub) = (Kind.Term.FN9 fnid orig (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 (Kind.Term.fn10 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) sub) = (Kind.Term.FN10 fnid orig (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 (Kind.Term.fn11 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) sub) = (Kind.Term.FN11 fnid orig (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 (Kind.Term.fn12 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) sub) = (Kind.Term.FN12 fnid orig (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 (Kind.Term.fn13 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) sub) = (Kind.Term.FN13 fnid orig (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 (Kind.Term.fn14 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) sub) = (Kind.Term.FN14 fnid orig (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 (Kind.Term.fn15 ctid orig x0) sub) = (Kind.Term.FN15 ctid orig (Kind.Term.fill x0 sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.fn16 ctid orig x0) sub) = (Kind.Term.FN16 ctid orig (Kind.Term.fill x0 sub))
|
|
|
|
|
(Kind.Term.fill (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) sub) = (Kind.Term.args15 (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 (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) λvalue (Kind.Term.fill value sub))
|
|
|
|
|
(Kind.Term.eval_let orig name expr body) = (body expr)
|
|
|
|
|
(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 expr type) = expr
|
|
|
|
|
(Maybe.match (Maybe.none) none some) = none
|
|
|
|
|
(Maybe.match (Maybe.some value_) none some) = (some value_)
|
|
|
|
|
(Kind.Term.eval_sub orig name indx redx expr) = expr
|
|
|
|
|
(Kind.Checker.extended checker name type vals) = (Kind.Checker.bind (Kind.Checker.extend name type vals) λx_2 (Kind.Checker.bind checker λgot (Kind.Checker.bind (Kind.Checker.shrink) λx_1 (Kind.Checker.pure got))))
|
|
|
|
|
(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 (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 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 (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.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) λx_1 (Kind.Checker.pure got))))
|
|
|
|
|
(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 (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.u60 orig num)) = (Kind.Term.u60 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 (Kind.Operator.add) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (+ a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.sub) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (- a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.mul) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (* a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.div) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (/ a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.mod) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (% a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.and) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (& a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.or) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (| a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.xor) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (^ a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.shl) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (<< a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.shr) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (>> a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.ltn) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (< a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.lte) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (<= a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.eql) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (== a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.gte) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (>= a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.gtn) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (> a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig (Kind.Operator.neq) (Kind.Term.u60 a.orig a.num) (Kind.Term.u60 b.orig b.num)) = (Kind.Term.u60 0 (!= a.num b.num))
|
|
|
|
|
(Kind.Term.eval_op orig op left right) = (Kind.Term.op2 orig op left right)
|
|
|
|
|
(Kind.Checker.run checker rhs) = (checker (Kind.Context.empty) 0 rhs (Kind.Subst.end) [] [])
|
|
|
|
|
(Kind.Coverage.check fnid) = let rules = (Kind.Axiom.RuleOf fnid); let type = (Kind.Axiom.TypeOf fnid); let problem = (Kind.Coverage.Problem.new type rules (Maybe.default (Maybe.map λx (Kind.Coverage.Rule.size x) (List.head rules)) 0)); (Kind.Checker.bind (Kind.Coverage.solve problem) λresult (Kind.Checker.bind (Kind.Checker.get_context) λctx (Kind.Checker.bind (Maybe.match result (Kind.Checker.pure (Unit.new)) λresult.value (Kind.Checker.fail (Kind.Error.uncovered_pattern ctx (Kind.Axiom.OrigOf fnid) result.value))) λx_1 (Kind.Checker.pure (Unit.new)))))
|
|
|
|
|
(Maybe.default (Maybe.none) dflt) = dflt
|
|
|
|
|
(Maybe.default (Maybe.some val) dflt) = val
|
|
|
|
|
(Kind.Checker.get_context) = λcontext λdepth λrhs λsubst λeqts λerrs (Kind.Result.checked context depth rhs subst eqts errs context)
|
|
|
|
|
(Kind.Coverage.solve problem) = (Kind.Coverage.done problem (Kind.Term.if_all (Kind.Coverage.Problem.type.get problem) λorig_ λname_ λtype λbody (Bool.if (Kind.Coverage.catches problem) (Kind.Coverage.intro_all type body problem) (Kind.Coverage.specialize (Kind.Term.eval type) body problem)) (Kind.Checker.pure (Maybe.none))))
|
|
|
|
|
(Kind.Coverage.intro_all type body (Kind.Coverage.Problem.new x_1 rows count)) = (Kind.Checker.bind (Kind.Checker.get_depth) λdepth (Kind.Checker.bind (Kind.Checker.extend 63 type []) λx_2 let var = (Kind.Term.var 0 63 depth); let new_type = (body var); let new_rows = (List.map rows λx (Kind.Coverage.Row.intro_all x)); (Kind.Checker.bind (Kind.Coverage.solve (Kind.Coverage.Problem.new new_type new_rows (- count 1))) λterm_result (Kind.Checker.pure (Maybe.map λscrutinee (List.cons (Kind.Term.Quoted.var 0 63 depth) scrutinee) term_result)))))
|
|
|
|
|
(Kind.Coverage.Row.intro_all (Kind.Rule.lhs term rule)) = rule
|
|
|
|
|
(Kind.Coverage.Row.intro_all rule) = rule
|
|
|
|
|
(Maybe.map f (Maybe.none)) = (Maybe.none)
|
|
|
|
|
(Maybe.map f (Maybe.some v)) = (Maybe.some (f v))
|
|
|
|
|
(List.map [] f) = []
|
|
|
|
|
(List.map (List.cons head tail) f) = (List.cons (f head) (List.map tail f))
|
|
|
|
|
(Kind.Coverage.done (Kind.Coverage.Problem.new type rows count) or_else) = (Bool.if (Bool.or (List.is_nil rows) (U60.to_bool (== count 0))) (Bool.if (List.is_nil rows) (Kind.Checker.pure (Maybe.some (List.repeat (Kind.Coverage.count_forall type (Nat.zero)) (Kind.Term.Quoted.var 0 63 0)))) (Kind.Checker.pure (Maybe.none))) or_else)
|
|
|
|
|
(List.is_nil []) = (Bool.true)
|
|
|
|
|
(List.is_nil (List.cons head tail)) = (Bool.false)
|
|
|
|
|
(Kind.Coverage.count_forall (Kind.Term.all x_1 x_2 x_3 body) acc) = (Kind.Coverage.count_forall (body (Kind.Term.var 0 63 0)) (Nat.succ acc))
|
|
|
|
|
(Kind.Coverage.count_forall x_4 acc) = acc
|
|
|
|
|
(List.repeat (Nat.zero) val) = []
|
|
|
|
|
(List.repeat (Nat.succ pred) val) = (List.cons val (List.repeat pred val))
|
|
|
|
|
(Kind.Coverage.Problem.type.get (Kind.Coverage.Problem.new type_ rows_ count_)) = type_
|
|
|
|
|
(Kind.Coverage.specialize type body problem) = (Kind.Coverage.Choice.match (Kind.Coverage.get_name type) λtype_name (Maybe.match (Kind.Axiom.Family.Constructors type_name) (Kind.Checker.pure (Maybe.some [(Kind.Term.Quoted.var 0 63 0)])) λconstructors (Kind.Coverage.specialize_list type_name constructors type body problem)) (Bool.if (List.any (Kind.Coverage.Problem.rows.get problem) λx (Kind.Coverage.Row.catches x)) (Kind.Coverage.intro_all type body problem) (Kind.Checker.pure (Maybe.some [(Kind.Term.Quoted.var 0 63 0)]))) (Kind.Checker.pure (Maybe.some [])))
|
|
|
|
|
(Kind.Coverage.get_name (Kind.Term.ct0 name x_1)) = (Kind.Coverage.Choice.on_cons name)
|
|
|
|
|
(Kind.Coverage.get_name (Kind.Term.ct1 name x_2 x_3)) = (Kind.Coverage.Choice.on_cons name)
|
|
|
|
|
(Kind.Coverage.get_name (Kind.Term.ct2 name x_4 x_5 x_6)) = (Kind.Coverage.Choice.on_cons name)
|
|
|
|
|
(Kind.Coverage.get_name (Kind.Term.ct3 name x_7 x_8 x_9 x_10)) = (Kind.Coverage.Choice.on_cons name)
|
|
|
|
|
(Kind.Coverage.get_name (Kind.Term.ct4 name x_11 x_12 x_13 x_14 x_15)) = (Kind.Coverage.Choice.on_cons name)
|
|
|
|
|
(Kind.Coverage.get_name (Kind.Term.ct5 name x_16 x_17 x_18 x_19 x_20 x_21)) = (Kind.Coverage.Choice.on_cons name)
|
|
|
|
|
(Kind.Coverage.get_name (Kind.Term.ct6 name x_22 x_23 x_24 x_25 x_26 x_27 x_28)) = (Kind.Coverage.Choice.on_cons name)
|
|
|
|
|
(Kind.Coverage.get_name (Kind.Term.ct8 name x_29 x_30 x_31 x_32 x_33 x_34 x_35 x_36 x_37)) = (Kind.Coverage.Choice.on_cons name)
|
|
|
|
|
(Kind.Coverage.get_name (Kind.Term.ct7 name x_38 x_39 x_40 x_41 x_42 x_43 x_44 x_45)) = (Kind.Coverage.Choice.on_cons name)
|
|
|
|
|
(Kind.Coverage.get_name (Kind.Term.ct9 name x_46 x_47 x_48 x_49 x_50 x_51 x_52 x_53 x_54 x_55)) = (Kind.Coverage.Choice.on_cons name)
|
|
|
|
|
(Kind.Coverage.get_name (Kind.Term.ct10 name x_56 x_57 x_58 x_59 x_60 x_61 x_62 x_63 x_64 x_65 x_66)) = (Kind.Coverage.Choice.on_cons name)
|
|
|
|
|
(Kind.Coverage.get_name (Kind.Term.ct11 name x_67 x_68 x_69 x_70 x_71 x_72 x_73 x_74 x_75 x_76 x_77 x_78)) = (Kind.Coverage.Choice.on_cons name)
|
|
|
|
|
(Kind.Coverage.get_name (Kind.Term.ct12 name x_79 x_80 x_81 x_82 x_83 x_84 x_85 x_86 x_87 x_88 x_89 x_90 x_91)) = (Kind.Coverage.Choice.on_cons name)
|
|
|
|
|
(Kind.Coverage.get_name (Kind.Term.ct13 name x_92 x_93 x_94 x_95 x_96 x_97 x_98 x_99 x_100 x_101 x_102 x_103 x_104 x_105)) = (Kind.Coverage.Choice.on_cons name)
|
|
|
|
|
(Kind.Coverage.get_name (Kind.Term.ct14 name x_106 x_107 x_108 x_109 x_110 x_111 x_112 x_113 x_114 x_115 x_116 x_117 x_118 x_119 x_120)) = (Kind.Coverage.Choice.on_cons name)
|
|
|
|
|
(Kind.Coverage.get_name (Kind.Term.ct15 name x_121 x_122)) = (Kind.Coverage.Choice.on_cons name)
|
|
|
|
|
(Kind.Coverage.get_name (Kind.Term.ct16 name x_123 x_124)) = (Kind.Coverage.Choice.on_cons name)
|
|
|
|
|
(Kind.Coverage.get_name (Kind.Term.ct16 name x_125 x_126)) = (Kind.Coverage.Choice.on_cons name)
|
|
|
|
|
(Kind.Coverage.get_name (Kind.Term.U60 x_127)) = (Kind.Coverage.Choice.on_U60)
|
|
|
|
|
(Kind.Coverage.get_name x_128) = (Kind.Coverage.Choice.none)
|
|
|
|
|
(Kind.Coverage.Row.catches (Kind.Rule.lhs (Kind.Term.var x_1 x_2 x_3) x_4)) = (Bool.true)
|
|
|
|
|
(Kind.Coverage.Row.catches x_5) = (Bool.false)
|
|
|
|
|
(Kind.Coverage.specialize_list type_name [] type body problem) = (Kind.Checker.pure (Maybe.none))
|
|
|
|
|
(Kind.Coverage.specialize_list type_name (List.cons name rest) type body problem) = (Kind.Checker.bind (Kind.Coverage.specialize_on type_name name type body problem) λresult (Maybe.match result (Kind.Coverage.specialize_list type_name rest type body problem) λresult.value (Kind.Checker.pure (Maybe.some result.value))))
|
|
|
|
|
(Kind.Coverage.specialize_on type_name constructor_name type body (Kind.Coverage.Problem.new current_problem_type rows count)) = (Maybe.match (Kind.Coverage.Maker.Mk constructor_name 0 type) (Kind.Checker.pure (Maybe.some [])) λconstructor_maker let new_type = (Kind.Coverage.Maker.make constructor_maker body); let params = (Kind.Axiom.Family.Params type_name); let args = (Kind.Axiom.ArgsCount constructor_name); (Kind.Checker.bind (Kind.Coverage.specialize_rules type_name constructor_name rows) λnew_rows let new_problem = (Kind.Coverage.Problem.new new_type new_rows (+ (- count 1) (- args params))); (Kind.Checker.bind (Kind.Coverage.solve new_problem) λterm_result (Maybe.match term_result (Kind.Checker.pure (Maybe.none)) λscrutinee let size = (Kind.Coverage.Maker.size constructor_maker); let took = (List.take scrutinee (U60.to_nat size)); let rest = (List.drop scrutinee (U60.to_nat size)); let pat = (Kind.Term.Quoted.ctr constructor_name 0 took); (Kind.Checker.pure (Maybe.some (List.cons pat rest)))))))
|
|
|
|
|
(Kind.Coverage.Maker.size (Kind.Coverage.Maker.Cons x_1 x_2 body)) = (+ 1 (Kind.Coverage.Maker.size (body (Kind.Term.var 0 0 0))))
|
|
|
|
|
(Kind.Coverage.Maker.size (Kind.Coverage.Maker.End x_3)) = 0
|
|
|
|
|
(Kind.Coverage.Maker.make (Kind.Coverage.Maker.Cons name typ body) and_then) = (Kind.Term.all 0 97 typ λarg (Kind.Coverage.Maker.make (body arg) and_then))
|
|
|
|
|
(Kind.Coverage.Maker.make (Kind.Coverage.Maker.End other) and_then) = (and_then other)
|
|
|
|
|
(List.drop xs (Nat.zero)) = xs
|
|
|
|
|
(List.drop (List.cons head tail) (Nat.succ pred)) = (List.drop tail pred)
|
|
|
|
|
(Kind.Coverage.specialize_rules type_name name (List.cons rule rules)) = let splitted = (Kind.Coverage.split_rule rule); (Maybe.match splitted (Kind.Coverage.specialize_rules type_name name rules) λvalue let params = (Kind.Axiom.Family.Params type_name); let row = (Kind.Coverage.specialize_rule name (Pair.fst value) (Pair.snd value)); (Kind.Checker.bind (Kind.Coverage.specialize_rules type_name name rules) λnext (Kind.Checker.pure (Maybe.match row next λvalue (List.cons (Kind.Coverage.drop_rule params value) next)))))
|
|
|
|
|
(Kind.Coverage.specialize_rules type_name name []) = (Kind.Checker.pure [])
|
|
|
|
|
(Kind.Coverage.drop_rule 0 rule) = rule
|
|
|
|
|
(Kind.Coverage.drop_rule n (Kind.Rule.lhs x_1 rule)) = (Kind.Coverage.drop_rule (- n 1) rule)
|
|
|
|
|
(Pair.snd (Pair.new fst snd)) = snd
|
|
|
|
|
(Kind.Coverage.split_rule (Kind.Rule.lhs term rest)) = (Maybe.some (Pair.new term rest))
|
|
|
|
|
(Kind.Coverage.split_rule x_1) = (Maybe.none)
|
|
|
|
|
(Kind.Coverage.specialize_rule n (Kind.Term.ct0 name orig) rule) = (Bool.if (Kind.Axiom.Compare n name) (Maybe.some rule) (Maybe.none))
|
|
|
|
|
(Kind.Coverage.specialize_rule n (Kind.Term.ct1 name orig x0) rule) = (Bool.if (Kind.Axiom.Compare n name) (Maybe.some (Kind.Rule.lhs x0 rule)) (Maybe.none))
|
|
|
|
|
(Kind.Coverage.specialize_rule n (Kind.Term.ct2 name orig x0 x1) rule) = (Bool.if (Kind.Axiom.Compare n name) (Maybe.some (Kind.Rule.lhs x0 (Kind.Rule.lhs x1 rule))) (Maybe.none))
|
|
|
|
|
(Kind.Coverage.specialize_rule n (Kind.Term.ct3 name orig x0 x1 x2) rule) = (Bool.if (Kind.Axiom.Compare n name) (Maybe.some (Kind.Rule.lhs x0 (Kind.Rule.lhs x1 (Kind.Rule.lhs x2 rule)))) (Maybe.none))
|
|
|
|
|
(Kind.Coverage.specialize_rule n (Kind.Term.ct4 name orig x0 x1 x2 x3) rule) = (Bool.if (Kind.Axiom.Compare n name) (Maybe.some (Kind.Rule.lhs x0 (Kind.Rule.lhs x1 (Kind.Rule.lhs x2 (Kind.Rule.lhs x3 rule))))) (Maybe.none))
|
|
|
|
|
(Kind.Coverage.specialize_rule n (Kind.Term.ct5 name orig x0 x1 x2 x3 x4) rule) = (Bool.if (Kind.Axiom.Compare n name) (Maybe.some (Kind.Rule.lhs x0 (Kind.Rule.lhs x1 (Kind.Rule.lhs x2 (Kind.Rule.lhs x3 (Kind.Rule.lhs x4 rule)))))) (Maybe.none))
|
|
|
|
|
(Kind.Coverage.specialize_rule n (Kind.Term.ct6 name orig x0 x1 x2 x3 x4 x5) rule) = (Bool.if (Kind.Axiom.Compare n name) (Maybe.some (Kind.Rule.lhs x0 (Kind.Rule.lhs x1 (Kind.Rule.lhs x2 (Kind.Rule.lhs x3 (Kind.Rule.lhs x4 (Kind.Rule.lhs x5 rule))))))) (Maybe.none))
|
|
|
|
|
(Kind.Coverage.specialize_rule n (Kind.Term.ct7 name orig x0 x1 x2 x3 x4 x5 x6) rule) = (Bool.if (Kind.Axiom.Compare n name) (Maybe.some (Kind.Rule.lhs x0 (Kind.Rule.lhs x1 (Kind.Rule.lhs x2 (Kind.Rule.lhs x3 (Kind.Rule.lhs x4 (Kind.Rule.lhs x5 (Kind.Rule.lhs x6 rule)))))))) (Maybe.none))
|
|
|
|
|
(Kind.Coverage.specialize_rule n (Kind.Term.ct8 name orig x0 x1 x2 x3 x4 x5 x6 x7) rule) = (Bool.if (Kind.Axiom.Compare n name) (Maybe.some (Kind.Rule.lhs x0 (Kind.Rule.lhs x1 (Kind.Rule.lhs x2 (Kind.Rule.lhs x3 (Kind.Rule.lhs x4 (Kind.Rule.lhs x5 (Kind.Rule.lhs x6 (Kind.Rule.lhs x7 rule))))))))) (Maybe.none))
|
|
|
|
|
(Kind.Coverage.specialize_rule n (Kind.Term.ct9 name orig x0 x1 x2 x3 x4 x5 x6 x7 x8) rule) = (Bool.if (Kind.Axiom.Compare n name) (Maybe.some (Kind.Rule.lhs x0 (Kind.Rule.lhs x1 (Kind.Rule.lhs x2 (Kind.Rule.lhs x3 (Kind.Rule.lhs x4 (Kind.Rule.lhs x5 (Kind.Rule.lhs x6 (Kind.Rule.lhs x7 (Kind.Rule.lhs x8 rule)))))))))) (Maybe.none))
|
|
|
|
|
(Kind.Coverage.specialize_rule n (Kind.Term.ct10 name orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) rule) = (Bool.if (Kind.Axiom.Compare n name) (Maybe.some (Kind.Rule.lhs x0 (Kind.Rule.lhs x1 (Kind.Rule.lhs x2 (Kind.Rule.lhs x3 (Kind.Rule.lhs x4 (Kind.Rule.lhs x5 (Kind.Rule.lhs x6 (Kind.Rule.lhs x7 (Kind.Rule.lhs x8 (Kind.Rule.lhs x9 rule))))))))))) (Maybe.none))
|
|
|
|
|
(Kind.Coverage.specialize_rule n (Kind.Term.ct11 name orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) rule) = (Bool.if (Kind.Axiom.Compare n name) (Maybe.some (Kind.Rule.lhs x0 (Kind.Rule.lhs x1 (Kind.Rule.lhs x2 (Kind.Rule.lhs x3 (Kind.Rule.lhs x4 (Kind.Rule.lhs x5 (Kind.Rule.lhs x6 (Kind.Rule.lhs x7 (Kind.Rule.lhs x8 (Kind.Rule.lhs x9 (Kind.Rule.lhs x10 rule)))))))))))) (Maybe.none))
|
|
|
|
|
(Kind.Coverage.specialize_rule n (Kind.Term.ct12 name orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) rule) = (Bool.if (Kind.Axiom.Compare n name) (Maybe.some (Kind.Rule.lhs x0 (Kind.Rule.lhs x1 (Kind.Rule.lhs x2 (Kind.Rule.lhs x3 (Kind.Rule.lhs x4 (Kind.Rule.lhs x5 (Kind.Rule.lhs x6 (Kind.Rule.lhs x7 (Kind.Rule.lhs x8 (Kind.Rule.lhs x9 (Kind.Rule.lhs x10 (Kind.Rule.lhs x11 rule))))))))))))) (Maybe.none))
|
|
|
|
|
(Kind.Coverage.specialize_rule n (Kind.Term.ct13 name orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) rule) = (Bool.if (Kind.Axiom.Compare n name) (Maybe.some (Kind.Rule.lhs x0 (Kind.Rule.lhs x1 (Kind.Rule.lhs x2 (Kind.Rule.lhs x3 (Kind.Rule.lhs x4 (Kind.Rule.lhs x5 (Kind.Rule.lhs x6 (Kind.Rule.lhs x7 (Kind.Rule.lhs x8 (Kind.Rule.lhs x9 (Kind.Rule.lhs x10 (Kind.Rule.lhs x11 (Kind.Rule.lhs x12 rule)))))))))))))) (Maybe.none))
|
|
|
|
|
(Kind.Coverage.specialize_rule n (Kind.Term.ct14 name orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) rule) = (Bool.if (Kind.Axiom.Compare n name) (Maybe.some (Kind.Rule.lhs x0 (Kind.Rule.lhs x1 (Kind.Rule.lhs x2 (Kind.Rule.lhs x3 (Kind.Rule.lhs x4 (Kind.Rule.lhs x5 (Kind.Rule.lhs x6 (Kind.Rule.lhs x7 (Kind.Rule.lhs x8 (Kind.Rule.lhs x9 (Kind.Rule.lhs x10 (Kind.Rule.lhs x11 (Kind.Rule.lhs x12 (Kind.Rule.lhs x13 rule))))))))))))))) (Maybe.none))
|
|
|
|
|
(Kind.Coverage.specialize_rule n (Kind.Term.ct15 name orig x0) rule) = (Bool.if (Kind.Axiom.Compare n name) (Kind.Coverage.specialize_rule n x0 rule) (Maybe.none))
|
|
|
|
|
(Kind.Coverage.specialize_rule n (Kind.Term.ct16 name orig x0) rule) = (Bool.if (Kind.Axiom.Compare n name) (Kind.Coverage.specialize_rule n x0 rule) (Maybe.none))
|
|
|
|
|
(Kind.Coverage.specialize_rule n (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) rule) = (Maybe.some (Kind.Rule.lhs x0 (Kind.Rule.lhs x1 (Kind.Rule.lhs x2 (Kind.Rule.lhs x3 (Kind.Rule.lhs x4 (Kind.Rule.lhs x5 (Kind.Rule.lhs x6 (Kind.Rule.lhs x7 (Kind.Rule.lhs x8 (Kind.Rule.lhs x9 (Kind.Rule.lhs x10 (Kind.Rule.lhs x11 (Kind.Rule.lhs x12 (Kind.Rule.lhs x13 (Kind.Rule.lhs x14 rule))))))))))))))))
|
|
|
|
|
(Kind.Coverage.specialize_rule n (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) rule) = (Maybe.some (Kind.Rule.lhs x0 (Kind.Rule.lhs x1 (Kind.Rule.lhs x2 (Kind.Rule.lhs x3 (Kind.Rule.lhs x4 (Kind.Rule.lhs x5 (Kind.Rule.lhs x6 (Kind.Rule.lhs x7 (Kind.Rule.lhs x8 (Kind.Rule.lhs x9 (Kind.Rule.lhs x10 (Kind.Rule.lhs x11 (Kind.Rule.lhs x12 (Kind.Rule.lhs x13 (Kind.Rule.lhs x14 (Kind.Rule.lhs x15 rule)))))))))))))))))
|
|
|
|
|
(Kind.Coverage.specialize_rule n (Kind.Term.var orig name index) rule) = (Maybe.some (Kind.Coverage.craft (Kind.Axiom.ArgsCount n) rule))
|
|
|
|
|
(Kind.Coverage.specialize_rule n x_1 rule) = (Maybe.none)
|
|
|
|
|
(Kind.Coverage.craft 0 rule) = rule
|
|
|
|
|
(Kind.Coverage.craft n rule) = (Kind.Coverage.craft (- n 1) (Kind.Rule.lhs (Kind.Term.var 0 65 0) rule))
|
|
|
|
|
(Pair.fst (Pair.new fst snd)) = fst
|
|
|
|
|
(U60.to_nat 0) = (Nat.zero)
|
|
|
|
|
(U60.to_nat n) = (Nat.succ (U60.to_nat (- n 1)))
|
|
|
|
|
(List.take (List.cons head tail) (Nat.succ pred)) = (List.cons head (List.take tail pred))
|
|
|
|
|
(List.take [] (Nat.succ pred)) = []
|
|
|
|
|
(List.take xs (Nat.zero)) = []
|
|
|
|
|
(List.any [] cond) = (Bool.false)
|
|
|
|
|
(List.any (List.cons head tail) cond) = (Bool.if (cond head) (Bool.true) (List.all tail cond))
|
|
|
|
|
(List.all [] cond) = (Bool.true)
|
|
|
|
|
(List.all (List.cons head tail) cond) = (Bool.if (cond head) (List.all tail cond) (Bool.false))
|
|
|
|
|
(Kind.Coverage.Choice.match (Kind.Coverage.Choice.on_cons name_) on_cons on_U60 none) = (on_cons name_)
|
|
|
|
|
(Kind.Coverage.Choice.match (Kind.Coverage.Choice.on_U60) on_cons on_U60 none) = on_U60
|
|
|
|
|
(Kind.Coverage.Choice.match (Kind.Coverage.Choice.none) on_cons on_U60 none) = none
|
|
|
|
|
(Kind.Coverage.Problem.rows.get (Kind.Coverage.Problem.new type_ rows_ count_)) = rows_
|
|
|
|
|
(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.Coverage.catches (Kind.Coverage.Problem.new type rows count)) = (List.all rows λx (Kind.Coverage.Row.catches x))
|
|
|
|
|
(List.head []) = (Maybe.none)
|
|
|
|
|
(List.head (List.cons head tail)) = (Maybe.some head)
|
|
|
|
|
(Kind.Checker.fail err) = λcontext λdepth λrhs λsubst λeqts λerrs (Kind.Result.errored context subst (List.cons err errs))
|
|
|
|
|
(Kind.Coverage.Rule.size (Kind.Rule.lhs x xs)) = (+ 1 (Kind.Coverage.Rule.size xs))
|
|
|
|
|
(Kind.Coverage.Rule.size x_1) = 0
|
|
|
|
|
(Kind.API.check_function.rules [] type) = []
|
|
|
|
|
(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 (Kind.Rule.lhs arg args) (Kind.Term.all orig name type body)) = (Kind.Checker.bind (Kind.Checker.check arg type) λx_2 (Kind.Checker.bind (Kind.Checker.rule args (body arg)) λx_1 (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)) λx_4 (Kind.Checker.bind (Kind.Checker.check expr type) λx_3 (Kind.Checker.pure (Unit.new))))
|
|
|
|
|
(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 []) λ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 [(Kind.Term.eval expr)]) λ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)) λx_25 (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)) λx_13 (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 [])))
|
|
|
|
|
(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 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.fail err) = λcontext λdepth λrhs λsubst λeqts λerrs (Kind.Result.errored context subst (List.cons err errs))
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.var orig name index)) = (Kind.Checker.bind (Kind.Checker.find index (Maybe.none) λn λt λv (Maybe.some t)) λgot_type (Maybe.match got_type (Kind.Checker.bind (Kind.Checker.get_context) λctx (Kind.Checker.fail (Kind.Error.unbound_variable ctx orig))) λvalue (Kind.Checker.pure value)))
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.var orig name index)) = (Kind.Checker.bind (Kind.Checker.find index (Maybe.none) λn λt λv (Maybe.some t)) λgot_type (Maybe.match got_type (Kind.Checker.bind (Kind.Checker.get_context) λctx (Kind.Checker.fail (Kind.Error.unbound_variable ctx orig))) λgot_type.value (Kind.Checker.pure got_type.value)))
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.hol orig numb)) = (Kind.Checker.bind (Kind.Checker.get_context) λctx (Kind.Checker.fail (Kind.Error.cant_infer_hole ctx orig)))
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.typ orig)) = (Kind.Checker.pure (Kind.Term.typ orig))
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.all orig name type body)) = (Kind.Checker.bind (Kind.Checker.get_depth) λdepth (Kind.Checker.bind (Kind.Checker.check type (Kind.Term.typ orig)) λx_2 (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.check (body (Kind.Term.var orig name depth)) (Kind.Term.typ orig)) name (Kind.Term.eval type) []) λx_1 (Kind.Checker.pure (Kind.Term.typ orig)))))
|
|
|
|
@ -480,8 +486,8 @@
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.app orig func argm)) = (Kind.Checker.bind (Kind.Checker.infer func) λfn_infer (Kind.Checker.bind (Kind.Checker.infer.forall fn_infer λfn_orig λfn_name λfn_type λfn_body (Kind.Checker.bind (Kind.Checker.check argm fn_type) λx_3 (Kind.Checker.pure (fn_body (Kind.Term.eval argm)))) (Kind.Checker.bind (Kind.Checker.get_context) λctx (Kind.Checker.fail (Kind.Error.invalid_call ctx orig)))) λap_infer (Kind.Checker.pure ap_infer)))
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.let orig name expr body)) = (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.infer (body (Kind.Term.var orig name dep))) name expr_typ [(Kind.Term.eval expr)]) λbody_typ (Kind.Checker.pure body_typ))))
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.ann orig expr type)) = let type = (Kind.Term.eval type); (Kind.Checker.bind (Kind.Checker.check expr type) λx_4 (Kind.Checker.pure type))
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.sub orig name indx redx expr)) = (Kind.Checker.bind (Kind.Checker.get_depth) λdep (Kind.Checker.bind (Kind.Checker.find indx (Maybe.none) λn λt λv (Maybe.some (Pair.new t v))) λgot (Maybe.match got (Kind.Checker.bind (Kind.Checker.get_context) λctx (Kind.Checker.fail (Kind.Error.unbound_variable ctx orig))) λvalue (Pair.match value λx_5 λsnd (Maybe.match (List.at.u60 snd redx) (Kind.Checker.bind (Kind.Checker.get_context) λctx (Kind.Checker.fail (Kind.Error.unbound_variable ctx orig))) λvalue (Kind.Checker.bind (Kind.Checker.infer expr) λexpr_typ (Kind.Checker.pure (Kind.Term.eval (Kind.Term.replace expr_typ indx value)))))))))
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.ct0 ctid orig)) = (Kind.Checker.pure (Kind.Term.eval (TypeOf ctid)))
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.sub orig name indx redx expr)) = (Kind.Checker.bind (Kind.Checker.get_depth) λdep (Kind.Checker.bind (Kind.Checker.find indx (Maybe.none) λn λt λv (Maybe.some (Pair.new t v))) λgot (Maybe.match got (Kind.Checker.bind (Kind.Checker.get_context) λctx (Kind.Checker.fail (Kind.Error.unbound_variable ctx orig))) λgot.value (Pair.new.match got.value λgot.value.fst λgot.value.snd (Maybe.match (List.at.u60 got.value.snd redx) (Kind.Checker.bind (Kind.Checker.get_context) λctx (Kind.Checker.fail (Kind.Error.unbound_variable ctx orig))) λreduction.value (Kind.Checker.bind (Kind.Checker.infer expr) λexpr_typ (Kind.Checker.pure (Kind.Term.eval (Kind.Term.replace expr_typ indx reduction.value)))))))))
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.ct0 ctid orig)) = (Kind.Checker.pure (Kind.Term.eval (Kind.Axiom.TypeOf ctid)))
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.ct1 ctid orig x0)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0))
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.ct2 ctid orig x0 x1)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1))
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.ct3 ctid orig x0 x1 x2)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2))
|
|
|
|
@ -498,7 +504,7 @@
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.ct14 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Checker.infer (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.ct0 ctid orig) x0) x1) x2) x3) x4) x5) x6) x7) x8) x9) x10) x11) x12) x13))
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.ct15 ctid orig x0)) = let expr = (Kind.Checker.infer_args x0); (Kind.Checker.infer (expr (Kind.Term.ct0 ctid orig) orig))
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.ct16 ctid orig x0)) = let expr = (Kind.Checker.infer_args x0); (Kind.Checker.infer (expr (Kind.Term.ct0 ctid orig) orig))
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.fn0 fnid orig)) = (Kind.Checker.pure (Kind.Term.eval (TypeOf fnid)))
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.fn0 fnid orig)) = (Kind.Checker.pure (Kind.Term.eval (Kind.Axiom.TypeOf fnid)))
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.fn1 fnid orig x0)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0))
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.fn2 fnid orig x0 x1)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1))
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.fn3 fnid orig x0 x1 x2)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 fnid orig) x0) x1) x2))
|
|
|
|
@ -518,15 +524,7 @@
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.hlp orig)) = (Kind.Checker.bind (Kind.Checker.get_context) λctx (Kind.Checker.fail (Kind.Error.inspection ctx orig (Kind.Term.hlp 0))))
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.U60 orig)) = (Kind.Checker.pure (Kind.Term.typ 0))
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.u60 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)) λx_7 (Kind.Checker.bind (Kind.Checker.check right (Kind.Term.U60 0)) λx_6 (Kind.Checker.pure (Kind.Term.U60 0))))
|
|
|
|
|
(Kind.Checker.infer.forall (Kind.Term.all orig name type body) then_fn else_val) = (then_fn orig name type body)
|
|
|
|
|
(Kind.Checker.infer.forall (Kind.Term.var orig name index) then_fn else_val) = (Kind.Checker.bind (Kind.Checker.find index [] λn λt λv v) λreducs (Kind.Checker.bind (Kind.Checker.infer.forall.try_values reducs then_fn else_val) λresult (Kind.Checker.pure result)))
|
|
|
|
|
(Kind.Checker.infer.forall other then_fn else_val) = else_val
|
|
|
|
|
(Kind.Checker.infer.forall.try_values (List.cons (Kind.Term.all orig name type body) terms) then_fn else_val) = (then_fn orig name type body)
|
|
|
|
|
(Kind.Checker.infer.forall.try_values (List.cons other terms) then_fn else_val) = (Kind.Checker.infer.forall.try_values terms then_fn else_val)
|
|
|
|
|
(Kind.Checker.infer.forall.try_values [] then_fn else_val) = else_val
|
|
|
|
|
(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)
|
|
|
|
|
(Kind.Checker.infer (Kind.Term.op2 orig oper left right)) = (Kind.Checker.bind (Kind.Checker.check left (Kind.Term.U60 0)) λx_6 (Kind.Checker.bind (Kind.Checker.check right (Kind.Term.U60 0)) λx_5 (Kind.Checker.pure (Kind.Term.U60 0))))
|
|
|
|
|
(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))
|
|
|
|
|
(Kind.Term.replace (Kind.Term.all orig name typ body) idx val) = (Kind.Term.all orig name (Kind.Term.replace typ idx val) λx (Kind.Term.replace (body x) idx val))
|
|
|
|
@ -572,11 +570,19 @@
|
|
|
|
|
(Kind.Term.replace (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) idx val) = (Kind.Term.args15 (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 (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.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)
|
|
|
|
|
(Kind.Checker.infer.forall (Kind.Term.all orig name type body) then_fn else_val) = (then_fn orig name type body)
|
|
|
|
|
(Kind.Checker.infer.forall (Kind.Term.var orig name index) then_fn else_val) = (Kind.Checker.bind (Kind.Checker.find index [] λn λt λv v) λreducs (Kind.Checker.bind (Kind.Checker.infer.forall.try_values reducs then_fn else_val) λresult (Kind.Checker.pure result)))
|
|
|
|
|
(Kind.Checker.infer.forall other then_fn else_val) = else_val
|
|
|
|
|
(Kind.Checker.infer.forall.try_values (List.cons (Kind.Term.all orig name type body) terms) then_fn else_val) = (then_fn orig name type body)
|
|
|
|
|
(Kind.Checker.infer.forall.try_values (List.cons other terms) then_fn else_val) = (Kind.Checker.infer.forall.try_values terms then_fn else_val)
|
|
|
|
|
(Kind.Checker.infer.forall.try_values [] then_fn else_val) = else_val
|
|
|
|
|
(Pair.new.match (Pair.new fst_ snd_) new) = (new fst_ snd_)
|
|
|
|
|
(List.at.u60 [] idx) = (Maybe.none)
|
|
|
|
|
(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.get_context) = λcontext λdepth λrhs λsubst λeqts λerrs (Kind.Result.checked context depth rhs subst eqts errs context)
|
|
|
|
|
(Pair.match (Pair.new fst_ snd_) new) = (new fst_ snd_)
|
|
|
|
|
(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.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))
|
|
|
|
|
(Kind.Term.get_origin (Kind.Term.hol orig numb) got) = (got orig (Kind.Term.hol orig numb))
|
|
|
|
@ -625,22 +631,11 @@
|
|
|
|
|
(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.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 [] x) = (List.pure x)
|
|
|
|
|
(List.append [] x) = [x]
|
|
|
|
|
(List.append (List.cons xs.h xs.t) x) = (List.cons xs.h (List.append xs.t x))
|
|
|
|
|
(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.run checker rhs) = (checker (Kind.Context.empty) 0 rhs (Kind.Subst.end) [] [])
|
|
|
|
|
(Kind.API.check_function.rules [] type) = []
|
|
|
|
|
(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 (Kind.Rule.lhs arg args) (Kind.Term.all orig name type body)) = (Kind.Checker.bind (Kind.Checker.check arg type) λx_2 (Kind.Checker.bind (Kind.Checker.rule args (body arg)) λx_1 (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)) λx_4 (Kind.Checker.bind (Kind.Checker.check expr type) λx_3 (Kind.Checker.pure (Unit.new))))
|
|
|
|
|
(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 xs) = (List.reverse.go xs [])
|
|
|
|
|
(List.reverse.go [] ys) = ys
|
|
|
|
|
(List.reverse.go (List.cons x xs) ys) = (List.reverse.go xs (List.cons x ys))
|
|
|
|
|
(Kind.API.output []) = []
|
|
|
|
|
(Kind.API.output (List.cons pair rest)) = (Pair.match pair λfst λsnd (List.concat (Kind.API.output.function fst snd) (Kind.API.output rest)))
|
|
|
|
|
(Kind.API.output (List.cons pair rest)) = (Pair.new.match pair λfst λsnd (List.concat (Kind.API.output.function fst snd) (Kind.API.output rest)))
|
|
|
|
|
(Kind.API.output.function fnid []) = []
|
|
|
|
|
(Kind.API.output.function fnid (List.cons (Kind.Result.checked ctx dep rhs sub eqt err val) checks)) = (Kind.API.output.function.show_errors err sub fnid checks)
|
|
|
|
|
(Kind.API.output.function fnid (List.cons (Kind.Result.errored ctx sub err) checks)) = (Kind.API.output.function.show_errors err sub fnid checks)
|
|
|
|
@ -655,6 +650,9 @@
|
|
|
|
|
(Kind.Error.quote (Kind.Error.inspection ctx orig term) sub) = (Kind.Error.Quoted.inspection (Kind.Context.quote ctx sub) orig (Kind.Term.quote term sub))
|
|
|
|
|
(Kind.Error.quote (Kind.Error.too_many_arguments ctx orig) sub) = (Kind.Error.Quoted.too_many_arguments (Kind.Context.quote ctx sub) orig)
|
|
|
|
|
(Kind.Error.quote (Kind.Error.type_mismatch ctx orig expected detected) sub) = (Kind.Error.Quoted.type_mismatch (Kind.Context.quote ctx sub) orig (Kind.Term.quote expected sub) (Kind.Term.quote detected sub))
|
|
|
|
|
(Kind.Error.quote (Kind.Error.uncovered_pattern ctx orig res) sub) = (Kind.Error.Quoted.uncovered_pattern (Kind.Context.quote ctx sub) orig res)
|
|
|
|
|
(Kind.Context.quote (Kind.Context.empty) sub) = []
|
|
|
|
|
(Kind.Context.quote (Kind.Context.entry name type vals rest) sub) = (List.cons (Pair.new name (Pair.new (Kind.Term.quote type sub) (List.map vals λx (Kind.Term.quote x sub)))) (Kind.Context.quote rest sub))
|
|
|
|
|
(Kind.Term.quote term sub) = (Kind.Term.quote.go (Kind.Term.fill term sub))
|
|
|
|
|
(Kind.Term.quote.go (Kind.Term.typ orig)) = (Kind.Term.Quoted.typ orig)
|
|
|
|
|
(Kind.Term.quote.go (Kind.Term.var orig name index)) = (Kind.Term.Quoted.var orig name index)
|
|
|
|
@ -705,9 +703,105 @@
|
|
|
|
|
(Kind.Term.quote.go (Kind.Term.op2 orig operator left right)) = (Kind.Term.Quoted.op2 orig operator (Kind.Term.quote.go left) (Kind.Term.quote.go right))
|
|
|
|
|
(Kind.Term.quote.args (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)) = [(Kind.Term.quote.go x0), (Kind.Term.quote.go x1), (Kind.Term.quote.go x2), (Kind.Term.quote.go x3), (Kind.Term.quote.go x4), (Kind.Term.quote.go x5), (Kind.Term.quote.go x6), (Kind.Term.quote.go x7), (Kind.Term.quote.go x8), (Kind.Term.quote.go x9), (Kind.Term.quote.go x10), (Kind.Term.quote.go x11), (Kind.Term.quote.go x12), (Kind.Term.quote.go x13), (Kind.Term.quote.go x14)]
|
|
|
|
|
(Kind.Term.quote.args (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)) = [(Kind.Term.quote.go x0), (Kind.Term.quote.go x1), (Kind.Term.quote.go x2), (Kind.Term.quote.go x3), (Kind.Term.quote.go x4), (Kind.Term.quote.go x5), (Kind.Term.quote.go x6), (Kind.Term.quote.go x7), (Kind.Term.quote.go x8), (Kind.Term.quote.go x9), (Kind.Term.quote.go x10), (Kind.Term.quote.go x11), (Kind.Term.quote.go x12), (Kind.Term.quote.go x13), (Kind.Term.quote.go x14), (Kind.Term.quote.go x15)]
|
|
|
|
|
(Kind.Context.quote (Kind.Context.empty) sub) = []
|
|
|
|
|
(Kind.Context.quote (Kind.Context.entry name type vals rest) sub) = (List.cons (Pair.new name (Pair.new (Kind.Term.quote type sub) (List.map vals λx (Kind.Term.quote x sub)))) (Kind.Context.quote rest sub))
|
|
|
|
|
(List.map [] f) = []
|
|
|
|
|
(List.map (List.cons head tail) f) = (List.cons (f head) (List.map tail f))
|
|
|
|
|
(List.concat [] ys) = ys
|
|
|
|
|
(List.concat (List.cons head tail) ys) = (List.cons head (List.concat tail ys))
|
|
|
|
|
(Kind.API.eval_main) = (Kind.Printer.text [(Kind.Term.show (Kind.Term.FN0 (Main.) 0)), (String.pure (Char.newline)), (String.pure (Char.newline))])
|
|
|
|
|
(Kind.Term.show term) = let sugars = [(Kind.Term.show.sugar.string term), (Kind.Term.show.sugar.list term), (Kind.Term.show.sugar.sigma term)]; (Maybe.try sugars (Kind.Term.show.go term))
|
|
|
|
|
(Maybe.try [] alt) = alt
|
|
|
|
|
(Maybe.try (List.cons maybe xs) alt) = (Maybe.match maybe (Maybe.try xs alt) λvalue value)
|
|
|
|
|
(Kind.Term.show.sugar.list term) = (Maybe.bind (Kind.Term.show.sugar.list.go term) λres (Maybe.some (Kind.Printer.text ["[", (String.join " " res), "]"])))
|
|
|
|
|
(Kind.Printer.text []) = ""
|
|
|
|
|
(Kind.Printer.text (List.cons x xs)) = (String.concat x (Kind.Printer.text xs))
|
|
|
|
|
(String.concat (String.cons x xs) ys) = (String.cons x (String.concat xs ys))
|
|
|
|
|
(String.concat "" ys) = ys
|
|
|
|
|
(Kind.Term.show.sugar.list.go (Kind.Term.ct0 (List.nil.) orig)) = (Maybe.some [])
|
|
|
|
|
(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.some (List.cons (Kind.Term.show x0) tail)))
|
|
|
|
|
(Kind.Term.show.sugar.list.go other) = (Maybe.none)
|
|
|
|
|
(Maybe.bind (Maybe.none) mb) = (Maybe.none)
|
|
|
|
|
(Maybe.bind (Maybe.some val) mb) = (mb val)
|
|
|
|
|
(String.join sep list) = (String.intercalate sep list)
|
|
|
|
|
(String.intercalate sep xs) = (String.flatten (List.intersperse sep xs))
|
|
|
|
|
(String.flatten []) = ""
|
|
|
|
|
(String.flatten (List.cons head tail)) = (String.concat head (String.flatten tail))
|
|
|
|
|
(List.intersperse sep []) = []
|
|
|
|
|
(List.intersperse sep [xh]) = [xh]
|
|
|
|
|
(List.intersperse sep (List.cons xh xt)) = (List.cons xh (List.cons sep (List.intersperse sep xt)))
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.typ orig)) = "Type"
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.var orig name index)) = (Kind.Printer.text [(Kind.Name.show name)])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.hol orig numb)) = (Kind.Printer.text ["_"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.all orig name type body)) = (Kind.Term.show.forall orig name type body)
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.lam orig name body)) = (Kind.Printer.text ["(", (Kind.Name.show name), " => ", (Kind.Term.show (body (Kind.Term.var orig name 0))), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.let orig name exp body)) = (Kind.Printer.text ["let ", (Kind.Name.show name), " = ", (Kind.Term.show exp), "; ", (Kind.Term.show (body (Kind.Term.var orig name 0)))])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ann orig expr type)) = (Kind.Printer.text ["{", (Kind.Term.show expr), " :: ", (Kind.Term.show type), "}"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.sub orig name indx redx expr)) = (Kind.Printer.text [(Kind.Term.show expr), " ## ", (Kind.Name.show name), "/", (Show.to_string (U60.show redx))])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.app orig func argm)) = (Kind.Printer.text ["(", (Kind.Term.show func), " ", (Kind.Term.show argm), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct0 ctid orig)) = (Kind.Axiom.NameOf ctid)
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct1 ctid orig x0)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct2 ctid orig x0 x1)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct3 ctid orig x0 x1 x2)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct4 ctid orig x0 x1 x2 x3)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct7 ctid orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct8 ctid orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct9 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct10 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct11 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct12 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct13 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct14 ctid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), " ", (Kind.Term.show x13), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct15 ctid orig x0)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.ct16 ctid orig x0)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf ctid), " ", (Kind.Term.show x0), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn0 fnid orig)) = (Kind.Axiom.NameOf fnid)
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn1 fnid orig x0)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn2 fnid orig x0 x1)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn3 fnid orig x0 x1 x2)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn4 fnid orig x0 x1 x2 x3)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn7 fnid orig x0 x1 x2 x3 x4 x5 x6)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn8 fnid orig x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn9 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn10 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn11 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn12 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn13 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn14 fnid orig x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), " ", (Kind.Term.show x13), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn15 fnid orig x0)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.fn16 fnid orig x0)) = (Kind.Printer.text ["(", (Kind.Axiom.NameOf fnid), " ", (Kind.Term.show x0), ")"])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.args15 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)) = (Kind.Printer.text [(Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), " ", (Kind.Term.show x13), " ", (Kind.Term.show x14)])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.args16 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)) = (Kind.Printer.text [(Kind.Term.show x0), " ", (Kind.Term.show x1), " ", (Kind.Term.show x2), " ", (Kind.Term.show x3), " ", (Kind.Term.show x4), " ", (Kind.Term.show x5), " ", (Kind.Term.show x6), " ", (Kind.Term.show x7), " ", (Kind.Term.show x8), " ", (Kind.Term.show x9), " ", (Kind.Term.show x10), " ", (Kind.Term.show x11), " ", (Kind.Term.show x12), " ", (Kind.Term.show x13), " ", (Kind.Term.show x14), " ", (Kind.Term.show x15)])
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.hlp orig)) = "?"
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.U60 orig)) = "U60"
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.u60 orig numb)) = (Show.to_string (U60.show numb))
|
|
|
|
|
(Kind.Term.show.go (Kind.Term.op2 orig operator left right)) = (Kind.Printer.text ["(", (Kind.Operator.show operator), " ", (Kind.Term.show left), " ", (Kind.Term.show right), ")"])
|
|
|
|
|
(Show.to_string show) = (show "")
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.add)) = "+"
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.sub)) = "-"
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.mul)) = "*"
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.div)) = "/"
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.mod)) = "%"
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.and)) = "&"
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.or)) = "|"
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.xor)) = "^"
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.shl)) = "<<"
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.shr)) = ">>"
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.ltn)) = "<"
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.lte)) = "<="
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.eql)) = "=="
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.gte)) = ">="
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.gtn)) = ">"
|
|
|
|
|
(Kind.Operator.show (Kind.Operator.neq)) = "!="
|
|
|
|
|
(Kind.Term.show.forall orig name type body) = (U60.if (== name 63) (Kind.Printer.text ["(", (Kind.Term.show type), " -> ", (Kind.Term.show (body (Kind.Term.var orig name 0))), ")"]) (Kind.Printer.text ["((", (Kind.Name.show name), ": ", (Kind.Term.show type), ") -> ", (Kind.Term.show (body (Kind.Term.var orig name 0))), ")"]))
|
|
|
|
|
(Kind.Name.show name) = (Kind.Name.show.go name "")
|
|
|
|
|
(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)))
|
|
|
|
|
(U60.if 0 t f) = f
|
|
|
|
|
(U60.if n t f) = t
|
|
|
|
|
(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.Term.show.sugar.sigma (Kind.Term.ct2 (Sigma.) orig typ (Kind.Term.lam orig_ name body))) = (Maybe.some (Kind.Printer.text ["([", (Kind.Name.show name), ": ", (Kind.Term.show typ), "] -> ", (Kind.Term.show (body (Kind.Term.var orig_ name 0))), ")"]))
|
|
|
|
|
(Kind.Term.show.sugar.sigma term) = (Maybe.none)
|
|
|
|
|
(Kind.Term.show.sugar.string term) = (Maybe.bind (Kind.Term.show.sugar.string.go term) λres let quot = "'"; (Maybe.some (Kind.Printer.text [quot, res, quot])))
|
|
|
|
|
(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.u60 orig1 x0) x1)) = (Maybe.bind (Kind.Term.show.sugar.string.go x1) λtail (Maybe.some (String.cons x0 tail)))
|
|
|
|
|
(Kind.Term.show.sugar.string.go other) = (Maybe.none)
|
|
|
|
|