From 97015e9390ae97b9ec4500466257dff7501c489e Mon Sep 17 00:00:00 2001 From: Victor Taelin Date: Thu, 7 Mar 2024 18:08:04 -0300 Subject: [PATCH] missing files? --- .gitignore | 1 + book/Bool.not.kind2 | 6 +- book/CNat.kind2 | 7 ++ book/CNat.succ.kind2 | 3 + book/CNat.zero.kind2 | 3 + src/book/compile.rs | 34 +++++++ src/kind2.hs | 44 ++++----- src/term/compile.rs | 209 +++++++++++++++++++++++++++++++++++++++++++ 8 files changed, 282 insertions(+), 25 deletions(-) create mode 100644 book/CNat.kind2 create mode 100644 book/CNat.succ.kind2 create mode 100644 book/CNat.zero.kind2 create mode 100644 src/book/compile.rs create mode 100644 src/term/compile.rs diff --git a/.gitignore b/.gitignore index 662ddc10..c916390c 100644 --- a/.gitignore +++ b/.gitignore @@ -5,3 +5,4 @@ plans.txt .check.hvm1 demo/ .fill.tmp +.check.hs diff --git a/book/Bool.not.kind2 b/book/Bool.not.kind2 index 8ead8ed9..5e0c81a7 100644 --- a/book/Bool.not.kind2 +++ b/book/Bool.not.kind2 @@ -1,7 +1,7 @@ Bool.not : ∀(x: Bool) Bool = λx - let P = λx Bool - let true = Bool.false - let false = Bool.true + let P = {λx Bool:_} + let true = {Bool.false:_} + let false = {Nat.zero:_} (~x P true false) \ No newline at end of file diff --git a/book/CNat.kind2 b/book/CNat.kind2 new file mode 100644 index 00000000..f0f61f44 --- /dev/null +++ b/book/CNat.kind2 @@ -0,0 +1,7 @@ +CNat +: * += $(self: CNat) + ∀(P: ∀(x: CNat) *) + ∀(s: ∀(i: (P self)) (P (CNat.succ i))) + ∀(z: (P CNat.zero)) + (P self) \ No newline at end of file diff --git a/book/CNat.succ.kind2 b/book/CNat.succ.kind2 new file mode 100644 index 00000000..1a9a7559 --- /dev/null +++ b/book/CNat.succ.kind2 @@ -0,0 +1,3 @@ +CNat.succ +: ∀(n: CNat) CNat += λn ~λP λs λz (s (n P s z)) \ No newline at end of file diff --git a/book/CNat.zero.kind2 b/book/CNat.zero.kind2 new file mode 100644 index 00000000..3bc1f7ff --- /dev/null +++ b/book/CNat.zero.kind2 @@ -0,0 +1,3 @@ +CNat.zero +: CNat += ~λP λs λz z \ No newline at end of file diff --git a/src/book/compile.rs b/src/book/compile.rs new file mode 100644 index 00000000..6375d573 --- /dev/null +++ b/src/book/compile.rs @@ -0,0 +1,34 @@ +use crate::{*}; + +use std::collections::BTreeMap; +use std::collections::BTreeSet; + +impl Book { + + pub fn to_hvm1(&self) -> String { + todo!() + //let mut used = BTreeSet::new(); + //let mut code = String::new(); + //for (name, term) in &self.defs { + //let metas = term.count_metas(); + //let mut lams = String::new(); + //for i in 0 .. term.count_metas() { + //lams = format!("{} λ_{}", lams, i); + //} + //let subs = (0 .. metas).map(|h| format!("(Pair \"{}\" None)", h)).collect::>().join(","); + //code.push_str(&format!("Book.{} = (Ref \"{}\" [{}] {}{})\n", name, name, subs, lams, term.to_hvm1(im::Vector::new(), &mut 0))); + //used.insert(name.clone()); + //} + //code + } + + pub fn to_hs(&self) -> String { + let mut code = String::new(); + for (name, term) in &self.defs { + let expr = term.to_hs(im::Vector::new(), &mut 0); + code.push_str(&format!("{} = (Ref \"{}\" {})\n", Term::to_hs_name(name), name, expr)); + } + code + } + +} diff --git a/src/kind2.hs b/src/kind2.hs index 649319f8..7ddae45e 100644 --- a/src/kind2.hs +++ b/src/kind2.hs @@ -25,7 +25,7 @@ data Term = All String Term (Term -> Term) | Lam String (Term -> Term) | App Term Term - | Ann Term Term + | Ann Bool Term Term | Slf String Term (Term -> Term) | Ins Term | Ref String Term @@ -231,7 +231,7 @@ instance Monad Env where termReduce :: Map Term -> Int -> Term -> Term termReduce fill lv (App fun arg) = termReduceApp fill lv (termReduce fill lv fun) arg -termReduce fill lv (Ann val typ) = termReduce fill lv val +termReduce fill lv (Ann chk val typ) = termReduce fill lv val termReduce fill lv (Ins val) = termReduce fill lv val termReduce fill lv (Ref nam val) = termReduceRef fill lv nam (termReduce fill lv val) termReduce fill lv (Let nam val bod) = termReduce fill lv (bod val) @@ -307,7 +307,7 @@ termNormal fill lv term dep = termNormalGo fill lv (termReduce fill lv term) dep termNormalGo fill lv (All nam inp bod) dep = All nam (termNormal fill lv inp dep) (\x -> termNormal fill lv (bod (Var nam dep)) (dep + 1)) termNormalGo fill lv (Lam nam bod) dep = Lam nam (\x -> termNormal fill lv (bod (Var nam dep)) (dep + 1)) termNormalGo fill lv (App fun arg) dep = App (termNormal fill lv fun dep) (termNormal fill lv arg dep) - termNormalGo fill lv (Ann val typ) dep = Ann (termNormal fill lv val dep) (termNormal fill lv typ dep) + termNormalGo fill lv (Ann chk val typ) dep = Ann chk (termNormal fill lv val dep) (termNormal fill lv typ dep) termNormalGo fill lv (Slf nam typ bod) dep = Slf nam typ (\x -> termNormal fill lv (bod (Var nam dep)) (dep + 1)) termNormalGo fill lv (Ins val) dep = Ins (termNormal fill lv val dep) termNormalGo fill lv (Ref nam val) dep = Ref nam (termNormal fill lv val dep) @@ -398,9 +398,9 @@ termIdenticalGo a (Let bNam bVal bBod) dep = termIdentical a (bBod bVal) dep termIdenticalGo Set Set dep = envPure True -termIdenticalGo (Ann aVal aTyp) b dep = +termIdenticalGo (Ann chk aVal aTyp) b dep = termIdentical aVal b dep -termIdenticalGo a (Ann bVal bTyp) dep = +termIdenticalGo a (Ann chk bVal bTyp) dep = termIdentical a bVal dep -- termIdenticalGo (Met aUid aSpn) (Met bUid bSpn) dep = -- envPure (aUid == bUid) @@ -493,7 +493,7 @@ termUnifySubst :: Int -> Term -> Term -> Term termUnifySubst lvl neo (All nam inp bod) = All nam (termUnifySubst lvl neo inp) (\x -> termUnifySubst lvl neo (bod x)) termUnifySubst lvl neo (Lam nam bod) = Lam nam (\x -> termUnifySubst lvl neo (bod x)) termUnifySubst lvl neo (App fun arg) = App (termUnifySubst lvl neo fun) (termUnifySubst lvl neo arg) -termUnifySubst lvl neo (Ann val typ) = Ann (termUnifySubst lvl neo val) (termUnifySubst lvl neo typ) +termUnifySubst lvl neo (Ann chk val typ) = Ann chk (termUnifySubst lvl neo val) (termUnifySubst lvl neo typ) termUnifySubst lvl neo (Slf nam typ bod) = Slf nam (termUnifySubst lvl neo typ) (\x -> termUnifySubst lvl neo (bod x)) termUnifySubst lvl neo (Ins val) = Ins (termUnifySubst lvl neo val) termUnifySubst lvl neo (Ref nam val) = Ref nam (termUnifySubst lvl neo val) @@ -528,7 +528,7 @@ termInfer term dep = termInferGo :: Term -> Int -> Env Term termInferGo (All nam inp bod) dep = do envSusp (Check 0 inp Set dep) - envSusp (Check 0 (bod (Ann (Var nam dep) inp)) Set (dep + 1)) + envSusp (Check 0 (bod (Ann False (Var nam dep) inp)) Set (dep + 1)) return Set termInferGo (App fun arg) dep = do ftyp <- termInfer fun dep @@ -540,10 +540,10 @@ termInferGo (App fun arg) dep = do otherwise -> do envLog (Error 0 ftyp (Hol "function" []) (App fun arg) dep) envFail -termInferGo (Ann val typ) dep = do +termInferGo (Ann chk val typ) dep = do return typ termInferGo (Slf nam typ bod) dep = do - envSusp (Check 0 (bod (Ann (Var nam dep) typ)) Set (dep + 1)) + envSusp (Check 0 (bod (Ann False (Var nam dep) typ)) Set (dep + 1)) return Set termInferGo (Ins val) dep = do vtyp <- termInfer val dep @@ -570,9 +570,9 @@ termInferGo (Op2 opr fst snd) dep = do return U60 termInferGo (Mat nam x z s p) dep = do envSusp (Check 0 x U60 dep) - envSusp (Check 0 (p (Ann (Var nam dep) U60)) Set dep) + envSusp (Check 0 (p (Ann False (Var nam dep) U60)) Set dep) envSusp (Check 0 z (p (Num 0)) dep) - envSusp (Check 0 (s (Ann (Var (stringConcat nam "-1") dep) U60)) (p (Op2 ADD (Num 1) (Var (stringConcat nam "-1") dep))) (dep + 1)) + envSusp (Check 0 (s (Ann False (Var (stringConcat nam "-1") dep) U60)) (p (Op2 ADD (Num 1) (Var (stringConcat nam "-1") dep))) (dep + 1)) return (p x) termInferGo (Lam nam bod) dep = do envLog (Error 0 (Hol "untyped_term" []) (Hol "type_annotation" []) (Lam nam bod) dep) @@ -602,7 +602,7 @@ termCheckGo src (Lam termNam termBod) typx dep = do fill <- envGetFill case termReduce fill 2 typx of (All typeNam typeInp typeBod) -> do - let ann = Ann (Var termNam dep) typeInp + let ann = Ann False (Var termNam dep) typeInp let term = termBod ann let typx = typeBod ann termCheck 0 term typx (dep + 1) @@ -619,7 +619,7 @@ termCheckGo src (Ins termVal) typx dep = do return () termCheckGo src (Let termNam termVal termBod) typx dep = do termTyp <- termInfer termVal dep - termCheck 0 (termBod (Ann (Var termNam dep) termTyp)) typx dep + termCheck 0 (termBod (Ann False termVal termTyp)) typx dep termCheckGo src (Hol termNam termCtx) typx dep = do envLog (Found termNam typx termCtx dep) return () @@ -650,9 +650,9 @@ termCheckGo src term typx dep = do -- envPure () termCheckDef :: Term -> Env () -termCheckDef (Ref nam (Ann val typ)) = termCheck 0 val typ 0 >> return () -termCheckDef (Ref nam val) = termInfer val 0 >> return () -termCheckDef other = error "invalid top-level definition" +termCheckDef (Ref nam (Ann chk val typ)) = termCheck 0 val typ 0 >> return () +termCheckDef (Ref nam val) = termInfer val 0 >> return () +termCheckDef other = error "invalid top-level definition" -- Stringification -- --------------- @@ -671,7 +671,7 @@ termShow (App fun arg) dep = let fun' = termShow fun dep arg' = termShow arg dep in stringJoin ["(" , fun' , " " , arg' , ")"] -termShow (Ann val typ) dep = +termShow (Ann chk val typ) dep = let val' = termShow val dep typ' = termShow typ dep in stringJoin ["{" , val' , ": " , typ' , "}"] @@ -738,8 +738,8 @@ contextShow fill [] dep = "" contextShow fill (x:xs) dep = stringJoin [" " , contextShowAnn fill x dep , contextShow fill xs dep] contextShowAnn :: Map Term -> Term -> Int -> String -contextShowAnn fill (Ann val typ) dep = stringJoin ["{" , termShow (termNormal fill 0 val dep) dep , ": " , termShow (termNormal fill 0 typ dep) dep , "}"] -contextShowAnn fill term dep = termShow (termNormal fill 0 term dep) dep +contextShowAnn fill (Ann chk val typ) dep = stringJoin ["{" , termShow (termNormal fill 0 val dep) dep , ": " , termShow (termNormal fill 0 typ dep) dep , "}"] +contextShowAnn fill term dep = termShow (termNormal fill 0 term dep) dep infoShow :: Map Term -> Info -> String infoShow fill (Found name typ ctx dep) = @@ -747,8 +747,8 @@ infoShow fill (Found name typ ctx dep) = ctx' = stringTail (contextShow fill ctx dep) in stringJoin ["#found{", name, " ", typ', " [", ctx', "]}"] infoShow fill (Error src expected detected value dep) = - let det = termShow detected dep - exp = termShow expected dep + let det = termShow (termNormal fill 1 detected dep) dep + exp = termShow (termNormal fill 1 expected dep) dep val = termShow (termNormal fill 0 value dep) dep in stringJoin ["#error{", exp, " ", det, " ", val, " ", u60Show src, "}"] infoShow fill (Solve name term dep) = @@ -785,7 +785,7 @@ hvmPrint = undefined -- ---- xtest :: Term -xtest = Ref "test" $ Ann val typ where +xtest = Ref "test" $ Ann True val typ where typ = (All "P" Set $ \p -> (All "f" (All "x" p $ \x -> p) $ \f -> (All "x" p $ \x -> p))) val = (Lam "P" $ \p -> (Lam "f" $ \f -> (Lam "x" $ \x -> f))) diff --git a/src/term/compile.rs b/src/term/compile.rs new file mode 100644 index 00000000..97503684 --- /dev/null +++ b/src/term/compile.rs @@ -0,0 +1,209 @@ +use crate::{*}; + +impl Oper { + + pub fn to_ctr(&self) -> &'static str { + match self { + Oper::Add => "ADD", + Oper::Sub => "SUB", + Oper::Mul => "MUL", + Oper::Div => "DIV", + Oper::Mod => "MOD", + Oper::Eq => "EQ", + Oper::Ne => "NE", + Oper::Lt => "LT", + Oper::Gt => "GT", + Oper::Lte => "LTE", + Oper::Gte => "GTE", + Oper::And => "AND", + Oper::Or => "OR", + Oper::Xor => "XOR", + Oper::Lsh => "LSH", + Oper::Rsh => "RSH", + } + } + + pub fn to_hvm1(&self) -> &'static str { + self.to_ctr() + } + + pub fn to_hs(&self) -> &'static str { + self.to_ctr() + } + +} + +impl Term { + + pub fn to_hvm1(&self, _env: im::Vector, _met: &mut usize) -> String { + todo!() + //fn binder(name: &str) -> String { + //format!("x{}", name.replace("-", "._.")) + //} + //match self { + //Term::All { nam, inp, bod } => { + //let inp = inp.to_hvm1(env.clone(), met); + //let bod = bod.to_hvm1(cons(&env, nam.clone()), met); + //format!("(All \"{}\" {} λ{} {})", nam, inp, binder(nam), bod) + //}, + //Term::Lam { nam, bod } => { + //let bod = bod.to_hvm1(cons(&env, nam.clone()), met); + //format!("(Lam \"{}\" λ{} {})", nam, binder(nam), bod) + //}, + //Term::App { fun, arg } => { + //let fun = fun.to_hvm1(env.clone(), met); + //let arg = arg.to_hvm1(env.clone(), met); + //format!("(App {} {})", fun, arg) + //}, + //Term::Ann { val, typ } => { + //let val = val.to_hvm1(env.clone(), met); + //let typ = typ.to_hvm1(env.clone(), met); + //format!("(Ann {} {})", val, typ) + //}, + //Term::Slf { nam, typ, bod } => { + //let typ = typ.to_hvm1(env.clone(), met); + //let bod = bod.to_hvm1(cons(&env, nam.clone()), met); + //format!("(Slf \"{}\" {} λ{} {})", nam, typ, binder(nam), bod) + //}, + //Term::Ins { val } => { + //let val = val.to_hvm1(env.clone(), met); + //format!("(Ins {})", val) + //}, + //Term::Set => { + //"(Set)".to_string() + //}, + //Term::U60 => { + //"(U60)".to_string() + //}, + //Term::Num { val } => { + //format!("(Num {})", val) + //}, + //Term::Op2 { opr, fst, snd } => { + //let fst = fst.to_hvm1(env.clone(), met); + //let snd = snd.to_hvm1(env.clone(), met); + //format!("(Op2 {} {} {})", opr.to_hvm1(), fst, snd) + //}, + //Term::Mat { nam, x, z, s, p } => { + //let x = x.to_hvm1(env.clone(), met); + //let z = z.to_hvm1(env.clone(), met); + //let s = s.to_hvm1(cons(&env, format!("{}-1", nam)), met); + //let p = p.to_hvm1(cons(&env, nam.clone()), met); + //format!("(Mat \"{}\" {} {} λ{} {} λ{} {})", nam, x, z, binder(&format!("{}-1", nam)), s, binder(nam), p) + //}, + //Term::Txt { txt } => { + //format!("(Txt \"{}\")", txt) + //}, + //Term::Let { nam, val, bod } => { + //let val = val.to_hvm1(env.clone(), met); + //let bod = bod.to_hvm1(cons(&env, nam.clone()), met); + //format!("(Let \"{}\" {} λ{} {})", nam, val, binder(nam), bod) + //}, + //Term::Hol { nam } => { + //let env_str = env.iter().map(|n| binder(n)).collect::>().join(","); + //format!("(Hol \"{}\" [{}])", nam, env_str) + //}, + //Term::Met {} => { + //let n = *met; + //*met += 1; + //format!("(Met {})", n) + //}, + //Term::Var { nam } => { + //if env.contains(nam) { + //format!("{}", binder(nam)) + //} else { + //format!("(Book.{})", nam) + //} + //}, + //Term::Src { src, val } => { + //let val = val.to_hvm1(env, met); + //format!("(Src {} {})", src.to_u64(), val) + //}, + //} + } + + pub fn to_hs_name(name: &str) -> String { + format!("x{}", name.replace("-", "_").replace(".","_")) + } + + pub fn to_hs(&self, env: im::Vector, met: &mut usize) -> String { + match self { + Term::All { nam, inp, bod } => { + let inp = inp.to_hs(env.clone(), met); + let bod = bod.to_hs(cons(&env, nam.clone()), met); + format!("(All \"{}\" {} $ \\{} -> {})", nam, inp, Term::to_hs_name(nam), bod) + }, + Term::Lam { nam, bod } => { + let bod = bod.to_hs(cons(&env, nam.clone()), met); + format!("(Lam \"{}\" $ \\{} -> {})", nam, Term::to_hs_name(nam), bod) + }, + Term::App { fun, arg } => { + let fun = fun.to_hs(env.clone(), met); + let arg = arg.to_hs(env.clone(), met); + format!("(App {} {})", fun, arg) + }, + Term::Ann { val, typ } => { + let val = val.to_hs(env.clone(), met); + let typ = typ.to_hs(env.clone(), met); + format!("(Ann True {} {})", val, typ) + }, + Term::Slf { nam, typ, bod } => { + let typ = typ.to_hs(env.clone(), met); + let bod = bod.to_hs(cons(&env, nam.clone()), met); + format!("(Slf \"{}\" {} $ \\{} -> {})", nam, typ, Term::to_hs_name(nam), bod) + }, + Term::Ins { val } => { + let val = val.to_hs(env.clone(), met); + format!("(Ins {})", val) + }, + Term::Set => { + "(Set)".to_string() + }, + Term::U60 => { + "(U60)".to_string() + }, + Term::Num { val } => { + format!("(Num {})", val) + }, + Term::Op2 { opr, fst, snd } => { + let fst = fst.to_hs(env.clone(), met); + let snd = snd.to_hs(env.clone(), met); + format!("(Op2 {} {} {})", opr.to_hs(), fst, snd) + }, + Term::Mat { nam, x, z, s, p } => { + let x = x.to_hs(env.clone(), met); + let z = z.to_hs(env.clone(), met); + let s = s.to_hs(cons(&env, format!("{}-1", nam)), met); + let p = p.to_hs(cons(&env, nam.clone()), met); + format!("(Mat \"{}\" {} {} (\\{} -> {}) (\\{} -> {}))", nam, x, z, Term::to_hs_name(&format!("{}-1", nam)), s, Term::to_hs_name(nam), p) + }, + Term::Txt { txt } => { + format!("(Txt \"{}\")", txt.replace("\n", "\\n")) + }, + Term::Let { nam, val, bod } => { + let val = val.to_hs(env.clone(), met); + let bod = bod.to_hs(cons(&env, nam.clone()), met); + format!("(Let \"{}\" {} $ \\{} -> {})", nam, val, Term::to_hs_name(nam), bod) + }, + Term::Hol { nam } => { + let env_str = env.iter().map(|n| Term::to_hs_name(n)).collect::>().join(","); + format!("(Hol \"{}\" [{}])", nam, env_str) + }, + Term::Met {} => { + let uid = *met; + *met += 1; + format!("(Met {} [])", uid) + //format!("(Met {} [{}])", uid, env.iter().rev().map(|n| Term::to_hs_name(n)).collect::>().join(",")) + }, + Term::Var { nam } => { + format!("{}", Term::to_hs_name(nam)) + }, + Term::Src { src, val } => { + let val = val.to_hs(env, met); + format!("(Src {} {})", src.to_u64(), val) + }, + } + } + + + +}