diff options
| -rw-r--r-- | grammar.txt | 2 | ||||
| -rw-r--r-- | src/ast.rs | 2 | ||||
| -rw-r--r-- | src/main.rs | 2 | ||||
| -rw-r--r-- | src/parser.rs | 5 |
4 files changed, 6 insertions, 5 deletions
diff --git a/grammar.txt b/grammar.txt index 607d759..516a248 100644 --- a/grammar.txt +++ b/grammar.txt @@ -13,7 +13,7 @@ set_field = "." , lower_ident , ":" , set ; variant_set = "variant" , "[" , [ variant_field { "|" , variant_field } ] , "]" ; variant_field = lower_ident , "." , ":" , set ; builtin_set = "Nat" | "Int" | "Float" | "Str" | "Bool" ; -claimed_set = "set" , "(" , instance , ")" ; +claimed_set = "set-of" , "(" , instance , ")" ; signature = "Set" | theory_sig | function_sig | sig_var | "(" , signature , ")" ; theory_sig = "theory" , "{" , [ sig_field { "," , sig_field } ] , "}" ; @@ -36,7 +36,7 @@ pub enum Set { #[display("variant [ {} ]", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" | "))] Variant(Vec<VariantField>), - #[display("set({_0})")] + #[display("set-of({_0})")] ClaimedSet(Instance), #[display("{_0}")] diff --git a/src/main.rs b/src/main.rs index c57eef6..984a438 100644 --- a/src/main.rs +++ b/src/main.rs @@ -46,7 +46,7 @@ let element compute : Nat = case injected of [ z. myz => myz .y .n | f. myf => 2 // .Edge = for (s : Nat) (t : Nat), Bool // } // -// let element node : set(natPoset .Node) = 7 +// let element node : set-of(natPoset .Node) = 7 "#; let programme = parser::parser::program(src); diff --git a/src/parser.rs b/src/parser.rs index 958f09d..4599f7e 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -32,6 +32,7 @@ parser! { rule kw_of() = "of" wb() rule kw_for() = "for" wb() rule kw_set() = "set" wb() + rule kw_set_of() = "set-of" wb() rule kw_Set() = "Set" wb() rule kw_Nat() = "Nat" wb() rule kw_Int() = "Int" wb() @@ -116,7 +117,7 @@ parser! { = n:inject_lower() _ ":" _ s:set() _ { VariantField { name: n, set: s } } rule claimed_set() -> Instance - = kw_set() "(" _ i:instance() _ ")" { i } + = kw_set_of() "(" _ i:instance() _ ")" { i } rule set() -> Set = kw_record() _ "{" fs:(set_field() ** ",") _ "}" { Set::Record(fs) } @@ -285,7 +286,7 @@ let set Maybe = variant [ .Edge = for (s : Nat) (t : Nat), Bool } - let element node : set(natPoset .Node) = 7 + let element node : set-of(natPoset .Node) = 7 "#; debug_parse(src); |