mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-08-17 06:40:28 +03:00
list/nat syntax sugars, reorganizations
This commit is contained in:
parent
d617aeac49
commit
dc5997bde8
4
Cargo.lock
generated
4
Cargo.lock
generated
@ -4,9 +4,9 @@ version = 3
|
|||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "TSPL"
|
name = "TSPL"
|
||||||
version = "0.0.6"
|
version = "0.0.8"
|
||||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
checksum = "c1ed463bdafa4b9eea9fe4120a51abb90289275c4f3411d344de2787567cb6ae"
|
checksum = "1cf26cc6171f5f62baf926d04bc23eab3412598d76908fff83fda919bba486f0"
|
||||||
dependencies = [
|
dependencies = [
|
||||||
"highlight_error",
|
"highlight_error",
|
||||||
]
|
]
|
||||||
|
@ -8,6 +8,6 @@ name = "kind2"
|
|||||||
path = "src/main.rs"
|
path = "src/main.rs"
|
||||||
|
|
||||||
[dependencies]
|
[dependencies]
|
||||||
TSPL = "0.0.6"
|
TSPL = "0.0.8"
|
||||||
highlight_error = "0.1.1"
|
highlight_error = "0.1.1"
|
||||||
im = "15.1.0"
|
im = "15.1.0"
|
||||||
|
@ -2,6 +2,6 @@ Bool
|
|||||||
: *
|
: *
|
||||||
= $(self: Bool)
|
= $(self: Bool)
|
||||||
∀(P: ∀(x: Bool) *)
|
∀(P: ∀(x: Bool) *)
|
||||||
∀(t: (P Bool.true))
|
∀(true: (P Bool.true))
|
||||||
∀(f: (P Bool.false))
|
∀(false: (P Bool.false))
|
||||||
(P self)
|
(P self)
|
@ -1,3 +1,3 @@
|
|||||||
Bool.lemma.notnot
|
Bool.lemma.notnot
|
||||||
: ∀(b: Bool) (Equal Bool (Bool.not (Bool.not b)) b)
|
: ∀(b: Bool) (Equal Bool (Bool.not (Bool.not b)) b)
|
||||||
= λb (~b _ ?a (Equal.refl Bool Bool.false))
|
= λb (~b _ (Equal.refl Bool Bool.true) (Equal.refl Bool Bool.false))
|
||||||
|
@ -3,9 +3,6 @@ List
|
|||||||
= λT
|
= λT
|
||||||
$(self: (List T))
|
$(self: (List T))
|
||||||
∀(P: ∀(xs: (List T)) *)
|
∀(P: ∀(xs: (List T)) *)
|
||||||
∀(cons:
|
∀(cons: ∀(head: T) ∀(tail: (List T)) (P (List.cons T head tail)))
|
||||||
∀(head: T) ∀(tail: (List T))
|
|
||||||
(P (List.cons T head tail))
|
|
||||||
)
|
|
||||||
∀(nil: (P (List.nil T)))
|
∀(nil: (P (List.nil T)))
|
||||||
(P self)
|
(P self)
|
@ -3,7 +3,5 @@ Sigma
|
|||||||
= λA λB
|
= λA λB
|
||||||
$(self: (Sigma A B))
|
$(self: (Sigma A B))
|
||||||
∀(P: ∀(x: (Sigma A B)) *)
|
∀(P: ∀(x: (Sigma A B)) *)
|
||||||
∀(new:
|
∀(new: ∀(a: A) ∀(b: (B a)) (P (Sigma.new A B a b)))
|
||||||
∀(a: A) ∀(b: (B a)) (P (Sigma.new A B a b))
|
|
||||||
)
|
|
||||||
(P self)
|
(P self)
|
9
book/The.kind2
Normal file
9
book/The.kind2
Normal file
@ -0,0 +1,9 @@
|
|||||||
|
The
|
||||||
|
: ∀(A: *)
|
||||||
|
∀(x: A)
|
||||||
|
*
|
||||||
|
= λA λx
|
||||||
|
$(self: (The A x))
|
||||||
|
∀(P: ∀(x: A) ∀(p: (The A x)) *)
|
||||||
|
∀(value: ∀(x: A) (P x (The.value A x)))
|
||||||
|
(P x self)
|
7
book/The.value.kind2
Normal file
7
book/The.value.kind2
Normal file
@ -0,0 +1,7 @@
|
|||||||
|
The.value
|
||||||
|
: ∀(A: *)
|
||||||
|
∀(x: A)
|
||||||
|
(The A x)
|
||||||
|
= λA λx
|
||||||
|
~λP λvalue (value x)
|
||||||
|
|
3
book/Vector.cons.kind2
Normal file
3
book/Vector.cons.kind2
Normal file
@ -0,0 +1,3 @@
|
|||||||
|
Vector.cons
|
||||||
|
: ∀(T: *) ∀(len: Nat) ∀(head: T) ∀(tail: (Vector T len)) (Vector T (Nat.succ len))
|
||||||
|
= λT λlen λhead λtail ~λP λcons λnil (cons len head tail)
|
8
book/Vector.kind2
Normal file
8
book/Vector.kind2
Normal file
@ -0,0 +1,8 @@
|
|||||||
|
Vector
|
||||||
|
: ∀(T: *) ∀(len: Nat) *
|
||||||
|
= λT λlen
|
||||||
|
$(self: (Vector T len))
|
||||||
|
∀(P: ∀(len: Nat) ∀(xs: (Vector T len)) *)
|
||||||
|
∀(cons: ∀(len: Nat) ∀(head: T) ∀(tail: (Vector T len)) (P (Nat.succ len) (Vector.cons T len head tail)))
|
||||||
|
∀(nil: (P Nat.zero (Vector.nil T)))
|
||||||
|
(P len self)
|
3
book/Vector.nil.kind2
Normal file
3
book/Vector.nil.kind2
Normal file
@ -0,0 +1,3 @@
|
|||||||
|
Vector.nil
|
||||||
|
: ∀(T: *) (Vector T Nat.zero)
|
||||||
|
= λT ~λP λcons λnil nil
|
@ -1,7 +1,7 @@
|
|||||||
_main
|
_main
|
||||||
: use list =
|
: use list =
|
||||||
(List.cons _ Nat.zero
|
(List.cons _ Nat.zero
|
||||||
(List.cons _ (Nat.succ Nat.zero)
|
(List.cons _ 1
|
||||||
(List.cons _ (Nat.succ (Nat.succ Nat.zero))
|
(List.cons _ (Nat.succ (Nat.succ Nat.zero))
|
||||||
(List.nil _))))
|
(List.nil _))))
|
||||||
(The (List Nat) list)
|
(The (List Nat) list)
|
||||||
|
@ -6,7 +6,6 @@ use std::collections::BTreeSet;
|
|||||||
mod compile;
|
mod compile;
|
||||||
mod format;
|
mod format;
|
||||||
mod parse;
|
mod parse;
|
||||||
mod show;
|
|
||||||
|
|
||||||
// <book> ::=
|
// <book> ::=
|
||||||
// DEF_ANN | <name> : <term> = <term> <book>
|
// DEF_ANN | <name> : <term> = <term> <book>
|
||||||
@ -20,6 +19,10 @@ pub struct Book {
|
|||||||
|
|
||||||
impl Book {
|
impl Book {
|
||||||
|
|
||||||
|
pub fn show(&self) -> String {
|
||||||
|
return self.format().flatten(None);
|
||||||
|
}
|
||||||
|
|
||||||
pub fn new() -> Self {
|
pub fn new() -> Self {
|
||||||
Book {
|
Book {
|
||||||
defs: BTreeMap::new(),
|
defs: BTreeMap::new(),
|
||||||
@ -57,6 +60,9 @@ impl Book {
|
|||||||
load_go("String", &mut book)?;
|
load_go("String", &mut book)?;
|
||||||
load_go("String.cons", &mut book)?;
|
load_go("String.cons", &mut book)?;
|
||||||
load_go("String.nil", &mut book)?;
|
load_go("String.nil", &mut book)?;
|
||||||
|
load_go("Nat", &mut book)?;
|
||||||
|
load_go("Nat.succ", &mut book)?;
|
||||||
|
load_go("Nat.zero", &mut book)?;
|
||||||
//println!("DONE!");
|
//println!("DONE!");
|
||||||
Ok(book)
|
Ok(book)
|
||||||
}
|
}
|
||||||
|
@ -1,13 +0,0 @@
|
|||||||
use crate::{*};
|
|
||||||
|
|
||||||
impl Book {
|
|
||||||
|
|
||||||
pub fn show(&self) -> String {
|
|
||||||
let mut book_str = String::new();
|
|
||||||
for (name, term) in &self.defs {
|
|
||||||
book_str.push_str(&format!("{} = {}\n", name, term.show()));
|
|
||||||
}
|
|
||||||
book_str
|
|
||||||
}
|
|
||||||
|
|
||||||
}
|
|
@ -1,3 +1,5 @@
|
|||||||
|
use crate::Term;
|
||||||
|
|
||||||
// Example:
|
// Example:
|
||||||
// ["(" "foo" "arg0" "arg1" "arg2" ")"]
|
// ["(" "foo" "arg0" "arg1" "arg2" ")"]
|
||||||
// Call:
|
// Call:
|
||||||
@ -75,45 +77,49 @@ impl Form {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// Flattens the Form structure into a string, respecting indentation and width limits.
|
// Flattens the Form structure into a string, respecting indentation and width limits.
|
||||||
pub fn flatten(&self, lim: usize) -> String {
|
pub fn flatten(&self, lim: Option<usize>) -> String {
|
||||||
let mut out = String::new();
|
let mut out = String::new();
|
||||||
self.flatten_into(&mut out, &mut 0, lim);
|
if let Some(lim) = lim {
|
||||||
|
self.flatten_into(&mut out, true, &mut 0, lim);
|
||||||
|
} else {
|
||||||
|
self.flatten_into(&mut out, false, &mut 0, 0);
|
||||||
|
}
|
||||||
out
|
out
|
||||||
}
|
}
|
||||||
|
|
||||||
// Helper function.
|
// Helper function.
|
||||||
pub fn flatten_into(&self, out: &mut String, tab: &mut usize, lim: usize) {
|
pub fn flatten_into(&self, out: &mut String, fmt: bool, tab: &mut usize, lim: usize) {
|
||||||
match self {
|
match self {
|
||||||
Form::Many { style, join, child } => {
|
Form::Many { style, join, child } => {
|
||||||
match style {
|
match style {
|
||||||
Style::Call => {
|
Style::Call => {
|
||||||
let add_lines = Form::no_lines(&child) && self.width(lim) >= lim;
|
let add_lines = fmt && Form::no_lines(&child) && self.width(lim) >= lim;
|
||||||
for (i, c) in child.iter().enumerate() {
|
for (i, c) in child.iter().enumerate() {
|
||||||
if add_lines && i > 0 && i < child.len() - 1 {
|
if add_lines && i > 0 && i < child.len() - 1 {
|
||||||
Form::Inc.flatten_into(out, tab, lim);
|
Form::Inc.flatten_into(out, fmt, tab, lim);
|
||||||
}
|
}
|
||||||
if add_lines && i > 0 {
|
if add_lines && i > 0 {
|
||||||
Form::Line.flatten_into(out, tab, lim);
|
Form::Line.flatten_into(out, fmt, tab, lim);
|
||||||
}
|
}
|
||||||
if !add_lines && i > 0 && i < child.len() - 1 {
|
if !add_lines && i > 0 && i < child.len() - 1 {
|
||||||
out.push_str(&join);
|
out.push_str(&join);
|
||||||
}
|
}
|
||||||
c.flatten_into(out, tab, lim);
|
c.flatten_into(out, fmt, tab, lim);
|
||||||
if add_lines && i > 0 && i < child.len() - 1 {
|
if add_lines && i > 0 && i < child.len() - 1 {
|
||||||
Form::Dec.flatten_into(out, tab, lim);
|
Form::Dec.flatten_into(out, fmt, tab, lim);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
Style::Pile => {
|
Style::Pile => {
|
||||||
let add_lines = Form::no_lines(&child) && self.width(lim) >= lim;
|
let add_lines = fmt && Form::no_lines(&child) && self.width(lim) >= lim;
|
||||||
for (i, c) in child.iter().enumerate() {
|
for (i, c) in child.iter().enumerate() {
|
||||||
if add_lines && i > 0 {
|
if add_lines && i > 0 {
|
||||||
Form::Line.flatten_into(out, tab, lim);
|
Form::Line.flatten_into(out, fmt, tab, lim);
|
||||||
}
|
}
|
||||||
if !add_lines && i > 0 {
|
if !add_lines && i > 0 {
|
||||||
out.push_str(&join);
|
out.push_str(&join);
|
||||||
}
|
}
|
||||||
c.flatten_into(out, tab, lim);
|
c.flatten_into(out, fmt, tab, lim);
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
Style::Glue => {
|
Style::Glue => {
|
||||||
@ -121,7 +127,7 @@ impl Form {
|
|||||||
if i > 0 {
|
if i > 0 {
|
||||||
out.push_str(&join);
|
out.push_str(&join);
|
||||||
}
|
}
|
||||||
c.flatten_into(out, tab, lim);
|
c.flatten_into(out, fmt, tab, lim);
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
}
|
}
|
||||||
|
@ -27,7 +27,10 @@ pub enum Info {
|
|||||||
},
|
},
|
||||||
Vague {
|
Vague {
|
||||||
nam: String,
|
nam: String,
|
||||||
}
|
},
|
||||||
|
Print {
|
||||||
|
val: Term,
|
||||||
|
},
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
@ -55,6 +58,9 @@ impl Info {
|
|||||||
},
|
},
|
||||||
Info::Vague { nam } => {
|
Info::Vague { nam } => {
|
||||||
format!("VAGUE: _{}", nam)
|
format!("VAGUE: _{}", nam)
|
||||||
|
},
|
||||||
|
Info::Print { val } => {
|
||||||
|
format!("{}", val.show())
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -56,6 +56,13 @@ impl<'i> KindParser<'i> {
|
|||||||
self.consume("}")?;
|
self.consume("}")?;
|
||||||
Ok(Info::Vague { nam })
|
Ok(Info::Vague { nam })
|
||||||
}
|
}
|
||||||
|
Some('p') => {
|
||||||
|
self.consume("print")?;
|
||||||
|
self.consume("{")?;
|
||||||
|
let val = self.parse_term(0)?;
|
||||||
|
self.consume("}")?;
|
||||||
|
Ok(Info::Print { val })
|
||||||
|
}
|
||||||
_ => self.expected("info type (solve, found, error)"),
|
_ => self.expected("info type (solve, found, error)"),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -1,5 +1,7 @@
|
|||||||
use crate::{*};
|
use crate::{*};
|
||||||
|
|
||||||
|
//./mod.rs//
|
||||||
|
|
||||||
impl Info {
|
impl Info {
|
||||||
|
|
||||||
pub fn show(&self) -> String {
|
pub fn show(&self) -> String {
|
||||||
@ -16,6 +18,9 @@ impl Info {
|
|||||||
},
|
},
|
||||||
Info::Vague { nam } => {
|
Info::Vague { nam } => {
|
||||||
format!("#vague{{?{}}}", nam)
|
format!("#vague{{?{}}}", nam)
|
||||||
|
},
|
||||||
|
Info::Print { val } => {
|
||||||
|
format!("#print{{{}}}", val.show())
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
31
src/kind2.hs
31
src/kind2.hs
@ -36,17 +36,19 @@ data Term
|
|||||||
| Num Int
|
| Num Int
|
||||||
| Op2 Oper Term Term
|
| Op2 Oper Term Term
|
||||||
| Mat String Term Term (Term -> Term) (Term -> Term)
|
| Mat String Term Term (Term -> Term) (Term -> Term)
|
||||||
| Txt String
|
|
||||||
| Hol String [Term]
|
| Hol String [Term]
|
||||||
| Met Int [Term]
|
| Met Int [Term]
|
||||||
| Var String Int
|
| Var String Int
|
||||||
| Src Int Term
|
| Src Int Term
|
||||||
|
| Txt String
|
||||||
|
| Nat Integer
|
||||||
|
|
||||||
data Info
|
data Info
|
||||||
= Found String Term [Term] Int
|
= Found String Term [Term] Int
|
||||||
| Solve Int Term Int
|
| Solve Int Term Int
|
||||||
| Error Int Term Term Term Int
|
| Error Int Term Term Term Int
|
||||||
| Vague String
|
| Vague String
|
||||||
|
| Print Term Int
|
||||||
|
|
||||||
data Check = Check Int Term Term Int
|
data Check = Check Int Term Term Int
|
||||||
data State = State (Map Term) [Check] [Info] -- state type
|
data State = State (Map Term) [Check] [Info] -- state type
|
||||||
@ -195,7 +197,7 @@ envRewind :: State -> Env Int
|
|||||||
envRewind state = Env $ \_ -> Done state 0
|
envRewind state = Env $ \_ -> Done state 0
|
||||||
|
|
||||||
envSusp :: Check -> Env ()
|
envSusp :: Check -> Env ()
|
||||||
envSusp chk = Env $ \(State fill susp logs) -> Done (State fill (chk : susp) logs) ()
|
envSusp chk = Env $ \(State fill susp logs) -> Done (State fill (listPush chk susp) logs) ()
|
||||||
|
|
||||||
envFill :: Int -> Term -> Env ()
|
envFill :: Int -> Term -> Env ()
|
||||||
envFill k v = Env $ \(State fill susp logs) -> Done (State (mapSet (key k) v fill) susp logs) ()
|
envFill k v = Env $ \(State fill susp logs) -> Done (State (mapSet (key k) v fill) susp logs) ()
|
||||||
@ -240,6 +242,7 @@ termReduce fill lv (Use nam val bod) = termReduce fill lv (bod val)
|
|||||||
termReduce fill lv (Op2 opr fst snd) = termReduceOp2 fill lv opr (termReduce fill lv fst) (termReduce fill lv snd)
|
termReduce fill lv (Op2 opr fst snd) = termReduceOp2 fill lv opr (termReduce fill lv fst) (termReduce fill lv snd)
|
||||||
termReduce fill lv (Mat nam x z s p) = termReduceMat fill lv nam (termReduce fill lv x) z s p
|
termReduce fill lv (Mat nam x z s p) = termReduceMat fill lv nam (termReduce fill lv x) z s p
|
||||||
termReduce fill lv (Txt txt) = termReduceTxt fill lv txt
|
termReduce fill lv (Txt txt) = termReduceTxt fill lv txt
|
||||||
|
termReduce fill lv (Nat val) = termReduceNat fill lv val
|
||||||
termReduce fill lv (Src src val) = termReduce fill lv val
|
termReduce fill lv (Src src val) = termReduce fill lv val
|
||||||
termReduce fill lv (Met uid spn) = termReduceMet fill lv uid spn
|
termReduce fill lv (Met uid spn) = termReduceMet fill lv uid spn
|
||||||
termReduce fill lv val = val
|
termReduce fill lv val = val
|
||||||
@ -292,7 +295,12 @@ termReduceRef fill 1 nam val = Ref nam val
|
|||||||
termReduceRef fill lv nam val = Ref nam val
|
termReduceRef fill lv nam val = Ref nam val
|
||||||
|
|
||||||
termReduceTxt :: Map Term -> Int -> String -> Term
|
termReduceTxt :: Map Term -> Int -> String -> Term
|
||||||
termReduceTxt fill lv txt = Txt txt
|
termReduceTxt fill lv [] = termReduce fill lv xString_nil
|
||||||
|
termReduceTxt fill lv (x:xs) = termReduce fill lv (App (App xString_cons (Num (ord x))) (Txt xs))
|
||||||
|
|
||||||
|
termReduceNat :: Map Term -> Int -> Integer -> Term
|
||||||
|
termReduceNat fill lv 0 = xNat_zero
|
||||||
|
termReduceNat fill lv n = App xNat_succ (termReduceNat fill lv (n - 1))
|
||||||
|
|
||||||
-- Normalization
|
-- Normalization
|
||||||
-- -------------
|
-- -------------
|
||||||
@ -322,6 +330,7 @@ termNormal fill lv term dep = termNormalGo fill lv (termReduce fill lv term) dep
|
|||||||
termNormalGo fill lv (Op2 opr fst snd) dep = Op2 opr (termNormal fill lv fst dep) (termNormal fill lv snd dep)
|
termNormalGo fill lv (Op2 opr fst snd) dep = Op2 opr (termNormal fill lv fst dep) (termNormal fill lv snd dep)
|
||||||
termNormalGo fill lv (Mat nam x z s p) dep = Mat nam (termNormal fill lv x dep) (termNormal fill lv z dep) (\k -> termNormal fill lv (s (Var (stringConcat nam "-1") dep)) dep) (\k -> termNormal fill lv (p (Var nam dep)) dep)
|
termNormalGo fill lv (Mat nam x z s p) dep = Mat nam (termNormal fill lv x dep) (termNormal fill lv z dep) (\k -> termNormal fill lv (s (Var (stringConcat nam "-1") dep)) dep) (\k -> termNormal fill lv (p (Var nam dep)) dep)
|
||||||
termNormalGo fill lv (Txt val) dep = Txt val
|
termNormalGo fill lv (Txt val) dep = Txt val
|
||||||
|
termNormalGo fill lv (Nat val) dep = Nat val
|
||||||
termNormalGo fill lv (Var nam idx) dep = Var nam idx
|
termNormalGo fill lv (Var nam idx) dep = Var nam idx
|
||||||
termNormalGo fill lv (Src src val) dep = Src src (termNormal fill lv val dep)
|
termNormalGo fill lv (Src src val) dep = Src src (termNormal fill lv val dep)
|
||||||
termNormalGo fill lv (Met uid spn) dep = Met uid spn -- TODO: normalize spine
|
termNormalGo fill lv (Met uid spn) dep = Met uid spn -- TODO: normalize spine
|
||||||
@ -437,6 +446,8 @@ termIdenticalGo (Mat aNam aX aZ aS aP) (Mat bNam bX bZ bS bP) dep =
|
|||||||
envPure (iX && iZ && iS && iP)
|
envPure (iX && iZ && iS && iP)
|
||||||
termIdenticalGo (Txt aTxt) (Txt bTxt) dep =
|
termIdenticalGo (Txt aTxt) (Txt bTxt) dep =
|
||||||
envPure (aTxt == bTxt)
|
envPure (aTxt == bTxt)
|
||||||
|
termIdenticalGo (Nat aVal) (Nat bVal) dep =
|
||||||
|
envPure (aVal == bVal)
|
||||||
termIdenticalGo (Src aSrc aVal) b dep =
|
termIdenticalGo (Src aSrc aVal) b dep =
|
||||||
termIdentical aVal b dep
|
termIdentical aVal b dep
|
||||||
termIdenticalGo a (Src bSrc bVal) dep =
|
termIdenticalGo a (Src bSrc bVal) dep =
|
||||||
@ -514,6 +525,7 @@ termUnifySubst lvl neo (Num n) = Num n
|
|||||||
termUnifySubst lvl neo (Op2 opr fst snd) = Op2 opr (termUnifySubst lvl neo fst) (termUnifySubst lvl neo snd)
|
termUnifySubst lvl neo (Op2 opr fst snd) = Op2 opr (termUnifySubst lvl neo fst) (termUnifySubst lvl neo snd)
|
||||||
termUnifySubst lvl neo (Mat nam x z s p) = Mat nam (termUnifySubst lvl neo x) (termUnifySubst lvl neo z) (\k -> termUnifySubst lvl neo (s k)) (\k -> termUnifySubst lvl neo (p k))
|
termUnifySubst lvl neo (Mat nam x z s p) = Mat nam (termUnifySubst lvl neo x) (termUnifySubst lvl neo z) (\k -> termUnifySubst lvl neo (s k)) (\k -> termUnifySubst lvl neo (p k))
|
||||||
termUnifySubst lvl neo (Txt txt) = Txt txt
|
termUnifySubst lvl neo (Txt txt) = Txt txt
|
||||||
|
termUnifySubst lvl neo (Nat val) = Nat val
|
||||||
termUnifySubst lvl neo (Var nam idx) = if lvl == idx then neo else Var nam idx
|
termUnifySubst lvl neo (Var nam idx) = if lvl == idx then neo else Var nam idx
|
||||||
termUnifySubst lvl neo (Src src val) = Src src (termUnifySubst lvl neo val)
|
termUnifySubst lvl neo (Src src val) = Src src (termUnifySubst lvl neo val)
|
||||||
|
|
||||||
@ -576,6 +588,8 @@ termInferGo (Num num) dep = do
|
|||||||
return U60
|
return U60
|
||||||
termInferGo (Txt txt) dep = do
|
termInferGo (Txt txt) dep = do
|
||||||
return xString
|
return xString
|
||||||
|
termInferGo (Nat val) dep = do
|
||||||
|
return xNat
|
||||||
termInferGo (Op2 opr fst snd) dep = do
|
termInferGo (Op2 opr fst snd) dep = do
|
||||||
envSusp (Check 0 fst U60 dep)
|
envSusp (Check 0 fst U60 dep)
|
||||||
envSusp (Check 0 snd U60 dep)
|
envSusp (Check 0 snd U60 dep)
|
||||||
@ -725,6 +739,7 @@ termShow (Mat nam x z s p) dep =
|
|||||||
p' = termShow (p (Var nam dep)) dep
|
p' = termShow (p (Var nam dep)) dep
|
||||||
in stringJoin ["#match " , nam' , " = " , x' , " { #0: " , z' , " #+: " , s' , " }: " , p']
|
in stringJoin ["#match " , nam' , " = " , x' , " { #0: " , z' , " #+: " , s' , " }: " , p']
|
||||||
termShow (Txt txt) dep = stringJoin [quote , txt , quote]
|
termShow (Txt txt) dep = stringJoin [quote , txt , quote]
|
||||||
|
termShow (Nat val) dep = show val
|
||||||
termShow (Hol nam ctx) dep = stringJoin ["?" , nam]
|
termShow (Hol nam ctx) dep = stringJoin ["?" , nam]
|
||||||
termShow (Met uid spn) dep = stringJoin ["(_", termShowSpn (reverse spn) dep, ")"]
|
termShow (Met uid spn) dep = stringJoin ["(_", termShowSpn (reverse spn) dep, ")"]
|
||||||
termShow (Var nam idx) dep = nam
|
termShow (Var nam idx) dep = nam
|
||||||
@ -777,10 +792,18 @@ infoShow fill (Solve name term dep) =
|
|||||||
in stringJoin ["#solve{", show name, " ", term', "}"]
|
in stringJoin ["#solve{", show name, " ", term', "}"]
|
||||||
infoShow fill (Vague name) =
|
infoShow fill (Vague name) =
|
||||||
stringJoin ["#vague{", name, "}"]
|
stringJoin ["#vague{", name, "}"]
|
||||||
|
infoShow fill (Print value dep) =
|
||||||
|
let val = termShow (termNormal fill 0 value dep) dep
|
||||||
|
in stringJoin ["#print{", val, "}"]
|
||||||
|
|
||||||
-- API
|
-- API
|
||||||
-- ---
|
-- ---
|
||||||
|
|
||||||
|
-- Normalizes a term
|
||||||
|
apiNormal :: Term -> IO ()
|
||||||
|
apiNormal term = putStrLn $ infoShow mapNew (Print (termNormal mapNew 2 term 0) 0)
|
||||||
|
|
||||||
|
-- Type-checks a term
|
||||||
apiCheck :: Term -> IO ()
|
apiCheck :: Term -> IO ()
|
||||||
apiCheck term = case envRun $ termCheckDef term of
|
apiCheck term = case envRun $ termCheckDef term of
|
||||||
Done state value -> apiPrintLogs state
|
Done state value -> apiPrintLogs state
|
||||||
@ -810,4 +833,4 @@ 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)))
|
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)))
|
val = (Lam "P" $ \p -> (Lam "f" $ \f -> (Lam "x" $ \x -> f)))
|
||||||
|
|
||||||
xString = undefined
|
xString = undefined; xString_cons = undefined; xString_nil = undefined; xNat = undefined; xNat_succ = undefined; xNat_zero = undefined
|
||||||
|
@ -40,7 +40,7 @@ fn generate_check_hs(book: &Book, command: &str, arg: &str) -> String {
|
|||||||
let book_hs = book.to_hs();
|
let book_hs = book.to_hs();
|
||||||
let main_hs = match command {
|
let main_hs = match command {
|
||||||
"check" => format!("main = (apiCheck {})\n", Term::to_hs_name(arg)),
|
"check" => format!("main = (apiCheck {})\n", Term::to_hs_name(arg)),
|
||||||
"run" => format!("Main = (apiNormal {})\n", Term::to_hs_name(arg)),
|
"run" => format!("main = (apiNormal {})\n", Term::to_hs_name(arg)),
|
||||||
_ => panic!("invalid command"),
|
_ => panic!("invalid command"),
|
||||||
};
|
};
|
||||||
let hs_code = format!("{}\n{}\n{}", kind_hs, book_hs, main_hs);
|
let hs_code = format!("{}\n{}\n{}", kind_hs, book_hs, main_hs);
|
||||||
@ -116,6 +116,12 @@ fn main() {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
//fn main() {
|
||||||
|
//env::set_current_dir("./book").expect("Failed to change directory to ./book");
|
||||||
|
//let adt = term::sugar::ADT::load("Bool");
|
||||||
|
//println!("{:?}", adt);
|
||||||
|
//}
|
||||||
|
|
||||||
fn show_help() {
|
fn show_help() {
|
||||||
eprintln!("Usage: kind2 [check|run] <name>");
|
eprintln!("Usage: kind2 [check|run] <name>");
|
||||||
std::process::exit(1);
|
std::process::exit(1);
|
||||||
|
@ -1,5 +1,7 @@
|
|||||||
use crate::{*};
|
use crate::{*};
|
||||||
|
|
||||||
|
//./mod.rs//
|
||||||
|
|
||||||
impl Oper {
|
impl Oper {
|
||||||
|
|
||||||
pub fn to_ctr(&self) -> &'static str {
|
pub fn to_ctr(&self) -> &'static str {
|
||||||
@ -176,9 +178,6 @@ impl Term {
|
|||||||
let p = p.to_hs(cons(&env, nam.clone()), 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)
|
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 } => {
|
Term::Let { nam, val, bod } => {
|
||||||
let val = val.to_hs(env.clone(), met);
|
let val = val.to_hs(env.clone(), met);
|
||||||
let bod = bod.to_hs(cons(&env, nam.clone()), met);
|
let bod = bod.to_hs(cons(&env, nam.clone()), met);
|
||||||
@ -206,6 +205,12 @@ impl Term {
|
|||||||
let val = val.to_hs(env, met);
|
let val = val.to_hs(env, met);
|
||||||
format!("(Src {} {})", src.to_u64(), val)
|
format!("(Src {} {})", src.to_u64(), val)
|
||||||
},
|
},
|
||||||
|
Term::Nat { nat } => {
|
||||||
|
format!("(Nat {})", nat)
|
||||||
|
},
|
||||||
|
Term::Txt { txt } => {
|
||||||
|
format!("(Txt \"{}\")", txt.replace("\n", "\\n"))
|
||||||
|
},
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -1,9 +1,37 @@
|
|||||||
use crate::{*};
|
use crate::{*};
|
||||||
|
|
||||||
|
|
||||||
|
//CONTEXT:
|
||||||
|
//./mod.rs//
|
||||||
|
//./sugar.rs//
|
||||||
|
//./../book/mod.rs//
|
||||||
|
//./../../book/Bool.kind2//
|
||||||
|
//./../../book/Nat.kind2//
|
||||||
|
//./../../book/List.kind2//
|
||||||
|
//./../../book/Sigma.kind2//
|
||||||
|
//./../../book/Monad.kind2//
|
||||||
|
|
||||||
impl Oper {
|
impl Oper {
|
||||||
|
|
||||||
pub fn format(&self) -> Box<Form> {
|
pub fn format(&self) -> Box<Form> {
|
||||||
Form::text(self.show())
|
Form::text(match self {
|
||||||
|
Oper::Add => "+",
|
||||||
|
Oper::Sub => "-",
|
||||||
|
Oper::Mul => "*",
|
||||||
|
Oper::Div => "/",
|
||||||
|
Oper::Mod => "%",
|
||||||
|
Oper::Eq => "==",
|
||||||
|
Oper::Ne => "!=",
|
||||||
|
Oper::Lt => "<",
|
||||||
|
Oper::Gt => ">",
|
||||||
|
Oper::Lte => "<=",
|
||||||
|
Oper::Gte => ">=",
|
||||||
|
Oper::And => "&",
|
||||||
|
Oper::Or => "|",
|
||||||
|
Oper::Xor => "^",
|
||||||
|
Oper::Lsh => "<<",
|
||||||
|
Oper::Rsh => ">>",
|
||||||
|
})
|
||||||
}
|
}
|
||||||
|
|
||||||
}
|
}
|
||||||
@ -11,10 +39,85 @@ impl Oper {
|
|||||||
impl Term {
|
impl Term {
|
||||||
|
|
||||||
pub fn format(&self) -> Box<Form> {
|
pub fn format(&self) -> Box<Form> {
|
||||||
self.clean().format_go()
|
return self.clean().format_go();
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn format_go(&self) -> Box<Form> {
|
pub fn format_go(&self) -> Box<Form> {
|
||||||
|
if let Some(nat) = self.as_nat() {
|
||||||
|
return Form::text(&format!("{}", nat));
|
||||||
|
}
|
||||||
|
|
||||||
|
if let Some(list) = self.as_list() {
|
||||||
|
if list.len() == 0 {
|
||||||
|
return Form::text("[]");
|
||||||
|
} else {
|
||||||
|
return Form::call("", vec![
|
||||||
|
Form::text("["),
|
||||||
|
Form::pile(", ", list.iter().map(|x| x.format_go()).collect()),
|
||||||
|
Form::text("]"),
|
||||||
|
]);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
//if let Some(adt) = self.as_adt() {
|
||||||
|
//return Form::glue("", vec![
|
||||||
|
//Form::text("data "),
|
||||||
|
//Form::text("TODO"),
|
||||||
|
//Form::glue(" ", adt.pars.iter().map(|(x,y)| {
|
||||||
|
//Form::call("", vec![
|
||||||
|
//Form::glue("", vec![
|
||||||
|
//Form::text("("),
|
||||||
|
//Form::text(x),
|
||||||
|
//Form::text(": "),
|
||||||
|
//]),
|
||||||
|
//y.format_go(),
|
||||||
|
//Form::text(")"),
|
||||||
|
//])
|
||||||
|
//}).collect()),
|
||||||
|
//Form::call("", vec![
|
||||||
|
//Form::text(":"),
|
||||||
|
//Form::pile(" ", adt.idxs.iter().map(|(x,y)| {
|
||||||
|
//Form::call("", vec![
|
||||||
|
//Form::glue("", vec![
|
||||||
|
//Form::text("("),
|
||||||
|
//Form::text(x),
|
||||||
|
//Form::text(": "),
|
||||||
|
//]),
|
||||||
|
//y.format_go(),
|
||||||
|
//Form::text(")"),
|
||||||
|
//])
|
||||||
|
//}).collect()),
|
||||||
|
//]),
|
||||||
|
//Form::line(),
|
||||||
|
//Form::glue("", adt.ctrs.iter().map(|ctr| {
|
||||||
|
//let mut vec = vec![
|
||||||
|
//Form::glue("", vec![
|
||||||
|
//Form::text("| "),
|
||||||
|
//Form::text(&ctr.name),
|
||||||
|
//])
|
||||||
|
//];
|
||||||
|
//for (x, y) in &ctr.flds {
|
||||||
|
//vec.push(Form::call("", vec![
|
||||||
|
//Form::glue("", vec![
|
||||||
|
//Form::text("("),
|
||||||
|
//Form::text(x),
|
||||||
|
//Form::text(": "),
|
||||||
|
//]),
|
||||||
|
//y.format_go(),
|
||||||
|
//Form::text(")"),
|
||||||
|
//]));
|
||||||
|
//}
|
||||||
|
//vec.push(Form::call("", vec![
|
||||||
|
//Form::glue("", vec![
|
||||||
|
//Form::text(":"),
|
||||||
|
//]),
|
||||||
|
//ctr.rtyp.format_go(),
|
||||||
|
//]));
|
||||||
|
//Form::pile(" ", vec)
|
||||||
|
//}).collect()),
|
||||||
|
//]);
|
||||||
|
//}
|
||||||
|
|
||||||
match self {
|
match self {
|
||||||
Term::All { .. } => {
|
Term::All { .. } => {
|
||||||
let mut bnd = vec![];
|
let mut bnd = vec![];
|
||||||
@ -146,9 +249,6 @@ impl Term {
|
|||||||
]),
|
]),
|
||||||
])
|
])
|
||||||
},
|
},
|
||||||
Term::Txt { txt } => {
|
|
||||||
Form::text(&format!("\"{}\"", txt))
|
|
||||||
},
|
|
||||||
Term::Let { nam, val, bod } => {
|
Term::Let { nam, val, bod } => {
|
||||||
Form::glue("", vec![
|
Form::glue("", vec![
|
||||||
Form::text("let "),
|
Form::text("let "),
|
||||||
@ -185,6 +285,12 @@ impl Term {
|
|||||||
Term::Src { src: _, val } => {
|
Term::Src { src: _, val } => {
|
||||||
val.format_go()
|
val.format_go()
|
||||||
},
|
},
|
||||||
|
Term::Txt { txt } => {
|
||||||
|
Form::text(&format!("\"{}\"", txt))
|
||||||
|
},
|
||||||
|
Term::Nat { nat } => {
|
||||||
|
Form::text(&format!("{}", nat))
|
||||||
|
},
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -1,10 +1,10 @@
|
|||||||
use crate::{*};
|
use crate::{*};
|
||||||
use std::collections::BTreeSet;
|
use std::collections::BTreeSet;
|
||||||
|
|
||||||
mod compile;
|
pub mod compile;
|
||||||
mod format;
|
pub mod format;
|
||||||
mod parse;
|
pub mod parse;
|
||||||
mod show;
|
pub mod sugar;
|
||||||
|
|
||||||
#[derive(Clone, Copy, Debug)]
|
#[derive(Clone, Copy, Debug)]
|
||||||
pub enum Oper {
|
pub enum Oper {
|
||||||
@ -33,8 +33,8 @@ pub struct Src {
|
|||||||
// NUM | #<uint>
|
// NUM | #<uint>
|
||||||
// OP2 | #(<oper> <term> <term>)
|
// OP2 | #(<oper> <term> <term>)
|
||||||
// MAT | #match <name> = <term> { #0: <term>; #+: <term> }: <term>
|
// MAT | #match <name> = <term> { #0: <term>; #+: <term> }: <term>
|
||||||
// MET | ?<name>
|
// HOL | ?<name>
|
||||||
// HOL | _
|
// MET | _
|
||||||
// CHR | '<char>'
|
// CHR | '<char>'
|
||||||
// STR | "<string>"
|
// STR | "<string>"
|
||||||
// LET | let <name> = <term> <term>
|
// LET | let <name> = <term> <term>
|
||||||
@ -52,13 +52,14 @@ pub enum Term {
|
|||||||
Num { val: u64 },
|
Num { val: u64 },
|
||||||
Op2 { opr: Oper, fst: Box<Term>, snd: Box<Term> },
|
Op2 { opr: Oper, fst: Box<Term>, snd: Box<Term> },
|
||||||
Mat { nam: String, x: Box<Term>, z: Box<Term>, s: Box<Term>, p: Box<Term> },
|
Mat { nam: String, x: Box<Term>, z: Box<Term>, s: Box<Term>, p: Box<Term> },
|
||||||
Txt { txt: String },
|
|
||||||
Let { nam: String, val: Box<Term>, bod: Box<Term> },
|
Let { nam: String, val: Box<Term>, bod: Box<Term> },
|
||||||
Use { nam: String, val: Box<Term>, bod: Box<Term> },
|
Use { nam: String, val: Box<Term>, bod: Box<Term> },
|
||||||
Var { nam: String },
|
Var { nam: String },
|
||||||
Hol { nam: String },
|
Hol { nam: String },
|
||||||
Met {},
|
Met {},
|
||||||
Src { src: Src, val: Box<Term> },
|
Src { src: Src, val: Box<Term> },
|
||||||
|
Nat { nat: u64 },
|
||||||
|
Txt { txt: String },
|
||||||
}
|
}
|
||||||
|
|
||||||
impl Src {
|
impl Src {
|
||||||
@ -95,8 +96,18 @@ pub fn cons<A>(vector: &im::Vector<A>, value: A) -> im::Vector<A> where A: Clone
|
|||||||
new_vector
|
new_vector
|
||||||
}
|
}
|
||||||
|
|
||||||
|
impl Oper {
|
||||||
|
pub fn show(&self) -> String {
|
||||||
|
return self.format().flatten(None);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
impl Term {
|
impl Term {
|
||||||
|
|
||||||
|
pub fn show(&self) -> String {
|
||||||
|
return self.format().flatten(None);
|
||||||
|
}
|
||||||
|
|
||||||
pub fn get_free_vars(&self, env: im::Vector<String>, free_vars: &mut BTreeSet<String>) {
|
pub fn get_free_vars(&self, env: im::Vector<String>, free_vars: &mut BTreeSet<String>) {
|
||||||
match self {
|
match self {
|
||||||
Term::All { nam, inp, bod } => {
|
Term::All { nam, inp, bod } => {
|
||||||
@ -134,6 +145,7 @@ impl Term {
|
|||||||
s.get_free_vars(cons(&env, format!("{}-1",nam)), free_vars);
|
s.get_free_vars(cons(&env, format!("{}-1",nam)), free_vars);
|
||||||
p.get_free_vars(cons(&env, nam.clone()), free_vars);
|
p.get_free_vars(cons(&env, nam.clone()), free_vars);
|
||||||
},
|
},
|
||||||
|
Term::Nat { nat: _ } => {},
|
||||||
Term::Txt { txt: _ } => {},
|
Term::Txt { txt: _ } => {},
|
||||||
Term::Let { nam, val, bod } => {
|
Term::Let { nam, val, bod } => {
|
||||||
val.get_free_vars(env.clone(), free_vars);
|
val.get_free_vars(env.clone(), free_vars);
|
||||||
@ -207,6 +219,9 @@ impl Term {
|
|||||||
let p = p.count_metas();
|
let p = p.count_metas();
|
||||||
x + z + s + p
|
x + z + s + p
|
||||||
},
|
},
|
||||||
|
Term::Nat { .. } => {
|
||||||
|
0
|
||||||
|
},
|
||||||
Term::Txt { .. } => {
|
Term::Txt { .. } => {
|
||||||
0
|
0
|
||||||
},
|
},
|
||||||
@ -301,6 +316,9 @@ impl Term {
|
|||||||
p: Box::new(p.clean()),
|
p: Box::new(p.clean()),
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
|
Term::Nat { nat } => {
|
||||||
|
Term::Nat { nat: *nat }
|
||||||
|
},
|
||||||
Term::Txt { txt } => {
|
Term::Txt { txt } => {
|
||||||
Term::Txt { txt: txt.clone() }
|
Term::Txt { txt: txt.clone() }
|
||||||
},
|
},
|
||||||
|
@ -1,5 +1,13 @@
|
|||||||
use crate::{*};
|
use crate::{*};
|
||||||
|
|
||||||
|
// FILES FOR CONTEXT:
|
||||||
|
|
||||||
|
//./mod.rs//
|
||||||
|
//./format.rs//
|
||||||
|
//./../../../TSPL/src/lib.rs//
|
||||||
|
|
||||||
|
// CURRENT FILE:
|
||||||
|
|
||||||
impl<'i> KindParser<'i> {
|
impl<'i> KindParser<'i> {
|
||||||
|
|
||||||
pub fn parse_oper(&mut self) -> Result<Oper, String> {
|
pub fn parse_oper(&mut self) -> Result<Oper, String> {
|
||||||
@ -35,8 +43,10 @@ impl<'i> KindParser<'i> {
|
|||||||
|
|
||||||
pub fn parse_term(&mut self, fid: u64) -> Result<Term, String> {
|
pub fn parse_term(&mut self, fid: u64) -> Result<Term, String> {
|
||||||
self.skip_trivia();
|
self.skip_trivia();
|
||||||
match self.peek_one() {
|
//println!("parsing ||{}", self.input[self.index..].replace("\n",""));
|
||||||
Some('∀') => {
|
|
||||||
|
// ALL ::= ∀(<name>: <term>) <term>
|
||||||
|
if self.starts_with("∀") {
|
||||||
let ini = *self.index() as u64;
|
let ini = *self.index() as u64;
|
||||||
self.consume("∀")?;
|
self.consume("∀")?;
|
||||||
self.consume("(")?;
|
self.consume("(")?;
|
||||||
@ -47,18 +57,22 @@ impl<'i> KindParser<'i> {
|
|||||||
let bod = Box::new(self.parse_term(fid)?);
|
let bod = Box::new(self.parse_term(fid)?);
|
||||||
let end = *self.index() as u64;
|
let end = *self.index() as u64;
|
||||||
let src = Src::new(fid, ini, end);
|
let src = Src::new(fid, ini, end);
|
||||||
Ok(Term::Src { src, val: Box::new(Term::All { nam, inp, bod }) })
|
return Ok(Term::Src { src, val: Box::new(Term::All { nam, inp, bod }) });
|
||||||
}
|
}
|
||||||
Some('λ') => {
|
|
||||||
|
// LAM ::= λ<name> <term>
|
||||||
|
if self.starts_with("λ") {
|
||||||
let ini = *self.index() as u64;
|
let ini = *self.index() as u64;
|
||||||
self.consume("λ")?;
|
self.consume("λ")?;
|
||||||
let nam = self.parse_name()?;
|
let nam = self.parse_name()?;
|
||||||
let bod = Box::new(self.parse_term(fid)?);
|
let bod = Box::new(self.parse_term(fid)?);
|
||||||
let end = *self.index() as u64;
|
let end = *self.index() as u64;
|
||||||
let src = Src::new(fid, ini, end);
|
let src = Src::new(fid, ini, end);
|
||||||
Ok(Term::Src { src, val: Box::new(Term::Lam { nam, bod }) })
|
return Ok(Term::Src { src, val: Box::new(Term::Lam { nam, bod }) });
|
||||||
}
|
}
|
||||||
Some('(') => {
|
|
||||||
|
// APP ::= (<term> <term>)
|
||||||
|
if self.starts_with("(") {
|
||||||
let ini = *self.index() as u64;
|
let ini = *self.index() as u64;
|
||||||
self.consume("(")?;
|
self.consume("(")?;
|
||||||
let fun = Box::new(self.parse_term(fid)?);
|
let fun = Box::new(self.parse_term(fid)?);
|
||||||
@ -74,9 +88,11 @@ impl<'i> KindParser<'i> {
|
|||||||
for arg in args {
|
for arg in args {
|
||||||
app = Box::new(Term::App { fun: app, arg });
|
app = Box::new(Term::App { fun: app, arg });
|
||||||
}
|
}
|
||||||
Ok(Term::Src { src, val: app })
|
return Ok(Term::Src { src, val: app });
|
||||||
}
|
}
|
||||||
Some('{') => {
|
|
||||||
|
// ANN ::= {<term>: <term>}
|
||||||
|
if self.starts_with("{") {
|
||||||
let ini = *self.index() as u64;
|
let ini = *self.index() as u64;
|
||||||
self.consume("{")?;
|
self.consume("{")?;
|
||||||
let val = Box::new(self.parse_term(fid)?);
|
let val = Box::new(self.parse_term(fid)?);
|
||||||
@ -85,9 +101,11 @@ impl<'i> KindParser<'i> {
|
|||||||
self.consume("}")?;
|
self.consume("}")?;
|
||||||
let end = *self.index() as u64;
|
let end = *self.index() as u64;
|
||||||
let src = Src::new(fid, ini, end);
|
let src = Src::new(fid, ini, end);
|
||||||
Ok(Term::Src { src, val: Box::new(Term::Ann { chk: true, val, typ }) })
|
return Ok(Term::Src { src, val: Box::new(Term::Ann { chk: true, val, typ }) });
|
||||||
}
|
}
|
||||||
Some('$') => {
|
|
||||||
|
// SLF ::= $(<name>: <term>) <term>
|
||||||
|
if self.starts_with("$") {
|
||||||
let ini = *self.index() as u64;
|
let ini = *self.index() as u64;
|
||||||
self.consume("$")?;
|
self.consume("$")?;
|
||||||
self.consume("(")?;
|
self.consume("(")?;
|
||||||
@ -98,48 +116,64 @@ impl<'i> KindParser<'i> {
|
|||||||
let bod = Box::new(self.parse_term(fid)?);
|
let bod = Box::new(self.parse_term(fid)?);
|
||||||
let end = *self.index() as u64;
|
let end = *self.index() as u64;
|
||||||
let src = Src::new(fid, ini, end);
|
let src = Src::new(fid, ini, end);
|
||||||
Ok(Term::Src { src, val: Box::new(Term::Slf { nam, typ, bod }) })
|
return Ok(Term::Src { src, val: Box::new(Term::Slf { nam, typ, bod }) });
|
||||||
}
|
}
|
||||||
Some('~') => {
|
|
||||||
|
// INS ::= ~<term>
|
||||||
|
if self.starts_with("~") {
|
||||||
let ini = *self.index() as u64;
|
let ini = *self.index() as u64;
|
||||||
self.consume("~")?;
|
self.consume("~")?;
|
||||||
let val = Box::new(self.parse_term(fid)?);
|
let val = Box::new(self.parse_term(fid)?);
|
||||||
let end = *self.index() as u64;
|
let end = *self.index() as u64;
|
||||||
let src = Src::new(fid, ini, end);
|
let src = Src::new(fid, ini, end);
|
||||||
Ok(Term::Src { src, val: Box::new(Term::Ins { val }) })
|
return Ok(Term::Src { src, val: Box::new(Term::Ins { val }) });
|
||||||
}
|
}
|
||||||
Some('*') => {
|
|
||||||
|
// SET ::= *
|
||||||
|
if self.starts_with("*") {
|
||||||
let ini = *self.index() as u64;
|
let ini = *self.index() as u64;
|
||||||
self.consume("*")?;
|
self.consume("*")?;
|
||||||
let end = *self.index() as u64;
|
let end = *self.index() as u64;
|
||||||
let src = Src::new(fid, ini, end);
|
let src = Src::new(fid, ini, end);
|
||||||
Ok(Term::Src { src, val: Box::new(Term::Set) })
|
return Ok(Term::Src { src, val: Box::new(Term::Set) });
|
||||||
}
|
}
|
||||||
Some('#') => {
|
|
||||||
|
// U60 ::= #U60
|
||||||
|
if self.starts_with("#U60") {
|
||||||
let ini = *self.index() as u64;
|
let ini = *self.index() as u64;
|
||||||
self.consume("#")?;
|
self.consume("#U60")?;
|
||||||
match self.peek_one() {
|
|
||||||
Some('U') => {
|
|
||||||
self.consume("U60")?;
|
|
||||||
let end = *self.index() as u64;
|
let end = *self.index() as u64;
|
||||||
let src = Src::new(fid, ini, end);
|
let src = Src::new(fid, ini, end);
|
||||||
Ok(Term::Src { src, val: Box::new(Term::U60) })
|
return Ok(Term::Src { src, val: Box::new(Term::U60) });
|
||||||
}
|
}
|
||||||
Some('(') => {
|
|
||||||
self.consume("(")?;
|
// OP2 ::= #(<oper> <term> <term>)
|
||||||
|
if self.starts_with("#(") {
|
||||||
|
let ini = *self.index() as u64;
|
||||||
|
self.consume("#(")?;
|
||||||
let opr = self.parse_oper()?;
|
let opr = self.parse_oper()?;
|
||||||
let fst = Box::new(self.parse_term(fid)?);
|
let fst = Box::new(self.parse_term(fid)?);
|
||||||
let snd = Box::new(self.parse_term(fid)?);
|
let snd = Box::new(self.parse_term(fid)?);
|
||||||
self.consume(")")?;
|
self.consume(")")?;
|
||||||
let end = *self.index() as u64;
|
let end = *self.index() as u64;
|
||||||
let src = Src::new(fid, ini, end);
|
let src = Src::new(fid, ini, end);
|
||||||
Ok(Term::Src { src, val: Box::new(Term::Op2 { opr, fst, snd }) })
|
return Ok(Term::Src { src, val: Box::new(Term::Op2 { opr, fst, snd }) });
|
||||||
}
|
}
|
||||||
Some('m') => {
|
|
||||||
self.consume("match")?;
|
// MAT ::= #match <name> = <term> { #0: <term>; #+: <term> }: <term>
|
||||||
|
// - The matched term is optional. Defaults to `Var { nam: <name> }`.
|
||||||
|
// - The return type is optional. Defaults to `Met {}`.
|
||||||
|
if self.starts_with("#match") {
|
||||||
|
let ini = *self.index() as u64;
|
||||||
|
self.consume("#match")?;
|
||||||
let nam = self.parse_name()?;
|
let nam = self.parse_name()?;
|
||||||
|
self.skip_trivia();
|
||||||
|
let x = if self.peek_one() == Some('=') {
|
||||||
self.consume("=")?;
|
self.consume("=")?;
|
||||||
let x = Box::new(self.parse_term(fid)?);
|
Box::new(self.parse_term(fid)?)
|
||||||
|
} else {
|
||||||
|
Box::new(Term::Var { nam: nam.clone() })
|
||||||
|
};
|
||||||
self.consume("{")?;
|
self.consume("{")?;
|
||||||
self.consume("#0")?;
|
self.consume("#0")?;
|
||||||
self.consume(":")?;
|
self.consume(":")?;
|
||||||
@ -148,82 +182,172 @@ impl<'i> KindParser<'i> {
|
|||||||
self.consume(":")?;
|
self.consume(":")?;
|
||||||
let s = Box::new(self.parse_term(fid)?);
|
let s = Box::new(self.parse_term(fid)?);
|
||||||
self.consume("}")?;
|
self.consume("}")?;
|
||||||
|
let p = if self.peek_one() == Some(':') {
|
||||||
self.consume(":")?;
|
self.consume(":")?;
|
||||||
let p = Box::new(self.parse_term(fid)?);
|
Box::new(self.parse_term(fid)?)
|
||||||
|
} else {
|
||||||
|
Box::new(Term::Met {})
|
||||||
|
};
|
||||||
let end = *self.index() as u64;
|
let end = *self.index() as u64;
|
||||||
let src = Src::new(fid, ini, end);
|
let src = Src::new(fid, ini, end);
|
||||||
Ok(Term::Src { src, val: Box::new(Term::Mat { nam, x, z, s, p }) })
|
return Ok(Term::Src { src, val: Box::new(Term::Mat { nam, x, z, s, p }) });
|
||||||
}
|
}
|
||||||
Some(_) => {
|
|
||||||
|
// NUM ::= #<uint>
|
||||||
|
if self.starts_with("#") {
|
||||||
|
let ini = *self.index() as u64;
|
||||||
|
self.advance_one();
|
||||||
let val = self.parse_u64()?;
|
let val = self.parse_u64()?;
|
||||||
let end = *self.index() as u64;
|
let end = *self.index() as u64;
|
||||||
let src = Src::new(fid, ini, end);
|
let src = Src::new(fid, ini, end);
|
||||||
Ok(Term::Src { src, val: Box::new(Term::Num { val }) })
|
return Ok(Term::Src { src, val: Box::new(Term::Num { val }) });
|
||||||
}
|
}
|
||||||
_ => {
|
|
||||||
self.expected("numeric-expression")
|
// HOL ::= ?<name>
|
||||||
}
|
if self.starts_with("?") {
|
||||||
}
|
|
||||||
}
|
|
||||||
Some('?') => {
|
|
||||||
let ini = *self.index() as u64;
|
let ini = *self.index() as u64;
|
||||||
self.consume("?")?;
|
self.advance_one();
|
||||||
let nam = self.parse_name()?;
|
let nam = self.parse_name()?;
|
||||||
let end = *self.index() as u64;
|
let end = *self.index() as u64;
|
||||||
let src = Src::new(fid, ini, end);
|
let src = Src::new(fid, ini, end);
|
||||||
Ok(Term::Src { src, val: Box::new(Term::Hol { nam }) })
|
return Ok(Term::Src { src, val: Box::new(Term::Hol { nam }) });
|
||||||
}
|
}
|
||||||
Some('_') => {
|
|
||||||
|
// MET ::= _
|
||||||
|
if self.starts_with("_") {
|
||||||
let ini = *self.index() as u64;
|
let ini = *self.index() as u64;
|
||||||
self.consume("_")?;
|
self.advance_one();
|
||||||
let end = *self.index() as u64;
|
let end = *self.index() as u64;
|
||||||
let src = Src::new(fid, ini, end);
|
let src = Src::new(fid, ini, end);
|
||||||
Ok(Term::Src { src, val: Box::new(Term::Met {}) })
|
return Ok(Term::Src { src, val: Box::new(Term::Met {}) });
|
||||||
}
|
}
|
||||||
Some('\'') => {
|
|
||||||
let ini = *self.index() as u64;
|
// TXT ::= "<string>"
|
||||||
let chr = self.parse_quoted_char()?;
|
if self.starts_with("\"") {
|
||||||
let end = *self.index() as u64;
|
|
||||||
let src = Src::new(fid, ini, end);
|
|
||||||
Ok(Term::Src { src, val: Box::new(Term::Num { val: chr as u64 }) })
|
|
||||||
}
|
|
||||||
Some('"') => {
|
|
||||||
let ini = *self.index() as u64;
|
let ini = *self.index() as u64;
|
||||||
let txt = self.parse_quoted_string()?;
|
let txt = self.parse_quoted_string()?;
|
||||||
let end = *self.index() as u64;
|
let end = *self.index() as u64;
|
||||||
let src = Src::new(fid, ini, end);
|
let src = Src::new(fid, ini, end);
|
||||||
Ok(Term::Src { src, val: Box::new(Term::Txt { txt }) })
|
return Ok(Term::Src { src, val: Box::new(Term::Txt { txt }) });
|
||||||
}
|
}
|
||||||
_ => {
|
|
||||||
if self.peek_many(4) == Some("let ") {
|
// LET ::= let <name> = <term> <term>
|
||||||
|
if self.starts_with("let ") {
|
||||||
let ini = *self.index() as u64;
|
let ini = *self.index() as u64;
|
||||||
self.advance_many(4);
|
self.consume("let ")?;
|
||||||
let nam = self.parse_name()?;
|
let nam = self.parse_name()?;
|
||||||
self.consume("=")?;
|
self.consume("=")?;
|
||||||
let val = Box::new(self.parse_term(fid)?);
|
let val = Box::new(self.parse_term(fid)?);
|
||||||
let bod = Box::new(self.parse_term(fid)?);
|
let bod = Box::new(self.parse_term(fid)?);
|
||||||
let end = *self.index() as u64;
|
let end = *self.index() as u64;
|
||||||
let src = Src::new(fid, ini, end);
|
let src = Src::new(fid, ini, end);
|
||||||
Ok(Term::Src { src, val: Box::new(Term::Let { nam, val, bod }) })
|
return Ok(Term::Src { src, val: Box::new(Term::Let { nam, val, bod }) });
|
||||||
} else if self.peek_many(4) == Some("use ") {
|
}
|
||||||
|
|
||||||
|
// USE ::= use <name> = <term> <term>
|
||||||
|
if self.starts_with("use ") {
|
||||||
let ini = *self.index() as u64;
|
let ini = *self.index() as u64;
|
||||||
self.advance_many(4);
|
self.consume("use ")?;
|
||||||
let nam = self.parse_name()?;
|
let nam = self.parse_name()?;
|
||||||
self.consume("=")?;
|
self.consume("=")?;
|
||||||
let val = Box::new(self.parse_term(fid)?);
|
let val = Box::new(self.parse_term(fid)?);
|
||||||
let bod = Box::new(self.parse_term(fid)?);
|
let bod = Box::new(self.parse_term(fid)?);
|
||||||
let end = *self.index() as u64;
|
let end = *self.index() as u64;
|
||||||
let src = Src::new(fid, ini, end);
|
let src = Src::new(fid, ini, end);
|
||||||
Ok(Term::Src { src, val: Box::new(Term::Use { nam, val, bod }) })
|
return Ok(Term::Src { src, val: Box::new(Term::Use { nam, val, bod }) });
|
||||||
} else {
|
}
|
||||||
|
|
||||||
|
// CHR ::= '<char>'
|
||||||
|
if self.starts_with("'") {
|
||||||
|
let ini = *self.index() as u64;
|
||||||
|
let chr = self.parse_quoted_char()?;
|
||||||
|
let end = *self.index() as u64;
|
||||||
|
let src = Src::new(fid, ini, end);
|
||||||
|
return Ok(Term::Src { src, val: Box::new(Term::Num { val: chr as u64 }) });
|
||||||
|
}
|
||||||
|
|
||||||
|
// LST ::= [ <term> , ... ]
|
||||||
|
if self.starts_with("[") {
|
||||||
|
let ini = *self.index() as u64;
|
||||||
|
self.consume("[")?;
|
||||||
|
let mut list = Vec::new();
|
||||||
|
while self.peek_one() != Some(']') {
|
||||||
|
list.push(Box::new(self.parse_term(fid)?));
|
||||||
|
self.skip_trivia();
|
||||||
|
if self.peek_one() == Some(',') {
|
||||||
|
self.consume(",")?;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
self.consume("]")?;
|
||||||
|
let end = *self.index() as u64;
|
||||||
|
let src = Src::new(fid, ini, end);
|
||||||
|
let val = Box::new(build_list(list));
|
||||||
|
return Ok(Term::Src { src, val });
|
||||||
|
}
|
||||||
|
|
||||||
|
// NAT ::= <uint>
|
||||||
|
if self.peek_one().map_or(false, |c| c.is_ascii_digit()) {
|
||||||
|
let ini = *self.index() as u64;
|
||||||
|
let nat = self.parse_u64()?;
|
||||||
|
let end = *self.index() as u64;
|
||||||
|
let src = Src::new(fid, ini, end);
|
||||||
|
return Ok(Term::Src { src, val: Box::new(Term::Nat { nat }) });
|
||||||
|
}
|
||||||
|
|
||||||
|
// MAT ::= match <name> = <term> { <name> : <term> <...> }: <term>
|
||||||
|
// The ADT match syntax is similar to the numeric match syntax, including the same optionals,
|
||||||
|
// but it allows any number of <name>:<term> cases. Also, similarly to the List syntax, there
|
||||||
|
// is no built-in "Mat" syntax on the Term type, so we must convert it to an applicative form:
|
||||||
|
// match x = val {
|
||||||
|
// List.cons: x.head
|
||||||
|
// List.nil: #0
|
||||||
|
// }: #U60
|
||||||
|
// Would be converted to:
|
||||||
|
// (~val _ (λx.head λx.tail x.tail) 0)
|
||||||
|
// Which is the same as:
|
||||||
|
// (APP (APP (APP (INS (VAR "val")) MET) (LAM "x.head" (LAM "x.tail" (VAR "x.head")))) (NUM 0))
|
||||||
|
// Note that, in our notation, fields are NOT written by the user. For example, this is WRONG:
|
||||||
|
// match x = val {
|
||||||
|
// (List.cons head tail): head
|
||||||
|
// List.nil: #0
|
||||||
|
// }: #U60
|
||||||
|
// Instead, we write only the constructors, and infer the fields from the datatype. To make
|
||||||
|
// this possible, we need to FIND the datatype that is currently matched. To do so, we get the
|
||||||
|
// first constructor name, remove the last `.part` (ex: `Foo.Bar.Tic.tac` will become
|
||||||
|
// `Foo.Bar.Tic`), and call the function `ADT::load(name: &str) -> ADT`. This will return a
|
||||||
|
// struct including the type's constructors and fields. We can then use it to create the
|
||||||
|
// lambdas when desugaring. For example, in the case above, the `λx.head` and `λx.tail` lambdas
|
||||||
|
// were created on the `List.cons` case, because the matched name is `x`, and the cons
|
||||||
|
// constructor has a `head` and a `tail` field.
|
||||||
|
|
||||||
|
// VAR ::= <name>
|
||||||
let ini = *self.index() as u64;
|
let ini = *self.index() as u64;
|
||||||
let nam = self.parse_name()?;
|
let nam = self.parse_name()?;
|
||||||
let end = *self.index() as u64;
|
let end = *self.index() as u64;
|
||||||
let src = Src::new(fid, ini, end);
|
let src = Src::new(fid, ini, end);
|
||||||
Ok(Term::Src { src, val: Box::new(Term::Var { nam }) })
|
return Ok(Term::Src { src, val: Box::new(Term::Var { nam }) });
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
// Builds a chain of applications of List.cons and List.nil from a Vec<Box<Term>>
|
||||||
|
fn build_list(list: Vec<Box<Term>>) -> Term {
|
||||||
|
let mut term = Term::App {
|
||||||
|
fun: Box::new(Term::Var { nam: "List.nil".to_string() }),
|
||||||
|
arg: Box::new(Term::Met {}),
|
||||||
|
};
|
||||||
|
for item in list.into_iter().rev() {
|
||||||
|
term = Term::App {
|
||||||
|
fun: Box::new(Term::App {
|
||||||
|
fun: Box::new(Term::App {
|
||||||
|
fun: Box::new(Term::Var { nam: "List.cons".to_string() }),
|
||||||
|
arg: Box::new(Term::Met {}),
|
||||||
|
}),
|
||||||
|
arg: item,
|
||||||
|
}),
|
||||||
|
arg: Box::new(term),
|
||||||
|
};
|
||||||
|
}
|
||||||
|
term
|
||||||
|
}
|
||||||
|
109
src/term/show.rs
109
src/term/show.rs
@ -1,109 +0,0 @@
|
|||||||
use crate::{*};
|
|
||||||
|
|
||||||
impl Oper {
|
|
||||||
|
|
||||||
pub fn show(&self) -> &'static str {
|
|
||||||
match self {
|
|
||||||
Oper::Add => "+",
|
|
||||||
Oper::Sub => "-",
|
|
||||||
Oper::Mul => "*",
|
|
||||||
Oper::Div => "/",
|
|
||||||
Oper::Mod => "%",
|
|
||||||
Oper::Eq => "==",
|
|
||||||
Oper::Ne => "!=",
|
|
||||||
Oper::Lt => "<",
|
|
||||||
Oper::Gt => ">",
|
|
||||||
Oper::Lte => "<=",
|
|
||||||
Oper::Gte => ">=",
|
|
||||||
Oper::And => "&",
|
|
||||||
Oper::Or => "|",
|
|
||||||
Oper::Xor => "^",
|
|
||||||
Oper::Lsh => "<<",
|
|
||||||
Oper::Rsh => ">>",
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
}
|
|
||||||
|
|
||||||
impl Term {
|
|
||||||
|
|
||||||
pub fn show(&self) -> String {
|
|
||||||
match self {
|
|
||||||
Term::All { nam, inp, bod } => {
|
|
||||||
let inp = inp.show();
|
|
||||||
let bod = bod.show();
|
|
||||||
format!("∀({}: {}) {}", nam, inp, bod)
|
|
||||||
},
|
|
||||||
Term::Lam { nam, bod } => {
|
|
||||||
let bod = bod.show();
|
|
||||||
format!("λ{} {}", nam, bod)
|
|
||||||
},
|
|
||||||
Term::App { fun, arg } => {
|
|
||||||
let fun = fun.show();
|
|
||||||
let arg = arg.show();
|
|
||||||
format!("({} {})", fun, arg)
|
|
||||||
},
|
|
||||||
Term::Ann { chk: _, val, typ } => {
|
|
||||||
let val = val.show();
|
|
||||||
let typ = typ.show();
|
|
||||||
format!("{{{}: {}}}", val, typ)
|
|
||||||
},
|
|
||||||
Term::Slf { nam, typ, bod } => {
|
|
||||||
let typ = typ.show();
|
|
||||||
let bod = bod.show();
|
|
||||||
format!("$({}: {}) {}", nam, typ, bod)
|
|
||||||
},
|
|
||||||
Term::Ins { val } => {
|
|
||||||
let val = val.show();
|
|
||||||
format!("~{}", val)
|
|
||||||
},
|
|
||||||
Term::Set => {
|
|
||||||
"*".to_string()
|
|
||||||
},
|
|
||||||
Term::U60 => {
|
|
||||||
"#U60".to_string()
|
|
||||||
},
|
|
||||||
Term::Num { val } => {
|
|
||||||
format!("#{}", val)
|
|
||||||
},
|
|
||||||
Term::Op2 { opr, fst, snd } => {
|
|
||||||
let fst = fst.show();
|
|
||||||
let snd = snd.show();
|
|
||||||
format!("#({} {} {})", opr.show(), fst, snd)
|
|
||||||
},
|
|
||||||
Term::Mat { nam, x, z, s, p } => {
|
|
||||||
let x = x.show();
|
|
||||||
let z = z.show();
|
|
||||||
let s = s.show();
|
|
||||||
let p = p.show();
|
|
||||||
format!("#match {} = {} {{ #0: {}; #+: {} }}: {}", nam, x, z, s, p)
|
|
||||||
},
|
|
||||||
Term::Txt { txt } => {
|
|
||||||
format!("\"{}\"", txt)
|
|
||||||
},
|
|
||||||
Term::Let { nam, val, bod } => {
|
|
||||||
let val = val.show();
|
|
||||||
let bod = bod.show();
|
|
||||||
format!("let {} = {} in {}", nam, val, bod)
|
|
||||||
},
|
|
||||||
Term::Use { nam, val, bod } => {
|
|
||||||
let val = val.show();
|
|
||||||
let bod = bod.show();
|
|
||||||
format!("use {} = {} in {}", nam, val, bod)
|
|
||||||
},
|
|
||||||
Term::Hol { nam } => {
|
|
||||||
format!("?{}", nam)
|
|
||||||
},
|
|
||||||
Term::Met {} => {
|
|
||||||
format!("_")
|
|
||||||
},
|
|
||||||
Term::Var { nam } => {
|
|
||||||
nam.clone()
|
|
||||||
},
|
|
||||||
Term::Src { src: _, val } => {
|
|
||||||
val.show()
|
|
||||||
},
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
}
|
|
Loading…
Reference in New Issue
Block a user