proof-of-concept

demos/calc-incremental/calc.ml

@@ -19,9 +19,9 @@ let rec loop lexbuf (checkpoint : int I.checkpoint) =
          and offer it to the parser, which will produce a new
          checkpoint. Then, repeat. *)
       let token = Lexer.token lexbuf in
-      let startp = lexbuf.lex_start_p
-      and endp = lexbuf.lex_curr_p in
-      let checkpoint = I.offer checkpoint (token, startp, endp) in
+      let startp = lexbuf.lex_start_pos
+      and endp = lexbuf.lex_curr_pos in
+      let checkpoint = I.offer checkpoint (token, (startp, endp)) in
       loop lexbuf checkpoint
   | I.Shifting _
   | I.AboutToReduce _ ->
@@ -57,7 +57,8 @@ let fail lexbuf (_ : int I.checkpoint) =
     (lexeme_start lexbuf)
 
 let loop lexbuf result =
-  let supplier = I.lexer_lexbuf_to_supplier Lexer.token lexbuf in
+  let get_location l = (l.Lexing.lex_start_pos, l.Lexing.lex_curr_pos) in
+  let supplier = I.lexer_lexbuf_to_supplier Lexer.token get_location lexbuf in
   I.loop_handle succeed (fail lexbuf) supplier result
 
 (* -------------------------------------------------------------------------- *)
@@ -66,8 +67,9 @@ let loop lexbuf result =
 
 let process (line : string) =
   let lexbuf = from_string line in
+  let loc = (lexbuf.lex_start_pos, lexbuf.lex_curr_pos) in
   try
-    loop lexbuf (Parser.Incremental.main lexbuf.lex_curr_p)
+    loop lexbuf (Parser.Incremental.main loc)
   with
   | Lexer.Error msg ->
       Printf.fprintf stderr "%s%!" msg
@@ -89,7 +91,7 @@ let rec repeat channel =
   process optional_line;
   if continue then
     repeat channel
-  
+
 let () =
   repeat (from_channel stdin)
 

demos/calc-incremental/parser.mly

+%location<MyLocation>
+
 %token <int> INT
 %token PLUS MINUS TIMES DIV
 %token LPAREN RPAREN
@@ -17,17 +19,17 @@ main:
 
 expr:
 | i = INT
-    { i }
+    { prerr_endline (MyLocation.trace $loc);i }
 | LPAREN e = expr RPAREN
-    { e }
+    { prerr_endline (MyLocation.trace $loc);e }
 | e1 = expr PLUS e2 = expr
-    { e1 + e2 }
+    { prerr_endline (MyLocation.trace $loc); e1 + e2 }
 | e1 = expr MINUS e2 = expr
-    { e1 - e2 }
+    { prerr_endline (MyLocation.trace $loc);e1 - e2 }
 | e1 = expr TIMES e2 = expr
-    { e1 * e2 }
+    { prerr_endline (MyLocation.trace $loc);e1 * e2 }
 | e1 = expr DIV e2 = expr
-    { e1 / e2 }
+    { prerr_endline (MyLocation.trace $loc);e1 / e2 }
 | MINUS e = expr %prec UMINUS
-    { - e }
+    { prerr_endline (MyLocation.trace $loc);- e }
 

demos/calc/Makefile

@@ -5,7 +5,7 @@ ifndef MENHIR
   MENHIR := $(shell ../find-menhir.sh)
 endif
 
-MENHIRFLAGS     := --infer
+MENHIRFLAGS     := --infer --table
 
 OCAMLBUILD      := ocamlbuild -use-ocamlfind -use-menhir -menhir "$(MENHIR) $(MENHIRFLAGS)"
 

demos/calc/parser.mly

@@ -2,6 +2,7 @@
 %token PLUS MINUS TIMES DIV
 %token LPAREN RPAREN
 %token EOL
+%location<MyLocation>
 
 %left PLUS MINUS        /* lowest precedence */
 %left TIMES DIV         /* medium precedence */

src/EngineTypes.ml

@@ -406,3 +406,18 @@ module type ENGINE = sig
      and type location := location
 
 end
+
+(* --------------------------------------------------------------------------- *)
+
+(* This signature describes the signature of locations manipulated by Menhir. *)
+
+module type LOCATION = sig
+  type t
+
+  val empty_after : t -> t
+  val join : t array -> t
+  val trace : t -> string
+  val get : Lexing.lexbuf -> t
+end
+
+module As_location(M : LOCATION) : LOCATION with type t = M.t = M

