aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/evarconv.ml5
-rw-r--r--pretyping/evarutil.ml202
-rw-r--r--pretyping/evarutil.mli2
-rw-r--r--pretyping/evd.ml9
-rw-r--r--pretyping/pretyping.ml14
-rw-r--r--pretyping/typing.ml61
-rw-r--r--tactics/equality.ml2
7 files changed, 170 insertions, 125 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 4af5a43cf..047b306ed 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -177,8 +177,9 @@ let rec evar_conv_x env isevars pbty term1 term2 =
true
else
*)
- (* Maybe convertible but since reducing can erase evars which [evar_apprec]*)
- (* could have found, we do it only if the terms are free of evar *)
+ (* Maybe convertible but since reducing can erase evars which [evar_apprec]
+ could have found, we do it only if the terms are free of evar.
+ Note: incomplete heuristic... *)
if
(not (has_undefined_evars isevars term1) &
not (has_undefined_evars isevars term2) &
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 746d2cd8e..0e87e5893 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -28,25 +28,6 @@ let rec filter_unique = function
if List.mem x l then filter_unique (List.filter (fun y -> x<>y) l)
else x::filter_unique l
-(*
-let distinct_id_list =
- let rec drec fresh = function
- [] -> List.rev fresh
- | id::rest ->
- let id' = next_ident_away_from id fresh in drec (id'::fresh) rest
- in drec []
-*)
-
-(*
-let filter_sign p sign x =
- sign_it
- (fun id ty (v,ids,sgn) ->
- let (disc,v') = p v (id,ty) in
- if disc then (v', id::ids, sgn) else (v', ids, add_sign (id,ty) sgn))
- sign
- (x,[],nil_sign)
-*)
-
(* Expanding existential variables (pretyping.ml) *)
(* 1- whd_ise fails if an existential is undefined *)
@@ -133,6 +114,16 @@ let evars_to_metas sigma (emap, c) =
| _ -> map_constr replace c in
(sigma', replace c)
+(* The list of non-instantiated existential declarations *)
+
+let non_instantiated sigma =
+ let listev = to_list sigma in
+ List.fold_left
+ (fun l (ev,evd) ->
+ if evd.evar_body = Evar_empty then
+ ((ev,nf_evar_info sigma evd)::l) else l)
+ [] listev
+
(*************************************)
(* Metas *)
@@ -229,13 +220,79 @@ let e_new_evar evd env ?(src=(dummy_loc,InternalHole)) ty =
evd := evd';
ev
-(* declare a new evar (tactic style) *)
-let w_Declare env sp ty evd =
- let sigma = evars_of evd in
- if Evd.in_dom sigma sp then
- error "w_Declare: cannot redeclare evar";
- let _ = Typing.type_of env sigma ty in (* Checks there is no meta *)
- Evd.evar_declare (named_context env) sp ty evd
+(*------------------------------------*
+ * operations on the evar constraints *
+ *------------------------------------*)
+
+let is_pattern inst =
+ let rec is_hopat l = function
+ [] -> true
+ | t :: tl ->
+ (isRel t or isVar t) && not (List.mem t l) && is_hopat (t::l) tl in
+ is_hopat [] (Array.to_list inst)
+
+let evar_well_typed_body evd ev evi body =
+ try
+ let env = evar_env evi in
+ let ty = evi.evar_concl in
+ Typing.check env (evars_of evd) body ty;
+ true
+ with e ->
+ pperrnl
+ (str "Ill-typed evar instantiation: " ++ fnl() ++
+ pr_evar_defs evd ++ fnl() ++
+ str "----> " ++ int ev ++ str " := " ++
+ print_constr body);
+ false
+
+let strict_inverse = false
+
+let inverse_instance env isevars ev evi inst rhs =
+ let subst = make_subst (evar_env evi) (Array.to_list inst) in
+ let subst = List.map (fun (x,y) -> (y,mkVar x)) subst in
+ let evd = ref isevars in
+ let error () =
+ error_not_clean env (evars_of !evd) ev rhs (evar_source ev !evd) in
+ let rec subs rigid k t =
+ match kind_of_term t with
+ | Rel i ->
+ if i<=k then t
+ else
+ (try List.assoc (mkRel (i-k)) subst
+ with Not_found ->
+ if rigid then error()
+ else if strict_inverse then
+ failwith "cannot solve pb yet"
+ else t)
+ | Var id ->
+ (try List.assoc t subst
+ with Not_found ->
+ if rigid then error()
+ else if
+ not strict_inverse &&
+ List.exists (fun (id',_,_) -> id=id') evi.evar_hyps
+ then
+ failwith "cannot solve pb yet"
+ else t)
+ | Evar (ev,args) ->
+ if Evd.is_defined_evar !evd (ev,args) then
+ subs rigid k (existential_value (evars_of !evd) (ev,args))
+ else
+ let args' = Array.map (subs false k) args in
+ mkEvar (ev,args')
+ | _ -> map_constr_with_binders succ (subs rigid) k t in
+ let body = subs true 0 (nf_evar (evars_of isevars) rhs) in
+ (!evd,body)
+
+
+let is_defined_equation env evd (ev,inst) rhs =
+ is_pattern inst &&
+ not (occur_evar ev rhs) &&
+ try
+ let evi = Evd.map (evars_of evd) ev in
+ let (evd',body) = inverse_instance env evd ev evi inst rhs in
+ evar_well_typed_body evd' ev evi body
+ with Failure _ -> false
(* Redefines an evar with a smaller context (i.e. it may depend on less
@@ -259,23 +316,7 @@ let do_restrict_hyps evd ev args =
nc
-
-
-(*------------------------------------*
- * operations on the evar constraints *
- *------------------------------------*)
-
let need_restriction isevars args = not (array_for_all closed0 args)
-
-(* The list of non-instantiated existential declarations *)
-
-let non_instantiated sigma =
- let listev = to_list sigma in
- List.fold_left
- (fun l (ev,evd) ->
- if evd.evar_body = Evar_empty then
- ((ev,nf_evar_info sigma evd)::l) else l)
- [] listev
(* We try to instanciate the evar assuming the body won't depend
* on arguments that are not Rels or Vars, or appearing several times.
@@ -318,30 +359,6 @@ let real_clean env isevars ev evi args rhs =
then error_not_clean env (evars_of !evd) ev body (evar_source ev !evd);
(!evd,body)
-(* [typed_evar_define evd sp c] (tactic style)
- *
- * Defines evar [sp] with term [c] in evar context [evd].
- * [c] is typed in the context of [sp] and evar context [evd] with
- * [sp] removed to avoid circular definitions.
- * No unification is performed in order to assert that [c] has the
- * correct type.
- *
-let typed_evar_define sp c evd =
- let sigma = evars_of evd in
- let spdecl = Evd.map sigma sp in
- let env = evar_env spdecl in
- let _ =
- (* Do not consider the metamap because evars may not depend on metas *)
- try Typing.check env (Evd.rmv sigma sp) c spdecl.evar_concl
- with
- Not_found -> error "Instantiation contains unlegal variables"
- | (Type_errors.TypeError (e, Type_errors.UnboundVar v))->
- errorlabstrm "typed_evar_define"
- (str "Cannot use variable " ++ pr_id v ++ str " to define " ++
- str (string_of_existential sp)) in
- Evd.evar_define sp c evd
-*)
-
(* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated
* evar, i.e. tries to find the body ?sp for lhs=mkEvar (sp,args)
* ?sp [ sp.hyps \ args ] unifies to rhs
@@ -370,8 +387,20 @@ let evar_define env (ev,argsv) rhs isevars =
let (isevars',body) = real_clean env isevars ev evi worklist rhs in
if occur_meta body then error "Meta cannot occur in evar body"
else
- let isevars'' = Evd.evar_define ev body isevars' in
- isevars'',[ev]
+ let _ =
+(* try*)
+ let env = evar_env evi in
+ let ty = evi.evar_concl in
+ Typing.check env (evars_of isevars') body ty
+(* with e ->
+ pperrnl
+ (str "Ill-typed evar instantiation: " ++ fnl() ++
+ pr_evar_defs isevars' ++ fnl() ++
+ str "----> " ++ int ev ++ str " := " ++
+ print_constr body);
+ raise e*) in
+ let isevars'' = Evd.evar_define ev body isevars' in
+ isevars'',[ev]
@@ -477,23 +506,26 @@ let solve_refl conv_algo env isevars ev argsv1 argsv2 =
(* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
- let t2 = nf_evar (evars_of isevars) t2 in
- let (isevars,lsp) = match kind_of_term t2 with
- | Evar (n2,args2 as ev2) ->
- if n1 = n2 then
- solve_refl conv_algo env isevars n1 args1 args2
- else
- if Array.length args1 < Array.length args2 then
- evar_define env ev2 (mkEvar ev1) isevars
- else
- evar_define env ev1 t2 isevars
- | _ ->
- evar_define env ev1 t2 isevars in
- let (isevars,pbs) = get_conv_pbs isevars (status_changed lsp) in
- List.fold_left
- (fun (isevars,b as p) (pbty,t1,t2) ->
- if b then conv_algo env isevars pbty t1 t2 else p) (isevars,true)
- pbs
+ try
+ let t2 = nf_evar (evars_of isevars) t2 in
+ let (isevars,lsp) = match kind_of_term t2 with
+ | Evar (n2,args2 as ev2) ->
+ if n1 = n2 then
+ solve_refl conv_algo env isevars n1 args1 args2
+ else
+ if Array.length args1 < Array.length args2 then
+ evar_define env ev2 (mkEvar ev1) isevars
+ else
+ evar_define env ev1 t2 isevars
+ | _ ->
+ evar_define env ev1 t2 isevars in
+ let (isevars,pbs) = get_conv_pbs isevars (status_changed lsp) in
+ List.fold_left
+ (fun (isevars,b as p) (pbty,t1,t2) ->
+ if b then conv_algo env isevars pbty t1 t2 else p) (isevars,true)
+ pbs
+ with e when precatchable_exception e ->
+ (isevars,false)
(* Operations on value/type constraints *)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 11965812d..4bcec5ef6 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -46,8 +46,6 @@ val new_evar_instance :
named_context -> evar_defs -> types -> ?src:loc * hole_kind -> constr list ->
evar_defs * constr
-val w_Declare : env -> evar -> types -> evar_defs -> evar_defs
-
(***********************************************************)
(* Instanciate evars *)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index d1d8d3817..4cf17fb77 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -221,7 +221,14 @@ let create_evar_defs sigma =
let evars_of d = d.evars
let evars_reset_evd evd d = {d with evars = evd}
let reset_evd (sigma,mmap) d = {d with evars = sigma; metas=mmap}
-let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs}
+let add_conv_pb pb d =
+(* let (pbty,c1,c2) = pb in
+ pperrnl
+ (Termops.print_constr c1 ++
+ (if pbty=Reduction.CUMUL then str " <="++ spc()
+ else str" =="++spc()) ++
+ Termops.print_constr c2);*)
+ {d with conv_pbs = pb::d.conv_pbs}
let evar_source ev d =
try List.assoc ev d.history
with Not_found -> (dummy_loc, InternalHole)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 098c3e095..6101396a4 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -989,7 +989,19 @@ let check_evars fail_evar env initial_sigma isevars c =
error_unsolvable_implicit loc env sigma k)
| _ -> iter_constr proc_rec c
in
- proc_rec c
+ proc_rec c(*;
+ let (_,pbs) = get_conv_pbs !isevars (fun _ -> true) in
+ if pbs <> [] then begin
+ pperrnl
+ (str"TYPING OF "++Termops.print_constr_env env c++fnl()++
+ prlist_with_sep fnl
+ (fun (pb,c1,c2) ->
+ Termops.print_constr c1 ++
+ (if pb=Reduction.CUMUL then str " <="++ spc()
+ else str" =="++spc()) ++
+ Termops.print_constr c2)
+ pbs ++ fnl())
+ end*)
(* TODO: comment faire remonter l'information si le typage a resolu des
variables du sigma original. il faudrait que la fonction de typage
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 2f3495702..dd2d781d5 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -18,6 +18,7 @@ open Pretype_errors
open Inductive
open Inductiveops
open Typeops
+open Evd
let meta_type env mv =
let ty =
@@ -31,44 +32,36 @@ let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
(* The typing machine without information, without universes but with
existential variables. *)
-let assumption_of_judgment env evd j =
- assumption_of_judgment env (j_nf_evar (Evd.evars_of evd) j)
-
-let type_judgment env evd j =
- type_judgment env (j_nf_evar (Evd.evars_of evd) j)
-
-let check_type env evd j ty =
- let sigma = Evd.evars_of evd in
- if not (is_conv_leq env sigma j.uj_type ty) then
- error_actual_type env (j_nf_evar sigma j) (nf_evar sigma ty)
-
+(* cstr must be in n.f. w.r.t. evars and execute returns a judgement
+ where both the term and type are in n.f. *)
let rec execute env evd cstr =
match kind_of_term cstr with
| Meta n ->
- { uj_val = cstr; uj_type = meta_type evd n }
+ { uj_val = cstr; uj_type = nf_evar (evars_of evd) (meta_type evd n) }
| Evar ev ->
let sigma = Evd.evars_of evd in
let ty = Evd.existential_type sigma ev in
- let jty = execute env evd ty in
- let jty = assumption_of_judgment env evd jty in
+ let jty = execute env evd (nf_evar (evars_of evd) ty) in
+ let jty = assumption_of_judgment env jty in
{ uj_val = cstr; uj_type = jty }
| Rel n ->
- judge_of_relative env n
+ j_nf_evar (evars_of evd) (judge_of_relative env n)
| Var id ->
- judge_of_variable env id
+ j_nf_evar (evars_of evd) (judge_of_variable env id)
| Const c ->
- make_judge cstr (constant_type env c)
+ make_judge cstr (nf_evar (evars_of evd) (constant_type env c))
| Ind ind ->
- make_judge cstr (type_of_inductive env ind)
+ make_judge cstr (nf_evar (evars_of evd) (type_of_inductive env ind))
| Construct cstruct ->
- make_judge cstr (type_of_constructor env cstruct)
-
+ make_judge cstr
+ (nf_evar (evars_of evd) (type_of_constructor env cstruct))
+
| Case (ci,p,c,lf) ->
let cj = execute env evd c in
let pj = execute env evd p in
@@ -102,23 +95,23 @@ let rec execute env evd cstr =
| Lambda (name,c1,c2) ->
let j = execute env evd c1 in
- let var = type_judgment env evd j in
+ let var = type_judgment env j in
let env1 = push_rel (name,None,var.utj_val) env in
let j' = execute env1 evd c2 in
judge_of_abstraction env1 name var j'
| Prod (name,c1,c2) ->
let j = execute env evd c1 in
- let varj = type_judgment env evd j in
+ let varj = type_judgment env j in
let env1 = push_rel (name,None,varj.utj_val) env in
let j' = execute env1 evd c2 in
- let varj' = type_judgment env1 evd j' in
+ let varj' = type_judgment env1 j' in
judge_of_product env name varj varj'
| LetIn (name,c1,c2,c3) ->
let j1 = execute env evd c1 in
let j2 = execute env evd c2 in
- let j2 = type_judgment env evd j2 in
+ let j2 = type_judgment env j2 in
let _ = judge_of_cast env j1 j2 in
let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in
let j3 = execute env1 evd c3 in
@@ -127,13 +120,13 @@ let rec execute env evd cstr =
| Cast (c,t) ->
let cj = execute env evd c in
let tj = execute env evd t in
- let tj = type_judgment env evd tj in
+ let tj = type_judgment env tj in
let j, _ = judge_of_cast env cj tj in
j
and execute_recdef env evd (names,lar,vdef) =
let larj = execute_array env evd lar in
- let lara = Array.map (assumption_of_judgment env evd) larj in
+ let lara = Array.map (assumption_of_judgment env) larj in
let env1 = push_rec_types (names,lara,vdef) env in
let vdefj = execute_array env1 evd vdef in
let vdefv = Array.map j_val vdefj in
@@ -153,19 +146,21 @@ and execute_list env evd = function
j::jr
let mcheck env evd c t =
- let j = execute env evd c in
- check_type env evd j t
+ let sigma = Evd.evars_of evd in
+ let j = execute env evd (nf_evar sigma c) in
+ if not (is_conv_leq env sigma j.uj_type t) then
+ error_actual_type env j (nf_evar sigma t)
(* Type of a constr *)
let mtype_of env evd c =
- let j = execute env evd c in
+ let j = execute env evd (nf_evar (evars_of evd) c) in
(* No normalization: it breaks Pattern! *)
(*nf_betaiota*) (body_of_type j.uj_type)
let msort_of env evd c =
- let j = execute env evd c in
- let a = type_judgment env evd j in
+ let j = execute env evd (nf_evar (evars_of evd) c) in
+ let a = type_judgment env j in
a.utj_type
let type_of env sigma c =
@@ -178,5 +173,5 @@ let check env sigma c =
(* The typed type of a judgment. *)
let mtype_of_type env evd constr =
- let j = execute env evd constr in
- assumption_of_judgment env evd j
+ let j = execute env evd (nf_evar (evars_of evd) constr) in
+ assumption_of_judgment env j
diff --git a/tactics/equality.ml b/tactics/equality.ml
index f5ccf4286..30a01d6a9 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -588,7 +588,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
let (a,p_i_minus_1) = match whd_beta_stack p_i with
| (_sigS,[a;p]) -> (a,p)
| _ -> anomaly "sig_clausal_form: should be a sigma type" in
- let ev = Evarutil.e_new_evar isevars env (new_Type ()) in
+ let ev = Evarutil.e_new_evar isevars env a in
let rty = beta_applist(p_i_minus_1,[ev]) in
let tuple_tail = sigrec_clausal_form (siglen-1) rty in
match
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 17:29:37 +0000