fix error message in SR checking

src/core/libTerm.ml

@@ -80,16 +80,20 @@ let distinct_vars : ctxt -> term array -> var array option = fun ctx ts ->
   in
   try Some (Array.map to_var ts) with Not_unique_var -> None
 
-(** If [ts] is not made of variables or function symbols prefixed by ['$']
-   only, then [nl_distinct_vars ts] returns [None]. Otherwise, it returns
-   a pair [(vs, map)] where [vs] is an array of variables made of the linear
-   variables of [ts] and fresh variables for the non-linear variables and the
-   symbols prefixed by ['$'], and [map] records by which variable each linear
-   symbol prefixed by ['$'] is replaced.
+(** Symbol name prefix used in [sr.ml] to recognize the symbols created to
+    forbid the instantiation of metavariables generated to replace the pattern
+    variables of a rule left hand-side when checking the type of right
+    hand-side. This prefix should not be a valid first character of an
+    identifier. *)
+let sym_meta_prefix = '$'
 
-   The symbols prefixed by ['$'] are introduced by [infer.ml] which converts
-   metavariables into fresh symbols, and those metavariables are introduced by
-   [sr.ml] which replaces pattern variables by metavariables. *)
+(** If [ts] is not made of variables or function symbols prefixed by
+    [sym_meta_perfix] only, then [nl_distinct_vars ts] returns
+    [None]. Otherwise, it returns a pair [(vs, map)] where [vs] is an array of
+    variables (of the same size of [ts]) made of the linear variables of [ts]
+    and fresh variables for the non-linear variables and the symbols prefixed
+    by [sym_meta_prefix], and [map] records by which variable each linear
+    symbol prefixed by [sym_meta_prefix] is replaced. *)
 let nl_distinct_vars : term array -> (var array * var StrMap.t) option =
   fun ts ->
   let exception Not_a_var in
@@ -104,7 +108,7 @@ let nl_distinct_vars : term array -> (var array * var StrMap.t) option =
         if VarSet.mem v !vars then nl_vars := VarSet.add v !nl_vars
         else vars := VarSet.add v !vars;
         v
-    | Symb(f) when f.sym_name <> "" && f.sym_name.[0] = '$' ->
+    | Symb(f) when f.sym_name <> "" && f.sym_name.[0] = sym_meta_prefix ->
         (* Symbols replacing pattern variables are considered as variables. *)
         let v =
           try StrMap.find f.sym_name !patt_vars
@@ -115,15 +119,13 @@ let nl_distinct_vars : term array -> (var array * var StrMap.t) option =
         in to_var (mk_Vari v)
     | _ -> raise Not_a_var
   in
-  let replace_nl_var v =
-    if VarSet.mem v !nl_vars then new_var "_" else v
-  in
+  let replace_nl_var v = if VarSet.mem v !nl_vars then new_var "_" else v in
   try
     let vs = Array.map to_var ts in
     let vs = Array.map replace_nl_var vs in
     (* We remove non-linear variables from [!patt_vars] as well. *)
-    let fn n v m = if VarSet.mem v !nl_vars then m else StrMap.add n v m in
-    let map = StrMap.fold fn !patt_vars StrMap.empty in
+    let f n v m = if VarSet.mem v !nl_vars then m else StrMap.add n v m in
+    let map = StrMap.fold f !patt_vars StrMap.empty in
     Some (vs, map)
   with Not_a_var -> None
 

src/core/print.ml

@@ -34,6 +34,12 @@ let print_contexts : bool ref = Console.register_flag "print_contexts" false
 (** Flag for printing metavariable arguments. *)
 let print_meta_args : bool ref = Console.register_flag "print_meta_args" false
 
+let print_implicits_and_domains_in f x =
+  let i = !print_implicits and d = !print_domains in
+  print_implicits := true; print_domains := true;
+  try let r = f x in print_implicits := i; print_domains := d; r
+  with e -> print_implicits := i; print_domains := d; raise e
+
 (*****************************************************************************
 printing functions
 *****************************************************************************)
@@ -278,7 +284,10 @@ and head idmap wrap ppf t =
   | Symb(s)     -> sym ppf s
   | Meta(m,e)   -> meta ppf m; if !print_meta_args then env (func idmap) ppf e
   | Plac(_)     -> out ppf "_"
-  | Patt(_,n,e) -> out ppf "$%a%a" uid n (env (func idmap)) e
+  | Patt(Some i,n,e) ->
+    if n="" then out ppf "$%d%a" i (env (func idmap)) e
+    else out ppf "$%s%a" n (env (func idmap)) e
+  | Patt(None,_,_) -> assert false
   | Bvar _      -> assert false
   (* Product and abstraction (only them can be wrapped). *)
   | Abst(a,b)   ->

src/parsing/lpLexer.ml

@@ -180,7 +180,6 @@ let escid = [%sedlex.regexp?
     "{|", nobars, '|', Star ('|' | Compl (Chars "|}"), nobars, '|'), '}']
 
 let id = [%sedlex.regexp? regid | escid]