src/IL.mli

@@ -29,6 +29,7 @@ and interface_item =
   | IIInclude of module_type
     (* Submodule. *)
   | IIModule of string * module_type
+  | IIModuleAlias of string * Stretch.t
     (* Comment. *)
   | IIComment of string
 
@@ -239,6 +240,7 @@ and modexpr =
     | MVar of string
     | MStruct of structure
     | MApp of modexpr * modexpr
+    | MTextual of Stretch.t
 
 (* Structures. *)
 

src/codeBits.ml

@@ -75,8 +75,14 @@ let tposition =
 
 (* A location is a pair of positions. This might change in the future. *)
 
-let tlocation =
-  tpair tposition tposition
+let default_tlocation = tpair tposition tposition
+
+let tlocation ~public grammar =
+  match grammar.UnparameterizedSyntax.location with
+  | None -> default_tlocation
+  | Some _path ->
+    let path = if public then "Location.t" else "Menhir__Location.t" in
+    TypApp (path, [])
 
 (* The type of lexer buffers. *)
 
@@ -252,6 +258,7 @@ let interface_item_to_structure_item = function
   | IIValDecls _
   | IIInclude _
   | IIModule (_, _)
+  | IIModuleAlias (_, _)
   | IIComment _ ->
       []
 

src/codeBits.mli

@@ -35,7 +35,8 @@ val tint: typ
 val tstring: typ
 val texn: typ
 val tposition: typ
-val tlocation: typ
+val default_tlocation: typ
+val tlocation: public:bool -> UnparameterizedSyntax.grammar -> typ
 val tlexbuf: typ
 val tobj : typ
 

src/codePieces.ml

@@ -72,6 +72,9 @@ let startp =
 let endp =
   "_endpos"
 
+let loc =
+  "_loc"
+
 (* ------------------------------------------------------------------------ *)
 
 (* Types for semantic values. *)

src/codePieces.mli

@@ -53,6 +53,7 @@ val token: string
 val beforeendp: string
 val startp: string
 val endp: string
+val loc: string
 
 (* ------------------------------------------------------------------------ *)
 

src/grammarFunctor.ml

@@ -1581,6 +1581,12 @@ module OnErrorReduce = struct
 
 end
 
+
+(* ------------------------------------------------------------------------ *)
+(* [%location] declaration. *)
+
+let location_module = G.grammar.location
+
 (* ------------------------------------------------------------------------ *)
 
 end (* module Make *)

src/grammarFunctor.mli

@@ -588,6 +588,11 @@ module OnErrorReduce : sig
 
 end
 
+(* ------------------------------------------------------------------------ *)
+(* [%location] declaration. *)
+
+val location_module : Stretch.t option
+
 (* ------------------------------------------------------------------------ *)
 (* Diagnostics. *)
 

src/infer.ml

@@ -112,7 +112,7 @@ let actiondef grammar symbol branch =
       PAnnot (PVar endp, tposition) ::
       PAnnot (PVar starto, tint) ::
       PAnnot (PVar endo, tint) ::
-      PAnnot (PVar loc, tlocation) ::
+      PAnnot (PVar loc, tlocation ~public:false grammar) ::
       formals
     ) [] branch.producers
   in
@@ -130,8 +130,8 @@ let actiondef grammar symbol branch =
     PAnnot (PVar "_endofs", tint) ::
     PAnnot (PVar "_endofs__0_", tint) ::
     PAnnot (PVar "_symbolstartofs", tint) ::
-    PAnnot (PVar "_sloc", tlocation) ::
-    PAnnot (PVar "_loc", tlocation) ::
+    PAnnot (PVar "_sloc", tlocation ~public:false grammar) ::
+    PAnnot (PVar "_loc", tlocation ~public:false grammar) ::
     formals
   in
 
@@ -151,6 +151,13 @@ let actiondef grammar symbol branch =
   | _ ->
       EFun (formals, body)
 
+let location_module grammar =
+  match grammar.UnparameterizedSyntax.location with
+  | None -> []
+  | Some path ->
+    let md = MApp (MVar "MenhirLib.EngineTypes.As_location", MTextual path) in
+    [SIModuleDef ("Menhir__Location", md)]
+
 (* [program] turns an entire grammar into a test program. *)
 
 let program grammar =
