mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-09-11 08:45:32 +03:00
Annotated lambdas
This commit is contained in:
parent
14b16122e7
commit
5a13856ada
6
Cargo.lock
generated
6
Cargo.lock
generated
@ -108,9 +108,9 @@ checksum = "809e18805660d7b6b2e2b9f316a5099521b5998d5cba4dda11b5157a21aaef03"
|
||||
|
||||
[[package]]
|
||||
name = "hvm"
|
||||
version = "0.1.70"
|
||||
version = "0.1.73"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "9b77c523f458e772df8ad9226d455907511d00c9596f0093500d1d09e7c3052d"
|
||||
checksum = "3a227613b46d330d50ee2fd4a4e1dbdd574dd4fcec7b2465694b84f49aba1592"
|
||||
dependencies = [
|
||||
"clap",
|
||||
"highlight_error",
|
||||
@ -140,7 +140,7 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "kind2"
|
||||
version = "0.2.49"
|
||||
version = "0.2.56"
|
||||
dependencies = [
|
||||
"clap",
|
||||
"highlight_error",
|
||||
|
@ -1,6 +1,6 @@
|
||||
[package]
|
||||
name = "kind2"
|
||||
version = "0.2.56"
|
||||
version = "0.2.57"
|
||||
edition = "2021"
|
||||
description = "A pure functional functional language that uses the HVM."
|
||||
repository = "https://github.com/Kindelia/Kind2"
|
||||
|
@ -793,11 +793,23 @@ pub fn parse_all(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
|
||||
let (state, _) = parser::consume(":", state)?;
|
||||
let (state, tipo) = parse_apps(state)?;
|
||||
let (state, _) = parser::consume(")", state)?;
|
||||
let (state, _) = parser::text("->", state)?;
|
||||
let (state, body) = parse_apps(state)?;
|
||||
let (state, last) = get_last_index(state)?;
|
||||
let orig = origin(0, init, last);
|
||||
Ok((state, Box::new(Term::All { orig, name, tipo, body })))
|
||||
let (state, isfn) = parser::text("=>", state)?;
|
||||
if isfn {
|
||||
let (state, body) = parse_apps(state)?;
|
||||
let (state, last) = get_last_index(state)?;
|
||||
let orig = origin(0, init, last);
|
||||
Ok((state, Box::new(Term::Ann {
|
||||
orig,
|
||||
expr: Box::new(Term::Lam { orig, name: name.clone(), body }),
|
||||
tipo: Box::new(Term::All { orig, name: name.clone(), tipo, body: Box::new(Term::Hol { orig, numb: 0 }) }),
|
||||
})))
|
||||
} else {
|
||||
let (state, _) = parser::text("->", state)?;
|
||||
let (state, body) = parse_apps(state)?;
|
||||
let (state, last) = get_last_index(state)?;
|
||||
let orig = origin(0, init, last);
|
||||
Ok((state, Box::new(Term::All { orig, name, tipo, body })))
|
||||
}
|
||||
}),
|
||||
state,
|
||||
)
|
||||
|
Loading…
Reference in New Issue
Block a user