Made the subterm finding function make_abstraction independent of the

proof engine. Moved it to unification.ml.

8 files changed, 211 insertions, 34 deletions

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 003665db59..d8f51054d2 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -46,6 +46,7 @@ type pretype_error =
   | UnexpectedType of constr * constr
   | NotProduct of constr
   | TypingError of type_error
+  | CannotUnifyOccurrences of Termops.subterm_unification_error
 
 exception PretypeError of env * Evd.evar_map * pretype_error
 
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index d9ee969e3c..f8e39f3164 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -47,6 +47,7 @@ type pretype_error =
   | UnexpectedType of constr * constr
   | NotProduct of constr
   | TypingError of type_error
+  | CannotUnifyOccurrences of Termops.subterm_unification_error
 
 exception PretypeError of env * Evd.evar_map * pretype_error
 
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index a4c72f4828..f1a9d6915b 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -26,8 +26,8 @@ Typeclasses
 Classops
 Program
 Coercion
-Unification
 Detyping
 Indrec
 Cases
 Pretyping
+Unification
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index a32d54b5e6..75f6f66fec 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -22,6 +22,7 @@ open Reductionops
 open Cbv
 open Patternops
 open Locus
+open Pretype_errors
 
 (* Errors *)
 
@@ -960,7 +961,7 @@ let e_contextually byhead (occs,c) f env sigma t =
   in
   let t' = traverse (env,c) t in
   if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs;
-    !evd, t'
+  !evd, t'
 
 let contextually byhead occs f env sigma t =
   let f' subst env sigma t = sigma, f subst env sigma t in
@@ -1075,9 +1076,9 @@ let compute = cbv_betadeltaiota
 (* Pattern *)
 
 let make_eq_univs_test evd c =