@@ -209,6 +216,7 @@ let program grammar =
 
   [ SIFunctor (grammar.parameters,
     interface_to_structure (tokentypedef grammar) @
+    location_module grammar @
     SIStretch grammar.preludes ::
     SIValDefs (false, [ begindef; def; enddef ]) ::
     SIStretch grammar.postludes ::

src/inliner.ml

@@ -311,6 +311,8 @@ and inline_modexpr = function
       MStruct (inline_structure s)
   | MApp (e1, e2) ->
       MApp (inline_modexpr e1, inline_modexpr e2)
+  | MTextual stretch ->
+      MTextual stretch
 
 (* The external entry point. *)
 

src/interface.ml

@@ -15,6 +15,11 @@ open UnparameterizedSyntax
 open IL
 open CodeBits
 
+(* -------------------------------------------------------------------------- *)
+
+(* The type of locations. *)
+
+
 (* -------------------------------------------------------------------------- *)
 
 (* The [Error] exception. *)
@@ -64,7 +69,7 @@ let incremental =
 
 let entrytypescheme_incremental grammar symbol =
   let t = TypTextual (ocamltype_of_start_symbol grammar symbol) in
-  type2scheme (marrow [ tlocation ] (checkpoint t))
+  type2scheme (marrow [ tlocation ~public:true grammar ] (checkpoint t))
 
 (* -------------------------------------------------------------------------- *)
 
@@ -128,7 +133,7 @@ let inspection_api grammar () =
 
 (* The incremental API. *)
 
-let incremental_engine () : module_type =
+let incremental_engine grammar : module_type =
   with_types WKNonDestructive
     "MenhirLib.IncrementalEngine.INCREMENTAL_ENGINE"
     [
@@ -136,8 +141,7 @@ let incremental_engine () : module_type =
       "token", (* NOT [tctoken], which is qualified if [--external-tokens] is used *)
       TokenType.ttoken;
       [],
-      "location",
-      CodeBits.tlocation
+      "location", tlocation ~public:true grammar
     ]
 
 let incremental_entry_points grammar : interface =
@@ -159,7 +163,7 @@ let incremental_api grammar () : interface =
     interpreter,
     MTSigEnd (
       IIComment "The incremental API." ::
-      IIInclude (incremental_engine()) ::
+      IIInclude (incremental_engine grammar) ::
       listiflazy Settings.inspection (inspection_api grammar)
     )
   ) ::
@@ -170,11 +174,19 @@ let incremental_api grammar () : interface =
 
 (* -------------------------------------------------------------------------- *)
 
+let location_module grammar =
+  match grammar.UnparameterizedSyntax.location with
+  | None -> []
+  | Some mpath -> [IIModuleAlias ("Location", mpath)]
+
+(* -------------------------------------------------------------------------- *)
+
 (* The complete interface of the generated parser. *)
 
 let interface grammar = [
   IIFunctor (grammar.parameters,
     monolithic_api grammar @
+    location_module grammar @
     listiflazy Settings.table (incremental_api grammar)
   )
 ]

src/invariant.ml

@@ -676,19 +676,32 @@ let () =
           (* [$startpos] and [$endpos] have been expanded away. *)
           assert false
         | Position (_, _, FlavorLocation) ->
-          (* [$loc] and [$sloc] have been expanded away. *)
-          assert false
+          begin match Grammar.location_module with
+            | None ->
+              (* [$loc] and [$sloc] have been expanded away. *)
+              assert false
+            | Some _ ->
+              (* $loc has been kept for custom locations. *)
+              ()
+          end
         | Position (RightNamed _, WhereSymbolStart, _) ->
           (* [$symbolstartpos(x)] does not exist. *)
           assert false
         | Position (RightNamed id, where, _) ->
-          (* If the semantic action mentions [$startpos($i)], then the
-             [i]-th symbol in the right-hand side must keep track of
-             its start position. Similarly for end positions. *)
-          Array.iteri (fun i id' ->
-              if id = id' then
-                record_ConVar true (rhs.(i), where)
-            ) ids
+          begin match Grammar.location_module with
+            | None ->
+              (* If the semantic action mentions [$startpos($i)], then the
+                 [i]-th symbol in the right-hand side must keep track of
+                 its start position. Similarly for end positions. *)
+              Array.iteri (fun i id' ->
+                  if id = id' then
+                    record_ConVar true (rhs.(i), where)
+                ) ids
+            | Some _ ->
+              (* $startpos when using custom locations should have been
+                 rejected before. *)
+              ()
+          end
       ) (Action.keywords action)
 
   ); (* end of loop on productions *)

src/printer.ml

@@ -696,6 +696,8 @@ and modexpr f = function
       structend f s
   | MApp (e1, e2) ->
       fprintf f "%a (%a)" modexpr e1 modexpr e2