-let pid = [%sedlex.regexp? id | strict_nat]
 
 (** Lexer. *)
 let rec token lb =
@@ -298,7 +297,7 @@ let rec token lb =
   | id -> UID(Utf8.lexeme lb)
   | '@', id -> UID_EXPL(remove_first lb)
   | '?', nat -> UID_META(int_of_string(remove_first lb))
-  | '$', pid -> UID_PATT(remove_first lb)
+  | '$', id -> UID_PATT(remove_first lb)
 
   | id, '.' -> qid false [remove_last lb] lb
   | '@', id, '.' -> qid true [remove_ends lb] lb

src/parsing/scope.ml

@@ -128,7 +128,7 @@ let fresh_patt : lhs_data -> string option -> term array -> term =
       mk_Patt (Some i, name, ts)
   | None ->
       let i = fresh_index () in
-      mk_Patt (Some i, string_of_int i, ts)
+      mk_Patt (Some i, "", ts)
 
 (* used in desugaring decimal notations *)
 let strint = Array.init 11 string_of_int

src/tool/sr.ml

@@ -34,24 +34,21 @@ let build_meta_type : problem -> int -> term = fun p k ->
   done;
   !res
 
-(** [symb_to_patt pos map names arities t] replaces in [t] every symbol [f]
-    such that [SymMap.find f map = Some(i)] by [Patt(i,names.(i),_)]. *)
+exception Meta_with_no_Patt of string
+
+(** [symb_to_patt pos s2p names arities t] replaces in [t] every symbol [f]
+    such that [SymMap.find f s2p = Some(i)] by [Patt(i,names.(i),_)]. *)
 let symb_to_patt : Pos.popt -> int option SymMap.t -> string array
                    -> int array -> term -> term =
-  fun pos map names arities ->
+  fun pos s2p names arities ->
   let rec symb_to_patt t =
     let (h, ts) = get_args t in
     let ts = List.map symb_to_patt ts in
     let (h, ts) =
       match h with
       | Symb(f) ->
-        begin match SymMap.find_opt f map with
-          | Some None ->
-            (* A symbol may also come from a metavariable that appeared in the
-               type of a metavariable that was replaced by a symbol. We do not
-               have concrete examples of that happening yet. *)
-            fatal pos "Bug. Introduced symbol [%s] cannot be removed. \
-                       Please contact the developers." f.sym_name
+        begin match SymMap.find_opt f s2p with
+          | Some None -> raise (Meta_with_no_Patt f.sym_name)
           | Some(Some(i)) ->
             let (ts1, ts2) = List.cut ts arities.(i) in
             (mk_Patt (Some i, names.(i), Array.of_list ts1), ts2)
@@ -103,7 +100,7 @@ let check_rule : Pos.popt -> sym_rule -> sym_rule =
             pattern variables are types and thus of sort KIND! *)
          LibMeta.fresh p (build_meta_type p arity) arity)
   in
-  (* Replace Patt's by Meta's. *)
+  (* Replace Patt's by Meta's of the same arity. *)
   let f m =
     let xs = Array.init m.meta_arity (new_var_ind "x") in
     let ts = Array.map mk_Vari xs in
@@ -119,44 +116,77 @@ let check_rule : Pos.popt -> sym_rule -> sym_rule =
   match Infer.infer_noexn p [] lhs_with_metas with
   | None -> fatal pos "The LHS is not typable."
   | Some (lhs_with_metas, ty_lhs) ->
-  (* Try to simplify constraints. *)
   if not (Unif.solve_noexn ~type_check:false p) then
     fatal pos "The LHS is not typable.";
+  (* Try to simplify constraints. *)
   let norm_constr (c,t,u) = (c, Eval.snf [] t, Eval.snf [] u) in
   let lhs_constrs = List.map norm_constr !p.unsolved in
   if Logger.log_enabled () then
     log_subj "@[<v>LHS type: %a@ LHS constraints: %a@ rule: %a ↪ %a@]"
       term ty_lhs constrs lhs_constrs
       term lhs_with_metas term rhs_with_metas;
   (* Instantiate all uninstantiated metavariables by fresh symbols. *)
-  (* map each symbol to its pattern index and arity *)
-  let map = Stdlib.ref SymMap.empty
-  (* map each meta to its symbol *)
-  and m2s = Stdlib.ref MetaMap.empty in
+  (* Map each uninstantiated meta to a fresh symbol. *)
+  let m2s = Stdlib.ref MetaMap.empty
+  (* Map each new symbol to Some pattern index if any, and None otherwise. *)
+  and s2p = Stdlib.ref SymMap.empty in
+  let sym_of_meta m =
+    let name = Printf.sprintf "%c%d" LibTerm.sym_meta_prefix m.meta_key in
+    Term.create_sym (Sign.current_path())
+      Privat Defin Eager false (Pos.none name) None !(m.meta_type) []
+  in
   let instantiate m =
     match !(m.meta_value) with
     | Some _ -> assert false
     | None ->
