From bf65d89f09e21e7f56339ee9e3b28a8a8df0f27e Mon Sep 17 00:00:00 2001 From: LunaAmora Date: Mon, 18 Mar 2024 11:10:40 -0300 Subject: [PATCH 1/4] Update kind2 file and compilation --- src/book/compile.rs | 2 +- src/kind2.hvm2 | 47 +++++++++++++++++++++++++++++++++++---------- src/main.rs | 1 + src/term/compile.rs | 4 ++-- 4 files changed, 41 insertions(+), 13 deletions(-) diff --git a/src/book/compile.rs b/src/book/compile.rs index eb4e8e17..91acb788 100644 --- a/src/book/compile.rs +++ b/src/book/compile.rs @@ -24,7 +24,7 @@ impl Book { let mut meta = 0; for (name, term) in &self.defs { let expr = term.to_hvm2_checker(im::Vector::new(), &mut meta); - code.push_str(&format!("Book.{} = (Ref \"{}\" {})\n", name, name, expr)); + code.push_str(&format!("Book.{} = (Ref \"{}\" {})\n", name.replace("/", "."), name, expr)); } code } diff --git a/src/kind2.hvm2 b/src/kind2.hvm2 index c42f8e95..1ebe15af 100644 --- a/src/kind2.hvm2 +++ b/src/kind2.hvm2 @@ -78,6 +78,10 @@ if n then else = then and True b = b and False _ = False +or True b = True +or a True = True +or _ _ = False + not True = False not False = True @@ -404,7 +408,7 @@ termSimilar (All aNam aInp aBod) (All bNam bInp bBod) dep = termSimilar (Lam aNam aBod) (Lam bNam bBod) dep = (termEqual (aBod (Var aNam dep)) (bBod (Var bNam dep)) (+ dep 1)) termSimilar (App aFun aArg) (App bFun bArg) dep = - (envBind (termEqual aFun bFun dep) λeFun + (envBind (termSimilar aFun bFun dep) λeFun (envBind (termEqual aArg bArg dep) λeArg (envPure (and eFun eArg)))) termSimilar (Slf aNam aTyp aBod) (Slf bNam bTyp bBod) dep = @@ -423,7 +427,7 @@ termSimilar (Swi aNam aX aZ aS aP) (Swi bNam bX bZ bS bP) dep = (envBind (termEqual (aS (Var (stringConcat aNam "-1") dep)) (bS (Var (stringConcat bNam "-1") dep)) dep) λeS (envBind (termEqual (aP (Var aNam dep)) (bP (Var bNam dep)) dep) λeP (envPure (and (and (and eX eZ) eS) eP)))))) -termSimilar a b dep = (envPure False) +termSimilar a b dep = (termIdentical a b dep) // termIdentical :: Term -> Term -> U60 -> Env Bool termIdentical a b dep = (termIdenticalGo a b dep) @@ -515,8 +519,7 @@ termIdenticalGo a b dep = // ?X = λx λy λz ... K // In this implementation, checking condition `2` is not necessary, because we // subst holes directly where they occur (rather than on top-level definitions), -// so, it is impossible for unbound variables to appear. We also don't check for -// condition 3, and just allow recursive solutions. +// so, it is impossible for unbound variables to appear. // If possible, solves a `(?X x y z ...) = K` problem, generating a subst. // termUnify :: U60 -> [Term] -> Term -> U60 -> Env Bool @@ -524,12 +527,16 @@ termUnify uid spn b dep = (envBind envGetFill λfill let unsolved = (not (mapHas (key uid) fill)) let solvable = (termUnifyValid fill spn []) - (If (and unsolved solvable) + let no_loops = (not (termUnifyIsRec fill uid b dep)) + (If (and (and unsolved solvable) no_loops) let solution = (termUnifySolve fill uid spn b) // (trace (stringJoin ["solve: ", (u60Show uid), " ", (termShow solution dep)]) (envBind (envFill uid solution) λ_ (envPure True)) - (envPure False))) + (envPure match b { + (Met bUid bSpn): (envPure (eq uid bUid)) + other : (envPure False) + }))) // Checks if an problem is solveable by pattern unification. // termUnifyValid :: Map Term -> [Term] -> [U60] -> Bool @@ -547,6 +554,26 @@ termUnifySolve fill uid (List.cons x spn) b = match (termReduce fill 0 x) { otherwise : (trace "unreachable" Unreachable) } +// Checks if a hole uid occurs recursively inside a term +// termUnifyIsRec :: Map Term -> Int -> Term -> Int -> Bool +termUnifyIsRec fill uid (All nam inp bod) dep = (or (termUnifyIsRec fill uid inp dep) (termUnifyIsRec fill uid (bod (Var nam dep)) (+ dep 1))) +termUnifyIsRec fill uid (Lam nam bod) dep = (or (termUnifyIsRec fill uid (bod (Var nam dep)) (+ dep 1))) +termUnifyIsRec fill uid (App fun arg) dep = (or (termUnifyIsRec fill uid fun dep) (termUnifyIsRec fill uid arg dep)) +termUnifyIsRec fill uid (Ann chk val typ) dep = (or (termUnifyIsRec fill uid val dep) (termUnifyIsRec fill uid typ dep)) +termUnifyIsRec fill uid (Slf nam typ bod) dep = (or (termUnifyIsRec fill uid typ dep) (termUnifyIsRec fill uid (bod (Var nam dep)) (+ dep 1))) +termUnifyIsRec fill uid (Ins val) dep = (or (termUnifyIsRec fill uid val dep)) +termUnifyIsRec fill uid (Let nam val bod) dep = (or (termUnifyIsRec fill uid val dep) (termUnifyIsRec fill uid (bod (Var nam dep)) (+ dep 1))) +termUnifyIsRec fill uid (Use nam val bod) dep = (or (termUnifyIsRec fill uid val dep) (termUnifyIsRec fill uid (bod (Var nam dep)) (+ dep 1))) +termUnifyIsRec fill uid (Hol nam ctx) dep = False +termUnifyIsRec fill uid (Op2 opr fst snd) dep = (or (termUnifyIsRec fill uid fst dep) (termUnifyIsRec fill uid snd dep)) +termUnifyIsRec fill uid (Swi nam x z s p) dep = (or (termUnifyIsRec fill uid x dep) (or (termUnifyIsRec fill uid z dep) (or (termUnifyIsRec fill uid (s (Var (stringConcat nam "-1") dep)) (+ dep 1)) (termUnifyIsRec fill uid (p (Var nam dep)) dep)))) +termUnifyIsRec fill uid (Src src val) dep = (termUnifyIsRec fill uid val dep) +termUnifyIsRec fill uid (Met bUid bSpn) dep = match (termReduceMet fill 2 bUid bSpn) { + (Met bUid bSpn): (eq uid bUid) + term : (termUnifyIsRec fill uid term dep) +} +termUnifyIsRec fill uid _ dep = False + // Substitutes a Bruijn level variable by a `neo` value in `term`. // termUnifySubst :: U60 -> Term -> Term -> Term // termUnifySubst lvl neo term = term @@ -779,22 +806,22 @@ termShow (Use nam val bod) dep = let bod_ = (termShow (bod (Var nam dep)) (+ dep 1)) (stringJoin ["use ", nam_, " = ", val_, "; ", bod_]) termShow Set dep = "*" -termShow U60 dep = "#U60" +termShow U60 dep = "U60" termShow (Num val) dep = let val_ = (u60Show val) - (stringJoin ["#", val_]) + (stringJoin [val_]) termShow (Op2 opr fst snd) dep = let opr_ = (operShow opr) let fst_ = (termShow fst dep) let snd_ = (termShow snd dep) - (stringJoin ["#(", opr_, " ", fst_, " ", snd_, ")"]) + (stringJoin ["(", opr_, " ", fst_, " ", snd_, ")"]) termShow (Swi nam x z s p) dep = let nam_ = nam let x_ = (termShow x dep) let z_ = (termShow z dep) let s_ = (termShow (s (Var (stringConcat nam "-1") dep)) (+ dep 1)) let p_ = (termShow (p (Var nam dep)) dep) - (stringJoin ["#match ", nam_, " = ", x_, " { #0: ", z_, " #+: ", s_, " }: ", p_]) + (stringJoin ["switch ", nam_, " = ", x_, " { 0: ", z_, " _: ", s_, " }: ", p_]) termShow (Txt txt) dep = (stringJoin [quote, txt, quote]) termShow (Nat val) dep = (u60Show val) termShow (Hol nam ctx) dep = (stringJoin ["?", nam]) diff --git a/src/main.rs b/src/main.rs index 8595e9e5..16b75c58 100644 --- a/src/main.rs +++ b/src/main.rs @@ -141,6 +141,7 @@ fn compare_runtimes() { let mut paths: Vec<_> = fs::read_dir(&book_dir) .expect("failed to read book directory") .map(|r| r.expect("failed to read entry").path()) + .filter_map(|r| r.extension().is_some_and(|e| e == "kind2").then_some(r)) .collect(); paths.sort(); diff --git a/src/term/compile.rs b/src/term/compile.rs index 0eaa2c8d..b3250020 100644 --- a/src/term/compile.rs +++ b/src/term/compile.rs @@ -66,7 +66,7 @@ impl Term { pub fn to_hvm2_checker(&self, env: im::Vector, met: &mut usize) -> String { fn binder(name: &str) -> String { - format!("x{}", name.replace("-", "._.")) + format!("x{}", name.replace("-", "._.").replace("/", ".")) } match self { Term::All { era: _, nam, inp, bod } => { @@ -137,7 +137,7 @@ impl Term { if env.contains(nam) { format!("{}", binder(nam)) } else { - format!("(Book.{})", nam) + format!("(Book.{})", nam.replace("/", ".")) } } Term::Src { src, val } => { From c2200dd30a89c768ec6e24cc820ed0d3349a71ae Mon Sep 17 00:00:00 2001 From: LunaAmora Date: Mon, 18 Mar 2024 16:54:01 -0300 Subject: [PATCH 2/4] Fix generated name on generate_check_hvm2 --- src/main.rs | 26 ++++++++++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) diff --git a/src/main.rs b/src/main.rs index 16b75c58..6c3384d9 100644 --- a/src/main.rs +++ b/src/main.rs @@ -42,8 +42,8 @@ fn generate_check_hvm2(book: &Book, command: &str, arg: &str) -> String { let kind_hvm2 = include_str!("./kind2.hvm2"); let book_hvm2 = book.to_hvm2_checker(); let main_hvm2 = match command { - "check" => format!("main = (apiCheck Book.{})\n", arg), - "run" => format!("main = (apiNormal Book.{})\n", arg), + "check" => format!("main = (apiCheck Book.{})\n", arg.replace("/", ".")), + "run" => format!("main = (apiNormal Book.{})\n", arg.replace("/", ".")), _ => panic!("invalid command"), }; format!("{}\n{}\n{}", kind_hvm2, book_hvm2, main_hvm2) @@ -136,6 +136,28 @@ fn compile(name: &str) { println!("{code}"); } +// fn read_dir_rec(path: &PathBuf) -> Vec { +// fn visit_dirs(dir: &PathBuf, cb: &mut impl FnMut(PathBuf)) { +// if dir.is_dir() { +// for entry in fs::read_dir(dir).expect("failed to read book directory") { +// let entry = entry.expect("failed to read entry"); +// let path = entry.path(); +// if path.is_dir() { +// visit_dirs(&path, cb); +// } else { +// cb(path); +// } +// } +// } +// } + +// let mut paths = Vec::new(); + +// visit_dirs(&path, &mut |a| paths.push(a)); +// paths.sort(); +// paths +// } + fn compare_runtimes() { let book_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("book"); let mut paths: Vec<_> = fs::read_dir(&book_dir) From 3c89c73d2f11e87e08d6b13884f0dc40a7dfb23f Mon Sep 17 00:00:00 2001 From: LunaAmora Date: Mon, 18 Mar 2024 16:59:44 -0300 Subject: [PATCH 3/4] Remove commented fn --- src/main.rs | 22 ---------------------- 1 file changed, 22 deletions(-) diff --git a/src/main.rs b/src/main.rs index 6c3384d9..d4a1cb73 100644 --- a/src/main.rs +++ b/src/main.rs @@ -136,28 +136,6 @@ fn compile(name: &str) { println!("{code}"); } -// fn read_dir_rec(path: &PathBuf) -> Vec { -// fn visit_dirs(dir: &PathBuf, cb: &mut impl FnMut(PathBuf)) { -// if dir.is_dir() { -// for entry in fs::read_dir(dir).expect("failed to read book directory") { -// let entry = entry.expect("failed to read entry"); -// let path = entry.path(); -// if path.is_dir() { -// visit_dirs(&path, cb); -// } else { -// cb(path); -// } -// } -// } -// } - -// let mut paths = Vec::new(); - -// visit_dirs(&path, &mut |a| paths.push(a)); -// paths.sort(); -// paths -// } - fn compare_runtimes() { let book_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("book"); let mut paths: Vec<_> = fs::read_dir(&book_dir) From 5008491fe92175647d9a0d1966cc21913609f84a Mon Sep 17 00:00:00 2001 From: LunaAmora Date: Mon, 18 Mar 2024 17:20:39 -0300 Subject: [PATCH 4/4] Add unification polishments to kind2.hvm2 --- src/kind2.hvm2 | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/kind2.hvm2 b/src/kind2.hvm2 index 1ebe15af..3534f221 100644 --- a/src/kind2.hvm2 +++ b/src/kind2.hvm2 @@ -465,12 +465,12 @@ termIdenticalGo a (Ann chk bVal bTyp) dep = (termIdentical a bVal dep) // termIdenticalGo (Met aUid aSpn) (Met bUid bSpn) dep = // envPure (eq aUid bUid) -termIdenticalGo (Met aUid aSpn) b dep = - // traceShow (stringJoin ["unify: ", (u60Show aUid), " x=", (termShow (Met aUid aSpn) dep), " t=", (termShow b dep)]) - (termUnify aUid aSpn b dep) termIdenticalGo a (Met bUid bSpn) dep = // traceShow (stringJoin ["unify: ", (u60Show bUid), " x=", (termShow (Met bUid bSpn) dep), " t=", (termShow a dep)]) (termUnify bUid bSpn a dep) +termIdenticalGo (Met aUid aSpn) b dep = + // traceShow (stringJoin ["unify: ", (u60Show aUid), " x=", (termShow (Met aUid aSpn) dep), " t=", (termShow b dep)]) + (termUnify aUid aSpn b dep) termIdenticalGo (Hol aNam aCtx) b dep = (envPure True) termIdenticalGo a (Hol bNam bCtx) dep =