Imported Upstream version 8.5~beta1+dfsg

1 files changed, 225 insertions, 70 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 8c66269e..2c9c695b 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -1,31 +1,29 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
 open Term
+open Vars
 open Termops
 open Namegen
-open Sign
 open Environ
 open Evd
 open Reduction
 open Reductionops
-open Glob_term
-open Pattern
 open Tacred
 open Pretype_errors
 open Evarutil
 open Unification
-open Mod_subst
-open Coercion.Default
+open Misctypes
 
 (* Abbreviations *)
 
@@ -44,10 +42,10 @@ type clausenv = {
 let cl_env ce = ce.env
 let cl_sigma ce =  ce.evd
 
-let subst_clenv sub clenv =
-  { templval = map_fl (subst_mps sub) clenv.templval;
-    templtyp = map_fl (subst_mps sub) clenv.templtyp;
-    evd = subst_evar_defs_light sub clenv.evd;
+let map_clenv sub clenv =
+  { templval = map_fl sub clenv.templval;
+    templtyp = map_fl sub clenv.templtyp;
+    evd = cmap sub clenv.evd;
     env = clenv.env }
 
 let clenv_nf_meta clenv c = nf_meta clenv.evd c
@@ -56,6 +54,15 @@ let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv
 let clenv_value clenv = meta_instance clenv.evd clenv.templval
 let clenv_type clenv = meta_instance clenv.evd clenv.templtyp
 
+let refresh_undefined_univs clenv =
+  match kind_of_term clenv.templval.rebus with
+  | Var _ -> clenv, Univ.empty_level_subst
+  | App (f, args) when isVar f -> clenv, Univ.empty_level_subst
+  | _ ->  
+    let evd', subst = Evd.refresh_undefined_universes clenv.evd in
+    let map_freelisted f = { f with rebus = subst_univs_level_constr subst f.rebus } in
+      { clenv with evd = evd'; templval = map_freelisted clenv.templval;
+	templtyp = map_freelisted clenv.templtyp }, subst
 
 let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
 
@@ -84,6 +91,16 @@ let clenv_push_prod cl =
 (* Instantiate the first [bound] products of [t] with metas (all products if
    [bound] is [None]; unfold local defs *)
 
+(** [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where
+   [lmetas] is a list of metas to be applied to a proof of [t] so that
+   it produces the unification pattern [ccl]; [sigma'] is [sigma]
+   extended with [lmetas]; if [n] is defined, it limits the size of
+   the list even if [ccl] is still a product; otherwise, it stops when
+   [ccl] is not a product; example: if [t] is [forall x y, x=y -> y=x]
+   and [n] is [None], then [lmetas] is [Meta n1;Meta n2;Meta n3] and
+   [ccl] is [Meta n1=Meta n2]; if [n] is [Some 1], [lmetas] is [Meta n1]
+   and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *)
+
 let clenv_environments evd bound t =
   let rec clrec (e,metas) n t =
     match n, kind_of_term t with
@@ -101,41 +118,13 @@ let clenv_environments evd bound t =
   in
   clrec (evd,[]) bound t
 
-(* Instantiate the first [bound] products of [t] with evars (all products if
-   [bound] is [None]; unfold local defs *)
-
-let clenv_environments_evars env evd bound t =
-  let rec clrec (e,ts) n t =
-    match n, kind_of_term t with
-      | (Some 0, _) -> (e, List.rev ts, t)
-      | (n, Cast (t,_,_)) -> clrec (e,ts) n t
-      | (n, Prod (na,t1,t2)) ->
-          let e',constr = Evarutil.new_evar e env t1 in
-	  let dep = dependent (mkRel 1) t2 in
-	  clrec (e', constr::ts) (Option.map ((+) (-1)) n)
-	    (if dep then (subst1 constr t2) else t2)
-      | (n, LetIn (na,b,_,t)) -> clrec (e,ts) n (subst1 b t)
-      | (n, _) -> (e, List.rev ts, t)
-  in
-  clrec (evd,[]) bound t
-
-let clenv_conv_leq env sigma t c bound =
-  let ty = Retyping.get_type_of env sigma c in
-  let evd = Evd.create_goal_evar_defs sigma in
-  let evars,args,_ = clenv_environments_evars env evd (Some bound) ty in
-  let evars = Evarconv.the_conv_x_leq env t (applist (c,args)) evars in
-  let evars = Evarconv.consider_remaining_unif_problems env evars in
-  let args = List.map (whd_evar evars) args in
-  check_evars env sigma evars (applist (c,args));
-  args
-
-let mk_clenv_from_env environ sigma n (c,cty) =
+let mk_clenv_from_env env sigma n (c,cty) =
   let evd = create_goal_evar_defs sigma in
   let (evd,args,concl) = clenv_environments evd n cty in
-  { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args));
+  { templval = mk_freelisted (applist (c,args));
     templtyp = mk_freelisted concl;
     evd = evd;
-    env = environ }
+    env = env }
 
 let mk_clenv_from_n gls n (c,cty) =
   mk_clenv_from_env (pf_env gls) gls.sigma n (c, cty)
@@ -152,13 +141,13 @@ let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
 
 let mentions clenv mv0 =
   let rec menrec mv1 =
-    mv0 = mv1 ||
+    Int.equal mv0 mv1 ||
     let mlist =
       try match meta_opt_fvalue clenv.evd mv1 with
       | Some (b,_) -> b.freemetas
       | None -> Metaset.empty
       with Not_found -> Metaset.empty in
-    meta_exists menrec mlist
+    Metaset.exists menrec mlist
   in menrec
 
 let error_incompatible_inst clenv mv  =
@@ -169,16 +158,16 @@ let error_incompatible_inst clenv mv  =
           (str "An incompatible instantiation has already been found for " ++
            pr_id id)
     | _ ->
-        anomaly "clenv_assign: non dependent metavar already assigned"
+        anomaly ~label:"clenv_assign" (Pp.str "non dependent metavar already assigned")
 
 (* TODO: replace by clenv_unify (mkMeta mv) rhs ? *)
 let clenv_assign mv rhs clenv =
   let rhs_fls = mk_freelisted rhs in
-  if meta_exists (mentions clenv mv) rhs_fls.freemetas then
+  if Metaset.exists (mentions clenv mv) rhs_fls.freemetas then
     error "clenv_assign: circularity in unification";
   try
     if meta_defined clenv.evd mv then
-      if not (eq_constr (fst (meta_fvalue clenv.evd mv)).rebus rhs) then
+      if not (Term.eq_constr (fst (meta_fvalue clenv.evd mv)).rebus rhs) then
         error_incompatible_inst clenv mv
       else
 	clenv
@@ -265,22 +254,49 @@ let clenv_dependent ce = clenv_dependent_gen false ce
 
 (******************************************************************)
 
-let clenv_unify ?(flags=default_unify_flags) cv_pb t1 t2 clenv =
+let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv =
   { clenv with
       evd = w_unify ~flags clenv.env clenv.evd cv_pb t1 t2 }
 
-let clenv_unify_meta_types ?(flags=default_unify_flags) clenv =
+let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
   { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
 
-let clenv_unique_resolver ?(flags=default_unify_flags) clenv gl =
+let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
   let concl = Goal.V82.concl clenv.evd (sig_it gl) in
-  if isMeta (fst (whd_stack clenv.evd clenv.templtyp.rebus)) then
+  if isMeta (fst (decompose_appvect (whd_nored clenv.evd clenv.templtyp.rebus))) then
     clenv_unify CUMUL ~flags (clenv_type clenv) concl
       (clenv_unify_meta_types ~flags clenv)
   else
     clenv_unify CUMUL ~flags
       (meta_reducible_instance clenv.evd clenv.templtyp) concl clenv
 
+let adjust_meta_source evd mv = function
+  | loc,Evar_kinds.VarInstance id ->
+    let rec match_name c l =
+      match kind_of_term c, l with
+      | Lambda (Name id,_,c), a::l when Constr.equal a (mkMeta mv) -> Some id
+      | Lambda (_,_,c), a::l -> match_name c l
+      | _ -> None in
+    (* This is very ad hoc code so that an evar inherits the name of the binder
+       in situations like "ex_intro (fun x => P) ?ev p" *)
+    let f = function (mv',(Cltyp (_,t) | Clval (_,_,t))) ->
+      if Metaset.mem mv t.freemetas then
+        let f,l = decompose_app t.rebus in
+        match kind_of_term f with
+        | Meta mv'' ->
+          (match meta_opt_fvalue evd mv'' with
+          | Some (c,_) -> match_name c.rebus l
+          | None -> None)
+        | Evar ev ->
+          (match existential_opt_value evd ev with
+          | Some c -> match_name c l
+          | None -> None)
+        | _ -> None
+      else None in
+    let id = try List.find_map f (Evd.meta_list evd) with Not_found -> id in
+    loc,Evar_kinds.VarInstance id
+  | src -> src
+
 (* [clenv_pose_metas_as_evars clenv dep_mvs]
  * For each dependent evar in the clause-env which does not have a value,
  * pose a value for it by constructing a fresh evar.  We do this in
@@ -317,14 +333,13 @@ let clenv_pose_metas_as_evars clenv dep_mvs =
       (* This assumes no cycle in the dependencies - is it correct ? *)
       if occur_meta ty then fold clenv (mvs@[mv])
       else
-	let (evd,evar) =
-	  new_evar clenv.evd (cl_env clenv) ~src:(dummy_loc,GoalEvar) ty in
+        let src = evar_source_of_meta mv clenv.evd in
+        let src = adjust_meta_source clenv.evd mv src in
+	let (evd,evar) = new_evar (cl_env clenv) clenv.evd ~src ty in
 	let clenv = clenv_assign mv evar {clenv with evd=evd} in
 	fold clenv mvs in
   fold clenv dep_mvs
 
-let evar_clenv_unique_resolver = clenv_unique_resolver
-
 (******************************************************************)
 
 let connect_clenv gls clenv =
@@ -333,6 +348,9 @@ let connect_clenv gls clenv =
     evd = evd ;
     env = Goal.V82.env evd (sig_it gls) }
 
+(* let connect_clenv_key = Profile.declare_profile "connect_clenv";; *)
+(* let connect_clenv = Profile.profile2 connect_clenv_key connect_clenv *)
+
 (* [clenv_fchain mv clenv clenv']
  *
  * Resolves the value of "mv" (which must be undefined) in clenv to be
@@ -357,11 +375,11 @@ let connect_clenv gls clenv =
    In particular, it assumes that [env'] and [sigma'] extend [env] and [sigma].
 *)
 
-let fchain_flags =
-  { default_unify_flags with
+let fchain_flags () =
+  { (default_unify_flags ()) with
     allow_K_in_toplevel_higher_order_unification = true }
 
-let clenv_fchain ?(flags=fchain_flags) mv clenv nextclenv =
+let clenv_fchain ?(flags=fchain_flags ()) mv clenv nextclenv =
   (* Add the metavars of [nextclenv] to [clenv], with their name-environment *)
   let clenv' =
     { templval = clenv.templval;
@@ -370,7 +388,7 @@ let clenv_fchain ?(flags=fchain_flags) mv clenv nextclenv =
       env = nextclenv.env } in
   (* unify the type of the template of [nextclenv] with the type of [mv] *)
   let clenv'' =
-    clenv_unify ~flags:flags CUMUL
+    clenv_unify ~flags CUMUL
       (clenv_term clenv' nextclenv.templtyp)
       (clenv_meta_type clenv' mv)
       clenv' in
@@ -397,8 +415,13 @@ let clenv_independent clenv =
   let deps = Metaset.union (dependent_in_type_of_metas clenv mvs) ctyp_mvs in
   List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
 
+let qhyp_eq h1 h2 = match h1, h2 with
+| NamedHyp n1, NamedHyp n2 -> Id.equal n1 n2
+| AnonHyp i1, AnonHyp i2 -> Int.equal i1 i2
+| _ -> false
+
 let check_bindings bl =
-  match list_duplicates (List.map pi2 bl) with
+  match List.duplicates qhyp_eq (List.map pi2 bl) with
     | NamedHyp s :: _ ->
 	errorlabstrm ""
 	  (str "The variable " ++ pr_id s ++
@@ -423,11 +446,11 @@ let error_already_defined b =
           (str "Binder name \"" ++ pr_id id ++
            str"\" already defined with incompatible value.")
     | AnonHyp n ->
-        anomalylabstrm ""
+        anomaly
           (str "Position " ++ int n ++ str" already defined.")
 
 let clenv_unify_binding_type clenv c t u =
-  if isMeta (fst (whd_stack clenv.evd u)) then
+  if isMeta (fst (decompose_appvect (whd_nored clenv.evd u))) then
     (* Not enough information to know if some subtyping is needed *)
     CoerceToType, clenv, c
   else
@@ -436,7 +459,8 @@ let clenv_unify_binding_type clenv c t u =
       let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in
       TypeProcessed, { clenv with evd = evd }, c
     with 
-      | PretypeError (_,_,NotClean _) as e -> raise e
+      | PretypeError (_,_,ActualTypeNotCoercible (_,_,NotClean _)) as e ->
+	  raise e
       | e when precatchable_exception e ->
 	  TypeNotProcessed, clenv, c
 
@@ -447,7 +471,7 @@ let clenv_assign_binding clenv k c =
   { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd }
 
 let clenv_match_args bl clenv =
-  if bl = [] then
+  if List.is_empty bl then
     clenv
   else
     let mvs = clenv_independent clenv in
@@ -456,7 +480,7 @@ let clenv_match_args bl clenv =
       (fun clenv (loc,b,c) ->
 	let k = meta_of_binder clenv loc mvs b in
         if meta_defined clenv.evd k then
-          if eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv
+          if Term.eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv
           else error_already_defined b
         else
 	  clenv_assign_binding clenv k c)
@@ -466,7 +490,7 @@ exception NoSuchBinding
 
 let clenv_constrain_last_binding c clenv =
   let all_mvs = collect_metas clenv.templval.rebus in
-  let k = try list_last all_mvs with Failure _ -> raise NoSuchBinding in
+  let k = try List.last all_mvs with Failure _ -> raise NoSuchBinding in
   clenv_assign_binding clenv k c
 
 let error_not_right_number_missing_arguments n =
@@ -475,17 +499,17 @@ let error_not_right_number_missing_arguments n =
       int n ++ str ").")
 
 let clenv_constrain_dep_args hyps_only bl clenv =
-  if bl = [] then
+  if List.is_empty bl then
     clenv
   else
     let occlist = clenv_dependent_gen hyps_only clenv in
-    if List.length occlist = List.length bl then
+    if Int.equal (List.length occlist) (List.length bl) then
       List.fold_left2 clenv_assign_binding clenv occlist bl
     else
       if hyps_only then
 	(* Tolerance for compatibility <= 8.3 *)
 	let occlist' = clenv_dependent_gen hyps_only ~iter:false clenv in
-	if List.length occlist' = List.length bl then
+	if Int.equal (List.length occlist') (List.length bl) then
 	  List.fold_left2 clenv_assign_binding clenv occlist' bl
 	else
 	  error_not_right_number_missing_arguments (List.length occlist)
@@ -508,9 +532,12 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
 
 let make_clenv_binding_env_apply env sigma n =
   make_clenv_binding_gen true n env sigma
+
+let make_clenv_binding_env env sigma =
+  make_clenv_binding_gen false None env sigma
 	
-let make_clenv_binding_apply gls n = make_clenv_binding_gen true n (pf_env gls) gls.sigma
-let make_clenv_binding gls = make_clenv_binding_gen false None (pf_env gls) gls.sigma
+let make_clenv_binding_apply env sigma n = make_clenv_binding_gen true n env sigma
+let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma
 
 (****************************************************************)
 (* Pretty-print *)
@@ -520,3 +547,131 @@ let pr_clenv clenv =
     (str"TEMPL: " ++ print_constr clenv.templval.rebus ++
      str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++
      pr_evar_map (Some 2) clenv.evd)
+
+(****************************************************************)
+(** Evar version of mk_clenv *)
+
+type hole = {
+  hole_evar : constr;
+  hole_type : types;
+  hole_deps  : bool;
+  hole_name : Name.t;
+}
+
+type clause = {
+  cl_holes : hole list;
+  cl_concl : types;
+}
+
+let make_evar_clause env sigma ?len t =
+  let bound = match len with
+  | None -> -1
+  | Some n -> assert (0 <= n); n
+  in
+  (** FIXME: do the renaming online *)
+  let t = rename_bound_vars_as_displayed [] [] t in
+  let rec clrec (sigma, holes) n t =
+    if n = 0 then (sigma, holes, t)
+    else match kind_of_term t with
+    | Cast (t, _, _) -> clrec (sigma, holes) n t
+    | Prod (na, t1, t2) ->
+      let store = Typeclasses.set_resolvable Evd.Store.empty false in
+      let sigma, ev = new_evar ~store env sigma t1 in
+      let dep = dependent (mkRel 1) t2 in
+      let hole = {
+        hole_evar = ev;
+        hole_type = t1;
+        hole_deps = dep;
+        (* We fix it later *)
+        hole_name = na;
+      } in
+      let t2 = if dep then subst1 ev t2 else t2 in
+      clrec (sigma, hole :: holes) (pred n) t2
+    | LetIn (na, b, _, t) -> clrec (sigma, holes) n (subst1 b t)
+    | _ -> (sigma, holes, t)
+  in
+  let (sigma, holes, t) = clrec (sigma, []) bound t in
+  let holes = List.rev holes in
+  let clause = { cl_concl = t; cl_holes = holes } in
+  (sigma, clause)
+
+let explain_no_such_bound_variable holes id =
+  let fold h accu = match h.hole_name with
+  | Anonymous -> accu
+  | Name id -> id :: accu
+  in
+  let mvl = List.fold_right fold holes [] in
+  let expl = match mvl with
+  | [] -> str " (no bound variables at all in the expression)."
+  | [id] -> str "(possible name is: " ++ pr_id id ++ str ")."
+  | _ -> str "(possible names are: " ++ pr_enum pr_id mvl ++ str ")."
+  in
+  errorlabstrm "" (str "No such bound variable " ++ pr_id id ++ expl)
+
+let evar_with_name holes id =
+  let map h = match h.hole_name with
+  | Anonymous -> None
+  | Name id' -> if Id.equal id id' then Some h else None
+  in
+  let hole = List.map_filter map holes in
+  match hole with
+  | [] -> explain_no_such_bound_variable holes id
+  | [h] -> h.hole_evar
+  | _ ->
+    errorlabstrm ""
+      (str "Binder name \"" ++ pr_id id ++
+        str "\" occurs more than once in clause.")
+
+let evar_of_binder holes = function
+| NamedHyp s -> evar_with_name holes s
+| AnonHyp n ->
+  try
+    let h = List.nth holes (pred n) in
+    h.hole_evar
+  with e when Errors.noncritical e ->
+    errorlabstrm "" (str "No such binder.")
+
+let define_with_type sigma env ev c =
+  let t = Retyping.get_type_of env sigma ev in
+  let ty = Retyping.get_type_of env sigma c in
+  let j = Environ.make_judge c ty in
+  let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j t in
+  let (ev, _) = destEvar ev in
+  let sigma = Evd.define ev j.Environ.uj_val sigma in
+  sigma
+
+let solve_evar_clause env sigma hyp_only clause = function
+| NoBindings -> sigma
+| ImplicitBindings largs ->
+  let fold holes h =
+    if h.hole_deps then
+      (** Some subsequent term uses the hole *)
+      let (ev, _) = destEvar h.hole_evar in
+      let is_dep hole = occur_evar ev hole.hole_type in
+      let in_hyp = List.exists is_dep holes in
+      let in_ccl = occur_evar ev clause.cl_concl in
+      let dep = if hyp_only then in_hyp && not in_ccl else in_hyp || in_ccl in
+      let h = { h with hole_deps = dep } in
+      h :: holes
+    else
+      (** The hole does not occur anywhere *)
+      h :: holes
+  in
+  let holes = List.fold_left fold [] (List.rev clause.cl_holes) in
+  let map h = if h.hole_deps then Some h.hole_evar else None in
+  let evs = List.map_filter map holes in
+  let len = List.length evs in
+  if Int.equal len (List.length largs) then
+    let fold sigma ev arg = define_with_type sigma env ev arg in
+    let sigma = List.fold_left2 fold sigma evs largs in
+    sigma
+  else
+    error_not_right_number_missing_arguments len
+| ExplicitBindings lbind ->
+  let () = check_bindings lbind in
+  let fold sigma (_, binder, c) =
+    let ev = evar_of_binder clause.cl_holes binder in
+    define_with_type sigma env ev c
+  in
+  let sigma = List.fold_left fold sigma lbind in
+  sigma