+  | MTextual mpath ->
+      fprintf f "(%a)" (stretch true) mpath
 
 let valdecl f (x, ts) =
   fprintf f "val %s: %a" x typ ts.body
@@ -743,6 +745,8 @@ and interface_item f item =
         fprintf f "include %a" module_type mt
     | IIModule (name, mt) ->
         fprintf f "module %s : %a" name module_type mt
+    | IIModuleAlias (name, mpath) ->
+        fprintf f "module %s = %a" name (stretch true) mpath
     | IIComment comment ->
         fprintf f "(* %s *)" comment
     end;

src/tableBackend.ml

@@ -159,10 +159,14 @@ let reducecellparams prod i _symbol (next : pattern) : pattern =
 
   let ids = Production.identifiers prod in
   let loc =
-    PTuple [
-      PVar (Printf.sprintf "_startpos_%s_" ids.(i));
-      PVar (Printf.sprintf "_endpos_%s_" ids.(i));
-    ]
+    match Grammar.location_module with
+    | None ->
+      PTuple [
+        PVar (Printf.sprintf "_startpos_%s_" ids.(i));
+        PVar (Printf.sprintf "_endpos_%s_" ids.(i));
+      ]
+    | Some _ ->
+      PVar (Printf.sprintf "_loc_%s_" ids.(i))
   in
 
   PRecord [
@@ -199,8 +203,11 @@ let reducecellcasts prod i symbol casts =
 (* 2015/11/04. The start and end positions of an epsilon production are obtained
    by taking the end position stored in the top stack cell (whatever it is). *)
 
+let location_of_top_stack_cell =
+  ERecordAccess(EVar stack, flocation)
+
 let endpos_of_top_stack_cell =
-  EApp (EVar "Pervasives.snd", [ERecordAccess(EVar stack, flocation)])
+  EApp (EVar "Pervasives.snd", [location_of_top_stack_cell])
 
 (* This is the body of the [reduce] function associated with
    production [prod]. It assumes that the variables [env] and [stack]
@@ -236,21 +243,36 @@ let reducebody prod =
      by the OCaml compiler. *)
 
   let posbindings =
-    ( PVar beforeendp,
-      endpos_of_top_stack_cell
-    ) ::
-    ( PVar startp,
-      if length > 0 then
-        EVar (Printf.sprintf "_startpos_%s_" ids.(0))
-      else
+    match Grammar.location_module with
+    | None ->
+      [ PVar beforeendp,
         endpos_of_top_stack_cell
-    ) ::
-    ( PVar endp,
-      if length > 0 then
-        EVar (Printf.sprintf "_endpos_%s_" ids.(length - 1))
-      else
-        EVar startp
-    ) :: []
+      ; PVar startp,
+        if length > 0 then
+          EVar (Printf.sprintf "_startpos_%s_" ids.(0))
+        else
+          endpos_of_top_stack_cell
+      ; PVar endp,
+        if length > 0 then
+          EVar (Printf.sprintf "_endpos_%s_" ids.(length - 1))
+        else
+          EVar startp
+      ]
+    | Some _ ->
+      [ PVar loc,
+        if length > 0 then
+          let loc id = EVar (Printf.sprintf "_loc_%s_" id) in
+          let locs = EArray (Array.to_list (Array.map loc ids)) in
+          EApp (
+            EVar "Menhir__Location.join",
+            [locs]
+          )
+        else
+          EApp (
+            EVar "Menhir__Location.empty_after",
+            [location_of_top_stack_cell]
+          )
+      ]
   in
 
   (* This cannot be one of the start productions. *)
@@ -264,25 +286,26 @@ let reducebody prod =
   let act =
     EAnnot (Action.to_il_expr action, type2scheme (semvtypent nt))
   in
-  let positions =
-    [EVar startp; EVar endp]
+  let elocation =
+    match Grammar.location_module with
+    | None -> ETuple [EVar startp; EVar endp]
+    | Some _ -> EVar loc
   in
-
   EComment (
     Production.print prod,
     blet (
-      (pat, EVar stack) ::                  (* destructure the stack *)
-      casts @                               (* perform type casts *)
-      posbindings @                         (* bind [startp] and [endp] *)
-      [ PVar semv, act ],                   (* run the user's code and bind [semv] *)
+      (pat, EVar stack) ::           (* destructure the stack *)
+      casts @                        (* perform type casts *)
+      posbindings @                  (* bind [startp] and [endp] *)
+      [ PVar semv, act ],            (* run the user's code and bind [semv] *)
 
       (* Return a new stack, onto which we have pushed a new stack cell. *)
 
-      ERecord [                             (* the new stack cell *)
-        fstate, EVar state;                 (* the current state after popping; it will be updated by [goto] *)
-        fsemv, ERepr (EVar semv);           (* the newly computed semantic value *)
-        flocation, ETuple positions;        (* the newly computed start and end positions *)
-        fnext, EVar stack;                  (* this is the stack after popping *)
+      ERecord [                      (* the new stack cell *)
+        fstate, EVar state;          (* the current state after popping; it will be updated by [goto] *)
+        fsemv, ERepr (EVar semv);    (* the newly computed semantic value *)
+        flocation, elocation;        (* the newly computed start and end positions *)
+        fnext, EVar stack;           (* this is the stack after popping *)
       ]
 
     )
@@ -301,7 +324,9 @@ let semantic_action prod =
     ELet (
 
       [ PVar stack, ERecordAccess (EVar env, fstack) ] @
-        (if Production.length prod = 0 then [ PVar state, ERecordAccess (EVar env, fcurrent) ] else []),
+      (if Production.length prod = 0
+       then [ PVar state, ERecordAccess (EVar env, fcurrent) ]
+       else []),
 
       reducebody prod
 
@@ -661,18 +686,53 @@ let trace =
 
 (* ------------------------------------------------------------------------ *)
 
-let location_typ = {
-  typename = "location";
-  typeparams = [];
-  typerhs = TAbbrev tlocation;
-  typeconstraint = None;
-}
+let location_module =
+  match Grammar.location_module with
+  | None -> []
+  | Some path ->
+    [SIModuleDef ("Menhir__Location",
+                  MApp (MVar "MenhirLib.EngineTypes.As_location",
+                        MTextual path))]
+
+let post_location_module =
+  match Grammar.location_module with
+  | None -> []
+  | Some path ->
+    [SIModuleDef ("Location", MTextual path)]
+
+let location_typ =
+  match Grammar.location_module with
+  | None ->
+    { typename = "location"
+    ; typeparams = []
+    ; typerhs = TAbbrev default_tlocation
+    ; typeconstraint = None
+    }
+  | Some _ ->
+    { typename = "location"
+    ; typeparams = []
+    ; typerhs = TAbbrev (TypApp ("Menhir__Location.t", []))
+    ; typeconstraint = None
+    }
 
-let trace_location = {
-  valpublic = false;
-  valpat = PVar "trace_location";
-  valval = EVar "MenhirLib.General.trace_location";
-}
+
+let trace_location =
+  match Grammar.location_module with
+  | None ->
+    { valpublic = false
+    ; valpat = PVar "trace_location"
+    ; valval = EVar "MenhirLib.General.trace_location"
+    }
+  | Some _ ->
+    { valpublic = false
+    ; valpat = PVar "trace_location"
+    ; valval = EVar "Menhir__Location.trace"
+    }
+
+let get_location =
+  match Grammar.location_module with
+  | None -> "MenhirLib.General.get_location"
+  | Some _ -> "Menhir__Location.get"
 
 (* ------------------------------------------------------------------------ *)
 
@@ -722,7 +782,7 @@ let monolithic_entry_point state nt t =
             EVar entry, [
               EIntConst (Lr1.number state);
               EVar lexer;
-              EVar "MenhirLib.General.get_location";
+              EVar get_location;
               EVar lexbuf
             ]
           )
@@ -1022,6 +1082,8 @@ let program =
 
     SIStretch grammar.preludes ::
 
+    location_module @
+
     (* Define the tables. *)
 
     SIModuleDef (tables,
@@ -1030,8 +1092,6 @@ let program =
            exception [Error] and of the type [token]. *)
         SIInclude (MVar basics);
 
-        SITypeDefs [location_typ];
-
         (* This is a non-recursive definition, so none of the names
            defined here are visible in the semantic actions. *)
         SIValDefs (false, [
@@ -1047,7 +1107,11 @@ let program =
           goto;
           semantic_action;
           trace;
-        ])
+        ]);
+
+        (* Define location_typ last, to satisfy the functor interface without
+           making the type location visible from the semantic actions. *)
+        SITypeDefs [location_typ];
       ]
     ) ::
 
@@ -1121,6 +1185,8 @@ let program =
       SIValDefs (false, incremental_api)
     ]) ::
 
+    post_location_module @
+