mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-10-05 19:27:30 +03:00
improved equality - check docs/equality.md
This commit is contained in:
Victor Taelin
parent
6dbe738b4c
commit
c8fd9e54d5
301
book/.check.hvm1
301
book/.check.hvm1
@ -17,7 +17,7 @@
|
||||
//| (Lam nam bod)
|
||||
//| (App fun arg)
|
||||
//| (Ann val typ)
|
||||
//| (Slf nam bod)
|
||||
//| (Slf nam typ bod)
|
||||
//| (Ins val)
|
||||
//| (Ref nam val)
|
||||
//| (Let nam val bod)
|
||||
@ -119,115 +119,185 @@
|
||||
// Evaluation
|
||||
// ----------
|
||||
|
||||
(Reduce r (App fun arg)) = (Reduce.app r (Reduce r fun) arg)
|
||||
(Reduce r (Ann val typ)) = (Reduce r val)
|
||||
(Reduce r (Ins val)) = (Reduce r val)
|
||||
(Reduce 1 (Ref nam val)) = (Reduce 1 val)
|
||||
(Reduce r (Let nam val bod)) = (Reduce r (bod val))
|
||||
(Reduce r (Op2 opr fst snd)) = (Reduce.op2 r opr fst snd)
|
||||
(Reduce r (Mat nam x z s p)) = (Reduce.mat r nam x z s p)
|
||||
(Reduce 1 (Txt txt)) = (Reduce.txt 1 txt)
|
||||
(Reduce r (Src src val)) = (Reduce r val)
|
||||
(Reduce r val) = val
|
||||
// Reduction levels:
|
||||
// - 0: does not reduce references and constructors
|
||||
// - 1: does not reduce constructors
|
||||
// - 2: reduces everything
|
||||
// Constructors are Refs that return Slf or Ins
|
||||
|
||||
(Reduce.app r (Lam nam bod) arg) = (Reduce r (bod (Reduce 0 arg)))
|
||||
//(Reduce.app r (Hol nam ctx ars) arg) = (Hol nam ctx (List.cons arg ars))
|
||||
(Reduce.app r fun arg) = (App fun arg)
|
||||
(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.op2 r ADD (Num fst) (Num snd)) = (Num (+ fst snd))
|
||||
(Reduce.op2 r SUB (Num fst) (Num snd)) = (Num (- fst snd))
|
||||
(Reduce.op2 r MUL (Num fst) (Num snd)) = (Num (* fst snd))
|
||||
(Reduce.op2 r DIV (Num fst) (Num snd)) = (Num (/ fst snd))
|
||||
(Reduce.op2 r MOD (Num fst) (Num snd)) = (Num (% fst snd))
|
||||
(Reduce.op2 r EQ (Num fst) (Num snd)) = (Num (== fst snd))
|
||||
(Reduce.op2 r NE (Num fst) (Num snd)) = (Num (!= fst snd))
|
||||
(Reduce.op2 r LT (Num fst) (Num snd)) = (Num (< fst snd))
|
||||
(Reduce.op2 r GT (Num fst) (Num snd)) = (Num (> fst snd))
|
||||
(Reduce.op2 r LTE (Num fst) (Num snd)) = (Num (<= fst snd))
|
||||
(Reduce.op2 r GTE (Num fst) (Num snd)) = (Num (>= fst snd))
|
||||
(Reduce.op2 r AND (Num fst) (Num snd)) = (Num (& fst snd))
|
||||
(Reduce.op2 r OR (Num fst) (Num snd)) = (Num (| fst snd))
|
||||
(Reduce.op2 r XOR (Num fst) (Num snd)) = (Num (^ fst snd))
|
||||
(Reduce.op2 r LSH (Num fst) (Num snd)) = (Num (<< fst snd))
|
||||
(Reduce.op2 r RSH (Num fst) (Num snd)) = (Num (>> fst snd))
|
||||
(Reduce.op2 r opr fst snd) = (Op2 opr fst snd)
|
||||
(Reduce.app lv (Lam nam bod) arg) = (Reduce lv (bod (Reduce 0 arg)))
|
||||
(Reduce.app lv fun arg) = (App fun arg)
|
||||
|
||||
(Reduce.mat r nam (Num 0) z s p) = (Reduce r z)
|
||||
(Reduce.mat r nam (Num n) z s p) = (Reduce r (s (Num (- n 1))))
|
||||
(Reduce.mat r nam (Op2 ADD (Num 1) k) z s p) = (Reduce r (s k))
|
||||
(Reduce.mat r nam val z s p) = (Mat nam val z s p)
|
||||
(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.txt r (String.cons x xs)) = (Reduce 1 (App (App Book.String.cons (Num x)) (Txt xs)))
|
||||
(Reduce.txt r String.nil) = (Reduce 1 Book.String.nil)
|
||||
(Reduce.txt r val) = val
|
||||
(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)
|
||||
|
||||
(Normal r term dep) = (Normal.term r (Reduce r term) dep)
|
||||
(Reduce.ref 1 nam val) = (Reduce 1 val)
|
||||
(Reduce.ref 2 nam val) = (Reduce 2 val)
|
||||
(Reduce.ref lv nam val) = (Ref nam val)
|
||||
|
||||
(Normal.term r (All nam inp bod) dep) = (All nam (Normal r inp dep) λx(Normal r (bod (Var nam dep)) (+ dep 1)))
|
||||
(Normal.term r (Lam nam bod) dep) = (Lam nam λx(Normal r (bod (Var nam dep)) (+ 1 dep)))
|
||||
(Normal.term r (App fun arg) dep) = (App (Normal r fun dep) (Normal r arg dep))
|
||||
(Normal.term r (Ann val typ) dep) = (Ann (Normal r val dep) (Normal r typ dep))
|
||||
(Normal.term r (Slf nam bod) dep) = (Slf nam λx(Normal r (bod (Var nam dep)) (+ 1 dep)))
|
||||
(Normal.term r (Ins val) dep) = (Ins (Normal r val dep))
|
||||
(Normal.term r (Ref nam val) dep) = (Ref nam (Normal r val dep))
|
||||
(Normal.term r (Let nam val bod) dep) = (Let nam (Normal r val bod) λx(Normal r (bod (Var nam dep)) (+ 1 dep)))
|
||||
(Normal.term r (Hol nam ctx) dep) = (Hol nam ctx)
|
||||
(Normal.term r Set dep) = Set
|
||||
(Normal.term r U60 dep) = U60
|
||||
(Normal.term r (Num val) dep) = (Num val)
|
||||
(Normal.term r (Op2 opr fst snd) dep) = (Op2 opr (Normal.term r fst dep) (Normal.term r snd dep))
|
||||
(Normal.term r (Mat nam x z s p) dep) = (Mat nam (Normal r x dep) (Normal r z dep) λk(Normal r (s (Var (String.concat nam "-1") dep)) dep) λk(Normal r (p (Var nam dep)) dep))
|
||||
(Normal.term r (Txt val) dep) = (Txt val)
|
||||
(Normal.term r (Var nam idx) dep) = (Var nam idx)
|
||||
(Normal.term r (Src src val) dep) = (Src src (Normal r val dep))
|
||||
(Reduce.txt 0 (Txt txt)) = (Txt txt)
|
||||
(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) = val
|
||||
|
||||
(Normal lv term dep) = (Normal.term lv (Reduce lv term) dep)
|
||||
|
||||
(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))
|
||||
|
||||
// Equality
|
||||
// --------
|
||||
|
||||
// NEW EQUALITY
|
||||
|
||||
// Check if two terms are identical. If not...
|
||||
(Equal a b dep) = (Equal.minor (Identical a b dep) a b dep)
|
||||
(Equal a b dep) =
|
||||
//(Debug dep ["Equal: " (U60.show dep)
|
||||
//NewLine "- " (Show a dep) " ~> " (Show (Reduce 2 a) dep)
|
||||
//NewLine "- " (Show b dep) " ~> " (Show (Reduce 2 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)))
|
||||
//)
|
||||
|
||||
// Check if they're identical after a minor weak reduction. If not...
|
||||
(Equal.minor 0 a b dep) = (Equal.major (Identical (Reduce 0 a) (Reduce 0 b) dep) a b dep)
|
||||
(Equal.minor 1 a b dep) = 1
|
||||
(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)
|
||||
(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
|
||||
|
||||
// Check if they're identical after a major weak reduction. If not...
|
||||
(Equal.major 0 a b dep) = (Equal.enter (Identical (Reduce 1 a) (Reduce 1 b) dep) a b dep)
|
||||
(Equal.major 1 a b dep) = 1
|
||||
(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
|
||||
|
||||
// Check if they become identical after reducing fields.
|
||||
(Equal.enter 0 a b dep) = (Comparer λaλbλdep(Equal a b dep) (Reduce 0 a) (Reduce 0 b) dep)
|
||||
(Equal.enter 1 a b dep) = 1
|
||||
// OLD EQUALITY
|
||||
|
||||
// Checks if two terms are identical, without reductions.
|
||||
(Identical a b dep) = (Comparer λaλbλdep(Identical a b dep) a b dep)
|
||||
//// Check if two terms are identical. If not...
|
||||
//(Equal a b dep) =
|
||||
//(Debug dep ["Equal:" NewLine "- " (Show a dep) NewLine "- " (Show b dep)]
|
||||
//(If (Identical a b dep) 1 (Equal (Reduce 2 a) (Reduce 2 b) dep)))
|
||||
////(Equal a b dep) = (If (Identical a b dep) 1 (Equal (Reduce 2 a) (Reduce 2 b) dep))
|
||||
|
||||
// Generic comparer.
|
||||
(Comparer rec (All a.nam a.inp a.bod) (All b.nam b.inp b.bod) dep) = (& (rec a.inp b.inp dep) (rec (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep)))
|
||||
(Comparer rec (Lam a.nam a.bod) (Lam b.nam b.bod) dep) = (rec (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep))
|
||||
(Comparer rec (App a.fun a.arg) (App b.fun b.arg) dep) = (& (rec a.fun b.fun dep) (rec a.arg b.arg dep))
|
||||
(Comparer rec (Slf a.nam a.bod) (Slf b.nam b.bod) dep) = (rec (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep))
|
||||
(Comparer rec (Ins a.val) b dep) = (rec a.val b dep)
|
||||
(Comparer rec a (Ins b.val) dep) = (rec a b.val dep)
|
||||
(Comparer rec (Ref a.nam a.val) (Ref b.nam b.val) dep) = (Same a.nam b.nam)
|
||||
(Comparer rec (Let a.nam a.val a.bod) b dep) = (rec (a.bod a.val) b dep)
|
||||
(Comparer rec a (Let b.nam b.val b.bod) dep) = (rec a (b.bod b.val) dep)
|
||||
(Comparer rec Set Set dep) = 1
|
||||
(Comparer rec (Var a.nam a.idx) (Var b.nam b.idx) dep) = (== a.idx b.idx)
|
||||
(Comparer rec (Ann a.val a.typ) b dep) = (rec a.val b dep)
|
||||
(Comparer rec a (Ann b.val b.typ) dep) = (rec a b.val dep)
|
||||
(Comparer rec (Hol a.nam a.ctx) b dep) = (Debug dep ["Found: ?" a.nam " = " (Show (Normal 0 b dep) dep)] 1)
|
||||
(Comparer rec a (Hol b.nam b.ctx) dep) = (Debug dep ["Found: ?" b.nam " = " (Show (Normal 0 a dep) dep)] 1)
|
||||
(Comparer rec (Hol a.nam a.ctx) (Hol b.nam b.ctx) dep) = (Same a.nam b.nam)
|
||||
(Comparer rec U60 U60 dep) = 1
|
||||
(Comparer rec (Num a.val) (Num b.val) dep) = (== a.val b.val)
|
||||
(Comparer rec (Op2 a.opr a.fst a.snd) (Op2 b.opr b.fst b.snd) dep) = (& (rec a.fst b.fst dep) (rec a.snd b.snd dep))
|
||||
(Comparer rec (Mat a.nam a.x a.z a.s a.p) (Mat b.nam b.x b.z b.s b.p) dep) = (& (rec a.x b.x dep) (& (rec a.z b.z dep) (& (rec (a.s (Var (String.concat a.nam "-1") dep)) (b.s (Var (String.concat b.nam "-1") dep)) dep) (rec (a.p (Var a.nam dep)) (b.p (Var b.nam dep)) dep))))
|
||||
(Comparer rec (Txt a.txt) (Txt b.txt) dep) = (Same a.txt b.txt)
|
||||
(Comparer rec (Src a.src a.val) b dep) = (Comparer rec a.val b dep)
|
||||
(Comparer rec a (Src b.src b.val) dep) = (Comparer rec a b.val dep)
|
||||
(Comparer rec a b dep) = 0
|
||||
//(Comparer rec a b dep) = (HVM.log (NOP (Show a dep) (Show b dep)) 0)
|
||||
|
||||
////// Check if they're identical after a minor weak reduction. If not...
|
||||
////(Equal.minor 0 a b dep) = (Equal.major (Identical (Reduce 0 a) (Reduce 0 b) dep) a b dep)
|
||||
////(Equal.minor 1 a b dep) = 1
|
||||
|
||||
////// Check if they're identical after a major weak reduction. If not...
|
||||
////(Equal.major 0 a b dep) = (Equal.final (Identical (Reduce 1 a) (Reduce 1 b) dep) a b dep)
|
||||
////(Equal.major 1 a b dep) = 1
|
||||
|
||||
////// Check if they're identical after a major weak reduction. If not...
|
||||
////(Equal.final 0 a b dep) = (Equal.enter (Identical (Reduce 2 a) (Reduce 2 b) dep) a b dep)
|
||||
////(Equal.final 1 a b dep) = 1
|
||||
|
||||
////// Check if they become identical after reducing fields.
|
||||
////(Equal.enter 0 a b dep) = (Comparer λaλbλdep(Equal a b dep) (Reduce 1 a) (Reduce 1 b) dep)
|
||||
////(Equal.enter 1 a b dep) = 1
|
||||
|
||||
//// Checks if two terms are identical, without reductions.
|
||||
//(Identical a b dep) = (Comparer λaλbλdep(Identical a b dep) a b dep)
|
||||
|
||||
//// Generic comparer.
|
||||
//(Comparer rec (All a.nam a.inp a.bod) (All b.nam b.inp b.bod) dep) = (& (rec a.inp b.inp dep) (rec (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep)))
|
||||
//(Comparer rec (Lam a.nam a.bod) (Lam b.nam b.bod) dep) = (rec (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep))
|
||||
//(Comparer rec (App a.fun a.arg) (App b.fun b.arg) dep) = (& (rec a.fun b.fun dep) (rec a.arg b.arg dep))
|
||||
//(Comparer rec (Slf a.nam a.typ a.bod) (Slf b.nam b.typ b.bod) dep) = (rec a.typ b.typ dep)
|
||||
//(Comparer rec (Ins a.val) b dep) = (rec a.val b dep)
|
||||
//(Comparer rec a (Ins b.val) dep) = (rec a b.val dep)
|
||||
//(Comparer rec (Ref a.nam a.val) (Ref b.nam b.val) dep) = (Same a.nam b.nam)
|
||||
//(Comparer rec (Let a.nam a.val a.bod) b dep) = (rec (a.bod a.val) b dep)
|
||||
//(Comparer rec a (Let b.nam b.val b.bod) dep) = (rec a (b.bod b.val) dep)
|
||||
//(Comparer rec Set Set dep) = 1
|
||||
//(Comparer rec (Var a.nam a.idx) (Var b.nam b.idx) dep) = (== a.idx b.idx)
|
||||
//(Comparer rec (Ann a.val a.typ) b dep) = (rec a.val b dep)
|
||||
//(Comparer rec a (Ann b.val b.typ) dep) = (rec a b.val dep)
|
||||
//(Comparer rec (Hol a.nam a.ctx) b dep) = (Debug dep ["Found: ?" a.nam " = " (Show (Normal 0 b dep) dep)] 1)
|
||||
//(Comparer rec a (Hol b.nam b.ctx) dep) = (Debug dep ["Found: ?" b.nam " = " (Show (Normal 0 a dep) dep)] 1)
|
||||
//(Comparer rec (Hol a.nam a.ctx) (Hol b.nam b.ctx) dep) = (Same a.nam b.nam)
|
||||
//(Comparer rec U60 U60 dep) = 1
|
||||
//(Comparer rec (Num a.val) (Num b.val) dep) = (== a.val b.val)
|
||||
//(Comparer rec (Op2 a.opr a.fst a.snd) (Op2 b.opr b.fst b.snd) dep) = (& (rec a.fst b.fst dep) (rec a.snd b.snd dep))
|
||||
//(Comparer rec (Mat a.nam a.x a.z a.s a.p) (Mat b.nam b.x b.z b.s b.p) dep) = (& (rec a.x b.x dep) (& (rec a.z b.z dep) (& (rec (a.s (Var (String.concat a.nam "-1") dep)) (b.s (Var (String.concat b.nam "-1") dep)) dep) (rec (a.p (Var a.nam dep)) (b.p (Var b.nam dep)) dep))))
|
||||
//(Comparer rec (Txt a.txt) (Txt b.txt) dep) = (Same a.txt b.txt)
|
||||
//(Comparer rec (Src a.src a.val) b dep) = (Comparer rec a.val b dep)
|
||||
//(Comparer rec a (Src b.src b.val) dep) = (Comparer rec a b.val dep)
|
||||
//(Comparer rec a b dep) = 0
|
||||
////(Comparer rec a b dep) = (HVM.log (NOP (Show a dep) (Show b dep)) 0)
|
||||
|
||||
// Type-Checking
|
||||
// -------------
|
||||
@ -235,8 +305,8 @@
|
||||
(IfAll (All nam inp bod) yep nop) = (yep nam inp bod)
|
||||
(IfAll other yep nop) = nop
|
||||
|
||||
(IfSlf (Slf nam bod) yep nop) = (yep nam bod)
|
||||
(IfSlf other yep nop) = nop
|
||||
(IfSlf (Slf nam typ bod) yep nop) = (yep nam typ bod)
|
||||
(IfSlf other yep nop) = nop
|
||||
|
||||
//(Infer term dep) = (Debug dep ["Infer: " (Show term dep)] (Infer.match term dep))
|
||||
(Infer term dep) = (Infer.match term dep)
|
||||
@ -246,10 +316,10 @@
|
||||
(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 ["Error: NonFunLam " (Show (Lam nam bod) dep)] (None))
|
||||
(Debug dep ["NON_FUNCTION_LAMBDA" NewLine "- detected: " (Show (Lam nam bod) dep)] (None))
|
||||
(Infer.match (App fun arg) dep) =
|
||||
(Maybe.bind (Infer fun dep) λfun_typ
|
||||
((IfAll (Reduce 1 fun_typ)
|
||||
((IfAll (Reduce 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)))
|
||||
@ -258,13 +328,13 @@
|
||||
fun arg))
|
||||
(Infer.match (Ann val typ) dep) =
|
||||
(Maybe.pure typ)
|
||||
(Infer.match (Slf nam bod) dep) =
|
||||
(Maybe.bind (Check 0 (bod (Ann (Var nam dep) (Slf nam bod))) Set (+ dep 1)) λslf
|
||||
(Infer.match (Slf nam typ bod) dep) =
|
||||
(Maybe.bind (Check 0 (bod (Ann (Var nam dep) typ)) Set (+ dep 1)) λslf
|
||||
(Maybe.pure Set))
|
||||
(Infer.match (Ins val) dep) =
|
||||
(Maybe.bind (Infer val dep) λval_typ
|
||||
((IfSlf (Reduce 1 val_typ)
|
||||
λval_nam λval_typ.bod λval (Maybe.pure (val_typ.bod (Ins val)))
|
||||
((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))
|
||||
(Infer.match (Ref nam val) dep) =
|
||||
@ -296,11 +366,11 @@
|
||||
(Infer.match (Src src val) dep) =
|
||||
(Infer.match val dep)
|
||||
|
||||
//(Check term type dep) = (Debug dep ["Check: " (Show term dep) " :: " (Show type dep)] (Check.match 0 term type dep))
|
||||
//(Check src term type dep) = (Debug dep ["Check: " (Show term dep) " :: " (Show type dep) " ~> " (Show (Reduce 2 type) dep)] (Check.match src term type dep))
|
||||
(Check src term type dep) = (Check.match src term type dep)
|
||||
|
||||
(Check.match src (Lam term.nam term.bod) type dep) =
|
||||
((IfAll (Reduce 1 type)
|
||||
((IfAll (Reduce 2 type)
|
||||
λtype.nam λtype.inp λtype.bod λterm.bod
|
||||
let ann = (Ann (Var term.nam dep) type.inp)
|
||||
let term = (term.bod ann)
|
||||
@ -310,8 +380,8 @@
|
||||
(Infer (Lam term.nam term.bod) dep))
|
||||
term.bod)
|
||||
(Check.match src (Ins term.val) type dep) =
|
||||
((IfSlf (Reduce 1 type)
|
||||
λtype.nam λtype.bod λterm.val (Check 0 term.val (type.bod (Ins term.val)) 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)
|
||||
(Check.match src (Let term.nam term.val term.bod) type dep) =
|
||||
@ -352,7 +422,7 @@
|
||||
(Show (Lam nam bod) dep) = (String.join ["λ" nam " " (Show (bod (Var nam dep)) (+ dep 1))])
|
||||
(Show (App fun arg) dep) = (String.join ["(" (Show.unwrap (Show fun dep)) " " (Show arg dep) ")"])
|
||||
(Show (Ann val typ) dep) = (String.join ["{" (Show val dep) ": " (Show typ dep) "}"])
|
||||
(Show (Slf nam bod) dep) = (String.join ["$" nam " " (Show (bod (Var nam dep)) (+ dep 1))])
|
||||
(Show (Slf nam typ bod) dep) = (String.join ["$(" nam ": " (Show typ dep) ") " (Show (bod (Var nam dep)) (+ dep 1))])
|
||||
(Show (Ins val) dep) = (String.join ["~" (Show val dep)])
|
||||
(Show (Ref nam val) dep) = nam
|
||||
(Show (Let nam val bod) dep) = (String.join ["let " nam " = " (Show val dep) "; " (Show (bod (Var nam dep)) (+ dep 1))])
|
||||
@ -411,7 +481,7 @@ Compile.primitives = [
|
||||
(Compile (Lam nam bod)) = λx(Compile (bod (Var "" x)))
|
||||
(Compile (App fun arg)) = ((Compile fun) (Compile arg))
|
||||
(Compile (Ann val typ)) = (Compile val)
|
||||
(Compile (Slf nam bod)) = 0
|
||||
(Compile (Slf nam typ bod)) = 0
|
||||
(Compile (Ins val)) = (Compile val)
|
||||
(Compile (Ref nam val)) = (Compile.ref Compile.primitives nam val)
|
||||
(Compile (Let nam val bod)) = (Compile (bod val))
|
||||
@ -476,11 +546,14 @@ Compile.primitives = [
|
||||
|
||||
(Checker.many list) = (If (Checker.many.go list) ALL_TERMS_CHECK ERRORS_FOUND)
|
||||
|
||||
Book.List.cons = (Ref "List.cons" (Ann (Src 5497633636480 (Lam "T" λ_T (Src 5497637830784 (Lam "head" λ_head (Src 5497645170816 (Lam "tail" λ_tail (Src 5497654608000 (Ins (Src 5497655656576 (Lam "P" λ_P (Src 5497659850880 (Lam "cons" λ_cons (Src 5497667190912 (Lam "nil" λ_nil (Src 5497675579520 (App (App (Src 5497676628085 _cons) (Src 5497681870970 _head)) (Src 5497687113855 _tail))))))))))))))))) (Src 5497570721861 (All "T" (Src 5497578061844 (Set)) λ_T (Src 5497583304773 (All "head" (Src 5497593790499 _T) λ_head (Src 5497599033413 (All "tail" (Src 5497609519161 (App (Src 5497610567734 (Book.List)) (Src 5497615810616 _T))) λ_tail (Src 5497622102085 (App (Src 5497623150658 (Book.List)) (Src 5497628393540 _T)))))))))))
|
||||
Book.List.nil = (Ref "List.nil" (Ann (Src 6597105418303 (Lam "T" λ_T (Src 6597111709759 (Ins (Src 6597112758335 (Lam "P" λ_P (Src 6597116952639 (Lam "cons" λ_cons (Src 6597124292671 (Lam "nil" λ_nil (Src 6597132681279 _nil))))))))))) (Src 6597081301023 (All "T" (Src 6597088641043 (Set)) λ_T (Src 6597093883935 (App (Src 6597094932508 (Book.List)) (Src 6597100175390 _T)))))))
|
||||
Book.Main = (Ref "Main" (Ann (Src 1099526307866 (Op2 ADD (Src 1099530502165 (Num 12)) (Src 1099534696473 (Num 30)))) (Src 1099518967819 (U60))))
|
||||
Book.List = (Ref "List" (Ann (Src 4398070628530 (Lam "T" λ_T (Src 4398076919986 (Slf "self" λ_self (Src 4398085308594 (All "P" (Src 4398092648511 (All "xs" (Src 4398101037116 (App (Src 4398102085689 (Book.List)) (Src 4398107328571 _T))) λ_xs (Src 4398111522879 (Set)))) λ_P (Src 4398116765874 (All "cons" (Src 4398127251593 (All "head" (Src 4398137737304 _T) λ_head (Src 4398140883081 (All "tail" (Src 4398151368812 (App (Src 4398152417385 (Book.List)) (Src 4398157660267 _T))) λ_tail (Src 4398161854601 (App (Src 4398162903152 _P) (Src 4398165000328 (App (App (App (Src 4398166048891 (Book.List.cons)) (Src 4398176534653 _T)) (Src 4398178631810 _head)) (Src 4398183874695 _tail))))))))) λ_cons (Src 4398194360498 (All "nil" (Src 4398203797670 (App (Src 4398204846232 _P) (Src 4398206943397 (App (Src 4398207991970 (Book.List.nil)) (Src 4398217429156 _T))))) λ_nil (Src 4398224769202 (App (Src 4398225817772 _P) (Src 4398227914929 _self))))))))))))) (Src 4398053851156 (All "T" (Src 4398061191183 (Set)) λ_T (Src 4398066434068 (Set))))))
|
||||
Book.Char = (Ref "Char" (Ann (Src 3298546417679 (U60)) (Src 3298542223368 (Set))))
|
||||
Book.String = (Ref "String" (Ann (Src 2199036887064 (App (Src 2199037935634 (Book.List)) (Src 2199043178519 (Book.Char)))) (Src 2199032692746 (Set))))
|
||||
Book.Main = (Ref "Main" (Ann (Src 1099585028173 (Lam "x" λ_x (Src 1099591319629 _x))) (Src 1099518967875 (All "x" (Src 1099526307881 (App (Src 1099527356444 (Book.Parser.Result)) (Src 1099542036520 (App (Src 1099543085090 (Book.List)) (Src 1099548327975 (Book.Char)))))) λ_x (Src 1099558813763 (App (Src 1099559862331 (Book.Parser.Result)) (Src 1099574542402 (Book.String))))))))
|
||||
Book.Parser.Result.done = (Ref "Parser.Result.done" (Ann (Src 8796186345620 (Lam "T" λ_T (Src 8796190539924 (Lam "code" λ_code (Src 8796197879956 (Lam "value" λ_value (Src 8796208365716 (Ins (Src 8796209414292 (Lam "P" λ_P (Src 8796213608596 (Lam "done" λ_done (Src 8796220948628 (Lam "fail" λ_fail (Src 8796230385812 (App (App (Src 8796231434376 _done) (Src 8796236677261 _code)) (Src 8796241920147 _value))))))))))))))))) (Src 8796115042390 (All "T" (Src 8796122382365 (Set)) λ_T (Src 8796127625302 (All "code" (Src 8796138111025 (Book.String)) λ_code (Src 8796148596822 (All "value" (Src 8796160131137 _T) λ_value (Src 8796165374038 (App (Src 8796166422611 (Book.Parser.Result)) (Src 8796181102677 _T)))))))))))
|
||||
Book.Parser.Result.fail = (Ref "Parser.Result.fail" (Ann (Src 9895682244729 (Lam "T" λ_T (Src 9895686439033 (Lam "error" λ_error (Src 9895696924793 (Ins (Src 9895697973369 (Lam "P" λ_P (Src 9895702167673 (Lam "done" λ_done (Src 9895709507705 (Lam "fail" λ_fail (Src 9895718944889 (App (Src 9895719993458 _fail) (Src 9895725236344 _error))))))))))))))) (Src 9895626670151 (All "T" (Src 9895634010141 (Set)) λ_T (Src 9895639253063 (All "error" (Src 9895650787378 (Book.String)) λ_error (Src 9895661273159 (App (Src 9895662321732 (Book.Parser.Result)) (Src 9895677001798 _T)))))))))
|
||||
Book.Char = (Ref "Char" (Ann (Src 3298546417679 (U60)) (Src 3298542223368 (Set))))
|
||||
Book.Parser.Result = (Ref "Parser.Result" (Ann (Src 7696614949125 (Lam "T" λ_T (Src 7696621240581 (Slf "self" (Src 7696629628991 (App (Src 7696630677564 (Book.Parser.Result)) (Src 7696645357630 _T))) λ_self (Src 7696651649285 (All "P" (Src 7696658989157 (All "x" (Src 7696666329186 (App (Src 7696667377759 (Book.Parser.Result)) (Src 7696682057825 _T))) λ_x (Src 7696686252133 (Set)))) λ_P (Src 7696691495173 (All "done" (Src 7696701980856 (All "code" (Src 7696712466563 (Book.String)) λ_code (Src 7696720855224 (All "value" (Src 7696732389521 _T) λ_value (Src 7696735535288 (App (Src 7696736583829 _P) (Src 7696738681015 (App (App (App (Src 7696739729577 (Book.Parser.Result.done)) (Src 7696759652523 _T)) (Src 7696761749680 _code)) (Src 7696766992566 _value))))))))) λ_done (Src 7696778526981 (All "fail" (Src 7696789012729 (All "error" (Src 7696800547031 (Book.String)) λ_error (Src 7696808935673 (App (Src 7696809984219 _P) (Src 7696812081400 (App (App (Src 7696813129967 (Book.Parser.Result.fail)) (Src 7696833052913 _T)) (Src 7696835150071 _error))))))) λ_fail (Src 7696846684421 (App (Src 7696847732991 _P) (Src 7696849830148 _self))))))))))))) (Src 7696598171677 (All "T" (Src 7696605511704 (Set)) λ_T (Src 7696610754589 (Set))))))
|
||||
Book.List = (Ref "List" (Ann (Src 4398070628542 (Lam "T" λ_T (Src 4398076919998 (Slf "self" (Src 4398085308461 (App (Src 4398086357034 (Book.List)) (Src 4398091599916 _T))) λ_self (Src 4398097891518 (All "P" (Src 4398105231435 (All "xs" (Src 4398113620040 (App (Src 4398114668613 (Book.List)) (Src 4398119911495 _T))) λ_xs (Src 4398124105803 (Set)))) λ_P (Src 4398129348798 (All "cons" (Src 4398139834517 (All "head" (Src 4398150320228 _T) λ_head (Src 4398153466005 (All "tail" (Src 4398163951736 (App (Src 4398165000309 (Book.List)) (Src 4398170243191 _T))) λ_tail (Src 4398174437525 (App (Src 4398175486076 _P) (Src 4398177583252 (App (App (App (Src 4398178631815 (Book.List.cons)) (Src 4398189117577 _T)) (Src 4398191214734 _head)) (Src 4398196457619 _tail))))))))) λ_cons (Src 4398206943422 (All "nil" (Src 4398216380594 (App (Src 4398217429156 _P) (Src 4398219526321 (App (Src 4398220574894 (Book.List.nil)) (Src 4398230012080 _T))))) λ_nil (Src 4398237352126 (App (Src 4398238400696 _P) (Src 4398240497853 _self))))))))))))) (Src 4398053851156 (All "T" (Src 4398061191183 (Set)) λ_T (Src 4398066434068 (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.List.cons = (Ref "List.cons" (Ann (Src 6597145264256 (Lam "T" λ_T (Src 6597149458560 (Lam "head" λ_head (Src 6597156798592 (Lam "tail" λ_tail (Src 6597166235776 (Ins (Src 6597167284352 (Lam "P" λ_P (Src 6597171478656 (Lam "cons" λ_cons (Src 6597178818688 (Lam "nil" λ_nil (Src 6597187207296 (App (App (Src 6597188255861 _cons) (Src 6597193498746 _head)) (Src 6597198741631 _tail))))))))))))))))) (Src 6597082349637 (All "T" (Src 6597089689620 (Set)) λ_T (Src 6597094932549 (All "head" (Src 6597105418275 _T) λ_head (Src 6597110661189 (All "tail" (Src 6597121146937 (App (Src 6597122195510 (Book.List)) (Src 6597127438392 _T))) λ_tail (Src 6597133729861 (App (Src 6597134778434 (Book.List)) (Src 6597140021316 _T)))))))))))
|
||||
|
||||
Main = (Normalizer Book.Main)
|
||||
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 "Parser.Result" Book.Parser.Result) (Pair "Parser.Result.done" Book.Parser.Result.done) (Pair "Parser.Result.fail" Book.Parser.Result.fail) (Pair "String" Book.String)])
|
||||
|
||||
@ -32,8 +32,6 @@ BBT.balance
|
||||
(~(BBT.got_size K V rgt) P new)
|
||||
(~(BBT.got_size K V lft) P new)
|
||||
|
||||
|
||||
|
||||
BBT.balance.lft_heavier
|
||||
: ∀(K: *)
|
||||
∀(V: *)
|
||||
|
||||
@ -3,7 +3,7 @@ BBT
|
||||
∀(V: *) // Value type
|
||||
*
|
||||
= λK λV
|
||||
$self
|
||||
$(self: (BBT K V))
|
||||
∀(P: ∀(bbt: (BBT K V)) *)
|
||||
∀(bin: ∀(size: #U60) ∀(key: K) ∀(val: V) ∀(lft: (BBT K V)) ∀(rgt: (BBT K V)) (P (BBT.bin K V size key val lft rgt)))
|
||||
∀(tip: (P (BBT.tip K V)))
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
Bool
|
||||
: *
|
||||
= $self
|
||||
= $(self: Bool)
|
||||
∀(P: ∀(x: Bool) *)
|
||||
∀(t: (P Bool.true))
|
||||
∀(f: (P Bool.false))
|
||||
|
||||
@ -1,6 +1,7 @@
|
||||
Bool.lemma.notnot
|
||||
: ∀(b: Bool)
|
||||
(Equal Bool (Bool.not (Bool.not b)) b)
|
||||
= λb (~b λx(Equal Bool (Bool.not (Bool.not x)) x)
|
||||
(Equal.refl Bool Bool.true)
|
||||
(Equal.refl Bool Bool.false))
|
||||
= λb
|
||||
(~b λx(Equal Bool (Bool.not (Bool.not x)) x)
|
||||
(Equal.refl Bool Bool.true)
|
||||
(Equal.refl Bool Bool.false))
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
Cmp
|
||||
: *
|
||||
= $self
|
||||
= $(self: Cmp)
|
||||
∀(P: ∀(cmp: Cmp) *)
|
||||
∀(ltn: (P Cmp.ltn))
|
||||
∀(eql: (P Cmp.eql))
|
||||
∀(gtn: (P Cmp.gtn))
|
||||
(P self)
|
||||
(P self)
|
||||
|
||||
@ -1,5 +1,5 @@
|
||||
Empty
|
||||
: *
|
||||
= $self
|
||||
= $(self: Empty)
|
||||
∀(P: ∀(x: Empty) *)
|
||||
(P self)
|
||||
|
||||
@ -1,7 +1,7 @@
|
||||
IO
|
||||
: ∀(A: *) *
|
||||
= λA
|
||||
$self
|
||||
$(self: (IO A))
|
||||
∀(P: ∀(x: (IO A)) *)
|
||||
∀(print: ∀(text: String) ∀(then: ∀(x: Unit) (IO A)) (P (IO.print A text then)))
|
||||
∀(load: ∀(file: String) ∀(then: ∀(x: String) (IO A)) (P (IO.load A file then)))
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
Kind.Oper
|
||||
: *
|
||||
= $self
|
||||
= $(self: Kind.Oper)
|
||||
∀(P: ∀(x: Kind.Oper) *)
|
||||
∀(add: (P Kind.Oper.add))
|
||||
∀(mul: (P Kind.Oper.mul))
|
||||
@ -18,4 +18,4 @@ Kind.Oper
|
||||
∀(xor: (P Kind.Oper.xor))
|
||||
∀(lsh: (P Kind.Oper.lsh))
|
||||
∀(rsh: (P Kind.Oper.rsh))
|
||||
(P self)
|
||||
(P self)
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
Kind.Term
|
||||
: *
|
||||
= $self
|
||||
= $(self: Kind.Term)
|
||||
∀(P: ∀(x: Kind.Term) *)
|
||||
∀(all: ∀(nam: String) ∀(inp: Kind.Term) ∀(bod: ∀(x: Kind.Term) Kind.Term) (P (Kind.all nam inp bod)))
|
||||
∀(lam: ∀(nam: String) ∀(bod: ∀(x: Kind.Term) Kind.Term) (P (Kind.lam nam bod)))
|
||||
|
||||
@ -2,7 +2,7 @@ List
|
||||
: ∀(T: *)
|
||||
*
|
||||
= λT
|
||||
$self
|
||||
$(self: (List T))
|
||||
∀(P: ∀(xs: (List T)) *)
|
||||
∀(cons: ∀(head: T) ∀(tail: (List T)) (P (List.cons T head tail)))
|
||||
∀(nil: (P (List.nil T)))
|
||||
|
||||
@ -1,6 +1,15 @@
|
||||
Main
|
||||
: #U60
|
||||
= #(+ #12 #30)
|
||||
: ∀(x: (Parser.Result (List Char)))
|
||||
(Parser.Result String)
|
||||
= λx
|
||||
x
|
||||
|
||||
//Main
|
||||
//: ∀(P: ∀(x: Bool) *)
|
||||
//∀(f: ∀(x: Bool) (P x))
|
||||
//(P (Bool.not (Bool.not Bool.true)))
|
||||
//= λP λf
|
||||
//?a
|
||||
|
||||
//TYPE_MISMATCH
|
||||
//- expected: (Pair (Maybe V) (String.Map V))
|
||||
|
||||
@ -2,7 +2,7 @@ Maybe
|
||||
: ∀(T: *)
|
||||
*
|
||||
= λT
|
||||
$self
|
||||
$(self: (Maybe T))
|
||||
∀(P: ∀(x: (Maybe T)) *)
|
||||
∀(some: ∀(value: T) (P (Maybe.some T value)))
|
||||
∀(none: (P (Maybe.none T)))
|
||||
|
||||
@ -1,7 +1,7 @@
|
||||
Monad
|
||||
: ∀(M: ∀(T: *) *) *
|
||||
= λM
|
||||
$self
|
||||
$(self: (Monad M))
|
||||
∀(P: ∀(x: (Monad M)) *)
|
||||
∀(new:
|
||||
∀(bind: ∀(A: *) ∀(B: *) ∀(a: (M A)) ∀(b: ∀(a: A) (M B)) (M B))
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
Nat
|
||||
: *
|
||||
= $self
|
||||
= $(self: Nat)
|
||||
∀(P: ∀(n: Nat) *)
|
||||
∀(succ: ∀(n: Nat) (P (Nat.succ n)))
|
||||
∀(zero: (P Nat.zero))
|
||||
|
||||
@ -3,7 +3,7 @@ Pair
|
||||
∀(B: *)
|
||||
*
|
||||
= λA λB
|
||||
$self
|
||||
$(self: (Pair A B))
|
||||
∀(P: ∀(pair: (Pair A B)) *)
|
||||
∀(new: ∀(fst: A) ∀(snd: B) (P (Pair.new A B fst snd)))
|
||||
(P self)
|
||||
|
||||
@ -2,8 +2,8 @@ Parser.Result
|
||||
: ∀(T: *)
|
||||
*
|
||||
= λT
|
||||
$self
|
||||
$(self: (Parser.Result T))
|
||||
∀(P: ∀(x: (Parser.Result T)) *)
|
||||
∀(done: ∀(code: String) ∀(value: T) (P (Parser.Result.done T code value)))
|
||||
∀(fail: ∀(error: String) (P (Parser.Result.fail T error)))
|
||||
(P self)
|
||||
(P self)
|
||||
|
||||
@ -35,7 +35,7 @@ QBool.false : QBool =
|
||||
~λP ~λS λp (p #1 λx x)
|
||||
|
||||
QBool : * =
|
||||
$self
|
||||
$(self: QBool)
|
||||
∀(P: ∀(x: QBool) *)
|
||||
(Sigma #U60 λt
|
||||
∀(x: #match t = t {
|
||||
|
||||
@ -32,7 +32,7 @@ QBool2.false : QBool2 = ~λP λnew (new #1)
|
||||
QBool2.bad : QBool2 = ~λP λnew (new #2 ?impossible)
|
||||
|
||||
QBool2 : * =
|
||||
$self
|
||||
$(self: QBool2)
|
||||
∀(P: ∀(x: QBool2) *)
|
||||
∀(new: ∀(tag: #U60) #match tag = tag {
|
||||
#0: (P QBool2.true)
|
||||
|
||||
@ -2,7 +2,7 @@ QUnit.one : QUnit =
|
||||
~λP ~λSP λnew (new #0 λone one)
|
||||
|
||||
QUnit : * =
|
||||
$self
|
||||
$(self: QUnit)
|
||||
∀(P: ∀(x: QUnit) *)
|
||||
(Sigma #U60 λtag
|
||||
#match tag = tag {
|
||||
|
||||
@ -3,7 +3,7 @@ Sigma
|
||||
∀(B: ∀(x: A) *)
|
||||
*
|
||||
= λA λB
|
||||
$self
|
||||
$(self: (Sigma A B))
|
||||
∀(P: ∀(x: (Sigma A B)) *)
|
||||
∀(new: ∀(a: A) ∀(b: (B a)) (P (Sigma.new A B a b)))
|
||||
(P self)
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
Unit
|
||||
: *
|
||||
= $self
|
||||
= $(self: Unit)
|
||||
∀(P: ∀(x: Unit) *)
|
||||
∀(one: (P Unit.one))
|
||||
(P self)
|
||||
|
||||
@ -3,7 +3,7 @@ test7.book
|
||||
= "
|
||||
Kind.Term
|
||||
: *
|
||||
= $self
|
||||
= $(self: Kind.Term)
|
||||
∀(P: ∀(x: Kind.Term) *)
|
||||
∀(all: ∀(nam: String) ∀(inp: Kind.Term) ∀(bod: ∀(x: Kind.Term) Kind.Term) (P (Kind.all nam inp bod)))
|
||||
∀(lam: ∀(nam: String) ∀(bod: ∀(x: Kind.Term) Kind.Term) (P (Kind.lam nam bod)))
|
||||
|
||||
181
docs/equality.md
Normal file
181
docs/equality.md
Normal file
@ -0,0 +1,181 @@
|
||||
## Kind2's Equality Algorithm
|
||||
|
||||
Since Kind2 is based on Self Types, that allows us to dispense a native
|
||||
datatype system in favor of existing λ-Encodings. We can represent ANY
|
||||
inductive family by taking the dependent eliminator of that family and
|
||||
replacing the witness by a self type. For example, Nats are just:
|
||||
|
||||
```javascript
|
||||
Nat
|
||||
: *
|
||||
= $self
|
||||
∀(P: ∀(n: Nat) *)
|
||||
∀(succ: ∀(n: Nat) (P (Nat.succ n)))
|
||||
∀(zero: (P Nat.zero))
|
||||
(P self)
|
||||
|
||||
Nat.succ : ∀(n: Nat) Nat
|
||||
= λn ~λP λsucc λzero (succ n)
|
||||
|
||||
Nat.zero : Nat
|
||||
= ~λP λsucc λzero zero
|
||||
```
|
||||
|
||||
Notice, though, there are many degrees of recursion in this representation:
|
||||
|
||||
1. The Nat.succ constructor stores a Nat.
|
||||
|
||||
2. The Nat motive, P, refers to Nat.
|
||||
|
||||
3. The Nat constructors Nat.succ and Nat.zero refer to Nat, and vice-versa.
|
||||
|
||||
This kind of self-reference is inevitable, because the dependent eliminator
|
||||
of an inductive datatype refers to the type being eliminated. This truth is
|
||||
universal: even in langauges like Coq, this effect is present, it is merely
|
||||
hidden within the type-checker of dependent eliminators.
|
||||
|
||||
Since we can't rely on a hard-coded datatype system, that means conversion
|
||||
checking must be capable of dealing with the degree of mutual recursion seen
|
||||
in these encodings, otherwise, it would fail to halt. Most dependent type
|
||||
checkers are NOT capable of handling even simple recursive types; for
|
||||
example, it is impossible to represent Scott Nats *directly* (without
|
||||
wrappers) in Coq, Lean, Agda, and even Haskell. Given that the type above is
|
||||
an *inductive* view of Scott Nats, there would be no hope to type-check it in
|
||||
existing proof assistants.
|
||||
|
||||
In Kind1, the solution we adopted for this was to keep a map of "seen"
|
||||
equations. If, during the recursion process, we arrive to an equation that we
|
||||
previously visited, we just return true, short-cutting the recursion. This
|
||||
approach works, but is also complex and slow. Thankfully, Kind2's approach is
|
||||
much simpler, faster, but it is also subtler, in the sense we rely on
|
||||
reductions being performed in a precise order, otherwise it would fall into
|
||||
infinite recursive limbos. The way it works is straightforward:
|
||||
|
||||
```javascript
|
||||
// Equal
|
||||
A == B ::=
|
||||
If A and B are identical:
|
||||
return true
|
||||
Otherwise:
|
||||
reduce A and B to weak normal
|
||||
check if A and B are similar
|
||||
|
||||
// Similar
|
||||
A ~~ B ::=
|
||||
check if the fields of A and B are equal
|
||||
|
||||
// Identical
|
||||
A <> B ::=
|
||||
check if A and B are "textually" the same
|
||||
```
|
||||
|
||||
So, for example, to check if `(pair 1 2) == (pair 1 (+ 2 2))`, we would first
|
||||
check of both sides are identical. They're not, as evidenced by the fact they
|
||||
have different writings. We then reduce A and B to weak normal, and check if
|
||||
they're similar. This will recursivelly check if `1 == 1` and `4 == (+ 2 2)`.
|
||||
The first is already identical. The second becomes identical after a single
|
||||
reduction. And that's it!
|
||||
|
||||
As you can see, this is obvious enough. So, what's the catch? Suppose we
|
||||
wanted to check a self-encoded type like `(List #U60) == (List Char)`, where
|
||||
`Char` is just an alias to `#U60`. In this case, we'd have something like:
|
||||
|
||||
```javascript
|
||||
(List #U60) == (List Char)
|
||||
------------------------------------------------------------------------ // not identical; reduce
|
||||
$self ∀(P: ∀(x:(List #U60)) *) ... ~~ $self ∀(P: ∀(x:(List Char)) *) ...
|
||||
------------------------------------------------------------------------ // recurse on components
|
||||
∀(P: ∀(x:(List #U60)) *) ... == ∀(P: ∀(x:(List Char)) *) ...
|
||||
------------------------------------------------------------------------ // not identical; reduce
|
||||
∀(P: ∀(x:(List #U60)) *) ... ~~ ∀(P: ∀(x:(List Char)) *) ...
|
||||
------------------------------------------------------------------------ // recurse on components
|
||||
(List #U60) == (List Char)
|
||||
------------------------------------------------------------------------ // not identical; reduce
|
||||
... infinite loop ...
|
||||
```
|
||||
|
||||
Now, as inoffensive as this problem may look, solving it often lead us to
|
||||
undesirable directions. It may be a good exercise to pause here and think
|
||||
about how you'd solve it. For example, an obvious idea could be to have a
|
||||
special flag for "constructors" (like `List` and `Char`), and never reduce
|
||||
these during the equality. This would cause the algorithm to check if both
|
||||
sides are component-wise equal BEFORE reducing, which would work on this
|
||||
case. Yet, in other cases where we need to expand a constructor, such as
|
||||
`(not true) == false`, that would fail. Kind1's approach was a solution,
|
||||
albeit over-engineered. There are many "wrong" ways one might approach this
|
||||
problem, that inevitably lead to complexity bloat and alterations on the
|
||||
"natural" equality algorithm that inevitably come to bite us later.
|
||||
|
||||
So, how do we solve it on Kind2? First, we must note that this algorithm is,
|
||||
obviously, undecidable in general. So, our first goal must be to cover, at
|
||||
least, the same set of instances that a classical checker like Coq would. The
|
||||
algorithm above accomplishes exactly that. After all, if two terms have the same
|
||||
normal form, this algorithm *will* identify them as equal, as can be easily
|
||||
seen. Coq only deals with normalizable terms, thus, this already covers the same
|
||||
set of programs and proofs!
|
||||
|
||||
The only problem is how we deal with terms that are NOT expressive in Coq. In
|
||||
most cases, we don't care! After all, if Kind isn't capable of handling a term
|
||||
that no other checker would, then it doesn't matter. The problem is, the example
|
||||
above IS an instance the algorithm above can't handle, and we NEED it to,
|
||||
because, otherwise, we'd not have a way to encode inductive datatypes! So, how
|
||||
do we modify our equality checker just enough to make it not drown in that
|
||||
specific case, without making it complex, slow or, worse, wrong?
|
||||
|
||||
First, notice that this problem is non-existant in existing proof checkers,
|
||||
because they can NOT reduce `(List #U60)` further; `List` is an axiom. Sadly, we
|
||||
can **not** prevent it from unrolling in Kind, since this mechanism is necessary
|
||||
to check constructors properly (otherwise, `λP λt λf t :: Bool` would be a
|
||||
`non-function-application`). So, it is unavoidable that self-types will,
|
||||
depending on the situation, unroll during conversion checking.
|
||||
|
||||
**As such, what we need is not a mechanism to block reduction, but a mechanism
|
||||
to undo a reduction.**
|
||||
|
||||
In general, this looks like a terrible idea and a massive complication. But, for
|
||||
self-types specifically, there is a quite straight-forward way to do it: **just
|
||||
annotate the `self` binder**! For example, `List` would be written as:
|
||||
|
||||
```javascript
|
||||
List = λT
|
||||
$(self: (List T))
|
||||
∀(P: ∀(xs: (List T)) *)
|
||||
∀(cons: ∀(head: T) ∀(tail: (List T)) (P (List.cons T head tail)))
|
||||
∀(nil: (P (List.nil T)))
|
||||
(P self)
|
||||
```
|
||||
|
||||
This looks like a small redundancy, but it allows us to modify the `similar`
|
||||
algorithm to do exactly that: "undo" the reduction on the `self` case. That is,
|
||||
instead of:
|
||||
|
||||
```
|
||||
($x A) ~~ ($y B) ::= (B (x:A)) == (D (y:C))
|
||||
```
|
||||
|
||||
We have:
|
||||
|
||||
```
|
||||
($(x:X) A) ~~ ($(y:Y) B) ::= X ~~ Y
|
||||
```
|
||||
Note that we do NOT recurse to `==` (equality), but to `~~` (similarity), which
|
||||
will NOT reduce `X` and `Y` and will, instead, check each component separately.
|
||||
This simple change effectively gives a mechanism for the conversion checker to
|
||||
move from the complex expansion of a self-type to its compact applicative form,
|
||||
and proceed to compare it component-wise.
|
||||
|
||||
This is correct, because type constructors are injective, so, no false positive
|
||||
can occur by doing this; it merely provides the checker a simpler route. Yet,
|
||||
this WILL result in a false negative: two "identical" self-types (such as `Bit`
|
||||
and `Bool`) will no longer pass the type-checker, because it will **not** try
|
||||
expanding these references. Which may even be seen as a feature, as it gives us
|
||||
a `newtype` functionality for free. (Note that a checker must not give false
|
||||
positives; false negatives are fine.)
|
||||
|
||||
This article turned out to be way more verbose, but this is a big problem that
|
||||
deserves to be documented in details. Not in the sense that it is hard, but in
|
||||
the sense that it is really easy to get wrong; so much that Kind1 operated for
|
||||
years with an inefficient solution that was one of its one of its main
|
||||
drawbacks. So, I'm glad to have made some progress in that front, and the new
|
||||
approach looks promising. Now, this all is just for conversion checking; now, on
|
||||
to actual unification. 💀
|
||||
230
src/kind2.hvm1
230
src/kind2.hvm1
@ -17,7 +17,7 @@
|
||||
//| (Lam nam bod)
|
||||
//| (App fun arg)
|
||||
//| (Ann val typ)
|
||||
//| (Slf nam bod)
|
||||
//| (Slf nam typ bod)
|
||||
//| (Ins val)
|
||||
//| (Ref nam val)
|
||||
//| (Let nam val bod)
|
||||
@ -119,115 +119,123 @@
|
||||
// Evaluation
|
||||
// ----------
|
||||
|
||||
(Reduce r (App fun arg)) = (Reduce.app r (Reduce r fun) arg)
|
||||
(Reduce r (Ann val typ)) = (Reduce r val)
|
||||
(Reduce r (Ins val)) = (Reduce r val)
|
||||
(Reduce 1 (Ref nam val)) = (Reduce 1 val)
|
||||
(Reduce r (Let nam val bod)) = (Reduce r (bod val))
|
||||
(Reduce r (Op2 opr fst snd)) = (Reduce.op2 r opr fst snd)
|
||||
(Reduce r (Mat nam x z s p)) = (Reduce.mat r nam x z s p)
|
||||
(Reduce 1 (Txt txt)) = (Reduce.txt 1 txt)
|
||||
(Reduce r (Src src val)) = (Reduce r val)
|
||||
(Reduce r val) = val
|
||||
(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.app r (Lam nam bod) arg) = (Reduce r (bod (Reduce 0 arg)))
|
||||
//(Reduce.app r (Hol nam ctx ars) arg) = (Hol nam ctx (List.cons arg ars))
|
||||
(Reduce.app r fun arg) = (App fun arg)
|
||||
(Reduce.app lv (Lam nam bod) arg) = (Reduce lv (bod (Reduce 0 arg)))
|
||||
(Reduce.app lv fun arg) = (App fun arg)
|
||||
|
||||
(Reduce.op2 r ADD (Num fst) (Num snd)) = (Num (+ fst snd))
|
||||
(Reduce.op2 r SUB (Num fst) (Num snd)) = (Num (- fst snd))
|
||||
(Reduce.op2 r MUL (Num fst) (Num snd)) = (Num (* fst snd))
|
||||
(Reduce.op2 r DIV (Num fst) (Num snd)) = (Num (/ fst snd))
|
||||
(Reduce.op2 r MOD (Num fst) (Num snd)) = (Num (% fst snd))
|
||||
(Reduce.op2 r EQ (Num fst) (Num snd)) = (Num (== fst snd))
|
||||
(Reduce.op2 r NE (Num fst) (Num snd)) = (Num (!= fst snd))
|
||||
(Reduce.op2 r LT (Num fst) (Num snd)) = (Num (< fst snd))
|
||||
(Reduce.op2 r GT (Num fst) (Num snd)) = (Num (> fst snd))
|
||||
(Reduce.op2 r LTE (Num fst) (Num snd)) = (Num (<= fst snd))
|
||||
(Reduce.op2 r GTE (Num fst) (Num snd)) = (Num (>= fst snd))
|
||||
(Reduce.op2 r AND (Num fst) (Num snd)) = (Num (& fst snd))
|
||||
(Reduce.op2 r OR (Num fst) (Num snd)) = (Num (| fst snd))
|
||||
(Reduce.op2 r XOR (Num fst) (Num snd)) = (Num (^ fst snd))
|
||||
(Reduce.op2 r LSH (Num fst) (Num snd)) = (Num (<< fst snd))
|
||||
(Reduce.op2 r RSH (Num fst) (Num snd)) = (Num (>> fst snd))
|
||||
(Reduce.op2 r opr fst snd) = (Op2 opr fst snd)
|
||||
(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.mat r nam (Num 0) z s p) = (Reduce r z)
|
||||
(Reduce.mat r nam (Num n) z s p) = (Reduce r (s (Num (- n 1))))
|
||||
(Reduce.mat r nam (Op2 ADD (Num 1) k) z s p) = (Reduce r (s k))
|
||||
(Reduce.mat r nam val z s p) = (Mat nam val z s p)
|
||||
(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.txt r (String.cons x xs)) = (Reduce 1 (App (App Book.String.cons (Num x)) (Txt xs)))
|
||||
(Reduce.txt r String.nil) = (Reduce 1 Book.String.nil)
|
||||
(Reduce.txt r val) = val
|
||||
(Reduce.ref 1 nam val) = (Reduce 1 val)
|
||||
(Reduce.ref 2 nam val) = (Reduce 2 val)
|
||||
(Reduce.ref lv nam val) = (Ref nam val)
|
||||
|
||||
(Normal r term dep) = (Normal.term r (Reduce r term) dep)
|
||||
(Reduce.txt 0 (Txt txt)) = (Txt txt)
|
||||
(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) = val
|
||||
|
||||
(Normal.term r (All nam inp bod) dep) = (All nam (Normal r inp dep) λx(Normal r (bod (Var nam dep)) (+ dep 1)))
|
||||
(Normal.term r (Lam nam bod) dep) = (Lam nam λx(Normal r (bod (Var nam dep)) (+ 1 dep)))
|
||||
(Normal.term r (App fun arg) dep) = (App (Normal r fun dep) (Normal r arg dep))
|
||||
(Normal.term r (Ann val typ) dep) = (Ann (Normal r val dep) (Normal r typ dep))
|
||||
(Normal.term r (Slf nam bod) dep) = (Slf nam λx(Normal r (bod (Var nam dep)) (+ 1 dep)))
|
||||
(Normal.term r (Ins val) dep) = (Ins (Normal r val dep))
|
||||
(Normal.term r (Ref nam val) dep) = (Ref nam (Normal r val dep))
|
||||
(Normal.term r (Let nam val bod) dep) = (Let nam (Normal r val bod) λx(Normal r (bod (Var nam dep)) (+ 1 dep)))
|
||||
(Normal.term r (Hol nam ctx) dep) = (Hol nam ctx)
|
||||
(Normal.term r Set dep) = Set
|
||||
(Normal.term r U60 dep) = U60
|
||||
(Normal.term r (Num val) dep) = (Num val)
|
||||
(Normal.term r (Op2 opr fst snd) dep) = (Op2 opr (Normal.term r fst dep) (Normal.term r snd dep))
|
||||
(Normal.term r (Mat nam x z s p) dep) = (Mat nam (Normal r x dep) (Normal r z dep) λk(Normal r (s (Var (String.concat nam "-1") dep)) dep) λk(Normal r (p (Var nam dep)) dep))
|
||||
(Normal.term r (Txt val) dep) = (Txt val)
|
||||
(Normal.term r (Var nam idx) dep) = (Var nam idx)
|
||||
(Normal.term r (Src src val) dep) = (Src src (Normal r val dep))
|
||||
(Normal lv term dep) = (Normal.term lv (Reduce lv term) dep)
|
||||
|
||||
(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))
|
||||
|
||||
// Equality
|
||||
// --------
|
||||
|
||||
// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
// WARNING: this is a very delicate algorithm!
|
||||
// Before changing it, READ `docs/equality.md`
|
||||
// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
// Check if two terms are identical. If not...
|
||||
(Equal a b dep) = (Equal.minor (Identical a b dep) a b dep)
|
||||
(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)))
|
||||
|
||||
// Check if they're identical after a minor weak reduction. If not...
|
||||
(Equal.minor 0 a b dep) = (Equal.major (Identical (Reduce 0 a) (Reduce 0 b) dep) a b dep)
|
||||
(Equal.minor 1 a b dep) = 1
|
||||
(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
|
||||
|
||||
// Check if they're identical after a major weak reduction. If not...
|
||||
(Equal.major 0 a b dep) = (Equal.enter (Identical (Reduce 1 a) (Reduce 1 b) dep) a b dep)
|
||||
(Equal.major 1 a b dep) = 1
|
||||
|
||||
// Check if they become identical after reducing fields.
|
||||
(Equal.enter 0 a b dep) = (Comparer λaλbλdep(Equal a b dep) (Reduce 0 a) (Reduce 0 b) dep)
|
||||
(Equal.enter 1 a b dep) = 1
|
||||
|
||||
// Checks if two terms are identical, without reductions.
|
||||
(Identical a b dep) = (Comparer λaλbλdep(Identical a b dep) a b dep)
|
||||
|
||||
// Generic comparer.
|
||||
(Comparer rec (All a.nam a.inp a.bod) (All b.nam b.inp b.bod) dep) = (& (rec a.inp b.inp dep) (rec (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep)))
|
||||
(Comparer rec (Lam a.nam a.bod) (Lam b.nam b.bod) dep) = (rec (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep))
|
||||
(Comparer rec (App a.fun a.arg) (App b.fun b.arg) dep) = (& (rec a.fun b.fun dep) (rec a.arg b.arg dep))
|
||||
(Comparer rec (Slf a.nam a.bod) (Slf b.nam b.bod) dep) = (rec (a.bod (Var a.nam dep)) (b.bod (Var b.nam dep)) (+ 1 dep))
|
||||
(Comparer rec (Ins a.val) b dep) = (rec a.val b dep)
|
||||
(Comparer rec a (Ins b.val) dep) = (rec a b.val dep)
|
||||
(Comparer rec (Ref a.nam a.val) (Ref b.nam b.val) dep) = (Same a.nam b.nam)
|
||||
(Comparer rec (Let a.nam a.val a.bod) b dep) = (rec (a.bod a.val) b dep)
|
||||
(Comparer rec a (Let b.nam b.val b.bod) dep) = (rec a (b.bod b.val) dep)
|
||||
(Comparer rec Set Set dep) = 1
|
||||
(Comparer rec (Var a.nam a.idx) (Var b.nam b.idx) dep) = (== a.idx b.idx)
|
||||
(Comparer rec (Ann a.val a.typ) b dep) = (rec a.val b dep)
|
||||
(Comparer rec a (Ann b.val b.typ) dep) = (rec a b.val dep)
|
||||
(Comparer rec (Hol a.nam a.ctx) b dep) = (Debug dep ["Found: ?" a.nam " = " (Show (Normal 0 b dep) dep)] 1)
|
||||
(Comparer rec a (Hol b.nam b.ctx) dep) = (Debug dep ["Found: ?" b.nam " = " (Show (Normal 0 a dep) dep)] 1)
|
||||
(Comparer rec (Hol a.nam a.ctx) (Hol b.nam b.ctx) dep) = (Same a.nam b.nam)
|
||||
(Comparer rec U60 U60 dep) = 1
|
||||
(Comparer rec (Num a.val) (Num b.val) dep) = (== a.val b.val)
|
||||
(Comparer rec (Op2 a.opr a.fst a.snd) (Op2 b.opr b.fst b.snd) dep) = (& (rec a.fst b.fst dep) (rec a.snd b.snd dep))
|
||||
(Comparer rec (Mat a.nam a.x a.z a.s a.p) (Mat b.nam b.x b.z b.s b.p) dep) = (& (rec a.x b.x dep) (& (rec a.z b.z dep) (& (rec (a.s (Var (String.concat a.nam "-1") dep)) (b.s (Var (String.concat b.nam "-1") dep)) dep) (rec (a.p (Var a.nam dep)) (b.p (Var b.nam dep)) dep))))
|
||||
(Comparer rec (Txt a.txt) (Txt b.txt) dep) = (Same a.txt b.txt)
|
||||
(Comparer rec (Src a.src a.val) b dep) = (Comparer rec a.val b dep)
|
||||
(Comparer rec a (Src b.src b.val) dep) = (Comparer rec a b.val dep)
|
||||
(Comparer rec a b dep) = 0
|
||||
//(Comparer rec a b dep) = (HVM.log (NOP (Show a dep) (Show b dep)) 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
|
||||
|
||||
// Type-Checking
|
||||
// -------------
|
||||
@ -235,8 +243,8 @@
|
||||
(IfAll (All nam inp bod) yep nop) = (yep nam inp bod)
|
||||
(IfAll other yep nop) = nop
|
||||
|
||||
(IfSlf (Slf nam bod) yep nop) = (yep nam bod)
|
||||
(IfSlf other yep nop) = nop
|
||||
(IfSlf (Slf nam typ bod) yep nop) = (yep nam typ bod)
|
||||
(IfSlf other yep nop) = nop
|
||||
|
||||
//(Infer term dep) = (Debug dep ["Infer: " (Show term dep)] (Infer.match term dep))
|
||||
(Infer term dep) = (Infer.match term dep)
|
||||
@ -246,10 +254,10 @@
|
||||
(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 ["Error: NonFunLam " (Show (Lam nam bod) dep)] (None))
|
||||
(Debug dep ["NON_FUNCTION_LAMBDA" NewLine "- detected: " (Show (Lam nam bod) dep)] (None))
|
||||
(Infer.match (App fun arg) dep) =
|
||||
(Maybe.bind (Infer fun dep) λfun_typ
|
||||
((IfAll (Reduce 1 fun_typ)
|
||||
((IfAll (Reduce 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)))
|
||||
@ -258,13 +266,13 @@
|
||||
fun arg))
|
||||
(Infer.match (Ann val typ) dep) =
|
||||
(Maybe.pure typ)
|
||||
(Infer.match (Slf nam bod) dep) =
|
||||
(Maybe.bind (Check 0 (bod (Ann (Var nam dep) (Slf nam bod))) Set (+ dep 1)) λslf
|
||||
(Infer.match (Slf nam typ bod) dep) =
|
||||
(Maybe.bind (Check 0 (bod (Ann (Var nam dep) typ)) Set (+ dep 1)) λslf
|
||||
(Maybe.pure Set))
|
||||
(Infer.match (Ins val) dep) =
|
||||
(Maybe.bind (Infer val dep) λval_typ
|
||||
((IfSlf (Reduce 1 val_typ)
|
||||
λval_nam λval_typ.bod λval (Maybe.pure (val_typ.bod (Ins val)))
|
||||
((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))
|
||||
(Infer.match (Ref nam val) dep) =
|
||||
@ -296,11 +304,11 @@
|
||||
(Infer.match (Src src val) dep) =
|
||||
(Infer.match val dep)
|
||||
|
||||
//(Check term type dep) = (Debug dep ["Check: " (Show term dep) " :: " (Show type dep)] (Check.match 0 term type dep))
|
||||
//(Check src term type dep) = (Debug dep ["Check: " (Show term dep) " :: " (Show type dep) " ~> " (Show (Reduce 2 type) dep)] (Check.match src term type dep))
|
||||
(Check src term type dep) = (Check.match src term type dep)
|
||||
|
||||
(Check.match src (Lam term.nam term.bod) type dep) =
|
||||
((IfAll (Reduce 1 type)
|
||||
((IfAll (Reduce 2 type)
|
||||
λtype.nam λtype.inp λtype.bod λterm.bod
|
||||
let ann = (Ann (Var term.nam dep) type.inp)
|
||||
let term = (term.bod ann)
|
||||
@ -310,8 +318,8 @@
|
||||
(Infer (Lam term.nam term.bod) dep))
|
||||
term.bod)
|
||||
(Check.match src (Ins term.val) type dep) =
|
||||
((IfSlf (Reduce 1 type)
|
||||
λtype.nam λtype.bod λterm.val (Check 0 term.val (type.bod (Ins term.val)) 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)
|
||||
(Check.match src (Let term.nam term.val term.bod) type dep) =
|
||||
@ -352,7 +360,7 @@
|
||||
(Show (Lam nam bod) dep) = (String.join ["λ" nam " " (Show (bod (Var nam dep)) (+ dep 1))])
|
||||
(Show (App fun arg) dep) = (String.join ["(" (Show.unwrap (Show fun dep)) " " (Show arg dep) ")"])
|
||||
(Show (Ann val typ) dep) = (String.join ["{" (Show val dep) ": " (Show typ dep) "}"])
|
||||
(Show (Slf nam bod) dep) = (String.join ["$" nam " " (Show (bod (Var nam dep)) (+ dep 1))])
|
||||
(Show (Slf nam typ bod) dep) = (String.join ["$(" nam ": " (Show typ dep) ") " (Show (bod (Var nam dep)) (+ dep 1))])
|
||||
(Show (Ins val) dep) = (String.join ["~" (Show val dep)])
|
||||
(Show (Ref nam val) dep) = nam
|
||||
(Show (Let nam val bod) dep) = (String.join ["let " nam " = " (Show val dep) "; " (Show (bod (Var nam dep)) (+ dep 1))])
|
||||
@ -411,7 +419,7 @@ Compile.primitives = [
|
||||
(Compile (Lam nam bod)) = λx(Compile (bod (Var "" x)))
|
||||
(Compile (App fun arg)) = ((Compile fun) (Compile arg))
|
||||
(Compile (Ann val typ)) = (Compile val)
|
||||
(Compile (Slf nam bod)) = 0
|
||||
(Compile (Slf nam typ bod)) = 0
|
||||
(Compile (Ins val)) = (Compile val)
|
||||
(Compile (Ref nam val)) = (Compile.ref Compile.primitives nam val)
|
||||
(Compile (Let nam val bod)) = (Compile (bod val))
|
||||
|
||||
22
src/main.rs
22
src/main.rs
@ -25,7 +25,7 @@ enum Term {
|
||||
Lam { nam: String, bod: Box<Term> },
|
||||
App { fun: Box<Term>, arg: Box<Term> },
|
||||
Ann { val: Box<Term>, typ: Box<Term> },
|
||||
Slf { nam: String, bod: Box<Term> },
|
||||
Slf { nam: String, typ: Box<Term>, bod: Box<Term> },
|
||||
Ins { val: Box<Term> },
|
||||
Set,
|
||||
U60,
|
||||
@ -129,7 +129,7 @@ impl Term {
|
||||
Term::Lam { nam, bod } => format!("λ{} {}", nam, bod.show()),
|
||||
Term::App { fun, arg } => format!("({} {})", fun.show(), arg.show()),
|
||||
Term::Ann { val, typ } => format!("{{{}: {}}}", val.show(), typ.show()),
|
||||
Term::Slf { nam, bod } => format!("${} {}", nam, bod.show()),
|
||||
Term::Slf { nam, typ, bod } => format!("$({}: {}) {}", nam, typ.show(), bod.show()),
|
||||
Term::Ins { val } => format!("~{}", val.show()),
|
||||
Term::Set => "*".to_string(),
|
||||
Term::U60 => "#U60".to_string(),
|
||||
@ -153,7 +153,7 @@ impl Term {
|
||||
Term::Lam { nam, bod } => format!("(Lam \"{}\" λ{} {})", nam, binder(nam), bod.to_hvm1(cons(&env, nam.clone()))),
|
||||
Term::App { fun, arg } => format!("(App {} {})", fun.to_hvm1(env.clone()), arg.to_hvm1(env.clone())),
|
||||
Term::Ann { val, typ } => format!("(Ann {} {})", val.to_hvm1(env.clone()), typ.to_hvm1(env.clone())),
|
||||
Term::Slf { nam, bod } => format!("(Slf \"{}\" λ{} {})", nam, binder(nam), bod.to_hvm1(cons(&env, nam.clone()))),
|
||||
Term::Slf { nam, typ, bod } => format!("(Slf \"{}\" {} λ{} {})", nam, typ.to_hvm1(env.clone()), binder(nam), bod.to_hvm1(cons(&env, nam.clone()))),
|
||||
Term::Ins { val } => format!("(Ins {})", val.to_hvm1(env.clone())),
|
||||
Term::Set => "(Set)".to_string(),
|
||||
Term::U60 => "(U60)".to_string(),
|
||||
@ -185,7 +185,8 @@ impl Term {
|
||||
val.get_free_vars(env.clone(), free);
|
||||
typ.get_free_vars(env.clone(), free);
|
||||
},
|
||||
Term::Slf { nam, bod } => {
|
||||
Term::Slf { nam, typ, bod } => {
|
||||
typ.get_free_vars(env.clone(), free);
|
||||
bod.get_free_vars(cons(&env, nam.clone()), free);
|
||||
},
|
||||
Term::Ins { val } => {
|
||||
@ -313,11 +314,15 @@ impl<'i> KindParser<'i> {
|
||||
Some('$') => {
|
||||
let ini = *self.index() as u64;
|
||||
self.consume("$")?;
|
||||
self.consume("(")?;
|
||||
let nam = self.parse_name()?;
|
||||
self.consume(":")?;
|
||||
let typ = Box::new(self.parse_term(fid)?);
|
||||
self.consume(")")?;
|
||||
let bod = Box::new(self.parse_term(fid)?);
|
||||
let end = *self.index() as u64;
|
||||
let src = new_src(fid, ini, end);
|
||||
Ok(Term::Src { src, val: Box::new(Term::Slf { nam, bod }) })
|
||||
Ok(Term::Src { src, val: Box::new(Term::Slf { nam, typ, bod }) })
|
||||
}
|
||||
Some('~') => {
|
||||
let ini = *self.index() as u64;
|
||||
@ -429,6 +434,7 @@ impl<'i> KindParser<'i> {
|
||||
}
|
||||
|
||||
fn parse_def(&mut self, fid: u64) -> Result<(String, Term), String> {
|
||||
self.skip_trivia();
|
||||
let nam = self.parse_name()?;
|
||||
self.skip_trivia();
|
||||
if self.peek_one() == Some(':') {
|
||||
@ -492,8 +498,8 @@ impl Book {
|
||||
//println!("... parsing: {}", name);
|
||||
let defs = KindParser::new(&text).parse_book(fid)?;
|
||||
//println!("... parsed: {}", name);
|
||||
for (def_name, def_term) in &defs.defs {
|
||||
book.defs.insert(def_name.clone(), def_term.clone());
|
||||
for (def_name, def_value) in &defs.defs {
|
||||
book.defs.insert(def_name.clone(), def_value.clone());
|
||||
}
|
||||
//println!("laoding deps for: {}", name);
|
||||
for (_, def_term) in defs.defs.into_iter() {
|
||||
@ -509,7 +515,7 @@ impl Book {
|
||||
}
|
||||
let mut book = Book::new();
|
||||
load_go(name, &mut book)?;
|
||||
load_go("String", &mut book)?;
|
||||
//load_go("String", &mut book)?;
|
||||
//println!("DONE!");
|
||||
Ok(book)
|
||||
}
|
||||
|
||||
Loading…
Reference in New Issue
Block a user