-      let s =
-        let name = Pos.none @@ Printf.sprintf "$%d" m.meta_key in
-        Term.create_sym (Sign.current_path())
-          Privat Defin Eager false name None !(m.meta_type) []
-      in
-      Stdlib.(map := SymMap.add s None !map; m2s := MetaMap.add m s !m2s);
+      let s = sym_of_meta m in
       let xs = Array.init m.meta_arity (new_var_ind "x") in
-      let s = mk_Symb s in
-      let def = Array.fold_left (fun t x -> mk_Appl (t, mk_Vari x)) s xs in
-      m.meta_value := Some(bind_mvar xs def)
+      let t =
+        Array.fold_left (fun t x -> mk_Appl(t,mk_Vari x)) (mk_Symb s) xs in
+      m.meta_value := Some(bind_mvar xs t);
+      if Logger.log_enabled() then
+        log_subj "%a[%d] -> %s" meta m m.meta_arity s.sym_name;
+      Stdlib.(m2s := MetaMap.add m s !m2s);
+      (* We record that this symbol needs to be eliminated. *)
+      Stdlib.(s2p := SymMap.add s None !s2p)
   in
   MetaSet.iter instantiate !p.metas;
-  (* For every [i], if the [i]-th meta is mapped to [s] in [m2s], then it has
-     not been instanciated and we map [s] to [i] and other data in [map]. *)
+  (* Map s to Some i if metas.(i) is mapped to s. *)
   let f i m =
     match MetaMap.find_opt m Stdlib.(!m2s) with
-    | Some s -> Stdlib.(map := SymMap.add s (Some i) !map)
+    | Some s ->
+      if Logger.log_enabled() then
+        log_subj "%s -> ?%d[%d]" s.sym_name i m.meta_arity;
+      Stdlib.(s2p := SymMap.add s (Some i) !s2p)
     | None -> ()
   in
   Array.iteri f metas;
+  (* If the meta associated to the pattern i is instantiated to another
+     meta/symbol s which is mapped to the pattern j, then we map s to i. *)
+  (*if Logger.log_enabled() then log_subj "---";
+  let f i m =
+    if Logger.log_enabled() then log_subj "%d" i;
+    match !(m.meta_value) with
+    | None -> ()
+    | Some b ->
+      let ts = Array.init m.meta_arity
+          (fun i -> mk_Vari (new_var_ind "x" i)) in
+      let t = msubst b ts in
+      if Logger.log_enabled() then log_subj "%a" term t;
+      match unfold t with
+      | Symb s ->
+        begin
+          match Stdlib.(SymMap.find_opt s !s2p) with
+          | Some None ->
+            if Logger.log_enabled() then
+              log_subj "%s[%d] -> ?%d[%d]"
+                s.sym_name m.meta_arity i arities.(i);
+            Stdlib.(s2p := SymMap.add s (Some i) !s2p)
+          | _ -> ()
+        end
+      | _ -> ()
+  in
+  Array.iteri f metas;*)
   if Logger.log_enabled () then
     log_subj "replace LHS metavariables by function symbols:@ %a ↪ %a"
       term lhs_with_metas term rhs_with_metas;
@@ -167,6 +197,9 @@ let check_rule : Pos.popt -> sym_rule -> sym_rule =
   match Infer.check_noexn p [] rhs_with_metas ty_lhs with
   | None -> fatal pos "The RHS does not have the same type as the LHS."
   | Some rhs_with_metas ->
+  if Logger.log_enabled () then
+    log_subj "rule after inference of RHS type:@ %a ↪ %a"
+      term lhs_with_metas term rhs_with_metas;
   (* Solving the typing constraints of the RHS. *)
   if not (Unif.solve_noexn p) then
     fatal pos "The rewriting rule does not preserve typing.";
@@ -205,8 +238,19 @@ let check_rule : Pos.popt -> sym_rule -> sym_rule =
       List.iter (fatal_msg "Cannot solve %a@." constr) cs;
       fatal pos "Unable to prove type preservation."
     end;
-  (* Replace metavariable symbols by Patt's. Here, in [map], a meta is mapped
-     to [Some i] if it is the [i]-th meta and is uninstantiated, and [None]
-     otherwise. *)
-  let rhs = symb_to_patt pos Stdlib.(!map) names arities rhs_with_metas in
-  s, {r with rhs}
+  if Logger.log_enabled () then
+    log_subj "rule after checking that the RHS has the same type:@ %a ↪ %a"
+      term lhs_with_metas term rhs_with_metas;
+  (* Replace metavariable symbols by patterns. *)
+  try
+    let rhs = symb_to_patt pos Stdlib.(!s2p) names arities rhs_with_metas in
+    s, {r with rhs}
+  with Meta_with_no_Patt n ->
+    (* The symbol comes from a metavariable appearing in the type of a
+       metavariable but corresponds to no pattern variable. *)
+    fatal pos "The rule obtained after typing is:@.%a@.↪ %a@.\
+               But %s cannot be deduced from the declared pattern \
+               variables.@.You need to explicit it."
+      term lhs_with_metas term rhs_with_metas n
+
+let check_rule p r = print_implicits_and_domains_in (check_rule p) r