From 0886a16d73145270e953b8c2e0a4452b518ea16e Mon Sep 17 00:00:00 2001 From: tslil Date: Fri, 1 May 2026 12:36:24 +0100 Subject: working on fixing app, rework ast to have generics etc --- src/ast.rs | 83 +++++++++---------- src/checker_set.rs | 26 +++--- src/checker_signature.rs | 71 +++++++++------- src/checker_state.rs | 41 +++++----- src/main.rs | 63 +++++++------- src/parser.rs | 209 +++++++++++++++++++++++------------------------ 6 files changed, 253 insertions(+), 240 deletions(-) (limited to 'src') diff --git a/src/ast.rs b/src/ast.rs index fab1236..76b6c9f 100644 --- a/src/ast.rs +++ b/src/ast.rs @@ -1,28 +1,35 @@ use derive_more::Display; -// Set layer +// Generic + +pub trait TypingSignifier { + const SIGNIFIER: &'static str; +} #[derive(Clone, PartialEq, Display, Debug)] -pub enum BuiltIn { - Nat, - Int, - Float, - Str, - Bool, +#[display(".{tag} {bound} => {body}")] +pub struct CaseArm { + pub tag: String, + pub bound: String, + pub body: T, } #[derive(Clone, PartialEq, Display, Debug)] -#[display("{name} : {set}")] -pub struct RecordField { +#[display("{name} {} {carries}", T::SIGNIFIER)] +pub struct Field { pub name: String, - pub set: Set, + pub carries: T, } +// Set layer + #[derive(Clone, PartialEq, Display, Debug)] -#[display("{name} : {set}")] -pub struct VariantField { - pub name: String, - pub set: Set, +pub enum BuiltIn { + Nat, + Int, + Float, + Str, + Bool, } #[derive(Clone, PartialEq, Display, Debug)] @@ -31,10 +38,10 @@ pub enum Set { BuiltIn(BuiltIn), #[display("record {{ {} }}", _0.iter().map(|f| f.to_string()).collect::>().join(" , "))] - Record(Vec), + Record(Vec>), #[display("variant [ {} ]", _0.iter().map(|f| f.to_string()).collect::>().join(" | "))] - Variant(Vec), + Variant(Vec>), #[display("set-of({_0})")] ClaimedSet(Instance), @@ -43,6 +50,10 @@ pub enum Set { Var(String), } +impl TypingSignifier for Set { + const SIGNIFIER: &'static str = ":"; +} + // Signature layer #[derive(Clone, PartialEq, Display, Debug)] @@ -52,20 +63,13 @@ pub struct Param { pub set: Set, } -#[derive(Clone, PartialEq, Display, Debug)] -#[display("{name} :: {signature}")] -pub struct SigField { - pub name: String, - pub signature: Signature, -} - #[derive(Clone, PartialEq, Display, Debug)] pub enum Signature { #[display("Set")] Set, #[display("theory {{ {} }}", _0.iter().map(|f| f.to_string()).collect::>().join(" , "))] - Theory(Vec), + Theory(Vec>), #[display("{} -> {}", params.iter().map(|p| p.to_string()).collect::>().join(", "), codomain)] Ext { @@ -77,6 +81,10 @@ pub enum Signature { Var(String), } +impl TypingSignifier for Signature { + const SIGNIFIER: &'static str = "::"; +} + // Element layer #[derive(Clone, PartialEq, Display, Debug)] @@ -95,14 +103,6 @@ pub struct ElemAssign { pub element: Element, } -#[derive(Clone, PartialEq, Display, Debug)] -#[display(".{tag} {bound} => {body}")] -pub struct CaseArm { - pub tag: String, - pub bound: String, - pub body: Element, -} - #[derive(Clone, PartialEq, Display, Debug)] pub enum Element { #[display("{_0}")] @@ -129,7 +129,7 @@ pub enum Element { #[display("case {} of {{ {} }}", scrutinee, arms.iter().map(|a| a.to_string()).collect::>().join(" | "))] Case { scrutinee: Box, - arms: Vec, + arms: Vec>, }, } @@ -142,14 +142,6 @@ pub struct InstAssign { pub instance: Instance, } -#[derive(Clone, PartialEq, Display, Debug)] -#[display(".{tag} {bound} => {body}")] -pub struct InstCaseArm { - pub tag: String, - pub bound: String, - pub body: Instance, -} - #[derive(Clone, PartialEq, Display, Debug)] pub enum Instance { #[display("({_0} :: Set)")] @@ -167,8 +159,11 @@ pub enum Instance { body: Box, }, - #[display("{_0} {_1}")] - App(Box, Box), + #[display("{instance} {}", args.iter().map(|e| e.to_string()).collect::>().join(" "))] + App { + instance: Box, + args: Vec, + }, #[display("{instance} .{field}")] Project { @@ -179,7 +174,7 @@ pub enum Instance { #[display("case {} of [ {} ]", scrutinee, arms.iter().map(|a| a.to_string()).collect::>().join(" | "))] Case { scrutinee: Box, - arms: Vec, + arms: Vec>, }, } diff --git a/src/checker_set.rs b/src/checker_set.rs index 6ef8182..626f74d 100644 --- a/src/checker_set.rs +++ b/src/checker_set.rs @@ -13,12 +13,12 @@ impl CheckerState { let mut ctx = self.clone(); let fields = fields .into_iter() - .map(|RecordField { name, set }| { - let set = ctx.check_set(set)?; + .map(|Field { name, carries }| { + let set = ctx.check_set(carries)?; ctx.add_element(name.clone(), ElementValue::Hypothetical, set.clone())?; - Ok(RecordField { + Ok(Field { name: name.clone(), - set, + carries: set, }) }) .collect::, _>>()?; @@ -27,11 +27,11 @@ impl CheckerState { Set::Variant(fields) => { let fields = fields .into_iter() - .map(|VariantField { name, set }| { - let set = self.check_set(set)?; - Ok(VariantField { + .map(|Field { name, carries }| { + let set = self.check_set(carries)?; + Ok(Field { name: name.clone(), - set, + carries: set, }) }) .collect::, _>>()?; @@ -161,9 +161,9 @@ impl CheckerState { let sub_elements = fields .iter() .map( - |RecordField { + |Field { name: f_n, - set: f_s, + carries: f_s, }| { let f_e = assignations .get(f_n) @@ -188,7 +188,7 @@ impl CheckerState { } => { // globally unique projections mean we know what the sets going // in and out must be - let Field { + let OwnedField { field: field_set, owner: owner_set, } = self.lookup_record_field(&field)?; @@ -238,7 +238,7 @@ impl CheckerState { // globally unique injections mean that we know what the sets // going in and out must be, but compared to projections their // roles are here interchanged - let Field { + let OwnedField { field: field_set, owner: owner_set, } = self.lookup_variant_field(&field)?; @@ -327,7 +327,7 @@ impl CheckerState { let mut computed_output = None; let mut processed_arms = Vec::new(); for arm in arms { - let Field { + let OwnedField { field: field_set, .. } = self.lookup_variant_field(&arm.tag)?; diff --git a/src/checker_signature.rs b/src/checker_signature.rs index bad38eb..2d5057f 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -31,8 +31,8 @@ impl CheckerState { let mut ctx = self.clone(); let temp_name = ctx.make_unique_name(); let mut new_fields = Vec::new(); - for SigField { signature, name } in fields { - let signature = ctx.check_signature(signature)?; + for Field { carries, name } in fields { + let signature = ctx.check_signature(carries)?; ctx.add_instance(name.clone(), InstanceValue::Hypothetical, signature.clone())?; // And lo, the special case, our chosen canonical form if signature == Signature::Set { @@ -41,9 +41,9 @@ impl CheckerState { Set::ClaimedSet(Instance::Var(name.clone())).into(), )?; } - new_fields.push(SigField { + new_fields.push(Field { name: name.clone(), - signature, + carries: signature, }); // We must iteratively add the entire signature so that // field lookup does something, as we rely on that for type @@ -140,9 +140,9 @@ impl CheckerState { let sub_instances = fields .iter() .map( - |SigField { + |Field { name: f_n, - signature: f_s, + carries: f_s, }| { let f_i = assignations .get(f_n) @@ -181,7 +181,7 @@ impl CheckerState { } } Instance::Project { instance, field } => { - let Field { + let OwnedField { field: field_signature, owner: owner_signature, } = self.lookup_signature_field(&field)?; @@ -268,7 +268,7 @@ impl CheckerState { let mut computed_output = None; let mut processed_arms = Vec::new(); for arm in arms { - let Field { + let OwnedField { field: field_set, .. } = self.lookup_variant_field(&arm.tag)?; @@ -288,7 +288,7 @@ impl CheckerState { ) } computed_output = Some(output.clone()); - InstCaseArm { + CaseArm { tag: arm.tag.clone(), bound: canonical, body: output, @@ -296,7 +296,7 @@ impl CheckerState { } else { let canonical = ctx.make_element_binding(binding_name, binding_set)?; let body = ctx.check_instance((&arm.body).into(), signature)?; - InstCaseArm { + CaseArm { tag: arm.tag.clone(), bound: canonical, body, @@ -386,14 +386,19 @@ impl CheckerState { }) } } - Instance::App(inner, element) => { + Instance::App { + instance: inner, + args, + } => { // this is the only time that we ever call check_instance with // signature = None, and in this mode all we want is to put // inner into a canonical form pushing stuck terms to the leaves // and simplifying everything else. let inner = self.check_instance(inner, None)?; + println!("HERE {:?}, {:?}", inner, args); match &inner { Instance::Var(v) => { + println!("VAR {}", v); let field = self.lookup_signature_field(&v)?; let Signature::Ext { ref params, @@ -426,11 +431,12 @@ impl CheckerState { }); } } - let element = self.check_element(element, ¶ms[0].set)?; - Ok(Instance::App( - Box::new(Instance::Var(v.clone())), - Box::new(element), - )) + todo!("finish") + // let element = self.check_element(args, ¶ms[0].set)?; + // Ok(Instance::App( + // Box::new(Instance::Var(v.clone())), + // Box::new(element), + // )) } Instance::For { params, body } => { if params.is_empty() { @@ -440,28 +446,33 @@ impl CheckerState { } let mut ctx = self.clone(); let first_set = ctx.check_set(¶ms[0].set)?; - let element_checked = self.check_element(element, &first_set)?; - ctx.add_element(params[0].name.clone(), element_checked.into(), first_set)?; - if params.len() == 1 { - ctx.check_instance(body, signature) - } else { - let residual = Instance::For { - params: params[1..].to_vec(), - body: body.clone(), - }; - ctx.check_instance(&residual, signature) - } + todo!("finish this") + // let element_checked = self.check_element(args, &first_set)?; + // ctx.add_element(params[0].name.clone(), element_checked.into(), first_set)?; + // if params.len() == 1 { + // ctx.check_instance(body, signature) + // } else { + // let residual = Instance::For { + // params: params[1..].to_vec(), + // body: body.clone(), + // }; + // ctx.check_instance(&residual, signature) + // } } Instance::Record(_) | Instance::SetCoerce(_) => { Err(CheckerError::NonFunctionalInstance { instance: inner, - element: *element.clone(), + elements: args.clone(), }) } - Instance::Project { .. } | Instance::App(_, _) | Instance::Case { .. } => { + Instance::Project { .. } | Instance::App { .. } | Instance::Case { .. } => { + println!("Stuck"); // it would appear that we are stuck here, so our only // choice is to continue to be so - Ok(Instance::App(Box::new(inner), element.clone())) + Ok(Instance::App { + instance: Box::new(inner), + args: args.clone(), + }) } } } diff --git a/src/checker_state.rs b/src/checker_state.rs index 3d933f2..a8473ff 100644 --- a/src/checker_state.rs +++ b/src/checker_state.rs @@ -50,10 +50,10 @@ pub enum CheckerError { claimed: Signature, reason: String, }, - #[display("Non-functional instance {instance} found in application to element {element}")] + #[display("Non-functional instance {instance} found in application to elements {}", elements.iter().map(|e| e.to_string()).collect::>().join(" "))] NonFunctionalInstance { instance: Instance, - element: Element, + elements: Vec, }, } @@ -61,7 +61,7 @@ pub enum CheckerError { // Generics for wrapping fields, values, and coercing them #[derive(Display, Clone)] #[display("{field} @ {owner}")] -pub struct Field { +pub struct OwnedField { pub field: T, pub owner: T, } @@ -115,9 +115,9 @@ pub struct CheckerState { wf_elements: HashMap, wf_signatures: HashMap, wf_instances: HashMap, - record_fields: HashMap>, - variant_fields: HashMap>, - signature_fields: HashMap>, + record_fields: HashMap>, + variant_fields: HashMap>, + signature_fields: HashMap>, binder_element: Arc, unique_name: Arc, } @@ -179,7 +179,7 @@ impl CheckerState { fn assert_correct_owner( &self, name: &String, - field: &Field, + field: &OwnedField, belongs_to: &T, ) -> Result<(), CheckerError> where @@ -225,7 +225,7 @@ impl CheckerState { }; self.record_fields.insert( name.clone(), - Field { + OwnedField { field: field_set.clone(), owner: owner_set.clone(), }, @@ -245,7 +245,7 @@ impl CheckerState { }; self.variant_fields.insert( name.clone(), - Field { + OwnedField { field: field_set.clone(), owner: owner_set.clone(), }, @@ -257,18 +257,18 @@ impl CheckerState { pub fn add_set(&mut self, name: String, set: SetValue) -> Result<(), CheckerError> { match &set { SetValue::Concrete(set @ Set::Record(fields)) => { - for RecordField { + for Field { name: rfn, - set: field_set, + carries: field_set, } in fields { self.add_record_field(rfn, field_set, set)?; } } SetValue::Concrete(set @ Set::Variant(fields)) => { - for VariantField { + for Field { name: vfn, - set: field_set, + carries: field_set, } in fields { self.add_variant_field(vfn, field_set, set)?; @@ -309,13 +309,13 @@ impl CheckerState { .map_or(Err(CheckerError::Unbound(name.clone())), Ok) } - pub fn lookup_record_field(&self, name: &String) -> Result<&Field, CheckerError> { + pub fn lookup_record_field(&self, name: &String) -> Result<&OwnedField, CheckerError> { self.record_fields .get(name) .map_or(Err(CheckerError::Unbound(name.clone())), Ok) } - pub fn lookup_variant_field(&self, name: &String) -> Result<&Field, CheckerError> { + pub fn lookup_variant_field(&self, name: &String) -> Result<&OwnedField, CheckerError> { self.variant_fields .get(name) .map_or(Err(CheckerError::Unbound(name.clone())), Ok) @@ -354,7 +354,7 @@ impl CheckerState { }; self.signature_fields.insert( name.clone(), - Field { + OwnedField { field: field_signature.clone(), owner: owner_signature.clone(), }, @@ -371,9 +371,9 @@ impl CheckerState { ) -> Result<(), CheckerError> { match &signature { Signature::Theory(fields) => { - for SigField { + for Field { name: field_name, - signature: field_sig, + carries: field_sig, } in fields { // TODO: are we supposed to recurse? @@ -420,7 +420,10 @@ impl CheckerState { .map_or(Err(CheckerError::Unbound(name.clone())), Ok) } - pub fn lookup_signature_field(&self, name: &String) -> Result<&Field, CheckerError> { + pub fn lookup_signature_field( + &self, + name: &String, + ) -> Result<&OwnedField, CheckerError> { self.signature_fields .get(name) .map_or(Err(CheckerError::Unbound(name.clone())), Ok) diff --git a/src/main.rs b/src/main.rs index 834792e..1925b41 100644 --- a/src/main.rs +++ b/src/main.rs @@ -18,35 +18,42 @@ fn main() { .init(); let src = r#" -let signature Graph = theory { - Node :: Set, - Edge :: (s : set-of(Node)) (t : set-of(Node)) -> Set +// let signature Graph = theory { +// Vertex :: Set, +// Edge :: (s : set-of(Vertex)) (t : set-of(Vertex)) -> Set +// } + +// let set Empty = variant[] +// let set Unit = record{} +// let element pt : Unit = {} +// let set F1 = variant [ one0 : Unit ] +// let set F2 = variant [ two0 : Unit | two1 : Unit ] +// let set F3 = variant [ three0 : Unit | three1 : Unit | three2: Unit ] + +// let instance oneSimplex :: Graph = { +// .Vertex = F3 :: Set, +// .Edge = for (s : set-of(Vertex)) (t : set-of(Vertex)), +// case s of [ +// three0. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Unit :: Set | three2. pt => Unit :: Set ] +// | three1. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Empty :: Set | three2. pt => Unit :: Set ] +// | three2. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Empty :: Set | three2. pt => Empty :: Set ] +// ] +// } + +// let set OneSimplexEdges = record { +// source: set-of(oneSimplex .Vertex), +// target: set-of(oneSimplex .Vertex), +// connected: set-of(oneSimplex .Edge source target) +// } + +// let element vertex0 : F3 = three0. {} +// let element vertex1 : F3 = three1. {} +// let element edge01 : set-of(oneSimplex .Edge vertex0 vertex1) = pt + +let signature S = theory { + F :: (x : Nat) (y : Bool) -> Set, + G :: (z : set-of(F 3 5)) -> Set } - -let set Empty = variant[] -let set Unit = record{} -let element pt : Unit = {} -let set F1 = variant [ one0 : Unit ] -let set F2 = variant [ two0 : Unit | two1 : Unit ] -let set F3 = variant [ three0 : Unit | three1 : Unit | three2: Unit ] - -let instance oneSimplex :: Graph = { - .Node = F3 :: Set, - .Edge = for (s : set-of(Node)) (t : set-of(Node)), - case s of [ - three0. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Unit :: Set | three2. pt => Unit :: Set ] - | three1. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Empty :: Set | three2. pt => Unit :: Set ] - | three2. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Empty :: Set | three2. pt => Empty :: Set ] - ] -} - -let set OneSimplexEdges = record { - source: set-of(oneSimplex .Node), - target: set-of(oneSimplex .Node), - connected: set-of(oneSimplex .Edge source target) -} - -let element edge : set-of(oneSimplex .Edge (three0. pt) (three1. pt)) = pt "#; let programme = parser::parse(src); diff --git a/src/parser.rs b/src/parser.rs index 6e4a09d..ecf6ab3 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -45,25 +45,25 @@ parser! { rule kw_false() = "false" wb() rule keyword() = - kw_let_set() / kw_let_element() / kw_let_signature() / kw_let_instance() - / kw_record() / kw_variant() / kw_theory() - / kw_case() / kw_of() / kw_for() - / kw_Set() / kw_set_of() / kw_set() - / kw_Nat() / kw_Int() / kw_Float() / kw_Str() / kw_Bool() - / kw_true() / kw_false() + kw_let_set() / kw_let_element() / kw_let_signature() / kw_let_instance() + / kw_record() / kw_variant() / kw_theory() + / kw_case() / kw_of() / kw_for() + / kw_Set() / kw_set_of() / kw_set() + / kw_Nat() / kw_Int() / kw_Float() / kw_Str() / kw_Bool() + / kw_true() / kw_false() // ==================================================================== // Identifiers // ==================================================================== rule lower_ident() -> String - = !keyword() s:$(['a'..='z'] ident_tail()*) { s.to_string() } + = !keyword() s:$(['a'..='z'] ident_tail()*) { s.to_string() } rule upper_ident() -> String - = !keyword() s:$(['A'..='Z'] ident_tail()*) { s.to_string() } + = !keyword() s:$(['A'..='Z'] ident_tail()*) { s.to_string() } rule any_ident() -> String - = !keyword() s:$(['a'..='z' | 'A'..='Z'] ident_tail()*) { s.to_string() } + = !keyword() s:$(['a'..='z' | 'A'..='Z'] ident_tail()*) { s.to_string() } rule elem_var() -> String = lower_ident() rule inst_var() -> String = lower_ident() @@ -75,11 +75,11 @@ parser! { // ==================================================================== rule project() -> String - = __ "." n:any_ident() { n } + = __ "." n:any_ident() { n } rule inject() -> String - = _ !keyword() s:$(['a'..='z' | 'A'..='Z'] ident_tail()*) "." __ - { s.to_string() } + = _ !keyword() s:$(['a'..='z' | 'A'..='Z'] ident_tail()*) "." __ + { s.to_string() } // ==================================================================== // Record-field labels @@ -93,170 +93,167 @@ parser! { // ==================================================================== rule nat_lit() -> Literal - = n:$(['0'..='9']+) !"." { Literal::Nat(n.parse().unwrap()) } + = n:$(['0'..='9']+) !"." { Literal::Nat(n.parse().unwrap()) } rule int_lit() -> Literal - = "-" n:$(['0'..='9']+) !"." { Literal::Int(-(n.parse::().unwrap())) } + = "-" n:$(['0'..='9']+) !"." { Literal::Int(-(n.parse::().unwrap())) } rule float_lit() -> Literal - = s:$("-"? ['0'..='9']+ "." ['0'..='9']+) { Literal::Float(s.parse().unwrap()) } + = s:$("-"? ['0'..='9']+ "." ['0'..='9']+) { Literal::Float(s.parse().unwrap()) } rule str_lit() -> Literal - = "\"" s:$((!"\"" [_])*) "\"" { Literal::Str(s.to_string()) } + = "\"" s:$((!"\"" [_])*) "\"" { Literal::Str(s.to_string()) } rule bool_lit() -> Literal - = kw_true() { Literal::Bool(true) } - / kw_false() { Literal::Bool(false) } + = kw_true() { Literal::Bool(true) } + / kw_false() { Literal::Bool(false) } rule literal() -> Literal - = float_lit() / int_lit() / nat_lit() / str_lit() / bool_lit() + = float_lit() / int_lit() / nat_lit() / str_lit() / bool_lit() rule builtin() -> BuiltIn - = kw_Nat() { BuiltIn::Nat } - / kw_Int() { BuiltIn::Int } - / kw_Float() { BuiltIn::Float } - / kw_Str() { BuiltIn::Str } - / kw_Bool() { BuiltIn::Bool } + = kw_Nat() { BuiltIn::Nat } + / kw_Int() { BuiltIn::Int } + / kw_Float() { BuiltIn::Float } + / kw_Str() { BuiltIn::Str } + / kw_Bool() { BuiltIn::Bool } // ==================================================================== // Sets // ==================================================================== - rule set_field() -> RecordField - = _ n:lower_ident() _ ":" _ s:set() _ - { RecordField { name: n, set: s } } + rule set_field() -> Field + = _ n:lower_ident() _ ":" _ s:set() _ + { Field { name: n, carries: s } } - rule variant_field() -> VariantField - = _ n:lower_ident() _ ":" _ s:set() _ - { VariantField { name: n, set: s } } + rule variant_field() -> Field + = _ n:lower_ident() _ ":" _ s:set() _ + { Field { name: n, carries: s } } rule claimed_set() -> Instance - = kw_set_of() _ "(" _ i:instance() _ ")" { i } + = kw_set_of() _ "(" _ i:instance() _ ")" { i } rule set() -> Set - = kw_record() _ "{" _ fs:(set_field() ** ",") _ "}" { Set::Record(fs) } - / kw_variant() _ "[" _ vs:(variant_field() ** "|") _ "]" { Set::Variant(vs) } - / b:builtin() { Set::BuiltIn(b) } - / i:claimed_set() { Set::ClaimedSet(i) } - / v:set_var() { Set::Var(v) } - / "(" _ s:set() _ ")" { s } + = kw_record() _ "{" _ fs:(set_field() ** ",") _ "}" { Set::Record(fs) } + / kw_variant() _ "[" _ vs:(variant_field() ** "|") _ "]" { Set::Variant(vs) } + / b:builtin() { Set::BuiltIn(b) } + / i:claimed_set() { Set::ClaimedSet(i) } + / v:set_var() { Set::Var(v) } + / "(" _ s:set() _ ")" { s } // ==================================================================== // Signatures // ==================================================================== rule param() -> Param - = "(" _ n:elem_var() _ ":" _ s:set() _ ")" { Param { name: n, set: s } } + = "(" _ n:elem_var() _ ":" _ s:set() _ ")" { Param { name: n, set: s } } rule param_list() -> Vec = param() ++ _ - rule sig_field() -> SigField - = _ n:upper_ident() _ "::" _ s:signature() _ - { SigField { name: n, signature: s } } + rule sig_field() -> Field + = _ n:upper_ident() _ "::" _ s:signature() _ + { Field { name: n, carries: s } } rule signature() -> Signature - = kw_Set() { Signature::Set } - / kw_theory() _ "{" _ fs:(sig_field() ** ",") _ "}" { Signature::Theory(fs) } - / ps:param_list() _ "->" _ cod:signature() - { Signature::Ext { params: ps, codomain: Box::new(cod) } } - / v:sig_var() { Signature::Var(v) } - / "(" _ s:signature() _ ")" { s } + = kw_Set() { Signature::Set } + / kw_theory() _ "{" _ fs:(sig_field() ** ",") _ "}" { Signature::Theory(fs) } + / ps:param_list() _ "->" _ cod:signature() + { Signature::Ext { params: ps, codomain: Box::new(cod) } } + / v:sig_var() { Signature::Var(v) } + / "(" _ s:signature() _ ")" { s } // ==================================================================== // Elements // ==================================================================== rule elem_assign() -> ElemAssign - = _ n:field_lower() _ "=" _ e:element() _ - { ElemAssign { name: n, element: e } } + = _ n:field_lower() _ "=" _ e:element() _ + { ElemAssign { name: n, element: e } } rule atom_elem() -> Element - = l:literal() { Element::Literal(l) } - / "{" _ fs:(elem_assign() ** ",") _ "}" { Element::Record(fs) } - / "(" _ e:element() _ ")" { e } - / v:elem_var() { Element::Var(v) } + = l:literal() { Element::Literal(l) } + / "{" _ fs:(elem_assign() ** ",") _ "}" { Element::Record(fs) } + / "(" _ e:element() _ ")" { e } + / v:elem_var() { Element::Var(v) } rule dot_elem() -> Element - = tags:(t:inject() _ { t })* head:atom_elem() projs:(p:project() { p })* - { - let base = projs.into_iter().fold(head, |acc, p| { - Element::Project { element: Box::new(acc), field: p } - }); - tags.into_iter().rev().fold(base, |acc, t| { - Element::Inject { field: t, element: Box::new(acc) } - }) - } - - rule case_arm() -> CaseArm - = _ t:inject() _ x:elem_var() _ "=>" _ body:element() _ - { CaseArm { tag: t, bound: x, body } } + = tags:(t:inject() _ { t })* head:atom_elem() projs:(p:project() { p })* + { + let base = projs.into_iter().fold(head, |acc, p| { + Element::Project { element: Box::new(acc), field: p } + }); + tags.into_iter().rev().fold(base, |acc, t| { + Element::Inject { field: t, element: Box::new(acc) } + }) + } + + rule case_arm() -> CaseArm + = _ t:inject() _ x:elem_var() _ "=>" _ body:element() _ + { CaseArm { tag: t, bound: x, body } } rule element() -> Element - = kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(case_arm() ** "|") _ "]" - { Element::Case { scrutinee: Box::new(scrut), arms } } - / d:dot_elem() { d } + = kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(case_arm() ** "|") _ "]" + { Element::Case { scrutinee: Box::new(scrut), arms } } + / d:dot_elem() { d } // ==================================================================== // Instances // ==================================================================== - rule inst_case_arm() -> InstCaseArm - = _ t:inject() _ x:elem_var() _ "=>" _ body:instance() _ - { InstCaseArm { tag: t, bound: x, body } } + rule inst_case_arm() -> CaseArm + = _ t:inject() _ x:elem_var() _ "=>" _ body:instance() _ + { CaseArm { tag: t, bound: x, body } } rule inst_assign() -> InstAssign - = _ n:field_upper() _ "=" _ i:instance() _ - { InstAssign { name: n, instance: i } } + = _ n:field_upper() _ "=" _ i:instance() _ + { InstAssign { name: n, instance: i } } rule explicit_set_coerce() -> Set - = s:set() _ "::" _ kw_Set() { s } + = s:set() _ "::" _ kw_Set() { s } rule atom_inst() -> Instance - = s:explicit_set_coerce() { Instance::SetCoerce(Box::new(s)) } - / v:inst_var() { Instance::Var(v) } - / f:sig_var() { Instance::Var(f) } - / "{" _ fs:(inst_assign() ** ",") _ "}" { Instance::Record(fs) } - / "(" _ i:instance() _ ")" { i } + = s:explicit_set_coerce() { Instance::SetCoerce(Box::new(s)) } + / v:inst_var() { Instance::Var(v) } + / f:sig_var() { Instance::Var(f) } + / "{" _ fs:(inst_assign() ** ",") _ "}" { Instance::Record(fs) } + / "(" _ i:instance() _ ")" { i } rule dot_inst() -> Instance - = head:atom_inst() projs:(p:project() { p })* - { - projs.into_iter().fold(head, |acc, p| { - Instance::Project { instance: Box::new(acc), field: p } - }) - } + = head:atom_inst() projs:(p:project() { p })* + { + projs.into_iter().fold(head, |acc, p| { + Instance::Project { instance: Box::new(acc), field: p } + }) + } rule app_inst() -> Instance - = head:dot_inst() tail:(__ a:dot_elem() { a })* - { - tail.into_iter().fold(head, |acc, a| { - Instance::App(Box::new(acc), Box::new(a)) - }) - } + = head:dot_inst() args:(__ a:dot_elem() { a })* + { if args.is_empty() { head } else { Instance::App{instance: Box::new(head), args } }} + rule instance() -> Instance - = kw_for() _ ps:param_list() _ "," _ body:instance() - { Instance::For { params: ps, body: Box::new(body) } } - / kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(inst_case_arm() ** "|") _ "]" - { Instance::Case { scrutinee: Box::new(scrut), arms } } - / app_inst() + = kw_for() _ ps:param_list() _ "," _ body:instance() + { Instance::For { params: ps, body: Box::new(body) } } + / kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(inst_case_arm() ** "|") _ "]" + { Instance::Case { scrutinee: Box::new(scrut), arms } } + / app_inst() // ==================================================================== // Top-level declarations // ==================================================================== rule decl() -> Decl - = kw_let_set() _ n:set_var() _ "=" _ s:set() - { Decl::Set { name: n, set: s } } - / kw_let_element() _ n:elem_var() _ ":" _ s:set() _ "=" _ e:element() - { Decl::Element { name: n, set: s, element: e } } - / kw_let_signature() _ n:sig_var() _ "=" _ sg:signature() - { Decl::Signature { name: n, signature: sg } } - / kw_let_instance() _ n:inst_var() _ "::" _ sg:signature() _ "=" _ i:instance() - { Decl::Instance { name: n, signature: sg, instance: i } } + = kw_let_set() _ n:set_var() _ "=" _ s:set() + { Decl::Set { name: n, set: s } } + / kw_let_element() _ n:elem_var() _ ":" _ s:set() _ "=" _ e:element() + { Decl::Element { name: n, set: s, element: e } } + / kw_let_signature() _ n:sig_var() _ "=" _ sg:signature() + { Decl::Signature { name: n, signature: sg } } + / kw_let_instance() _ n:inst_var() _ "::" _ sg:signature() _ "=" _ i:instance() + { Decl::Instance { name: n, signature: sg, instance: i } } pub rule program() -> Programme - = _ ds:(decl() ** _) _ { Programme(ds) } + = _ ds:(decl() ** _) _ { Programme(ds) } } } -- cgit v1.3.1