summaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml39
-rw-r--r--pretyping/classops.ml7
-rw-r--r--pretyping/clenv.ml45
-rw-r--r--pretyping/clenv.mli32
-rw-r--r--pretyping/coercion.ml144
-rw-r--r--pretyping/evarconv.ml152
-rw-r--r--pretyping/evarconv.mli4
-rw-r--r--pretyping/evarutil.ml140
-rw-r--r--pretyping/evarutil.mli10
-rw-r--r--pretyping/evd.ml43
-rw-r--r--pretyping/evd.mli6
-rw-r--r--pretyping/inductiveops.ml8
-rw-r--r--pretyping/inductiveops.mli4
-rw-r--r--pretyping/matching.ml4
-rw-r--r--pretyping/pretype_errors.ml6
-rw-r--r--pretyping/pretype_errors.mli5
-rw-r--r--pretyping/pretyping.ml69
-rw-r--r--pretyping/pretyping.mli3
-rw-r--r--pretyping/rawterm.ml4
-rw-r--r--pretyping/rawterm.mli13
-rw-r--r--pretyping/recordops.ml8
-rwxr-xr-xpretyping/recordops.mli4
-rw-r--r--pretyping/reductionops.ml31
-rw-r--r--pretyping/reductionops.mli10
-rw-r--r--pretyping/retyping.ml52
-rw-r--r--pretyping/retyping.mli5
-rw-r--r--pretyping/termops.ml15
-rw-r--r--pretyping/termops.mli10
-rw-r--r--pretyping/typing.ml21
-rw-r--r--pretyping/unification.ml183
-rw-r--r--pretyping/vnorm.ml271
-rw-r--r--pretyping/vnorm.mli18
32 files changed, 971 insertions, 395 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b0fe83a3..58dda021 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: cases.ml 8875 2006-05-29 19:59:11Z msozeau $ *)
+(* $Id: cases.ml 9215 2006-10-05 15:40:31Z herbelin $ *)
open Util
open Names
@@ -336,8 +336,8 @@ let inh_coerce_to_ind isevars env ty tyi =
un inductif cela doit être égal *)
let _ = e_cumul env isevars expected_typ ty in ()
-let unify_tomatch_with_patterns isevars env typ tm =
- match find_row_ind tm with
+let unify_tomatch_with_patterns isevars env loc typ pats =
+ match find_row_ind pats with
| None -> NotInd (None,typ)
| Some (_,(ind,_)) ->
inh_coerce_to_ind isevars env typ ind;
@@ -345,29 +345,26 @@ let unify_tomatch_with_patterns isevars env typ tm =
with Not_found -> NotInd (None,typ)
let find_tomatch_tycon isevars env loc = function
- (* Try first if some 'in I ...' is present and can be used as a constraint *)
- | Some (_,ind,_,_),_
- (* Otherwise try to get constraints from (the 1st) constructor in clauses *)
- | None, Some (_,(ind,_)) ->
- mk_tycon (inductive_template isevars env loc ind)
- | None, None ->
- empty_tycon
-
-let coerce_row typing_fun isevars env cstropt (tomatch,(_,indopt)) =
+ (* Try if some 'in I ...' is present and can be used as a constraint *)
+ | Some (_,ind,_,_) -> mk_tycon (inductive_template isevars env loc ind)
+ | None -> empty_tycon
+
+let coerce_row typing_fun isevars env pats (tomatch,(_,indopt)) =
let loc = Some (loc_of_rawconstr tomatch) in
- let tycon = find_tomatch_tycon isevars env loc (indopt,cstropt) in
+ let tycon = find_tomatch_tycon isevars env loc indopt in
let j = typing_fun tycon env tomatch in
let typ = nf_evar (Evd.evars_of !isevars) j.uj_type in
- let t =
+ let t =
try IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ)
- with Not_found -> NotInd (None,typ) in
+ with Not_found ->
+ unify_tomatch_with_patterns isevars env loc typ pats in
(j.uj_val,t)
let coerce_to_indtype typing_fun isevars env matx tomatchl =
let pats = List.map (fun r -> r.patterns) matx in
let matx' = match matrix_transpose pats with
- | [] -> List.map (fun _ -> None) tomatchl (* no patterns at all *)
- | m -> List.map find_row_ind m in
+ | [] -> List.map (fun _ -> []) tomatchl (* no patterns at all *)
+ | m -> m in
List.map2 (coerce_row typing_fun isevars env) matx' tomatchl
(************************************************************************)
@@ -500,12 +497,12 @@ let rec adjust_local_defs loc = function
| [], [] -> []
| _ -> raise NotAdjustable
-let check_and_adjust_constructor ind cstrs = function
+let check_and_adjust_constructor env ind cstrs = function
| PatVar _ as pat -> pat
| PatCstr (loc,((_,i) as cstr),args,alias) as pat ->
(* Check it is constructor of the right type *)
let ind' = inductive_of_constructor cstr in
- if ind' = ind then
+ if Closure.mind_equiv env ind' ind then
(* Check the constructor has the right number of args *)
let ci = cstrs.(i-1) in
let nb_args_constr = ci.cs_nargs in
@@ -1132,7 +1129,7 @@ let first_clause_irrefutable env = function
| eqn::mat -> List.for_all (irrefutable env) eqn.patterns
| _ -> false
-let group_equations pb mind current cstrs mat =
+let group_equations pb ind current cstrs mat =
let mat =
if first_clause_irrefutable pb.env mat then [List.hd mat] else mat in
let brs = Array.create (Array.length cstrs) [] in
@@ -1142,7 +1139,7 @@ let group_equations pb mind current cstrs mat =
(fun eqn () ->
let rest = remove_current_pattern eqn in
let pat = current_pattern eqn in
- match check_and_adjust_constructor mind cstrs pat with
+ match check_and_adjust_constructor pb.env ind cstrs pat with
| PatVar (_,name) ->
(* This is a default clause that we expand *)
for i=1 to Array.length cstrs do
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index b6cce031..bbad005c 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: classops.ml 8642 2006-03-17 10:09:02Z notin $ *)
+(* $Id: classops.ml 9257 2006-10-21 17:28:28Z herbelin $ *)
open Util
open Pp
@@ -154,7 +154,8 @@ let lookup_pattern_path_between (s,t) =
coe.coe_value
in
match kind_of_term c with
- | Construct sp -> (sp, coe.coe_param)
+ | Construct cstr ->
+ (cstr, Inductiveops.constructor_nrealargs (Global.env()) cstr -1)
| _ -> raise Not_found) l
(* find_class_type : constr -> cl_typ * int *)
@@ -207,7 +208,7 @@ let class_of env sigma t =
let inductive_class_of ind = fst (class_info (CL_IND ind))
-let class_args_of c = snd (decompose_app c)
+let class_args_of c = snd (find_class_type c)
let string_of_class = function
| CL_FUN -> "Funclass"
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 6113ec2d..abe31e06 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: clenv.ml 8752 2006-04-27 19:37:33Z herbelin $ *)
+(* $Id: clenv.ml 9279 2006-10-25 15:51:24Z herbelin $ *)
open Pp
open Util
@@ -74,6 +74,26 @@ let clenv_get_type_of ce c =
(meta_list ce.env) in
Retyping.get_type_of_with_meta (cl_env ce) (cl_sigma ce) metamap c
+exception NotExtensibleClause
+
+let clenv_push_prod cl =
+ let typ = whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_type cl) in
+ let rec clrec typ = match kind_of_term typ with
+ | Cast (t,_,_) -> clrec t
+ | Prod (na,t,u) ->
+ let mv = new_meta () in
+ let dep = dependent (mkRel 1) u in
+ let na' = if dep then na else Anonymous in
+ let e' = meta_declare mv t ~name:na' cl.env 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;
+ templtyp = mk_freelisted concl;
+ env = e';
+ templenv = cl.templenv }
+ | _ -> raise NotExtensibleClause
+ in clrec typ
+
let clenv_environments evd bound c =
let rec clrec (e,metas) n c =
match n, kind_of_term c with
@@ -258,7 +278,20 @@ let connect_clenv gls clenv =
* resolution can cause unification of already-existing metavars, and
* of the fresh ones which get created. This operation is a composite
* of operations which pose new metavars, perform unification on
- * terms, and make bindings. *)
+ * terms, and make bindings.
+
+ Otherwise said, from
+
+ [clenv] = [env;sigma;metas |- c:T]
+ [clenv'] = [env';sigma';metas' |- d:U]
+ [mv] = [mi] of type [Ti] in [metas]
+
+ then, if the unification of [Ti] and [U] produces map [rho], the
+ chaining is [env';sigma';rho'(metas),rho(metas') |- c:rho'(T)] for
+ [rho'] being [rho;mi:=d].
+
+ In particular, it assumes that [env'] and [sigma'] extend [env] and [sigma].
+*)
let clenv_fchain mv clenv nextclenv =
(* Add the metavars of [nextclenv] to [clenv], with their name-environment *)
let clenv' =
@@ -412,18 +445,18 @@ let clenv_constrain_missing_args mlist clause =
(****************************************************************)
(* Clausal environment for an application *)
-let make_clenv_binding_gen n gls (c,t) = function
+let make_clenv_binding_gen hyps_only n gls (c,t) = function
| ImplicitBindings largs ->
let clause = mk_clenv_from_n gls n (c,t) in
- clenv_constrain_dep_args (n <> None) clause largs
+ clenv_constrain_dep_args hyps_only clause largs
| ExplicitBindings lbind ->
let clause = mk_clenv_rename_from_n gls n (c,t) in
clenv_match_args lbind clause
| NoBindings ->
mk_clenv_from_n gls n (c,t)
-let make_clenv_binding_apply wc n = make_clenv_binding_gen (Some n) wc
-let make_clenv_binding = make_clenv_binding_gen None
+let make_clenv_binding_apply gls n = make_clenv_binding_gen true n gls
+let make_clenv_binding = make_clenv_binding_gen false None
(****************************************************************)
(* Pretty-print *)
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index f585dfea..b5433cac 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: clenv.mli 7659 2005-12-17 21:07:17Z herbelin $ i*)
+(*i $Id: clenv.mli 9277 2006-10-25 13:02:22Z herbelin $ i*)
(*i*)
open Util
@@ -17,6 +17,7 @@ open Environ
open Evd
open Evarutil
open Mod_subst
+open Rawterm
(*i*)
(***************************************************************)
@@ -93,24 +94,41 @@ val clenv_missing : clausenv -> metavariable list
(* defines metas corresponding to the name of the bindings *)
val clenv_match_args :
- constr Rawterm.explicit_bindings -> clausenv -> clausenv
+ constr explicit_bindings -> clausenv -> clausenv
val clenv_constrain_with_bindings : arg_bindings -> clausenv -> clausenv
(* start with a clenv to refine with a given term with bindings *)
-(* 1- the arity of the lemma is fixed *)
+(* the arity of the lemma is fixed *)
+(* the optional int tells how many prods of the lemma have to be used *)
+(* use all of them if None *)
val make_clenv_binding_apply :
- evar_info sigma -> int -> constr * constr -> constr Rawterm.bindings ->
+ evar_info sigma -> int option -> constr * constr -> constr bindings ->
clausenv
val make_clenv_binding :
- evar_info sigma -> constr * constr -> constr Rawterm.bindings -> clausenv
-
-(* other stuff *)
+ evar_info sigma -> constr * constr -> constr bindings -> clausenv
+
+(* [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] *)
val clenv_environments :
evar_defs -> int option -> types -> evar_defs * constr list * types
+
+(* [clenv_environments_evars env sigma n t] does the same but returns
+ a list of Evar's defined in [env] and extends [sigma] accordingly *)
val clenv_environments_evars :
env -> evar_defs -> int option -> types -> evar_defs * constr list * types
+(* if the clause is a product, add an extra meta for this product *)
+exception NotExtensibleClause
+val clenv_push_prod : clausenv -> clausenv
+
(***************************************************************)
(* Pretty-print *)
val pr_clenv : clausenv -> Pp.std_ppcmds
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index d0ee913f..cc74b0ad 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coercion.ml 8875 2006-05-29 19:59:11Z msozeau $ *)
+(* $Id: coercion.ml 9257 2006-10-21 17:28:28Z herbelin $ *)
open Util
open Names
@@ -20,6 +20,7 @@ open Evarutil
open Evarconv
open Retyping
open Evd
+open Termops
module type S = sig
(*s Coercions. *)
@@ -66,7 +67,14 @@ module Default = struct
(* Typing operations dealing with coercions *)
exception NoCoercion
- let class_of1 env sigma t = class_of env sigma (nf_evar sigma t)
+ let whd_app_evar sigma t =
+ match kind_of_term t with
+ | App (f,l) -> mkApp (whd_evar sigma f,l)
+ | _ -> whd_evar sigma t
+
+ let class_of1 env isevars t =
+ let sigma = evars_of isevars in
+ class_of env sigma (whd_app_evar sigma t)
(* Here, funj is a coercion therefore already typed in global context *)
let apply_coercion_args env argl funj =
@@ -84,7 +92,6 @@ module Default = struct
apply_rec [] funj.uj_type argl
(* appliquer le chemin de coercions de patterns p *)
-
let apply_pattern_coercion loc pat p =
List.fold_left
(fun pat (co,n) ->
@@ -100,7 +107,6 @@ module Default = struct
apply_pattern_coercion loc pat p
(* appliquer le chemin de coercions p à hj *)
-
let apply_coercion env p hj typ_cl =
try
fst (List.fold_left
@@ -120,22 +126,23 @@ module Default = struct
let t = whd_betadeltaiota env (evars_of isevars) j.uj_type in
match kind_of_term t with
| Prod (_,_,_) -> (isevars,j)
- | Evar ev when not (is_defined_evar isevars ev) ->
+ | Evar ev ->
let (isevars',t) = define_evar_as_arrow isevars ev in
(isevars',{ uj_val = j.uj_val; uj_type = t })
| _ ->
(try
- let t,i1 = class_of1 env (evars_of isevars) j.uj_type in
+ let t,i1 = class_of1 env isevars j.uj_type in
let p = lookup_path_to_fun_from i1 in
(isevars,apply_coercion env p j t)
with Not_found -> (isevars,j))
let inh_tosort_force loc env isevars j =
try
- let t,i1 = class_of1 env (evars_of isevars) j.uj_type in
+ let t,i1 = class_of1 env isevars j.uj_type in
let p = lookup_path_to_sort_from i1 in
let j1 = apply_coercion env p j t in
- (isevars,type_judgment env (j_nf_evar (evars_of isevars) j1))
+ let j2 = on_judgment_type (whd_evar (evars_of isevars)) j1 in
+ (isevars,type_judgment env j2)
with Not_found ->
error_not_a_type_loc loc env (evars_of isevars) j
@@ -154,8 +161,8 @@ module Default = struct
let inh_coerce_to_fail env isevars c1 v t =
let v', t' =
try
- let t1,i1 = class_of1 env (evars_of isevars) c1 in
- let t2,i2 = class_of1 env (evars_of isevars) t in
+ let t1,i1 = class_of1 env isevars c1 in
+ let t2,i2 = class_of1 env isevars t in
let p = lookup_path_between (i2,i1) in
match v with
Some v ->
@@ -166,64 +173,68 @@ module Default = struct
in
try (the_conv_x_leq env t' c1 isevars, v', t')
with Reduction.NotConvertible -> raise NoCoercion
- open Pp
+
let rec inh_conv_coerce_to_fail loc env isevars v t c1 =
try (the_conv_x_leq env t c1 isevars, v, t)
with Reduction.NotConvertible ->
- (try
- inh_coerce_to_fail env isevars c1 v t
- with NoCoercion ->
- (match kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
- kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with
- | Prod (_,t1,t2), Prod (name,u1,u2) ->
- let v' = option_map (whd_betadeltaiota env (evars_of isevars)) v in
- let (evd',b) =
- match v' with
- Some v' ->
- (match kind_of_term v' with
- | Lambda (x,v1,v2) ->
- (try the_conv_x env v1 u1 isevars, Some (x, v1, v2) (* leq v1 u1? *)
- with Reduction.NotConvertible -> (isevars, None))
- | _ -> (isevars, None))
- | None -> (isevars, None)
- in
- (match b with
- Some (x, v1, v2) ->
- let env1 = push_rel (x,None,v1) env in
- let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd'
- (Some v2) t2 u2 in
- (evd'', option_map (fun v2' -> mkLambda (x, v1, v2')) v2',
- mkProd (x, v1, t2'))
- | None ->
- (* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
- (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *)
- (* has type (name:u1)u2 (with v' recursively obtained) *)
- let name = (match name with
- | Anonymous -> Name (id_of_string "x")
- | _ -> name) in
- let env1 = push_rel (name,None,u1) env in
- let (evd', v1', t1') =
- inh_conv_coerce_to_fail loc env1 isevars
- (Some (mkRel 1)) (lift 1 u1) (lift 1 t1)
- in
- let (evd'', v2', t2') =
- let v2 =
- match v with
- Some v -> option_map (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1'
- | None -> None
- and evd', t2 =
- match v1' with
- Some v1' -> evd', subst1 v1' t2
- | None ->
- let evd', ev = new_evar evd' env ~src:(loc, InternalHole) t1' in
- evd', subst1 ev t2
- in
- inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2
- in
- (evd'', option_map (fun v2' -> mkLambda (name, u1, v2')) v2',
- mkProd (name, u1, t2')))
- | _ -> raise NoCoercion))
-
+ try inh_coerce_to_fail env isevars c1 v t
+ with NoCoercion ->
+ match
+ kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
+ kind_of_term (whd_betadeltaiota env (evars_of isevars) c1)
+ with
+ | Prod (_,t1,t2), Prod (name,u1,u2) ->
+ let v' = option_map (whd_betadeltaiota env (evars_of isevars)) v in
+ let (evd',b) =
+ match v' with
+ | Some v' ->
+ (match kind_of_term v' with
+ | Lambda (x,v1,v2) ->
+ (* sous-typage non contravariant: pas de "leq v1 u1" *)
+ (try the_conv_x env v1 u1 isevars, Some (x, v1, v2)
+ with Reduction.NotConvertible -> (isevars, None))
+ | _ -> (isevars, None))
+ | None -> (isevars, None)
+ in
+ (match b with
+ | Some (x, v1, v2) ->
+ let env1 = push_rel (x,None,v1) env in
+ let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd'
+ (Some v2) t2 u2 in
+ (evd'', option_map (fun v2' -> mkLambda (x, v1, v2')) v2',
+ mkProd (x, v1, t2'))
+ | None ->
+ (* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
+ (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *)
+ (* has type (name:u1)u2 (with v' recursively obtained) *)
+ let name = match name with
+ | Anonymous -> Name (id_of_string "x")
+ | _ -> name
+ in
+ let env1 = push_rel (name,None,u1) env in
+ let (evd', v1', t1') =
+ inh_conv_coerce_to_fail loc env1 isevars
+ (Some (mkRel 1)) (lift 1 u1) (lift 1 t1)
+ in
+ let (evd'', v2', t2') =
+ let v2 =
+ match v with
+ | Some v -> option_map (fun x -> mkApp(lift 1 v,[|x|])) v1'
+ | None -> None
+ and evd', t2 =
+ match v1' with
+ | Some v1' -> evd', subst_term v1' t2
+ | None ->
+ let evd', ev =
+ new_evar evd' env ~src:(loc, InternalHole) t1' in
+ evd', subst_term ev t2
+ in
+ inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2
+ in
+ (evd'', option_map (fun v2' -> mkLambda (name, u1, v2')) v2',
+ mkProd (name, u1, t2')))
+ | _ -> raise NoCoercion
+
(* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
let inh_conv_coerce_to loc env isevars cj (n, t) =
match n with
@@ -236,8 +247,7 @@ module Default = struct
error_actual_type_loc loc env sigma cj t
in
let val' = match val' with Some v -> v | None -> assert(false) in
- let nf = nf_isevar evd' in
- (evd',{ uj_val = nf val'; uj_type = nf t })
+ (evd',{ uj_val = val'; uj_type = t })
| Some (init, cur) -> (isevars, cj)
let inh_conv_coerces_to loc env (isevars : evar_defs) t (abs, t') = isevars
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 458f5bd3..3c4a23ec 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,14 +6,16 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: evarconv.ml 8793 2006-05-05 17:41:41Z barras $ *)
+(* $Id: evarconv.ml 9141 2006-09-15 10:07:01Z herbelin $ *)
+open Pp
open Util
open Names
open Term
open Closure
open Reduction
open Reductionops
+open Termops
open Environ
open Typing
open Classops
@@ -83,7 +85,7 @@ let evar_apprec env isevars stack c =
| Evar (n,_ as ev) when Evd.is_defined sigma n ->
aux (Evd.existential_value sigma ev, stack)
| _ -> (t, list_of_stack stack)
- in aux (c, append_stack (Array.of_list stack) empty_stack)
+ in aux (c, append_stack_list stack empty_stack)
let apprec_nohdbeta env isevars c =
let (t,stack as s) = Reductionops.whd_stack c in
@@ -126,7 +128,6 @@ let check_conv_record (t1,l1) (t2,l2) =
with _ ->
raise Not_found
-
(* Precondition: one of the terms of the pb is an uninstantiated evar,
* possibly applied to arguments. *)
@@ -190,12 +191,7 @@ let rec evar_conv_x env isevars pbty term1 term2 =
else
let (t1,l1) = apprec_nohdbeta env isevars term1 in
let (t2,l2) = apprec_nohdbeta env isevars term2 in
- if (head_is_embedded_evar isevars t1 & not(is_eliminator t2))
- or (head_is_embedded_evar isevars t2 & not(is_eliminator t1))
- then
- (add_conv_pb (pbty,applist(t1,l1),applist(t2,l2)) isevars, true)
- else
- evar_eqappr_x env isevars pbty (t1,l1) (t2,l2)
+ evar_eqappr_x env isevars pbty (t1,l1) (t2,l2)
and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
(* Evar must be undefined since we have whd_ised *)
@@ -229,7 +225,20 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
| Flexible ev1, MaybeFlexible flex2 ->
let f1 i =
- if List.length l1 <= List.length l2 then
+ if
+ is_unification_pattern_evar ev1 l1 &
+ not (occur_evar (fst ev1) (applist (term2,l2)))
+ then
+ (* Miller-Pfenning's patterns unification *)
+ (* Preserve generality (except that CCI has no eta-conversion) *)
+ let t2 = nf_evar (evars_of isevars) (applist(term2,l2)) in
+ let t2 = solve_pattern_eqn env l1 t2 in
+ solve_simple_eqn evar_conv_x env isevars (pbty,ev1,t2)
+ else if
+ List.length l1 <= List.length l2
+ then
+ (* Try first-order unification *)
+ (* (heuristic that gives acceptable results in practice) *)
let (deb2,rest2) =
list_chop (List.length l2-List.length l1) l2 in
ise_and i
@@ -248,7 +257,20 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
| MaybeFlexible flex1, Flexible ev2 ->
let f1 i =
- if List.length l2 <= List.length l1 then
+ if
+ is_unification_pattern_evar ev2 l2 &
+ not (occur_evar (fst ev2) (applist (term1,l1)))
+ then
+ (* Miller-Pfenning's patterns unification *)
+ (* Preserve generality (except that CCI has no eta-conversion) *)
+ let t1 = nf_evar (evars_of isevars) (applist(term1,l1)) in
+ let t1 = solve_pattern_eqn env l2 t1 in
+ solve_simple_eqn evar_conv_x env isevars (pbty,ev2,t1)
+ else if
+ List.length l2 <= List.length l1
+ then
+ (* Try first-order unification *)
+ (* (heuristic that gives acceptable results in practice) *)
let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
ise_and i
(* First compare extra args for better failure message *)
@@ -273,8 +295,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
(try conv_record env i
(try check_conv_record appr1 appr2
with Not_found -> check_conv_record appr2 appr1)
-(* TODO: remove this _ !!! *)
- with _ -> (i,false))
+ with Not_found -> (i,false))
and f4 i =
(* heuristic: unfold second argument first, exception made
if the first argument is a beta-redex (expand a constant
@@ -295,38 +316,39 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
ise_try isevars [f2; f3; f4]
| Flexible ev1, Rigid _ ->
- if (List.length l1 <= List.length l2) then
- let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
- ise_and isevars
- (* First compare extra args for better failure message *)
- [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) l1 rest2);
- (fun i ->
- (* Then instantiate evar unless already done by unifying args *)
- let t2 = applist(term2,deb2) in
- if is_defined_evar i ev1 then
- evar_conv_x env i pbty (mkEvar ev1) t2
- else
- solve_simple_eqn evar_conv_x env i (pbty,ev1,t2))]
- else (isevars,false)
+ if
+ is_unification_pattern_evar ev1 l1 &
+ not (occur_evar (fst ev1) (applist (term2,l2)))
+ then
+ (* Miller-Pfenning's patterns unification *)
+ (* Preserve generality (except that CCI has no eta-conversion) *)
+ let t2 = nf_evar (evars_of isevars) (applist(term2,l2)) in
+ let t2 = solve_pattern_eqn env l1 t2 in
+ solve_simple_eqn evar_conv_x env isevars (pbty,ev1,t2)
+ else
+ (* Postpone the use of an heuristic *)
+ add_conv_pb (pbty,applist(term1,l1),applist(term2,l2)) isevars,
+ true
+
| Rigid _, Flexible ev2 ->
- if List.length l2 <= List.length l1 then
- let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
- ise_and isevars
- (* First compare extra args for better failure message *)
- [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest1 l2);
- (fun i ->
- (* Then instantiate evar unless already done by unifying args *)
- let t1 = applist(term1,deb1) in
- if is_defined_evar i ev2 then
- evar_conv_x env i pbty t1 (mkEvar ev2)
- else
- solve_simple_eqn evar_conv_x env i (pbty,ev2,t1))]
- else (isevars,false)
+ if
+ is_unification_pattern_evar ev2 l2 &
+ not (occur_evar (fst ev2) (applist (term1,l1)))
+ then
+ (* Miller-Pfenning's patterns unification *)
+ (* Preserve generality (except that CCI has no eta-conversion) *)
+ let t1 = nf_evar (evars_of isevars) (applist(term1,l1)) in
+ let t1 = solve_pattern_eqn env l2 t1 in
+ solve_simple_eqn evar_conv_x env isevars (pbty,ev2,t1)
+ else
+ (* Postpone the use of an heuristic *)
+ add_conv_pb (pbty,applist(term1,l1),applist(term2,l2)) isevars,
+ true
| MaybeFlexible flex1, Rigid _ ->
let f3 i =
(try conv_record env i (check_conv_record appr1 appr2)
- with _ -> (i,false))
+ with Not_found -> (i,false))
and f4 i =
match eval_flexible_term env flex1 with
| Some v1 ->
@@ -337,8 +359,8 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
| Rigid _ , MaybeFlexible flex2 ->
let f3 i =
- (try (conv_record env i (check_conv_record appr2 appr1))
- with _ -> (i,false))
+ (try conv_record env i (check_conv_record appr2 appr1)
+ with Not_found -> (i,false))
and f4 i =
match eval_flexible_term env flex2 with
| Some v2 ->
@@ -468,7 +490,51 @@ and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) =
params1 params);
(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) ts ts1);
(fun i -> evar_conv_x env i CONV c1 (applist (c,(List.rev ks))))]
-
+
+let first_order_unification env isevars pbty (term1,l1) (term2,l2) =
+ match kind_of_term term1, kind_of_term term2 with
+ | Evar ev1,_ when List.length l1 <= List.length l2 ->
+ let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
+ ise_and isevars
+ (* First compare extra args for better failure message *)
+ [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest2 l1);
+ (fun i ->
+ (* Then instantiate evar unless already done by unifying args *)
+ let t2 = applist(term2,deb2) in
+ if is_defined_evar i ev1 then
+ evar_conv_x env i pbty t2 (mkEvar ev1)
+ else
+ solve_simple_eqn evar_conv_x env i (pbty,ev1,t2))]
+ | _,Evar ev2 when List.length l2 <= List.length l1 ->
+ let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
+ ise_and isevars
+ (* First compare extra args for better failure message *)
+ [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest1 l2);
+ (fun i ->
+ (* Then instantiate evar unless already done by unifying args *)
+ let t1 = applist(term1,deb1) in
+ if is_defined_evar i ev2 then
+ evar_conv_x env i pbty t1 (mkEvar ev2)
+ else
+ solve_simple_eqn evar_conv_x env i (pbty,ev2,t1))]
+ | _ ->
+ (* Some head evar have been instantiated *)
+ evar_conv_x env isevars pbty (applist(term1,l1)) (applist(term2,l2))
+
+let consider_remaining_unif_problems env isevars =
+ let (isevars,pbs) = get_conv_pbs isevars (fun _ -> true) in
+ List.fold_left
+ (fun (isevars,b as p) (pbty,t1,t2) ->
+ (* Pas le bon env pour le problème... *)
+ if b then first_order_unification env isevars pbty
+ (apprec_nohdbeta env isevars (whd_castappevar (evars_of isevars) t1))
+ (apprec_nohdbeta env isevars (whd_castappevar (evars_of isevars) t2))
+ else p)
+ (isevars,true)
+ pbs
+
+(* Main entry points *)
+
let the_conv_x env t1 t2 isevars =
match evar_conv_x env isevars CONV t1 t2 with
(evd',true) -> evd'
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index a6f5b489..f92a6fdb 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: evarconv.mli 6109 2004-09-15 16:50:56Z barras $ i*)
+(*i $Id: evarconv.mli 9141 2006-09-15 10:07:01Z herbelin $ i*)
(*i*)
open Term
@@ -33,3 +33,5 @@ val evar_eqappr_x :
conv_pb -> constr * constr list -> constr * constr list ->
evar_defs * bool
(*i*)
+
+val consider_remaining_unif_problems : env -> evar_defs -> evar_defs * bool
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 506cd03f..307c9886 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: evarutil.ml 8759 2006-04-28 12:24:14Z herbelin $ *)
+(* $Id: evarutil.ml 9154 2006-09-20 17:18:18Z corbinea $ *)
open Util
open Pp
@@ -21,13 +21,6 @@ open Evd
open Reductionops
open Pretype_errors
-
-let rec filter_unique = function
- | [] -> []
- | x::l ->
- if List.mem x l then filter_unique (List.filter (fun y -> x<>y) l)
- else x::filter_unique l
-
(* Expanding existential variables (pretyping.ml) *)
(* 1- whd_ise fails if an existential is undefined *)
@@ -63,9 +56,9 @@ let jv_nf_evar = Pretype_errors.jv_nf_evar
let tj_nf_evar = Pretype_errors.tj_nf_evar
let nf_evar_info evc info =
- { evar_concl = Reductionops.nf_evar evc info.evar_concl;
- evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps;
- evar_body = info.evar_body}
+ { info with
+ evar_concl = Reductionops.nf_evar evc info.evar_concl;
+ evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps}
let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
evm Evd.empty
@@ -310,29 +303,45 @@ let is_defined_equation env evd (ev,inst) rhs =
* ?3 <-- ?1 no pb: env of ?3 is larger than ?1's
* ?1 <-- (list ?2) pb: ?2 may depend on x, but not ?1.
* What we do is that ?2 is defined by a new evar ?4 whose context will be
- * a prefix of ?2's env, included in ?1's env. *)
+ * a prefix of ?2's env, included in ?1's env.
+
+ Concretely, the assumptions are "env |- ev : T" and "Gamma |-
+ ev[hyps:=args]" for some Gamma whose de Bruijn context has length k.
+ We create "env' |- ev' : T" for some env' <= env and define ev:=ev'
+*)
-let do_restrict_hyps evd ev args =
+let do_restrict_hyps env k evd ev args =
let args = Array.to_list args in
let evi = Evd.find (evars_of !evd) ev in
- let env = evar_env evi in
let hyps = evar_context evi in
- let (sign,ncargs) = list_filter2 (fun _ a -> closed0 a) (hyps,args) in
+ let (hyps',ncargs) = list_filter2 (fun _ a -> closedn k a) (hyps,args) in
(* No care is taken in case the evar type uses vars filtered out!
- Is it important ? *)
- let nc =
- let env =
- Sign.fold_named_context push_named sign ~init:(reset_context env) in
- e_new_evar evd env ~src:(evar_source ev !evd) evi.evar_concl in
+ Assuming that the restriction comes from a well-typed Flex/Flex
+ unification problem (see real_clean), the type of the evar cannot
+ depend on variables that are not in the scope of the other evar,
+ since this other evar has the same type (up to unification).
+ Since moreover, the evar contexts uses names only, the
+ restriction raise no de Bruijn reallocation problem *)
+ let env' =
+ Sign.fold_named_context push_named hyps' ~init:(reset_context env) in
+ let nc = e_new_evar evd env' ~src:(evar_source ev !evd) evi.evar_concl in
evd := Evd.evar_define ev nc !evd;
let (evn,_) = destEvar nc in
mkEvar(evn,Array.of_list ncargs)
-
-let need_restriction isevars args = not (array_for_all closed0 args)
+let need_restriction k args = not (array_for_all (closedn k) args)
(* We try to instantiate the evar assuming the body won't depend
- * on arguments that are not Rels or Vars, or appearing several times.
+ * on arguments that are not Rels or Vars, or appearing several times
+ (i.e. we tackle only Miller-Pfenning patterns unification)
+
+ 1) Let a unification problem "env |- ev[hyps:=args] = rhs"
+ 2) We limit it to a patterns unification problem "env |- ev[subst] = rhs"
+ where only Rel's and Var's are relevant in subst
+ 3) We recur on rhs, "imitating" the term failing if some Rel/Var not in scope
+
+ Note: we don't assume rhs in normal form, it may fail while it would
+ have succeeded after some reductions
*)
(* Note: error_not_clean should not be an error: it simply means that the
* conversion test that lead to the faulty call to [real_clean] should return
@@ -341,36 +350,52 @@ let need_restriction isevars args = not (array_for_all closed0 args)
let real_clean env isevars ev evi args rhs =
let evd = ref isevars in
- let subst = List.map (fun (x,y) -> (y,mkVar x)) (filter_unique args) in
+ let subst = List.map (fun (x,y) -> (y,mkVar x)) (list_uniquize args) 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 -> t)
+ else
+ (* Flex/Rel problem: unifiable as a pattern iff Rel in ev scope *)
+ (try List.assoc (mkRel (i-k)) subst
+ with Not_found -> if rigid then raise Exit 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
+ (* Flex/Flex problem: restriction to a common scope *)
let args' = Array.map (subs false k) args in
- if need_restriction !evd args' then
- do_restrict_hyps evd ev args'
+ if need_restriction k args' then
+ do_restrict_hyps (reset_context env) k evd ev args'
else
mkEvar (ev,args')
| Var id ->
+ (* Flex/Var problem: unifiable as a pattern iff Var in scope of ev *)
(try List.assoc t subst
with Not_found ->
if
not rigid
+ (* I don't understand this line: vars from evar_context evi
+ are private (especially some of them are freshly
+ generated in push_rel_context_to_named_context). They
+ have a priori nothing to do with the vars in env. I
+ remove the test [HH 25/8/06]
+
or List.exists (fun (id',_,_) -> id=id') (evar_context evi)
+ *)
then t
- else
- error_not_clean env (evars_of !evd) ev rhs
- (evar_source ev !evd))
- | _ -> map_constr_with_binders succ (subs rigid) k t
+ else raise Exit)
+
+ | _ ->
+ (* Flex/Rigid problem (or assimilated if not normal): we "imitate" *)
+ map_constr_with_binders succ (subs rigid) k t
in
- let body = subs true 0 (nf_evar (evars_of isevars) rhs) in
- if not (closed0 body)
- then error_not_clean env (evars_of !evd) ev body (evar_source ev !evd);
+ let rhs = nf_evar (evars_of isevars) rhs in
+ let rhs = whd_beta rhs (* heuristic *) in
+ let body =
+ try subs true 0 rhs
+ with Exit ->
+ error_not_clean env (evars_of !evd) ev rhs (evar_source ev !evd) in
(!evd,body)
(* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated
@@ -464,6 +489,34 @@ let head_evar =
in
hrec
+(* Check if an applied evar "?X[args] l" is a Miller's pattern; note
+ that we don't care whether args itself contains Rel's or even Rel's
+ distinct from the ones in l *)
+
+let is_unification_pattern_evar (_,args) l =
+ let l' = Array.to_list args @ l in
+ List.for_all (fun a -> isRel a or isVar a) l' & list_distinct l'
+
+let is_unification_pattern f l =
+ match kind_of_term f with
+ | Meta _ -> array_for_all isRel l & array_distinct l
+ | Evar ev -> is_unification_pattern_evar ev (Array.to_list l)
+ | _ -> false
+
+(* From a unification problem "?X l1 = term1 l2" such that l1 is made
+ of distinct rel's, build "\x1...xn.(term1 l2)" (patterns unification) *)
+
+let solve_pattern_eqn env l1 c =
+ let c' = List.fold_right (fun a c ->
+ let c' = subst_term (lift 1 a) (lift 1 c) in
+ match kind_of_term a with
+ (* Rem: if [a] links to a let-in, do as if it were an assumption *)
+ | Rel n -> let (na,_,t) = lookup_rel n env in mkLambda (na,lift n t,c')
+ | Var id -> let (id,_,t) = lookup_named id env in mkNamedLambda id t c'
+ | _ -> assert false)
+ l1 c in
+ whd_eta c'
+
(* This code (i.e. solve_pb, etc.) takes a unification
* problem, and tries to solve it. If it solves it, then it removes
* all the conversion problems, and re-runs conversion on each one, in
@@ -550,11 +603,28 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
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)
+ if b then conv_algo env isevars pbty t1 t2 else p) (isevars,true)
pbs
with e when precatchable_exception e ->
(isevars,false)
+
+(* [check_evars] fails if some unresolved evar remains *)
+(* it assumes that the defined existentials have already been substituted *)
+
+let check_evars env initial_sigma isevars c =
+ let sigma = evars_of isevars in
+ let c = nf_evar sigma c in
+ let rec proc_rec c =
+ match kind_of_term c with
+ | Evar (ev,args) ->
+ assert (Evd.mem sigma ev);
+ if not (Evd.mem initial_sigma ev) then
+ let (loc,k) = evar_source ev isevars in
+ error_unsolvable_implicit loc env sigma k
+ | _ -> iter_constr proc_rec c
+ in proc_rec c
+
(* Operations on value/type constraints *)
type type_constraint_type = (int * int) option * constr
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 7429cd16..3ac05481 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 8695 2006-04-10 16:33:52Z msozeau $ i*)
+(*i $Id: evarutil.mli 9141 2006-09-15 10:07:01Z herbelin $ i*)
(*i*)
open Util
@@ -78,10 +78,18 @@ val solve_simple_eqn :
-> env -> evar_defs -> conv_pb * existential * constr ->
evar_defs * bool
+(* [check_evars env initial_sigma extended_sigma c] fails if some
+ new unresolved evar remains in [c] *)
+val check_evars : env -> evar_map -> evar_defs -> constr -> unit
+
val define_evar_as_arrow : evar_defs -> existential -> evar_defs * types
val define_evar_as_lambda : evar_defs -> existential -> evar_defs * types
val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts
+val is_unification_pattern_evar : existential -> constr list -> bool
+val is_unification_pattern : constr -> constr array -> bool
+val solve_pattern_eqn : env -> constr list -> constr -> constr
+
(***********************************************************)
(* Value/Type constraints *)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 33f88ebd..030983e1 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: evd.ml 8759 2006-04-28 12:24:14Z herbelin $ *)
+(* $Id: evd.ml 9154 2006-09-20 17:18:18Z corbinea $ *)
open Pp
open Util
@@ -30,7 +30,8 @@ type evar_body =
type evar_info = {
evar_concl : constr;
evar_hyps : named_context_val;
- evar_body : evar_body}
+ evar_body : evar_body;
+ evar_extra : Dyn.t option}
let evar_context evi = named_context_of_val evi.evar_hyps
@@ -46,7 +47,11 @@ type evar_map1 = evar_info Evarmap.t
let empty = Evarmap.empty
-let to_list evc = Evarmap.fold (fun ev x acc -> (ev,x)::acc) evc []
+let to_list evc = (* Workaround for change in Map.fold behavior *)
+ let l = ref [] in
+ Evarmap.iter (fun ev x -> l:=(ev,x)::!l) evc;
+ !l
+
let dom evc = Evarmap.fold (fun ev _ acc -> ev::acc) evc []
let find evc k = Evarmap.find k evc
let remove evc k = Evarmap.remove k evc
@@ -60,9 +65,8 @@ let define evd ev body =
try find evd ev
with Not_found -> error "Evd.define: cannot define undeclared evar" in
let newinfo =
- { evar_concl = oldinfo.evar_concl;
- evar_hyps = oldinfo.evar_hyps;
- evar_body = Evar_defined body} in
+ { oldinfo with
+ evar_body = Evar_defined body } in
match oldinfo.evar_body with
| Evar_empty -> Evarmap.add ev newinfo evd
| _ -> anomaly "Evd.define: cannot define an isevar twice"
@@ -377,14 +381,7 @@ 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 =
-(* 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 add_conv_pb pb d = {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)
@@ -396,7 +393,10 @@ let evar_define sp body isevars =
let evar_declare hyps evn ty ?(src=(dummy_loc,InternalHole)) evd =
{ evd with
evars = add evd.evars evn
- {evar_hyps=hyps; evar_concl=ty; evar_body=Evar_empty};
+ {evar_hyps=hyps;
+ evar_concl=ty;
+ evar_body=Evar_empty;
+ evar_extra=None};
history = (evn,src)::evd.history }
let is_defined_evar isevars (n,_) = is_defined isevars.evars n
@@ -548,14 +548,21 @@ let pr_evar_map sigma =
h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi))
(to_list sigma))
+let pr_constraints pbs =
+ h 0
+ (prlist_with_sep pr_fnl (fun (pbty,t1,t2) ->
+ print_constr t1 ++ spc() ++
+ str (match pbty with
+ | Reduction.CONV -> "=="
+ | Reduction.CUMUL -> "<=") ++
+ spc() ++ print_constr t2) pbs)
+
let pr_evar_defs evd =
let pp_evm =
if evd.evars = empty then mt() else
str"EVARS:"++brk(0,1)++pr_evar_map evd.evars++fnl() in
- let n = List.length evd.conv_pbs in
let cstrs =
- if n=0 then mt() else
- str"=> " ++ int n ++ str" constraints" ++ fnl() ++ fnl() in
+ str"CONSTRAINTS:"++brk(0,1)++pr_constraints evd.conv_pbs++fnl() in
let pp_met =
if evd.metas = Metamap.empty then mt() else
str"METAS:"++brk(0,1)++pr_meta_map evd.metas in
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index cbc96b04..876c34d2 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: evd.mli 8759 2006-04-28 12:24:14Z herbelin $ i*)
+(*i $Id: evd.mli 9154 2006-09-20 17:18:18Z corbinea $ i*)
(*i*)
open Util
@@ -32,7 +32,8 @@ type evar_body =
type evar_info = {
evar_concl : constr;
evar_hyps : Environ.named_context_val;
- evar_body : evar_body}
+ evar_body : evar_body;
+ evar_extra : Dyn.t option}
val eq_evar_info : evar_info -> evar_info -> bool
val evar_context : evar_info -> named_context
@@ -94,6 +95,7 @@ type 'a freelisted = {
rebus : 'a;
freemetas : Metaset.t }
+val metavars_of : constr -> Metaset.t
val mk_freelisted : constr -> constr freelisted
val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index e0cdeeee..14136f61 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: inductiveops.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
+(* $Id: inductiveops.ml 9310 2006-10-28 19:35:09Z herbelin $ *)
open Util
open Names
@@ -23,7 +23,7 @@ open Reductionops
let type_of_inductive env ind =
let specif = Inductive.lookup_mind_specif env ind in
- Inductive.type_of_inductive specif
+ Inductive.type_of_inductive env specif
(* Return type as quoted by the user *)
let type_of_constructor env cstr =
@@ -126,6 +126,10 @@ let inductive_nargs env ind =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
mib.mind_nparams, mip.mind_nrealargs
+let allowed_sorts env (kn,i as ind) =
+ let (mib,mip) = Inductive.lookup_mind_specif env ind in
+ mip.mind_kelim
+
(* Annotation for cases *)
let make_case_info env ind style pats_source =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index dcd86716..d49b64d9 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: inductiveops.mli 8845 2006-05-23 07:41:58Z herbelin $ i*)
+(*i $Id: inductiveops.mli 9194 2006-10-01 09:25:19Z herbelin $ i*)
open Names
open Term
@@ -66,6 +66,8 @@ val constructor_nrealhyps : env -> constructor -> int
val get_full_arity_sign : env -> inductive -> rel_context
+val allowed_sorts : env -> inductive -> sorts_family list
+
(* Extract information from an inductive family *)
type constructor_summary = {
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 12c1ea33..65ce2ef4 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: matching.ml 8827 2006-05-17 15:15:34Z jforest $ *)
+(* $Id: matching.ml 9280 2006-10-25 21:37:37Z herbelin $ *)
(*i*)
open Util
@@ -119,6 +119,8 @@ let matches_core convert allow_partial_app pat c =
| PSort (RType _), Sort (Type _) -> sigma
+ | PApp (p, [||]), _ -> sorec stk sigma p t
+
| PApp (PApp (h, a1), a2), _ ->
sorec stk sigma (PApp(h,Array.append a1 a2)) t
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index f5a81659..59cdad04 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pretype_errors.ml 8752 2006-04-27 19:37:33Z herbelin $ *)
+(* $Id: pretype_errors.ml 9217 2006-10-05 17:31:23Z notin $ *)
open Util
open Stdpp
@@ -27,6 +27,7 @@ type pretype_error =
| NotClean of existential_key * constr * Evd.hole_kind
| UnsolvableImplicit of Evd.hole_kind
| CannotUnify of constr * constr
+ | CannotUnifyLocal of Environ.env * constr * constr * constr
| CannotUnifyBindingType of constr * constr
| CannotGeneralize of constr
| NoOccurrenceFound of constr
@@ -157,6 +158,9 @@ let error_unsolvable_implicit loc env sigma e =
let error_cannot_unify env sigma (m,n) =
raise (PretypeError (env_ise sigma env,CannotUnify (m,n)))
+let error_cannot_unify_local env sigma (e,m,n,sn) =
+ raise (PretypeError (env_ise sigma env,CannotUnifyLocal (e,m,n,sn)))
+
let error_cannot_coerce env sigma (m,n) =
raise (PretypeError (env_ise sigma env,CannotUnify (m,n)))
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 3c78d48d..137ef639 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pretype_errors.mli 8688 2006-04-07 15:08:12Z msozeau $ i*)
+(*i $Id: pretype_errors.mli 9217 2006-10-05 17:31:23Z notin $ i*)
(*i*)
open Pp
@@ -29,6 +29,7 @@ type pretype_error =
| NotClean of existential_key * constr * Evd.hole_kind
| UnsolvableImplicit of Evd.hole_kind
| CannotUnify of constr * constr
+ | CannotUnifyLocal of Environ.env * constr * constr * constr
| CannotUnifyBindingType of constr * constr
| CannotGeneralize of constr
| NoOccurrenceFound of constr
@@ -96,6 +97,8 @@ val error_unsolvable_implicit :
val error_cannot_unify : env -> Evd.evar_map -> constr * constr -> 'b
+val error_cannot_unify_local : env -> Evd.evar_map -> Environ.env * constr * constr * constr -> 'b
+
(*s Ml Case errors *)
val error_cant_find_case_type_loc :
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e3cfe974..0b00c82c 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pretyping.ml 8992 2006-06-27 21:29:18Z herbelin $ *)
+(* $Id: pretyping.ml 9338 2006-11-03 13:09:53Z herbelin $ *)
open Pp
open Util
@@ -245,6 +245,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let ccl' = mkLambda (Anonymous, ind, ccl) in
{uj_val=lam_it ccl' sign; uj_type=prod_it s' sign}
+ let evar_kind_of_term sigma c =
+ kind_of_term (whd_evar (Evd.evars_of sigma) c)
+
(*************************************************************************)
(* Main pretyping function *)
@@ -375,10 +378,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
| Prod (na,c1,c2) ->
let hj = pretype (mk_tycon c1) env isevars lvar c in
let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
- let typ' = nf_isevar !isevars typ in
apply_rec env (n+1)
- { uj_val = nf_isevar !isevars value;
- uj_type = typ' }
+ { uj_val = value;
+ uj_type = typ }
rest
| _ ->
let hj = pretype empty_tycon env isevars lvar c in
@@ -386,15 +388,18 @@ module Pretyping_F (Coercion : Coercion.S) = struct
(join_loc floc argloc) env (evars_of !isevars)
resj [hj]
in
- let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj args) in
+ let resj = apply_rec env 1 fj args in
let resj =
- match kind_of_term resj.uj_val with
- | App (f,args) when isInd f ->
- let sigma = evars_of !isevars in
- let t = Retyping.type_of_inductive_knowing_parameters env sigma (destInd f) args in
- let s = snd (splay_arity env sigma t) in
- on_judgment_type (set_inductive_level env s) resj
- (* Rem: no need to send sigma: no head evar, it's an arity *)
+ match evar_kind_of_term !isevars resj.uj_val with
+ | App (f,args) ->
+ let f = whd_evar (Evd.evars_of !isevars) f in
+ begin match kind_of_term f with
+ | Ind _ (* | Const _ *) ->
+ let sigma = evars_of !isevars in
+ let c = mkApp (f,Array.map (whd_evar sigma) args) in
+ let t = Retyping.get_type_of env sigma c in
+ make_judge c t
+ | _ -> resj end
| _ -> resj in
inh_conv_coerce_to_tycon loc env isevars resj tycon
@@ -455,7 +460,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
| Some p ->
let env_p = push_rels psign env in
let pj = pretype_type empty_valcon env_p isevars lvar p in
- let ccl = nf_evar (evars_of !isevars) pj.utj_val in
+ let ccl = nf_isevar !isevars pj.utj_val in
let psign = make_arity_signature env true indf in (* with names *)
let p = it_mkLambda_or_LetIn ccl psign in
let inst =
@@ -475,7 +480,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let tycon = lift_tycon cs.cs_nargs tycon in
let fj = pretype tycon env_f isevars lvar d in
let f = it_mkLambda_or_LetIn fj.uj_val fsign in
- let ccl = nf_evar (evars_of !isevars) fj.uj_type in
+ let ccl = nf_isevar !isevars fj.uj_type in
let ccl =
if noccur_between 1 cs.cs_nargs ccl then
lift (- cs.cs_nargs) ccl
@@ -632,35 +637,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct
(pretype_type empty_valcon env isevars lvar c).utj_val in
nf_evar (evars_of !isevars) c'
- (* [check_evars] fails if some unresolved evar remains *)
- (* it assumes that the defined existentials have already been substituted
- (should be done in unsafe_infer and unsafe_infer_type) *)
-
- let check_evars env initial_sigma isevars c =
- let sigma = evars_of !isevars in
- let rec proc_rec c =
- match kind_of_term c with
- | Evar (ev,args) ->
- assert (Evd.mem sigma ev);
- if not (Evd.mem initial_sigma ev) then
- let (loc,k) = evar_source ev !isevars in
- error_unsolvable_implicit loc env sigma k
- | _ -> iter_constr proc_rec c
- in
- 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
retourne aussi le nouveau sigma...
@@ -669,7 +645,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let understand_judgment sigma env c =
let isevars = ref (create_evar_defs sigma) in
let j = pretype empty_tycon env isevars ([],[]) c in
- let j = j_nf_evar (evars_of !isevars) j in
+ let isevars,_ = consider_remaining_unif_problems env !isevars in
+ let j = j_nf_evar (evars_of isevars) j in
check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
j
@@ -686,8 +663,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let ise_pretype_gen fail_evar sigma env lvar kind c =
let isevars = ref (Evd.create_evar_defs sigma) in
let c = pretype_gen isevars env lvar kind c in
+ let isevars,_ = consider_remaining_unif_problems env !isevars in
+ let c = nf_evar (evars_of isevars) c in
if fail_evar then check_evars env sigma isevars c;
- !isevars, c
+ isevars, c
(** Entry points of the high-level type synthesis algorithm *)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 7bb8c374..b1ed20c2 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pretyping.mli 8688 2006-04-07 15:08:12Z msozeau $ i*)
+(*i $Id: pretyping.mli 9141 2006-09-15 10:07:01Z herbelin $ i*)
(*i*)
open Names
@@ -78,7 +78,6 @@ sig
(* Idem but do not fail on unresolved evars *)
val understand_judgment_tcc : evar_defs ref -> env -> rawconstr -> unsafe_judgment
-
(*i*)
(* Internal of Pretyping...
*)
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index ece536d1..00dd034d 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: rawterm.ml 8969 2006-06-22 12:51:04Z msozeau $ *)
+(* $Id: rawterm.ml 9226 2006-10-09 16:11:01Z herbelin $ *)
(*i*)
open Util
@@ -26,7 +26,7 @@ type cases_pattern =
| PatVar of loc * name
| PatCstr of loc * constructor * cases_pattern list * name
-let pattern_loc = function
+let cases_pattern_loc = function
PatVar(loc,_) -> loc
| PatCstr(loc,_,_,_) -> loc
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 89b13ff0..6c2276d7 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: rawterm.mli 8969 2006-06-22 12:51:04Z msozeau $ i*)
+(*i $Id: rawterm.mli 9226 2006-10-09 16:11:01Z herbelin $ i*)
(*i*)
open Util
@@ -17,7 +17,8 @@ open Libnames
open Nametab
(*i*)
-(* Untyped intermediate terms, after ASTs and before constr. *)
+(**********************************************************************)
+(* The kind of patterns that occurs in "match ... with ... end" *)
(* locs here refers to the ident's location, not whole pat *)
(* the last argument of PatCstr is a possible alias ident for the pattern *)
@@ -25,7 +26,13 @@ type cases_pattern =
| PatVar of loc * name
| PatCstr of loc * constructor * cases_pattern list * name
-val pattern_loc : cases_pattern -> loc
+val cases_pattern_loc : cases_pattern -> loc
+
+(**********************************************************************)
+(* Untyped intermediate terms, after constr_expr and before constr *)
+(* Resolution of names, insertion of implicit arguments placeholder, *)
+(* and notations are done, but coercions, inference of implicit *)
+(* arguments and pattern-matching compilation are not *)
type patvar = identifier
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 74df5eea..5bbaa207 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: recordops.ml 9032 2006-07-07 16:30:34Z herbelin $ *)
+(* $Id: recordops.ml 9166 2006-09-23 11:20:06Z herbelin $ *)
open Util
open Pp
@@ -20,6 +20,7 @@ open Libobject
open Library
open Classops
open Mod_subst
+open Reductionops
(*s A structure S is a non recursive inductive type with a single
constructor (the name of which defaults to Build_S) *)
@@ -78,7 +79,7 @@ let (inStruc,outStruc) =
discharge_function = discharge_structure;
export_function = (function x -> Some x) }
-let declare_structure (s,c,_,kl,pl) =
+let declare_structure (s,c,kl,pl) =
Lib.add_anonymous_leaf (inStruc (s,c,kl,pl))
let lookup_structure indsp = Indmap.find indsp !structure_table
@@ -197,7 +198,8 @@ let check_and_decompose_canonical_structure ref =
let vc = match Environ.constant_opt_value env sp with
| Some vc -> vc
| None -> error_not_structure ref in
- let f,args = match kind_of_term (snd (decompose_lam vc)) with
+ let body = snd (splay_lambda (Global.env()) Evd.empty vc) in
+ let f,args = match kind_of_term body with
| App (f,args) -> f,args
| _ -> error_not_structure ref in
let indsp = match kind_of_term f with
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 91bc2ba1..0a05aef6 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: recordops.mli 9032 2006-07-07 16:30:34Z herbelin $ i*)
+(*i $Id: recordops.mli 9082 2006-08-24 17:03:28Z herbelin $ i*)
(*i*)
open Names
@@ -22,7 +22,7 @@ open Library
constructor (the name of which defaults to Build_S) *)
val declare_structure :
- inductive * identifier * int * bool list * constant option list -> unit
+ inductive * identifier * bool list * constant option list -> unit
(* [lookup_projections isp] returns the projections associated to the
inductive path [isp] if it corresponds to a structure, otherwise
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 82cc1b7d..19f515d0 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: reductionops.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
+(* $Id: reductionops.ml 9106 2006-09-01 11:18:17Z herbelin $ *)
open Pp
open Util
@@ -37,11 +37,12 @@ type 'a stack_member =
and 'a stack = 'a stack_member list
let empty_stack = []
-let append_stack_list = function
+let append_stack_list l s =
+ match (l,s) with
| ([],s) -> s
| (l1, Zapp l :: s) -> Zapp (l1@l) :: s
| (l1, s) -> Zapp l1 :: s
-let append_stack v s = append_stack_list (Array.to_list v, s)
+let append_stack v s = append_stack_list (Array.to_list v) s
(* Collapse the shifts in the stack *)
let zshift n s =
@@ -227,6 +228,7 @@ open RedFlags
(* Local *)
let beta = mkflags [fbeta]
+let eta = mkflags [feta]
let evar = mkflags [fevar]
let betaevar = mkflags [fevar; fbeta]
let betaiota = mkflags [fiota; fbeta]
@@ -251,7 +253,7 @@ let rec stacklam recfun env t stack =
| _ -> recfun (substl env t, stack)
let beta_applist (c,l) =
- stacklam app_stack [] c (append_stack (Array.of_list l) empty_stack)
+ stacklam app_stack [] c (append_stack_list l empty_stack)
(* Iota reduction tools *)
@@ -261,7 +263,7 @@ type 'a miota_args = {
mci : case_info; (* special info to re-build pattern *)
mcargs : 'a list; (* the constructor's arguments *)
mlf : 'a array } (* the branch code vector *)
-
+
let reducible_mind_case c = match kind_of_term c with
| Construct _ | CoFix _ -> true
| _ -> false
@@ -505,6 +507,10 @@ let whd_betadeltaiota_nolet_stack env sigma x =
let whd_betadeltaiota_nolet env sigma x =
app_stack (whd_betadeltaiota_nolet_state env sigma (x, empty_stack))
+(* 3. Eta reduction Functions *)
+
+let whd_eta c = app_stack (local_whd_state_gen eta (c,empty_stack))
+
(****************************************************************************)
(* Reduction Functions *)
(****************************************************************************)
@@ -641,7 +647,7 @@ let is_fconv = function | CONV -> is_conv | CUMUL -> is_conv_leq
let whd_meta metamap c = match kind_of_term c with
| Meta p -> (try List.assoc p metamap with Not_found -> c)
| _ -> c
-
+
(* Try to replace all metas. Does not replace metas in the metas' values
* Differs from (strong whd_meta). *)
let plain_instance s c =
@@ -668,7 +674,7 @@ let plain_instance s c =
| _ -> map_constr irec u
in
if s = [] then c else irec c
-
+
(* Pourquoi ne fait-on pas nf_betaiota si s=[] ? *)
let instance s c =
if s = [] then c else local_strong whd_betaiota (plain_instance s c)
@@ -746,7 +752,7 @@ let splay_arity env sigma c =
| _ -> error "not an arity"
let sort_of_arity env c = snd (splay_arity env Evd.empty c)
-
+
let decomp_n_prod env sigma n =
let rec decrec env m ln c = if m = 0 then (ln,c) else
match kind_of_term (whd_betadeltaiota env sigma c) with
@@ -764,7 +770,12 @@ let decomp_sort env sigma t =
| Sort s -> s
| _ -> raise NotASort
-(* One step of approximation *)
+let is_sort env sigma arity =
+ try let _ = decomp_sort env sigma arity in true
+ with NotASort -> false
+
+(* reduction to head-normal-form allowing delta/zeta only in argument
+ of case/fix (heuristic used by evar_conv) *)
let rec apprec env sigma s =
let (t, stack as s) = whd_betaiota_state s in
@@ -782,8 +793,6 @@ let rec apprec env sigma s =
| NotReducible -> s)
| _ -> s
-let hnf env sigma c = apprec env sigma (c, empty_stack)
-
(* A reduction function like whd_betaiota but which keeps casts
* and does not reduce redexes containing existential variables.
* Used in Correctness.
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 78afd22b..1e9b3b5b 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: reductionops.mli 8812 2006-05-13 11:46:02Z herbelin $ i*)
+(*i $Id: reductionops.mli 9106 2006-09-01 11:18:17Z herbelin $ i*)
(*i*)
open Names
@@ -37,6 +37,7 @@ and 'a stack = 'a stack_member list
val empty_stack : 'a stack
val append_stack : 'a array -> 'a stack -> 'a stack
+val append_stack_list : 'a list -> 'a stack -> 'a stack
val decomp_stack : 'a stack -> ('a * 'a stack) option
val list_of_stack : 'a stack -> 'a list
@@ -140,6 +141,7 @@ val whd_betadeltaiotaeta_stack : stack_reduction_function
val whd_betadeltaiotaeta_state : state_reduction_function
val whd_betadeltaiotaeta : reduction_function
+val whd_eta : constr -> constr
@@ -162,6 +164,7 @@ val decomp_n_prod :
val splay_prod_assum :
env -> evar_map -> constr -> Sign.rel_context * constr
val decomp_sort : env -> evar_map -> types -> sorts
+val is_sort : env -> evar_map -> types -> bool
type 'a miota_args = {
mP : constr; (* the result type *)
@@ -206,11 +209,8 @@ val whd_meta : (metavariable * constr) list -> constr -> constr
val plain_instance : (metavariable * constr) list -> constr -> constr
val instance : (metavariable * constr) list -> constr -> constr
-(*s Obsolete Reduction Functions *)
+(*s Heuristic for Conversion with Evar *)
-(*i
-val hnf : env -> 'a evar_map -> constr -> constr * constr list
-i*)
val apprec : state_reduction_function
(*s Meta-related reduction functions *)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 428a7306..ecead438 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: retyping.ml 8871 2006-05-28 16:46:48Z herbelin $ *)
+(* $Id: retyping.ml 9314 2006-10-29 20:11:08Z herbelin $ *)
open Util
open Term
@@ -17,6 +17,7 @@ open Reductionops
open Environ
open Typeops
open Declarations
+open Termops
let rec subst_type env sigma typ = function
| [] -> typ
@@ -38,6 +39,11 @@ let sort_of_atomic_type env sigma ft args =
| _ -> decomp_sort env sigma (subst_type env sigma ft (Array.to_list args))
in concl_of_arity env ft
+let type_of_var env id =
+ try let (_,_,ty) = lookup_named id env in ty
+ with Not_found ->
+ anomaly ("type_of: variable "^(string_of_id id)^" unbound")
+
let typeur sigma metamap =
let rec type_of env cstr=
match kind_of_term cstr with
@@ -47,18 +53,11 @@ let typeur sigma metamap =
| Rel n ->
let (_,_,ty) = lookup_rel n env in
lift n ty
- | Var id ->
- (try
- let (_,_,ty) = lookup_named id env in
- body_of_type ty
- with Not_found ->
- anomaly ("type_of: variable "^(string_of_id id)^" unbound"))
- | Const c ->
- let cb = lookup_constant c env in
- body_of_type cb.const_type
+ | Var id -> type_of_var env id
+ | Const cst -> Typeops.type_of_constant env cst
| Evar ev -> Evd.existential_type sigma ev
- | Ind ind -> body_of_type (type_of_inductive env ind)
- | Construct cstr -> body_of_type (type_of_constructor env cstr)
+ | Ind ind -> type_of_inductive env ind
+ | Construct cstr -> type_of_constructor env cstr
| Case (_,p,c,lf) ->
let Inductiveops.IndType(_,realargs) =
try Inductiveops.find_rectype env sigma (type_of env c)
@@ -73,8 +72,8 @@ let typeur sigma metamap =
subst1 b (type_of (push_rel (name,Some b,c1) env) c2)
| Fix ((_,i),(_,tys,_)) -> tys.(i)
| CoFix (i,(_,tys,_)) -> tys.(i)
- | App(f,args) when isInd f ->
- let t = type_of_inductive_knowing_parameters env (destInd f) args in
+ | App(f,args) when isGlobalRef f ->
+ let t = type_of_global_reference_knowing_parameters env f args in
strip_outer_cast (subst_type env sigma t (Array.to_list args))
| App(f,args) ->
strip_outer_cast
@@ -97,8 +96,8 @@ let typeur sigma metamap =
| Prop Pos, (Type u2) -> Type (Univ.sup Univ.base_univ u2)
| Prop Null, (Type _ as s) -> s
| Type u1, Type u2 -> Type (Univ.sup u1 u2))
- | App(f,args) when isInd f ->
- let t = type_of_inductive_knowing_parameters env (destInd f) args in
+ | App(f,args) when isGlobalRef f ->
+ let t = type_of_global_reference_knowing_parameters env f args in
sort_of_atomic_type env sigma t args
| App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
| Lambda _ | Fix _ | Construct _ ->
@@ -117,18 +116,27 @@ let typeur sigma metamap =
anomaly "sort_of: Not a type (1)"
| _ -> family_of_sort (decomp_sort env sigma (type_of env t))
- and type_of_inductive_knowing_parameters env ind args =
- let (_,mip) = lookup_mind_specif env ind in
+ and type_of_global_reference_knowing_parameters env c args =
let argtyps = Array.map (fun c -> nf_evar sigma (type_of env c)) args in
- Inductive.type_of_inductive_knowing_parameters env mip argtyps
+ match kind_of_term c with
+ | Ind ind ->
+ let (_,mip) = lookup_mind_specif env ind in
+ Inductive.type_of_inductive_knowing_parameters env mip argtyps
+ | Const cst ->
+ let t = constant_type env cst in
+ Typeops.type_of_constant_knowing_parameters env t argtyps
+ | Var id -> type_of_var env id
+ | Construct cstr -> type_of_constructor env cstr
+ | _ -> assert false
- in type_of, sort_of, sort_family_of, type_of_inductive_knowing_parameters
+ in type_of, sort_of, sort_family_of,
+ type_of_global_reference_knowing_parameters
let get_type_of env sigma c = let f,_,_,_ = typeur sigma [] in f env c
let get_sort_of env sigma t = let _,f,_,_ = typeur sigma [] in f env t
let get_sort_family_of env sigma c = let _,_,f,_ = typeur sigma [] in f env c
-let type_of_inductive_knowing_parameters env sigma ind args =
- let _,_,_,f = typeur sigma [] in f env ind args
+let type_of_global_reference_knowing_parameters env sigma c args =
+ let _,_,_,f = typeur sigma [] in f env c args
let get_type_of_with_meta env sigma metamap =
let f,_,_,_ = typeur sigma metamap in f env
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 923123c5..733cb4b1 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: retyping.mli 8871 2006-05-28 16:46:48Z herbelin $ i*)
+(*i $Id: retyping.mli 9314 2006-10-29 20:11:08Z herbelin $ i*)
(*i*)
open Names
@@ -34,5 +34,6 @@ val get_assumption_of : env -> evar_map -> constr -> types
(* Makes an unsafe judgment from a constr *)
val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment
-val type_of_inductive_knowing_parameters : env -> evar_map -> inductive ->
+val type_of_global_reference_knowing_parameters : env -> evar_map -> constr ->
constr array -> types
+
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 823da969..9b8764f2 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: termops.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
+(* $Id: termops.ml 9314 2006-10-29 20:11:08Z herbelin $ *)
open Pp
open Util
@@ -855,7 +855,12 @@ let next_global_ident_away allow_secvar id avoid =
else
next_global_ident_from allow_secvar (lift_ident id) avoid
-(* Nouvelle version de renommage des variables (DEC 98) *)
+let isGlobalRef c =
+ match kind_of_term c with
+ | Const _ | Ind _ | Construct _ | Var _ -> true
+ | _ -> false
+
+(* nouvelle version de renommage des variables (DEC 98) *)
(* This is the algorithm to display distinct bound variables
- Règle 1 : un nom non anonyme, même non affiché, contribue à la liste
@@ -1020,3 +1025,9 @@ let rec rename_bound_var env l c =
| Cast (c,k,t) -> mkCast (rename_bound_var env l c, k,t)
| x -> c
+(* Combinators on judgments *)
+
+let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type }
+let on_judgment_value f j = { j with uj_val = f j.uj_val }
+let on_judgment_type f j = { j with uj_type = f j.uj_type }
+
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 49de4838..e406b148 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 8845 2006-05-23 07:41:58Z herbelin $ i*)
+(*i $Id: termops.mli 9314 2006-10-29 20:11:08Z herbelin $ i*)
open Util
open Pp
@@ -203,3 +203,11 @@ val global_vars_set_of_decl : env -> named_declaration -> Idset.t
(* Test if an identifier is the basename of a global reference *)
val is_section_variable : identifier -> bool
+
+val isGlobalRef : constr -> bool
+
+(* Combinators on judgments *)
+
+val on_judgment : (types -> types) -> unsafe_judgment -> unsafe_judgment
+val on_judgment_value : (types -> types) -> unsafe_judgment -> unsafe_judgment
+val on_judgment_type : (types -> types) -> unsafe_judgment -> unsafe_judgment
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 78902a7d..63fdd6d5 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: typing.ml 8871 2006-05-28 16:46:48Z herbelin $ *)
+(* $Id: typing.ml 9310 2006-10-28 19:35:09Z herbelin $ *)
open Util
open Names
@@ -53,7 +53,7 @@ let rec execute env evd cstr =
j_nf_evar (evars_of evd) (judge_of_variable env id)
| Const c ->
- make_judge cstr (nf_evar (evars_of evd) (constant_type env c))
+ make_judge cstr (nf_evar (evars_of evd) (type_of_constant env c))
| Ind ind ->
make_judge cstr (nf_evar (evars_of evd) (type_of_inductive env ind))
@@ -90,12 +90,17 @@ let rec execute env evd cstr =
| App (f,args) ->
let jl = execute_array env evd args in
let j =
- if isInd f then
- (* Sort-polymorphism of inductive types *)
- judge_of_inductive_knowing_parameters env (destInd f)
- (jv_nf_evar (evars_of evd) jl)
- else
- execute env evd f
+ match kind_of_term f with
+ | Ind ind ->
+ (* Sort-polymorphism of inductive types *)
+ judge_of_inductive_knowing_parameters env ind
+ (jv_nf_evar (evars_of evd) jl)
+ | Const cst ->
+ (* Sort-polymorphism of inductive types *)
+ judge_of_constant_knowing_parameters env cst
+ (jv_nf_evar (evars_of evd) jl)
+ | _ ->
+ execute env evd f
in
fst (judge_of_apply env j jl)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e4bde925..fabe24ef 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: unification.ml 8759 2006-04-28 12:24:14Z herbelin $ *)
+(* $Id: unification.ml 9217 2006-10-05 17:31:23Z notin $ *)
open Pp
open Util
@@ -47,6 +47,16 @@ let abstract_list_all env sigma typ c l =
with UserError _ ->
raise (PretypeError (env,CannotGeneralize typ))
+(**)
+
+let solve_pattern_eqn_array env f l c (metasubst,evarsubst) =
+ match kind_of_term f with
+ | Meta k ->
+ (k,solve_pattern_eqn env (Array.to_list l) c)::metasubst,evarsubst
+ | Evar ev ->
+ (* Currently unused: incompatible with eauto/eassumption backtracking *)
+ metasubst,(f,solve_pattern_eqn env (Array.to_list l) c)::evarsubst
+ | _ -> assert false
(*******************************)
@@ -70,58 +80,77 @@ let sort_eqns = unify_r2l
let unify_0 env sigma cv_pb mod_delta m n =
let trivial_unify pb substn m n =
- if (not(occur_meta m)) && (if mod_delta then is_fconv pb env sigma m n else eq_constr m n) then substn
+ if (not(occur_meta m)) &&
+ (if mod_delta then is_fconv pb env sigma m n else eq_constr m n)
+ then substn
else error_cannot_unify env sigma (m,n) in
- let rec unirec_rec pb ((metasubst,evarsubst) as substn) m n =
- let cM = Evarutil.whd_castappevar sigma m
- and cN = Evarutil.whd_castappevar sigma n in
- match (kind_of_term cM,kind_of_term cN) with
- | Meta k1, Meta k2 ->
- if k1 < k2 then (k1,cN)::metasubst,evarsubst
- else if k1 = k2 then substn
- else (k2,cM)::metasubst,evarsubst
- | Meta k, _ -> (k,cN)::metasubst,evarsubst
- | _, Meta k -> (k,cM)::metasubst,evarsubst
- | Evar _, _ -> metasubst,((cM,cN)::evarsubst)
- | _, Evar _ -> metasubst,((cN,cM)::evarsubst)
-
- | Lambda (_,t1,c1), Lambda (_,t2,c2) ->
- unirec_rec CONV (unirec_rec CONV substn t1 t2) c1 c2
- | Prod (_,t1,c1), Prod (_,t2,c2) ->
- unirec_rec pb (unirec_rec CONV substn t1 t2) c1 c2
- | LetIn (_,b,_,c), _ -> unirec_rec pb substn (subst1 b c) cN
- | _, LetIn (_,b,_,c) -> unirec_rec pb substn cM (subst1 b c)
-
- | App (f1,l1), App (f2,l2) ->
- let len1 = Array.length l1
- and len2 = Array.length l2 in
- let (f1,l1,f2,l2) =
- if len1 = len2 then (f1,l1,f2,l2)
- else if len1 < len2 then
- let extras,restl2 = array_chop (len2-len1) l2 in
- (f1, l1, appvect (f2,extras), restl2)
- else
- let extras,restl1 = array_chop (len1-len2) l1 in
- (appvect (f1,extras), restl1, f2, l2) in
- (try
- array_fold_left2 (unirec_rec CONV)
- (unirec_rec CONV substn f1 f2) l1 l2
- with ex when precatchable_exception ex ->
- trivial_unify pb substn cM cN)
- | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
- array_fold_left2 (unirec_rec CONV)
- (unirec_rec CONV (unirec_rec CONV substn p1 p2) c1 c2) cl1 cl2
-
- | _ -> trivial_unify pb substn cM cN
-
+ let rec unirec_rec curenv pb ((metasubst,evarsubst) as substn) curm curn =
+ let cM = Evarutil.whd_castappevar sigma curm
+ and cN = Evarutil.whd_castappevar sigma curn in
+ match (kind_of_term cM,kind_of_term cN) with
+ | Meta k1, Meta k2 ->
+ if k1 < k2
+ then (k1,cN)::metasubst,evarsubst
+ else if k1 = k2 then substn else (k2,cM)::metasubst,evarsubst
+ | Meta k, _ ->
+ (* Here we check that [cN] does not contain any local variables *)
+ if (closedn (nb_rel env) cN)
+ then (k,cN)::metasubst,evarsubst
+ else error_cannot_unify_local curenv sigma (curenv,m,n,cN)
+ | _, Meta k ->
+ (* Here we check that [cM] does not contain any local variables *)
+ if (closedn (nb_rel env) cM)
+ then (k,cM)::metasubst,evarsubst
+ else error_cannot_unify_local curenv sigma (curenv,m,n,cM)
+ | Evar _, _ -> metasubst,((cM,cN)::evarsubst)
+ | _, Evar _ -> metasubst,((cN,cM)::evarsubst)
+ | Lambda (na,t1,c1), Lambda (_,t2,c2) ->
+ unirec_rec (push_rel_assum (na,t1) curenv) CONV
+ (unirec_rec curenv CONV substn t1 t2) c1 c2
+ | Prod (na,t1,c1), Prod (_,t2,c2) ->
+ unirec_rec (push_rel_assum (na,t1) curenv) pb
+ (unirec_rec curenv CONV substn t1 t2) c1 c2
+ | LetIn (_,b,_,c), _ -> unirec_rec curenv pb substn (subst1 b c) cN
+ | _, LetIn (_,b,_,c) -> unirec_rec curenv pb substn cM (subst1 b c)
+
+ | App (f1,l1), App (f2,l2) ->
+ if
+ isMeta f1 & is_unification_pattern f1 l1 & not (dependent f1 cN)
+ then
+ solve_pattern_eqn_array curenv f1 l1 cN substn
+ else if
+ isMeta f2 & is_unification_pattern f2 l2 & not (dependent f2 cM)
+ then
+ solve_pattern_eqn_array curenv f2 l2 cM substn
+ else
+ let len1 = Array.length l1
+ and len2 = Array.length l2 in
+ let (f1,l1,f2,l2) =
+ if len1 = len2 then (f1,l1,f2,l2)
+ else if len1 < len2 then
+ let extras,restl2 = array_chop (len2-len1) l2 in
+ (f1, l1, appvect (f2,extras), restl2)
+ else
+ let extras,restl1 = array_chop (len1-len2) l1 in
+ (appvect (f1,extras), restl1, f2, l2) in
+ (try
+ array_fold_left2 (unirec_rec curenv CONV)
+ (unirec_rec curenv CONV substn f1 f2) l1 l2
+ with ex when precatchable_exception ex ->
+ trivial_unify pb substn cM cN)
+ | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
+ array_fold_left2 (unirec_rec curenv CONV)
+ (unirec_rec curenv CONV
+ (unirec_rec curenv CONV substn p1 p2) c1 c2) cl1 cl2
+ | _ -> trivial_unify pb substn cM cN
in
- if (not(occur_meta m)) &&
- (if mod_delta then is_fconv cv_pb env sigma m n else eq_constr m n)
- then
- ([],[])
- else
- let (mc,ec) = unirec_rec cv_pb ([],[]) m n in
- ((*sort_eqns*) mc, (*sort_eqns*) ec)
+ if (not(occur_meta m)) &&
+ (if mod_delta then is_fconv cv_pb env sigma m n else eq_constr m n)
+ then
+ ([],[])
+ else
+ let (mc,ec) = unirec_rec env cv_pb ([],[]) m n in
+ ((*sort_eqns*) mc, (*sort_eqns*) ec)
(* Unification
@@ -442,30 +471,30 @@ let w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd =
let w_unify allow_K env cv_pb ?(mod_delta=true) ty1 ty2 evd =
let hd1,l1 = whd_stack ty1 in
let hd2,l2 = whd_stack ty2 in
- match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with
- (* Pattern case *)
- | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true)
- when List.length l1 = List.length l2 ->
- (try
- w_typed_unify env cv_pb mod_delta ty1 ty2 evd
- with ex when precatchable_exception ex ->
- try
- w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd
- with PretypeError (env,NoOccurrenceFound c) as e -> raise e
- | ex when precatchable_exception ex ->
- error "Cannot solve a second-order unification problem")
-
- (* Second order case *)
- | (Meta _, true, _, _ | _, _, Meta _, true) ->
- (try
- w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd
- with PretypeError (env,NoOccurrenceFound c) as e -> raise e
- | ex when precatchable_exception ex ->
- try
- w_typed_unify env cv_pb mod_delta ty1 ty2 evd
- with ex when precatchable_exception ex ->
- error "Cannot solve a second-order unification problem")
-
- (* General case: try first order *)
- | _ -> w_unify_0 env cv_pb mod_delta ty1 ty2 evd
+ match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with
+ (* Pattern case *)
+ | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true)
+ when List.length l1 = List.length l2 ->
+ (try
+ w_typed_unify env cv_pb mod_delta ty1 ty2 evd
+ with ex when precatchable_exception ex ->
+ try
+ w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd
+ with PretypeError (env,NoOccurrenceFound c) as e -> raise e
+ | ex when precatchable_exception ex ->
+ error "Cannot solve a second-order unification problem")
+
+ (* Second order case *)
+ | (Meta _, true, _, _ | _, _, Meta _, true) ->
+ (try
+ w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd
+ with PretypeError (env,NoOccurrenceFound c) as e -> raise e
+ | ex when precatchable_exception ex ->
+ try
+ w_typed_unify env cv_pb mod_delta ty1 ty2 evd
+ with ex when precatchable_exception ex ->
+ error "Cannot solve a second-order unification problem")
+
+ (* General case: try first order *)
+ | _ -> w_unify_0 env cv_pb mod_delta ty1 ty2 evd
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
new file mode 100644
index 00000000..55f798de
--- /dev/null
+++ b/pretyping/vnorm.ml
@@ -0,0 +1,271 @@
+open Names
+open Declarations
+open Term
+open Environ
+open Inductive
+open Reduction
+open Vm
+
+(*******************************************)
+(* Calcul de la forme normal d'un terme *)
+(*******************************************)
+
+let crazy_type = mkSet
+
+let decompose_prod env t =
+ let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in
+ if name = Anonymous then (Name (id_of_string "x"),dom,codom)
+ else res
+
+exception Find_at of int
+
+(* rend le numero du constructeur correspondant au tag [tag],
+ [cst] = true si c'est un constructeur constant *)
+
+let invert_tag cst tag reloc_tbl =
+ try
+ for j = 0 to Array.length reloc_tbl - 1 do
+ let tagj,arity = reloc_tbl.(j) in
+ if tag = tagj && (cst && arity = 0 || not(cst || arity = 0)) then
+ raise (Find_at j)
+ else ()
+ done;raise Not_found
+ with Find_at j -> (j+1)
+ (* Argggg, ces constructeurs de ... qui commencent a 1*)
+
+let find_rectype_a env c =
+ let (t, l) =
+ let t = whd_betadeltaiota env c in
+ try destApp t with _ -> (t,[||]) in
+ match kind_of_term t with
+ | Ind ind -> (ind, l)
+ | _ -> raise Not_found
+
+(* Instantiate inductives and parameters in constructor type *)
+let build_type_constructor mind mib params ctyp =
+ let si = ind_subst mind mib in
+ let ctyp1 = substl si ctyp in
+ let nparams = Array.length params in
+ if nparams = 0 then ctyp1
+ else
+ let _,ctyp2 = decompose_prod_n nparams ctyp1 in
+ let sp = List.rev (Array.to_list params) in substl sp ctyp2
+
+let construct_of_constr_const env tag typ =
+ let ind,params = find_rectype env typ in
+ let (_,mip) = lookup_mind_specif env ind in
+ let i = invert_tag true tag mip.mind_reloc_tbl in
+ applistc (mkConstruct(ind,i)) params
+
+let construct_of_constr_block env tag typ =
+ let (mind,_ as ind), allargs = find_rectype_a env typ in
+ let (mib,mip) = lookup_mind_specif env ind in
+ let nparams = mib.mind_nparams in
+ let i = invert_tag false tag mip.mind_reloc_tbl in
+ let params = Array.sub allargs 0 nparams in
+ let specif = mip.mind_nf_lc in
+ let ctyp = build_type_constructor mind mib params specif.(i-1) in
+ (mkApp(mkConstruct(ind,i), params), ctyp)
+
+let constr_type_of_idkey env idkey =
+ match idkey with
+ | ConstKey cst ->
+ mkConst cst, Typeops.type_of_constant env cst
+ | VarKey id ->
+ let (_,_,ty) = lookup_named id env in
+ mkVar id, ty
+ | RelKey i ->
+ let n = (nb_rel env - i) in
+ let (_,_,ty) = lookup_rel n env in
+ mkRel n, lift n ty
+
+let type_of_ind env ind =
+ type_of_inductive env (Inductive.lookup_mind_specif env ind)
+
+let build_branches_type env (mind,_ as _ind) mib mip params dep p =
+ let rtbl = mip.mind_reloc_tbl in
+ (* [build_one_branch i cty] construit le type de la ieme branche (commence
+ a 0) et les lambda correspondant aux realargs *)
+ let build_one_branch i cty =
+ let typi = build_type_constructor mind mib params cty in
+ let decl,indapp = Term.decompose_prod typi in
+ let ind,cargs = find_rectype_a env indapp in
+ let nparams = Array.length params in
+ let carity = snd (rtbl.(i)) in
+ let crealargs = Array.sub cargs nparams (Array.length cargs - nparams) in
+ let codom =
+ let papp = mkApp(p,crealargs) in
+ if dep then
+ let cstr = ith_constructor_of_inductive ind (i+1) in
+ let relargs = Array.init carity (fun i -> mkRel (carity-i)) in
+ let dep_cstr = mkApp(mkApp(mkConstruct cstr,params),relargs) in
+ mkApp(papp,[|dep_cstr|])
+ else papp
+ in
+ decl, codom
+ in Array.mapi build_one_branch mip.mind_nf_lc
+
+let build_case_type dep p realargs c =
+ if dep then mkApp(mkApp(p, realargs), [|c|])
+ else mkApp(p, realargs)
+
+(* La fonction de normalisation *)
+
+let rec nf_val env v t = nf_whd env (whd_val v) t
+
+and nf_vtype env v = nf_val env v crazy_type
+
+and nf_whd env whd typ =
+ match whd with
+ | Vsort s -> mkSort s
+ | Vprod p ->
+ let dom = nf_vtype env (dom p) in
+ let name = Name (id_of_string "x") in
+ let vc = body_of_vfun (nb_rel env) (codom p) in
+ let codom = nf_vtype (push_rel (name,None,dom) env) vc in
+ mkProd(name,dom,codom)
+ | Vfun f -> nf_fun env f typ
+ | Vfix(f,None) -> nf_fix env f
+ | Vfix(f,Some vargs) -> fst (nf_fix_app env f vargs)
+ | Vcofix(cf,_,None) -> nf_cofix env cf
+ | Vcofix(cf,_,Some vargs) ->
+ let cfd = nf_cofix env cf in
+ let i,(_,ta,_) = destCoFix cfd in
+ let t = ta.(i) in
+ let _, args = nf_args env vargs t in
+ mkApp(cfd,args)
+ | Vconstr_const n -> construct_of_constr_const env n typ
+ | Vconstr_block b ->
+ let capp,ctyp = construct_of_constr_block env (btag b) typ in
+ let args = nf_bargs env b ctyp in
+ mkApp(capp,args)
+ | Vatom_stk(Aid idkey, stk) ->
+ let c,typ = constr_type_of_idkey env idkey in
+ nf_stk env c typ stk
+ | Vatom_stk(Aiddef(idkey,v), stk) ->
+ nf_whd env (whd_stack v stk) typ
+ | Vatom_stk(Aind ind, stk) ->
+ nf_stk env (mkInd ind) (type_of_ind env ind) stk
+
+and nf_stk env c t stk =
+ match stk with
+ | [] -> c
+ | Zapp vargs :: stk ->
+ let t, args = nf_args env vargs t in
+ nf_stk env (mkApp(c,args)) t stk
+ | Zfix (f,vargs) :: stk ->
+ let fa, typ = nf_fix_app env f vargs in
+ let _,_,codom = decompose_prod env typ in
+ nf_stk env (mkApp(fa,[|c|])) (subst1 c codom) stk
+ | Zswitch sw :: stk ->
+ let (mind,_ as ind),allargs = find_rectype_a env t in
+ let (mib,mip) = Inductive.lookup_mind_specif env ind in
+ let nparams = mib.mind_nparams in
+ let params,realargs = Util.array_chop nparams allargs in
+ let pT =
+ hnf_prod_applist env (type_of_ind env ind) (Array.to_list params) in
+ let dep, p = nf_predicate env ind mip params (type_of_switch sw) pT in
+ (* Calcul du type des branches *)
+ let btypes = build_branches_type env ind mib mip params dep p in
+ (* calcul des branches *)
+ let bsw = branch_of_switch (nb_rel env) sw in
+ let mkbranch i (n,v) =
+ let decl,codom = btypes.(i) in
+ let env =
+ List.fold_right
+ (fun (name,t) env -> push_rel (name,None,t) env) decl env in
+ let b = nf_val env v codom in
+ compose_lam decl b
+ in
+ let branchs = Array.mapi mkbranch bsw in
+ let tcase = build_case_type dep p realargs c in
+ let ci = case_info sw in
+ nf_stk env (mkCase(ci, p, c, branchs)) tcase stk
+
+and nf_predicate env ind mip params v pT =
+ match whd_val v, kind_of_term pT with
+ | Vfun f, Prod _ ->
+ let k = nb_rel env in
+ let vb = body_of_vfun k f in
+ let name,dom,codom = decompose_prod env pT in
+ let dep,body =
+ nf_predicate (push_rel (name,None,dom) env) ind mip params vb codom in
+ dep, mkLambda(name,dom,body)
+ | Vfun f, _ ->
+ let k = nb_rel env in
+ let vb = body_of_vfun k f in
+ let name = Name (id_of_string "c") in
+ let n = mip.mind_nrealargs in
+ let rargs = Array.init n (fun i -> mkRel (n-i)) in
+ let dom = mkApp(mkApp(mkInd ind,params),rargs) in
+ let body = nf_vtype (push_rel (name,None,dom) env) vb in
+ true, mkLambda(name,dom,body)
+ | _, _ -> false, nf_val env v crazy_type
+
+and nf_args env vargs t =
+ let t = ref t in
+ let len = nargs vargs in
+ let args =
+ Array.init len
+ (fun i ->
+ let _,dom,codom = decompose_prod env !t in
+ let c = nf_val env (arg vargs i) dom in
+ t := subst1 c codom; c) in
+ !t,args
+
+and nf_bargs env b t =
+ let t = ref t in
+ let len = bsize b in
+ let args =
+ Array.init len
+ (fun i ->
+ let _,dom,codom = decompose_prod env !t in
+ let c = nf_val env (bfield b i) dom in
+ t := subst1 c codom; c) in
+ args
+
+and nf_fun env f typ =
+ let k = nb_rel env in
+ let vb = body_of_vfun k f in
+ let name,dom,codom = decompose_prod env typ in
+ let body = nf_val (push_rel (name,None,dom) env) vb codom in
+ mkLambda(name,dom,body)
+
+and nf_fix env f =
+ let init = current_fix f in
+ let rec_args = rec_args f in
+ let k = nb_rel env in
+ let vb, vt = reduce_fix k f in
+ let ndef = Array.length vt in
+ let ft = Array.map (fun v -> nf_val env v crazy_type) vt in
+ let name = Array.init ndef (fun _ -> (Name (id_of_string "Ffix"))) in
+ let env = push_rec_types (name,ft,ft) env in
+ let fb = Util.array_map2 (fun v t -> nf_fun env v t) vb ft in
+ mkFix ((rec_args,init),(name,ft,fb))
+
+and nf_fix_app env f vargs =
+ let fd = nf_fix env f in
+ let (_,i),(_,ta,_) = destFix fd in
+ let t = ta.(i) in
+ let t, args = nf_args env vargs t in
+ mkApp(fd,args),t
+
+and nf_cofix env cf =
+ let init = current_cofix cf in
+ let k = nb_rel env in
+ let vb,vt = reduce_cofix k cf in
+ let ndef = Array.length vt in
+ let cft = Array.map (fun v -> nf_val env v crazy_type) vt in
+ let name = Array.init ndef (fun _ -> (Name (id_of_string "Fcofix"))) in
+ let env = push_rec_types (name,cft,cft) env in
+ let cfb = Util.array_map2 (fun v t -> nf_val env v t) vb cft in
+ mkCoFix (init,(name,cft,cfb))
+
+let cbv_vm env c t =
+ let transp = transp_values () in
+ if not transp then set_transp_values true;
+ let v = Vconv.val_of_constr env c in
+ let c = nf_val env v t in
+ if not transp then set_transp_values false;
+ c
+
diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli
new file mode 100644
index 00000000..2ea94bfb
--- /dev/null
+++ b/pretyping/vnorm.mli
@@ -0,0 +1,18 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i*)
+open Names
+open Term
+open Environ
+open Reduction
+(*i*)
+
+(*s Reduction functions *)
+val cbv_vm : env -> constr -> types -> constr
+