summaryrefslogtreecommitdiff
path: root/proofs/clenv.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/clenv.ml')
-rw-r--r--proofs/clenv.ml194
1 files changed, 100 insertions, 94 deletions
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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Pp
@@ -12,11 +14,12 @@ open Util
open Names
open Nameops
open Term
-open Vars
open Termops
open Namegen
open Environ
open Evd
+open EConstr
+open Vars
open Reduction
open Reductionops
open Tacred
@@ -24,12 +27,6 @@ open Pretype_errors
open Evarutil
open Unification
open Misctypes
-open Sigma.Notations
-
-(* Abbreviations *)
-
-let pf_env = Refiner.pf_env
-let pf_type_of gls c = Typing.unsafe_type_of (pf_env gls) gls.sigma c
(******************************************************************)
(* Clausal environments *)
@@ -43,12 +40,6 @@ type clausenv = {
let cl_env ce = ce.env
let cl_sigma ce = ce.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
let clenv_term clenv c = meta_instance clenv.evd c
let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv
@@ -56,9 +47,9 @@ 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
+ match EConstr.kind clenv.evd clenv.templval.rebus with
| Var _ -> 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-08 02:35:43 +0000