elpi:if version <component> ...

Author: gares

CHANGES.md

@@ -1,3 +1,14 @@
+# v2.0.7 (January 2025)
+
+Requires Menhir 20211230 and OCaml 4.13 or above.
+
+- Parser:
+  - New `elpi:if version <name> <op> <ma>.<mi>.<p>`
+
+- API:
+  - New `Setup.init` takes a `?versions` dictionary to declare versions
+    of external components
+
 # v2.0.6 (December 2024)
 
 Requires Menhir 20211230 and OCaml 4.13 or above.

ELPI.md

@@ -308,9 +308,15 @@ This text is ignored if the version of Elpi old
 % elpi:endif
 ```
 
-Currently the only variable available is `version` and it must be placed
-on the left of the operator (either `<` or `>` or `=`) and ifdefs cannot
-be nested. If not available (e.g. `dune subst` did not run) the version
+Currently the only supported expression is `version <component>` where
+`<component>` defaults to `elpi`. The OCaml APIs let one declare the version
+of other components of the host application that may affect the code to
+be parsed.
+The expression and it must be placed on the left of the operator
+(either `<` or `>` or `=`) and ifdefs cannot
+be nested.
+
+If not available (e.g. `dune subst` did not run) the version of `elpi`
 defaults to `99.99.99`.
 
 One can also ask the lexer to always skip some text. That can be useful if one

src/API.ml

@@ -25,7 +25,9 @@ let set_trace argv =
   args
 
 module Setup = struct
-
+  module StrMap = Util.StrMap
+ 
+ 
 type state_descriptor = Data.State.descriptor
 type quotations_descriptor = Compiler_data.QuotationHooks.descriptor ref
 type hoas_descriptor = Data.HoasHooks.descriptor ref
@@ -44,14 +46,14 @@ type elpi = {
 }
 type flags = Compiler.flags
 
-let init ?(flags=Compiler.default_flags) ?(state=default_state_descriptor) ?(quotations=default_quotations_descriptor) ?(hoas=default_hoas_descriptor) ?(calc=default_calc_descriptor) ~builtins ?file_resolver () : elpi =
+let init ?(versions=Elpi_util.Util.StrMap.empty) ?(flags=Compiler.default_flags) ?(state=default_state_descriptor) ?(quotations=default_quotations_descriptor) ?(hoas=default_hoas_descriptor) ?(calc=default_calc_descriptor) ~builtins ?file_resolver () : elpi =
   (* At the moment we can only init the parser once *)
   let file_resolver =
     match file_resolver with
     | Some x -> x
     | None -> fun ?cwd:_ ~unit:_ () ->
         raise (Failure "'accumulate' is disabled since Setup.init was not given a ~file_resolver.") in
-  let parser = (module Parse.Make(struct let resolver = file_resolver end) : Parse.Parser) in
+  let parser = (module Parse.Make(struct let versions = versions let resolver = file_resolver end) : Parse.Parser) in
   Data.Global_symbols.lock ();
   let header_src =
     builtins |> List.map (fun (fname,decls) ->
@@ -1359,6 +1361,8 @@ module Utils = struct
   module IntSet = Util.IntSet
   module LocSet : Util.Set.S with type elt = Ast.Loc.t = Util.Set.Make(Ast.Loc)
 
+  let version_parser = Util.version_parser
+
 end
 
 module RawPp = struct

src/API.mli

@@ -154,6 +154,12 @@ module Setup : sig
   (* Handle to an elpi instance *)
   type elpi
 
+  module StrMap : sig
+    include Map.S with type key = string
+    val show : (Format.formatter -> 'a -> unit) -> 'a t -> string
+    val pp : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
+  end
+ 
   (** Initialize ELPI.
 
       [init] must be called before invoking the parser.
@@ -170,6 +176,7 @@ module Setup : sig
         [builtins] and where accumulate resolves files with the given
         [file_resolver]. *)
   val init :
+    ?versions:(int * int * int) StrMap.t ->
     ?flags:flags ->
     ?state:state_descriptor ->
     ?quotations:quotations_descriptor ->
@@ -302,11 +309,7 @@ end
 
 module Data : sig
 
-  module StrMap : sig
-   include Map.S with type key = string
-   val show : (Format.formatter -> 'a -> unit) -> 'a t -> string
-   val pp : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
-  end
+  module StrMap = Setup.StrMap
 
   (* what is assigned to the query variables *)
   type term
@@ -1375,6 +1378,15 @@ module Utils : sig
   module IntSet : Set.S with type elt = int
   module LocSet : Set.S with type elt = Ast.Loc.t
 
+  (* Parses a version string as it parses the elpi one:
+     - drop leading 'v'
+     - drop trailing '-...'
+     - splits on '.'
+       - expects 3 numerical components
+       - or a single component (defaults to 99.99.99)
+  *)
+  val version_parser : what:string -> string -> int * int * int
+
 end
 
 module RawPp : sig

src/parser/ast.ml

@@ -126,7 +126,7 @@ let mkQuoted loc pad s =
                                  Loc.source_stop = loc.Loc.source_stop - m;
              } in
   (* Printf.eprintf "mkQuoted '%s'\n" s; *)
-  let rec find_data i pad =
+  let find_data i pad =
     match s.[i] with
     (* | '{' -> assert false; find_data (i+1) (pad+1) *)
     | ':' ->

src/parser/lexer.mll.in

@@ -22,29 +22,25 @@
       b.lex_start_p <- start_p;
       r
 
-    let version_ma, version_mi, version_p =
-      let is_number x = try let _ = int_of_string x in true with _ -> false in
-      let v = "%%VERSION_NUM%%" in
-      let v' = Re.Str.(replace_first (regexp "^v") "" v) in    (* v1.20... -> 1.20... *)
-      let v' = Re.Str.(replace_first (regexp "-.*$") "" v') in  (* ...-10-fjdnfs -> ... *)
-      let l = String.split_on_char '.' v' in
-      match l with
-      | [ma;mi;p] when List.for_all is_number l -> int_of_string ma, int_of_string mi, int_of_string p
-      | [_] -> 99, 99, 99
-      | _ -> Elpi_util.Util.error ("lexer: version parser: cannot parse: " ^ v)
-
-    let version_test ops ma mi p =
+    let version_test v l ops ma mi p =
       let ma = int_of_string ma in
       let mi = int_of_string mi in
       let p  = int_of_string p in
+      let version =
+        match l with
+        | None | Some "elpi" ->
+            Elpi_util.Util.version_parser ~what:"elpi" "%%VERSION_NUM%%"
+        | Some l ->
+            try Elpi_util.Util.StrMap.find l v
+            with Not_found -> raise (Error ("elpi: lexer: no version declared for " ^ l)) in
       let op =
         match ops with
         | '<' -> (<)
         | '=' -> (=)
         | '>' -> (>)
         | _ -> assert false in
-      let rc = op (version_ma,version_mi,version_p) (ma,mi,p) in
-      (*Printf.eprintf "%d.%d.%d %c %d.%d.%d = %b\n" version_ma version_mi version_p ops ma mi p rc;*)
+      let rc = op version (ma,mi,p) in
+      (* let v1 ,v2 ,v3 = version in Printf.eprintf "%d.%d.%d %c %d.%d.%d = %b\n" v1 v2 v3 ops ma mi p rc;*)
       rc
 
 }
@@ -66,46 +62,46 @@ let symbchar = lcase | ucase | digit | schar | ':'
 let symbcharstar = symbchar *
 let symbcharplus = symbchar +
 
-rule linecomment = parse
-| '\n' { new_line lexbuf; token lexbuf }
-| eof { token lexbuf }
-| "elpi:skip " (pnum as n) { linecomment_skip (int_of_string n) lexbuf }
-| "elpi:if" (' '+) "version" (' '+) (['<' '>' '='] as op) (' '+) (pnum as ma) "." (pnum as mi) "." (pnum as p) {
-     if not @@ version_test op ma mi p then linecomment_if lexbuf else linecomment_drop lexbuf }
-| ' ' { linecomment lexbuf }
-| _ { linecomment_drop lexbuf }
-
-and linecomment_drop = parse
-| '\n' { new_line lexbuf; token lexbuf }
-| eof { token lexbuf }
-| _ { linecomment_drop lexbuf }
-
-and linecomment_skip skipno = parse
-| '\n' { new_line lexbuf; if skipno > 0 then skip_lines skipno lexbuf else token lexbuf }
-| eof { token lexbuf }
-| _ { linecomment_skip skipno lexbuf }
-
-and linecomment_if = parse
-| '\n' { new_line lexbuf; skip_lines_endif lexbuf }
-| eof { token lexbuf }
-| _ { linecomment_if lexbuf }
-
-and skip_lines_endif = parse
-| '\n' { new_line lexbuf; skip_lines_endif lexbuf }
-| '%' (' '+) "elpi:endif" { token lexbuf }
-| eof { token lexbuf }
-| _ { skip_lines_endif lexbuf }
-
-and skip_lines skipno = parse
-| '\n' { new_line lexbuf; let skipno = skipno - 1 in if skipno > 0 then skip_lines skipno lexbuf else token lexbuf }
-| eof { token lexbuf }
-| _ { skip_lines skipno lexbuf }
-
-and multilinecomment nest = parse
-| '\n' { new_line lexbuf; multilinecomment nest lexbuf }
-| "*/" { if nest = 0 then token lexbuf else multilinecomment (nest - 1) lexbuf }
-| "/*" { multilinecomment (nest+1) lexbuf }
-| _ { multilinecomment nest lexbuf }
+rule linecomment v = parse
+| '\n' { new_line lexbuf; token v lexbuf }
+| eof { token v lexbuf }
+| "elpi:skip " (pnum as n) { linecomment_skip v (int_of_string n) lexbuf }
+| "elpi:if" (' '+) "version" ( ' '+ ([ 'A' - 'Z' 'a' - 'z' '-' '_' '.' ]+ as l) )? (' '+) (['<' '>' '='] as op) (' '+) (pnum as ma) "." (pnum as mi) "." (pnum as p) {
+     if not @@ version_test v l op ma mi p then linecomment_if v lexbuf else linecomment_drop v lexbuf }
+| ' ' { linecomment v lexbuf }
+| _ { linecomment_drop v lexbuf }
+
+and linecomment_drop v = parse
+| '\n' { new_line lexbuf; token v lexbuf }
+| eof { token v lexbuf }
+| _ { linecomment_drop v lexbuf }
+
+and linecomment_skip v skipno = parse
+| '\n' { new_line lexbuf; if skipno > 0 then skip_lines v skipno lexbuf else token v lexbuf }
+| eof { token v lexbuf }
+| _ { linecomment_skip v skipno lexbuf }
+
+and linecomment_if v = parse
+| '\n' { new_line lexbuf; skip_lines_endif v lexbuf }
+| eof { token v lexbuf }
+| _ { linecomment_if v lexbuf }
+
+and skip_lines_endif v = parse
+| '\n' { new_line lexbuf; skip_lines_endif v lexbuf }
+| '%' (' '+) "elpi:endif" { token v lexbuf }
+| eof { token v lexbuf }
+| _ { skip_lines_endif v lexbuf }
+
+and skip_lines v skipno = parse
+| '\n' { new_line lexbuf; let skipno = skipno - 1 in if skipno > 0 then skip_lines v skipno lexbuf else token v lexbuf }
+| eof { token v lexbuf }
+| _ { skip_lines v skipno lexbuf }
+
+and multilinecomment v nest = parse
+| '\n' { new_line lexbuf; multilinecomment v nest lexbuf }
+| "*/" { if nest = 0 then token v lexbuf else multilinecomment v (nest - 1) lexbuf }
+| "/*" { multilinecomment v (nest+1) lexbuf }
+| _ { multilinecomment v nest lexbuf }
 
 and string b = parse
 | '\n'     { Buffer.add_char b '\n'; new_line lexbuf; string b lexbuf }
@@ -155,7 +151,7 @@ and lookahead_open b n = parse
     if n = 1 then () else lookahead_open b (n-1) lexbuf
   }
 
-and token = parse
+and token v = parse
 | ("#line" " "+ (num as n) " "+ '"' ([^'"']+ as f) '"' " "* '\n' as x) {
     let open Lexing in
     lexbuf.lex_curr_p <- {
@@ -166,11 +162,11 @@ and token = parse
     };
     lexbuf.lex_abs_pos <- - (String.length x) - lexbuf.lex_start_p.pos_cnum;
     lexbuf.lex_start_p <- lexbuf.lex_curr_p;
-    token lexbuf }
-| ( ' ' | '\t' | '\r' ) { token lexbuf }
-| '\n' { new_line lexbuf; token lexbuf }
-| '%' { linecomment lexbuf }
-| "/*" { multilinecomment 0 lexbuf }
+    token v lexbuf }
+| ( ' ' | '\t' | '\r' ) { token v lexbuf }
+| '\n' { new_line lexbuf; token v lexbuf }
+| '%' { linecomment v lexbuf }
+| "/*" { multilinecomment v 0 lexbuf }
 | "." { FULLSTOP }
 | "_" idchar + as c { CONSTANT c }
 | "_" { FRESHUV }

src/parser/parse.ml

@@ -26,6 +26,7 @@ module type Parser_w_Internals = sig
 end
 
 module type Config = sig
+  val versions : (int * int * int) Util.StrMap.t
   val resolver : ?cwd:string -> unit:string -> unit -> string
 
 end
@@ -51,7 +52,7 @@ let chunk s (p1,p2) =
   String.sub s p1.Lexing.pos_cnum (p2.Lexing.pos_cnum - p1.Lexing.pos_cnum)
 
 let parse grammar lexbuf =
-  let buffer, lexer = MenhirLib.ErrorReports.wrap Lexer.token in
+  let buffer, lexer = MenhirLib.ErrorReports.wrap Lexer.(token C.versions) in
   try
     grammar lexer lexbuf
   with

src/parser/parse.mli

@@ -27,6 +27,7 @@ module type Parser_w_Internals = sig
 end
 
 module type Config = sig
+  val versions : (int * int * int) Util.StrMap.t
   val resolver : ?cwd:string -> unit:string -> unit -> string
 end
 

src/parser/test_lexer.ml

@@ -112,7 +112,7 @@ let rec expect s b = function
   | [] -> ()
   | sp :: spec ->
       begin try
-      let tok2 = Lexer.token b in
+      let tok2 = Lexer.token Elpi_util.Util.StrMap.empty b in
       let open Lexing in
       let p = b.lex_curr_p in
       let lnum2, bol2, bnum2, cnum2 = p.pos_lnum, p.pos_bol, b.lex_start_p.pos_cnum, p.pos_cnum in

src/parser/test_parser.ml

@@ -34,7 +34,7 @@ let chunk s (p1,p2) =
 
 let message_of_state s = try Error_messages.message s with Not_found -> "syntax error"
 
-module Parser = Parse.Make(struct let resolver = Elpi_util.Util.std_resolver ~paths:[] () end)
+module Parser = Parse.Make(struct let versions = Elpi_util.Util.StrMap.empty let resolver = Elpi_util.Util.std_resolver ~paths:[] () end)
 
 let warn = ref None
 let () = Elpi_util.Util.set_warn (fun ?loc str -> warn := Some str)
@@ -276,16 +276,16 @@ let sanity_check : unit =
           | Extensible ({ start; mk_token; non_enclosed ; at_least_one_char; _ } as e)->
               let start = if at_least_one_char then start ^ "x" else start in
               start, mk_token, (if non_enclosed then Some (fun x -> start ^ x ^ start) else None), Some e in
-    let tok = Lexer.token (Lexing.from_string start) in
+    let tok = Lexer.token Elpi_util.Util.StrMap.empty (Lexing.from_string start) in
     let token = mk_token start in
     assert(tok = token);
     begin try match fixity with
     | Infix | Infixl | Infixr ->
-        ignore(Parser.Internal.infix_SYMB Lexer.token (Lexing.from_string start))
+        ignore(Parser.Internal.infix_SYMB Lexer.(token Elpi_util.Util.StrMap.empty) (Lexing.from_string start))
     | Postfix ->
-        ignore(Parser.Internal.postfix_SYMB Lexer.token (Lexing.from_string start))
+        ignore(Parser.Internal.postfix_SYMB Lexer.(token Elpi_util.Util.StrMap.empty) (Lexing.from_string start))
     | Prefix ->
-        ignore(Parser.Internal.prefix_SYMB Lexer.token (Lexing.from_string start))
+        ignore(Parser.Internal.prefix_SYMB Lexer.(token Elpi_util.Util.StrMap.empty) (Lexing.from_string start))
     with _ ->
       Printf.eprintf "\n           (*          1         2         3 *)";
       Printf.eprintf "\n           (* 123456789012345678901234567890 *)";
@@ -296,7 +296,7 @@ let sanity_check : unit =
     | None -> ()
     | Some f ->
       let v = f "xx" in
-      assert(CONSTANT v = Lexer.token (Lexing.from_string v));
+      assert(CONSTANT v = Lexer.token Elpi_util.Util.StrMap.empty (Lexing.from_string v));
     end;
     x) tokens) |> List.concat |> List.length in
   assert(extensible_SYMB = 14)

src/utils/util.ml

@@ -725,3 +725,15 @@ module Map = Map.Make(Self)
 module Set = Set.Make(Self)
 include Self
 end
+
+let version_parser ~what v =
+  try
+    let is_number x = try let _ = int_of_string x in true with _ -> false in
+    let v' = Re.Str.(replace_first (regexp "^v") "" v) in    (* v1.20... -> 1.20... *)
+    let v' = Re.Str.(replace_first (regexp "-.*$") "" v') in  (* ...-10-fjdnfs -> ... *)
+    let l = String.split_on_char '.' v' in
+    match l with
+    | [ma;mi;p] when List.for_all is_number l -> int_of_string ma, int_of_string mi, int_of_string p
+    | [_] -> 99, 99, 99
+    | _ -> raise (Failure "invalid format")
+  with Failure msg -> error ("elpi: version_parser: cannot parse version of "^what^" '" ^ v ^ "': " ^ msg)

src/utils/util.mli

@@ -306,4 +306,6 @@ module Constants : sig
   val pp : Format.formatter -> t -> unit
   val show : t -> string
   val compare : t -> t -> int
-end
+end
+
+val version_parser : what:string -> string -> int * int * int

tests/sources/ifdef.elpi

@@ -9,4 +9,8 @@ pred x.
 x.
 % elpi:endif
 
+% elpi:if version elpi = 100.0.0
+pred foo. pred pred.
+% elpi:endif
+
 main :- x.