-  { match_fun = (fun evd c' -> 
-    let b, cst = Universes.eq_constr_universes c c' in 
-      if b then 
+  { match_fun = (fun evd c' ->
+    let b, cst = Universes.eq_constr_universes c c' in
+      if b then
 	try Evd.add_universe_constraints evd cst
 	with Evd.UniversesDiffer -> raise NotUnifiable
       else raise NotUnifiable);
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index d9cd58cea8..67559e6863 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -679,30 +679,33 @@ let replace_term = replace_term_gen eq_constr
    occurrence except the ones in l and b=false, means all occurrences
    except the ones in l *)
 
-let error_invalid_occurrence l =
+type occurrence_error =
+  | InvalidOccurrence of int list
+  | IncorrectInValueOccurrence of Id.t
+
+let explain_invalid_occurrence l =
   let l = List.sort_uniquize Int.compare l in
-  errorlabstrm ""
-    (str ("Invalid occurrence " ^ String.plural (List.length l) "number" ^": ") ++
-     prlist_with_sep spc int l ++ str ".")
-
-let pr_position (cl,pos) =
-  let clpos = match cl with
-    | None -> str " of the goal"
-    | Some (id,InHyp) -> str " of hypothesis " ++ pr_id id
-    | Some (id,InHypTypeOnly) -> str " of the type of hypothesis " ++ pr_id id
-    | Some (id,InHypValueOnly) -> str " of the body of hypothesis " ++ pr_id id in
-  int pos ++ clpos
-
-let error_cannot_unify_occurrences nested (cl2,pos2,t2) (cl1,pos1,t1) =
-  let s = if nested then "Found nested occurrences of the pattern"
-    else "Found incompatible occurrences of the pattern" in
-  errorlabstrm ""
-    (str s ++ str ":" ++
-     spc () ++ str "Matched term " ++ quote (print_constr t2) ++
-     strbrk " at position " ++ pr_position (cl2,pos2) ++ 
-     strbrk " is not compatible with matched term " ++
-     quote (print_constr t1) ++ strbrk " at position " ++ 
-     pr_position (cl1,pos1) ++ str ".")
+  str ("Invalid occurrence " ^ String.plural (List.length l) "number" ^": ")
+  ++ prlist_with_sep spc int l ++ str "."
+
+let explain_incorrect_in_value_occurrence id =
+  pr_id id ++ str " has no value."
+
+let explain_occurrence_error = function
+  | InvalidOccurrence l -> explain_invalid_occurrence l
+  | IncorrectInValueOccurrence id -> explain_incorrect_in_value_occurrence id
+
+let error_occurrences_error e =
+  errorlabstrm "" (explain_occurrence_error e)
+
+let error_invalid_occurrence occ =
+  error_occurrences_error (InvalidOccurrence occ)
+
+type position =(Id.t * Locus.hyp_location_flag) option
+
+type subterm_unification_error = bool * (position * int * constr) * (position * int * constr)
+
+exception SubtermUnificationError of subterm_unification_error
 
 exception NotUnifiable
 
@@ -724,7 +727,7 @@ let subst_closed_term_occ_gen_modulo occs test cl occ t =
       test.last_found <- Some (cl,!pos,t)
     with NotUnifiable ->
       let lastpos = Option.get test.last_found in
-      error_cannot_unify_occurrences !nested (cl,!pos,t) lastpos in
+     raise (SubtermUnificationError (!nested,(cl,!pos,t),lastpos)) in
   let rec substrec k t =
     if nowhere_except_in && !pos > maxocc then t else
     try
@@ -749,7 +752,7 @@ let check_used_occurrences nbocc (nowhere_except_in,locs) =
   let rest = List.filter (fun o -> o >= nbocc) locs in
   match rest with
   | [] -> ()
-  | _ -> error_invalid_occurrence rest
+  | _ -> error_occurrences_error (InvalidOccurrence rest)
 
 let proceed_with_occurrences f occs x =
   match occs with
@@ -785,7 +788,7 @@ let map_named_declaration_with_hyploc f hyploc acc (id,bodyopt,typ) =
   let f = f (Some (id,hyploc)) in
   match bodyopt,hyploc with
   | None, InHypValueOnly ->
-      errorlabstrm "" (pr_id id ++ str " has no value.")
+      error_occurrences_error (IncorrectInValueOccurrence id)
   | None, _ | Some _, InHypTypeOnly ->
       let acc,typ = f acc typ in acc,(id,bodyopt,typ)
   | Some body, InHypValueOnly ->
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 8b4d02e046..72a1152313 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -155,7 +155,16 @@ val subst_closed_term_occ_gen :
     testing function returning a substitution of type ['a] (or failing
     with NotUnifiable); a function for merging substitution (possibly
     failing with NotUnifiable) and an initial substitution are
-    required too *)
+    required too; [subst_closed_term_occ_modulo] itself turns a
+    NotUnifiable exception into a SubtermUnificationError *)
+
+exception NotUnifiable
+
+type position =(Id.t * Locus.hyp_location_flag) option
+
+type subterm_unification_error = bool * (position * int * constr) * (position * int * constr)
+
+exception SubtermUnificationError of subterm_unification_error
 
 type 'a testing_function = {
   match_fun : 'a -> constr -> 'a;
@@ -166,8 +175,6 @@ type 'a testing_function = {
 
 val make_eq_test : constr -> unit testing_function
 
-exception NotUnifiable
-
 val subst_closed_term_occ_modulo :
   occurrences -> 'a testing_function -> (Id.t * hyp_location_flag) option
   -> constr -> types
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 219d03b9e7..dbdc0a4e40 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -24,6 +24,7 @@ open Retyping
 open Coercion
 open Recordops
 open Locus
+open Locusops
 
 let occur_meta_or_undefined_evar evd c =
   let rec occrec c = match kind_of_term c with
@@ -1156,6 +1157,153 @@ let iter_fail f a =
       with ex when precatchable_exception ex -> ffail (i+1)
   in ffail 0
 
