mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-07-14 22:40:33 +03:00
wip
This commit is contained in:
Victor Taelin
parent
9a6ffc9a81
commit
4fd07958bc
631
book/.check.hvm1
631
book/.check.hvm1
@ -82,12 +82,16 @@
|
||||
|
||||
(Pair.get (Pair fst snd) fun) = (fun fst snd)
|
||||
|
||||
(Maybe.match (Some value) some none) = (some value)
|
||||
(Maybe.match None some none) = none
|
||||
|
||||
(Maybe.pure x) = (Some x)
|
||||
(Maybe.bind a b) = (Maybe.match a λvalue(b value) None)
|
||||
|
||||
(Maybe.bind a b) = (Maybe.bind.match a b)
|
||||
|
||||
(Maybe.bind.match None b) = None
|
||||
(Maybe.bind.match (Some a) b) = (b a)
|
||||
// Converts an U60 to a bitstring
|
||||
(U60.to_bits 0) = E
|
||||
(U60.to_bits 1) = (I E)
|
||||
(U60.to_bits n) = (If (== (% n 2) 0) (O (U60.to_bits (/ n 2))) (I (U60.to_bits (/ n 2))))
|
||||
|
||||
(String.color RESET) = (String.cons 27 "[0m")
|
||||
(String.color BRIGHT) = (String.cons 27 "[1m")
|
||||
@ -116,73 +120,145 @@
|
||||
(String.color BG_GRAY) = (String.cons 27 "[100m")
|
||||
(String.color x) = "?"
|
||||
|
||||
// BitsMap
|
||||
// -------
|
||||
|
||||
//// data BM A = BM.Nil | (BM.Node A BM BM)
|
||||
|
||||
//// Returns true if value is present on BM
|
||||
//(BM.has E (BM.node (Some val) lft rgt)) = 1
|
||||
//(BM.has (O bits) (BM.node val lft rgt)) = (BM.has bits lft)
|
||||
//(BM.has (I bits) (BM.node val lft rgt)) = (BM.has bits rgt)
|
||||
//(BM.has key val) = 0
|
||||
|
||||
//// Gets a value from a BM
|
||||
//(BM.get E (BM.leaf)) = None
|
||||
//(BM.get E (BM.node val lft rgt)) = val
|
||||
//(BM.get (O bits) (BM.leaf)) = None
|
||||
//(BM.get (O bits) (BM.node val lft rgt)) = (BM.get bits lft)
|
||||
//(BM.get (I bits) (BM.leaf)) = None
|
||||
//(BM.get (I bits) (BM.node val lft rgt)) = (BM.get bits rgt)
|
||||
|
||||
//// Sets a value on a BM
|
||||
//(BM.set E val (BM.leaf)) = (BM.node (Some val) BM.leaf BM.leaf)
|
||||
//(BM.set E val (BM.node _ lft rgt)) = (BM.node (Some val) lft rgt)
|
||||
//(BM.set (O bits) val (BM.leaf)) = (BM.node None (BM.set bits val BM.leaf) BM.leaf)
|
||||
//(BM.set (O bits) val (BM.node v lft rgt)) = (BM.node v (BM.set bits val lft) rgt)
|
||||
//(BM.set (I bits) val (BM.leaf)) = (BM.node None BM.leaf (BM.set bits val BM.leaf))
|
||||
//(BM.set (I bits) val (BM.node v lft rgt)) = (BM.node v lft (BM.set bits val rgt))
|
||||
|
||||
//// Map wrapper with String keys
|
||||
//(Map.new) = BM.leaf
|
||||
//(Map.has key map) = (BM.has (U60.to_bits key) map)
|
||||
//(Map.get key map) = (BM.get (U60.to_bits key) map)
|
||||
//(Map.set key val map) = (BM.set (U60.to_bits key) val map)
|
||||
|
||||
(Map.new) = List.nil
|
||||
|
||||
(Map.has k (List.cons (Pair key val) map)) = (If (Same key k) 1 (Map.has k map))
|
||||
(Map.has k List.nil) = 0
|
||||
|
||||
(Map.put k v (List.cons (Pair key val) map)) = ((If (Same key k) λmap(None) λmap(Maybe.bind (Map.set k v map) λmap (List.cons (Pair key val) map))) map)
|
||||
(Map.put k v List.nil) = (Some (List.cons (Pair k v) List.nil))
|
||||
|
||||
(Map.set k v (List.cons (Pair key val) map)) = ((If (Same key k) λmap(List.cons (Pair k v) map) λmap(List.cons (Pair key val) (Map.set k v map))) map)
|
||||
(Map.set k v List.nil) = (List.cons (Pair k v) List.nil)
|
||||
|
||||
(Map.get k (List.cons (Pair key val) map)) = (If (Same key k) (Some val) (Map.get k map))
|
||||
(Map.get k List.nil) = None
|
||||
|
||||
// Evaluation
|
||||
// ----------
|
||||
|
||||
(Reduce lv (App fun arg)) = (Reduce.app lv (Reduce lv fun) arg)
|
||||
(Reduce lv (Ann val typ)) = (Reduce lv val)
|
||||
(Reduce lv (Ins val)) = (Reduce lv val)
|
||||
(Reduce lv (Ref nam val)) = (Reduce.ref lv nam (Reduce lv val))
|
||||
(Reduce lv (Let nam val bod)) = (Reduce lv (bod val))
|
||||
(Reduce lv (Op2 opr fst snd)) = (Reduce.op2 lv opr (Reduce lv fst) (Reduce lv snd))
|
||||
(Reduce lv (Mat nam x z s p)) = (Reduce.mat lv nam (Reduce lv x) z s p)
|
||||
(Reduce lv (Txt txt)) = (Reduce.txt lv txt)
|
||||
(Reduce lv (Src src val)) = (Reduce lv val)
|
||||
(Reduce lv val) = val
|
||||
(Reduce fill lv (App fun arg)) = (Reduce.app fill lv (Reduce fill lv fun) arg)
|
||||
(Reduce fill lv (Ann val typ)) = (Reduce fill lv val)
|
||||
(Reduce fill lv (Ins val)) = (Reduce fill lv val)
|
||||
(Reduce fill lv (Ref nam val)) = (Reduce.ref fill lv nam (Reduce fill lv val))
|
||||
(Reduce fill lv (Let nam val bod)) = (Reduce fill lv (bod val))
|
||||
(Reduce fill lv (Op2 opr fst snd)) = (Reduce.op2 fill lv opr (Reduce fill lv fst) (Reduce fill lv snd))
|
||||
(Reduce fill lv (Mat nam x z s p)) = (Reduce.mat fill lv nam (Reduce fill lv x) z s p)
|
||||
(Reduce fill lv (Txt txt)) = (Reduce.txt fill lv txt)
|
||||
(Reduce fill lv (Src src val)) = (Reduce fill lv val)
|
||||
(Reduce fill lv (Hol nam ctx)) = (Reduce.hol fill lv nam ctx)
|
||||
(Reduce fill lv val) = val
|
||||
|
||||
(Reduce.app lv (Lam nam bod) arg) = (Reduce lv (bod (Reduce 0 arg)))
|
||||
(Reduce.app lv fun arg) = (App fun arg)
|
||||
(Reduce.app fill lv (Lam nam bod) arg) = (Reduce fill lv (bod (Reduce fill 0 arg)))
|
||||
(Reduce.app fill lv fun arg) = (App fun arg)
|
||||
|
||||
(Reduce.op2 lv ADD (Num fst) (Num snd)) = (Num (+ fst snd))
|
||||
(Reduce.op2 lv SUB (Num fst) (Num snd)) = (Num (- fst snd))
|
||||
(Reduce.op2 lv MUL (Num fst) (Num snd)) = (Num (* fst snd))
|
||||
(Reduce.op2 lv DIV (Num fst) (Num snd)) = (Num (/ fst snd))
|
||||
(Reduce.op2 lv MOD (Num fst) (Num snd)) = (Num (% fst snd))
|
||||
(Reduce.op2 lv EQ (Num fst) (Num snd)) = (Num (== fst snd))
|
||||
(Reduce.op2 lv NE (Num fst) (Num snd)) = (Num (!= fst snd))
|
||||
(Reduce.op2 lv LT (Num fst) (Num snd)) = (Num (< fst snd))
|
||||
(Reduce.op2 lv GT (Num fst) (Num snd)) = (Num (> fst snd))
|
||||
(Reduce.op2 lv LTE (Num fst) (Num snd)) = (Num (<= fst snd))
|
||||
(Reduce.op2 lv GTE (Num fst) (Num snd)) = (Num (>= fst snd))
|
||||
(Reduce.op2 lv AND (Num fst) (Num snd)) = (Num (& fst snd))
|
||||
(Reduce.op2 lv OR (Num fst) (Num snd)) = (Num (| fst snd))
|
||||
(Reduce.op2 lv XOR (Num fst) (Num snd)) = (Num (^ fst snd))
|
||||
(Reduce.op2 lv LSH (Num fst) (Num snd)) = (Num (<< fst snd))
|
||||
(Reduce.op2 lv RSH (Num fst) (Num snd)) = (Num (>> fst snd))
|
||||
(Reduce.op2 lv opr fst snd) = (Op2 opr fst snd)
|
||||
(Reduce.op2 fill lv ADD (Num fst) (Num snd)) = (Num (+ fst snd))
|
||||
(Reduce.op2 fill lv SUB (Num fst) (Num snd)) = (Num (- fst snd))
|
||||
(Reduce.op2 fill lv MUL (Num fst) (Num snd)) = (Num (* fst snd))
|
||||
(Reduce.op2 fill lv DIV (Num fst) (Num snd)) = (Num (/ fst snd))
|
||||
(Reduce.op2 fill lv MOD (Num fst) (Num snd)) = (Num (% fst snd))
|
||||
(Reduce.op2 fill lv EQ (Num fst) (Num snd)) = (Num (== fst snd))
|
||||
(Reduce.op2 fill lv NE (Num fst) (Num snd)) = (Num (!= fst snd))
|
||||
(Reduce.op2 fill lv LT (Num fst) (Num snd)) = (Num (< fst snd))
|
||||
(Reduce.op2 fill lv GT (Num fst) (Num snd)) = (Num (> fst snd))
|
||||
(Reduce.op2 fill lv LTE (Num fst) (Num snd)) = (Num (<= fst snd))
|
||||
(Reduce.op2 fill lv GTE (Num fst) (Num snd)) = (Num (>= fst snd))
|
||||
(Reduce.op2 fill lv AND (Num fst) (Num snd)) = (Num (& fst snd))
|
||||
(Reduce.op2 fill lv OR (Num fst) (Num snd)) = (Num (| fst snd))
|
||||
(Reduce.op2 fill lv XOR (Num fst) (Num snd)) = (Num (^ fst snd))
|
||||
(Reduce.op2 fill lv LSH (Num fst) (Num snd)) = (Num (<< fst snd))
|
||||
(Reduce.op2 fill lv RSH (Num fst) (Num snd)) = (Num (>> fst snd))
|
||||
(Reduce.op2 fill lv opr fst snd) = (Op2 opr fst snd)
|
||||
|
||||
(Reduce.mat lv nam (Num 0) z s p) = (Reduce lv z)
|
||||
(Reduce.mat lv nam (Num n) z s p) = (Reduce lv (s (Num (- n 1))))
|
||||
(Reduce.mat lv nam (Op2 ADD (Num 1) k) z s p) = (Reduce lv (s k))
|
||||
(Reduce.mat lv nam val z s p) = (Mat nam val z s p)
|
||||
(Reduce.mat fill lv nam (Num 0) z s p) = (Reduce fill lv z)
|
||||
(Reduce.mat fill lv nam (Num n) z s p) = (Reduce fill lv (s (Num (- n 1))))
|
||||
(Reduce.mat fill lv nam (Op2 ADD (Num 1) k) z s p) = (Reduce fill lv (s k))
|
||||
(Reduce.mat fill lv nam val z s p) = (Mat nam val z s p)
|
||||
|
||||
(Reduce.ref 1 nam val) = (Reduce 1 val)
|
||||
(Reduce.ref 2 nam val) = (Reduce 2 val)
|
||||
(Reduce.ref lv nam val) = (Ref nam val)
|
||||
(Reduce.ref fill 1 nam val) = (Reduce fill 1 val)
|
||||
(Reduce.ref fill 2 nam val) = (Reduce fill 2 val)
|
||||
(Reduce.ref fill lv nam val) = (Ref nam val)
|
||||
|
||||
(Reduce.txt lv (String.cons x xs)) = (Reduce lv (App (App Book.String.cons (Num x)) (Txt xs)))
|
||||
(Reduce.txt lv String.nil) = (Reduce lv Book.String.nil)
|
||||
(Reduce.txt lv val) = (Txt val)
|
||||
(Reduce.txt fill lv (String.cons x xs)) = (Reduce fill lv (App (App Book.String.cons (Num x)) (Txt xs)))
|
||||
(Reduce.txt fill lv String.nil) = (Reduce fill lv Book.String.nil)
|
||||
(Reduce.txt fill lv val) = (Txt val)
|
||||
|
||||
(Normal lv term dep) = (Normal.term lv (Reduce lv term) dep)
|
||||
(Reduce.hol fill lv nam ctx) = (Maybe.match (Map.get nam fill) λval(Reduce fill lv val) (Hol nam ctx))
|
||||
|
||||
(Normal.term lv (All nam inp bod) dep) = (All nam (Normal lv inp dep) λx(Normal lv (bod (Var nam dep)) (+ dep 1)))
|
||||
(Normal.term lv (Lam nam bod) dep) = (Lam nam λx(Normal lv (bod (Var nam dep)) (+ 1 dep)))
|
||||
(Normal.term lv (App fun arg) dep) = (App (Normal lv fun dep) (Normal lv arg dep))
|
||||
(Normal.term lv (Ann val typ) dep) = (Ann (Normal lv val dep) (Normal lv typ dep))
|
||||
(Normal.term lv (Slf nam typ bod) dep) = (Slf nam typ λx(Normal lv (bod (Var nam dep)) (+ 1 dep)))
|
||||
(Normal.term lv (Ins val) dep) = (Ins (Normal lv val dep))
|
||||
(Normal.term lv (Ref nam val) dep) = (Ref nam (Normal lv val dep))
|
||||
(Normal.term lv (Let nam val bod) dep) = (Let nam (Normal lv val bod) λx(Normal lv (bod (Var nam dep)) (+ 1 dep)))
|
||||
(Normal.term lv (Hol nam ctx) dep) = (Hol nam ctx)
|
||||
(Normal.term lv Set dep) = Set
|
||||
(Normal.term lv U60 dep) = U60
|
||||
(Normal.term lv (Num val) dep) = (Num val)
|
||||
(Normal.term lv (Op2 opr fst snd) dep) = (Op2 opr (Normal.term lv fst dep) (Normal.term lv snd dep))
|
||||
(Normal.term lv (Mat nam x z s p) dep) = (Mat nam (Normal lv x dep) (Normal lv z dep) λk(Normal lv (s (Var (String.concat nam "-1") dep)) dep) λk(Normal lv (p (Var nam dep)) dep))
|
||||
(Normal.term lv (Txt val) dep) = (Txt val)
|
||||
(Normal.term lv (Var nam idx) dep) = (Var nam idx)
|
||||
(Normal.term lv (Src src val) dep) = (Src src (Normal lv val dep))
|
||||
(Normal fill lv term dep) = (Normal.term fill lv (Reduce fill lv term) dep)
|
||||
|
||||
(Normal.term fill lv (All nam inp bod) dep) = (All nam (Normal fill lv inp dep) λx(Normal fill lv (bod (Var nam dep)) (+ dep 1)))
|
||||
(Normal.term fill lv (Lam nam bod) dep) = (Lam nam λx(Normal fill lv (bod (Var nam dep)) (+ 1 dep)))
|
||||
(Normal.term fill lv (App fun arg) dep) = (App (Normal fill lv fun dep) (Normal fill lv arg dep))
|
||||
(Normal.term fill lv (Ann val typ) dep) = (Ann (Normal fill lv val dep) (Normal fill lv typ dep))
|
||||
(Normal.term fill lv (Slf nam typ bod) dep) = (Slf nam typ λx(Normal fill lv (bod (Var nam dep)) (+ 1 dep)))
|
||||
(Normal.term fill lv (Ins val) dep) = (Ins (Normal fill lv val dep))
|
||||
(Normal.term fill lv (Ref nam val) dep) = (Ref nam (Normal fill lv val dep))
|
||||
(Normal.term fill lv (Let nam val bod) dep) = (Let nam (Normal fill lv val bod) λx(Normal fill lv (bod (Var nam dep)) (+ 1 dep)))
|
||||
(Normal.term fill lv (Hol nam ctx) dep) = (Hol nam ctx)
|
||||
(Normal.term fill lv Set dep) = Set
|
||||
(Normal.term fill lv U60 dep) = U60
|
||||
(Normal.term fill lv (Num val) dep) = (Num val)
|
||||
(Normal.term fill lv (Op2 opr fst snd) dep) = (Op2 opr (Normal.term fill lv fst dep) (Normal.term fill lv snd dep))
|
||||
(Normal.term fill lv (Mat nam x z s p) dep) = (Mat nam (Normal fill lv x dep) (Normal fill lv z dep) λk(Normal fill lv (s (Var (String.concat nam "-1") dep)) dep) λk(Normal fill lv (p (Var nam dep)) dep))
|
||||
(Normal.term fill lv (Txt val) dep) = (Txt val)
|
||||
(Normal.term fill lv (Var nam idx) dep) = (Var nam idx)
|
||||
(Normal.term fill lv (Src src val) dep) = (Src src (Normal fill lv val dep))
|
||||
|
||||
// Checker
|
||||
// -------
|
||||
|
||||
// type Result A = (Done State A) | (Fail State String)
|
||||
// type Checker A = State -> (Result A)
|
||||
|
||||
(Result.match (Done state value) done fail) = (done state value)
|
||||
(Result.match (Fail state error) done fail) = (fail state error)
|
||||
|
||||
(State.get (State fill logs) got) = (got fill logs)
|
||||
(State.new) = (State Map.new [])
|
||||
|
||||
(Checker.bind a b) = λstate (Result.match (a state) λstateλvalue((b value) state) λstateλerror(Fail state error))
|
||||
(Checker.pure a) = λstate (Done state a)
|
||||
(Checker.fail e) = λstate (Fail state e)
|
||||
(Checker.run chk) = (chk State.new)
|
||||
(Checker.log msg) = λstate (Done (State.get state λfill λlogs (State fill (List.cons msg logs))) 1)
|
||||
(Checker.fill key val) = λstate (Done (State.get state λfill λlogs (State (Map.set key val fill) logs)) 1)
|
||||
(Checker.get_fill) = λstate (Done state (Pair.fst state))
|
||||
(Checker.save) = λstate (Done state state)
|
||||
(Checker.load state) = λerase (Done state 0)
|
||||
|
||||
// Equality
|
||||
// --------
|
||||
@ -192,49 +268,193 @@
|
||||
// Before changing it, READ `docs/equality.md`
|
||||
// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
// Check if two terms are identical. If not...
|
||||
// Checks if two term are equal
|
||||
(Equal a b dep) =
|
||||
(If (Identical a b dep) 1
|
||||
let a = (Reduce 2 a)
|
||||
let b = (Reduce 2 b)
|
||||
(If (Identical a b dep) 1
|
||||
(Similar a b dep)))
|
||||
(Checker.bind (Checker.save) λstate
|
||||
(Checker.bind (Identical a b dep) λequal
|
||||
(If equal
|
||||
(Checker.pure equal)
|
||||
(Checker.bind (Checker.load state) λx
|
||||
(Checker.bind (Checker.get_fill) λfill
|
||||
let a = (Reduce fill 2 a)
|
||||
let b = (Reduce fill 2 b)
|
||||
(Checker.bind (Identical a b dep) λequal
|
||||
(If equal
|
||||
(Checker.pure equal)
|
||||
(Similar a b dep))))))))
|
||||
|
||||
(Similar (All a.nam a.inp a.bod) (All b.nam b.inp b.bod) dep) = (& (Equal a.inp b.inp dep) (Equal (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep)))
|
||||
(Similar (Lam a.nam a.bod) (Lam b.nam b.bod) dep) = (Equal (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep))
|
||||
(Similar (App a.fun a.arg) (App b.fun b.arg) dep) = (& (Equal a.fun b.fun dep) (Equal a.arg b.arg dep))
|
||||
(Similar (Slf a.nam a.typ a.bod) (Slf b.nam b.typ b.bod) dep) = (Similar (Reduce 0 a.typ) (Reduce 0 b.typ) dep) // <- must call Similar, NOT Equal
|
||||
(Similar (Hol a.nam a.ctx) b dep) = (Debug dep ["Found: ?" a.nam " = " (Show (Normal 0 b dep) dep)] 1)
|
||||
(Similar a (Hol b.nam b.ctx) dep) = (Debug dep ["Found: ?" b.nam " = " (Show (Normal 0 a dep) dep)] 1)
|
||||
(Similar (Hol a.nam a.ctx) (Hol b.nam b.ctx) dep) = (Same a.nam b.nam)
|
||||
(Similar (Op2 a.opr a.fst a.snd) (Op2 b.opr b.fst b.snd) dep) = (& (Equal a.fst b.fst dep) (Equal a.snd b.snd dep))
|
||||
(Similar (Mat a.nam a.x a.z a.s a.p) (Mat b.nam b.x b.z b.s b.p) dep) = (& (Equal a.x b.x dep) (& (Equal a.z b.z dep) (& (Equal (a.s (Var (String.concat a.nam "-1") dep)) (b.s (Var (String.concat b.nam "-1") dep)) dep) (Equal (a.p (Var a.nam dep)) (b.p (Var b.nam dep)) dep))))
|
||||
(Similar a b dep) = 0
|
||||
// Checks if all components of a term are equal
|
||||
(Similar (All a.nam a.inp a.bod) (All b.nam b.inp b.bod) dep) =
|
||||
(Checker.bind (Equal a.inp b.inp dep) λe.inp
|
||||
(Checker.bind (Equal (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep)) λe.bod
|
||||
(Checker.pure (& e.inp e.bod))))
|
||||
(Similar (Lam a.nam a.bod) (Lam b.nam b.bod) dep) =
|
||||
(Equal (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep))
|
||||
(Similar (App a.fun a.arg) (App b.fun b.arg) dep) =
|
||||
(Checker.bind (Equal a.fun b.fun dep) λe.fun
|
||||
(Checker.bind (Equal a.arg b.arg dep) λe.arg
|
||||
(Checker.pure (& e.fun e.arg))))
|
||||
(Similar (Slf a.nam a.typ a.bod) (Slf b.nam b.typ b.bod) dep) =
|
||||
(Similar (Reduce Map.new 0 a.typ) (Reduce Map.new 0 b.typ) dep) // <- must call Similar, NOT Equal
|
||||
(Similar (Hol a.nam a.ctx) (Hol b.nam b.ctx) dep) =
|
||||
(Checker.pure (Same a.nam b.nam))
|
||||
(Similar (Op2 a.opr a.fst a.snd) (Op2 b.opr b.fst b.snd) dep) =
|
||||
(Checker.bind (Equal a.fst b.fst dep) λe.fst
|
||||
(Checker.bind (Equal a.snd b.snd dep) λe.snd
|
||||
(Checker.pure (Same e.fst e.snd))))
|
||||
(Similar (Mat a.nam a.x a.z a.s a.p) (Mat b.nam b.x b.z b.s b.p) dep) =
|
||||
(Checker.bind (Equal a.x b.x dep) λe.x
|
||||
(Checker.bind (Equal a.z b.z dep) λe.z
|
||||
(Checker.bind (Equal (a.s (Var (String.concat a.nam "-1") dep)) (b.s (Var (String.concat b.nam "-1") dep)) dep) λe.s
|
||||
(Checker.bind (Equal (a.p (Var a.nam dep)) (b.p (Var b.nam dep)) dep) λe.p
|
||||
(& e.x (& e.z (& e.s e.p)))))))
|
||||
(Similar a b dep) =
|
||||
(Checker.pure 0)
|
||||
|
||||
(Identical (All a.nam a.inp a.bod) (All b.nam b.inp b.bod) dep) = (& (Identical a.inp b.inp dep) (Identical (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep)))
|
||||
(Identical (Lam a.nam a.bod) (Lam b.nam b.bod) dep) = (Identical (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep))
|
||||
(Identical (App a.fun a.arg) (App b.fun b.arg) dep) = (& (Identical a.fun b.fun dep) (Identical a.arg b.arg dep))
|
||||
(Identical (Slf a.nam a.typ a.bod) (Slf b.nam b.typ b.bod) dep) = (Identical a.typ b.typ dep)
|
||||
(Identical (Ins a.val) b dep) = (Identical a.val b dep)
|
||||
(Identical a (Ins b.val) dep) = (Identical a b.val dep)
|
||||
(Identical (Ref a.nam a.val) (Ref b.nam b.val) dep) = (Same a.nam b.nam)
|
||||
(Identical (Let a.nam a.val a.bod) b dep) = (Identical (a.bod a.val) b dep)
|
||||
(Identical a (Let b.nam b.val b.bod) dep) = (Identical a (b.bod b.val) dep)
|
||||
(Identical Set Set dep) = 1
|
||||
(Identical (Var a.nam a.idx) (Var b.nam b.idx) dep) = (== a.idx b.idx)
|
||||
(Identical (Ann a.val a.typ) b dep) = (Identical a.val b dep)
|
||||
(Identical a (Ann b.val b.typ) dep) = (Identical a b.val dep)
|
||||
(Identical (Hol a.nam a.ctx) b dep) = (Debug dep ["Found: ?" a.nam " = " (Show (Normal 0 b dep) dep)] 1)
|
||||
(Identical a (Hol b.nam b.ctx) dep) = (Debug dep ["Found: ?" b.nam " = " (Show (Normal 0 a dep) dep)] 1)
|
||||
(Identical (Hol a.nam a.ctx) (Hol b.nam b.ctx) dep) = (Same a.nam b.nam)
|
||||
(Identical U60 U60 dep) = 1
|
||||
(Identical (Num a.val) (Num b.val) dep) = (== a.val b.val)
|
||||
(Identical (Op2 a.opr a.fst a.snd) (Op2 b.opr b.fst b.snd) dep) = (& (Identical a.fst b.fst dep) (Identical a.snd b.snd dep))
|
||||
(Identical (Mat a.nam a.x a.z a.s a.p) (Mat b.nam b.x b.z b.s b.p) dep) = (& (Identical a.x b.x dep) (& (Identical a.z b.z dep) (& (Identical (a.s (Var (String.concat a.nam "-1") dep)) (b.s (Var (String.concat b.nam "-1") dep)) dep) (Identical (a.p (Var a.nam dep)) (b.p (Var b.nam dep)) dep))))
|
||||
(Identical (Txt a.txt) (Txt b.txt) dep) = (Same a.txt b.txt)
|
||||
(Identical (Src a.src a.val) b dep) = (Identical a.val b dep)
|
||||
(Identical a (Src b.src b.val) dep) = (Identical a b.val dep)
|
||||
(Identical a b dep) = 0
|
||||
// Checks if two terms are structurally identical
|
||||
(Identical a b dep) =
|
||||
//(Debug dep ["Identical?" NewLine "- " (Show a dep) NewLine "- " (Show b dep)]
|
||||
(Unify.try b a dep
|
||||
(Unify.try a b dep
|
||||
(Identical.go a b dep)))
|
||||
|
||||
(Identical.go (All a.nam a.inp a.bod) (All b.nam b.inp b.bod) dep) =
|
||||
(Checker.bind (Identical a.inp b.inp dep) λi.inp
|
||||
(Checker.bind (Identical (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep)) λi.bod
|
||||
(Checker.pure (& i.inp i.bod))))
|
||||
(Identical.go (Lam a.nam a.bod) (Lam b.nam b.bod) dep) =
|
||||
(Identical (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep))
|
||||
(Identical.go (App a.fun a.arg) (App b.fun b.arg) dep) =
|
||||
(Checker.bind (Identical a.fun b.fun dep) λi.fun
|
||||
(Checker.bind (Identical a.arg b.arg dep) λi.arg
|
||||
(Checker.pure (& i.fun i.arg))))
|
||||
(Identical.go (Slf a.nam a.typ a.bod) (Slf b.nam b.typ b.bod) dep) =
|
||||
(Identical a.typ b.typ dep)
|
||||
(Identical.go (Ins a.val) b dep) =
|
||||
(Identical a.val b dep)
|
||||
(Identical.go a (Ins b.val) dep) =
|
||||
(Identical a b.val dep)
|
||||
(Identical.go (Let a.nam a.val a.bod) b dep) =
|
||||
(Identical (a.bod a.val) b dep)
|
||||
(Identical.go a (Let b.nam b.val b.bod) dep) =
|
||||
(Identical a (b.bod b.val) dep)
|
||||
(Identical.go Set Set dep) =
|
||||
(Checker.pure 1)
|
||||
(Identical.go (Ann a.val a.typ) b dep) =
|
||||
(Identical a.val b dep)
|
||||
(Identical.go a (Ann b.val b.typ) dep) =
|
||||
(Identical a b.val dep)
|
||||
(Identical.go (Hol a.nam a.ctx) (Hol b.nam b.ctx) dep) =
|
||||
(Checker.pure (Same a.nam b.nam))
|
||||
(Identical.go U60 U60 dep) =
|
||||
(Checker.pure 1)
|
||||
(Identical.go (Num a.val) (Num b.val) dep) =
|
||||
(Checker.pure (== a.val b.val))
|
||||
(Identical.go (Op2 a.opr a.fst a.snd) (Op2 b.opr b.fst b.snd) dep) =
|
||||
(Checker.bind (Identical a.fst b.fst dep) λi.fst
|
||||
(Checker.bind (Identical a.snd b.snd dep) λi.snd
|
||||
(Checker.pure (& i.fst i.snd))))
|
||||
(Identical.go (Mat a.nam a.x a.z a.s a.p) (Mat b.nam b.x b.z b.s b.p) dep) =
|
||||
(Checker.bind (Identical a.x b.x dep) λi.x
|
||||
(Checker.bind (Identical a.z b.z dep) λi.z
|
||||
(Checker.bind (Identical (a.s (Var (String.concat a.nam "-1") dep)) (b.s (Var (String.concat b.nam "-1") dep)) dep) λi.s
|
||||
(Checker.bind (Identical (a.p (Var a.nam dep)) (b.p (Var b.nam dep)) dep) λi.p
|
||||
(& i.x (& i.z (& i.s i.p)))))))
|
||||
(Identical.go (Txt a.txt) (Txt b.txt) dep) =
|
||||
(Checker.pure (Same a.txt b.txt))
|
||||
(Identical.go (Src a.src a.val) b dep) =
|
||||
(Identical a.val b dep)
|
||||
(Identical.go a (Src b.src b.val) dep) =
|
||||
(Identical a b.val dep)
|
||||
(Identical.go (Ref a.nam a.val) (Ref b.nam b.val) dep) =
|
||||
(Checker.pure (Same a.nam b.nam))
|
||||
(Identical.go (Var a.nam a.idx) (Var b.nam b.idx) dep) =
|
||||
(Checker.pure (== a.idx b.idx))
|
||||
(Identical.go a b dep) =
|
||||
(Checker.pure 0)
|
||||
|
||||
// From smalltt:
|
||||
// 1. spine consists of distinct bound variables
|
||||
// 2. every free variable of rhs occurs in spine
|
||||
// 3. ?α does not occur in rhs
|
||||
|
||||
// Unify.try : Term -> Term -> U60 -> (Checker U60) -> (Checker U60)
|
||||
(Unify.try a b dep else) =
|
||||
(Maybe.match (Unify.pat a b dep Map.new)
|
||||
λkv(Pair.get kv λkλv(Debug dep ["- unify: ?" k " = " (Show v dep)] (Checker.fill k v)))
|
||||
(else))
|
||||
|
||||
// Unify.pat : Term -> Term -> U60 -> (Map U60 Term) -> (Maybe (Pair nam Term))
|
||||
(Unify.pat (App fun (Var nam idx)) b dep ctx) =
|
||||
(Maybe.bind (Map.put idx $x ctx) λctx
|
||||
(Maybe.bind (Unify.pat fun b dep ctx) λkv
|
||||
(Pair.get kv λkλv(Maybe.pure (Pair k (Lam nam λ$x(v)))))))
|
||||
(Unify.pat (Hol nam ctx) b dep ctx) =
|
||||
(Maybe.bind (Unify.sub b dep nam ctx) λneo
|
||||
(Maybe.pure (Pair nam neo)))
|
||||
(Unify.pat (App fun (Ann val _)) b dep ctx) = (Unify.pat (App fun val) b dep ctx)
|
||||
(Unify.pat (App fun (Ins val)) b dep ctx) = (Unify.pat (App fun val) b dep ctx)
|
||||
(Unify.pat (App fun (Src _ val)) b dep ctx) = (Unify.pat (App fun val) b dep ctx)
|
||||
(Unify.pat (Ann val typ) b dep ctx) = (Unify.pat val b dep ctx)
|
||||
(Unify.pat (Ins val) b dep ctx) = (Unify.pat val b dep ctx)
|
||||
(Unify.pat (Src src val) b dep ctx) = (Unify.pat val b dep ctx)
|
||||
(Unify.pat other b dep ctx) = None
|
||||
|
||||
// Unify.sub : Term -> U60 -> String -> (Map U60 Term) -> (Maybe Term)
|
||||
(Unify.sub (All nam inp bod) dep hol ctx) =
|
||||
(Maybe.bind (Unify.sub inp dep hol ctx) λinp
|
||||
(Maybe.bind (Unify.sub (bod (Var nam dep)) (+ dep 1) hol ctx) λbod
|
||||
(Maybe.pure (All nam inp λ_(bod)))))
|
||||
(Unify.sub (Lam nam bod) dep hol ctx) =
|
||||
(Maybe.bind (Unify.sub (bod (Var nam dep)) (+ 1 dep) hol ctx) λbod
|
||||
(Maybe.pure (Lam nam λ_(bod))))
|
||||
(Unify.sub (App fun arg) dep hol ctx) =
|
||||
(Maybe.bind (Unify.sub fun dep hol ctx) λfun
|
||||
(Maybe.bind (Unify.sub arg dep hol ctx) λarg
|
||||
(Maybe.pure (App fun arg))))
|
||||
(Unify.sub (Ann val typ) dep hol ctx) =
|
||||
(Maybe.bind (Unify.sub val dep hol ctx) λval
|
||||
(Maybe.bind (Unify.sub typ dep hol ctx) λtyp
|
||||
(Maybe.pure (Ann val typ))))
|
||||
(Unify.sub (Slf nam typ bod) dep hol ctx) =
|
||||
(Unify.sub typ dep hol ctx)
|
||||
(Unify.sub (Ins val) dep hol ctx) =
|
||||
(Maybe.bind (Unify.sub val dep hol ctx) λval
|
||||
(Maybe.pure (Ins val)))
|
||||
(Unify.sub (Ref nam val) dep hol ctx) =
|
||||
(Maybe.pure (Ref nam val))
|
||||
(Unify.sub (Let nam val bod) dep hol ctx) =
|
||||
(Maybe.bind (Unify.sub val dep hol ctx) λval
|
||||
(Maybe.bind (Unify.sub (bod (Var nam dep)) (+ 1 dep) hol ctx) λbod
|
||||
(Maybe.pure (Let nam val λ_(bod)))))
|
||||
(Unify.sub (Hol nam ctx) dep hol ctx) =
|
||||
(If (Same nam hol) None (Maybe.pure (Hol nam ctx)))
|
||||
(Unify.sub Set dep hol ctx) =
|
||||
(Maybe.pure Set)
|
||||
(Unify.sub U60 dep hol ctx) =
|
||||
(Maybe.pure U60)
|
||||
(Unify.sub (Num val) dep hol ctx) =
|
||||
(Maybe.pure (Num val))
|
||||
(Unify.sub (Op2 opr fst snd) dep hol ctx) =
|
||||
(Maybe.bind (Unify.sub fst dep hol ctx) λfst
|
||||
(Maybe.bind (Unify.sub snd dep hol ctx) λsnd
|
||||
(Maybe.pure (Op2 opr fst snd))))
|
||||
(Unify.sub (Mat nam x z s p) dep hol ctx) =
|
||||
(Maybe.bind (Unify.sub x dep hol ctx) λx
|
||||
(Maybe.bind (Unify.sub z dep hol ctx) λz
|
||||
(Maybe.bind (Unify.sub (s (Var (String.concat nam "-1") dep)) dep hol ctx) λs
|
||||
(Maybe.bind (Unify.sub (p (Var nam dep)) dep hol ctx) λp
|
||||
(Maybe.pure (Mat nam x z λ_(s) λ_(p)))))))
|
||||
(Unify.sub (Txt val) dep hol ctx) =
|
||||
(Maybe.pure (Txt val))
|
||||
(Unify.sub (Var nam idx) dep hol ctx) =
|
||||
(Maybe.bind (Map.get idx ctx) λval
|
||||
(Maybe.pure val))
|
||||
(Unify.sub (Src src val) dep hol ctx) =
|
||||
(Maybe.bind (Unify.sub val dep hol ctx) λval
|
||||
(Maybe.pure (Src src val)))
|
||||
(Unify.sub term dep hol ctx) =
|
||||
(HVM.log (UNEXPECTED (Show term dep)) None)
|
||||
|
||||
// Type-Checking
|
||||
// -------------
|
||||
@ -249,57 +469,61 @@
|
||||
(Infer term dep) = (Infer.match term dep)
|
||||
|
||||
(Infer.match (All nam inp bod) dep) =
|
||||
(Maybe.bind (Check 0 inp Set dep) λinp_typ
|
||||
(Maybe.bind (Check 0 (bod (Ann (Var nam dep) inp)) Set (+ 1 dep)) λbod_typ
|
||||
(Maybe.pure Set)))
|
||||
(Infer.match (Lam nam bod) dep) =
|
||||
(Debug dep ["NON_FUNCTION_LAMBDA" NewLine "- detected: " (Show (Lam nam bod) dep)] (None))
|
||||
(Checker.bind (Check 0 inp Set dep) λinp_typ
|
||||
(Checker.bind (Check 0 (bod (Ann (Var nam dep) inp)) Set (+ 1 dep)) λbod_typ
|
||||
(Checker.pure Set)))
|
||||
(Infer.match (App fun arg) dep) =
|
||||
(Maybe.bind (Infer fun dep) λfun_typ
|
||||
((IfAll (Reduce 2 fun_typ)
|
||||
(Checker.bind (Infer fun dep) λfun_typ
|
||||
(Checker.bind (Checker.get_fill) λfill
|
||||
((IfAll (Reduce fill 2 fun_typ)
|
||||
λfun_nam λfun_typ.inp λfun_typ.bod λfun λarg
|
||||
(Maybe.bind (Check 0 arg fun_typ.inp dep) λval_typ
|
||||
(Maybe.pure (fun_typ.bod arg)))
|
||||
(Checker.bind (Check 0 arg fun_typ.inp dep) λvty
|
||||
(Checker.pure (fun_typ.bod arg)))
|
||||
λfun λarg
|
||||
(Debug dep ["Error: NonFunApp " (Show (App fun arg) dep)] None))
|
||||
fun arg))
|
||||
(Checker.fail (NonFunApp (App fun arg) dep)))
|
||||
fun arg)))
|
||||
(Infer.match (Ann val typ) dep) =
|
||||
(Maybe.pure typ)
|
||||
(Checker.pure typ)
|
||||
(Infer.match (Slf nam typ bod) dep) =
|
||||
(Maybe.bind (Check 0 (bod (Ann (Var nam dep) typ)) Set (+ dep 1)) λslf
|
||||
(Maybe.pure Set))
|
||||
(Checker.bind (Check 0 (bod (Ann (Var nam dep) typ)) Set (+ dep 1)) λslf
|
||||
(Checker.pure Set))
|
||||
(Infer.match (Ins val) dep) =
|
||||
(Maybe.bind (Infer val dep) λval_typ
|
||||
((IfSlf (Reduce 2 val_typ)
|
||||
λval_typ.nam λval_typ.typ λval_typ.bod λval (Maybe.pure (val_typ.bod (Ins val)))
|
||||
λval (Debug dep ["Error: NonSlfIns " (Show (Ins val) dep)] None))
|
||||
val))
|
||||
(Checker.bind (Infer val dep) λvty
|
||||
(Checker.bind (Checker.get_fill) λfill
|
||||
((IfSlf (Reduce fill 2 vty)
|
||||
λvty.nam λvty.typ λvty.bod λval
|
||||
(Checker.pure (vty.bod (Ins val)))
|
||||
λval
|
||||
(Checker.fail (NonSlfIns (Ins val))))
|
||||
val)))
|
||||
(Infer.match (Ref nam val) dep) =
|
||||
(Infer val dep)
|
||||
(Infer.match (Let nam val bod) dep) =
|
||||
(Debug dep ["Error: NonAnnLet " (Show (Let nam val bod) dep)] (None))
|
||||
(Infer.match Set dep) =
|
||||
(Maybe.pure Set)
|
||||
(Checker.pure Set)
|
||||
(Infer.match U60 dep) =
|
||||
(Maybe.pure Set)
|
||||
(Checker.pure Set)
|
||||
(Infer.match (Num num) dep) =
|
||||
(Maybe.pure U60)
|
||||
(Checker.pure U60)
|
||||
(Infer.match (Txt txt) dep) =
|
||||
(Maybe.pure Book.String)
|
||||
(Checker.pure Book.String)
|
||||
(Infer.match (Op2 opr fst snd) dep) =
|
||||
(Maybe.bind (Check 0 fst U60 dep) λfst
|
||||
(Maybe.bind (Check 0 snd U60 dep) λsnd
|
||||
(Maybe.pure U60)))
|
||||
(Checker.bind (Check 0 fst U60 dep) λfst
|
||||
(Checker.bind (Check 0 snd U60 dep) λsnd
|
||||
(Checker.pure U60)))
|
||||
(Infer.match (Mat nam x z s p) dep) =
|
||||
(Maybe.bind (Check 0 x U60 dep) λx_typ
|
||||
(Maybe.bind (Check 0 (p (Ann (Var nam dep) U60)) Set dep) λp_typ
|
||||
(Maybe.bind (Check 0 z (p (Num 0)) dep) λz_typ
|
||||
(Maybe.bind (Check 0 (s (Ann (Var (String.concat nam "-1") dep) U60)) (p (Op2 ADD (Num 1) (Var (String.concat nam "-1") dep))) (+ dep 1)) λs_typ
|
||||
(Maybe.pure (p x))))))
|
||||
(Checker.bind (Check 0 x U60 dep) λx_typ
|
||||
(Checker.bind (Check 0 (p (Ann (Var nam dep) U60)) Set dep) λp_typ
|
||||
(Checker.bind (Check 0 z (p (Num 0)) dep) λz_typ
|
||||
(Checker.bind (Check 0 (s (Ann (Var (String.concat nam "-1") dep) U60)) (p (Op2 ADD (Num 1) (Var (String.concat nam "-1") dep))) (+ dep 1)) λs_typ
|
||||
(Checker.pure (p x))))))
|
||||
(Infer.match (Lam nam bod) dep) =
|
||||
(Checker.fail (CantInfer (Lam nam bod) dep))
|
||||
(Infer.match (Let nam val bod) dep) =
|
||||
(Checker.fail (CantInfer (Let nam val bod) dep))
|
||||
(Infer.match (Hol nam ctx) dep) =
|
||||
(Debug dep ["Error: NonAnnHol " (Show (Hol nam ctx) dep)] None)
|
||||
(Checker.fail (CantInfer (Hol nam ctx) dep))
|
||||
(Infer.match (Var nam idx) dep) =
|
||||
(Debug dep ["Error: NonAnnVar " (Show (Var nam idx) dep)] None)
|
||||
(Checker.fail (CantInfer (Var nam idx) dep))
|
||||
(Infer.match (Src src val) dep) =
|
||||
(Infer.match val dep)
|
||||
|
||||
@ -307,7 +531,8 @@
|
||||
(Check src term type dep) = (Check.match src term type dep)
|
||||
|
||||
(Check.match src (Lam term.nam term.bod) type dep) =
|
||||
((IfAll (Reduce 2 type)
|
||||
(Checker.bind (Checker.get_fill) λfill
|
||||
((IfAll (Reduce fill 2 type)
|
||||
λtype.nam λtype.inp λtype.bod λterm.bod
|
||||
let ann = (Ann (Var term.nam dep) type.inp)
|
||||
let term = (term.bod ann)
|
||||
@ -315,19 +540,23 @@
|
||||
(Check 0 term type (+ dep 1))
|
||||
λterm.bod
|
||||
(Infer (Lam term.nam term.bod) dep))
|
||||
term.bod)
|
||||
term.bod))
|
||||
(Check.match src (Ins term.val) type dep) =
|
||||
((IfSlf (Reduce 2 type)
|
||||
λtype.nam λtype.typ λtype.bod λterm.val (Check 0 term.val (type.bod (Ins term.val)) dep)
|
||||
λterm.val (Infer (Ins term.val) dep))
|
||||
term.val)
|
||||
(Checker.bind (Checker.get_fill) λfill
|
||||
((IfSlf (Reduce fill 2 type)
|
||||
λtype.nam λtype.typ λtype.bod λterm.val
|
||||
(Check 0 term.val (type.bod (Ins term.val)) dep)
|
||||
λterm.val
|
||||
(Infer (Ins term.val) dep))
|
||||
term.val))
|
||||
(Check.match src (Let term.nam term.val term.bod) type dep) =
|
||||
(Check 0 (term.bod term.val) type (+ 1 dep))
|
||||
(Check.match src (Hol term.nam term.ctx) type dep) =
|
||||
(Debug dep [(String.color BRIGHT) "HOLE: ?" term.nam " :: " (Show (Normal 0 type dep) dep) (String.color RESET) (Context.show term.ctx dep)]
|
||||
(Maybe.pure 0))
|
||||
(Checker.bind (Checker.log (FoundHole term.nam type term.ctx dep)) λx
|
||||
(Checker.pure 0))
|
||||
(Check.match src (Ref term.nam (Ann term.val term.typ)) type dep) = // better printing
|
||||
(Check.report src (Equal type term.typ dep) term.typ type (Ref term.nam term.val) dep)
|
||||
(Checker.bind (Equal type term.typ dep) λequal
|
||||
(Check.report src equal term.typ type (Ref term.nam term.val) dep))
|
||||
(Check.match src (Src term.src term.val) type dep) =
|
||||
(Check term.src term.val type dep)
|
||||
//(Check.match src (Ref term.nam term.val) type dep) =
|
||||
@ -336,21 +565,14 @@
|
||||
(Check.verify src term type dep)
|
||||
|
||||
(Check.verify src term type dep) =
|
||||
(Maybe.bind (Infer term dep) λinfer
|
||||
(Check.report src (Equal type infer dep) infer type term dep))
|
||||
(Checker.bind (Infer term dep) λinfer
|
||||
(Checker.bind (Equal type infer dep) λequal
|
||||
(Check.report src equal infer type term dep)))
|
||||
|
||||
(Check.report src 0 detected expected value dep) =
|
||||
let det = (Show (Normal 0 detected dep) dep)
|
||||
let exp = (Show (Normal 0 expected dep) dep)
|
||||
let val = (Show (Normal 0 value dep) dep)
|
||||
(Debug dep [(String.color BRIGHT) "TYPE_MISMATCH" NewLine
|
||||
"- expected: " (String.color RESET) (String.color GREEN) exp NewLine (String.color RESET) (String.color BRIGHT)
|
||||
"- detected: " (String.color RESET) (String.color RED) det NewLine (String.color RESET) (String.color BRIGHT)
|
||||
"- bad_term: " (String.color RESET) (String.color DIM) val NewLine (String.color RESET)
|
||||
"##LOC{" (U60.show src) "}LOC##" NewLine
|
||||
] None)
|
||||
(Check.report src n inferred expected value dep) =
|
||||
(Maybe.pure 0)
|
||||
(Checker.fail (TypeMismatch src detected expected value dep))
|
||||
(Check.report src n detected expected value dep) =
|
||||
(Checker.pure 0)
|
||||
|
||||
// Syntax
|
||||
// ------
|
||||
@ -372,6 +594,7 @@
|
||||
(Show (Hol nam ctx) dep) = (String.join ["?" nam])
|
||||
(Show (Var nam idx) dep) = (String.join [nam])
|
||||
(Show (Src src val) dep) = (Show val dep)
|
||||
//(Show (Src src val) dep) = (String.join ["!" (Show val dep)])
|
||||
//(Show (Var nam idx) dep) = (String.join [nam "'" (U60.show idx)])
|
||||
|
||||
(Show.many List.nil dep) = ""
|
||||
@ -392,13 +615,36 @@
|
||||
(Op2.show MUL) = "*"
|
||||
(Op2.show DIV) = "/"
|
||||
|
||||
(Context.show List.nil dep) = ""
|
||||
(Context.show (List.cons x xs) dep) = (String.join [NewLine "- " (Context.show.ann x dep) (Context.show xs dep)])
|
||||
(Context.show fill List.nil dep) = ""
|
||||
(Context.show fill (List.cons x xs) dep) = (String.join [NewLine "- " (Context.show.ann fill x dep) (Context.show fill xs dep)])
|
||||
|
||||
(Context.show.ann (Ann val typ) dep) = (String.join ["{" (Show (Normal 0 val dep) dep) ": " (Show (Normal 0 typ dep) dep) "}"])
|
||||
(Context.show.ann term dep) = (Show (Normal 0 term dep) dep)
|
||||
(Context.show.ann fill (Ann val typ) dep) = (String.join ["{" (Show (Normal fill 0 val dep) dep) ": " (Show (Normal fill 0 typ dep) dep) "}"])
|
||||
(Context.show.ann fill term dep) = (Show (Normal fill 0 term dep) dep)
|
||||
//(Context.show.ann val dep) = (String.join ["{" (Show (Normal 0 val dep) dep) ": " (Show (Normal 0 (Infer val dep) dep) dep) "}"])
|
||||
|
||||
(Message.show fill (FoundHole name type ctx dep)) =
|
||||
let bold = (String.color BRIGHT)
|
||||
let reset = (String.color RESET)
|
||||
let type = (Show (Normal fill 0 type dep) dep)
|
||||
let ctx = (Context.show fill ctx dep)
|
||||
(String.join [bold "HOLE: ?" name " :: " type ctx reset])
|
||||
(Message.show fill (NonFunApp term dep)) =
|
||||
let term = (Show term dep)
|
||||
(String.join ["NON_FUNCTION_APPLICATION:" term])
|
||||
(Message.show fill (CantInfer term dep)) =
|
||||
let term = (Show term dep)
|
||||
(String.join ["CANT_INFER:" term])
|
||||
(Message.show fill (TypeMismatch src detected expected value dep)) =
|
||||
let det = (Show (Normal fill 0 detected dep) dep)
|
||||
let exp = (Show (Normal fill 0 expected dep) dep)
|
||||
let val = (Show (Normal fill 0 value dep) dep)
|
||||
(String.join [(String.color BRIGHT) "TYPE_MISMATCH" NewLine
|
||||
"- expected: " (String.color RESET) (String.color GREEN) exp NewLine (String.color RESET) (String.color BRIGHT)
|
||||
"- detected: " (String.color RESET) (String.color RED) det NewLine (String.color RESET) (String.color BRIGHT)
|
||||
"- bad_term: " (String.color RESET) (String.color DIM) val NewLine (String.color RESET)
|
||||
"##LOC{" (U60.show src) "}LOC##" NewLine
|
||||
])
|
||||
|
||||
// Compilation
|
||||
// -----------
|
||||
|
||||
@ -461,35 +707,44 @@ Compile.primitives = [
|
||||
// API
|
||||
// ---
|
||||
|
||||
(Normalizer (Ref nam val)) = (Normalizer val)
|
||||
(Normalizer (Ann val typ)) = (Normalizer val)
|
||||
(Normalizer (Src src val)) = (Normalizer val)
|
||||
(Normalizer val) = (Compile val)
|
||||
//(Normalizer val) = (Str.view (Compile val))
|
||||
(API.normal (Ref nam val)) = (API.normal val)
|
||||
(API.normal (Ann val typ)) = (API.normal val)
|
||||
(API.normal (Src src val)) = (API.normal val)
|
||||
(API.normal val) = (Compile val)
|
||||
//(API.normal val) = (Str.view (Compile val))
|
||||
|
||||
(Checker name (Ref nam val)) = (Checker name val)
|
||||
(Checker name (Src src (Ann val typ))) = (Checker.report name (Check src val typ 0))
|
||||
(Checker name (Src src val)) = (Checker name val)
|
||||
(Checker name (Ann val typ)) = (Checker.report name (Check 0 val typ 0))
|
||||
(Checker name val) = (Checker.report name (Infer val 0))
|
||||
// Checker
|
||||
|
||||
(Checker.report name (Some x)) = 1
|
||||
(Checker.report name None) = 0
|
||||
//(Checker.report name (Some x)) = (HVM.print (String.join [(String.color GREEN) "- " name ": ✔" (String.color RESET)]) 1)
|
||||
//(Checker.report name None) = (HVM.print (String.join [(String.color RED) "- " name ": ✘" (String.color RESET)]) 0)
|
||||
(API.check name (Ref nam val)) = (API.check name val)
|
||||
(API.check name (Src src (Ann val typ))) = (API.check.report name (Checker.run (Check src val typ 0)))
|
||||
(API.check name (Src src val)) = (API.check name val)
|
||||
(API.check name (Ann val typ)) = (API.check.report name (Checker.run (Check 0 val typ 0)))
|
||||
(API.check name val) = (API.check.report name (Checker.run (Infer val 0)))
|
||||
|
||||
(Checker.many.go (List.cons (Pair name def) defs)) = (& (Checker name def) (Checker.many.go defs))
|
||||
(Checker.many.go List.nil) = 1
|
||||
(API.check.many list) = (If (API.check.many.go list) ALL_TERMS_CHECK ERRORS_FOUND)
|
||||
|
||||
(Checker.many list) = (If (Checker.many.go list) ALL_TERMS_CHECK ERRORS_FOUND)
|
||||
(API.check.many.go (List.cons (Pair name def) defs)) = (& (API.check name def) (API.check.many.go defs))
|
||||
(API.check.many.go List.nil) = 1
|
||||
|
||||
Book.Main = (Ref "Main" (Ann (Src 1099526307859 (Txt "foo")) (Src 1099518967819 (U60))))
|
||||
Book.List = (Ref "List" (Ann (Src 3298559000766 (Lam "T" λ_T (Src 3298565292222 (Slf "self" (Src 3298573680685 (App (Src 3298574729258 (Book.List)) (Src 3298579972140 _T))) λ_self (Src 3298586263742 (All "P" (Src 3298593603659 (All "xs" (Src 3298601992264 (App (Src 3298603040837 (Book.List)) (Src 3298608283719 _T))) λ_xs (Src 3298612478027 (Set)))) λ_P (Src 3298617721022 (All "cons" (Src 3298628206741 (All "head" (Src 3298638692452 _T) λ_head (Src 3298641838229 (All "tail" (Src 3298652323960 (App (Src 3298653372533 (Book.List)) (Src 3298658615415 _T))) λ_tail (Src 3298662809749 (App (Src 3298663858300 _P) (Src 3298665955476 (App (App (App (Src 3298667004039 (Book.List.cons)) (Src 3298677489801 _T)) (Src 3298679586958 _head)) (Src 3298684829843 _tail))))))))) λ_cons (Src 3298695315646 (All "nil" (Src 3298704752818 (App (Src 3298705801380 _P) (Src 3298707898545 (App (Src 3298708947118 (Book.List.nil)) (Src 3298718384304 _T))))) λ_nil (Src 3298725724350 (App (Src 3298726772920 _P) (Src 3298728870077 _self))))))))))))) (Src 3298542223380 (All "T" (Src 3298549563407 (Set)) λ_T (Src 3298554806292 (Set))))))
|
||||
Book.String = (Ref "String" (Ann (Src 2199036887064 (App (Src 2199037935634 (Book.List)) (Src 2199043178519 (Book.Char)))) (Src 2199032692746 (Set))))
|
||||
Book.List.nil = (Ref "List.nil" (Ann (Src 5497593790527 (Lam "T" λ_T (Src 5497600081983 (Ins (Src 5497601130559 (Lam "P" λ_P (Src 5497605324863 (Lam "cons" λ_cons (Src 5497612664895 (Lam "nil" λ_nil (Src 5497621053503 _nil))))))))))) (Src 5497569673247 (All "T" (Src 5497577013267 (Set)) λ_T (Src 5497582256159 (App (Src 5497583304732 (Book.List)) (Src 5497588547614 _T)))))))
|
||||
Book.Char = (Ref "Char" (Ann (Src 6597081301007 (U60)) (Src 6597077106696 (Set))))
|
||||
Book.String.cons = (Ref "String.cons" (Ann (Src 7696645357681 (Lam "head" λ_head (Src 7696652697713 (Lam "tail" λ_tail (Src 7696662134897 (Ins (Src 7696663183473 (Lam "P" λ_P (Src 7696667377777 (Lam "cons" λ_cons (Src 7696674717809 (Lam "nil" λ_nil (Src 7696683106417 (App (App (Src 7696684154982 _cons) (Src 7696689397867 _head)) (Src 7696694640752 _tail))))))))))))))) (Src 7696596074554 (All "head" (Src 7696606560284 (Book.Char)) λ_head (Src 7696614948922 (All "tail" (Src 7696625434672 (Book.String)) λ_tail (Src 7696635920442 (Book.String))))))))
|
||||
Book.List.cons = (Ref "List.cons" (Ann (Src 4398122008704 (Lam "T" λ_T (Src 4398126203008 (Lam "head" λ_head (Src 4398133543040 (Lam "tail" λ_tail (Src 4398142980224 (Ins (Src 4398144028800 (Lam "P" λ_P (Src 4398148223104 (Lam "cons" λ_cons (Src 4398155563136 (Lam "nil" λ_nil (Src 4398163951744 (App (App (Src 4398165000309 _cons) (Src 4398170243194 _head)) (Src 4398175486079 _tail))))))))))))))))) (Src 4398059094085 (All "T" (Src 4398066434068 (Set)) λ_T (Src 4398071676997 (All "head" (Src 4398082162723 _T) λ_head (Src 4398087405637 (All "tail" (Src 4398097891385 (App (Src 4398098939958 (Book.List)) (Src 4398104182840 _T))) λ_tail (Src 4398110474309 (App (Src 4398111522882 (Book.List)) (Src 4398116765764 _T)))))))))))
|
||||
Book.String.nil = (Ref "String.nil" (Ann (Src 8796116090925 (Ins (Src 8796117139501 (Lam "P" λ_P (Src 8796121333805 (Lam "cons" λ_cons (Src 8796128673837 (Lam "nil" λ_nil (Src 8796137062445 _nil))))))))) (Src 8796106653715 (Book.String))))
|
||||
// Reporter
|
||||
|
||||
Main = (Checker.many [(Pair "Char" Book.Char) (Pair "List" Book.List) (Pair "List.cons" Book.List.cons) (Pair "List.nil" Book.List.nil) (Pair "Main" Book.Main) (Pair "String" Book.String) (Pair "String.cons" Book.String.cons) (Pair "String.nil" Book.String.nil)])
|
||||
(API.log fill (List.cons msg msgs)) = (HVM.print (Message.show fill msg) (API.log fill msgs))
|
||||
(API.log fill List.nil) = λx x
|
||||
|
||||
(API.check.report name (Done (State fill logs) val)) = ((API.log fill logs) 1)
|
||||
(API.check.report name (Fail (State fill logs) err)) = ((API.log fill logs) ((API.log fill [err]) 0))
|
||||
|
||||
|
||||
Book.Main = (Ref "Main" (Ann (Src 1099665768614 (Lam "b" λ_b (Src 1099669962918 (App (App (App (Src 1099671011482 (Ins (Src 1099672060058 _b))) (Src 1099674157215 (Src 1099675205790 (Hol "A" [_b])))) (Src 1099679400098 (Hol "B" [_b]))) (Src 1099682545829 (Hol "C" [_b])))))) (Src 1099644797072 (All "b" (Src 1099652137098 (Book.Bool)) λ_b (Src 1099658428560 (Book.Bool))))))
|
||||
Book.String = (Ref "String" (Ann (Src 5497571770392 (App (Src 5497572818962 (Book.List)) (Src 5497578061847 (Book.Char)))) (Src 5497567576074 (Set))))
|
||||
Book.List.nil = (Ref "List.nil" (Ann (Src 8796128673855 (Lam "T" λ_T (Src 8796134965311 (Ins (Src 8796136013887 (Lam "P" λ_P (Src 8796140208191 (Lam "cons" λ_cons (Src 8796147548223 (Lam "nil" λ_nil (Src 8796155936831 _nil))))))))))) (Src 8796104556575 (All "T" (Src 8796111896595 (Set)) λ_T (Src 8796117139487 (App (Src 8796118188060 (Book.List)) (Src 8796123430942 _T)))))))
|
||||
Book.List = (Ref "List" (Ann (Src 6597093884094 (Lam "T" λ_T (Src 6597100175550 (Slf "self" (Src 6597108564013 (App (Src 6597109612586 (Book.List)) (Src 6597114855468 _T))) λ_self (Src 6597121147070 (All "P" (Src 6597128486987 (All "xs" (Src 6597136875592 (App (Src 6597137924165 (Book.List)) (Src 6597143167047 _T))) λ_xs (Src 6597147361355 (Set)))) λ_P (Src 6597152604350 (All "cons" (Src 6597163090069 (All "head" (Src 6597173575780 _T) λ_head (Src 6597176721557 (All "tail" (Src 6597187207288 (App (Src 6597188255861 (Book.List)) (Src 6597193498743 _T))) λ_tail (Src 6597197693077 (App (Src 6597198741628 _P) (Src 6597200838804 (App (App (App (Src 6597201887367 (Book.List.cons)) (Src 6597212373129 _T)) (Src 6597214470286 _head)) (Src 6597219713171 _tail))))))))) λ_cons (Src 6597230198974 (All "nil" (Src 6597239636146 (App (Src 6597240684708 _P) (Src 6597242781873 (App (Src 6597243830446 (Book.List.nil)) (Src 6597253267632 _T))))) λ_nil (Src 6597260607678 (App (Src 6597261656248 _P) (Src 6597263753405 _self))))))))))))) (Src 6597077106708 (All "T" (Src 6597084446735 (Set)) λ_T (Src 6597089689620 (Set))))))
|
||||
Book.Bool.false = (Ref "Bool.false" (Ann (Src 4398067482658 (Ins (Src 4398068531234 (Lam "P" λ_P (Src 4398072725538 (Lam "t" λ_t (Src 4398076919842 (Lam "f" λ_f (Src 4398081114146 _f))))))))) (Src 4398060142609 (Book.Bool))))
|
||||
Book.List.cons = (Ref "List.cons" (Ann (Src 7696656892032 (Lam "T" λ_T (Src 7696661086336 (Lam "head" λ_head (Src 7696668426368 (Lam "tail" λ_tail (Src 7696677863552 (Ins (Src 7696678912128 (Lam "P" λ_P (Src 7696683106432 (Lam "cons" λ_cons (Src 7696690446464 (Lam "nil" λ_nil (Src 7696698835072 (App (App (Src 7696699883637 _cons) (Src 7696705126522 _head)) (Src 7696710369407 _tail))))))))))))))))) (Src 7696593977413 (All "T" (Src 7696601317396 (Set)) λ_T (Src 7696606560325 (All "head" (Src 7696617046051 _T) λ_head (Src 7696622288965 (All "tail" (Src 7696632774713 (App (Src 7696633823286 (Book.List)) (Src 7696639066168 _T))) λ_tail (Src 7696645357637 (App (Src 7696646406210 (Book.List)) (Src 7696651649092 _T)))))))))))
|
||||
Book.Char = (Ref "Char" (Ann (Src 9895616184335 (U60)) (Src 9895611990024 (Set))))
|
||||
Book.String.cons = (Ref "String.cons" (Ann (Src 10995180241009 (Lam "head" λ_head (Src 10995187581041 (Lam "tail" λ_tail (Src 10995197018225 (Ins (Src 10995198066801 (Lam "P" λ_P (Src 10995202261105 (Lam "cons" λ_cons (Src 10995209601137 (Lam "nil" λ_nil (Src 10995217989745 (App (App (Src 10995219038310 _cons) (Src 10995224281195 _head)) (Src 10995229524080 _tail))))))))))))))) (Src 10995130957882 (All "head" (Src 10995141443612 (Book.Char)) λ_head (Src 10995149832250 (All "tail" (Src 10995160318000 (Book.String)) λ_tail (Src 10995170803770 (Book.String))))))))
|
||||
Book.String.nil = (Ref "String.nil" (Ann (Src 12094650974253 (Ins (Src 12094652022829 (Lam "P" λ_P (Src 12094656217133 (Lam "cons" λ_cons (Src 12094663557165 (Lam "nil" λ_nil (Src 12094671945773 _nil))))))))) (Src 12094641537043 (Book.String))))
|
||||
Book.Bool = (Ref "Bool" (Ann (Src 2199034789997 (Slf "self" (Src 2199043178519 (Book.Bool)) λ_self (Src 2199051567213 (All "P" (Src 2199058907184 (All "x" (Src 2199066247213 (Book.Bool)) λ_x (Src 2199072538672 (Set)))) λ_P (Src 2199077781613 (All "t" (Src 2199085121608 (App (Src 2199086170173 _P) (Src 2199088267335 (Book.Bool.true)))) λ_t (Src 2199102947437 (All "f" (Src 2199110287457 (App (Src 2199111336021 _P) (Src 2199113433184 (Book.Bool.false)))) λ_f (Src 2199129161837 (App (Src 2199130210407 _P) (Src 2199132307564 _self))))))))))) (Src 2199030595592 (Set))))
|
||||
Book.Bool.true = (Ref "Bool.true" (Ann (Src 3298554806305 (Ins (Src 3298555854881 (Lam "P" λ_P (Src 3298560049185 (Lam "t" λ_t (Src 3298564243489 (Lam "f" λ_f (Src 3298568437793 _t))))))))) (Src 3298547466256 (Book.Bool))))
|
||||
|
||||
Main = (API.check "Main" Book.Main)
|
||||
|
||||
@ -1,6 +1,23 @@
|
||||
Main
|
||||
: #U60
|
||||
= "foo"
|
||||
//: ∀(x: ?A) (List #U60)
|
||||
//= λx
|
||||
//(List.cons ?B x
|
||||
//(List.cons ?C #10
|
||||
//(List.cons ?D #20
|
||||
//(List.nil ?E))))
|
||||
: ∀(b: Bool) Bool
|
||||
= λb (~b (?A) ?B ?C)
|
||||
|
||||
|
||||
|
||||
//(?A Bool.true) == (~b λx(*) Nat String)
|
||||
|
||||
|
||||
//Main = (List.cons ?A #1 (List.cons ?B #2 (List.nil ?C)))
|
||||
|
||||
//Main
|
||||
//: #U60
|
||||
//= "foo"
|
||||
|
||||
//Main
|
||||
//: ∀(P: ∀(x: Bool) *)
|
||||
@ -263,3 +280,4 @@ Main
|
||||
//#+: ">"
|
||||
//}: String
|
||||
//}: String
|
||||
|
||||
|
||||
610
src/kind2.hvm1
610
src/kind2.hvm1
@ -82,12 +82,16 @@
|
||||
|
||||
(Pair.get (Pair fst snd) fun) = (fun fst snd)
|
||||
|
||||
(Maybe.match (Some value) some none) = (some value)
|
||||
(Maybe.match None some none) = none
|
||||
|
||||
(Maybe.pure x) = (Some x)
|
||||
(Maybe.bind a b) = (Maybe.match a λvalue(b value) None)
|
||||
|
||||
(Maybe.bind a b) = (Maybe.bind.match a b)
|
||||
|
||||
(Maybe.bind.match None b) = None
|
||||
(Maybe.bind.match (Some a) b) = (b a)
|
||||
// Converts an U60 to a bitstring
|
||||
(U60.to_bits 0) = E
|
||||
(U60.to_bits 1) = (I E)
|
||||
(U60.to_bits n) = (If (== (% n 2) 0) (O (U60.to_bits (/ n 2))) (I (U60.to_bits (/ n 2))))
|
||||
|
||||
(String.color RESET) = (String.cons 27 "[0m")
|
||||
(String.color BRIGHT) = (String.cons 27 "[1m")
|
||||
@ -116,73 +120,145 @@
|
||||
(String.color BG_GRAY) = (String.cons 27 "[100m")
|
||||
(String.color x) = "?"
|
||||
|
||||
// BitsMap
|
||||
// -------
|
||||
|
||||
//// data BM A = BM.Nil | (BM.Node A BM BM)
|
||||
|
||||
//// Returns true if value is present on BM
|
||||
//(BM.has E (BM.node (Some val) lft rgt)) = 1
|
||||
//(BM.has (O bits) (BM.node val lft rgt)) = (BM.has bits lft)
|
||||
//(BM.has (I bits) (BM.node val lft rgt)) = (BM.has bits rgt)
|
||||
//(BM.has key val) = 0
|
||||
|
||||
//// Gets a value from a BM
|
||||
//(BM.get E (BM.leaf)) = None
|
||||
//(BM.get E (BM.node val lft rgt)) = val
|
||||
//(BM.get (O bits) (BM.leaf)) = None
|
||||
//(BM.get (O bits) (BM.node val lft rgt)) = (BM.get bits lft)
|
||||
//(BM.get (I bits) (BM.leaf)) = None
|
||||
//(BM.get (I bits) (BM.node val lft rgt)) = (BM.get bits rgt)
|
||||
|
||||
//// Sets a value on a BM
|
||||
//(BM.set E val (BM.leaf)) = (BM.node (Some val) BM.leaf BM.leaf)
|
||||
//(BM.set E val (BM.node _ lft rgt)) = (BM.node (Some val) lft rgt)
|
||||
//(BM.set (O bits) val (BM.leaf)) = (BM.node None (BM.set bits val BM.leaf) BM.leaf)
|
||||
//(BM.set (O bits) val (BM.node v lft rgt)) = (BM.node v (BM.set bits val lft) rgt)
|
||||
//(BM.set (I bits) val (BM.leaf)) = (BM.node None BM.leaf (BM.set bits val BM.leaf))
|
||||
//(BM.set (I bits) val (BM.node v lft rgt)) = (BM.node v lft (BM.set bits val rgt))
|
||||
|
||||
//// Map wrapper with String keys
|
||||
//(Map.new) = BM.leaf
|
||||
//(Map.has key map) = (BM.has (U60.to_bits key) map)
|
||||
//(Map.get key map) = (BM.get (U60.to_bits key) map)
|
||||
//(Map.set key val map) = (BM.set (U60.to_bits key) val map)
|
||||
|
||||
(Map.new) = List.nil
|
||||
|
||||
(Map.has k (List.cons (Pair key val) map)) = (If (Same key k) 1 (Map.has k map))
|
||||
(Map.has k List.nil) = 0
|
||||
|
||||
(Map.put k v (List.cons (Pair key val) map)) = ((If (Same key k) λmap(None) λmap(Maybe.bind (Map.set k v map) λmap (List.cons (Pair key val) map))) map)
|
||||
(Map.put k v List.nil) = (Some (List.cons (Pair k v) List.nil))
|
||||
|
||||
(Map.set k v (List.cons (Pair key val) map)) = ((If (Same key k) λmap(List.cons (Pair k v) map) λmap(List.cons (Pair key val) (Map.set k v map))) map)
|
||||
(Map.set k v List.nil) = (List.cons (Pair k v) List.nil)
|
||||
|
||||
(Map.get k (List.cons (Pair key val) map)) = (If (Same key k) (Some val) (Map.get k map))
|
||||
(Map.get k List.nil) = None
|
||||
|
||||
// Evaluation
|
||||
// ----------
|
||||
|
||||
(Reduce lv (App fun arg)) = (Reduce.app lv (Reduce lv fun) arg)
|
||||
(Reduce lv (Ann val typ)) = (Reduce lv val)
|
||||
(Reduce lv (Ins val)) = (Reduce lv val)
|
||||
(Reduce lv (Ref nam val)) = (Reduce.ref lv nam (Reduce lv val))
|
||||
(Reduce lv (Let nam val bod)) = (Reduce lv (bod val))
|
||||
(Reduce lv (Op2 opr fst snd)) = (Reduce.op2 lv opr (Reduce lv fst) (Reduce lv snd))
|
||||
(Reduce lv (Mat nam x z s p)) = (Reduce.mat lv nam (Reduce lv x) z s p)
|
||||
(Reduce lv (Txt txt)) = (Reduce.txt lv txt)
|
||||
(Reduce lv (Src src val)) = (Reduce lv val)
|
||||
(Reduce lv val) = val
|
||||
(Reduce fill lv (App fun arg)) = (Reduce.app fill lv (Reduce fill lv fun) arg)
|
||||
(Reduce fill lv (Ann val typ)) = (Reduce fill lv val)
|
||||
(Reduce fill lv (Ins val)) = (Reduce fill lv val)
|
||||
(Reduce fill lv (Ref nam val)) = (Reduce.ref fill lv nam (Reduce fill lv val))
|
||||
(Reduce fill lv (Let nam val bod)) = (Reduce fill lv (bod val))
|
||||
(Reduce fill lv (Op2 opr fst snd)) = (Reduce.op2 fill lv opr (Reduce fill lv fst) (Reduce fill lv snd))
|
||||
(Reduce fill lv (Mat nam x z s p)) = (Reduce.mat fill lv nam (Reduce fill lv x) z s p)
|
||||
(Reduce fill lv (Txt txt)) = (Reduce.txt fill lv txt)
|
||||
(Reduce fill lv (Src src val)) = (Reduce fill lv val)
|
||||
(Reduce fill lv (Hol nam ctx)) = (Reduce.hol fill lv nam ctx)
|
||||
(Reduce fill lv val) = val
|
||||
|
||||
(Reduce.app lv (Lam nam bod) arg) = (Reduce lv (bod (Reduce 0 arg)))
|
||||
(Reduce.app lv fun arg) = (App fun arg)
|
||||
(Reduce.app fill lv (Lam nam bod) arg) = (Reduce fill lv (bod (Reduce fill 0 arg)))
|
||||
(Reduce.app fill lv fun arg) = (App fun arg)
|
||||
|
||||
(Reduce.op2 lv ADD (Num fst) (Num snd)) = (Num (+ fst snd))
|
||||
(Reduce.op2 lv SUB (Num fst) (Num snd)) = (Num (- fst snd))
|
||||
(Reduce.op2 lv MUL (Num fst) (Num snd)) = (Num (* fst snd))
|
||||
(Reduce.op2 lv DIV (Num fst) (Num snd)) = (Num (/ fst snd))
|
||||
(Reduce.op2 lv MOD (Num fst) (Num snd)) = (Num (% fst snd))
|
||||
(Reduce.op2 lv EQ (Num fst) (Num snd)) = (Num (== fst snd))
|
||||
(Reduce.op2 lv NE (Num fst) (Num snd)) = (Num (!= fst snd))
|
||||
(Reduce.op2 lv LT (Num fst) (Num snd)) = (Num (< fst snd))
|
||||
(Reduce.op2 lv GT (Num fst) (Num snd)) = (Num (> fst snd))
|
||||
(Reduce.op2 lv LTE (Num fst) (Num snd)) = (Num (<= fst snd))
|
||||
(Reduce.op2 lv GTE (Num fst) (Num snd)) = (Num (>= fst snd))
|
||||
(Reduce.op2 lv AND (Num fst) (Num snd)) = (Num (& fst snd))
|
||||
(Reduce.op2 lv OR (Num fst) (Num snd)) = (Num (| fst snd))
|
||||
(Reduce.op2 lv XOR (Num fst) (Num snd)) = (Num (^ fst snd))
|
||||
(Reduce.op2 lv LSH (Num fst) (Num snd)) = (Num (<< fst snd))
|
||||
(Reduce.op2 lv RSH (Num fst) (Num snd)) = (Num (>> fst snd))
|
||||
(Reduce.op2 lv opr fst snd) = (Op2 opr fst snd)
|
||||
(Reduce.op2 fill lv ADD (Num fst) (Num snd)) = (Num (+ fst snd))
|
||||
(Reduce.op2 fill lv SUB (Num fst) (Num snd)) = (Num (- fst snd))
|
||||
(Reduce.op2 fill lv MUL (Num fst) (Num snd)) = (Num (* fst snd))
|
||||
(Reduce.op2 fill lv DIV (Num fst) (Num snd)) = (Num (/ fst snd))
|
||||
(Reduce.op2 fill lv MOD (Num fst) (Num snd)) = (Num (% fst snd))
|
||||
(Reduce.op2 fill lv EQ (Num fst) (Num snd)) = (Num (== fst snd))
|
||||
(Reduce.op2 fill lv NE (Num fst) (Num snd)) = (Num (!= fst snd))
|
||||
(Reduce.op2 fill lv LT (Num fst) (Num snd)) = (Num (< fst snd))
|
||||
(Reduce.op2 fill lv GT (Num fst) (Num snd)) = (Num (> fst snd))
|
||||
(Reduce.op2 fill lv LTE (Num fst) (Num snd)) = (Num (<= fst snd))
|
||||
(Reduce.op2 fill lv GTE (Num fst) (Num snd)) = (Num (>= fst snd))
|
||||
(Reduce.op2 fill lv AND (Num fst) (Num snd)) = (Num (& fst snd))
|
||||
(Reduce.op2 fill lv OR (Num fst) (Num snd)) = (Num (| fst snd))
|
||||
(Reduce.op2 fill lv XOR (Num fst) (Num snd)) = (Num (^ fst snd))
|
||||
(Reduce.op2 fill lv LSH (Num fst) (Num snd)) = (Num (<< fst snd))
|
||||
(Reduce.op2 fill lv RSH (Num fst) (Num snd)) = (Num (>> fst snd))
|
||||
(Reduce.op2 fill lv opr fst snd) = (Op2 opr fst snd)
|
||||
|
||||
(Reduce.mat lv nam (Num 0) z s p) = (Reduce lv z)
|
||||
(Reduce.mat lv nam (Num n) z s p) = (Reduce lv (s (Num (- n 1))))
|
||||
(Reduce.mat lv nam (Op2 ADD (Num 1) k) z s p) = (Reduce lv (s k))
|
||||
(Reduce.mat lv nam val z s p) = (Mat nam val z s p)
|
||||
(Reduce.mat fill lv nam (Num 0) z s p) = (Reduce fill lv z)
|
||||
(Reduce.mat fill lv nam (Num n) z s p) = (Reduce fill lv (s (Num (- n 1))))
|
||||
(Reduce.mat fill lv nam (Op2 ADD (Num 1) k) z s p) = (Reduce fill lv (s k))
|
||||
(Reduce.mat fill lv nam val z s p) = (Mat nam val z s p)
|
||||
|
||||
(Reduce.ref 1 nam val) = (Reduce 1 val)
|
||||
(Reduce.ref 2 nam val) = (Reduce 2 val)
|
||||
(Reduce.ref lv nam val) = (Ref nam val)
|
||||
(Reduce.ref fill 1 nam val) = (Reduce fill 1 val)
|
||||
(Reduce.ref fill 2 nam val) = (Reduce fill 2 val)
|
||||
(Reduce.ref fill lv nam val) = (Ref nam val)
|
||||
|
||||
(Reduce.txt lv (String.cons x xs)) = (Reduce lv (App (App Book.String.cons (Num x)) (Txt xs)))
|
||||
(Reduce.txt lv String.nil) = (Reduce lv Book.String.nil)
|
||||
(Reduce.txt lv val) = (Txt val)
|
||||
(Reduce.txt fill lv (String.cons x xs)) = (Reduce fill lv (App (App Book.String.cons (Num x)) (Txt xs)))
|
||||
(Reduce.txt fill lv String.nil) = (Reduce fill lv Book.String.nil)
|
||||
(Reduce.txt fill lv val) = (Txt val)
|
||||
|
||||
(Normal lv term dep) = (Normal.term lv (Reduce lv term) dep)
|
||||
(Reduce.hol fill lv nam ctx) = (Maybe.match (Map.get nam fill) λval(Reduce fill lv val) (Hol nam ctx))
|
||||
|
||||
(Normal.term lv (All nam inp bod) dep) = (All nam (Normal lv inp dep) λx(Normal lv (bod (Var nam dep)) (+ dep 1)))
|
||||
(Normal.term lv (Lam nam bod) dep) = (Lam nam λx(Normal lv (bod (Var nam dep)) (+ 1 dep)))
|
||||
(Normal.term lv (App fun arg) dep) = (App (Normal lv fun dep) (Normal lv arg dep))
|
||||
(Normal.term lv (Ann val typ) dep) = (Ann (Normal lv val dep) (Normal lv typ dep))
|
||||
(Normal.term lv (Slf nam typ bod) dep) = (Slf nam typ λx(Normal lv (bod (Var nam dep)) (+ 1 dep)))
|
||||
(Normal.term lv (Ins val) dep) = (Ins (Normal lv val dep))
|
||||
(Normal.term lv (Ref nam val) dep) = (Ref nam (Normal lv val dep))
|
||||
(Normal.term lv (Let nam val bod) dep) = (Let nam (Normal lv val bod) λx(Normal lv (bod (Var nam dep)) (+ 1 dep)))
|
||||
(Normal.term lv (Hol nam ctx) dep) = (Hol nam ctx)
|
||||
(Normal.term lv Set dep) = Set
|
||||
(Normal.term lv U60 dep) = U60
|
||||
(Normal.term lv (Num val) dep) = (Num val)
|
||||
(Normal.term lv (Op2 opr fst snd) dep) = (Op2 opr (Normal.term lv fst dep) (Normal.term lv snd dep))
|
||||
(Normal.term lv (Mat nam x z s p) dep) = (Mat nam (Normal lv x dep) (Normal lv z dep) λk(Normal lv (s (Var (String.concat nam "-1") dep)) dep) λk(Normal lv (p (Var nam dep)) dep))
|
||||
(Normal.term lv (Txt val) dep) = (Txt val)
|
||||
(Normal.term lv (Var nam idx) dep) = (Var nam idx)
|
||||
(Normal.term lv (Src src val) dep) = (Src src (Normal lv val dep))
|
||||
(Normal fill lv term dep) = (Normal.term fill lv (Reduce fill lv term) dep)
|
||||
|
||||
(Normal.term fill lv (All nam inp bod) dep) = (All nam (Normal fill lv inp dep) λx(Normal fill lv (bod (Var nam dep)) (+ dep 1)))
|
||||
(Normal.term fill lv (Lam nam bod) dep) = (Lam nam λx(Normal fill lv (bod (Var nam dep)) (+ 1 dep)))
|
||||
(Normal.term fill lv (App fun arg) dep) = (App (Normal fill lv fun dep) (Normal fill lv arg dep))
|
||||
(Normal.term fill lv (Ann val typ) dep) = (Ann (Normal fill lv val dep) (Normal fill lv typ dep))
|
||||
(Normal.term fill lv (Slf nam typ bod) dep) = (Slf nam typ λx(Normal fill lv (bod (Var nam dep)) (+ 1 dep)))
|
||||
(Normal.term fill lv (Ins val) dep) = (Ins (Normal fill lv val dep))
|
||||
(Normal.term fill lv (Ref nam val) dep) = (Ref nam (Normal fill lv val dep))
|
||||
(Normal.term fill lv (Let nam val bod) dep) = (Let nam (Normal fill lv val bod) λx(Normal fill lv (bod (Var nam dep)) (+ 1 dep)))
|
||||
(Normal.term fill lv (Hol nam ctx) dep) = (Hol nam ctx)
|
||||
(Normal.term fill lv Set dep) = Set
|
||||
(Normal.term fill lv U60 dep) = U60
|
||||
(Normal.term fill lv (Num val) dep) = (Num val)
|
||||
(Normal.term fill lv (Op2 opr fst snd) dep) = (Op2 opr (Normal.term fill lv fst dep) (Normal.term fill lv snd dep))
|
||||
(Normal.term fill lv (Mat nam x z s p) dep) = (Mat nam (Normal fill lv x dep) (Normal fill lv z dep) λk(Normal fill lv (s (Var (String.concat nam "-1") dep)) dep) λk(Normal fill lv (p (Var nam dep)) dep))
|
||||
(Normal.term fill lv (Txt val) dep) = (Txt val)
|
||||
(Normal.term fill lv (Var nam idx) dep) = (Var nam idx)
|
||||
(Normal.term fill lv (Src src val) dep) = (Src src (Normal fill lv val dep))
|
||||
|
||||
// Checker
|
||||
// -------
|
||||
|
||||
// type Result A = (Done State A) | (Fail State String)
|
||||
// type Checker A = State -> (Result A)
|
||||
|
||||
(Result.match (Done state value) done fail) = (done state value)
|
||||
(Result.match (Fail state error) done fail) = (fail state error)
|
||||
|
||||
(State.get (State fill logs) got) = (got fill logs)
|
||||
(State.new) = (State Map.new [])
|
||||
|
||||
(Checker.bind a b) = λstate (Result.match (a state) λstateλvalue((b value) state) λstateλerror(Fail state error))
|
||||
(Checker.pure a) = λstate (Done state a)
|
||||
(Checker.fail e) = λstate (Fail state e)
|
||||
(Checker.run chk) = (chk State.new)
|
||||
(Checker.log msg) = λstate (Done (State.get state λfill λlogs (State fill (List.cons msg logs))) 1)
|
||||
(Checker.fill key val) = λstate (Done (State.get state λfill λlogs (State (Map.set key val fill) logs)) 1)
|
||||
(Checker.get_fill) = λstate (Done state (Pair.fst state))
|
||||
(Checker.save) = λstate (Done state state)
|
||||
(Checker.load state) = λerase (Done state 0)
|
||||
|
||||
// Equality
|
||||
// --------
|
||||
@ -192,49 +268,193 @@
|
||||
// Before changing it, READ `docs/equality.md`
|
||||
// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
// Check if two terms are identical. If not...
|
||||
// Checks if two term are equal
|
||||
(Equal a b dep) =
|
||||
(If (Identical a b dep) 1
|
||||
let a = (Reduce 2 a)
|
||||
let b = (Reduce 2 b)
|
||||
(If (Identical a b dep) 1
|
||||
(Similar a b dep)))
|
||||
(Checker.bind (Checker.save) λstate
|
||||
(Checker.bind (Identical a b dep) λequal
|
||||
(If equal
|
||||
(Checker.pure equal)
|
||||
(Checker.bind (Checker.load state) λx
|
||||
(Checker.bind (Checker.get_fill) λfill
|
||||
let a = (Reduce fill 2 a)
|
||||
let b = (Reduce fill 2 b)
|
||||
(Checker.bind (Identical a b dep) λequal
|
||||
(If equal
|
||||
(Checker.pure equal)
|
||||
(Similar a b dep))))))))
|
||||
|
||||
(Similar (All a.nam a.inp a.bod) (All b.nam b.inp b.bod) dep) = (& (Equal a.inp b.inp dep) (Equal (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep)))
|
||||
(Similar (Lam a.nam a.bod) (Lam b.nam b.bod) dep) = (Equal (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep))
|
||||
(Similar (App a.fun a.arg) (App b.fun b.arg) dep) = (& (Equal a.fun b.fun dep) (Equal a.arg b.arg dep))
|
||||
(Similar (Slf a.nam a.typ a.bod) (Slf b.nam b.typ b.bod) dep) = (Similar (Reduce 0 a.typ) (Reduce 0 b.typ) dep) // <- must call Similar, NOT Equal
|
||||
(Similar (Hol a.nam a.ctx) b dep) = (Debug dep ["Found: ?" a.nam " = " (Show (Normal 0 b dep) dep)] 1)
|
||||
(Similar a (Hol b.nam b.ctx) dep) = (Debug dep ["Found: ?" b.nam " = " (Show (Normal 0 a dep) dep)] 1)
|
||||
(Similar (Hol a.nam a.ctx) (Hol b.nam b.ctx) dep) = (Same a.nam b.nam)
|
||||
(Similar (Op2 a.opr a.fst a.snd) (Op2 b.opr b.fst b.snd) dep) = (& (Equal a.fst b.fst dep) (Equal a.snd b.snd dep))
|
||||
(Similar (Mat a.nam a.x a.z a.s a.p) (Mat b.nam b.x b.z b.s b.p) dep) = (& (Equal a.x b.x dep) (& (Equal a.z b.z dep) (& (Equal (a.s (Var (String.concat a.nam "-1") dep)) (b.s (Var (String.concat b.nam "-1") dep)) dep) (Equal (a.p (Var a.nam dep)) (b.p (Var b.nam dep)) dep))))
|
||||
(Similar a b dep) = 0
|
||||
// Checks if all components of a term are equal
|
||||
(Similar (All a.nam a.inp a.bod) (All b.nam b.inp b.bod) dep) =
|
||||
(Checker.bind (Equal a.inp b.inp dep) λe.inp
|
||||
(Checker.bind (Equal (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep)) λe.bod
|
||||
(Checker.pure (& e.inp e.bod))))
|
||||
(Similar (Lam a.nam a.bod) (Lam b.nam b.bod) dep) =
|
||||
(Equal (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep))
|
||||
(Similar (App a.fun a.arg) (App b.fun b.arg) dep) =
|
||||
(Checker.bind (Equal a.fun b.fun dep) λe.fun
|
||||
(Checker.bind (Equal a.arg b.arg dep) λe.arg
|
||||
(Checker.pure (& e.fun e.arg))))
|
||||
(Similar (Slf a.nam a.typ a.bod) (Slf b.nam b.typ b.bod) dep) =
|
||||
(Similar (Reduce Map.new 0 a.typ) (Reduce Map.new 0 b.typ) dep) // <- must call Similar, NOT Equal
|
||||
(Similar (Hol a.nam a.ctx) (Hol b.nam b.ctx) dep) =
|
||||
(Checker.pure (Same a.nam b.nam))
|
||||
(Similar (Op2 a.opr a.fst a.snd) (Op2 b.opr b.fst b.snd) dep) =
|
||||
(Checker.bind (Equal a.fst b.fst dep) λe.fst
|
||||
(Checker.bind (Equal a.snd b.snd dep) λe.snd
|
||||
(Checker.pure (Same e.fst e.snd))))
|
||||
(Similar (Mat a.nam a.x a.z a.s a.p) (Mat b.nam b.x b.z b.s b.p) dep) =
|
||||
(Checker.bind (Equal a.x b.x dep) λe.x
|
||||
(Checker.bind (Equal a.z b.z dep) λe.z
|
||||
(Checker.bind (Equal (a.s (Var (String.concat a.nam "-1") dep)) (b.s (Var (String.concat b.nam "-1") dep)) dep) λe.s
|
||||
(Checker.bind (Equal (a.p (Var a.nam dep)) (b.p (Var b.nam dep)) dep) λe.p
|
||||
(& e.x (& e.z (& e.s e.p)))))))
|
||||
(Similar a b dep) =
|
||||
(Checker.pure 0)
|
||||
|
||||
(Identical (All a.nam a.inp a.bod) (All b.nam b.inp b.bod) dep) = (& (Identical a.inp b.inp dep) (Identical (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep)))
|
||||
(Identical (Lam a.nam a.bod) (Lam b.nam b.bod) dep) = (Identical (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep))
|
||||
(Identical (App a.fun a.arg) (App b.fun b.arg) dep) = (& (Identical a.fun b.fun dep) (Identical a.arg b.arg dep))
|
||||
(Identical (Slf a.nam a.typ a.bod) (Slf b.nam b.typ b.bod) dep) = (Identical a.typ b.typ dep)
|
||||
(Identical (Ins a.val) b dep) = (Identical a.val b dep)
|
||||
(Identical a (Ins b.val) dep) = (Identical a b.val dep)
|
||||
(Identical (Ref a.nam a.val) (Ref b.nam b.val) dep) = (Same a.nam b.nam)
|
||||
(Identical (Let a.nam a.val a.bod) b dep) = (Identical (a.bod a.val) b dep)
|
||||
(Identical a (Let b.nam b.val b.bod) dep) = (Identical a (b.bod b.val) dep)
|
||||
(Identical Set Set dep) = 1
|
||||
(Identical (Var a.nam a.idx) (Var b.nam b.idx) dep) = (== a.idx b.idx)
|
||||
(Identical (Ann a.val a.typ) b dep) = (Identical a.val b dep)
|
||||
(Identical a (Ann b.val b.typ) dep) = (Identical a b.val dep)
|
||||
(Identical (Hol a.nam a.ctx) b dep) = (Debug dep ["Found: ?" a.nam " = " (Show (Normal 0 b dep) dep)] 1)
|
||||
(Identical a (Hol b.nam b.ctx) dep) = (Debug dep ["Found: ?" b.nam " = " (Show (Normal 0 a dep) dep)] 1)
|
||||
(Identical (Hol a.nam a.ctx) (Hol b.nam b.ctx) dep) = (Same a.nam b.nam)
|
||||
(Identical U60 U60 dep) = 1
|
||||
(Identical (Num a.val) (Num b.val) dep) = (== a.val b.val)
|
||||
(Identical (Op2 a.opr a.fst a.snd) (Op2 b.opr b.fst b.snd) dep) = (& (Identical a.fst b.fst dep) (Identical a.snd b.snd dep))
|
||||
(Identical (Mat a.nam a.x a.z a.s a.p) (Mat b.nam b.x b.z b.s b.p) dep) = (& (Identical a.x b.x dep) (& (Identical a.z b.z dep) (& (Identical (a.s (Var (String.concat a.nam "-1") dep)) (b.s (Var (String.concat b.nam "-1") dep)) dep) (Identical (a.p (Var a.nam dep)) (b.p (Var b.nam dep)) dep))))
|
||||
(Identical (Txt a.txt) (Txt b.txt) dep) = (Same a.txt b.txt)
|
||||
(Identical (Src a.src a.val) b dep) = (Identical a.val b dep)
|
||||
(Identical a (Src b.src b.val) dep) = (Identical a b.val dep)
|
||||
(Identical a b dep) = 0
|
||||
// Checks if two terms are structurally identical
|
||||
(Identical a b dep) =
|
||||
//(Debug dep ["Identical?" NewLine "- " (Show a dep) NewLine "- " (Show b dep)]
|
||||
(Unify.try b a dep
|
||||
(Unify.try a b dep
|
||||
(Identical.go a b dep)))
|
||||
|
||||
(Identical.go (All a.nam a.inp a.bod) (All b.nam b.inp b.bod) dep) =
|
||||
(Checker.bind (Identical a.inp b.inp dep) λi.inp
|
||||
(Checker.bind (Identical (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep)) λi.bod
|
||||
(Checker.pure (& i.inp i.bod))))
|
||||
(Identical.go (Lam a.nam a.bod) (Lam b.nam b.bod) dep) =
|
||||
(Identical (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep))
|
||||
(Identical.go (App a.fun a.arg) (App b.fun b.arg) dep) =
|
||||
(Checker.bind (Identical a.fun b.fun dep) λi.fun
|
||||
(Checker.bind (Identical a.arg b.arg dep) λi.arg
|
||||
(Checker.pure (& i.fun i.arg))))
|
||||
(Identical.go (Slf a.nam a.typ a.bod) (Slf b.nam b.typ b.bod) dep) =
|
||||
(Identical a.typ b.typ dep)
|
||||
(Identical.go (Ins a.val) b dep) =
|
||||
(Identical a.val b dep)
|
||||
(Identical.go a (Ins b.val) dep) =
|
||||
(Identical a b.val dep)
|
||||
(Identical.go (Let a.nam a.val a.bod) b dep) =
|
||||
(Identical (a.bod a.val) b dep)
|
||||
(Identical.go a (Let b.nam b.val b.bod) dep) =
|
||||
(Identical a (b.bod b.val) dep)
|
||||
(Identical.go Set Set dep) =
|
||||
(Checker.pure 1)
|
||||
(Identical.go (Ann a.val a.typ) b dep) =
|
||||
(Identical a.val b dep)
|
||||
(Identical.go a (Ann b.val b.typ) dep) =
|
||||
(Identical a b.val dep)
|
||||
(Identical.go (Hol a.nam a.ctx) (Hol b.nam b.ctx) dep) =
|
||||
(Checker.pure (Same a.nam b.nam))
|
||||
(Identical.go U60 U60 dep) =
|
||||
(Checker.pure 1)
|
||||
(Identical.go (Num a.val) (Num b.val) dep) =
|
||||
(Checker.pure (== a.val b.val))
|
||||
(Identical.go (Op2 a.opr a.fst a.snd) (Op2 b.opr b.fst b.snd) dep) =
|
||||
(Checker.bind (Identical a.fst b.fst dep) λi.fst
|
||||
(Checker.bind (Identical a.snd b.snd dep) λi.snd
|
||||
(Checker.pure (& i.fst i.snd))))
|
||||
(Identical.go (Mat a.nam a.x a.z a.s a.p) (Mat b.nam b.x b.z b.s b.p) dep) =
|
||||
(Checker.bind (Identical a.x b.x dep) λi.x
|
||||
(Checker.bind (Identical a.z b.z dep) λi.z
|
||||
(Checker.bind (Identical (a.s (Var (String.concat a.nam "-1") dep)) (b.s (Var (String.concat b.nam "-1") dep)) dep) λi.s
|
||||
(Checker.bind (Identical (a.p (Var a.nam dep)) (b.p (Var b.nam dep)) dep) λi.p
|
||||
(& i.x (& i.z (& i.s i.p)))))))
|
||||
(Identical.go (Txt a.txt) (Txt b.txt) dep) =
|
||||
(Checker.pure (Same a.txt b.txt))
|
||||
(Identical.go (Src a.src a.val) b dep) =
|
||||
(Identical a.val b dep)
|
||||
(Identical.go a (Src b.src b.val) dep) =
|
||||
(Identical a b.val dep)
|
||||
(Identical.go (Ref a.nam a.val) (Ref b.nam b.val) dep) =
|
||||
(Checker.pure (Same a.nam b.nam))
|
||||
(Identical.go (Var a.nam a.idx) (Var b.nam b.idx) dep) =
|
||||
(Checker.pure (== a.idx b.idx))
|
||||
(Identical.go a b dep) =
|
||||
(Checker.pure 0)
|
||||
|
||||
// From smalltt:
|
||||
// 1. spine consists of distinct bound variables
|
||||
// 2. every free variable of rhs occurs in spine
|
||||
// 3. ?α does not occur in rhs
|
||||
|
||||
// Unify.try : Term -> Term -> U60 -> (Checker U60) -> (Checker U60)
|
||||
(Unify.try a b dep else) =
|
||||
(Maybe.match (Unify.pat a b dep Map.new)
|
||||
λkv(Pair.get kv λkλv(Debug dep ["- unify: ?" k " = " (Show v dep)] (Checker.fill k v)))
|
||||
(else))
|
||||
|
||||
// Unify.pat : Term -> Term -> U60 -> (Map U60 Term) -> (Maybe (Pair nam Term))
|
||||
(Unify.pat (App fun (Var nam idx)) b dep ctx) =
|
||||
(Maybe.bind (Map.put idx $x ctx) λctx
|
||||
(Maybe.bind (Unify.pat fun b dep ctx) λkv
|
||||
(Pair.get kv λkλv(Maybe.pure (Pair k (Lam nam λ$x(v)))))))
|
||||
(Unify.pat (Hol nam ctx) b dep ctx) =
|
||||
(Maybe.bind (Unify.sub b dep nam ctx) λneo
|
||||
(Maybe.pure (Pair nam neo)))
|
||||
(Unify.pat (App fun (Ann val _)) b dep ctx) = (Unify.pat (App fun val) b dep ctx)
|
||||
(Unify.pat (App fun (Ins val)) b dep ctx) = (Unify.pat (App fun val) b dep ctx)
|
||||
(Unify.pat (App fun (Src _ val)) b dep ctx) = (Unify.pat (App fun val) b dep ctx)
|
||||
(Unify.pat (Ann val typ) b dep ctx) = (Unify.pat val b dep ctx)
|
||||
(Unify.pat (Ins val) b dep ctx) = (Unify.pat val b dep ctx)
|
||||
(Unify.pat (Src src val) b dep ctx) = (Unify.pat val b dep ctx)
|
||||
(Unify.pat other b dep ctx) = None
|
||||
|
||||
// Unify.sub : Term -> U60 -> String -> (Map U60 Term) -> (Maybe Term)
|
||||
(Unify.sub (All nam inp bod) dep hol ctx) =
|
||||
(Maybe.bind (Unify.sub inp dep hol ctx) λinp
|
||||
(Maybe.bind (Unify.sub (bod (Var nam dep)) (+ dep 1) hol ctx) λbod
|
||||
(Maybe.pure (All nam inp λ_(bod)))))
|
||||
(Unify.sub (Lam nam bod) dep hol ctx) =
|
||||
(Maybe.bind (Unify.sub (bod (Var nam dep)) (+ 1 dep) hol ctx) λbod
|
||||
(Maybe.pure (Lam nam λ_(bod))))
|
||||
(Unify.sub (App fun arg) dep hol ctx) =
|
||||
(Maybe.bind (Unify.sub fun dep hol ctx) λfun
|
||||
(Maybe.bind (Unify.sub arg dep hol ctx) λarg
|
||||
(Maybe.pure (App fun arg))))
|
||||
(Unify.sub (Ann val typ) dep hol ctx) =
|
||||
(Maybe.bind (Unify.sub val dep hol ctx) λval
|
||||
(Maybe.bind (Unify.sub typ dep hol ctx) λtyp
|
||||
(Maybe.pure (Ann val typ))))
|
||||
(Unify.sub (Slf nam typ bod) dep hol ctx) =
|
||||
(Unify.sub typ dep hol ctx)
|
||||
(Unify.sub (Ins val) dep hol ctx) =
|
||||
(Maybe.bind (Unify.sub val dep hol ctx) λval
|
||||
(Maybe.pure (Ins val)))
|
||||
(Unify.sub (Ref nam val) dep hol ctx) =
|
||||
(Maybe.pure (Ref nam val))
|
||||
(Unify.sub (Let nam val bod) dep hol ctx) =
|
||||
(Maybe.bind (Unify.sub val dep hol ctx) λval
|
||||
(Maybe.bind (Unify.sub (bod (Var nam dep)) (+ 1 dep) hol ctx) λbod
|
||||
(Maybe.pure (Let nam val λ_(bod)))))
|
||||
(Unify.sub (Hol nam ctx) dep hol ctx) =
|
||||
(If (Same nam hol) None (Maybe.pure (Hol nam ctx)))
|
||||
(Unify.sub Set dep hol ctx) =
|
||||
(Maybe.pure Set)
|
||||
(Unify.sub U60 dep hol ctx) =
|
||||
(Maybe.pure U60)
|
||||
(Unify.sub (Num val) dep hol ctx) =
|
||||
(Maybe.pure (Num val))
|
||||
(Unify.sub (Op2 opr fst snd) dep hol ctx) =
|
||||
(Maybe.bind (Unify.sub fst dep hol ctx) λfst
|
||||
(Maybe.bind (Unify.sub snd dep hol ctx) λsnd
|
||||
(Maybe.pure (Op2 opr fst snd))))
|
||||
(Unify.sub (Mat nam x z s p) dep hol ctx) =
|
||||
(Maybe.bind (Unify.sub x dep hol ctx) λx
|
||||
(Maybe.bind (Unify.sub z dep hol ctx) λz
|
||||
(Maybe.bind (Unify.sub (s (Var (String.concat nam "-1") dep)) dep hol ctx) λs
|
||||
(Maybe.bind (Unify.sub (p (Var nam dep)) dep hol ctx) λp
|
||||
(Maybe.pure (Mat nam x z λ_(s) λ_(p)))))))
|
||||
(Unify.sub (Txt val) dep hol ctx) =
|
||||
(Maybe.pure (Txt val))
|
||||
(Unify.sub (Var nam idx) dep hol ctx) =
|
||||
(Maybe.bind (Map.get idx ctx) λval
|
||||
(Maybe.pure val))
|
||||
(Unify.sub (Src src val) dep hol ctx) =
|
||||
(Maybe.bind (Unify.sub val dep hol ctx) λval
|
||||
(Maybe.pure (Src src val)))
|
||||
(Unify.sub term dep hol ctx) =
|
||||
(HVM.log (UNEXPECTED (Show term dep)) None)
|
||||
|
||||
// Type-Checking
|
||||
// -------------
|
||||
@ -249,57 +469,61 @@
|
||||
(Infer term dep) = (Infer.match term dep)
|
||||
|
||||
(Infer.match (All nam inp bod) dep) =
|
||||
(Maybe.bind (Check 0 inp Set dep) λinp_typ
|
||||
(Maybe.bind (Check 0 (bod (Ann (Var nam dep) inp)) Set (+ 1 dep)) λbod_typ
|
||||
(Maybe.pure Set)))
|
||||
(Infer.match (Lam nam bod) dep) =
|
||||
(Debug dep ["NON_FUNCTION_LAMBDA" NewLine "- detected: " (Show (Lam nam bod) dep)] (None))
|
||||
(Checker.bind (Check 0 inp Set dep) λinp_typ
|
||||
(Checker.bind (Check 0 (bod (Ann (Var nam dep) inp)) Set (+ 1 dep)) λbod_typ
|
||||
(Checker.pure Set)))
|
||||
(Infer.match (App fun arg) dep) =
|
||||
(Maybe.bind (Infer fun dep) λfun_typ
|
||||
((IfAll (Reduce 2 fun_typ)
|
||||
(Checker.bind (Infer fun dep) λfun_typ
|
||||
(Checker.bind (Checker.get_fill) λfill
|
||||
((IfAll (Reduce fill 2 fun_typ)
|
||||
λfun_nam λfun_typ.inp λfun_typ.bod λfun λarg
|
||||
(Maybe.bind (Check 0 arg fun_typ.inp dep) λval_typ
|
||||
(Maybe.pure (fun_typ.bod arg)))
|
||||
(Checker.bind (Check 0 arg fun_typ.inp dep) λvty
|
||||
(Checker.pure (fun_typ.bod arg)))
|
||||
λfun λarg
|
||||
(Debug dep ["Error: NonFunApp " (Show (App fun arg) dep)] None))
|
||||
fun arg))
|
||||
(Checker.fail (NonFunApp (App fun arg) dep)))
|
||||
fun arg)))
|
||||
(Infer.match (Ann val typ) dep) =
|
||||
(Maybe.pure typ)
|
||||
(Checker.pure typ)
|
||||
(Infer.match (Slf nam typ bod) dep) =
|
||||
(Maybe.bind (Check 0 (bod (Ann (Var nam dep) typ)) Set (+ dep 1)) λslf
|
||||
(Maybe.pure Set))
|
||||
(Checker.bind (Check 0 (bod (Ann (Var nam dep) typ)) Set (+ dep 1)) λslf
|
||||
(Checker.pure Set))
|
||||
(Infer.match (Ins val) dep) =
|
||||
(Maybe.bind (Infer val dep) λval_typ
|
||||
((IfSlf (Reduce 2 val_typ)
|
||||
λval_typ.nam λval_typ.typ λval_typ.bod λval (Maybe.pure (val_typ.bod (Ins val)))
|
||||
λval (Debug dep ["Error: NonSlfIns " (Show (Ins val) dep)] None))
|
||||
val))
|
||||
(Checker.bind (Infer val dep) λvty
|
||||
(Checker.bind (Checker.get_fill) λfill
|
||||
((IfSlf (Reduce fill 2 vty)
|
||||
λvty.nam λvty.typ λvty.bod λval
|
||||
(Checker.pure (vty.bod (Ins val)))
|
||||
λval
|
||||
(Checker.fail (NonSlfIns (Ins val))))
|
||||
val)))
|
||||
(Infer.match (Ref nam val) dep) =
|
||||
(Infer val dep)
|
||||
(Infer.match (Let nam val bod) dep) =
|
||||
(Debug dep ["Error: NonAnnLet " (Show (Let nam val bod) dep)] (None))
|
||||
(Infer.match Set dep) =
|
||||
(Maybe.pure Set)
|
||||
(Checker.pure Set)
|
||||
(Infer.match U60 dep) =
|
||||
(Maybe.pure Set)
|
||||
(Checker.pure Set)
|
||||
(Infer.match (Num num) dep) =
|
||||
(Maybe.pure U60)
|
||||
(Checker.pure U60)
|
||||
(Infer.match (Txt txt) dep) =
|
||||
(Maybe.pure Book.String)
|
||||
(Checker.pure Book.String)
|
||||
(Infer.match (Op2 opr fst snd) dep) =
|
||||
(Maybe.bind (Check 0 fst U60 dep) λfst
|
||||
(Maybe.bind (Check 0 snd U60 dep) λsnd
|
||||
(Maybe.pure U60)))
|
||||
(Checker.bind (Check 0 fst U60 dep) λfst
|
||||
(Checker.bind (Check 0 snd U60 dep) λsnd
|
||||
(Checker.pure U60)))
|
||||
(Infer.match (Mat nam x z s p) dep) =
|
||||
(Maybe.bind (Check 0 x U60 dep) λx_typ
|
||||
(Maybe.bind (Check 0 (p (Ann (Var nam dep) U60)) Set dep) λp_typ
|
||||
(Maybe.bind (Check 0 z (p (Num 0)) dep) λz_typ
|
||||
(Maybe.bind (Check 0 (s (Ann (Var (String.concat nam "-1") dep) U60)) (p (Op2 ADD (Num 1) (Var (String.concat nam "-1") dep))) (+ dep 1)) λs_typ
|
||||
(Maybe.pure (p x))))))
|
||||
(Checker.bind (Check 0 x U60 dep) λx_typ
|
||||
(Checker.bind (Check 0 (p (Ann (Var nam dep) U60)) Set dep) λp_typ
|
||||
(Checker.bind (Check 0 z (p (Num 0)) dep) λz_typ
|
||||
(Checker.bind (Check 0 (s (Ann (Var (String.concat nam "-1") dep) U60)) (p (Op2 ADD (Num 1) (Var (String.concat nam "-1") dep))) (+ dep 1)) λs_typ
|
||||
(Checker.pure (p x))))))
|
||||
(Infer.match (Lam nam bod) dep) =
|
||||
(Checker.fail (CantInfer (Lam nam bod) dep))
|
||||
(Infer.match (Let nam val bod) dep) =
|
||||
(Checker.fail (CantInfer (Let nam val bod) dep))
|
||||
(Infer.match (Hol nam ctx) dep) =
|
||||
(Debug dep ["Error: NonAnnHol " (Show (Hol nam ctx) dep)] None)
|
||||
(Checker.fail (CantInfer (Hol nam ctx) dep))
|
||||
(Infer.match (Var nam idx) dep) =
|
||||
(Debug dep ["Error: NonAnnVar " (Show (Var nam idx) dep)] None)
|
||||
(Checker.fail (CantInfer (Var nam idx) dep))
|
||||
(Infer.match (Src src val) dep) =
|
||||
(Infer.match val dep)
|
||||
|
||||
@ -307,7 +531,8 @@
|
||||
(Check src term type dep) = (Check.match src term type dep)
|
||||
|
||||
(Check.match src (Lam term.nam term.bod) type dep) =
|
||||
((IfAll (Reduce 2 type)
|
||||
(Checker.bind (Checker.get_fill) λfill
|
||||
((IfAll (Reduce fill 2 type)
|
||||
λtype.nam λtype.inp λtype.bod λterm.bod
|
||||
let ann = (Ann (Var term.nam dep) type.inp)
|
||||
let term = (term.bod ann)
|
||||
@ -315,19 +540,23 @@
|
||||
(Check 0 term type (+ dep 1))
|
||||
λterm.bod
|
||||
(Infer (Lam term.nam term.bod) dep))
|
||||
term.bod)
|
||||
term.bod))
|
||||
(Check.match src (Ins term.val) type dep) =
|
||||
((IfSlf (Reduce 2 type)
|
||||
λtype.nam λtype.typ λtype.bod λterm.val (Check 0 term.val (type.bod (Ins term.val)) dep)
|
||||
λterm.val (Infer (Ins term.val) dep))
|
||||
term.val)
|
||||
(Checker.bind (Checker.get_fill) λfill
|
||||
((IfSlf (Reduce fill 2 type)
|
||||
λtype.nam λtype.typ λtype.bod λterm.val
|
||||
(Check 0 term.val (type.bod (Ins term.val)) dep)
|
||||
λterm.val
|
||||
(Infer (Ins term.val) dep))
|
||||
term.val))
|
||||
(Check.match src (Let term.nam term.val term.bod) type dep) =
|
||||
(Check 0 (term.bod term.val) type (+ 1 dep))
|
||||
(Check.match src (Hol term.nam term.ctx) type dep) =
|
||||
(Debug dep [(String.color BRIGHT) "HOLE: ?" term.nam " :: " (Show (Normal 0 type dep) dep) (String.color RESET) (Context.show term.ctx dep)]
|
||||
(Maybe.pure 0))
|
||||
(Checker.bind (Checker.log (FoundHole term.nam type term.ctx dep)) λx
|
||||
(Checker.pure 0))
|
||||
(Check.match src (Ref term.nam (Ann term.val term.typ)) type dep) = // better printing
|
||||
(Check.report src (Equal type term.typ dep) term.typ type (Ref term.nam term.val) dep)
|
||||
(Checker.bind (Equal type term.typ dep) λequal
|
||||
(Check.report src equal term.typ type (Ref term.nam term.val) dep))
|
||||
(Check.match src (Src term.src term.val) type dep) =
|
||||
(Check term.src term.val type dep)
|
||||
//(Check.match src (Ref term.nam term.val) type dep) =
|
||||
@ -336,21 +565,14 @@
|
||||
(Check.verify src term type dep)
|
||||
|
||||
(Check.verify src term type dep) =
|
||||
(Maybe.bind (Infer term dep) λinfer
|
||||
(Check.report src (Equal type infer dep) infer type term dep))
|
||||
(Checker.bind (Infer term dep) λinfer
|
||||
(Checker.bind (Equal type infer dep) λequal
|
||||
(Check.report src equal infer type term dep)))
|
||||
|
||||
(Check.report src 0 detected expected value dep) =
|
||||
let det = (Show (Normal 0 detected dep) dep)
|
||||
let exp = (Show (Normal 0 expected dep) dep)
|
||||
let val = (Show (Normal 0 value dep) dep)
|
||||
(Debug dep [(String.color BRIGHT) "TYPE_MISMATCH" NewLine
|
||||
"- expected: " (String.color RESET) (String.color GREEN) exp NewLine (String.color RESET) (String.color BRIGHT)
|
||||
"- detected: " (String.color RESET) (String.color RED) det NewLine (String.color RESET) (String.color BRIGHT)
|
||||
"- bad_term: " (String.color RESET) (String.color DIM) val NewLine (String.color RESET)
|
||||
"##LOC{" (U60.show src) "}LOC##" NewLine
|
||||
] None)
|
||||
(Check.report src n inferred expected value dep) =
|
||||
(Maybe.pure 0)
|
||||
(Checker.fail (TypeMismatch src detected expected value dep))
|
||||
(Check.report src n detected expected value dep) =
|
||||
(Checker.pure 0)
|
||||
|
||||
// Syntax
|
||||
// ------
|
||||
@ -372,6 +594,7 @@
|
||||
(Show (Hol nam ctx) dep) = (String.join ["?" nam])
|
||||
(Show (Var nam idx) dep) = (String.join [nam])
|
||||
(Show (Src src val) dep) = (Show val dep)
|
||||
//(Show (Src src val) dep) = (String.join ["!" (Show val dep)])
|
||||
//(Show (Var nam idx) dep) = (String.join [nam "'" (U60.show idx)])
|
||||
|
||||
(Show.many List.nil dep) = ""
|
||||
@ -392,13 +615,36 @@
|
||||
(Op2.show MUL) = "*"
|
||||
(Op2.show DIV) = "/"
|
||||
|
||||
(Context.show List.nil dep) = ""
|
||||
(Context.show (List.cons x xs) dep) = (String.join [NewLine "- " (Context.show.ann x dep) (Context.show xs dep)])
|
||||
(Context.show fill List.nil dep) = ""
|
||||
(Context.show fill (List.cons x xs) dep) = (String.join [NewLine "- " (Context.show.ann fill x dep) (Context.show fill xs dep)])
|
||||
|
||||
(Context.show.ann (Ann val typ) dep) = (String.join ["{" (Show (Normal 0 val dep) dep) ": " (Show (Normal 0 typ dep) dep) "}"])
|
||||
(Context.show.ann term dep) = (Show (Normal 0 term dep) dep)
|
||||
(Context.show.ann fill (Ann val typ) dep) = (String.join ["{" (Show (Normal fill 0 val dep) dep) ": " (Show (Normal fill 0 typ dep) dep) "}"])
|
||||
(Context.show.ann fill term dep) = (Show (Normal fill 0 term dep) dep)
|
||||
//(Context.show.ann val dep) = (String.join ["{" (Show (Normal 0 val dep) dep) ": " (Show (Normal 0 (Infer val dep) dep) dep) "}"])
|
||||
|
||||
(Message.show fill (FoundHole name type ctx dep)) =
|
||||
let bold = (String.color BRIGHT)
|
||||
let reset = (String.color RESET)
|
||||
let type = (Show (Normal fill 0 type dep) dep)
|
||||
let ctx = (Context.show fill ctx dep)
|
||||
(String.join [bold "HOLE: ?" name " :: " type ctx reset])
|
||||
(Message.show fill (NonFunApp term dep)) =
|
||||
let term = (Show term dep)
|
||||
(String.join ["NON_FUNCTION_APPLICATION:" term])
|
||||
(Message.show fill (CantInfer term dep)) =
|
||||
let term = (Show term dep)
|
||||
(String.join ["CANT_INFER:" term])
|
||||
(Message.show fill (TypeMismatch src detected expected value dep)) =
|
||||
let det = (Show (Normal fill 0 detected dep) dep)
|
||||
let exp = (Show (Normal fill 0 expected dep) dep)
|
||||
let val = (Show (Normal fill 0 value dep) dep)
|
||||
(String.join [(String.color BRIGHT) "TYPE_MISMATCH" NewLine
|
||||
"- expected: " (String.color RESET) (String.color GREEN) exp NewLine (String.color RESET) (String.color BRIGHT)
|
||||
"- detected: " (String.color RESET) (String.color RED) det NewLine (String.color RESET) (String.color BRIGHT)
|
||||
"- bad_term: " (String.color RESET) (String.color DIM) val NewLine (String.color RESET)
|
||||
"##LOC{" (U60.show src) "}LOC##" NewLine
|
||||
])
|
||||
|
||||
// Compilation
|
||||
// -----------
|
||||
|
||||
@ -461,24 +707,30 @@ Compile.primitives = [
|
||||
// API
|
||||
// ---
|
||||
|
||||
(Normalizer (Ref nam val)) = (Normalizer val)
|
||||
(Normalizer (Ann val typ)) = (Normalizer val)
|
||||
(Normalizer (Src src val)) = (Normalizer val)
|
||||
(Normalizer val) = (Compile val)
|
||||
//(Normalizer val) = (Str.view (Compile val))
|
||||
(API.normal (Ref nam val)) = (API.normal val)
|
||||
(API.normal (Ann val typ)) = (API.normal val)
|
||||
(API.normal (Src src val)) = (API.normal val)
|
||||
(API.normal val) = (Compile val)
|
||||
//(API.normal val) = (Str.view (Compile val))
|
||||
|
||||
(Checker name (Ref nam val)) = (Checker name val)
|
||||
(Checker name (Src src (Ann val typ))) = (Checker.report name (Check src val typ 0))
|
||||
(Checker name (Src src val)) = (Checker name val)
|
||||
(Checker name (Ann val typ)) = (Checker.report name (Check 0 val typ 0))
|
||||
(Checker name val) = (Checker.report name (Infer val 0))
|
||||
// Checker
|
||||
|
||||
(Checker.report name (Some x)) = 1
|
||||
(Checker.report name None) = 0
|
||||
//(Checker.report name (Some x)) = (HVM.print (String.join [(String.color GREEN) "- " name ": ✔" (String.color RESET)]) 1)
|
||||
//(Checker.report name None) = (HVM.print (String.join [(String.color RED) "- " name ": ✘" (String.color RESET)]) 0)
|
||||
(API.check name (Ref nam val)) = (API.check name val)
|
||||
(API.check name (Src src (Ann val typ))) = (API.check.report name (Checker.run (Check src val typ 0)))
|
||||
(API.check name (Src src val)) = (API.check name val)
|
||||
(API.check name (Ann val typ)) = (API.check.report name (Checker.run (Check 0 val typ 0)))
|
||||
(API.check name val) = (API.check.report name (Checker.run (Infer val 0)))
|
||||
|
||||
(Checker.many.go (List.cons (Pair name def) defs)) = (& (Checker name def) (Checker.many.go defs))
|
||||
(Checker.many.go List.nil) = 1
|
||||
(API.check.many list) = (If (API.check.many.go list) ALL_TERMS_CHECK ERRORS_FOUND)
|
||||
|
||||
(API.check.many.go (List.cons (Pair name def) defs)) = (& (API.check name def) (API.check.many.go defs))
|
||||
(API.check.many.go List.nil) = 1
|
||||
|
||||
// Reporter
|
||||
|
||||
(API.log fill (List.cons msg msgs)) = (HVM.print (Message.show fill msg) (API.log fill msgs))
|
||||
(API.log fill List.nil) = λx x
|
||||
|
||||
(API.check.report name (Done (State fill logs) val)) = ((API.log fill logs) 1)
|
||||
(API.check.report name (Fail (State fill logs) err)) = ((API.log fill logs) ((API.log fill [err]) 0))
|
||||
|
||||
(Checker.many list) = (If (Checker.many.go list) ALL_TERMS_CHECK ERRORS_FOUND)
|
||||
|
||||
@ -591,8 +591,9 @@ fn generate_check_hvm1(book: &Book, command: &str, arg: &str) -> String {
|
||||
let kind2_hvm1 = include_str!("./kind2.hvm1");
|
||||
let book_hvm1 = book.to_hvm1();
|
||||
let main_hvm1 = match command {
|
||||
"check" => format!("Main = (Checker.many [{}])\n", used_defs),
|
||||
"run" => format!("Main = (Normalizer Book.{})\n", arg),
|
||||
"check" => format!("Main = (API.check \"{}\" Book.{})\n", arg, arg),
|
||||
//"check" => format!("Main = (API.check.many [{}])\n", used_defs),
|
||||
"run" => format!("Main = (API.normal Book.{})\n", arg),
|
||||
_ => panic!("invalid command"),
|
||||
};
|
||||
let hvm1_code = format!("{}\n{}\n{}", kind2_hvm1, book_hvm1, main_hvm1);
|
||||
|
||||
Loading…
Reference in New Issue
Block a user