summaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
commitcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch)
treeb7832bd5d412a5a5d69cb36ae2ded62c71124c22 /pretyping
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml9
-rw-r--r--pretyping/evarconv.ml25
-rw-r--r--pretyping/evarutil.ml170
-rw-r--r--pretyping/evarutil.mli13
-rw-r--r--pretyping/evd.ml9
-rw-r--r--pretyping/evd.mli10
-rw-r--r--pretyping/indrec.ml15
-rw-r--r--pretyping/indrec.mli5
-rw-r--r--pretyping/inductiveops.ml54
-rw-r--r--pretyping/inductiveops.mli7
-rw-r--r--pretyping/matching.ml268
-rw-r--r--pretyping/matching.mli42
-rw-r--r--pretyping/pretyping.ml39
-rw-r--r--pretyping/rawterm.ml4
-rw-r--r--pretyping/recordops.ml19
-rwxr-xr-xpretyping/recordops.mli13
-rw-r--r--pretyping/reductionops.ml40
-rw-r--r--pretyping/retyping.ml28
-rw-r--r--pretyping/retyping.mli4
-rw-r--r--pretyping/tacred.ml155
-rw-r--r--pretyping/termops.ml43
-rw-r--r--pretyping/termops.mli16
-rw-r--r--pretyping/typeclasses.ml109
-rw-r--r--pretyping/typeclasses.mli22
-rw-r--r--pretyping/unification.ml189
-rw-r--r--pretyping/vnorm.ml19
26 files changed, 905 insertions, 422 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 9482bf92..52b73535 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: cases.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: cases.ml 11708 2008-12-20 10:50:20Z msozeau $ *)
open Util
open Names
@@ -150,8 +150,11 @@ let mkSpecialLetInJudge j (na,(deppat,nondeppat,d,t)) =
then
(* The body of pat is not needed to type j - see *)
(* insert_aliases - and both deppat and nondeppat have the *)
- (* same type, then one can freely substitute one by the other *)
- subst1 nondeppat j.uj_val
+ (* same type, then one can freely substitute one by the other. *)
+ (* We use nondeppat only if it's a Rel to preserve sharing. *)
+ if isRel nondeppat then
+ subst1 nondeppat j.uj_val
+ else subst1 deppat j.uj_val
else
(* The body of pat is not needed to type j but its value *)
(* is dependent in the type of j; our choice is to *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 323cd06f..58369811 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: evarconv.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: evarconv.ml 11745 2009-01-04 18:43:08Z herbelin $ *)
open Pp
open Util
@@ -164,10 +164,9 @@ let rec evar_conv_x env evd pbty term1 term2 =
(* Maybe convertible but since reducing can erase evars which [evar_apprec]
could have found, we do it only if the terms are free of evar.
Note: incomplete heuristic... *)
- if is_ground_term evd term1 && is_ground_term evd term2 &
- is_fconv pbty env (evars_of evd) term1 term2
- then
- (evd,true)
+ if is_ground_term evd term1 && is_ground_term evd term2
+ && is_ground_env evd env
+ then (evd, is_fconv pbty env (evars_of evd) term1 term2)
else
let term1 = apprec_nohdbeta env evd term1 in
let term2 = apprec_nohdbeta env evd term2 in
@@ -211,7 +210,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
| Flexible ev1, MaybeFlexible flex2 ->
let f1 i =
if
- is_unification_pattern_evar env ev1 l1 &
+ is_unification_pattern_evar env ev1 l1 (applist appr2) &
not (occur_evar (fst ev1) (applist appr2))
then
(* Miller-Pfenning's patterns unification *)
@@ -243,7 +242,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
| MaybeFlexible flex1, Flexible ev2 ->
let f1 i =
if
- is_unification_pattern_evar env ev2 l2 &
+ is_unification_pattern_evar env ev2 l2 (applist appr1) &
not (occur_evar (fst ev2) (applist appr1))
then
(* Miller-Pfenning's patterns unification *)
@@ -311,7 +310,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
| Flexible ev1, Rigid _ ->
if
- is_unification_pattern_evar env ev1 l1 &
+ is_unification_pattern_evar env ev1 l1 (applist appr2) &
not (occur_evar (fst ev1) (applist appr2))
then
(* Miller-Pfenning's patterns unification *)
@@ -326,7 +325,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
| Rigid _, Flexible ev2 ->
if
- is_unification_pattern_evar env ev2 l2 &
+ is_unification_pattern_evar env ev2 l2 (applist appr1) &
not (occur_evar (fst ev2) (applist appr1))
then
(* Miller-Pfenning's patterns unification *)
@@ -514,15 +513,15 @@ let apply_conversion_problem_heuristic env evd pbty t1 t2 =
let (term1,l1 as appr1) = decompose_app t1 in
let (term2,l2 as appr2) = decompose_app t2 in
match kind_of_term term1, kind_of_term term2 with
- | Evar (evk1,args1), (Rel _|Var _) when l1 = [] & l2 = [] ->
+ | Evar (evk1,args1), (Rel _|Var _) when l1 = [] & l2 = []
+ & array_for_all (fun a -> a = term2 or isEvar a) args1 ->
(* The typical kind of constraint coming from pattern-matching return
type inference *)
- assert (array_for_all (fun a -> a = term2 or isEvar a) args1);
choose_less_dependent_instance evk1 evd term2 args1, true
- | (Rel _|Var _), Evar (evk2,args2) when l1 = [] & l2 = [] ->
+ | (Rel _|Var _), Evar (evk2,args2) when l1 = [] & l2 = []
+ & array_for_all (fun a -> a = term1 or isEvar a) args2 ->
(* The typical kind of constraint coming from pattern-matching return
type inference *)
- assert (array_for_all ((=) term1) args2);
choose_less_dependent_instance evk2 evd term1 args2, true
| Evar ev1,_ when List.length l1 <= List.length l2 ->
(* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 130e23b8..b418f996 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: evarutil.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: evarutil.ml 11819 2009-01-20 20:04:50Z herbelin $ *)
open Util
open Pp
@@ -258,13 +258,19 @@ let e_new_evar evdref env ?(src=(dummy_loc,InternalHole)) ?filter ty =
* operations on the evar constraints *
*------------------------------------*)
+let is_pattern inst =
+ array_for_all (fun a -> isRel a || isVar a) inst &&
+ array_distinct inst
+
(* Pb: defined Rels and Vars should not be considered as a pattern... *)
+(*
let is_pattern inst =
let rec is_hopat l = function
[] -> true
| t :: tl ->
(isRel t or isVar t) && not (List.mem t l) && is_hopat (t::l) tl in
is_hopat [] (Array.to_list inst)
+*)
let evar_well_typed_body evd ev evi body =
try
@@ -431,7 +437,7 @@ let rec check_and_clear_in_constr evdref err ids c =
has dependencies in another hyp of the context of ev
and transitively remember the dependency *)
match List.filter (fun (id,_) -> occur_var_in_decl (Global.env()) id h) ri with
- | rid' :: _ -> (hy,ar,(rid,List.assoc rid ri)::ri)
+ | (_,id') :: _ -> (hy,ar,(rid,id')::ri)
| _ ->
(* No dependency at all, we can keep this ev's context hyp *)
(h::hy,a::ar,ri))
@@ -484,24 +490,42 @@ let clear_hyps_in_evi evdref hyps concl ids =
dependencies in variables are canonically associated to the most ancient
variable in its family of aliased variables *)
-let rec expand_var env x = match kind_of_term x with
+let expand_var_once env x = match kind_of_term x with
| Rel n ->
- begin try match pi2 (lookup_rel n env) with
- | Some t when isRel t -> expand_var env (lift n t)
- | _ -> x
- with Not_found -> x
+ begin match pi2 (lookup_rel n env) with
+ | Some t when isRel t or isVar t -> lift n t
+ | _ -> raise Not_found
end
| Var id ->
begin match pi2 (lookup_named id env) with
- | Some t when isVar t -> expand_var env t
- | _ -> x
+ | Some t when isVar t -> t
+ | _ -> raise Not_found
end
- | _ -> x
+ | _ ->
+ raise Not_found
+
+let rec expand_var_at_least_once env x =
+ let t = expand_var_once env x in
+ try expand_var_at_least_once env t
+ with Not_found -> t
+
+let expand_var env x =
+ try expand_var_at_least_once env x with Not_found -> x
+
+let expand_var_opt env x =
+ try Some (expand_var_at_least_once env x) with Not_found -> None
let rec expand_vars_in_term env t = match kind_of_term t with
| Rel _ | Var _ -> expand_var env t
| _ -> map_constr_with_full_binders push_rel expand_vars_in_term env t
+let rec expansions_of_var env x =
+ try
+ let t = expand_var_once env x in
+ t :: expansions_of_var env t
+ with Not_found ->
+ [x]
+
(* [find_projectable_vars env sigma y subst] finds all vars of [subst]
* that project on [y]. It is able to find solutions to the following
* two kinds of problems:
@@ -540,16 +564,16 @@ type evar_projection =
| ProjectVar
| ProjectEvar of existential * evar_info * identifier * evar_projection
-let rec find_projectable_vars env sigma y subst =
+let rec find_projectable_vars with_evars env sigma y subst =
let is_projectable (id,(idc,y')) =
let y' = whd_evar sigma y' in
if y = y' or expand_var env y = expand_var env y'
then (idc,(y'=y,(id,ProjectVar)))
- else if isEvar y' then
+ else if with_evars & isEvar y' then
let (evk,argsv as t) = destEvar y' in
let evi = Evd.find sigma evk in
let subst = make_projectable_subst sigma evi argsv in
- let l = find_projectable_vars env sigma y subst in
+ let l = find_projectable_vars with_evars env sigma y subst in
match l with
| [id',p] -> (idc,(true,(id,ProjectEvar (t,evi,id',p))))
| _ -> failwith ""
@@ -568,7 +592,7 @@ let filter_solution = function
| [id,p] -> (mkVar id, p)
let project_with_effects env sigma effects t subst =
- let c, p = filter_solution (find_projectable_vars env sigma t subst) in
+ let c, p = filter_solution (find_projectable_vars false env sigma t subst) in
effects := p :: !effects;
c
@@ -690,8 +714,8 @@ let do_restrict_hyps_virtual evd evk filter =
unsolvable.
Computing whether y is erasable or not may be costly and the
interest for this early detection in practice is not obvious. We let
- it for future work. Anyway, thanks to the use of filters, the whole
- context remains consistent. *)
+ it for future work. In any case, thanks to the use of filters, the whole
+ (unrestricted) context remains consistent. *)
let evi = Evd.find (evars_of evd) evk in
let env = evar_unfiltered_env evi in
let oldfilter = evar_filter evi in
@@ -822,7 +846,7 @@ let rec invert_definition env evd (evk,argsv as ev) rhs =
let project_variable t =
(* Evar/Var problem: unifiable iff variable projectable from ev subst *)
try
- let sols = find_projectable_vars env (evars_of !evdref) t subst in
+ let sols = find_projectable_vars true env (evars_of !evdref) t subst in
let c, p = filter_solution sols 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
@@ -833,7 +857,9 @@ let rec invert_definition env evd (evk,argsv as ev) rhs =
| NotUnique ->
if not !progress then raise NotEnoughInformationToProgress;
(* No unique projection but still restrict to where it is possible *)
- let filter = array_map_to_list (fun c -> isEvar c or c = t) argsv in
+ let ts = expansions_of_var env t in
+ let test c = isEvar c or List.mem c ts in
+ let filter = array_map_to_list test argsv in
let args' = filter_along (fun x -> x) filter argsv in
let evd,evar = do_restrict_hyps_virtual !evdref evk filter in
let evk',_ = destEvar evar in
@@ -891,6 +917,12 @@ let rec invert_definition env evd (evk,argsv as ev) rhs =
* context "hyps" and not referring to itself.
*)
+and occur_existential evm c =
+ let rec occrec c = match kind_of_term c with
+ | Evar (e, _) -> if not (is_defined evm e) then raise Occur
+ | _ -> iter_constr occrec c
+ in try occrec c; false with Occur -> true
+
and evar_define env (evk,_ as ev) rhs evd =
try
let (evd',body) = invert_definition env evd ev rhs in
@@ -934,6 +966,13 @@ let has_undefined_evars evd t =
let is_ground_term evd t =
not (has_undefined_evars evd t)
+let is_ground_env evd env =
+ let is_ground_decl = function
+ (_,Some b,_) -> is_ground_term evd b
+ | _ -> true in
+ List.for_all is_ground_decl (rel_context env) &&
+ List.for_all is_ground_decl (named_context env)
+
let head_evar =
let rec hrec c = match kind_of_term c with
| Evar (evk,_) -> evk
@@ -948,16 +987,50 @@ let head_evar =
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 env (_,args) l =
- let l' = Array.to_list args @ l in
- let l' = List.map (expand_var env) l' in
- List.for_all (fun a -> isRel a or isVar a) l' & list_distinct l'
-
-let is_unification_pattern env f l =
+let rec expand_and_check_vars env = function
+ | [] -> []
+ | a::l ->
+ if isRel a or isVar a then
+ let l = expand_and_check_vars env l in
+ match expand_var_opt env a with
+ | None -> a :: l
+ | Some a' when isRel a' or isVar a' -> list_add_set a' l
+ | _ -> raise Exit
+ else
+ raise Exit
+
+let is_unification_pattern_evar env (_,args) l t =
+ List.for_all (fun x -> isRel x || isVar x) l (* common failure case *)
+ &&
+ let l' = Array.to_list args @ l in
+ let l'' = try Some (expand_and_check_vars env l') with Exit -> None in
+ match l'' with
+ | Some l ->
+ let deps =
+ if occur_meta_or_existential t then
+ (* Probably no restrictions on allowed vars in presence of evars *)
+ l
+ else
+ (* Probably strong restrictions coming from t being evar-closed *)
+ let fv_rels = free_rels t in
+ let fv_ids = global_vars env t in
+ List.filter (fun c ->
+ match kind_of_term c with
+ | Var id -> List.mem id fv_ids
+ | Rel n -> Intset.mem n fv_rels
+ | _ -> assert false) l in
+ list_distinct deps
+ | None -> false
+
+let is_unification_pattern (env,nb) f l t =
match kind_of_term f with
- | Meta _ -> array_for_all isRel l & array_distinct l
- | Evar ev -> is_unification_pattern_evar env ev (Array.to_list l)
- | _ -> false
+ | Meta _ ->
+ array_for_all (fun c -> isRel c && destRel c <= nb) l
+ && array_distinct l
+ | Evar ev ->
+ is_unification_pattern_evar env ev (Array.to_list l) t
+ | _ ->
+ 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) *)
@@ -1045,16 +1118,47 @@ 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
| _ ->
- evar_define env ev1 t2 evd in
+ let evd = evar_define 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
+ else evd
+ in
let (evd,pbs) = extract_changed_conv_pbs evd status_changed in
- List.fold_left
- (fun (evd,b as p) (pbty,env,t1,t2) ->
- if b then conv_algo env evd pbty t1 t2 else p) (evd,true)
- pbs
+ List.fold_left
+ (fun (evd,b as p) (pbty,env,t1,t2) ->
+ if b then conv_algo env evd pbty t1 t2 else p) (evd,true)
+ pbs
with e when precatchable_exception e ->
(evd,false)
-
+let evars_of_term c =
+ let rec evrec acc c =
+ match kind_of_term c with
+ | Evar (n, _) -> Intset.add n acc
+ | _ -> fold_constr evrec acc c
+ in
+ evrec Intset.empty c
+
+let evars_of_named_context nc =
+ List.fold_right (fun (_, b, t) s ->
+ Option.fold_left (fun s t ->
+ Intset.union s (evars_of_term t))
+ s b) nc Intset.empty
+
+let evars_of_evar_info evi =
+ Intset.union (evars_of_term evi.evar_concl)
+ (Intset.union
+ (match evi.evar_body with
+ | Evar_empty -> Intset.empty
+ | Evar_defined b -> evars_of_term b)
+ (evars_of_named_context (named_context_of_val evi.evar_hyps)))
+
(* [check_evars] fails if some unresolved evar remains *)
(* it assumes that the defined existentials have already been substituted *)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index ca446c01..a687fdf0 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 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: evarutil.mli 11745 2009-01-04 18:43:08Z herbelin $ i*)
(*i*)
open Util
@@ -73,6 +73,7 @@ val non_instantiated : evar_map -> (evar * evar_info) list
(* Unification utils *)
val is_ground_term : evar_defs -> constr -> bool
+val is_ground_env : evar_defs -> env -> bool
val solve_refl :
(env -> evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool)
-> env -> evar_defs -> existential_key -> constr array -> constr array ->
@@ -90,10 +91,16 @@ val define_evar_as_product : 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 : env -> existential -> constr list -> bool
-val is_unification_pattern : env -> constr -> constr array -> bool
+val is_unification_pattern_evar : env -> existential -> constr list ->
+ constr -> bool
+val is_unification_pattern : env * int -> constr -> constr array ->
+ constr -> bool
val solve_pattern_eqn : env -> constr list -> constr -> constr
+val evars_of_term : constr -> Intset.t
+val evars_of_named_context : named_context -> Intset.t
+val evars_of_evar_info : evar_info -> Intset.t
+
(***********************************************************)
(* Value/Type constraints *)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index bf3cd623..af070d7e 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: evd.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: evd.ml 11865 2009-01-28 17:34:30Z herbelin $ *)
open Pp
open Util
@@ -300,6 +300,9 @@ let is_defined (sigma,_) = is_defined sigma
let existential_value (sigma,_) = existential_value sigma
let existential_type (sigma,_) = existential_type sigma
let existential_opt_value (sigma,_) = existential_opt_value sigma
+let eq_evar_map x y = x == y ||
+ (Evarmap.equal eq_evar_info (fst x) (fst y) &&
+ UniverseMap.equal (=) (snd x) (snd y))
let merge e e' = fold (fun n v sigma -> add sigma n v) e' e
@@ -400,10 +403,12 @@ let metamap_to_list m =
(*************************)
(* Unification state *)
+type obligation_definition_status = Define of bool | Expand
+
type hole_kind =
| ImplicitArg of global_reference * (int * identifier option)
| BinderType of name
- | QuestionMark of bool
+ | QuestionMark of obligation_definition_status
| CasesType
| InternalHole
| TomatchTypeParameter of inductive * int
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 5810f93d..b9cb2142 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: evd.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: evd.mli 11865 2009-01-28 17:34:30Z herbelin $ i*)
(*i*)
open Util
@@ -52,6 +52,7 @@ val evar_unfiltered_env : evar_info -> env
val evar_env : evar_info -> env
type evar_map
+val eq_evar_map : evar_map -> evar_map -> bool
val empty : evar_map
@@ -166,11 +167,16 @@ val empty_evar_defs : evar_defs
val evars_of : evar_defs -> evar_map
val evars_reset_evd : evar_map -> evar_defs -> evar_defs
+(* Should the obligation be defined (opaque or transparent (default)) or
+ defined transparent and expanded in the term? *)
+
+type obligation_definition_status = Define of bool | Expand
+
(* Evars *)
type hole_kind =
| ImplicitArg of global_reference * (int * identifier option)
| BinderType of name
- | QuestionMark of bool (* Can it be turned into an obligation ? *)
+ | QuestionMark of obligation_definition_status
| CasesType
| InternalHole
| TomatchTypeParameter of inductive * int
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index b4b8f0b8..d3123eb6 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: indrec.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: indrec.ml 11735 2009-01-02 17:22:31Z herbelin $ *)
open Pp
open Util
@@ -29,8 +29,7 @@ open Sign
(* Errors related to recursors building *)
type recursion_scheme_error =
- | NotAllowedCaseAnalysis of bool * sorts * inductive
- | BadInduction of bool * identifier * sorts
+ | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * inductive
| NotMutualInScheme of inductive * inductive
exception RecursionSchemeError of recursion_scheme_error
@@ -57,8 +56,7 @@ let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind =
if not (List.mem kind (elim_sorts specif)) then
raise
(RecursionSchemeError
- (NotAllowedCaseAnalysis
- (dep,(new_sort_in_family kind),ind)));
+ (NotAllowedCaseAnalysis (false,new_sort_in_family kind,ind)));
let ndepar = mip.mind_nrealargs + 1 in
@@ -502,10 +500,10 @@ let instantiate_type_indrec_scheme sort npars term =
let check_arities listdepkind =
let _ = List.fold_left
(fun ln ((_,ni as mind),mibi,mipi,dep,kind) ->
- let id = mipi.mind_typename in
let kelim = elim_sorts (mibi,mipi) in
if not (List.exists ((=) kind) kelim) then raise
- (RecursionSchemeError (BadInduction (dep,id,new_sort_in_family kind)))
+ (RecursionSchemeError
+ (NotAllowedCaseAnalysis (true,new_sort_in_family kind,mind)))
else if List.mem ni ln then raise
(RecursionSchemeError (NotMutualInScheme (mind,mind)))
else ni::ln)
@@ -593,7 +591,8 @@ let lookup_eliminator ind_sp s =
errorlabstrm "default_elim"
(strbrk "Cannot find the elimination combinator " ++
pr_id id ++ strbrk ", the elimination of the inductive definition " ++
- pr_id id ++ strbrk " on sort " ++ pr_sort_family s ++
+ pr_global_env Idset.empty (IndRef ind_sp) ++
+ strbrk " on sort " ++ pr_sort_family s ++
strbrk " is probably not allowed.")
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index 6f177474..102c7c7f 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: indrec.mli 9831 2007-05-17 18:55:42Z herbelin $ i*)
+(*i $Id: indrec.mli 11562 2008-11-09 11:30:10Z herbelin $ i*)
(*i*)
open Names
@@ -20,8 +20,7 @@ open Evd
(* Errors related to recursors building *)
type recursion_scheme_error =
- | NotAllowedCaseAnalysis of bool * sorts * inductive
- | BadInduction of bool * identifier * sorts
+ | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * inductive
| NotMutualInScheme of inductive * inductive
exception RecursionSchemeError of recursion_scheme_error
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 127cd0f2..9f8c06da 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: inductiveops.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: inductiveops.ml 11436 2008-10-07 13:56:55Z barras $ *)
open Util
open Names
@@ -393,6 +393,58 @@ let arity_of_case_predicate env (ind,params) dep k =
it_mkProd_or_LetIn concl arsign
(***********************************************)
+(* Inferring the sort of parameters of a polymorphic inductive type
+ knowing the sort of the conclusion *)
+
+(* Check if u (sort of a parameter) appears in the sort of the
+ inductive (is). This is done by trying to enforce u > u' >= is
+ in the empty univ graph. If an inconsistency appears, then
+ is depends on u. *)
+let is_constrained is u =
+ try
+ let u' = fresh_local_univ() in
+ let _ =
+ merge_constraints
+ (enforce_geq u (super u')
+ (enforce_geq u' is Constraint.empty))
+ initial_universes in
+ false
+ with UniverseInconsistency _ -> true
+
+(* Compute the inductive argument types: replace the sorts
+ that appear in the type of the inductive by the sort of the
+ conclusion, and the other ones by fresh universes. *)
+let rec instantiate_universes env scl is = function
+ | (_,Some _,_ as d)::sign, exp ->
+ d :: instantiate_universes env scl is (sign, exp)
+ | d::sign, None::exp ->
+ d :: instantiate_universes env scl is (sign, exp)
+ | (na,None,ty)::sign, Some u::exp ->
+ let ctx,_ = Reduction.dest_arity env ty in
+ let s =
+ if is_constrained is u then
+ scl (* constrained sort: replace by scl *)
+ else
+ (* unconstriained sort: replace by fresh universe *)
+ new_Type_sort() in
+ (na,None,mkArity(ctx,s)):: instantiate_universes env scl is (sign, exp)
+ | sign, [] -> sign (* Uniform parameters are exhausted *)
+ | [], _ -> assert false
+
+(* Does not deal with universes, but only with Set/Type distinction *)
+let type_of_inductive_knowing_conclusion env mip conclty =
+ match mip.mind_arity with
+ | Monomorphic s ->
+ s.mind_user_arity
+ | Polymorphic ar ->
+ let _,scl = Reduction.dest_arity env conclty in
+ let ctx = List.rev mip.mind_arity_ctxt in
+ let ctx =
+ instantiate_universes
+ env scl ar.poly_level (ctx,ar.poly_param_levels) in
+ mkArity (List.rev ctx,scl)
+
+(***********************************************)
(* Guard condition *)
(* A function which checks that a term well typed verifies both
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 1d24659c..1cf940cb 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 11301 2008-08-04 19:41:18Z herbelin $ i*)
+(*i $Id: inductiveops.mli 11436 2008-10-07 13:56:55Z barras $ i*)
open Names
open Term
@@ -113,6 +113,11 @@ val make_default_case_info : env -> case_style -> inductive -> case_info
i*)
(********************)
+
+val type_of_inductive_knowing_conclusion :
+ env -> one_inductive_body -> types -> types
+
+(********************)
val control_only_guard : env -> types -> unit
val subst_inductive : Mod_subst.substitution -> inductive -> inductive
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index d066a58d..93bac98e 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: matching.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: matching.ml 11735 2009-01-02 17:22:31Z herbelin $ *)
(*i*)
open Util
@@ -44,15 +44,37 @@ open Pattern
*)
+type bound_ident_map = (identifier * identifier) list
+
exception PatternMatchingFailure
-let constrain (n,m) sigma =
- if List.mem_assoc n sigma then
- if eq_constr m (List.assoc n sigma) then sigma
+let constrain (n,m) (names,terms as subst) =
+ try
+ if eq_constr m (List.assoc n terms) then subst
else raise PatternMatchingFailure
- else
- (n,m)::sigma
-
+ with
+ Not_found ->
+ if List.mem_assoc n names then
+ Flags.if_verbose Pp.warning
+ ("Collision between bound variable "^string_of_id n^
+ " and a metavariable of same name.");
+ (names,(n,m)::terms)
+
+let add_binders na1 na2 (names,terms as subst) =
+ match na1, na2 with
+ | Name id1, Name id2 ->
+ if List.mem_assoc id1 names then
+ (Flags.if_verbose Pp.warning
+ ("Collision between bound variables of name"^string_of_id id1);
+ (names,terms))
+ else
+ (if List.mem_assoc id1 terms then
+ Flags.if_verbose Pp.warning
+ ("Collision between bound variable "^string_of_id id1^
+ " and another bound variable of same name.");
+ ((id1,id2)::names,terms));
+ | _ -> subst
+
let build_lambda toabstract stk (m : constr) =
let rec buildrec m p_0 p_1 = match p_0,p_1 with
| (_, []) -> m
@@ -77,7 +99,10 @@ let same_case_structure (_,cs1,ind,_) ci2 br1 br2 =
| None -> cs1 = ci2.ci_cstr_nargs
let matches_core convert allow_partial_app pat c =
- let rec sorec stk sigma p t =
+ let conv = match convert with
+ | None -> eq_constr
+ | Some (env,sigma) -> is_conv env sigma in
+ let rec sorec stk subst p t =
let cT = strip_outer_cast t in
match p,kind_of_term cT with
| PSoApp (n,args),m ->
@@ -89,7 +114,7 @@ let matches_core convert allow_partial_app pat c =
args in
let frels = Intset.elements (free_rels cT) in
if list_subset frels relargs then
- constrain (n,build_lambda relargs stk cT) sigma
+ constrain (n,build_lambda relargs stk cT) subst
else
raise PatternMatchingFailure
@@ -97,66 +122,63 @@ let matches_core convert allow_partial_app pat c =
let depth = List.length stk in
if depth = 0 then
(* Optimisation *)
- constrain (n,cT) sigma
+ constrain (n,cT) subst
else
let frels = Intset.elements (free_rels cT) in
if List.for_all (fun i -> i > depth) frels then
- constrain (n,lift (-depth) cT) sigma
+ constrain (n,lift (-depth) cT) subst
else
raise PatternMatchingFailure
- | PMeta None, m -> sigma
+ | PMeta None, m -> subst
- | PRef (VarRef v1), Var v2 when v1 = v2 -> sigma
+ | PRef (VarRef v1), Var v2 when v1 = v2 -> subst
- | PVar v1, Var v2 when v1 = v2 -> sigma
+ | PVar v1, Var v2 when v1 = v2 -> subst
- | PRef ref, _ when constr_of_global ref = cT -> sigma
+ | PRef ref, _ when conv (constr_of_global ref) cT -> subst
- | PRel n1, Rel n2 when n1 = n2 -> sigma
+ | PRel n1, Rel n2 when n1 = n2 -> subst
- | PSort (RProp c1), Sort (Prop c2) when c1 = c2 -> sigma
+ | PSort (RProp c1), Sort (Prop c2) when c1 = c2 -> subst
- | PSort (RType _), Sort (Type _) -> sigma
+ | PSort (RType _), Sort (Type _) -> subst
- | PApp (p, [||]), _ -> sorec stk sigma p t
+ | PApp (p, [||]), _ -> sorec stk subst p t
| PApp (PApp (h, a1), a2), _ ->
- sorec stk sigma (PApp(h,Array.append a1 a2)) t
+ sorec stk subst (PApp(h,Array.append a1 a2)) t
| PApp (PMeta (Some n),args1), App (c2,args2) when allow_partial_app ->
let p = Array.length args2 - Array.length args1 in
if p>=0 then
let args21, args22 = array_chop p args2 in
- let sigma =
+ let subst =
let depth = List.length stk in
let c = mkApp(c2,args21) in
let frels = Intset.elements (free_rels c) in
if List.for_all (fun i -> i > depth) frels then
- constrain (n,lift (-depth) c) sigma
+ constrain (n,lift (-depth) c) subst
else
raise PatternMatchingFailure in
- array_fold_left2 (sorec stk) sigma args1 args22
+ array_fold_left2 (sorec stk) subst args1 args22
else raise PatternMatchingFailure
| PApp (c1,arg1), App (c2,arg2) ->
- (try array_fold_left2 (sorec stk) (sorec stk sigma c1 c2) arg1 arg2
+ (try array_fold_left2 (sorec stk) (sorec stk subst c1 c2) arg1 arg2
with Invalid_argument _ -> raise PatternMatchingFailure)
| PProd (na1,c1,d1), Prod(na2,c2,d2) ->
- sorec ((na2,c2)::stk) (sorec stk sigma c1 c2) d1 d2
+ sorec ((na2,c2)::stk)
+ (add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2
| PLambda (na1,c1,d1), Lambda(na2,c2,d2) ->
- sorec ((na2,c2)::stk) (sorec stk sigma c1 c2) d1 d2
+ sorec ((na2,c2)::stk)
+ (add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2
| PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) ->
- sorec ((na2,t2)::stk) (sorec stk sigma c1 c2) d1 d2
-
- | PRef (ConstRef _ as ref), _ when convert <> None ->
- let (env,evars) = Option.get convert in
- let c = constr_of_global ref in
- if is_conv env evars c cT then sigma
- else raise PatternMatchingFailure
+ sorec ((na2,t2)::stk)
+ (add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2
| PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
let ctx,b2 = decompose_lam_n_assum ci.ci_cstr_nargs.(0) b2 in
@@ -167,118 +189,128 @@ let matches_core convert allow_partial_app pat c =
let s = List.fold_left (fun l (na,_,t) -> (na,t)::l) stk ctx in
let s' = List.fold_left (fun l (na,_,t) -> (na,t)::l) stk ctx' in
let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in
- sorec s' (sorec s (sorec stk sigma a1 a2) b1 b2) b1' b2'
+ sorec s' (sorec s (sorec stk subst a1 a2) b1 b2) b1' b2'
else
raise PatternMatchingFailure
| PCase (ci1,p1,a1,br1), Case (ci2,p2,a2,br2) ->
if same_case_structure ci1 ci2 br1 br2 then
array_fold_left2 (sorec stk)
- (sorec stk (sorec stk sigma a1 a2) p1 p2) br1 br2
+ (sorec stk (sorec stk subst a1 a2) p1 p2) br1 br2
else
raise PatternMatchingFailure
- | PFix c1, Fix _ when eq_constr (mkFix c1) cT -> sigma
- | PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> sigma
+ | PFix c1, Fix _ when eq_constr (mkFix c1) cT -> subst
+ | PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> subst
| _ -> raise PatternMatchingFailure
- in
- Sort.list (fun (a,_) (b,_) -> a<b) (sorec [] [] pat c)
+ in
+ let names,terms = sorec [] ([],[]) pat c in
+ (names,Sort.list (fun (a,_) (b,_) -> a<b) terms)
-let matches = matches_core None true
+let extended_matches = matches_core None true
-let pmatches = matches_core None true
+let matches c p = snd (matches_core None true c p)
-(* To skip to the next occurrence *)
-exception NextOccurrence of int
+let special_meta = (-1)
(* Tells if it is an authorized occurrence and if the instance is closed *)
-let authorized_occ nocc mres =
- if not (List.for_all (fun (_,c) -> closed0 c) (fst mres)) then
- raise PatternMatchingFailure;
- if nocc = 0 then mres
- else raise (NextOccurrence nocc)
-
-let special_meta = (-1)
+let authorized_occ partial_app closed pat c mk_ctx next =
+ try
+ let sigma = matches_core None partial_app pat c in
+ if closed && not (List.for_all (fun (_,c) -> closed0 c) (snd sigma))
+ then next ()
+ else sigma, mk_ctx (mkMeta special_meta), next
+ with
+ PatternMatchingFailure -> next ()
(* Tries to match a subterm of [c] with [pat] *)
-let rec sub_match nocc pat c =
+let sub_match ?(partial_app=false) ?(closed=true) pat c =
+ let rec aux c mk_ctx next =
match kind_of_term c with
| Cast (c1,k,c2) ->
- (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
- | PatternMatchingFailure ->
- let (lm,lc) = try_sub_match nocc pat [c1] in
- (lm,mkCast (List.hd lc, k,c2))
- | NextOccurrence nocc ->
- let (lm,lc) = try_sub_match (nocc - 1) pat [c1] in
- (lm,mkCast (List.hd lc, k,c2)))
- | Lambda (x,c1,c2) ->
- (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
- | PatternMatchingFailure ->
- let (lm,lc) = try_sub_match nocc pat [c1;c2] in
- (lm,mkLambda (x,List.hd lc,List.nth lc 1))
- | NextOccurrence nocc ->
- let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in
- (lm,mkLambda (x,List.hd lc,List.nth lc 1)))
+ authorized_occ partial_app closed pat c mk_ctx (fun () ->
+ let mk_ctx lc = mk_ctx (mkCast (List.hd lc, k,c2)) in
+ try_aux [c1] mk_ctx next)
+ | Lambda (x,c1,c2) ->
+ authorized_occ partial_app closed pat c mk_ctx (fun () ->
+ let mk_ctx lc = mk_ctx (mkLambda (x,List.hd lc,List.nth lc 1)) in
+ try_aux [c1;c2] mk_ctx next)
| Prod (x,c1,c2) ->
- (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
- | PatternMatchingFailure ->
- let (lm,lc) = try_sub_match nocc pat [c1;c2] in
- (lm,mkProd (x,List.hd lc,List.nth lc 1))
- | NextOccurrence nocc ->
- let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in
- (lm,mkProd (x,List.hd lc,List.nth lc 1)))
- | LetIn (x,c1,t2,c2) ->
- (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
- | PatternMatchingFailure ->
- let (lm,lc) = try_sub_match nocc pat [c1;t2;c2] in
- (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2))
- | NextOccurrence nocc ->
- let (lm,lc) = try_sub_match (nocc - 1) pat [c1;t2;c2] in
- (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2)))
+ authorized_occ partial_app closed pat c mk_ctx (fun () ->
+ let mk_ctx lc = mk_ctx (mkProd (x,List.hd lc,List.nth lc 1)) in
+ try_aux [c1;c2] mk_ctx next)
+ | LetIn (x,c1,t,c2) ->
+ authorized_occ partial_app closed pat c mk_ctx (fun () ->
+ let mk_ctx = function [c1;c2] -> mkLetIn (x,c1,t,c2) | _ -> assert false
+ in try_aux [c1;c2] mk_ctx next)
| App (c1,lc) ->
- (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
- | PatternMatchingFailure ->
- let (lm,le) = try_sub_match nocc pat (c1::(Array.to_list lc)) in
- (lm,mkApp (List.hd le, Array.of_list (List.tl le)))
- | NextOccurrence nocc ->
- let (lm,le) = try_sub_match (nocc - 1) pat (c1::(Array.to_list lc)) in
- (lm,mkApp (List.hd le, Array.of_list (List.tl le))))
+ authorized_occ partial_app closed pat c mk_ctx (fun () ->
+ let topdown = true in
+ if partial_app then
+ if topdown then
+ let lc1 = Array.sub lc 0 (Array.length lc - 1) in
+ let app = mkApp (c1,lc1) in
+ let mk_ctx = function
+ | [app';c] -> mk_ctx (mkApp (app',[|c|]))
+ | _ -> assert false in
+ try_aux [app;array_last lc] mk_ctx next
+ else
+ let rec aux2 app args next =
+ match args with
+ | [] ->
+ let mk_ctx le =
+ mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
+ try_aux (c1::Array.to_list lc) mk_ctx next
+ | arg :: args ->
+ let app = mkApp (app,[|arg|]) in
+ let next () = aux2 app args next in
+ let mk_ctx ce = mk_ctx (mkApp (ce, Array.of_list args)) in
+ aux app mk_ctx next in
+ aux2 c1 (Array.to_list lc) next
+ else
+ let mk_ctx le =
+ mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
+ try_aux (c1::Array.to_list lc) mk_ctx next)
| Case (ci,hd,c1,lc) ->
- (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
- | PatternMatchingFailure ->
- let (lm,le) = try_sub_match nocc pat (c1::Array.to_list lc) in
- (lm,mkCase (ci,hd,List.hd le,Array.of_list (List.tl le)))
- | NextOccurrence nocc ->
- let (lm,le) = try_sub_match (nocc - 1) pat (c1::Array.to_list lc) in
- (lm,mkCase (ci,hd,List.hd le,Array.of_list (List.tl le))))
+ authorized_occ partial_app closed pat c mk_ctx (fun () ->
+ let mk_ctx le =
+ mk_ctx (mkCase (ci,hd,List.hd le,Array.of_list (List.tl le))) in
+ try_aux (c1::Array.to_list lc) mk_ctx next)
| Construct _ | Fix _ | Ind _|CoFix _ |Evar _|Const _
| Rel _|Meta _|Var _|Sort _ ->
- (try authorized_occ nocc ((matches pat c),mkMeta special_meta) with
- | PatternMatchingFailure -> raise (NextOccurrence nocc)
- | NextOccurrence nocc -> raise (NextOccurrence (nocc - 1)))
-
-(* Tries [sub_match] for all terms in the list *)
-and try_sub_match nocc pat lc =
- let rec try_sub_match_rec nocc pat lacc = function
- | [] -> raise (NextOccurrence nocc)
- | c::tl ->
- (try
- let (lm,ce) = sub_match nocc pat c in
- (lm,lacc@(ce::tl))
- with
- | NextOccurrence nocc -> try_sub_match_rec nocc pat (lacc@[c]) tl) in
- try_sub_match_rec nocc pat [] lc
-
-let match_subterm nocc pat c =
- try sub_match nocc pat c
- with NextOccurrence _ -> raise PatternMatchingFailure
-
-let is_matching pat n =
- try let _ = matches pat n in true
+ authorized_occ partial_app closed pat c mk_ctx next
+
+ (* Tries [sub_match] for all terms in the list *)
+ and try_aux lc mk_ctx next =
+ let rec try_sub_match_rec lacc = function
+ | [] -> next ()
+ | c::tl ->
+ let mk_ctx ce = mk_ctx (List.rev_append lacc (ce::tl)) in
+ let next () = try_sub_match_rec (c::lacc) tl in
+ aux c mk_ctx next in
+ try_sub_match_rec [] lc in
+ aux c (fun x -> x) (fun () -> raise PatternMatchingFailure)
+
+type subterm_matching_result =
+ (bound_ident_map * patvar_map) * constr * (unit -> subterm_matching_result)
+
+let match_subterm pat c = sub_match pat c
+
+let match_appsubterm pat c = sub_match ~partial_app:true pat c
+
+let match_subterm_gen app pat c = sub_match ~partial_app:app pat c
+
+let is_matching pat c =
+ try let _ = matches pat c in true
+ with PatternMatchingFailure -> false
+
+let is_matching_appsubterm ?(closed=true) pat c =
+ try let _ = sub_match ~partial_app:true ~closed pat c in true
with PatternMatchingFailure -> false
-let matches_conv env sigma = matches_core (Some (env,sigma)) false
+let matches_conv env sigma c p =
+ snd (matches_core (Some (env,sigma)) false c p)
let is_matching_conv env sigma pat n =
try let _ = matches_conv env sigma pat n in true
diff --git a/pretyping/matching.mli b/pretyping/matching.mli
index e6065c68..b54a17b7 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: matching.mli 6616 2005-01-21 17:18:23Z herbelin $ i*)
+(*i $Id: matching.mli 11739 2009-01-02 19:33:19Z herbelin $ i*)
(*i*)
open Names
@@ -22,30 +22,58 @@ exception PatternMatchingFailure
val special_meta : metavariable
+type bound_ident_map = (identifier * identifier) list
+
(* [matches pat c] matches [c] against [pat] and returns the resulting
assignment of metavariables; it raises [PatternMatchingFailure] if
not matchable; bindings are given in increasing order based on the
numbers given in the pattern *)
val matches : constr_pattern -> constr -> patvar_map
-(* [is_matching pat c] just tells if [c] matches against [pat] *)
+(* [extended_matches pat c] also returns the names of bound variables
+ in [c] that matches the bound variables in [pat]; if several bound
+ variables or metavariables have the same name, the metavariable,
+ or else the rightmost bound variable, takes precedence *)
+val extended_matches :
+ constr_pattern -> constr -> bound_ident_map * patvar_map
+(* [is_matching pat c] just tells if [c] matches against [pat] *)
val is_matching : constr_pattern -> constr -> bool
(* [matches_conv env sigma] matches up to conversion in environment
[(env,sigma)] when constants in pattern are concerned; it raises
[PatternMatchingFailure] if not matchable; bindings are given in
increasing order based on the numbers given in the pattern *)
-
val matches_conv :env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
+(* The type of subterm matching results: a substitution + a context
+ (whose hole is denoted with [special_meta]) + a continuation that
+ either returns the next matching subterm or raise PatternMatchingFailure *)
+type subterm_matching_result =
+ (bound_ident_map * patvar_map) * constr * (unit -> subterm_matching_result)
+
(* [match_subterm n pat c] returns the substitution and the context
- corresponding to the [n+1]th **closed** subterm of [c] matching [pat];
- It raises PatternMatchingFailure if no such matching exists *)
-val match_subterm : int -> constr_pattern -> constr -> patvar_map * constr
+ corresponding to the first **closed** subterm of [c] matching [pat], and
+ a continuation that looks for the next matching subterm.
+ It raises PatternMatchingFailure if no subterm matches the pattern *)
+val match_subterm : constr_pattern -> constr -> subterm_matching_result
+
+(* [match_appsubterm pat c] returns the substitution and the context
+ corresponding to the first **closed** subterm of [c] matching [pat],
+ considering application contexts as well. It also returns a
+ continuation that looks for the next matching subterm.
+ It raises PatternMatchingFailure if no subterm matches the pattern *)
+val match_appsubterm : constr_pattern -> constr -> subterm_matching_result
+
+(* [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *)
+val match_subterm_gen : bool (* true = with app context *) ->
+ constr_pattern -> constr -> subterm_matching_result
+
+(* [is_matching_appsubterm pat c] tells if a subterm of [c] matches
+ against [pat] taking partial subterms into consideration *)
+val is_matching_appsubterm : ?closed:bool -> constr_pattern -> constr -> bool
(* [is_matching_conv env sigma pat c] tells if [c] matches against [pat]
up to conversion for constants in patterns *)
-
val is_matching_conv :
env -> Evd.evar_map -> constr_pattern -> constr -> bool
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a3246bc8..1cac9011 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pretyping.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: pretyping.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
open Pp
open Util
@@ -586,7 +586,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
mkCase (ci, pred, cj.uj_val, [|b1;b2|])
in
{ uj_val = v; uj_type = p }
-
+
| RCases (loc,sty,po,tml,eqns) ->
Cases.compile_cases loc sty
((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref)
@@ -605,8 +605,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
(* ... except for Correctness *)
let v = mkCast (cj.uj_val, k, tj.utj_val) in
{ uj_val = v; uj_type = tj.utj_val }
- in
- inh_conv_coerce_to_tycon loc env evdref cj tycon
+ in inh_conv_coerce_to_tycon loc env evdref cj tycon
| RDynamic (loc,d) ->
if (tag d) = "constr" then
@@ -657,12 +656,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct
| IsType ->
(pretype_type empty_valcon env evdref lvar c).utj_val in
let evd,_ = consider_remaining_unif_problems env !evdref in
- evdref := evd; c'
+ evdref := evd;
+ nf_isevar !evdref c'
let pretype_gen evdref env lvar kind c =
let c = pretype_gen_aux evdref env lvar kind c in
evdref := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env !evdref;
- nf_evar (evars_of !evdref) c
+ nf_isevar !evdref c
(* TODO: comment faire remonter l'information si le typage a resolu des
variables du sigma original. il faudrait que la fonction de typage
@@ -691,14 +691,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let ise_pretype_gen fail_evar sigma env lvar kind c =
let evdref = ref (Evd.create_evar_defs sigma) in
- let c = pretype_gen evdref env lvar kind c in
- let evd,_ = consider_remaining_unif_problems env !evdref in
+ let c = pretype_gen_aux evdref env lvar kind c in
if fail_evar then
- let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in
+ let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env !evdref in
let c = Evarutil.nf_isevar evd c in
check_evars env Evd.empty evd c;
evd, c
- else evd, c
+ else !evdref, c
(** Entry points of the high-level type synthesis algorithm *)
@@ -716,17 +715,17 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let understand_tcc_evars evdref env kind c =
pretype_gen evdref env ([],[]) kind c
-
+
let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c =
let evd, t =
- if resolve_classes then
- ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c
- else
- let evdref = ref (Evd.create_evar_defs sigma) in
- let c = pretype_gen_aux evdref env ([],[]) (OfType exptyp) c in
- !evdref, nf_isevar !evdref c
- in
- Evd.evars_of evd, t
+ let evdref = ref (Evd.create_evar_defs sigma) in
+ let c =
+ if resolve_classes then
+ pretype_gen evdref env ([],[]) (OfType exptyp) c
+ else
+ pretype_gen_aux evdref env ([],[]) (OfType exptyp) c
+ in !evdref, c
+ in Evd.evars_of evd, t
end
-
+
module Default : S = Pretyping_F(Coercion.Default)
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 3726b8df..30b62ea8 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: rawterm.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: rawterm.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
(*i*)
open Util
@@ -219,7 +219,7 @@ let free_rawvars =
| RLambda (loc,na,_,ty,c) | RProd (loc,na,_,ty,c) | RLetIn (loc,na,ty,c) ->
let vs' = vars bounded vs ty in
let bounded' = add_name_to_ids bounded na in
- vars bounded' vs' c
+ vars bounded' vs' c
| RCases (loc,sty,rtntypopt,tml,pl) ->
let vs1 = vars_option bounded vs rtntypopt in
let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 06289434..7c4023b9 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: recordops.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: recordops.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
open Util
open Pp
@@ -32,9 +32,9 @@ open Reductionops
projection ou bien une fonction constante (associée à un LetIn) *)
type struc_typ = {
- s_CONST : identifier;
+ s_CONST : constructor;
s_EXPECTEDPARAM : int;
- s_PROJKIND : bool list;
+ s_PROJKIND : (name * bool) list;
s_PROJ : constant option list }
let structure_table = ref (Indmap.empty : struc_typ Indmap.t)
@@ -61,8 +61,9 @@ let subst_structure (_,subst,((kn,i),id,kl,projs as obj)) =
(Option.smartmap (fun kn -> fst (subst_con subst kn)))
projs
in
- if projs' == projs && kn' == kn then obj else
- ((kn',i),id,kl,projs')
+ let id' = fst (subst_constructor subst id) in
+ if projs' == projs && kn' == kn && id' == id then obj else
+ ((kn',i),id',kl,projs')
let discharge_structure (_,(ind,id,kl,projs)) =
Some (Lib.discharge_inductive ind, id, kl,
@@ -88,6 +89,10 @@ let find_projection_nparams = function
| ConstRef cst -> (Cmap.find cst !projection_table).s_EXPECTEDPARAM
| _ -> raise Not_found
+let find_projection = function
+ | ConstRef cst -> Cmap.find cst !projection_table
+ | _ -> raise Not_found
+
(************************************************************************)
(*s A canonical structure declares "canonical" conversion hints between *)
@@ -135,7 +140,7 @@ let canonical_projections () =
!object_table []
let keep_true_projections projs kinds =
- map_succeed (function (p,true) -> p | _ -> failwith "")
+ map_succeed (function (p,(_,true)) -> p | _ -> failwith "")
(List.combine projs kinds)
let cs_pattern_of_constr t =
@@ -237,7 +242,7 @@ let check_and_decompose_canonical_structure ref =
| Construct (indsp,1) -> indsp
| _ -> error_not_structure ref in
let s = try lookup_structure indsp with Not_found -> error_not_structure ref in
- let ntrue_projs = List.length (List.filter (fun x -> x) s.s_PROJKIND) in
+ let ntrue_projs = List.length (List.filter (fun (_, x) -> x) s.s_PROJKIND) in
if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then
error_not_structure ref;
(sp,indsp)
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 74f6a9ce..ea960aa9 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 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: recordops.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
(*i*)
open Names
@@ -21,8 +21,14 @@ open Library
(*s A structure S is a non recursive inductive type with a single
constructor (the name of which defaults to Build_S) *)
+type struc_typ = {
+ s_CONST : constructor;
+ s_EXPECTEDPARAM : int;
+ s_PROJKIND : (name * bool) list;
+ s_PROJ : constant option list }
+
val declare_structure :
- inductive * identifier * bool list * constant option list -> unit
+ inductive * constructor * (name * 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
@@ -32,6 +38,9 @@ val lookup_projections : inductive -> constant option list
(* raise [Not_found] if not a projection *)
val find_projection_nparams : global_reference -> int
+(* raise [Not_found] if not a projection *)
+val find_projection : global_reference -> struc_typ
+
(*s A canonical structure declares "canonical" conversion hints between *)
(* the effective components of a structure and the projections of the *)
(* structure *)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 21e881b9..a1603d69 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: reductionops.ml 11343 2008-09-01 20:55:13Z herbelin $ *)
+(* $Id: reductionops.ml 11796 2009-01-18 13:41:39Z herbelin $ *)
open Pp
open Util
@@ -537,6 +537,8 @@ let nf_evar sigma =
local_strong (whd_evar sigma)
(* lazy reduction functions. The infos must be created for each term *)
+(* Note by HH [oct 08] : why would it be the job of clos_norm_flags to add
+ a [nf_evar] here *)
let clos_norm_flags flgs env sigma t =
norm_val (create_clos_infos flgs env) (inject (nf_evar sigma t))
@@ -625,8 +627,23 @@ let pb_equal = function
let sort_cmp = sort_cmp
+
+let nf_red_env sigma env =
+ let nf_decl = function
+ (x,Some t,ty) -> (x,Some (nf_evar sigma t),ty)
+ | d -> d in
+ let sign = named_context env in
+ let ctxt = rel_context env in
+ let env = reset_context env in
+ let env = Sign.fold_named_context
+ (fun d env -> push_named (nf_decl d) env) ~init:env sign in
+ Sign.fold_rel_context
+ (fun d env -> push_rel (nf_decl d) env) ~init:env ctxt
+
+
let test_conversion f env sigma x y =
- try let _ = f env (nf_evar sigma x) (nf_evar sigma y) in true
+ try let _ =
+ f (nf_red_env sigma env) (nf_evar sigma x) (nf_evar sigma y) in true
with NotConvertible -> false
let is_conv env sigma = test_conversion Reduction.conv env sigma
@@ -652,11 +669,11 @@ let whd_meta metamap c = match kind_of_term c with
(* Try to replace all metas. Does not replace metas in the metas' values
* Differs from (strong whd_meta). *)
let plain_instance s c =
- let rec irec u = match kind_of_term u with
- | Meta p -> (try List.assoc p s with Not_found -> u)
+ let rec irec n u = match kind_of_term u with
+ | Meta p -> (try lift n (List.assoc p s) with Not_found -> u)
| App (f,l) when isCast f ->
let (f,_,t) = destCast f in
- let l' = Array.map irec l in
+ let l' = Array.map (irec n) l in
(match kind_of_term f with
| Meta p ->
(* Don't flatten application nodes: this is used to extract a
@@ -669,12 +686,13 @@ let plain_instance s c =
mkLetIn (Name h,g,t,mkApp(mkRel 1,Array.map (lift 1) l'))
| _ -> mkApp (g,l')
with Not_found -> mkApp (f,l'))
- | _ -> mkApp (irec f,l'))
+ | _ -> mkApp (irec n f,l'))
| Cast (m,_,_) when isMeta m ->
- (try List.assoc (destMeta m) s with Not_found -> u)
- | _ -> map_constr irec u
+ (try lift n (List.assoc (destMeta m) s) with Not_found -> u)
+ | _ ->
+ map_constr_with_binders succ irec n u
in
- if s = [] then c else irec c
+ if s = [] then c else irec 0 c
(* [instance] is used for [res_pf]; the call to [local_strong whd_betaiota]
has (unfortunately) different subtle side effects:
@@ -706,8 +724,8 @@ let plain_instance s c =
If a lemma has the type "(fun x => p) t" then rewriting t may fail
if the type of the lemma is first beta-reduced (this typically happens
when rewriting a single variable and the type of the lemma is obtained
- by meta_instance (with empty map) which itself call instance with this
- empty map.
+ by meta_instance (with empty map) which itself calls instance with this
+ empty map).
*)
let instance s c =
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 82c2668c..2465bd1e 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: retyping.ml 11077 2008-06-09 11:26:32Z herbelin $ *)
+(* $Id: retyping.ml 11778 2009-01-13 13:17:39Z msozeau $ *)
open Util
open Term
@@ -49,7 +49,7 @@ let retype sigma metamap =
match kind_of_term cstr with
| Meta n ->
(try strip_outer_cast (List.assoc n metamap)
- with Not_found -> anomaly "type_of: this is not a well-typed term")
+ with Not_found -> anomaly ("type_of: unknown meta " ^ string_of_int n))
| Rel n ->
let (_,_,ty) = lookup_rel n env in
lift n ty
@@ -111,9 +111,15 @@ let retype sigma metamap =
| Cast (c,_, s) when isSort s -> family_of_sort (destSort s)
| Sort (Prop c) -> InType
| Sort (Type u) -> InType
- | Prod (name,t,c2) -> sort_family_of (push_rel (name,None,t) env) c2
+ | Prod (name,t,c2) ->
+ let s2 = sort_family_of (push_rel (name,None,t) env) c2 in
+ if Environ.engagement env <> Some ImpredicativeSet &&
+ s2 = InSet & sort_family_of env t = InType then InType else s2
+ | App(f,args) when isGlobalRef f ->
+ let t = type_of_global_reference_knowing_parameters env f args in
+ family_of_sort (sort_of_atomic_type env sigma t args)
| App(f,args) ->
- family_of_sort (sort_of_atomic_type env sigma (type_of env f) args)
+ family_of_sort (sort_of_atomic_type env sigma (type_of env f) args)
| Lambda _ | Fix _ | Construct _ ->
anomaly "sort_of: Not a type (1)"
| _ -> family_of_sort (decomp_sort env sigma (type_of env t))
@@ -139,6 +145,20 @@ let get_sort_family_of env sigma c = let _,_,f,_ = retype sigma [] in f env c
let type_of_global_reference_knowing_parameters env sigma c args =
let _,_,_,f = retype sigma [] in f env c args
+let type_of_global_reference_knowing_conclusion env sigma c conclty =
+ let conclty = nf_evar sigma conclty in
+ match kind_of_term c with
+ | Ind ind ->
+ let (_,mip) = Inductive.lookup_mind_specif env ind in
+ type_of_inductive_knowing_conclusion env mip conclty
+ | Const cst ->
+ let t = constant_type env cst in
+ (* TODO *)
+ Typeops.type_of_constant_knowing_parameters env t [||]
+ | Var id -> type_of_var env id
+ | Construct cstr -> type_of_constructor env cstr
+ | _ -> assert false
+
(* We are outside the kernel: we take fresh universes *)
(* to avoid tactics and co to refresh universes themselves *)
let get_type_of env sigma c =
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 733cb4b1..ec1fc827 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 9314 2006-10-29 20:11:08Z herbelin $ i*)
+(*i $Id: retyping.mli 11436 2008-10-07 13:56:55Z barras $ i*)
(*i*)
open Names
@@ -37,3 +37,5 @@ val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment
val type_of_global_reference_knowing_parameters : env -> evar_map -> constr ->
constr array -> types
+val type_of_global_reference_knowing_conclusion :
+ env -> evar_map -> constr -> types -> types
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 57fdbb09..88a6f499 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tacred.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: tacred.ml 11654 2008-12-03 18:39:40Z barras $ *)
open Pp
open Util
@@ -99,10 +99,11 @@ let reference_value sigma env c =
(* One reuses the name of the function after reduction of the fixpoint *)
type constant_evaluation =
- | EliminationFix of int * (int * (int * constr) list * int)
+ | EliminationFix of int * int * (int * (int * constr) list * int)
| EliminationMutualFix of
int * evaluable_reference *
- (evaluable_reference option array * (int * (int * constr) list * int))
+ ((int*evaluable_reference) option array *
+ (int * (int * constr) list * int))
| EliminationCases of int
| NotAnElimination
@@ -171,24 +172,24 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
| _ ->
raise Elimconst) args
in
- if list_distinct (List.map fst li) then
- let k = lv.(i) in
- if k < nargs then
+ if not (list_distinct (List.map fst li)) then
+ raise Elimconst;
+ let k = lv.(i) in
+ if k < nargs then
(* Such an optimisation would need eta-expansion
let p = destRel (List.nth args k) in
EliminationFix (n-p+1,(nbfix,li,n))
*)
- EliminationFix (n,(nbfix,li,n))
- else
- EliminationFix (n-nargs+lv.(i)+1,(nbfix,li,n))
- else
- raise Elimconst
+ EliminationFix (n,nargs,(nbfix,li,n))
+ else
+ EliminationFix (n-nargs+k+1,nargs,(nbfix,li,n))
(* Heuristic to look if global names are associated to other
components of a mutual fixpoint *)
let invert_name labs l na0 env sigma ref = function
| Name id ->
+ let minfxargs = List.length l in
if na0 <> Name id then
let refi = match ref with
| EvalRel _ | EvalEvar _ -> None
@@ -205,9 +206,10 @@ let invert_name labs l na0 env sigma ref = function
let labs',ccl = decompose_lam c in
let _, l' = whd_betalet_stack ccl in
let labs' = List.map snd labs' in
- if labs' = labs & l = l' then Some ref else None
+ if labs' = labs & l = l' then Some (minfxargs,ref)
+ else None
with Not_found (* Undefined ref *) -> None
- else Some ref
+ else Some (minfxargs,ref)
| Anonymous -> None (* Actually, should not occur *)
(* [compute_consteval_direct] expand all constant in a whole, but
@@ -242,7 +244,7 @@ let compute_consteval_mutual_fix sigma env ref =
(match compute_consteval_direct sigma env ref with
| NotAnElimination -> (*Above const was eliminable but this not!*)
NotAnElimination
- | EliminationFix (minarg',infos) ->
+ | EliminationFix (minarg',minfxargs,infos) ->
let refs =
Array.map
(invert_name labs l names.(i) env sigma ref) names in
@@ -263,7 +265,7 @@ let compute_consteval_mutual_fix sigma env ref =
let compute_consteval sigma env ref =
match compute_consteval_direct sigma env ref with
- | EliminationFix (_,(nbfix,_,_)) when nbfix <> 1 ->
+ | EliminationFix (_,_,(nbfix,_,_)) when nbfix <> 1 ->
compute_consteval_mutual_fix sigma env ref
| elim -> elim
@@ -323,28 +325,107 @@ let make_elim_fun (names,(nbfix,lv,n)) largs =
fun i ->
match names.(i) with
| None -> None
- | Some ref ->
+ | Some (minargs,ref) ->
let body = applistc (mkEvalRef ref) la in
let g =
list_fold_left_i (fun q (* j from comment is n+1-q *) c (ij,tij) ->
let subst = List.map (lift (-q)) (list_firstn (n-ij) la) in
let tij' = substl (List.rev subst) tij in
mkLambda (x,tij',c)) 1 body (List.rev lv)
- in Some g
+ in Some (minargs,g)
(* [f] is convertible to [Fix(recindices,bodynum),bodyvect)]:
do so that the reduction uses this extra information *)
-let contract_fix_use_function f
+let dummy = mkProp
+let vfx = id_of_string"_expanded_fix_"
+let vfun = id_of_string"_elimminator_function_"
+
+(* Mark every occurrence of substituted vars (associated to a function)
+ as a problem variable: an evar that can be instantiated either by
+ vfx (expanded fixpoint) or vfun (named function). *)
+let substl_with_function subst constr =
+ let cnt = ref 0 in
+ let evd = ref Evd.empty in
+ let minargs = ref Intmap.empty in
+ let v = Array.of_list subst in
+ let rec subst_total k c =
+ match kind_of_term c with
+ Rel i when k<i ->
+ if i <= k + Array.length v then
+ match v.(i-k-1) with
+ | (fx,Some(min,ref)) ->
+ decr cnt;
+ evd := Evd.add !evd !cnt
+ (Evd.make_evar
+ (val_of_named_context
+ [(vfx,None,dummy);(vfun,None,dummy)])
+ dummy);
+ minargs := Intmap.add !cnt min !minargs;
+ lift k (mkEvar(!cnt,[|fx;ref|]))
+ | (fx,None) -> lift k fx
+ else mkRel (i - Array.length v)
+ | _ ->
+ map_constr_with_binders succ subst_total k c in
+ let c = subst_total 0 constr in
+ (c,!evd,!minargs)
+
+exception Partial
+
+(* each problem variable that cannot be made totally applied even by
+ reduction is solved by the expanded fix term. *)
+let solve_arity_problem env sigma fxminargs c =
+ let evm = ref sigma in
+ let set_fix i = evm := Evd.define !evm i (mkVar vfx) in
+ let rec check strict c =
+ let c' = whd_betaiotazeta c in
+ let (h,rcargs) = decompose_app c' in
+ match kind_of_term h with
+ Evar(i,_) when Intmap.mem i fxminargs && not (Evd.is_defined !evm i) ->
+ let minargs = Intmap.find i fxminargs in
+ if List.length rcargs < minargs then
+ if strict then set_fix i
+ else raise Partial;
+ List.iter (check strict) rcargs
+ | (Var _|Const _) when isEvalRef env h ->
+ (match reference_opt_value sigma env (destEvalRef h) with
+ Some h' ->
+ let bak = !evm in
+ (try List.iter (check false) rcargs
+ with Partial ->
+ evm := bak;
+ check strict (applist(h',rcargs)))
+ | None -> List.iter (check strict) rcargs)
+ | _ -> iter_constr (check strict) c' in
+ check true c;
+ !evm
+
+let substl_checking_arity env subst c =
+ (* we initialize the problem: *)
+ let body,sigma,minargs = substl_with_function subst c in
+ (* we collect arity constraints *)
+ let sigma' = solve_arity_problem env sigma minargs body in
+ (* we propagate the constraints: solved problems are substituted;
+ the other ones are replaced by the function symbol *)
+ let rec nf_fix c =
+ match kind_of_term c with
+ Evar(i,[|fx;f|] as ev) when Intmap.mem i minargs ->
+ (match Evd.existential_opt_value sigma' ev with
+ Some c' -> c'
+ | None -> f)
+ | _ -> map_constr nf_fix c in
+ nf_fix body
+
+
+
+let contract_fix_use_function env f
((recindices,bodynum),(_names,_types,bodies as typedbodies)) =
let nbodies = Array.length recindices in
- let make_Fi j = match f j with
- | None -> mkFix((recindices,j),typedbodies)
- | Some c -> c in
+ let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in
let lbodies = list_tabulate make_Fi nbodies in
- substl (List.rev lbodies) bodies.(bodynum)
+ substl_checking_arity env (List.rev lbodies) (nf_beta bodies.(bodynum))
-let reduce_fix_use_function f whfun fix stack =
+let reduce_fix_use_function env f whfun fix stack =
match fix_recarg fix stack with
| None -> NotReducible
| Some (recargnum,recarg) ->
@@ -357,16 +438,15 @@ let reduce_fix_use_function f whfun fix stack =
let stack' = stack_assign stack recargnum (app_stack recarg') in
(match kind_of_term recarg'hd with
| Construct _ ->
- Reduced (contract_fix_use_function f fix,stack')
+ Reduced (contract_fix_use_function env f fix,stack')
| _ -> NotReducible)
-let contract_cofix_use_function f (bodynum,(_names,_,bodies as typedbodies)) =
+let contract_cofix_use_function env f
+ (bodynum,(_names,_,bodies as typedbodies)) =
let nbodies = Array.length bodies in
- let make_Fi j = match f j with
- | None -> mkCoFix(j,typedbodies)
- | Some c -> c in
+ let make_Fi j = (mkCoFix(j,typedbodies), f j) in
let subbodies = list_tabulate make_Fi nbodies in
- substl (List.rev subbodies) bodies.(bodynum)
+ substl_checking_arity env (List.rev subbodies) (nf_beta bodies.(bodynum))
let reduce_mind_case_use_function func env mia =
match kind_of_term mia.mconstr with
@@ -377,8 +457,9 @@ let reduce_mind_case_use_function func env mia =
let build_cofix_name =
if isConst func then
let (mp,dp,_) = repr_con (destConst func) in
+ let minargs = List.length mia.mcargs in
fun i ->
- if i = bodynum then Some func
+ if i = bodynum then Some (minargs,func)
else match names.(i) with
| Anonymous -> None
| Name id ->
@@ -389,11 +470,13 @@ let reduce_mind_case_use_function func env mia =
let kn = make_con mp dp (label_of_id id) in
try match constant_opt_value env kn with
| None -> None
- | Some _ -> Some (mkConst kn)
+ (* TODO: check kn is correct *)
+ | Some _ -> Some (minargs,mkConst kn)
with Not_found -> None
else
fun _ -> None in
- let cofix_def = contract_cofix_use_function build_cofix_name cofix in
+ let cofix_def =
+ contract_cofix_use_function env build_cofix_name cofix in
mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf)
| _ -> assert false
@@ -432,12 +515,12 @@ let rec red_elim_const env sigma ref largs =
let c', lrest = whd_betadelta_state env sigma (c,largs) in
let whfun = whd_simpl_state env sigma in
(special_red_case sigma env whfun (destCase c'), lrest)
- | EliminationFix (min,infos) when stack_args_size largs >=min ->
+ | EliminationFix (min,minfxargs,infos) when stack_args_size largs >=min ->
let c = reference_value sigma env ref in
let d, lrest = whd_betadelta_state env sigma (c,largs) in
- let f = make_elim_fun ([|Some ref|],infos) largs in
+ let f = make_elim_fun ([|Some (minfxargs,ref)|],infos) largs in
let whfun = whd_construct_state env sigma in
- (match reduce_fix_use_function f whfun (destFix d) lrest with
+ (match reduce_fix_use_function env f whfun (destFix d) lrest with
| NotReducible -> raise Redelimination
| Reduced (c,rest) -> (nf_beta c, rest))
| EliminationMutualFix (min,refgoal,refinfos)
@@ -453,7 +536,7 @@ let rec red_elim_const env sigma ref largs =
let d, lrest = whd_betadelta_state env sigma s in
let f = make_elim_fun refinfos midargs in
let whfun = whd_construct_state env sigma in
- (match reduce_fix_use_function f whfun (destFix d) lrest with
+ (match reduce_fix_use_function env f whfun (destFix d) lrest with
| NotReducible -> raise Redelimination
| Reduced (c,rest) -> (nf_beta c, rest))
| _ -> raise Redelimination
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 1ce53e88..f93212f8 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: termops.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: termops.ml 11639 2008-11-27 17:48:32Z barras $ *)
open Pp
open Util
@@ -425,11 +425,11 @@ let fold_constr_with_binders g f n acc c = match kind_of_term c with
| Fix (_,(lna,tl,bl)) ->
let n' = iterate g (Array.length tl) n in
let fd = array_map2 (fun t b -> (t,b)) tl bl in
- Array.fold_left (fun acc (t,b) -> f n (f n' acc t) b) acc fd
+ Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
| CoFix (_,(lna,tl,bl)) ->
let n' = iterate g (Array.length tl) n in
let fd = array_map2 (fun t b -> (t,b)) tl bl in
- Array.fold_left (fun acc (t,b) -> f n (f n' acc t) b) acc fd
+ Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
(* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate
subterms of [c]; it carries an extra data [acc] which is processed by [g] at
@@ -473,6 +473,13 @@ let occur_existential c =
| _ -> iter_constr occrec c
in try occrec c; false with Occur -> true
+let occur_meta_or_existential c =
+ let rec occrec c = match kind_of_term c with
+ | Evar _ -> raise Occur
+ | Meta _ -> raise Occur
+ | _ -> iter_constr occrec c
+ in try occrec c; false with Occur -> true
+
let occur_const s c =
let rec occur_rec c = match kind_of_term c with
| Const sp when sp=s -> raise Occur
@@ -671,10 +678,18 @@ let subst_term_occ (nowhere_except_in,locs as plocs) c t =
if rest <> [] then error_invalid_occurrence rest;
t'
-let subst_term_occ_decl (nowhere_except_in,locs as plocs) c (id,bodyopt,typ as d) =
- match bodyopt with
- | None -> (id,None,subst_term_occ plocs c typ)
- | Some body ->
+type hyp_location_flag = (* To distinguish body and type of local defs *)
+ | InHyp
+ | InHypTypeOnly
+ | InHypValueOnly
+
+let subst_term_occ_decl ((nowhere_except_in,locs as plocs),hloc) c (id,bodyopt,typ as d) =
+ match bodyopt,hloc with
+ | None, InHypValueOnly -> errorlabstrm "" (pr_id id ++ str " has no value")
+ | None, _ -> (id,None,subst_term_occ plocs c typ)
+ | Some body, InHypTypeOnly -> (id,Some body,subst_term_occ plocs c typ)
+ | Some body, InHypValueOnly -> (id,Some (subst_term_occ plocs c body),typ)
+ | Some body, InHyp ->
if locs = [] then
if nowhere_except_in then d
else (id,Some (subst_term c body),subst_term c typ)
@@ -685,7 +700,6 @@ let subst_term_occ_decl (nowhere_except_in,locs as plocs) c (id,bodyopt,typ as d
if rest <> [] then error_invalid_occurrence rest;
(id,Some body',t')
-
(* First character of a constr *)
let lowercase_first_char id =
@@ -1040,6 +1054,19 @@ let global_vars_set_of_decl env = function
Idset.union (global_vars_set env t)
(global_vars_set env c)
+let dependency_closure env sign hyps =
+ if Idset.is_empty hyps then [] else
+ let (_,lh) =
+ Sign.fold_named_context_reverse
+ (fun (hs,hl) (x,_,_ as d) ->
+ if Idset.mem x hs then
+ (Idset.union (global_vars_set_of_decl env d) (Idset.remove x hs),
+ x::hl)
+ else (hs,hl))
+ ~init:(hyps,[])
+ sign in
+ List.rev lh
+
let default_x = id_of_string "x"
let rec next_name_away_in_cases_pattern id avoid =
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 645b7d72..d44c762e 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 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: termops.mli 11639 2008-11-27 17:48:32Z barras $ i*)
open Util
open Pp
@@ -93,6 +93,7 @@ val strip_head_cast : constr -> constr
exception Occur
val occur_meta : types -> bool
val occur_existential : types -> bool
+val occur_meta_or_existential : types -> bool
val occur_const : constant -> types -> bool
val occur_evar : existential_key -> types -> bool
val occur_in_global : env -> identifier -> constr -> unit
@@ -147,8 +148,15 @@ val subst_term_occ : occurrences -> constr -> constr -> constr
(* [subst_term_occ_decl occl c decl] replaces occurrences of [c] at
positions [occl] by [Rel 1] in [decl] *)
+
+type hyp_location_flag = (* To distinguish body and type of local defs *)
+ | InHyp
+ | InHypTypeOnly
+ | InHypValueOnly
+
val subst_term_occ_decl :
- occurrences -> constr -> named_declaration -> named_declaration
+ occurrences * hyp_location_flag -> constr -> named_declaration ->
+ named_declaration
val error_invalid_occurrence : int list -> 'a
@@ -244,6 +252,10 @@ val make_all_name_different : env -> env
val global_vars : env -> constr -> identifier list
val global_vars_set_of_decl : env -> named_declaration -> Idset.t
+(* Gives an ordered list of hypotheses, closed by dependencies,
+ containing a given set *)
+val dependency_closure : env -> named_context -> Idset.t -> identifier list
+
(* Test if an identifier is the basename of a global reference *)
val is_section_variable : identifier -> bool
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 86168a1f..8680e578 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 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: typeclasses.ml 11576 2008-11-10 19:13:15Z msozeau $ i*)
(*i*)
open Names
@@ -35,25 +35,24 @@ type typeclass = {
cl_impl : global_reference;
(* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
- cl_context : ((global_reference * bool) option * rel_declaration) list;
+ cl_context : (global_reference * bool) option list * rel_context;
(* Context of definitions and properties on defs, will not be shared *)
cl_props : rel_context;
(* The method implementaions as projections. *)
- cl_projs : (identifier * constant) list;
+ cl_projs : (identifier * constant option) list;
}
type typeclasses = (global_reference, typeclass) Gmap.t
-type globality = int option
-
type instance = {
is_class: global_reference;
is_pri: int option;
- is_global: globality;
(* Sections where the instance should be redeclared,
- Some n for n sections, None for discard at end of section. *)
+ -1 for discard, 0 for none, mutable to avoid redeclarations
+ when multiple rebuild_object happen. *)
+ is_global: int ref;
is_impl: constant;
}
@@ -64,13 +63,13 @@ let instance_impl is = is.is_impl
let new_instance cl pri glob impl =
let global =
if Lib.sections_are_opened () then
- if glob then Some (Lib.sections_depth ())
- else None
- else Some 0
+ if glob then Lib.sections_depth ()
+ else -1
+ else 0
in
{ is_class = cl.cl_impl;
is_pri = pri ;
- is_global = global ;
+ is_global = ref global ;
is_impl = impl }
let classes : typeclasses ref = ref Gmap.empty
@@ -112,7 +111,7 @@ let gmap_cmap_merge old ne =
ne Gmap.empty
in
Gmap.fold (fun cl insts acc ->
- if Gmap.mem cl ne' then acc
+ if Gmap.mem cl acc then acc
else Gmap.add cl insts acc)
old ne'
@@ -138,23 +137,21 @@ let subst (_,subst,(cl,m,inst)) =
and do_subst c = Mod_subst.subst_mps subst c
and do_subst_gr gr = fst (subst_global subst gr)
in
- let do_subst_named ctx =
+ let do_subst_ctx ctx =
list_smartmap (fun (na, b, t) ->
(na, Option.smartmap do_subst b, do_subst t))
ctx
in
- let do_subst_ctx ctx =
- list_smartmap (fun (cl, (na, b, t)) ->
- (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b) cl,
- (na, Option.smartmap do_subst b, do_subst t)))
- ctx
+ let do_subst_context (grs,ctx) =
+ list_smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs,
+ do_subst_ctx ctx
in
- let do_subst_projs projs = list_smartmap (fun (x, y) -> (x, do_subst_con y)) projs in
+ let do_subst_projs projs = list_smartmap (fun (x, y) -> (x, Option.smartmap do_subst_con y)) projs in
let subst_class k cl classes =
let k = do_subst_gr k in
let cl' = { cl_impl = k;
- cl_context = do_subst_ctx cl.cl_context;
- cl_props = do_subst_named cl.cl_props;
+ cl_context = do_subst_context cl.cl_context;
+ cl_props = do_subst_ctx cl.cl_props;
cl_projs = do_subst_projs cl.cl_projs; }
in
let cl' = if cl' = cl then cl else cl' in
@@ -173,14 +170,18 @@ let subst (_,subst,(cl,m,inst)) =
let instances = Gmap.fold subst_inst inst Gmap.empty in
(classes, m, instances)
+let rel_of_variable_context ctx =
+ List.fold_right (fun (n,_,b,t) (ctx', subst)->
+ let decl = (Name n, Option.map (substn_vars 1 subst) b, substn_vars 1 subst t) in
+ (decl :: ctx', n :: subst)) ctx ([], [])
+
let discharge (_,(cl,m,inst)) =
- let discharge_context subst rel =
+ let discharge_rel_context subst n rel =
let ctx, _ =
List.fold_right
- (fun (gr, (id, b, t)) (ctx, k) ->
- let gr' = Option.map (fun (gr, b) -> Lib.discharge_global gr, b) gr in
- ((gr', (id, Option.map (substn_vars k subst) b, substn_vars k subst t)) :: ctx), succ k)
- rel ([], 0)
+ (fun (id, b, t) (ctx, k) ->
+ (id, Option.smartmap (substn_vars k subst) b, substn_vars k subst t) :: ctx, succ k)
+ rel ([], n)
in ctx
in
let abs_context cl =
@@ -189,17 +190,22 @@ let discharge (_,(cl,m,inst)) =
| ConstRef cst -> Lib.section_segment_of_constant cst
| IndRef (ind,_) -> Lib.section_segment_of_mutual_inductive ind
in
+ let discharge_context ctx' subst (grs, ctx) =
+ let grs' = List.map (fun _ -> None) subst @
+ list_smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs
+ in grs', discharge_rel_context subst 1 ctx @ ctx'
+ in
let subst_class k cl acc =
let cl_impl' = Lib.discharge_global cl.cl_impl in
let cl' =
if cl_impl' == cl.cl_impl then cl
else
let ctx = abs_context cl in
- { cl with cl_impl = cl_impl';
- cl_context =
- List.map (fun (na,impl,b,t) -> None, (Name na,b,t)) ctx @
- (discharge_context (List.map (fun (na, _, _, _) -> na) ctx) cl.cl_context);
- cl_projs = list_smartmap (fun (x, y) -> x, Lib.discharge_con y) cl.cl_projs }
+ let ctx', subst = rel_of_variable_context ctx in
+ { cl_impl = cl_impl';
+ cl_context = discharge_context ctx' subst cl.cl_context;
+ cl_props = discharge_rel_context subst (succ (List.length (fst cl.cl_context))) cl.cl_props;
+ cl_projs = list_smartmap (fun (x, y) -> x, Option.smartmap Lib.discharge_con y) cl.cl_projs }
in Gmap.add cl_impl' cl' acc
in
let classes = Gmap.fold subst_class cl Gmap.empty in
@@ -220,13 +226,13 @@ let rebuild (cl,m,inst) =
let inst =
Gmap.map (fun insts ->
Cmap.fold (fun k is insts ->
- match is.is_global with
- | None -> insts
- | Some 0 -> Cmap.add k is insts
- | Some n ->
+ match !(is.is_global) with
+ | -1 -> insts
+ | 0 -> Cmap.add k is insts
+ | n ->
add_instance_hint is.is_impl is.is_pri;
- let is' = { is with is_global = Some (pred n) }
- in Cmap.add k is' insts) insts Cmap.empty)
+ is.is_global := pred n;
+ Cmap.add k is insts) insts Cmap.empty)
inst
in (cl, m, inst)
@@ -247,7 +253,10 @@ let update () =
let add_class c =
classes := Gmap.add c.cl_impl c !classes;
- methods := List.fold_left (fun acc x -> Gmap.add (snd x) c.cl_impl acc) !methods c.cl_projs;
+ methods := List.fold_left (fun acc x ->
+ match snd x with
+ | Some m -> Gmap.add m c.cl_impl acc
+ | None -> acc) !methods c.cl_projs;
update ()
let class_info c =
@@ -255,7 +264,7 @@ let class_info c =
with _ -> not_a_class (Global.env()) (constr_of_global c)
let instance_constructor cl args =
- let pars = fst (list_chop (List.length cl.cl_context) args) in
+ let pars = fst (list_chop (List.length (fst cl.cl_context)) args) in
match cl.cl_impl with
| IndRef ind -> applistc (mkConstruct (ind, 1)) args,
applistc (mkInd ind) pars
@@ -319,19 +328,15 @@ let is_implicit_arg k =
| InternalHole -> true
| _ -> false
-let class_of_constr c =
- let extract_cl c =
- try Some (class_info (global_of_constr c)) with _ -> None
- in
- match kind_of_term c with
- App (c, _) -> extract_cl c
- | _ -> extract_cl c
-
-let dest_class_app c =
- let cl c = class_info (global_of_constr c) in
- match kind_of_term c with
- App (c, args) -> cl c, args
- | _ -> cl c, [||]
+let global_class_of_constr env c =
+ try class_info (global_of_constr c)
+ with Not_found -> not_a_class env c
+
+let dest_class_app env c =
+ let cl, args = decompose_app c in
+ global_class_of_constr env cl, args
+
+let class_of_constr c = try Some (fst (dest_class_app (Global.env ()) c)) with _ -> None
(* To embed a boolean for resolvability status.
This is essentially a hack to mark which evars correspond to
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index fdbb78a9..d8e15895 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: typeclasses.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: typeclasses.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
(*i*)
open Names
@@ -25,18 +25,20 @@ open Util
(* This module defines type-classes *)
type typeclass = {
(* The class implementation: a record parameterized by the context with defs in it or a definition if
- the class is a singleton. This acts as the classe's global identifier. *)
+ the class is a singleton. This acts as the class' global identifier. *)
cl_impl : global_reference;
(* Context in which the definitions are typed. Includes both typeclass parameters and superclasses.
- The boolean indicates if the typeclass argument is a direct superclass. *)
- cl_context : ((global_reference * bool) option * rel_declaration) list;
+ The boolean indicates if the typeclass argument is a direct superclass and the global reference
+ gives a direct link to the class itself. *)
+ cl_context : (global_reference * bool) option list * rel_context;
(* Context of definitions and properties on defs, will not be shared *)
cl_props : rel_context;
- (* The methods implementations of the typeclass as projections. *)
- cl_projs : (identifier * constant) list;
+ (* The methods implementations of the typeclass as projections. Some may be undefinable due to
+ sorting restrictions. *)
+ cl_projs : (identifier * constant option) list;
}
type instance
@@ -52,9 +54,13 @@ val add_instance : instance -> unit
val class_info : global_reference -> typeclass (* raises a UserError if not a class *)
-val class_of_constr : constr -> typeclass option
-val dest_class_app : constr -> typeclass * constr array (* raises a UserError if not a class *)
+(* These raise a UserError if not a class. *)
+val dest_class_app : env -> constr -> typeclass * constr list
+
+(* Just return None if not a class *)
+val class_of_constr : constr -> typeclass option
+
val instance_impl : instance -> constant
val is_class : global_reference -> bool
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index b3c920a2..981a5605 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: unification.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: unification.ml 11819 2009-01-20 20:04:50Z herbelin $ *)
open Pp
open Util
@@ -86,18 +86,22 @@ let rec subst_meta_instances bl c =
| Meta i -> (try assoc_pair i bl with Not_found -> c)
| _ -> map_constr (subst_meta_instances bl) c
-let solve_pattern_eqn_array env f l c (metasubst,evarsubst) =
+let solve_pattern_eqn_array (env,nb) sigma f l c (metasubst,evarsubst) =
match kind_of_term f with
| Meta k ->
let c = solve_pattern_eqn env (Array.to_list l) c in
let n = Array.length l - List.length (fst (decompose_lam c)) in
let pb = (ConvUpToEta n,TypeNotProcessed) in
- (k,c,pb)::metasubst,evarsubst
+ if noccur_between 1 nb c then
+ (k,lift (-nb) c,pb)::metasubst,evarsubst
+ else error_cannot_unify_local env sigma (mkApp (f, l),c,c)
| Evar ev ->
(* Currently unused: incompatible with eauto/eassumption backtracking *)
metasubst,(ev,solve_pattern_eqn env (Array.to_list l) c)::evarsubst
| _ -> assert false
+let push d (env,n) = (push_rel_assum d env,n+1)
+
(*******************************)
(* Unification à l'ordre 0 de m et n: [unify_0 env sigma cv_pb m n]
@@ -136,28 +140,47 @@ let default_no_delta_unify_flags = {
modulo_delta = empty_transparent_state;
}
-let expand_constant env flags c =
- match kind_of_term c with
+let expand_key env = function
+ | Some (ConstKey cst) -> constant_opt_value env cst
+ | Some (VarKey id) -> named_body id env
+ | Some (RelKey _) -> None
+ | None -> None
+
+let key_of flags f =
+ match kind_of_term f with
| Const cst when is_transparent (ConstKey cst) &&
- Cpred.mem cst (snd flags.modulo_delta) ->
- constant_opt_value env cst
+ Cpred.mem cst (snd flags.modulo_delta) ->
+ Some (ConstKey cst)
| Var id when is_transparent (VarKey id) &&
- Idpred.mem id (fst flags.modulo_delta) ->
- named_body id env
+ Idpred.mem id (fst flags.modulo_delta) ->
+ Some (VarKey id)
| _ -> None
-
+
+let oracle_order env cf1 cf2 =
+ match cf1 with
+ | None ->
+ (match cf2 with
+ | None -> None
+ | Some k2 -> Some false)
+ | Some k1 ->
+ match cf2 with
+ | None -> Some true
+ | Some k2 -> Some (Conv_oracle.oracle_order k1 k2)
+
let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n =
- let nb = nb_rel env in
- let trivial_unify pb (metasubst,_) m n =
+ let trivial_unify curenv pb (metasubst,_) m n =
let subst = if flags.use_metas_eagerly then metasubst else fst subst in
match subst_defined_metas subst m with
- | Some m ->
- (match flags.modulo_conv_on_closed_terms with
+ | Some m1 ->
+ if (match flags.modulo_conv_on_closed_terms with
Some flags ->
- is_trans_fconv (conv_pb_of pb) flags env sigma m n
- | None -> constr_cmp (conv_pb_of cv_pb) m n)
- | _ -> constr_cmp (conv_pb_of cv_pb) m n in
- let rec unirec_rec curenv pb b ((metasubst,evarsubst) as substn) curm curn =
+ is_trans_fconv (conv_pb_of pb) flags env sigma m1 n
+ | None -> false) then true else
+ if (not (is_ground_term (create_evar_defs sigma) m1))
+ || occur_meta_or_existential n then false else
+ error_cannot_unify curenv sigma (m, n)
+ | _ -> false in
+ let rec unirec_rec (curenv,nb as curenvnb) pb b ((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
@@ -167,41 +190,48 @@ let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n =
then (k1,cN,stN)::metasubst,evarsubst
else if k1 = k2 then substn
else (k2,cM,stM)::metasubst,evarsubst
- | Meta k, _ ->
+ | Meta k, _ when not (dependent cM cN) ->
(* Here we check that [cN] does not contain any local variables *)
- if (closedn nb cN)
- then (k,cN,snd (extract_instance_status pb))::metasubst,evarsubst
+ if nb = 0 then
+ (k,cN,snd (extract_instance_status pb))::metasubst,evarsubst
+ else if noccur_between 1 nb cN then
+ (k,lift (-nb) cN,snd (extract_instance_status pb))::metasubst,
+ evarsubst
else error_cannot_unify_local curenv sigma (m,n,cN)
- | _, Meta k ->
+ | _, Meta k when not (dependent cN cM) ->
(* Here we check that [cM] does not contain any local variables *)
- if (closedn nb cM)
- then (k,cM,fst (extract_instance_status pb))::metasubst,evarsubst
+ if nb = 0 then
+ (k,cM,snd (extract_instance_status pb))::metasubst,evarsubst
+ else if noccur_between 1 nb cM
+ then
+ (k,lift (-nb) cM,fst (extract_instance_status pb))::metasubst,
+ evarsubst
else error_cannot_unify_local curenv sigma (m,n,cM)
| Evar ev, _ -> metasubst,((ev,cN)::evarsubst)
| _, Evar ev -> metasubst,((ev,cM)::evarsubst)
| Lambda (na,t1,c1), Lambda (_,t2,c2) ->
- unirec_rec (push_rel_assum (na,t1) curenv) topconv true
- (unirec_rec curenv topconv true substn t1 t2) c1 c2
+ unirec_rec (push (na,t1) curenvnb) topconv true
+ (unirec_rec curenvnb topconv true substn t1 t2) c1 c2
| Prod (na,t1,c1), Prod (_,t2,c2) ->
- unirec_rec (push_rel_assum (na,t1) curenv) (prod_pb pb) true
- (unirec_rec curenv topconv true substn t1 t2) c1 c2
- | LetIn (_,a,_,c), _ -> unirec_rec curenv pb b substn (subst1 a c) cN
- | _, LetIn (_,a,_,c) -> unirec_rec curenv pb b substn cM (subst1 a c)
+ unirec_rec (push (na,t1) curenvnb) (prod_pb pb) true
+ (unirec_rec curenvnb topconv true substn t1 t2) c1 c2
+ | LetIn (_,a,_,c), _ -> unirec_rec curenvnb pb b substn (subst1 a c) cN
+ | _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb b substn cM (subst1 a c)
| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
- array_fold_left2 (unirec_rec curenv topconv true)
- (unirec_rec curenv topconv true
- (unirec_rec curenv topconv true substn p1 p2) c1 c2) cl1 cl2
+ array_fold_left2 (unirec_rec curenvnb topconv true)
+ (unirec_rec curenvnb topconv true
+ (unirec_rec curenvnb topconv true substn p1 p2) c1 c2) cl1 cl2
| App (f1,l1), _ when
- isMeta f1 & is_unification_pattern curenv f1 l1 &
+ isMeta f1 & is_unification_pattern curenvnb f1 l1 cN &
not (dependent f1 cN) ->
- solve_pattern_eqn_array curenv f1 l1 cN substn
+ solve_pattern_eqn_array curenvnb sigma f1 l1 cN substn
| _, App (f2,l2) when
- isMeta f2 & is_unification_pattern curenv f2 l2 &
+ isMeta f2 & is_unification_pattern curenvnb f2 l2 cM &
not (dependent f2 cM) ->
- solve_pattern_eqn_array curenv f2 l2 cM substn
+ solve_pattern_eqn_array curenvnb sigma f2 l2 cM substn
| App (f1,l1), App (f2,l2) ->
let len1 = Array.length l1
@@ -216,43 +246,66 @@ let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n =
let extras,restl1 = array_chop (len1-len2) l1 in
(appvect (f1,extras), restl1, f2, l2) in
let pb = ConvUnderApp (len1,len2) in
- array_fold_left2 (unirec_rec curenv topconv true)
- (unirec_rec curenv pb true substn f1 f2) l1 l2
+ array_fold_left2 (unirec_rec curenvnb topconv true)
+ (unirec_rec curenvnb pb true substn f1 f2) l1 l2
with ex when precatchable_exception ex ->
- expand curenv pb b substn cM f1 l1 cN f2 l2)
+ expand curenvnb pb b substn cM f1 l1 cN f2 l2)
- | _ ->
+ | _ ->
+ if constr_cmp (conv_pb_of cv_pb) cM cN then substn else
let (f1,l1) =
match kind_of_term cM with App (f,l) -> (f,l) | _ -> (cM,[||]) in
let (f2,l2) =
match kind_of_term cN with App (f,l) -> (f,l) | _ -> (cN,[||]) in
- expand curenv pb b substn cM f1 l1 cN f2 l2
+ expand curenvnb pb b substn cM f1 l1 cN f2 l2
- and expand curenv pb b substn cM f1 l1 cN f2 l2 =
- if trivial_unify pb substn cM cN then substn
+ and expand (curenv,_ as curenvnb) pb b substn cM f1 l1 cN f2 l2 =
+ if trivial_unify curenv pb substn cM cN then substn
else if b then
- match expand_constant curenv flags f1 with
- | Some c ->
- unirec_rec curenv pb b substn (whd_betaiotazeta (mkApp(c,l1))) cN
- | None ->
- match expand_constant curenv flags f2 with
- | Some c ->
- unirec_rec curenv pb b substn cM (whd_betaiotazeta (mkApp(c,l2)))
- | None ->
- error_cannot_unify curenv sigma (cM,cN)
+ let cf1 = key_of flags f1 and cf2 = key_of flags f2 in
+ match oracle_order curenv cf1 cf2 with
+ | None -> error_cannot_unify curenv sigma (cM,cN)
+ | Some true ->
+ (match expand_key curenv cf1 with
+ | Some c ->
+ unirec_rec curenvnb pb b substn (whd_betaiotazeta (mkApp(c,l1))) cN
+ | None ->
+ (match expand_key curenv cf2 with
+ | Some c ->
+ unirec_rec curenvnb pb b substn cM (whd_betaiotazeta (mkApp(c,l2)))
+ | None ->
+ error_cannot_unify curenv sigma (cM,cN)))
+ | Some false ->
+ (match expand_key curenv cf2 with
+ | Some c ->
+ unirec_rec curenvnb pb b substn cM (whd_betaiotazeta (mkApp(c,l2)))
+ | None ->
+ (match expand_key curenv cf1 with
+ | Some c ->
+ unirec_rec curenvnb pb b substn (whd_betaiotazeta (mkApp(c,l1))) cN
+ | None ->
+ error_cannot_unify curenv sigma (cM,cN)))
else
error_cannot_unify curenv sigma (cM,cN)
in
- if (not(occur_meta m)) &&
- (match flags.modulo_conv_on_closed_terms with
+ if (if occur_meta m then false else
+ if (match flags.modulo_conv_on_closed_terms with
Some flags ->
is_trans_fconv (conv_pb_of cv_pb) flags env sigma m n
- | None -> constr_cmp (conv_pb_of cv_pb) m n)
- then
+ | None -> constr_cmp (conv_pb_of cv_pb) m n) then true else
+ if (not (is_ground_term (create_evar_defs sigma) m))
+ || occur_meta_or_existential n then false else
+ if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
+ | Some (cv_id, cv_k), (dl_id, dl_k) ->
+ Idpred.subset dl_id cv_id && Cpred.subset dl_k cv_k
+ | None,(dl_id, dl_k) ->
+ Idpred.is_empty dl_id && Cpred.is_empty dl_k)
+ then error_cannot_unify env sigma (m, n) else false)
+ then
subst
else
- unirec_rec env cv_pb conv_at_top subst m n
+ unirec_rec (env,0) cv_pb conv_at_top subst m n
let unify_0 = unify_0_with_initial_metas ([],[]) true
@@ -428,7 +481,7 @@ let w_coerce_to_type env evd c cty mvty =
try_to_coerce env evd c cty tycon
let w_coerce env evd mv c =
- let cty = get_type_of env (evars_of evd) c in
+ let cty = get_type_of_with_meta env (evars_of evd) (metas_of evd) c in
let mvty = Typing.meta_type evd mv in
w_coerce_to_type env evd c cty mvty
@@ -443,7 +496,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 mvty then
+ if occur_meta_or_existential mvty then
unify_to_type env evd flags c mvty
else ([],[])
@@ -490,9 +543,9 @@ let w_merge env with_types flags (metas,evars) evd =
let evd' = mimick_evar evd flags f (Array.length cl) evn in
w_merge_rec evd' metas evars eqns
| _ ->
- w_merge_rec (solve_simple_evar_eqn env evd ev rhs')
- metas evars' eqns
- end
+ w_merge_rec (solve_simple_evar_eqn env evd ev rhs')
+ metas evars' eqns
+ end
| [] ->
(* Process metas *)
@@ -536,7 +589,7 @@ let w_merge env with_types flags (metas,evars) evd =
let (evd', c) = applyHead sp_env evd nargs hdc in
let (mc,ec) =
unify_0 sp_env (evars_of evd') Cumul flags
- (Retyping.get_type_of sp_env (evars_of evd') c) ev.evar_concl in
+ (Retyping.get_type_of_with_meta sp_env (evars_of evd') (metas_of evd') c) ev.evar_concl in
let evd'' = w_merge_rec evd' mc ec [] in
if (evars_of evd') == (evars_of evd'')
then Evd.evar_define sp c evd''
@@ -559,10 +612,10 @@ let w_unify_meta_types env ?(flags=default_unify_flags) evd =
[clenv_typed_unify M N clenv] expects in addition that expected
types of metavars are unifiable with the types of their instances *)
-let check_types env evd subst m n =
+let check_types env evd flags subst m n =
if isEvar (fst (whd_stack m)) or isEvar (fst (whd_stack n)) then
unify_0_with_initial_metas subst true env (evars_of evd) topconv
- default_unify_flags
+ flags
(Retyping.get_type_of_with_meta env (evars_of evd) (metas_of evd) m)
(Retyping.get_type_of_with_meta env (evars_of evd) (metas_of evd) n)
else
@@ -570,7 +623,7 @@ let check_types env evd subst m n =
let w_unify_core_0 env with_types cv_pb flags m n evd =
let (mc1,evd') = retract_coercible_metas evd in
- let subst1 = check_types env evd (mc1,[]) m n in
+ let subst1 = check_types env evd flags (mc1,[]) m n in
let subst2 =
unify_0_with_initial_metas subst1 true env (evars_of evd') cv_pb flags m n
in
@@ -659,7 +712,7 @@ let w_unify_to_subterm_list env flags allow_K oplist t evd =
if isMeta op then
if allow_K then (evd,op::l)
else error "Match_subterm"
- else if occur_meta op then
+ else if occur_meta_or_existential op then
let (evd',cl) =
try
(* This is up to delta for subterms w/o metas ... *)
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 465c062b..5d09570e 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: vnorm.ml 11017 2008-05-29 13:00:24Z barras $ i*)
+(*i $Id: vnorm.ml 11424 2008-09-30 12:10:28Z jforest $ i*)
open Names
open Declarations
@@ -20,7 +20,7 @@ open Vm
(* Calcul de la forme normal d'un terme *)
(*******************************************)
-let crazy_type = mkSet
+let crazy_type = mkSet
let decompose_prod env t =
let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in
@@ -178,7 +178,7 @@ and nf_stk env c t stk =
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
+ let _,_,codom = try decompose_prod env typ with _ -> exit 120 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
@@ -187,6 +187,7 @@ and nf_stk env c t stk =
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 pT = whd_betadeltaiota env pT 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
@@ -210,7 +211,7 @@ and nf_predicate env ind mip params v pT =
| 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 name,dom,codom = try decompose_prod env pT with _ -> exit 121 in
let dep,body =
nf_predicate (push_rel (name,None,dom) env) ind mip params vb codom in
dep, mkLambda(name,dom,body)
@@ -232,7 +233,7 @@ and nf_args env vargs t =
let args =
Array.init len
(fun i ->
- let _,dom,codom = decompose_prod env !t in
+ let _,dom,codom = try decompose_prod env !t with _ -> exit 123 in
let c = nf_val env (arg vargs i) dom in
t := subst1 c codom; c) in
!t,args
@@ -243,7 +244,7 @@ and nf_bargs env b t =
let args =
Array.init len
(fun i ->
- let _,dom,codom = decompose_prod env !t in
+ let _,dom,codom = try decompose_prod env !t with _ -> exit 124 in
let c = nf_val env (bfield b i) dom in
t := subst1 c codom; c) in
args
@@ -251,7 +252,11 @@ and nf_bargs env b t =
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 name,dom,codom =
+ try decompose_prod env typ
+ with _ ->
+ raise (Type_errors.TypeError(env,Type_errors.ReferenceVariables typ))
+ in
let body = nf_val (push_rel (name,None,dom) env) vb codom in
mkLambda(name,dom,body)
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-29 12:12:24 +0000