From 83e022803d43c0dc049420572a28363c5482c61f Mon Sep 17 00:00:00 2001 From: engboris Date: Sun, 16 Jun 2024 00:28:29 +0200 Subject: [PATCH] Update identifiers grammar, add constant $, fix :, add placeholder _ --- src/lexer.mll | 6 ++++-- src/parser.mly | 4 ++++ src/stellar.ml | 21 ++++++++++++++------- 3 files changed, 22 insertions(+), 9 deletions(-) diff --git a/src/lexer.mll b/src/lexer.mll index 823cdf9..b44d1a8 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -2,8 +2,8 @@ open Parser } -let var_id = ['A'-'Z'] ['A'-'Z' '0'-'9']* -let func_id = ['a'-'z' '0'-'9' '_']+ +let var_id = ['A'-'Z'] ['A'-'Z' '0'-'9' '_' '-']* '\''* +let func_id = ['a'-'z' '0'-'9'] ['a'-'z' 'A'-'Z' '0'-'9' '_' '-']* '\''* '?'? let space = [' ' '\t']+ let newline = '\r' | '\n' | "\r\n" @@ -12,6 +12,7 @@ rule read = parse | func_id { SYM (Lexing.lexeme lexbuf) } | '\'' { comment lexbuf } | "'''" { comments lexbuf } + | '_' { PLACEHOLDER } | '[' { LEFT_BRACK } | ']' { RIGHT_BRACK } | '(' { LEFT_PAR } @@ -20,6 +21,7 @@ rule read = parse | '@' { AT } | '+' { PLUS } | '-' { MINUS } + | '$' { EMPTY_SYM } | ':' { CONS } | ';' { SEMICOLON } | space { read lexbuf } diff --git a/src/parser.mly b/src/parser.mly index 90d3d32..28d7ae9 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -7,6 +7,8 @@ %token CONS %token AT %token SEMICOLON +%token PLACEHOLDER +%token EMPTY_SYM %token EOF %right CONS @@ -33,6 +35,8 @@ symbol: | f = SYM { (Stellar.Null, f) } ray: +| EMPTY_SYM { Stellar.to_func ((Stellar.Null, "$"), []) } +| PLACEHOLDER { Stellar.to_var ("_"^(Stellar.fresh_placeholder ())) } | x = VAR { Stellar.to_var x } | r1 = ray; CONS; r2 = ray { Stellar.to_func ((Stellar.Null, ":"), [r1; r2]) } | pf = symbol; LEFT_PAR; ts = separated_nonempty_list(COMMA?, ray); RIGHT_PAR diff --git a/src/stellar.ml b/src/stellar.ml index db43dc5..c55dbd8 100644 --- a/src/stellar.ml +++ b/src/stellar.ml @@ -31,6 +31,12 @@ open StellarRays Stars and Constellations --------------------------------------- *) +let counter_placeholder = ref 0 +let fresh_placeholder () = + let r = !counter_placeholder in + (counter_placeholder := !counter_placeholder + 1); + (Int.to_string r) + type ray = term type star = ray list type constellation = star list @@ -58,10 +64,6 @@ let is_polarised r : bool = | (Null, _) -> false in exists_func aux r -let is_prefixed ~by:_ : ray -> bool = function - | Func (_, _) -> true - | _ -> false - (* --------------------------------------- Pretty Printer --------------------------------------- *) @@ -69,6 +71,9 @@ let is_prefixed ~by:_ : ray -> bool = function let rec string_of_ray = function | Var x -> x | Func (pf, []) -> string_of_polsym pf + | Func ((Null, ":"), [Func ((Null, ":"), [r1; r2]); r3]) -> + "(" ^ (string_of_ray r1) ^ ":" ^ (string_of_ray r2) ^ "):" ^ + (string_of_ray r3) | Func ((Null, ":"), [r1; r2]) -> (string_of_ray r1) ^ ":" ^ (string_of_ray r2) | Func (pf, ts) -> string_of_polsym pf ^ @@ -199,11 +204,13 @@ let interaction ?(withloops=true) ?(showtrace=false) ?(selfint=false) cs space = output_string stdout "\n"; end; let new_stars = + search_partners ~withloops ~showtrace (r, accr@s') (cs@space') + |> if selfint then - self_interaction ~withloops ~showtrace (r, accr@s') @ - search_partners ~withloops ~showtrace (r, accr@s') cs + List.append (self_interaction ~withloops ~showtrace (r, accr@s')) else - search_partners ~withloops ~showtrace (r, accr@s') cs in + Fn.id + in if List.is_empty new_stars then select_ray (r::accr) s' else Some new_stars in let new_stars = select_ray [] s in