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/parser.rs | 209 +++++++++++++++++++++++++++++----------------------------- 1 file changed, 103 insertions(+), 106 deletions(-) (limited to 'src/parser.rs') 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