fix virtual positions for symbols and rules generated by inductive (#1448)

- fix Pos.pos_end by setting start_offset properly
- remove Pos.before (unused)
- unfold Pos.after to Pos.shift 1 to easily localize all the uses of shift
- Tactic.p_term_of_string_term: fix initial buffer position using pos_of_string
- rename Lcr.shift into Lcr.reindex to avoid confusion with Pos.shift

Author: fblanqui

src/common/pos.ml

@@ -101,7 +101,8 @@ let equal : popt -> popt -> bool = fun p1 p2 ->
 let pos_end : popt -> popt = fun po ->
   match po with
   | None -> None
-  | Some p -> Some {p with start_line = p.end_line; start_col = p.end_col}
+  | Some p -> Some {p with start_offset=p.end_offset
+                         ; start_line = p.end_line; start_col = p.end_col}
 
 (** [cat] extends and hide the above [cat] function from [pos] to [popt]. *)
 let cat : popt -> popt -> popt = fun p1 p2 ->
@@ -111,15 +112,14 @@ let cat : popt -> popt -> popt = fun p1 p2 ->
   | None, Some p -> Some p
   | None, None -> None
 
-(** [shift k p] returns a position that is [k] characters after [p]. *)
+(** [shift k p] returns a position that is [k] characters after [p].
+    /!\ The generated position may not actually exist in the user input.
+    The fields start_offset, end_offset and end_col are inconsistent. *)
 let shift : int -> popt -> popt = fun k p ->
   match p with
   | None -> assert false
   | Some ({start_col; _} as p) -> Some {p with start_col = start_col + k}
 
-let after = shift 1
-let before = shift (-1)
-
 (** [lexing_opt p] converts a [popt] into a [Lexing.position]. *)
 let lexing_opt (p:popt): Lexing.position =
   match p with

src/core/term.ml

@@ -200,9 +200,12 @@ and sym =
     the same time a definition (i.e., {!field:sym_def} different from [None])
     and rewriting rules (i.e., {!field:sym_rules} is non-empty). *)
 
-(** {b NOTE} For generated symbols (recursors, axioms), {!field:sym_pos} may
-   not be valid positions in the source. These virtual positions are however
-   important for exporting lambdapi files to other formats. *)
+(** {b NOTE} For generated symbols (axioms, inductive types, constructors,
+    recursors), {!field:sym_decl_pos} may not be an actual position in the
+    source. These virtual positions are used to order symbol and rule
+    declarations when exporting a signature. They should NOT be used as
+    references to user source files. This field may be removed in the
+    future. *)
 
 (** {3 Representation of rewriting rules} *)
 

src/export/dk.ml

@@ -88,11 +88,11 @@ type decl =
   | Sym of sym
   | Rule of (Path.t * string * rule)
 
-(** Declarations are ordered wrt their positions in the source. *)
+(** Declarations are ordered wrt their declaration positions. *)
 
 let pos_of_decl : decl -> Pos.popt = fun i ->
   match i with
-  | Sym s -> s.sym_pos
+  | Sym s -> s.sym_decl_pos
   | Rule (_,_,r) -> r.rule_pos
 
 let cmp : decl cmp = cmp_map (Lplib.Option.cmp Pos.cmp) pos_of_decl

src/handle/command.ml

@@ -178,10 +178,11 @@ let handle_modifiers :
   in
   (prop, expo, strat, opaq)
 
-(** [handle_inductive_symbol ss e p strat x xs a] handles the command
-    [e p strat symbol x xs : a] with [ss] as the signature state.
-    The command is at position [pos].
-    On success, an updated signature state and the new symbol are returned. *)
+(** [handle_inductive_symbol ss expo prop strat id declpos xs a] handles the
+    command [expo prop strat symbol id xs : a] with [ss] as the signature
+    state. /!\ Use [declpos] as its position (used in commands exporting
+    signatures). On success, an updated signature state and the new symbol are
+    returned. *)
 let handle_inductive_symbol : sig_state -> expo -> prop -> match_strat
     -> p_ident -> popt -> p_params list -> p_term -> sig_state * sym =
   fun ss expo prop mstrat ({elt=name;pos} as id) declpos xs typ ->