+(* make_abstraction: a variant of w_unify_to_subterm which works on
+   contexts, with evars, and possibly with occurrences *)
+
+let out_arg = function
+  | Misctypes.ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable")
+  | Misctypes.ArgArg x -> x
+
+let occurrences_of_hyp id cls =
+  let rec hyp_occ = function
+      [] -> None
+    | ((occs,id'),hl)::_ when Id.equal id id' ->
+        Some (occurrences_map (List.map out_arg) occs, hl)
+    | _::l -> hyp_occ l in
+  match cls.onhyps with
+      None -> Some (AllOccurrences,InHyp)
+    | Some l -> hyp_occ l
+
+let occurrences_of_goal cls =
+  if cls.concl_occs == NoOccurrences then None
+  else Some (occurrences_map (List.map out_arg) cls.concl_occs)
+
+let in_every_hyp cls = Option.is_empty cls.onhyps
+
+let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env initial_sigma (sigma,c) =
+  let sigma = Pretyping.solve_remaining_evars flags env initial_sigma sigma
+  in Evd.evar_universe_context sigma, nf_evar sigma c
+
+let default_matching_flags sigma = {
+  modulo_conv_on_closed_terms = Some empty_transparent_state;
+  use_metas_eagerly_in_conv_on_closed_terms = false;
+  modulo_delta = empty_transparent_state;
+  modulo_delta_types = full_transparent_state;
+  modulo_delta_in_merge = Some full_transparent_state;
+  check_applied_meta_types = true;
+  resolve_evars = false;
+  use_pattern_unification = false;
+  use_meta_bound_pattern_unification = false;
+  frozen_evars =
+    fold_undefined (fun evk _ evars -> Evar.Set.add evk evars)
+      sigma Evar.Set.empty;
+  restrict_conv_on_strict_subterms = false;
+  modulo_betaiota = false;
+  modulo_eta = false;
+  allow_K_in_toplevel_higher_order_unification = false
+}
+
+(* This supports search of occurrences of term from a pattern *)
+
+let make_pattern_test inf_flags env sigma0 (sigma,c) =
+  let flags = default_matching_flags sigma0 in
+  let matching_fun _ t =
+    try let sigma = w_typed_unify env sigma Reduction.CONV flags c t in
+	  Some(sigma, t)
+    with e when Errors.noncritical e -> raise NotUnifiable in
+  let merge_fun c1 c2 =
+    match c1, c2 with
+    | Some (evd,c1), Some (_,c2) ->
+      (try let evd = w_typed_unify env evd Reduction.CONV flags c1 c2 in
+	     Some (evd, c1)
+       with e when Errors.noncritical e -> raise NotUnifiable)
+    | Some _, None -> c1
+    | None, Some _ -> c2
+    | None, None -> None
+  in
+  { match_fun = matching_fun; merge_fun = merge_fun;
+    testing_state = None; last_found = None },
+  (fun test -> match test.testing_state with
+  | None ->
+      finish_evar_resolution ~flags:inf_flags env sigma0 (sigma,c)
+  | Some (sigma,_) ->
+     let univs, subst = nf_univ_variables sigma in
+     Evd.evar_universe_context univs,
+     subst_univs_constr subst (nf_evar sigma c))
+
+let make_eq_test evd c =
+  let out cstr =
+    Evd.evar_universe_context cstr.testing_state, c
+  in
+    (Tacred.make_eq_univs_test evd c, out)
+
+let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env concl =
+  let id =
+    let t = match ty with Some t -> t | None -> get_type_of env sigmac c in
+    let x = id_of_name_using_hdchar (Global.env()) t name in
+    let ids = ids_of_named_context (named_context env) in
+    if name == Anonymous then next_ident_away_in_goal x ids else
+    if mem_named_context x (named_context env) then
+      error ("The variable "^(Id.to_string x)^" is already declared.")
+    else
+      x
+  in
+  let compute_dependency _ (hyp,_,_ as d) depdecls =
+    match occurrences_of_hyp hyp occs with
+    | None -> depdecls
+    | Some ((AllOccurrences, InHyp) as occ) ->
+        let newdecl = subst_closed_term_occ_decl_modulo occ test d in
+        if Context.eq_named_declaration d newdecl then
+          if check_occs && not (in_every_hyp occs)
+          then raise (PretypeError (env,sigmac,NoOccurrenceFound (c,Some hyp)))
+          else depdecls
+        else
+          (subst1_named_decl (mkVar id) newdecl)::depdecls
+    | Some occ ->
+        let newdecl = subst_closed_term_occ_decl_modulo occ test d in
+        (subst1_named_decl (mkVar id) newdecl)::depdecls in
+  try
+    let depdecls = fold_named_context compute_dependency env ~init:[] in
+    let ccl = match occurrences_of_goal occs with
+      | None -> concl
+      | Some occ ->
+          subst1 (mkVar id) (subst_closed_term_occ_modulo occ test None concl)
+    in
+    let lastlhyp =
+      if List.is_empty depdecls then None else Some (pi1(List.last depdecls)) in
+    (id,depdecls,lastlhyp,ccl,out test)
+  with
+    SubtermUnificationError e ->
+      raise (PretypeError (env,sigmac,CannotUnifyOccurrences e))
+
+(** [make_abstraction] is the main entry point to abstract over a term
+    or pattern at some occurrences; it returns:
+    - the id used for the abstraction
+    - the type of the abstraction
+    - the hypotheses from the context which depend on the term or pattern
+    - the most recent hyp before which there is no dependency in the term of pattern
+    - the abstracted conclusion
+    - an evar universe context effect to apply on the goal
+    - the term or pattern to abstract fully instantiated
+*)
+
+type abstraction_request =
+| AbstractPattern of Name.t * (evar_map * constr) * clause * bool * Pretyping.inference_flags
+| AbstractExact of Name.t * constr * types option * clause * bool
+
+type abstraction_result =
+  Names.Id.t * Context.named_declaration list * Names.Id.t option *
+    constr * (Evd.evar_universe_context * constr)
+
+let make_abstraction env evd ccl abs =
+  match abs with
+  | AbstractPattern (name,c,occs,check_occs,flags) ->
+      make_abstraction_core name
+        (make_pattern_test flags env evd c) c None occs check_occs env ccl
+  | AbstractExact (name,c,ty,occs,check_occs) ->
+      make_abstraction_core name
+        (make_eq_test evd c) (evd,c) ty occs check_occs env ccl
+
 (* Tries to find an instance of term [cl] in term [op].
    Unifies [cl] to every subterm of [op] until it finds a match.
    Fails if no match is found *)
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 3f93d817d2..de8eecc274 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -53,6 +53,22 @@ val w_unify_meta_types : env -> ?flags:unify_flags -> evar_map -> evar_map
 val w_coerce_to_type : env -> evar_map -> constr -> types -> types ->
   evar_map * constr
 
+(* Looking for subterms in contexts at some occurrences, possibly with pattern*)
+
+type abstraction_request =
+| AbstractPattern of Names.Name.t * (evar_map * constr) * Locus.clause * bool * Pretyping.inference_flags
+| AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool
+
+val finish_evar_resolution : ?flags:Pretyping.inference_flags ->
+  env -> Evd.evar_map -> open_constr -> Evd.evar_universe_context * constr
+
+type abstraction_result =
+  Names.Id.t * Context.named_declaration list * Names.Id.t option *
+    constr * (Evd.evar_universe_context * constr)
+
+val make_abstraction : env -> Evd.evar_map -> constr ->
+  abstraction_request -> abstraction_result
+
 (*i This should be in another module i*)
 
 (** [abstract_list_all env evd t c l]