From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- proofs/clenv.ml | 194 +++++++++++++++++++++++++++++--------------------------- 1 file changed, 100 insertions(+), 94 deletions(-) (limited to 'proofs/clenv.ml') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 0a90e0db..03ff580a 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* 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 + | App (f, args) when isVar clenv.evd 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 @@ -71,15 +62,18 @@ let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c exception NotExtensibleClause +let mk_freelisted c = + map_fl EConstr.of_constr (mk_freelisted (EConstr.Unsafe.to_constr c)) + let clenv_push_prod cl = let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in - let rec clrec typ = match kind_of_term typ with + let rec clrec typ = match EConstr.kind cl.evd typ with | Cast (t,_,_) -> clrec t | Prod (na,t,u) -> let mv = new_meta () in - let dep = dependent (mkRel 1) u in + let dep = not (noccurn (cl_sigma cl) 1 u) in let na' = if dep then na else Anonymous in - let e' = meta_declare mv t ~name:na' cl.evd in + let e' = meta_declare mv (EConstr.Unsafe.to_constr t) ~name:na' cl.evd in let concl = if dep then subst1 (mkMeta mv) u else u in let def = applist (cl.templval.rebus,[mkMeta mv]) in { templval = mk_freelisted def; @@ -103,14 +97,17 @@ let clenv_push_prod cl = and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *) let clenv_environments evd bound t = + let open EConstr in + let open Vars in let rec clrec (e,metas) n t = - match n, kind_of_term t with + match n, EConstr.kind evd t with | (Some 0, _) -> (e, List.rev metas, t) | (n, Cast (t,_,_)) -> clrec (e,metas) n t | (n, Prod (na,t1,t2)) -> let mv = new_meta () in - let dep = not (noccurn 1 t2) in + let dep = not (noccurn evd 1 t2) in let na' = if dep then na else Anonymous in + let t1 = EConstr.Unsafe.to_constr t1 in let e' = meta_declare mv t1 ~name:na' e in clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n) (if dep then (subst1 (mkMeta mv) t2) else t2) @@ -128,11 +125,13 @@ let mk_clenv_from_env env sigma n (c,cty) = env = env } let mk_clenv_from_n gls n (c,cty) = - mk_clenv_from_env (pf_env gls) gls.sigma n (c, cty) + let env = Proofview.Goal.env gls in + let sigma = Tacmach.New.project gls in + mk_clenv_from_env env sigma n (c, cty) let mk_clenv_from gls = mk_clenv_from_n gls None -let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t) +let mk_clenv_type_of gls t = mk_clenv_from gls (t,Tacmach.New.pf_unsafe_type_of gls t) (******************************************************************) @@ -155,28 +154,28 @@ let error_incompatible_inst clenv mv = let na = meta_name clenv.evd mv in match na with Name id -> - errorlabstrm "clenv_assign" + user_err ~hdr:"clenv_assign" (str "An incompatible instantiation has already been found for " ++ - pr_id id) + Id.print id) | _ -> - anomaly ~label:"clenv_assign" (Pp.str "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 Metaset.exists (mentions clenv mv) rhs_fls.freemetas then - error "clenv_assign: circularity in unification"; + user_err Pp.(str "clenv_assign: circularity in unification"); try if meta_defined clenv.evd mv then - if not (Term.eq_constr (fst (meta_fvalue clenv.evd mv)).rebus rhs) then + if not (EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd mv)).rebus) rhs) then error_incompatible_inst clenv mv else clenv else let st = (Conv,TypeNotProcessed) in - {clenv with evd = meta_assign mv (rhs_fls.rebus,st) clenv.evd} + {clenv with evd = meta_assign mv (EConstr.Unsafe.to_constr rhs_fls.rebus,st) clenv.evd} with Not_found -> - error "clenv_assign: undefined meta" + user_err Pp.(str "clenv_assign: undefined meta") @@ -219,7 +218,7 @@ let clenv_assign mv rhs clenv = *) let clenv_metas_in_type_of_meta evd mv = - (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas + (mk_freelisted (meta_instance evd (map_fl EConstr.of_constr (meta_ftype evd mv)))).freemetas let dependent_in_type_of_metas clenv mvs = List.fold_right @@ -262,35 +261,38 @@ let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 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 concl = Goal.V82.concl clenv.evd (sig_it gl) in - if isMeta (fst (decompose_appvect (whd_nored clenv.evd clenv.templtyp.rebus))) then +let clenv_unique_resolver_gen ?(flags=default_unify_flags ()) clenv concl = + if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (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 old_clenv_unique_resolver ?flags clenv gl = + let concl = Goal.V82.concl clenv.evd (sig_it gl) in + clenv_unique_resolver_gen ?flags clenv concl + +let clenv_unique_resolver ?flags clenv gl = + let concl = Proofview.Goal.concl gl in + clenv_unique_resolver_gen ?flags clenv concl + 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 + match EConstr.kind evd c, l with + | Lambda (Name id,_,c), a::l when EConstr.eq_constr evd 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 + let f,l = decompose_app evd (EConstr.of_constr t.rebus) in + match EConstr.kind evd 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 + | Some (c,_) -> match_name (EConstr.of_constr c.rebus) l | None -> None) | _ -> None else None in @@ -332,13 +334,12 @@ let clenv_pose_metas_as_evars clenv dep_mvs = let ty = clenv_meta_type clenv mv in (* Postpone the evar-ization if dependent on another meta *) (* This assumes no cycle in the dependencies - is it correct ? *) - if occur_meta ty then fold clenv (mvs@[mv]) + if occur_meta clenv.evd ty then fold clenv (mvs@[mv]) else let src = evar_source_of_meta mv clenv.evd in let src = adjust_meta_source clenv.evd mv src in - let evd = Sigma.Unsafe.of_evar_map clenv.evd in - let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src ty in - let evd = Sigma.to_evar_map evd in + let evd = clenv.evd in + let (evd, evar) = new_evar (cl_env clenv) evd ~src ty in let clenv = clenv_assign mv evar {clenv with evd=evd} in fold clenv mvs in fold clenv dep_mvs @@ -404,7 +405,7 @@ type arg_bindings = constr explicit_bindings * of cval, ctyp. *) let clenv_independent clenv = - let mvs = collect_metas (clenv_value clenv) in + let mvs = collect_metas clenv.evd (clenv_value clenv) in let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in let deps = Metaset.union (dependent_in_type_of_metas clenv mvs) ctyp_mvs in List.filter (fun mv -> not (Metaset.mem mv deps)) mvs @@ -415,13 +416,13 @@ let qhyp_eq h1 h2 = match h1, h2 with | _ -> false let check_bindings bl = - match List.duplicates qhyp_eq (List.map pi2 bl) with + match List.duplicates qhyp_eq (List.map (fun {CAst.v=x} -> fst x) bl) with | NamedHyp s :: _ -> - errorlabstrm "" - (str "The variable " ++ pr_id s ++ + user_err + (str "The variable " ++ Id.print s ++ str " occurs more than once in binding list."); | AnonHyp n :: _ -> - errorlabstrm "" + user_err (str "The position " ++ int n ++ str " occurs more than once in binding list.") | [] -> () @@ -432,16 +433,16 @@ let explain_no_such_bound_variable evd id = | Cltyp (na, _) -> na | Clval (na, _, _) -> na in - if na != Anonymous then out_name na :: l else l + if na != Anonymous then Name.get_id na :: l else l in let mvl = List.fold_left fold [] (Evd.meta_list evd) in - errorlabstrm "Evd.meta_with_name" - (str"No such bound variable " ++ pr_id id ++ + user_err ~hdr:"Evd.meta_with_name" + (str"No such bound variable " ++ Id.print id ++ (if mvl == [] then str " (no bound variables at all in the expression)." else (str" (possible name" ++ str (if List.length mvl == 1 then " is: " else "s are: ") ++ - pr_enum pr_id mvl ++ str")."))) + pr_enum Id.print mvl ++ str")."))) let meta_with_name evd id = let na = Name id in @@ -460,8 +461,8 @@ let meta_with_name evd id = | ([n],_|_,[n]) -> n | _ -> - errorlabstrm "Evd.meta_with_name" - (str "Binder name \"" ++ pr_id id ++ + user_err ~hdr:"Evd.meta_with_name" + (str "Binder name \"" ++ Id.print id ++ strbrk "\" occurs more than once in clause.") let meta_of_binder clause loc mvs = function @@ -469,20 +470,20 @@ let meta_of_binder clause loc mvs = function | AnonHyp n -> try List.nth mvs (n-1) with (Failure _|Invalid_argument _) -> - errorlabstrm "" (str "No such binder.") + user_err (str "No such binder.") let error_already_defined b = match b with | NamedHyp id -> - errorlabstrm "" - (str "Binder name \"" ++ pr_id id ++ + user_err + (str "Binder name \"" ++ Id.print id ++ str"\" already defined with incompatible value.") | AnonHyp n -> anomaly (str "Position " ++ int n ++ str" already defined.") let clenv_unify_binding_type clenv c t u = - if isMeta (fst (decompose_appvect (whd_nored clenv.evd u))) then + if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd u))) then (* Not enough information to know if some subtyping is needed *) CoerceToType, clenv, c else @@ -499,8 +500,9 @@ let clenv_unify_binding_type clenv c t u = let clenv_assign_binding clenv k c = let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in - let c_typ = nf_betaiota clenv.evd (clenv_get_type_of clenv c) in + let c_typ = nf_betaiota clenv.env clenv.evd (clenv_get_type_of clenv c) in let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in + let c = EConstr.Unsafe.to_constr c in { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd } let clenv_match_args bl clenv = @@ -510,10 +512,10 @@ let clenv_match_args bl clenv = let mvs = clenv_independent clenv in check_bindings bl; List.fold_left - (fun clenv (loc,b,c) -> + (fun clenv {CAst.loc;v=(b,c)} -> let k = meta_of_binder clenv loc mvs b in if meta_defined clenv.evd k then - if Term.eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv + if EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd k)).rebus) c then clenv else error_already_defined b else clenv_assign_binding clenv k c) @@ -522,12 +524,12 @@ let clenv_match_args bl clenv = exception NoSuchBinding let clenv_constrain_last_binding c clenv = - let all_mvs = collect_metas clenv.templval.rebus in + let all_mvs = collect_metas clenv.evd clenv.templval.rebus 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 = - errorlabstrm "" + user_err (strbrk "Not the right number of missing arguments (expected " ++ int n ++ str ").") @@ -557,8 +559,9 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function let clause = mk_clenv_from_env env sigma n (c,t) in clenv_constrain_dep_args hyps_only largs clause | ExplicitBindings lbind -> + let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in let clause = mk_clenv_from_env env sigma n - (c,rename_bound_vars_as_displayed [] [] t) + (c, t) in clenv_match_args lbind clause | NoBindings -> mk_clenv_from_env env sigma n (c,t) @@ -585,34 +588,34 @@ let pr_clenv clenv = (** Evar version of mk_clenv *) type hole = { - hole_evar : constr; - hole_type : types; + hole_evar : EConstr.constr; + hole_type : EConstr.types; hole_deps : bool; hole_name : Name.t; } type clause = { cl_holes : hole list; - cl_concl : types; + cl_concl : EConstr.types; } let make_evar_clause env sigma ?len t = + let open EConstr in + let open Vars in 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 t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in let rec clrec (sigma, holes) n t = if n = 0 then (sigma, holes, t) - else match kind_of_term t with + else match EConstr.kind sigma 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 = Sigma.Unsafe.of_evar_map sigma in - let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in - let sigma = Sigma.to_evar_map sigma in - let dep = dependent (mkRel 1) t2 in + let (sigma, ev) = new_evar ~store env sigma t1 in + let dep = not (noccurn sigma 1 t2) in let hole = { hole_evar = ev; hole_type = t1; @@ -638,10 +641,10 @@ let explain_no_such_bound_variable holes id = 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 ")." + | [id] -> str "(possible name is: " ++ Id.print id ++ str ")." + | _ -> str "(possible names are: " ++ pr_enum Id.print mvl ++ str ")." in - errorlabstrm "" (str "No such bound variable " ++ pr_id id ++ expl) + user_err (str "No such bound variable " ++ Id.print id ++ expl) let evar_with_name holes id = let map h = match h.hole_name with @@ -653,38 +656,41 @@ let evar_with_name holes id = | [] -> explain_no_such_bound_variable holes id | [h] -> h.hole_evar | _ -> - errorlabstrm "" - (str "Binder name \"" ++ pr_id id ++ + user_err + (str "Binder name \"" ++ Id.print 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 + let nondeps = List.filter (fun hole -> not hole.hole_deps) holes in + let h = List.nth nondeps (pred n) in h.hole_evar with e when CErrors.noncritical e -> - errorlabstrm "" (str "No such binder.") + user_err (str "No such binder.") let define_with_type sigma env ev c = + let open EConstr in 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 + let (sigma, j) = Coercion.inh_conv_coerce_to true env sigma j t in + let (ev, _) = destEvar sigma ev in + let sigma = Evd.define ev (EConstr.Unsafe.to_constr j.Environ.uj_val) sigma in sigma let solve_evar_clause env sigma hyp_only clause = function | NoBindings -> sigma | ImplicitBindings largs -> + let open EConstr in 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 (ev, _) = destEvar sigma h.hole_evar in + let is_dep hole = occur_evar sigma 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 in_ccl = occur_evar sigma 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 @@ -704,7 +710,7 @@ let solve_evar_clause env sigma hyp_only clause = function error_not_right_number_missing_arguments len | ExplicitBindings lbind -> let () = check_bindings lbind in - let fold sigma (_, binder, c) = + let fold sigma {CAst.v=(binder, c)} = let ev = evar_of_binder clause.cl_holes binder in define_with_type sigma env ev c in -- cgit v1.2.3