@@ -354,12 +355,9 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
                        inductive types.";
       if opaq then
         fatal pos "Inductive types cannot be declared opaque.";
-      (* Add inductive types in the signature. *)
+      (* Add inductive types in the signature, all at position [pos]. *)
       let add_ind_sym (ss, ind_sym_list) {elt=(id,pt,_); _} =
         let (ss, ind_sym) =
-          (* All inductive types are declared at position [pos]
-             so that constructors are declared afterwards. *)
-          let id = {id with pos} in
           handle_inductive_symbol ss expo Const Eager id pos params pt in
         (ss, ind_sym::ind_sym_list)
       in
@@ -369,13 +367,13 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
       let params =
         List.map (fun (idopts,typopt,_) -> (idopts,typopt,true)) params in
       (* Add constructors in the signature. *)
+      let cons_pos = shift 1 pos in (* after types *)
       let add_constructors
             (ss, cons_sym_list_list) {elt=(_,_,p_cons_list); _} =
         let add_cons_sym (ss, cons_sym_list) (id, pt) =
           let (ss, cons_sym) =
-            handle_inductive_symbol ss expo Const Eager id pos
-            params pt in
-          (ss, cons_sym::cons_sym_list)
+            handle_inductive_symbol ss expo Const Eager id cons_pos params pt
+          in (ss, cons_sym::cons_sym_list)
         in
         let (ss, cons_sym_list_rev) =
           List.fold_left add_cons_sym (ss, []) p_cons_list in
@@ -406,19 +404,19 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
         Inductive.gen_rec_types cfg pos ind_list vs env ind_pred_map x_str
       in
       (* Add the induction principles in the signature. *)
+      let rec_pos = shift 2 pos in (* after types and constructors *)
       let add_recursor (ss, rec_sym_list) ind_sym rec_typ =
         let rec_name = Inductive.rec_name ind_sym in
         if Sign.mem ss.signature rec_name then
           fatal pos "Symbol %a already exists." uid rec_name;
         let (ss, rec_sym) =
           Console.out 2 (Color.gre "symbol %a : %a")
             uid rec_name term rec_typ;
-          (* Recursors are declared after the types and constructors. *)
-          let pos = after (pos_end pos) in
+          (* Add recursors in the signature, all at position [shift 2 pos]. *)
           let id = Pos.make pos rec_name in
           let r =
-            Sig_state.add_symbol ss expo Defin Eager false id
-             None rec_typ [] None
+            Sig_state.add_symbol ss expo Defin Eager false id rec_pos
+              rec_typ [] None
           in sig_state := fst r; r
         in
         (ss, rec_sym::rec_sym_list)

src/handle/inductive.ml

@@ -294,8 +294,6 @@ let iter_rec_rules :
       popt -> inductive -> var array -> ind_pred_map
       -> (p_rule -> unit) -> unit =
   fun pos ind_list vs ind_pred_map f ->
-  (* Rules are declared after recursor declarations. *)
-  let rules_pos = shift (List.length ind_list + 1) (pos_end pos) in
   let n = Array.length vs in
 
   (* variable name used for a recursor case argument *)
@@ -325,6 +323,8 @@ let iter_rec_rules :
     P.appl (P.appl_wild head (List.length ts - n)) t
   in
 
+  let rule_pos = shift 3 pos in (* after types, constructors and recursors *)
+
   (* [gen_rule_cons ind_sym rec_sym cons_sym] generates the p_rule of the
      recursor [rec_sym] of the inductive type [ind_sym] for the constructor
      [cons_sym]. *)
@@ -347,7 +347,7 @@ let iter_rec_rules :
     let nonrec_dom _ _ next = next in
     let codom xs rhs _ ts =
       let cons_arg = P.appl_list (P.iden cons_sym.sym_name) (List.rev xs) in
