summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/context.rs5
-rw-r--r--src/core.rs62
-rw-r--r--src/grammar.lalrpop7
-rw-r--r--src/lexer.rs10
-rw-r--r--src/typecheck.rs24
5 files changed, 50 insertions, 58 deletions
diff --git a/src/context.rs b/src/context.rs
index 4d6abf2..b72182d 100644
--- a/src/context.rs
+++ b/src/context.rs
@@ -1,4 +1,3 @@
-use std::borrow::Cow;
use std::collections::HashMap;
/// A `(Context a)` associates `Text` labels with values of type `a`
@@ -14,7 +13,7 @@ use std::collections::HashMap;
/// `n`th occurrence of a given key.
///
#[derive(Debug, Clone)]
-pub struct Context<'i, T>(HashMap<Cow<'i, str>, Vec<T>>);
+pub struct Context<'i, T>(HashMap<&'i str, Vec<T>>);
impl<'i, T> Context<'i, T> {
/// An empty context with no key-value pairs
@@ -41,7 +40,7 @@ impl<'i, T> Context<'i, T> {
impl<'i, T: Clone> Context<'i, T> {
/// Add a key-value pair to the `Context`
- pub fn insert(&self, k: Cow<'i, str>, v: T) -> Self {
+ pub fn insert(&self, k: &'i str, v: T) -> Self {
let mut ctx = (*self).clone();
{
let m = ctx.0.entry(k).or_insert(vec![]);
diff --git a/src/core.rs b/src/core.rs
index 5bf90db..0bc42d4 100644
--- a/src/core.rs
+++ b/src/core.rs
@@ -1,5 +1,4 @@
#![allow(non_snake_case)]
-use std::borrow::Cow;
use std::collections::HashMap;
use std::path::PathBuf;
@@ -95,8 +94,8 @@ pub enum Path {
/// Zero indices are omitted when pretty-printing `Var`s and non-zero indices
/// appear as a numeric suffix.
///
-#[derive(Debug, Clone, PartialEq, Eq)] // (Eq, Show)
-pub struct V<'i>(pub Cow<'i, str>, pub usize);
+#[derive(Debug, Copy, Clone, PartialEq, Eq)] // (Eq, Show)
+pub struct V<'i>(pub &'i str, pub usize);
/*
instance IsString Var where
@@ -115,15 +114,15 @@ pub enum Expr<'i, S, A> {
/// `Var (V x n) ~ x@n`
Var(V<'i>),
/// `Lam x A b ~ λ(x : A) -> b`
- Lam(Cow<'i, str>, Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
+ Lam(&'i str, Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
/// `Pi "_" A B ~ A -> B`
/// `Pi x A B ~ ∀(x : A) -> B`
- Pi(Cow<'i, str>, Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
+ Pi(&'i str, Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
/// `App f A ~ f A`
App(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
/// `Let x Nothing r e ~ let x = r in e`
/// `Let x (Just t) r e ~ let x : t = r in e`
- Let(Cow<'i, str>, Option<Box<Expr<'i, S, A>>>, Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
+ Let(&'i str, Option<Box<Expr<'i, S, A>>>, Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
/// `Annot x t ~ x : t`
Annot(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
/// `Bool ~ Bool`
@@ -198,19 +197,19 @@ pub enum Expr<'i, S, A> {
/// `OptionalFold ~ Optional/fold`
OptionalFold,
/// `Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 }`
- Record(HashMap<Cow<'i, str>, Expr<'i, S, A>>),
+ Record(HashMap<&'i str, Expr<'i, S, A>>),
/// `RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 }`
- RecordLit(HashMap<Cow<'i, str>, Expr<'i, S, A>>),
+ RecordLit(HashMap<&'i str, Expr<'i, S, A>>),
/// `Union [(k1, t1), (k2, t2)] ~ < k1 : t1, k2 : t2 >`
- Union(HashMap<Cow<'i, str>, Expr<'i, S, A>>),
+ Union(HashMap<&'i str, Expr<'i, S, A>>),
/// `UnionLit (k1, v1) [(k2, t2), (k3, t3)] ~ < k1 = t1, k2 : t2, k3 : t3 >`
- UnionLit(Cow<'i, str>, Box<Expr<'i, S, A>>, HashMap<Cow<'i, str>, Expr<'i, S, A>>),
+ UnionLit(&'i str, Box<Expr<'i, S, A>>, HashMap<&'i str, Expr<'i, S, A>>),
/// `Combine x y ~ x ∧ y`
Combine(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
/// `Merge x y t ~ merge x y : t`
Merge(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
/// `Field e x ~ e.x`
- Field(Box<Expr<'i, S, A>>, Cow<'i, str>),
+ Field(Box<Expr<'i, S, A>>, &'i str),
/// `Note S x ~ e`
Note(S, Box<Expr<'i, S, A>>),
/// `Embed path ~ path`
@@ -254,18 +253,18 @@ impl<'i, S, A> Expr<'i, S, A> {
impl<'i> From<&'i str> for V<'i> {
fn from(s: &'i str) -> Self {
- V(Cow::Borrowed(s), 0)
+ V(s, 0)
}
}
impl<'i, S, A> From<&'i str> for Expr<'i, S, A> {
fn from(s: &'i str) -> Self {
- Expr::Var(V(Cow::Borrowed(s), 0))
+ Expr::Var(s.into())
}
}
pub fn pi<'i, S, A, Name, Et, Ev>(var: Name, ty: Et, value: Ev) -> Expr<'i, S, A>
- where Name: Into<Cow<'i, str>>,
+ where Name: Into<&'i str>,
Et: Into<Expr<'i, S, A>>,
Ev: Into<Expr<'i, S, A>>
{
@@ -378,30 +377,28 @@ pub fn shift<'i, S, T, A>(d: isize, v: V, e: Expr<'i, S, A>) -> Expr<'i, T, A>
A: ::std::fmt::Debug,
{
use Expr::*;
+ let V(x, n) = v;
match e {
Const(a) => Const(a),
Var(V(x2, n2)) => {
- let V(x, n) = v;
let n3 = if x == x2 && n <= n2 { add_ui(n2, d) } else { n2 };
Var(V(x2, n3))
}
Lam(x2, tA, b) => {
- let V(x, n) = v;
let n2 = if x == x2 { n + 1 } else { n };
- let tA2 = shift(d, V(x.clone(), n ), *tA);
- let b2 = shift(d, V(x, n2), *b);
+ let tA2 = shift(d, V(x, n ), *tA);
+ let b2 = shift(d, V(x, n2), *b);
Lam(x2, bx(tA2), bx(b2))
}
Pi(x2, tA, tB) => {
- let V(x, n) = v;
let n2 = if x == x2 { n + 1 } else { n };
- let tA2 = shift(d, V(x.clone(), n ), *tA);
+ let tA2 = shift(d, V(x, n ), *tA);
let tB2 = shift(d, V(x, n2), *tB);
pi(x2, tA2, tB2)
}
App(f, a) => {
- let f2 = shift(d, v.clone(), *f);
- let a2 = shift(d, v, *a);
+ let f2 = shift(d, v, *f);
+ let a2 = shift(d, v, *a);
App(bx(f2), bx(a2))
}
/*
@@ -419,7 +416,7 @@ shift d v (Annot a b) = Annot a' b'
b' = shift d v b
*/
BoolLit(a) => BoolLit(a),
- BoolAnd(a, b) => BoolAnd(bx(shift(d, v.clone(), *a)), bx(shift(d, v, *b))),
+ BoolAnd(a, b) => BoolAnd(bx(shift(d, v, *a)), bx(shift(d, v, *b))),
/*
shift d v (BoolOr a b) = BoolOr a' b'
where
@@ -533,30 +530,29 @@ pub fn subst<'i, S, T, A>(v: V<'i>, a: Expr<'i, S, A>, b: Expr<'i, T, A>) -> Exp
A: Clone + ::std::fmt::Debug,
{
use Expr::*;
+ let V(x, n) = v;
match (a, b) {
(_, Const(a)) => Const(a),
(e, Lam(y, tA, b)) => {
- let V(x, n) = v;
let n2 = if x == y { n + 1 } else { n };
- let tA2 = subst(V(x.clone(), n), e.clone(), *tA);
- let b2 = subst(V(x, n2), shift(1, V(y.clone(), 0), e), *b);
+ let tA2 = subst(V(x, n), e.clone(), *tA);
+ let b2 = subst(V(x, n2), shift(1, V(y, 0), e), *b);
Lam(y, bx(tA2), bx(b2))
}
(e, Pi(y, tA, tB)) => {
- let V(x, n) = v;
let n2 = if x == y { n + 1 } else { n };
- let tA2 = subst(V(x.clone(), n), e.clone(), *tA);
- let tB2 = subst(V(x, n2), shift(1, V(y.clone(), 0), e), *tB);
+ let tA2 = subst(V(x, n), e.clone(), *tA);
+ let tB2 = subst(V(x, n2), shift(1, V(y, 0), e), *tB);
pi(y, tA2, tB2)
}
(e, App(f, a)) => {
- let f2 = subst(v.clone(), e.clone(), *f);
+ let f2 = subst(v, e.clone(), *f);
let a2 = subst(v, e, *a);
app(f2, a2)
}
(e, Var(v2)) => if v == v2 { e } else { Var(v2) },
(e, ListLit(a, b)) => {
- let b2 = b.into_iter().map(|be| subst(v.clone(), e.clone(), be)).collect();
+ let b2 = b.into_iter().map(|be| subst(v, e.clone(), be)).collect();
let a2 = subst(v, e, *a);
ListLit(bx(a2), b2)
}
@@ -599,8 +595,8 @@ pub fn normalize<S, T, A>(e: Expr<S, A>) -> Expr<T, A>
App(f, a) => match normalize::<S, T, A>(*f) {
Lam(x, _A, b) => { // Beta reduce
let vx0 = V(x, 0);
- let a2 = shift::<S, S, A>( 1, vx0.clone(), *a);
- let b2 = subst::<S, T, A>(vx0.clone(), a2, *b);
+ let a2 = shift::<S, S, A>( 1, vx0, *a);
+ let b2 = subst::<S, T, A>(vx0, a2, *b);
let b3 = shift::<S, T, A>(-1, vx0, b2);
normalize(b3)
}
diff --git a/src/grammar.lalrpop b/src/grammar.lalrpop
index 91f8b8d..63c17ad 100644
--- a/src/grammar.lalrpop
+++ b/src/grammar.lalrpop
@@ -4,7 +4,6 @@ use core::Expr::*;
use grammar_util::*;
use lexer::*;
-use std::borrow::Cow;
use std::collections::HashMap;
use std::iter;
use std::iter::FromIterator;
@@ -25,7 +24,7 @@ extern {
Nat => Tok::Natural(<usize>),
Text => Tok::Text(<String>),
Bool => Tok::Bool(<bool>),
- Label => Tok::Identifier(<Cow<'input, str>>),
+ Label => Tok::Identifier(<&'input str>),
Const => Tok::Const(<core::Const>),
Let => Tok::Keyword(Keyword::Let),
In => Tok::Keyword(Keyword::In),
@@ -65,7 +64,7 @@ ExprB: BoxExpr<'input> = {
Lambda "(" <Label> ":" <Expr> ")" "->" <ExprB> => bx(Lam(<>)),
Pi "(" <Label> ":" <Expr> ")" "->" <ExprB> => bx(Pi(<>)),
If <Expr> Then <ExprB> Else <ExprC> => bx(BoolIf(<>)),
- <ExprC> "->" <ExprB> => bx(Pi(Cow::Borrowed("_"), <>)),
+ <ExprC> "->" <ExprB> => bx(Pi("_", <>)),
Let <Label> <(":" <Expr>)?> "=" <Expr> In <ExprB> => bx(Let(<>)),
"[" <a:Elems> "]" ":" <b:ListLike> <c:ExprE> => bx(b(c, a)),
ExprC,
@@ -157,6 +156,6 @@ Record: BoxExpr<'input> = {
FieldValues = SepBy1<",", Field<"=">>;
FieldTypes = SepBy<",", Field<":">>;
-Field<Sep>: (Cow<'input, str>, ParsedExpr<'input>) = {
+Field<Sep>: (&'input str, ParsedExpr<'input>) = {
<a:Label> Sep <b:Expr> => (a, *b),
};
diff --git a/src/lexer.rs b/src/lexer.rs
index ca181ce..499f762 100644
--- a/src/lexer.rs
+++ b/src/lexer.rs
@@ -2,8 +2,6 @@ use nom;
use core::Const;
-use std::borrow::Cow;
-
#[derive(Debug, PartialEq, Eq)]
pub enum Keyword {
Let,
@@ -43,7 +41,7 @@ pub enum Builtin {
#[derive(Debug, PartialEq, Eq)]
pub enum Tok<'i> {
- Identifier(Cow<'i, str>),
+ Identifier(&'i str),
Keyword(Keyword),
Builtin(Builtin),
ListLike(ListLike),
@@ -260,7 +258,7 @@ named!(token<&str, Tok>, alt!(
map!(list_like, Tok::ListLike) |
map!(natural, Tok::Natural) |
map!(integer, Tok::Integer) |
- map!(identifier, |s| Tok::Identifier(Cow::Borrowed(s))) |
+ map!(identifier, Tok::Identifier) |
map!(string_lit, Tok::Text) |
value!(Tok::BraceL, tag!("{")) |
@@ -371,12 +369,12 @@ fn test_lex() {
let s = "λ(b : Bool) → b == False";
let expected = [Lambda,
ParenL,
- Identifier(Cow::Borrowed("b")),
+ Identifier("b"),
Ascription,
Builtin(self::Builtin::Bool),
ParenR,
Arrow,
- Identifier(Cow::Borrowed("b")),
+ Identifier("b"),
CompareEQ,
Bool(false)];
let lexer = Lexer::new(s);
diff --git a/src/typecheck.rs b/src/typecheck.rs
index e552de5..36d75e4 100644
--- a/src/typecheck.rs
+++ b/src/typecheck.rs
@@ -29,12 +29,12 @@ fn rule(a: core::Const, b: core::Const) -> Result<core::Const, ()> {
fn match_vars(vl: &V, vr: &V, ctx: &[(&str, &str)]) -> bool {
let xxs = ctx.get(0).map(|x| (x, ctx.split_at(1).1));
match (vl, vr, xxs) {
- (&V(ref xL, nL), &V(ref xR, nR), None) => xL == xR && nL == nR,
- (&V(ref xL, 0), &V(ref xR, 0), Some((&(ref xL2, ref xR2), _))) if xL == xL2 && xR == xR2 => true,
- (&V(ref xL, nL), &V(ref xR, nR), Some((&(ref xL2, ref xR2), xs))) => {
- let nL2 = if *xL == xL2.as_ref() { nL - 1 } else { nL };
- let nR2 = if *xR == xR2.as_ref() { nR - 1 } else { nR };
- match_vars(&V(xL.clone(), nL2), &V(xR.clone(), nR2), xs)
+ (&V(xL, nL), &V(xR, nR), None) => xL == xR && nL == nR,
+ (&V(xL, 0), &V(xR, 0), Some((&(xL2, xR2), _))) if xL == xL2 && xR == xR2 => true,
+ (&V(xL, nL), &V(xR, nR), Some((&(xL2, xR2), xs))) => {
+ let nL2 = if xL == xL2 { nL - 1 } else { nL };
+ let nR2 = if xR == xR2 { nR - 1 } else { nR };
+ match_vars(&V(xL, nL2), &V(xR, nR2), xs)
}
}
}
@@ -126,9 +126,9 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
.ok_or_else(|| TypeError::new(ctx, &e, UnboundVariable))
}
&Lam(ref x, ref tA, ref b) => {
- let ctx2 = ctx.insert(x.clone(), (**tA).clone()).map(|e| core::shift(1, V(x.clone(), 0), e.clone()));
+ let ctx2 = ctx.insert(x, (**tA).clone()).map(|e| core::shift(1, V(x, 0), e.clone()));
let tB = type_with(&ctx2, b)?;
- let p = Pi(x.clone(), tA.clone(), bx(tB));
+ let p = Pi(x, tA.clone(), bx(tB));
let _ = type_with(ctx, &p)?;
//Ok(Cow::Owned(p))
Ok(p)
@@ -140,7 +140,7 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
_ => return Err(TypeError::new(ctx, e, InvalidInputType((**tA).clone()))),
};
- let ctx2 = ctx.insert(x.clone(), (**tA).clone()).map(|e| core::shift(1, V(x.clone(), 0), e.clone()));
+ let ctx2 = ctx.insert(x, (**tA).clone()).map(|e| core::shift(1, V(x, 0), e.clone()));
let tB = normalize(type_with(&ctx2, tB)?);
let kB = match tB {
Const(k) => k,
@@ -161,8 +161,8 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
let tA2 = type_with(ctx, a)?;
if prop_equal(&tA, &tA2) {
let vx0 = V(x, 0);
- let a2 = shift::<S, S, X>( 1, vx0.clone(), (**a).clone());
- let tB2 = subst(vx0.clone(), a2, (*tB).clone());
+ let a2 = shift::<S, S, X>( 1, vx0, (**a).clone());
+ let tB2 = subst(vx0, a2, (*tB).clone());
let tB3 = shift::<S, S, X>(-1, vx0, tB2);
Ok(tB3)
} else {
@@ -181,7 +181,7 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
_ => return Err(TypeError::new(ctx, &e, InvalidInputType(tR))),
};
- let ctx2 = ctx.insert(f.clone(), tR.clone());
+ let ctx2 = ctx.insert(f, tR.clone());
let tB = type_with(&ctx2, b)?;
let ttB = normalize::<S, S, X>(type_with(ctx, &tB)?);
let kB = match ttB {
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-28 04:19:06 +0000