diff --git a/book/.check.hvm1 b/book/.check.hvm1 index 108cb797..9872fbc2 100644 --- a/book/.check.hvm1 +++ b/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) diff --git a/book/Main.kind2 b/book/Main.kind2 index 9a1a0cc3..35138ccb 100644 --- a/book/Main.kind2 +++ b/book/Main.kind2 @@ -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 + diff --git a/src/kind2.hvm1 b/src/kind2.hvm1 index b59f7565..23d64c0d 100644 --- a/src/kind2.hvm1 +++ b/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) diff --git a/src/main.rs b/src/main.rs index 3fb172c3..4b532cab 100644 --- a/src/main.rs +++ b/src/main.rs @@ -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);