mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-10-03 18:27:13 +03:00
Merge branch 'master' of https://github.com/Derenash/kind2.0
This commit is contained in:
commit
3ce20b7003
6
book/U60.fib.kind2
Normal file
6
book/U60.fib.kind2
Normal file
@ -0,0 +1,6 @@
|
||||
fib (n: U60) : U60 =
|
||||
switch n {
|
||||
0: 0
|
||||
1: 1
|
||||
_: (+ (fib (- n 1)) (fib (- n 2)))
|
||||
}
|
5
book/U60.sum.kind2
Normal file
5
book/U60.sum.kind2
Normal file
@ -0,0 +1,5 @@
|
||||
sum (n: U60) : U60 =
|
||||
switch n {
|
||||
0: 0
|
||||
_: (+ n (sum n-1))
|
||||
}
|
@ -4,9 +4,8 @@
|
||||
|
||||
//use Nat.{succ,zero}
|
||||
|
||||
_main : Nat =
|
||||
#50
|
||||
|
||||
_main : U60 =
|
||||
(U60.fib 6)
|
||||
|
||||
//_main (a: Nat) (b: Nat) (e: (Equal A a b)) : (Equal A a b) =
|
||||
//switch a {
|
||||
|
@ -750,7 +750,7 @@ termShow (Use nam val bod) dep =
|
||||
bod' = termShow (bod (Var nam dep)) (dep + 1)
|
||||
in stringJoin ["use " , nam' , " = " , val' , "; " , bod']
|
||||
termShow Set dep = "*"
|
||||
termShow U60 dep = "#U60"
|
||||
termShow U60 dep = "U60"
|
||||
termShow (Num val) dep =
|
||||
let val' = u60Show val
|
||||
in stringJoin [val']
|
||||
@ -765,7 +765,7 @@ termShow (Swi nam x z s p) dep =
|
||||
z' = termShow z dep
|
||||
s' = termShow (s (Var (stringConcat nam "-1") dep)) (dep + 1)
|
||||
p' = termShow (p (Var nam dep)) dep
|
||||
in stringJoin ["switch " , nam' , " = " , x' , " { #0: " , z' , " #+: " , s' , " }: " , p']
|
||||
in stringJoin ["switch " , nam' , " = " , x' , " { 0: " , z' , " _: " , s' , " }: " , p']
|
||||
termShow (Txt txt) dep = stringJoin [quote , txt , quote]
|
||||
termShow (Nat val) dep = show val
|
||||
termShow (Hol nam ctx) dep = stringJoin ["?" , nam]
|
||||
|
@ -94,6 +94,25 @@ impl<'i> KindParser<'i> {
|
||||
if self.starts_with("λ") {
|
||||
let ini = *self.index() as u64;
|
||||
self.consume("λ")?;
|
||||
// Annotated
|
||||
if self.peek_one() == Some('(') {
|
||||
self.consume("(")?;
|
||||
let nam = self.parse_name()?;
|
||||
self.consume(":")?;
|
||||
let typ = Box::new(self.parse_term(fid, uses)?);
|
||||
self.consume(")")?;
|
||||
let bod = Box::new(self.parse_term(fid, &shadow(&nam, uses))?);
|
||||
let end = *self.index() as u64;
|
||||
let src = Src::new(fid, ini, end);
|
||||
let typ = Box::new(Term::All { nam: nam.clone(), inp: typ, bod: Box::new(Term::Met {}) });
|
||||
let val = Box::new(Term::Lam { nam: nam.clone(), bod });
|
||||
let val = Box::new(Term::Ann { chk: true, typ, val });
|
||||
return Ok(Term::Src { src, val });
|
||||
}
|
||||
//λ(x: A) B
|
||||
//-----------------
|
||||
//{λx B: ∀(x: A) _}
|
||||
// Untyped
|
||||
let nam = self.parse_name()?;
|
||||
let bod = Box::new(self.parse_term(fid, &shadow(&nam, uses))?);
|
||||
let end = *self.index() as u64;
|
||||
@ -218,6 +237,24 @@ impl<'i> KindParser<'i> {
|
||||
// SWI ::= switch <name> = <term> { 0: <term>; +: <term> }: <term>
|
||||
// - The matched term is optional. Defaults to `Var { nam: <name> }`.
|
||||
// - The return type is optional. Defaults to `Met {}`.
|
||||
// - Consecutive numbers can be chained, as a syntax sugar. Example:
|
||||
// switch x = expr {
|
||||
// 0: ... zero case ...
|
||||
// 1: ... one case ...
|
||||
// 2: ... two case ...
|
||||
// _: ... >=3 case, with access to x-3 ...
|
||||
// }: return_type
|
||||
// Is desugared to:
|
||||
// switch x = expr {
|
||||
// 0: ... zero case ...
|
||||
// _: switch x = x-1 {
|
||||
// 0: ... one case ...
|
||||
// _: switch x = x-2 {
|
||||
// 0: ... two case ...
|
||||
// _: ... >=3 case, with access to x-3 ...
|
||||
// }: _
|
||||
// }:_
|
||||
// }: return_type
|
||||
if self.starts_with("switch ") {
|
||||
let ini = *self.index() as u64;
|
||||
self.consume("switch ")?;
|
||||
@ -230,10 +267,20 @@ impl<'i> KindParser<'i> {
|
||||
Box::new(Term::Var { nam: nam.clone() })
|
||||
};
|
||||
self.consume("{")?;
|
||||
self.consume("0:")?;
|
||||
let z = Box::new(self.parse_term(fid, uses)?);
|
||||
self.consume("+:")?;
|
||||
let s = Box::new(self.parse_term(fid, &shadow(&format!("{}-1",nam), uses))?);
|
||||
let mut cases = Vec::new();
|
||||
while self.peek_one() != Some('}') {
|
||||
if self.peek_one() == Some('_') {
|
||||
self.consume("_:")?;
|
||||
let body = Box::new(self.parse_term(fid, &shadow(&format!("{}-{}",nam,cases.len()), uses))?);
|
||||
cases.push(body);
|
||||
break;
|
||||
} else {
|
||||
self.consume(&format!("{}:", cases.len()))?;
|
||||
let body = Box::new(self.parse_term(fid, uses)?);
|
||||
cases.push(body);
|
||||
self.skip_trivia();
|
||||
}
|
||||
}
|
||||
self.consume("}")?;
|
||||
let p = if self.peek_one() == Some(':') {
|
||||
self.consume(":")?;
|
||||
@ -243,7 +290,23 @@ impl<'i> KindParser<'i> {
|
||||
};
|
||||
let end = *self.index() as u64;
|
||||
let src = Src::new(fid, ini, end);
|
||||
return Ok(Term::Src { src, val: Box::new(Term::Swi { nam, x, z, s, p }) });
|
||||
// Desugars a long switch into a nested chain of switches
|
||||
let mut val = cases.pop().unwrap();
|
||||
val = Box::new(Term::Use {
|
||||
nam: format!("{}-{}", nam, cases.len()),
|
||||
val: Box::new(Term::Var { nam: format!("{}-1", nam) }),
|
||||
bod: val,
|
||||
});
|
||||
for i in (1..(cases.len())).rev() {
|
||||
let x = Box::new(Term::Var { nam: format!("{}-1", nam.clone()) });
|
||||
let z = cases[i].clone();
|
||||
let s = val;
|
||||
let p = Box::new(Term::Met {});
|
||||
val = Box::new(Term::Swi { nam: nam.clone(), x, z, s, p });
|
||||
}
|
||||
val = Box::new(Term::Swi { nam, x, z: cases[0].clone(), s: val, p });
|
||||
//println!("SWITCH:\n{}", val.show());
|
||||
return Ok(Term::Src { src, val });
|
||||
}
|
||||
|
||||
// NAT ::= #<uint>
|
||||
|
@ -149,15 +149,15 @@ impl Term {
|
||||
Show::text("*")
|
||||
},
|
||||
Term::U60 => {
|
||||
Show::text("#U60")
|
||||
Show::text("U60")
|
||||
},
|
||||
Term::Num { val } => {
|
||||
Show::text(&format!("#{}", val))
|
||||
Show::text(&format!("{}", val))
|
||||
},
|
||||
Term::Op2 { opr, fst, snd } => {
|
||||
Show::call(" ", vec![
|
||||
Show::glue("", vec![
|
||||
Show::text("#("),
|
||||
Show::text("("),
|
||||
opr.format(),
|
||||
]),
|
||||
Show::glue("", vec![
|
||||
@ -183,7 +183,7 @@ impl Term {
|
||||
z.format_go(),
|
||||
]),
|
||||
Show::glue("", vec![
|
||||
Show::text("+: "),
|
||||
Show::text("_: "),
|
||||
s.format_go(),
|
||||
Show::text(" "),
|
||||
]),
|
||||
|
Loading…
Reference in New Issue
Block a user