aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/main.rs34
-rw-r--r--src/parser.rs32
2 files changed, 36 insertions, 30 deletions
diff --git a/src/main.rs b/src/main.rs
index 7d04891..491f6d6 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -20,34 +20,34 @@ fn main() {
let src = r#"
// let X be the set Y, call it Z
-let set X = record { .b : Bool, .n : Nat }
+let set X = record { b : Bool, n : Nat }
let set Y = X
-let set Z = record { .y : Y }
+let set Z = record { y : Y }
// make some elements
let element x : X = { .b = true, .n = 41 }
let element z : Z = { .y = x }
// exercise case matching
-let set Z_or_Float = variant [ z. : Z | f. : Float ]
+let set Z_or_Float = variant [ z : Z | f : Float ]
let element injected : Z_or_Float = z. z
let element check_cases : Nat = case injected of [ z. myz => myz .y .n | f. myf => 2 ]
let signature Graph = theory {
- .Node :: Set,
- .Edge :: (s : Node) (t : Node) -> Set
+ Node :: Set,
+ Edge :: (s : Node) (t : Node) -> Set
}
-// let instance natPoset :: Graph = {
-// .Node = Nat,
-// .Edge = for (s : Nat) (t : Nat), Bool
-// }
-//
-// 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)
-// }
+let instance natPoset :: Graph = {
+ .Node = Nat,
+ .Edge = for (s : Nat) (t : Nat), Bool
+}
+
+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)
+}
"#;
let programme = parser::parser::program(src);
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);