Hi-level error message when subst fails

Author: strub

src/ecCorePrinting.ml

@@ -73,6 +73,15 @@ module type PrinterAPI = sig
 
   val pp_codepos     : PPEnv.t -> EcMatching.Position.codepos pp
 
+  (* ------------------------------------------------------------------ *)
+  type vsubst = [
+    | `Local of EcIdent.t
+    | `Glob  of EcIdent.t * EcMemory.memory
+    | `PVar  of EcTypes.prog_var * EcMemory.memory
+  ]
+  
+  val pp_vsubst : PPEnv.t -> vsubst pp
+
   (* ------------------------------------------------------------------ *)
   val pp_typedecl    : PPEnv.t -> (path * tydecl                  ) pp
   val pp_opdecl      : ?long:bool -> PPEnv.t -> (path * operator  ) pp

src/ecHiGoal.ml

@@ -1964,9 +1964,24 @@ let process_subst syms (tc : tcenv1) =
         "this formula is not subject to substitution"
   in
 
-  match List.map resolve syms with
-  | []   -> t_repeat t_subst tc
-  | syms -> FApi.t_seqs (List.map (fun var tc -> t_subst ~var tc) syms) tc
+  let exception NothingToSubstitute of vsubst in
+
+  try
+    match List.map resolve syms with
+    | []   -> t_repeat t_subst tc
+    | syms ->
+        FApi.t_seqs
+          (List.map
+            (fun var tc -> t_subst ~exn:(NothingToSubstitute var) ~var tc)
+            syms)
+          tc
+
+    with NothingToSubstitute v ->
+      tc_error_lazy !!tc (fun fmt ->
+        let ppe = EcPrinting.PPEnv.ofenv (FApi.tc1_env tc) in
+        Format.fprintf fmt "nothing to substitute for `%a'"
+        (EcPrinting.pp_vsubst ppe) v
+      )
 
 (* -------------------------------------------------------------------- *)
 type cut_t = intropattern * pformula * (ptactics located) option

src/ecLowGoal.ml

@@ -1937,7 +1937,7 @@ let t_rw_for_subst y togen concl side eqid tc =
             (* pre'; id: x = f |- (hpost => post => concl){x <- f} *)
             t_intros_i ids] tc
 
-let t_subst_x ?kind ?(except = Sid.empty) ?(clear = SCall) ?var ?tside ?eqid (tc : tcenv1) =
+let t_subst_x ?(exn = InvalidGoalShape) ?kind ?(except = Sid.empty) ?(clear = SCall) ?var ?tside ?eqid (tc : tcenv1) =
   let env, hyps, concl = FApi.tc1_eflat tc in
 
   let subst_pre (subst, check, depend) moved (id, lk) =
@@ -2047,11 +2047,11 @@ let t_subst_x ?kind ?(except = Sid.empty) ?(clear = SCall) ?var ?tside ?eqid (tc
   in
 
   try  List.find_map try1 eqs
-  with Not_found -> raise InvalidGoalShape
+  with Not_found -> raise exn
 
-let t_subst ?kind ?except ?(clear = true) ?var ?tside ?eqid (tc : tcenv1) =
+let t_subst ?exn ?kind ?except ?(clear = true) ?var ?tside ?eqid (tc : tcenv1) =
   let clear = if clear then SCall else SChyp in
-  fst (t_subst_x ?kind ?except ~clear ?var ?tside ?eqid tc)
+  fst (t_subst_x ?exn ?kind ?except ~clear ?var ?tside ?eqid tc)
 
 (* -------------------------------------------------------------------- *)
 let t_absurd_hyp ?(conv  = `AlphaEq) id tc =

src/ecLowGoal.mli

@@ -232,7 +232,8 @@ val t_rewrite_hyp :
 type tside = [`All of [`LtoR | `RtoL] option | `LtoR | `RtoL]
 
 val t_subst:
-     ?kind:subst_kind
+     ?exn:exn
+  -> ?kind:subst_kind
   -> ?except:Sid.t
   -> ?clear:bool
   -> ?var:vsubst

src/ecPrinting.ml

@@ -820,6 +820,22 @@ let pp_memtype (ppe : PPEnv.t) (fmt : Format.formatter) (mt : memtype) =
       let lty = Mty.bindings mty in
       Format.fprintf fmt "@[{%a}@]" (pp_list ",@ " pp_bind) lty
 
+(* -------------------------------------------------------------------- *)
+type vsubst = [
+  | `Local of EcIdent.t
+  | `Glob  of EcIdent.t * EcMemory.memory
+  | `PVar  of EcTypes.prog_var * EcMemory.memory
+]
+
+let pp_vsubst (ppe : PPEnv.t) (fmt : Format.formatter) (v : vsubst) =
+  match v with
+  | `Local x ->
+      Format.fprintf fmt "%a" (pp_local ppe) x
+  | `Glob (mp, m) ->
+      Format.fprintf fmt "(glob %a){%a}" (pp_topmod ppe) (EcPath.mident mp) (pp_mem ppe) m
+  | `PVar (pv, m) ->
+      Format.fprintf fmt "%a{%a}" (pp_pv ppe) pv (pp_mem ppe) m
+
 (* -------------------------------------------------------------------- *)
 let pp_opname (fmt : Format.formatter) ((nm, op) : symbol list * symbol) =
   let op =