aboutsummaryrefslogtreecommitdiff
path: root/src/parser.rs
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser.rs')
-rw-r--r--src/parser.rs32
1 files changed, 19 insertions, 13 deletions
diff --git a/src/parser.rs b/src/parser.rs
index 4599f7e..6810927 100644
--- a/src/parser.rs
+++ b/src/parser.rs
@@ -111,10 +111,10 @@ parser! {
// set layer
rule set_field() -> RecordField
- = n:project_lower() _ ":" _ s:set() { RecordField { name: n, set: s } }
+ = _ n:lower_ident() _ ":" _ s:set() { RecordField { name: n, set: s } }
rule variant_field() -> VariantField
- = n:inject_lower() _ ":" _ s:set() _ { VariantField { name: n, set: s } }
+ = _ n:lower_ident() _ ":" _ s:set() _ { VariantField { name: n, set: s } }
rule claimed_set() -> Instance
= kw_set_of() "(" _ i:instance() _ ")" { i }
@@ -135,7 +135,7 @@ parser! {
rule param_list() -> Vec<Param> = param() ++ _
rule sig_field() -> SigField
- = n:project_upper() _ "::" _ s:signature() { SigField { name: n, signature: s } }
+ = _ n:upper_ident() _ "::" _ s:signature() { SigField { name: n, signature: s } }
rule signature() -> Signature
= kw_Set() { Signature::Set }
@@ -176,7 +176,7 @@ parser! {
// instance layer
rule inst_assign() -> InstAssign
- = n:project() _ "=" _ i:instance()
+ = n:project_upper() _ "=" _ i:instance()
{ InstAssign { name: n, instance: i } }
rule atom_inst() -> Instance
@@ -244,16 +244,16 @@ mod tests {
fn test_sets() {
let src = r#"
let set Config = record {
- .enabled : Bool,
- .count : Nat,
- .offset : Int,
- .scale : Float,
- .label : Str
+ enabled : Bool,
+ count : Nat,
+ offset : Int,
+ scale : Float,
+ label : Str
}
let set Maybe = variant [
- none. : record {}
- | some. : Config
+ none : record {}
+ | some : Config
]
"#;
@@ -277,8 +277,8 @@ let set Maybe = variant [
fn test_theories_and_instances() {
let src = r#"
let signature Graph = theory {
- .Node :: Set,
- .Edge :: (s : Node) (t : Node) -> Set
+ Node :: Set,
+ Edge :: (s : Node) (t : Node) -> Set
}
let instance natPoset :: Graph = {
@@ -287,6 +287,12 @@ let set Maybe = variant [
}
let element node : set-of(natPoset .Node) = 7
+
+ let set NatEdges = record {
+ source: set-of(natPoset .Node),
+ target: set-of(natPoset .Node),
+ connected: set-of(natPoset .Edge source target)
+ }
"#;
debug_parse(src);