From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- proofs/clenv.ml | 295 ++++++++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 225 insertions(+), 70 deletions(-) (limited to 'proofs/clenv.ml') 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 *) -(* 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 -- cgit v1.2.3