HigherOrderCO/Kind
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind.git synced 2024-10-03 18:27:13 +03:00
Code Issues Packages Projects Releases Wiki Activity

parse _ in name, fix hole parser

Browse Source
This commit is contained in:
Victor Taelin 2024-06-22 23:37:35 -03:00
parent 314aaeee1c
commit c6779b7581
6 changed files with 31 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
book/test0.kind2
View File

@ -9,4 +9,4 @@ test0
∀(b: B)
A
= λA λB λaa λab λba λbb λa λb
(ba (ab (aa a)))
(ba (ab (aa (aa a))))

3
src/book/compile.rs
View File

@ -12,8 +12,9 @@ impl Book {
pub fn to_kindc(&self) -> String {
let mut code = String::new();
let mut meta = 0;
for (name, term) in &self.defs {
code.push_str(&format!("{} = {};\n", name, term.to_kindc(&mut 0)));
code.push_str(&format!("{} = {};\n", name, term.to_kindc(im::Vector::new(), &mut meta)));
}
code
}

9
src/kindc.hs
View File

@ -1086,7 +1086,12 @@ parseNat = do
parseHol = do
P.char '?'
nam <- parseName
return $ Hol nam []
ctx <- P.option [] $ do
P.char '['
terms <- P.sepBy parseTerm (P.char ',')
P.char ']'
return terms
return $ Hol nam ctx
parseMet = do
P.char '_'
@ -1103,7 +1108,7 @@ parseSrc = do
parseName :: P.Parsec String () String
parseName = do
head <- P.letter
tail <- P.many (P.alphaNum <|> P.char '/' <|> P.char '.')
tail <- P.many (P.alphaNum <|> P.char '/' <|> P.char '.' <|> P.char '_')
return (head : tail)
parseOper = P.choice

33
src/term/compile.rs
View File

@ -139,53 +139,58 @@ impl Term {
}
impl Term {
pub fn to_kindc(&self, met: &mut usize) -> String {
pub fn to_kindc(&self, env: im::Vector<String>, met: &mut usize) -> String {
match self {
Term::All { era: _, nam, inp, bod } => {
format!("∀({}: {}) {}", nam, inp.to_kindc(met), bod.to_kindc(met))
format!("∀({}: {}) {}", nam, inp.to_kindc(env.clone(), met), bod.to_kindc(cons(&env, nam.clone()), met))
},
Term::Lam { era: _, nam, bod } => {
format!("λ{} {}", nam, bod.to_kindc(met))
format!("λ{} {}", nam, bod.to_kindc(cons(&env, nam.clone()), met))
},
Term::App { era: _, fun, arg } => {
format!("({} {})", fun.to_kindc(met), arg.to_kindc(met))
format!("({} {})", fun.to_kindc(env.clone(), met), arg.to_kindc(env.clone(), met))
},
Term::Ann { chk, val, typ } => {
format!("{{{}:{} {}}}", val.to_kindc(met), if *chk { ":" } else { "" }, typ.to_kindc(met))
format!("{{{}:{} {}}}", val.to_kindc(env.clone(), met), if *chk { ":" } else { "" }, typ.to_kindc(env.clone(), met))
},
Term::Slf { nam, typ, bod } => {
format!("$({}: {}) {}", nam, typ.to_kindc(met), bod.to_kindc(met))
format!("$({}: {}) {}", nam, typ.to_kindc(env.clone(), met), bod.to_kindc(cons(&env, nam.clone()), met))
},
Term::Ins { val } => {
format!("~{}", val.to_kindc(met))
format!("~{}", val.to_kindc(env.clone(), met))
},
Term::Set => "*".to_string(),
Term::U60 => "U60".to_string(),
Term::Num { val } => val.to_string(),
Term::Op2 { opr, fst, snd } => {
format!("({} {} {})", opr.to_kindc(), fst.to_kindc(met), snd.to_kindc(met))
format!("({} {} {})", opr.to_kindc(), fst.to_kindc(env.clone(), met), snd.to_kindc(env.clone(), met))
},
Term::Swi { nam, x, z, s, p } => {
format!("switch {} = {} {{ 0: {} _: {} }}: {}", nam, x.to_kindc(met), z.to_kindc(met), s.to_kindc(met), p.to_kindc(met))
format!("switch {} = {} {{ 0: {} _: {} }}: {}", nam, x.to_kindc(env.clone(), met), z.to_kindc(env.clone(), met), s.to_kindc(cons(&env, format!("{}-1", nam)), met), p.to_kindc(cons(&env, nam.clone()), met))
},
Term::Let { nam, val, bod } => {
format!("let {} = {}; {}", nam, val.to_kindc(met), bod.to_kindc(met))
format!("let {} = {}; {}", nam, val.to_kindc(env.clone(), met), bod.to_kindc(cons(&env, nam.clone()), met))
},
Term::Use { nam, val, bod } => {
format!("use {} = {}; {}", nam, val.to_kindc(met), bod.to_kindc(met))
format!("use {} = {}; {}", nam, val.to_kindc(env.clone(), met), bod.to_kindc(cons(&env, nam.clone()), met))
},
Term::Hol { nam } => {
let env_str = env.iter().map(|n| Term::to_kindc_name(n)).collect::<Vec<_>>().join(",");
format!("?{}[{}]", nam, env_str)
},
Term::Hol { nam } => format!("?{}", nam),
Term::Met { .. } => {
let uid = *met;
*met += 1;
format!("_{}", uid)
},
Term::Var { nam } => nam.clone(),
Term::Src { src, val } => format!("!{} {}", src.to_u64(), val.to_kindc(met)),
Term::Var { nam } => Term::to_kindc_name(nam),
Term::Src { src, val } => format!("!{} {}", src.to_u64(), val.to_kindc(env, met)),
Term::Nat { nat } => format!("#{}", nat),
Term::Txt { txt } => format!("\"{}\"", txt.replace("\n", "\\n")),
Term::Mch { .. } => unreachable!(),
}
}
pub fn to_kindc_name(name: &str) -> String {