summaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml29
-rw-r--r--pretyping/evarconv.ml10
-rw-r--r--pretyping/evarutil.ml49
-rw-r--r--pretyping/evarutil.mli12
-rw-r--r--pretyping/pretyping.ml10
-rw-r--r--pretyping/recordops.ml7
-rw-r--r--pretyping/termops.ml11
-rw-r--r--pretyping/termops.mli4
-rw-r--r--pretyping/typeclasses.ml4
-rw-r--r--pretyping/unification.ml6
10 files changed, 86 insertions, 56 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a4880f5e..c2d8921e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: cases.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: cases.ml 12167 2009-06-06 20:07:22Z herbelin $ *)
open Util
open Names
@@ -130,7 +130,7 @@ let push_rel_defs =
(* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize
over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *)
-let regeneralize_rel i k j = if j = i+k then k else if j < i+k then j else j
+let regeneralize_rel i k j = if j = i+k then k+1 else j
let rec regeneralize_index i k t = match kind_of_term t with
| Rel j when j = i+k -> mkRel (k+1)
@@ -605,19 +605,13 @@ let find_dependencies_signature deps_in_rhs typs =
let _,l = List.fold_right2 find_dependencies deps_in_rhs typs (k,[]) in
List.map (fun (_,deps,_) -> deps) l
-(******)
+(* Assume we had terms t1..tq to match in a context xp:Tp,...,x1:T1 |-
+ and xn:Tn has just been regeneralized into x:Tn so that the terms
+ to match are now to be considered in the context xp:Tp,...,x1:T1,x:Tn |-.
-(* A Pushed term to match has just been substituted by some
- constructor t = (ci x1...xn) and the terms x1 ... xn have been added to
- match
-
- - all terms to match and to push (dependent on t by definition)
- must have (Rel depth) substituted by t and Rel's>depth lifted by n
- - all pushed terms to match (non dependent on t by definition) must
- be lifted by n
-
- We start with depth=1
-*)
+ [regeneralize_index_tomatch n tomatch] updates t1..tq so that
+ former references to xn are now references to x. Note that t1..tq
+ are already adjusted to the context xp:Tp,...,x1:T1,x:Tn |-. *)
let regeneralize_index_tomatch n =
let rec genrec depth = function
@@ -661,6 +655,13 @@ let replace_tomatch n c =
let liftn_rel_declaration n k = map_rel_declaration (liftn n k)
let substnl_rel_declaration sigma k = map_rel_declaration (substnl sigma k)
+(* [liftn_tomatch_stack]: a term to match has just been substituted by
+ some constructor t = (ci x1...xn) and the terms x1 ... xn have been
+ added to match; all pushed terms to match must be lifted by n
+ (knowing that [Abstract] introduces a binder in the list of pushed
+ terms to match).
+*)
+
let rec liftn_tomatch_stack n depth = function
| [] -> []
| Pushed ((c,tm),l,dep)::rest ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 4c5ebe3e..043a326d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: evarconv.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: evarconv.ml 12205 2009-06-22 16:10:15Z barras $ *)
open Pp
open Util
@@ -474,11 +474,11 @@ and conv_record env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
let (evd',ks,_) =
List.fold_left
(fun (i,ks,m) b ->
- if m=0 then (i,t2::ks, n-1) else
+ if m=n then (i,t2::ks, m-1) else
let dloc = (dummy_loc,InternalHole) in
let (i',ev) = new_evar i env ~src:dloc (substl ks b) in
- (i', ev :: ks, n - 1))
- (evd,[],n) bs
+ (i', ev :: ks, m - 1))
+ (evd,[],List.length bs - 1) bs
in
ise_and evd'
[(fun i ->
@@ -505,7 +505,7 @@ let first_order_unification env evd (ev1,l1) (term2,l2) =
if is_defined_evar i ev1 then
evar_conv_x env i CONV t2 (mkEvar ev1)
else
- solve_simple_eqn evar_conv_x env i (CONV,ev1,t2))]
+ solve_simple_eqn ~choose:true evar_conv_x env i (CONV,ev1,t2))]
let choose_less_dependent_instance evk evd term args =
let evi = Evd.find (evars_of evd) evk in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index c0c0b941..994da427 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: evarutil.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: evarutil.ml 12107 2009-04-25 19:58:24Z herbelin $ *)
open Util
open Pp
@@ -673,7 +673,11 @@ let invert_arg_from_subst env k sigma subst_in_env c_in_env_extended_with_k_bind
let invert_arg env k sigma (evk,args_in_env) c_in_env_extended_with_k_binders =
let subst_in_env = make_projectable_subst sigma (Evd.find sigma evk) args_in_env in
- invert_arg_from_subst env k sigma subst_in_env c_in_env_extended_with_k_binders
+ let res = invert_arg_from_subst env k sigma subst_in_env c_in_env_extended_with_k_binders in
+ match res with
+ | Invertible (UniqueProjection (c,_)) when occur_evar evk c -> CannotInvert
+ | _ -> res
+
let effective_projections =
map_succeed (function Invertible c -> c | _ -> failwith"")
@@ -836,7 +840,7 @@ let expand_rhs env sigma subst rhs =
exception NotInvertibleUsingOurAlgorithm of constr
exception NotEnoughInformationToProgress
-let rec invert_definition env evd (evk,argsv as ev) rhs =
+let rec invert_definition choose env evd (evk,argsv as ev) rhs =
let evdref = ref evd in
let progress = ref false in
let evi = Evd.find (evars_of evd) evk in
@@ -847,7 +851,11 @@ let rec invert_definition env evd (evk,argsv as ev) rhs =
(* Evar/Var problem: unifiable iff variable projectable from ev subst *)
try
let sols = find_projectable_vars true env (evars_of !evdref) t subst in
- let c, p = filter_solution sols in
+ let c, p = match sols with
+ | [] -> raise Not_found
+ | [id,p] -> (mkVar id, p)
+ | (id,p)::_::_ -> if choose then (mkVar id, p) else raise NotUnique
+ in
let ty = lazy (Retyping.get_type_of env (evars_of !evdref) t) in
let evd = do_projection_effects evar_define env ty !evdref p in
evdref := evd;
@@ -923,9 +931,9 @@ and occur_existential evm c =
| _ -> iter_constr occrec c
in try occrec c; false with Occur -> true
-and evar_define env (evk,_ as ev) rhs evd =
+and evar_define ?(choose=false) env (evk,_ as ev) rhs evd =
try
- let (evd',body) = invert_definition env evd ev rhs in
+ let (evd',body) = invert_definition choose env evd ev rhs in
if occur_meta body then error "Meta cannot occur in evar body.";
(* invert_definition may have instantiate some evars of rhs with evk *)
(* so we recheck acyclicity *)
@@ -1120,7 +1128,7 @@ let solve_refl conv_algo env evd evk argsv1 argsv2 =
* if the problem couldn't be solved. *)
(* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
-let solve_simple_eqn conv_algo env evd (pbty,(evk1,args1 as ev1),t2) =
+let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) =
try
let t2 = whd_evar (evars_of evd) t2 in
let evd = match kind_of_term t2 with
@@ -1132,15 +1140,18 @@ let solve_simple_eqn conv_algo env evd (pbty,(evk1,args1 as ev1),t2) =
then solve_evar_evar evar_define env evd ev1 ev2
else add_conv_pb (pbty,env,mkEvar ev1,t2) evd
| _ ->
- let evd = evar_define env ev1 t2 evd in
+ let evd = evar_define ~choose env ev1 t2 evd in
let evm = evars_of evd in
let evi = Evd.find evm evk1 in
if occur_existential evm evi.evar_concl then
let evenv = evar_env evi in
let evc = nf_isevar evd evi.evar_concl in
- let body = match evi.evar_body with Evar_defined b -> b | Evar_empty -> assert false in
- let ty = nf_isevar evd (Retyping.get_type_of_with_meta evenv evm (metas_of evd) body) in
- add_conv_pb (Reduction.CUMUL,evenv,ty,evc) evd
+ match evi.evar_body with
+ | Evar_defined body ->
+ let ty = nf_isevar evd (Retyping.get_type_of_with_meta evenv evm (metas_of evd) body) in
+ add_conv_pb (Reduction.CUMUL,evenv,ty,evc) evd
+ | Evar_empty -> (* Resulted in a constraint *)
+ evd
else evd
in
let (evd,pbs) = extract_changed_conv_pbs evd status_changed in
@@ -1251,8 +1262,8 @@ let define_evar_as_abstraction abs evd (ev,args) =
let evrng =
fst (destEvar rng), array_cons (mkRel 1) (Array.map (lift 1) args) in
let prod' = abs (Name nvar, mkEvar evdom, mkEvar evrng) in
- (evd3,prod')
-
+ (evd3,prod')
+
let define_evar_as_product evd (ev,args) =
define_evar_as_abstraction (fun t -> mkProd t) evd (ev,args)
@@ -1263,7 +1274,6 @@ let define_evar_as_sort evd (ev,args) =
let s = new_Type () in
Evd.evar_define ev s evd, destSort s
-
(* We don't try to guess in which sort the type should be defined, since
any type has type Type. May cause some trouble, but not so far... *)
@@ -1275,27 +1285,26 @@ let judge_of_new_Type () = Typeops.judge_of_type (new_univ ())
an evar instantiate it with the product of 2 new evars. *)
let split_tycon loc env evd tycon =
- let rec real_split c =
- let sigma = evars_of evd in
- let t = whd_betadeltaiota env sigma c in
+ let rec real_split evd c =
+ let t = whd_betadeltaiota env (Evd.evars_of evd) c in
match kind_of_term t with
| Prod (na,dom,rng) -> evd, (na, dom, rng)
| Evar ev when not (Evd.is_defined_evar evd ev) ->
let (evd',prod) = define_evar_as_product evd ev in
let (_,dom,rng) = destProd prod in
evd',(Anonymous, dom, rng)
- | _ -> error_not_product_loc loc env sigma c
+ | _ -> error_not_product_loc loc env (Evd.evars_of evd) c
in
match tycon with
| None -> evd,(Anonymous,None,None)
| Some (abs, c) ->
(match abs with
None ->
- let evd', (n, dom, rng) = real_split c in
+ let evd', (n, dom, rng) = real_split evd c in
evd', (n, mk_tycon dom, mk_tycon rng)
| Some (init, cur) ->
if cur = 0 then
- let evd', (x, dom, rng) = real_split c in
+ let evd', (x, dom, rng) = real_split evd c in
evd, (Anonymous,
Some (None, dom),
Some (None, rng))
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index a687fdf0..cb54f400 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: evarutil.mli 11745 2009-01-04 18:43:08Z herbelin $ i*)
+(*i $Id: evarutil.mli 12053 2009-04-06 16:20:42Z msozeau $ i*)
(*i*)
open Util
@@ -53,11 +53,11 @@ val make_pure_subst : evar_info -> constr array -> (identifier * constr) list
(***********************************************************)
(* Instantiate evars *)
-(* [evar_define env ev c] try to instantiate [ev] with [c] (typed in [env]),
+(* [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]),
possibly solving related unification problems, possibly leaving open
- some problems that cannot be solved in a unique way;
- failed if the instance is not valid for the given [ev] *)
-val evar_define : env -> existential -> constr -> evar_defs -> evar_defs
+ some problems that cannot be solved in a unique way (except if choose is
+ true); fails if the instance is not valid for the given [ev] *)
+val evar_define : ?choose:bool -> env -> existential -> constr -> evar_defs -> evar_defs
(***********************************************************)
(* Evars/Metas switching... *)
@@ -80,7 +80,7 @@ val solve_refl :
evar_defs
val solve_simple_eqn :
(env -> evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool)
- -> env -> evar_defs -> conv_pb * existential * constr ->
+ -> ?choose:bool -> env -> evar_defs -> conv_pb * existential * constr ->
evar_defs * bool
(* [check_evars env initial_sigma extended_sigma c] fails if some
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1cac9011..c0f820a2 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pretyping.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
+(* $Id: pretyping.ml 12053 2009-04-06 16:20:42Z msozeau $ *)
open Pp
open Util
@@ -443,7 +443,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct
inh_conv_coerce_to_tycon loc env evdref resj tycon
| RLetIn(loc,name,c1,c2) ->
- let j = pretype empty_tycon env evdref lvar c1 in
+ let j =
+ match c1 with
+ | RCast (loc, c, CastConv (DEFAULTcast, t)) ->
+ let tj = pretype_type empty_valcon env evdref lvar t in
+ pretype (mk_tycon tj.utj_val) env evdref lvar c
+ | _ -> pretype empty_tycon env evdref lvar c1
+ in
let t = refresh_universes j.uj_type in
let var = (name,Some j.uj_val,t) in
let tycon = lift_tycon 1 tycon in
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 7c4023b9..711f332e 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: recordops.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
+(* $Id: recordops.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
open Util
open Pp
@@ -65,8 +65,11 @@ let subst_structure (_,subst,((kn,i),id,kl,projs as obj)) =
if projs' == projs && kn' == kn && id' == id then obj else
((kn',i),id',kl,projs')
+let discharge_constructor (ind, n) =
+ (Lib.discharge_inductive ind, n)
+
let discharge_structure (_,(ind,id,kl,projs)) =
- Some (Lib.discharge_inductive ind, id, kl,
+ Some (Lib.discharge_inductive ind, discharge_constructor id, kl,
List.map (Option.map Lib.discharge_con) projs)
let (inStruc,outStruc) =
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index f93212f8..4f38fbb3 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: termops.ml 11639 2008-11-27 17:48:32Z barras $ *)
+(* $Id: termops.ml 12058 2009-04-08 10:54:59Z herbelin $ *)
open Pp
open Util
@@ -1017,6 +1017,15 @@ let assums_of_rel_context sign =
| None -> (na, t)::l)
sign ~init:[]
+let fold_map_rel_context f env sign =
+ let rec aux env acc = function
+ | d::sign ->
+ aux (push_rel d env) (map_rel_declaration (f env) d :: acc) sign
+ | [] ->
+ acc
+ in
+ aux env [] (List.rev sign)
+
let map_rel_context_with_binders f sign =
let rec aux k = function
| d::sign -> map_rel_declaration (f k) d :: aux (k-1) sign
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index d44c762e..e0bbe7b5 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: termops.mli 11639 2008-11-27 17:48:32Z barras $ i*)
+(*i $Id: termops.mli 12058 2009-04-08 10:54:59Z herbelin $ i*)
open Util
open Pp
@@ -241,6 +241,8 @@ val process_rel_context : (rel_declaration -> env -> env) -> env -> env
val assums_of_rel_context : rel_context -> (name * constr) list
val lift_rel_context : int -> rel_context -> rel_context
val substl_rel_context : constr list -> rel_context -> rel_context
+val fold_map_rel_context :
+ (env -> constr -> constr) -> env -> rel_context -> rel_context
val map_rel_context_with_binders :
(int -> constr -> constr) -> rel_context -> rel_context
val fold_named_context_both_sides :
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 8680e578..216a0611 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: typeclasses.ml 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id: typeclasses.ml 12189 2009-06-15 05:08:44Z msozeau $ i*)
(*i*)
open Names
@@ -381,7 +381,7 @@ let solve_instanciation_problem = ref (fun _ _ _ -> assert false)
let resolve_typeclasses ?(onlyargs=false) ?(split=true) ?(fail=true) env evd =
if not (has_typeclasses (Evd.evars_of evd)) then evd
else
- !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) onlyargs split fail
+ !solve_instanciations_problem env evd onlyargs split fail
let resolve_one_typeclass env evm t =
!solve_instanciation_problem env evm t
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index fb29196c..bfd601e2 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: unification.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: unification.ml 12163 2009-06-06 17:36:47Z herbelin $ *)
open Pp
open Util
@@ -492,7 +492,7 @@ let w_coerce env evd mv c =
let unify_to_type env evd flags c u =
let sigma = evars_of evd in
let c = refresh_universes c in
- let t = get_type_of_with_meta env sigma (metas_of evd) c in
+ let t = get_type_of_with_meta env sigma (List.map (on_snd (nf_meta evd)) (metas_of evd)) (nf_meta evd c) in
let t = Tacred.hnf_constr env sigma (nf_betaiota sigma (nf_meta evd t)) in
let u = Tacred.hnf_constr env sigma u in
try unify_0 env sigma Cumul flags t u
@@ -500,7 +500,7 @@ let unify_to_type env evd flags c u =
let unify_type env evd flags mv c =
let mvty = Typing.meta_type evd mv in
- if occur_meta_or_existential mvty then
+ if occur_meta_or_existential mvty or is_arity env (evars_of evd) mvty then
unify_to_type env evd flags c mvty
else ([],[])
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-06 10:54:08 +0000