-      Pos.make rules_pos (arec ind_sym ts cons_arg, rhs)
+      Pos.make rule_pos (arec ind_sym ts cons_arg, rhs)
     in
     fold_cons_type pos ind_pred_map "" ind_sym vs cons_sym inj_var
       init aux acc_rec_dom rec_dom acc_nonrec_dom nonrec_dom codom

src/handle/tactic.ml

@@ -34,13 +34,14 @@ let add_axiom : Sig_state.t -> popt -> meta -> sym =
   let sym =
     wrn sym_pos "axiom %a: %a" uid name term !(m.meta_type);
     (* Temporary hack for axioms to have a declaration position in the order
-       they are created. *)
+       they are created, and strictly before the symbol. *)
+    (* FIXME: use sym_decl_pos instead ? *)
+    let id = {elt=name; pos=sym_pos} in
     let pos = shift Stdlib.(!admitted) sym_pos in
-    let id = Pos.make pos name in
     (* We ignore the new ss returned by Sig_state.add_symbol: axioms do not
        need to be in scope. *)
     snd (Sig_state.add_symbol ss
-           Public Defin Eager true id None !(m.meta_type) [] None)
+           Public Defin Eager true id pos !(m.meta_type) [] None)
   in
   (* Create the value which will be substituted for the metavariable. This
      value is [sym x0 ... xn] where [xi] are variables that will be
@@ -304,14 +305,21 @@ let p_ident_of_var (pos:popt) (t:term) :p_ident =
   | Vari v -> Pos.make pos (base_name v)
   | _ -> fatal pos "Not a variable of the proof context: %a." term t
 
+(* [pos_of_string s] assumes that [s] is a string literal and returns the
+   lexing position of the content of [s]. *)
+let pos_of_string: sym -> Lexing.position =
+  let f p = {p with start_offset=p.start_offset+1; start_col=p.start_col+1;
+                    end_offset=p.end_offset-1; end_col=p.end_col-1} in
+  fun s -> lexing_opt (Option.map f s.sym_pos)
+
 (** [p_term_of_string_term pos t] turns into a p_term a string literal term
     [t] that is part of a bigger term obtained by scoping and normalizing of a
     p_term at position [pos]. *)
 let p_term_of_string_term (pos:popt) (t:term): p_term =
   match t with
   | Symb s when String.is_string_literal s.sym_name ->
-    let p = lexing_opt (after s.sym_pos) in
-    Parsing.Parser.Lp.parse_term_string p (String.remove_quotes s.sym_name)
+    Parsing.Parser.Lp.parse_term_string (pos_of_string s)
+      (String.remove_quotes s.sym_name)
   | _ -> fatal pos "not a string literal"
 
 (** [p_rwpatt_of_string_term pos t] turns into a p_rwpatt option a string
@@ -323,9 +331,8 @@ let p_rwpatt_of_string_term (pos:popt) (t:term): p_rwpatt option =
   match t with
   | Symb s when String.is_string_literal s.sym_name ->
       let string = String.remove_quotes s.sym_name in
-      if string = "" then None
-      else let p = lexing_opt (after s.sym_pos) in
-           Some (Parsing.Parser.Lp.parse_rwpatt_string p string)
+      if string = "" then None else
+        Some (Parsing.Parser.Lp.parse_rwpatt_string (pos_of_string s) string)
   | _ -> fatal pos "not a string literal"
 
 (** [int_of_term pos t] returns the int contained in a string literal

src/parsing/parser.ml

@@ -160,7 +160,6 @@ sig
     set_filename lb lexpos.pos_fname;
     Stream.next (parse_lexbuf' ~allow_rocq_syntax None entry lb)
 
-
   (* exported functions *)
   let parse_term_string =
     parse_entry_string ~allow_rocq_syntax:false LpParser.term
@@ -193,7 +192,6 @@ let path_of_string : string -> Path.t = fun s ->
       LpLexer.SyntaxError _ ->
       fatal_no_pos "Syntax error: \"%s\" is not a path." s
 
-
 (** [qident_of_string s] converts the string [s] into a qident. *)
 let qident_of_string : string -> Core.Term.qident = fun s ->
   let lb = Utf8.from_string s in

src/tool/lcr.ml

@@ -21,9 +21,9 @@ Warning: we currently do not take into account the rules having higher-order
 
 Remark: When trying to unify a subterm of a rule LHS with the LHS of another
    rule, we need to rename the pattern variables of one of the LHS to avoid
-   name clashes. To this end, we use the [shift] function below which replaces
-   [Patt(i,n,_)] by [Patt(-i-1,n ^ "'",_)]. The printing function [subs] below
-   takes this into account. *)
+   name clashes. To this end, we use the [reindex] function below which
+   replaces [Patt(i,n,_)] by [Patt(-i-1,n ^ "'",_)]. The printing function
+   [subs] below takes this into account. *)
 
 open Core open Term open Print
 open Timed
@@ -99,8 +99,8 @@ let occurs : int -> term -> bool = fun i ->
     | LLet _ -> assert false
   in occ
 
-(** [shift t] replaces in [t] every pattern index i by -i-1. *)
-let rec shift : term -> term = fun t ->
+(** [reindex t] replaces in [t] every pattern index i by -i-1. *)
+let rec reindex : term -> term = fun t ->
   match unfold t with
   | Vari _
   | Type
@@ -109,16 +109,16 @@ let rec shift : term -> term = fun t ->
   | Wild
   | Plac _
   | TRef _ -> t
-  | Prod(a,b) -> mk_Prod (shift a, shift_binder b)
-  | Abst(a,b) -> mk_Abst (shift a, shift_binder b)
-  | Appl(a,b) -> mk_Appl (shift a, shift b)
-  | Meta(m,ts) -> mk_Meta (m, Array.map shift ts)
+  | Prod(a,b) -> mk_Prod (reindex a, reindex_binder b)
+  | Abst(a,b) -> mk_Abst (reindex a, reindex_binder b)
+  | Appl(a,b) -> mk_Appl (reindex a, reindex b)
+  | Meta(m,ts) -> mk_Meta (m, Array.map reindex ts)
   | Patt(None,_,_) -> assert false
-  | Patt(Some i,n,ts) -> mk_Patt (Some(-i-1), n ^ "'", Array.map shift ts)
+  | Patt(Some i,n,ts) -> mk_Patt (Some(-i-1), n ^ "'", Array.map reindex ts)
   | Bvar _ -> assert false
-  | LLet(a,t,b) -> mk_LLet (shift a, shift t, shift_binder b)
-and shift_binder b =
-  let x, t = unbind b in bind_var x (shift t)
+  | LLet(a,t,b) -> mk_LLet (reindex a, reindex t, reindex_binder b)
+and reindex_binder b =
+  let x, t = unbind b in bind_var x (reindex t)
 
 (** Type for pattern variable substitutions. *)
 type subs = term IntMap.t
@@ -372,7 +372,7 @@ let iter_cps_with_rule :
   (*if Logger.log_enabled() then
     log_cp "iter_cps_with_rule@.%a@.%a" Print.rule lr Print.rule gd;*)
   let l = lhs lr and r = rhs lr and g = lhs gd and d = rhs gd in
-  let l = shift l and r = shift r in
+  let l = reindex l and r = reindex r in
   let i = id_sym_rule lr and j = id_sym_rule gd in
   let f _ p l_p = cp_cand_fun h pos i l r p l_p j g d in
   iter_subterms pos f l
@@ -555,7 +555,7 @@ let check_cps_subterms_eq : Pos.popt -> sym_rule -> unit =
   if Logger.log_enabled() then log_cp "check_cps_subterms_eq";
   (*if Logger.log_enabled() then
     log_cp "check_cps_subterms_eq@.%a@.%a" Print.rule lr Print.rule gd;*)
-  let l = shift (lhs lr) and r = shift (rhs lr) in
+  let l = reindex (lhs lr) and r = reindex (rhs lr) in
   let i = id_sym_rule lr in
   let f s p l_p =
     match !(s.sym_def) with