From 2aa16013b4690faf17a4cf38527bee311c9651ca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 9 Jul 2026 15:51:42 +0200 Subject: [PATCH 1/3] fix virtual positions for symbols and rules generated by inductive --- src/common/pos.ml | 10 +++++----- src/export/dk.ml | 4 ++-- src/handle/command.ml | 28 +++++++++++++--------------- src/handle/inductive.ml | 6 +++--- src/handle/tactic.ml | 16 +++++++++++----- src/parsing/parser.ml | 2 -- src/tool/lcr.ml | 30 +++++++++++++++--------------- 7 files changed, 49 insertions(+), 47 deletions(-) diff --git a/src/common/pos.ml b/src/common/pos.ml index 395777779..aa251026e 100644 --- a/src/common/pos.ml +++ b/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 diff --git a/src/export/dk.ml b/src/export/dk.ml index c475afe27..a0bc82657 100644 --- a/src/export/dk.ml +++ b/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 diff --git a/src/handle/command.ml b/src/handle/command.ml index d0a10f141..de0938aa0 100644 --- a/src/handle/command.ml +++ b/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,6 +404,7 @@ 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 @@ -413,12 +412,11 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output = 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) diff --git a/src/handle/inductive.ml b/src/handle/inductive.ml index ff2eaa2bd..0fa4ac4f6 100644 --- a/src/handle/inductive.ml +++ b/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 diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index e82a4f6fa..fcb09c30e 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -304,14 +304,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 +330,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 diff --git a/src/parsing/parser.ml b/src/parsing/parser.ml index dcc83fa18..df74b37c3 100644 --- a/src/parsing/parser.ml +++ b/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 diff --git a/src/tool/lcr.ml b/src/tool/lcr.ml index 42719d12b..d6e5d6e64 100644 --- a/src/tool/lcr.ml +++ b/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 From 27a394946198459932f3748e0337f9d9ce441ada Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 9 Jul 2026 17:42:31 +0200 Subject: [PATCH 2/3] wip --- src/core/term.ml | 9 ++++++--- src/handle/tactic.ml | 7 ++++--- src/tool/indexing.ml | 4 ++-- 3 files changed, 12 insertions(+), 8 deletions(-) diff --git a/src/core/term.ml b/src/core/term.ml index 1791c8b57..19f661a75 100644 --- a/src/core/term.ml +++ b/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} *) diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index fcb09c30e..1c2b2ff0a 100644 --- a/src/handle/tactic.ml +++ b/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 diff --git a/src/tool/indexing.ml b/src/tool/indexing.ml index 2ef01751a..efcf2ac65 100644 --- a/src/tool/indexing.ml +++ b/src/tool/indexing.ml @@ -768,11 +768,11 @@ let index_sym sym = raise (Common.Error.Fatal (None,string_of_sym_name qname ^ " already indexed", "")); - DB.insert_name (snd qname) ((qname,sym.sym_decl_pos),[Name]) ; + DB.insert_name (snd qname) ((qname,sym.sym_pos),[Name]) ; (* Type + InType *) let typ = Timed.(!(sym.Core.Term.sym_type)) in index_term_and_subterms ~is_spine:true typ - (fun where -> ((qname,sym.sym_decl_pos),[Type where])) ; + (fun where -> ((qname,sym.sym_pos),[Type where])) ; (* InBody??? sym.sym_def : term option ref but all the subterms are too much; collect only the constants? *) (* Rules *) From 60558fbd660f78a5c1bf299dea1124b4696a65bc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 9 Jul 2026 23:05:12 +0200 Subject: [PATCH 3/3] revert changes in indexing.ml --- src/tool/indexing.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tool/indexing.ml b/src/tool/indexing.ml index efcf2ac65..2ef01751a 100644 --- a/src/tool/indexing.ml +++ b/src/tool/indexing.ml @@ -768,11 +768,11 @@ let index_sym sym = raise (Common.Error.Fatal (None,string_of_sym_name qname ^ " already indexed", "")); - DB.insert_name (snd qname) ((qname,sym.sym_pos),[Name]) ; + DB.insert_name (snd qname) ((qname,sym.sym_decl_pos),[Name]) ; (* Type + InType *) let typ = Timed.(!(sym.Core.Term.sym_type)) in index_term_and_subterms ~is_spine:true typ - (fun where -> ((qname,sym.sym_pos),[Type where])) ; + (fun where -> ((qname,sym.sym_decl_pos),[Type where])) ; (* InBody??? sym.sym_def : term option ref but all the subterms are too much; collect only the constants? *) (* Rules *)