From 72b9a7df489ea47b3e5470741fd39f6100d31676 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Sat, 18 Aug 2007 20:34:57 +0000 Subject: Imported Upstream version 8.1.pl1+dfsg --- pretyping/cases.mli | 12 +++++++++++- pretyping/clenv.ml | 4 ++-- pretyping/detyping.ml | 28 +++++++++++++++++----------- pretyping/detyping.mli | 4 ++-- pretyping/evarconv.ml | 9 ++++----- pretyping/evarutil.ml | 16 +++++++++------- pretyping/evd.ml | 15 +++++++-------- pretyping/evd.mli | 10 +++++----- pretyping/pattern.ml | 4 ++-- pretyping/pretyping.ml | 6 +++--- pretyping/rawterm.ml | 17 +++++++++-------- pretyping/rawterm.mli | 8 ++++---- pretyping/tacred.ml | 4 ++-- 13 files changed, 77 insertions(+), 60 deletions(-) (limited to 'pretyping') diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 9e902126..30f68083 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: cases.mli 8741 2006-04-26 22:30:32Z herbelin $ i*) +(*i $Id: cases.mli 9976 2007-07-12 11:58:30Z msozeau $ i*) (*i*) open Util @@ -32,10 +32,20 @@ type pattern_matching_error = exception PatternMatchingError of env * pattern_matching_error +val raise_pattern_matching_error : (loc * env * pattern_matching_error) -> 'a + val error_wrong_numarg_constructor_loc : loc -> env -> constructor -> int -> 'a val error_wrong_numarg_inductive_loc : loc -> env -> inductive -> int -> 'a +val error_bad_constructor_loc : loc -> constructor -> inductive -> 'a + +val error_bad_pattern_loc : loc -> constructor -> constr -> 'a + +val error_wrong_predicate_arity_loc : loc -> env -> constr -> constr -> constr -> 'a + +val error_needs_inversion : env -> constr -> types -> 'a + (*s Compilation of pattern-matching. *) module type S = sig diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index abe31e06..29dbe83d 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: clenv.ml 9279 2006-10-25 15:51:24Z herbelin $ *) +(* $Id: clenv.ml 9665 2007-02-21 17:08:10Z herbelin $ *) open Pp open Util @@ -54,7 +54,7 @@ let cl_sigma ce = evars_of ce.env let subst_clenv sub clenv = { templval = map_fl (subst_mps sub) clenv.templval; templtyp = map_fl (subst_mps sub) clenv.templtyp; - env = subst_evar_defs sub clenv.env; + env = subst_evar_defs_light sub clenv.env; templenv = clenv.templenv } let clenv_nf_meta clenv c = nf_meta clenv.env c diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index ff435bfc..4a2e5ee3 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: detyping.ml 9535 2007-01-26 09:26:08Z jforest $ *) +(* $Id: detyping.ml 9976 2007-07-12 11:58:30Z msozeau $ *) open Pp open Util @@ -355,12 +355,15 @@ let detype_sort = function (**********************************************************************) (* Main detyping function *) -let rec detype isgoal avoid env t = +let detype_anonymous = ref (fun loc n -> anomaly "detype: index to an anonymous variable") +let set_detype_anonymous f = detype_anonymous := f + +let rec detype (isgoal:bool) avoid env t = match kind_of_term (collapse_appl t) with | Rel n -> (try match lookup_name_of_rel n env with | Name id -> RVar (dl, id) - | Anonymous -> anomaly "detype: index to an anonymous variable" + | Anonymous -> !detype_anonymous dl n with Not_found -> let s = "_UNBOUND_REL_"^(string_of_int n) in RVar (dl, id_of_string s)) @@ -374,8 +377,7 @@ let rec detype isgoal avoid env t = RVar (dl, id)) | Sort s -> RSort (dl,detype_sort s) | Cast (c1,k,c2) -> - RCast(dl,detype isgoal avoid env c1, CastConv k, - detype isgoal avoid env c2) + RCast(dl,detype isgoal avoid env c1, CastConv (k, detype isgoal avoid env c2)) | Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c | Lambda (na,ty,c) -> detype_binder isgoal BLambda avoid env na ty c | LetIn (na,b,_,c) -> detype_binder isgoal BLetIn avoid env na b c @@ -627,14 +629,18 @@ let rec subst_rawconstr subst raw = let ref',_ = subst_global subst ref in if ref' == ref then raw else RHole (loc,InternalHole) - | RHole (loc, (BinderType _ | QuestionMark | CasesType | + | RHole (loc, (BinderType _ | QuestionMark _ | CasesType | InternalHole | TomatchTypeParameter _)) -> raw - | RCast (loc,r1,k,r2) -> - let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in - if r1' == r1 && r2' == r2 then raw else - RCast (loc,r1',k,r2') - + | RCast (loc,r1,k) -> + (match k with + CastConv (k,r2) -> + let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in + if r1' == r1 && r2' == r2 then raw else + RCast (loc,r1', CastConv (k,r2')) + | CastCoerce -> + let r1' = subst_rawconstr subst r1 in + if r1' == r1 then raw else RCast (loc,r1',k)) | RDynamic _ -> raw (* Utilities to transform kernel cases to simple pattern-matching problem *) diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index bbe2fcc9..7ac7162f 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: detyping.mli 8831 2006-05-19 09:29:54Z herbelin $ i*) +(*i $Id: detyping.mli 9976 2007-07-12 11:58:30Z msozeau $ i*) (*i*) open Util @@ -44,7 +44,7 @@ val detype_sort : sorts -> rawsort val lookup_name_as_renamed : env -> constr -> identifier -> int option val lookup_index_as_renamed : env -> constr -> int -> int option - +val set_detype_anonymous : (loc -> int -> rawconstr) -> unit val force_wildcard : unit -> bool val synthetize_type : unit -> bool val force_if : case_info -> bool diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3c4a23ec..2764633b 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarconv.ml 9141 2006-09-15 10:07:01Z herbelin $ *) +(* $Id: evarconv.ml 9665 2007-02-21 17:08:10Z herbelin $ *) open Pp open Util @@ -327,7 +327,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = solve_simple_eqn evar_conv_x env isevars (pbty,ev1,t2) else (* Postpone the use of an heuristic *) - add_conv_pb (pbty,applist(term1,l1),applist(term2,l2)) isevars, + add_conv_pb (pbty,env,applist(term1,l1),applist(term2,l2)) isevars, true | Rigid _, Flexible ev2 -> @@ -342,7 +342,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = solve_simple_eqn evar_conv_x env isevars (pbty,ev2,t1) else (* Postpone the use of an heuristic *) - add_conv_pb (pbty,applist(term1,l1),applist(term2,l2)) isevars, + add_conv_pb (pbty,env,applist(term1,l1),applist(term2,l2)) isevars, true | MaybeFlexible flex1, Rigid _ -> @@ -524,8 +524,7 @@ let first_order_unification env isevars pbty (term1,l1) (term2,l2) = let consider_remaining_unif_problems env isevars = let (isevars,pbs) = get_conv_pbs isevars (fun _ -> true) in List.fold_left - (fun (isevars,b as p) (pbty,t1,t2) -> - (* Pas le bon env pour le problème... *) + (fun (isevars,b as p) (pbty,env,t1,t2) -> if b then first_order_unification env isevars pbty (apprec_nohdbeta env isevars (whd_castappevar (evars_of isevars) t1)) (apprec_nohdbeta env isevars (whd_castappevar (evars_of isevars) t2)) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index b545bd38..6896ca69 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarutil.ml 9573 2007-01-31 20:18:18Z notin $ *) +(* $Id: evarutil.ml 9869 2007-05-29 11:07:04Z herbelin $ *) open Util open Pp @@ -424,6 +424,8 @@ let need_restriction k args = not (array_for_all (closedn k) args) * false. The problem is that we won't get the right error message. *) +exception NotClean of constr + let real_clean env isevars ev evi args rhs = let evd = ref isevars in let subst = List.map (fun (x,y) -> (y,mkVar x)) (list_uniquize args) in @@ -434,7 +436,7 @@ let real_clean env isevars ev evi args rhs = else (* Flex/Rel problem: unifiable as a pattern iff Rel in ev scope *) (try List.assoc (mkRel (i-k)) subst - with Not_found -> if rigid then raise Exit else t) + with Not_found -> if rigid then raise (NotClean t) else t) | Evar (ev,args) -> if Evd.is_defined_evar !evd (ev,args) then subs rigid k (existential_value (evars_of !evd) (ev,args)) @@ -460,7 +462,7 @@ let real_clean env isevars ev evi args rhs = or List.exists (fun (id',_,_) -> id=id') (evar_context evi) *) then t - else raise Exit) + else raise (NotClean t)) | _ -> (* Flex/Rigid problem (or assimilated if not normal): we "imitate" *) @@ -470,8 +472,8 @@ let real_clean env isevars ev evi args rhs = let rhs = whd_beta rhs (* heuristic *) in let body = try subs true 0 rhs - with Exit -> - error_not_clean env (evars_of !evd) ev rhs (evar_source ev !evd) in + with NotClean t -> + error_not_clean env (evars_of !evd) ev t (evar_source ev !evd) in (!evd,body) (* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated @@ -619,7 +621,7 @@ let solve_pattern_eqn env l1 c = * ass. *) -let status_changed lev (pbty,t1,t2) = +let status_changed lev (pbty,_,t1,t2) = try List.mem (head_evar t1) lev or List.mem (head_evar t2) lev with Failure _ -> @@ -678,7 +680,7 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) = evar_define env ev1 t2 isevars in let (isevars,pbs) = get_conv_pbs isevars (status_changed lsp) in List.fold_left - (fun (isevars,b as p) (pbty,t1,t2) -> + (fun (isevars,b as p) (pbty,env,t1,t2) -> if b then conv_algo env isevars pbty t1 t2 else p) (isevars,true) pbs with e when precatchable_exception e -> diff --git a/pretyping/evd.ml b/pretyping/evd.ml index c68a7a73..69d4352f 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evd.ml 9573 2007-01-31 20:18:18Z notin $ *) +(* $Id: evd.ml 9976 2007-07-12 11:58:30Z msozeau $ *) open Pp open Util @@ -358,24 +358,23 @@ let metamap_to_list m = type hole_kind = | ImplicitArg of global_reference * (int * identifier option) | BinderType of name - | QuestionMark + | QuestionMark of bool | CasesType | InternalHole | TomatchTypeParameter of inductive * int type conv_pb = Reduction.conv_pb -type evar_constraint = conv_pb * constr * constr +type evar_constraint = conv_pb * Environ.env * constr * constr type evar_defs = { evars : evar_map; conv_pbs : evar_constraint list; history : (existential_key * (loc * hole_kind)) list; metas : clbinding Metamap.t } -let subst_evar_defs sub evd = +let subst_evar_defs_light sub evd = + assert (evd.evars = (Evarmap.empty,UniverseMap.empty)); + assert (evd.conv_pbs = []); { evd with - conv_pbs = - List.map (fun (k,t1,t2) ->(k,subst_mps sub t1,subst_mps sub t2)) - evd.conv_pbs; metas = Metamap.map (map_clb (subst_mps sub)) evd.metas } let create_evar_defs sigma = @@ -552,7 +551,7 @@ let pr_evar_map sigma = let pr_constraints pbs = h 0 - (prlist_with_sep pr_fnl (fun (pbty,t1,t2) -> + (prlist_with_sep pr_fnl (fun (pbty,_,t1,t2) -> print_constr t1 ++ spc() ++ str (match pbty with | Reduction.CONV -> "==" diff --git a/pretyping/evd.mli b/pretyping/evd.mli index e1fc425b..ef6a3d7b 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: evd.mli 9573 2007-01-31 20:18:18Z notin $ i*) +(*i $Id: evd.mli 9976 2007-07-12 11:58:30Z msozeau $ i*) (*i*) open Util @@ -111,8 +111,8 @@ val map_clb : (constr -> constr) -> clbinding -> clbinding (* Unification state *) type evar_defs -(* Substitution is not applied to the [evar_map] *) -val subst_evar_defs : substitution -> evar_defs -> evar_defs +(* Assume empty [evar_map] and [conv_pbs] *) +val subst_evar_defs_light : substitution -> evar_defs -> evar_defs (* create an [evar_defs] with empty meta map: *) val create_evar_defs : evar_map -> evar_defs @@ -123,7 +123,7 @@ val evars_reset_evd : evar_map -> evar_defs -> evar_defs type hole_kind = | ImplicitArg of global_reference * (int * identifier option) | BinderType of name - | QuestionMark + | QuestionMark of bool (* Can it be turned into an obligation ? *) | CasesType | InternalHole | TomatchTypeParameter of inductive * int @@ -138,7 +138,7 @@ val evar_source : existential_key -> evar_defs -> loc * hole_kind (* Unification constraints *) type conv_pb = Reduction.conv_pb -type evar_constraint = conv_pb * constr * constr +type evar_constraint = conv_pb * Environ.env * constr * constr val add_conv_pb : evar_constraint -> evar_defs -> evar_defs val get_conv_pbs : evar_defs -> (evar_constraint -> bool) -> evar_defs * evar_constraint list diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index eb8a25eb..3060ee03 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pattern.ml 8963 2006-06-19 18:54:49Z barras $ *) +(* $Id: pattern.ml 9976 2007-07-12 11:58:30Z msozeau $ *) open Util open Names @@ -233,7 +233,7 @@ let rec pat_of_raw metas vars = function PSort s | RHole _ -> PMeta None - | RCast (_,c,_,t) -> + | RCast (_,c,_) -> Options.if_verbose Pp.warning "Cast not taken into account in constr pattern"; pat_of_raw metas vars c diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 0b00c82c..0db64a52 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pretyping.ml 9338 2006-11-03 13:09:53Z herbelin $ *) +(* $Id: pretyping.ml 9976 2007-07-12 11:58:30Z msozeau $ *) open Pp open Util @@ -571,13 +571,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct ((fun vtyc env -> pretype vtyc env isevars lvar),isevars) tycon env (* loc *) (po,tml,eqns) - | RCast(loc,c,k,t) -> + | RCast (loc,c,k) -> let cj = match k with CastCoerce -> let cj = pretype empty_tycon env isevars lvar c in evd_comb1 (Coercion.inh_coerce_to_base loc env) isevars cj - | CastConv k -> + | CastConv (k,t) -> let tj = pretype_type empty_valcon env isevars lvar t in let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in (* User Casts are for helping pretyping, experimentally not to be kept*) diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index d7e3ac77..aaf9e63d 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: rawterm.ml 9535 2007-01-26 09:26:08Z jforest $ *) +(* $Id: rawterm.ml 9976 2007-07-12 11:58:30Z msozeau $ *) (*i*) open Util @@ -47,8 +47,8 @@ type 'a bindings = type 'a with_bindings = 'a * 'a bindings -type cast_type = - | CastConv of cast_kind +type 'a cast_type = + | CastConv of cast_kind * 'a | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *) type rawconstr = @@ -68,7 +68,7 @@ type rawconstr = rawconstr array * rawconstr array | RSort of loc * rawsort | RHole of (loc * hole_kind) - | RCast of loc * rawconstr * cast_type * rawconstr + | RCast of loc * rawconstr * rawconstr cast_type | RDynamic of loc * Dyn.t and rawdecl = name * rawconstr option * rawconstr @@ -120,7 +120,7 @@ let map_rawconstr f = function | RRec (loc,fk,idl,bl,tyl,bv) -> RRec (loc,fk,idl,Array.map (List.map (map_rawdecl f)) bl, Array.map f tyl,Array.map f bv) - | RCast (loc,c,k,t) -> RCast (loc,f c,k,f t) + | RCast (loc,c,k) -> RCast (loc,f c, match k with CastConv (k,t) -> CastConv (k, f t) | x -> x) | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> x @@ -190,7 +190,7 @@ let occur_rawconstr id = (na=Name id or not(occur_fix bl)) in occur_fix bl) idl bl tyl bv) - | RCast (loc,c,_,t) -> (occur c) or (occur t) + | RCast (loc,c,k) -> (occur c) or (match k with CastConv (_, t) -> occur t | CastCoerce -> false) | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> false and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c) @@ -247,7 +247,8 @@ let free_rawvars = vars bounded1 vs2 bv.(i) in array_fold_left_i vars_fix vs idl - | RCast (loc,c,_,t) -> vars bounded (vars bounded vs c) t + | RCast (loc,c,k) -> let v = vars bounded vs c in + (match k with CastConv (_,t) -> vars bounded v t | _ -> v) | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> vs and vars_pattern bounded vs (loc,idl,p,c) = @@ -280,7 +281,7 @@ let loc_of_rawconstr = function | RRec (loc,_,_,_,_,_) -> loc | RSort (loc,_) -> loc | RHole (loc,_) -> loc - | RCast (loc,_,_,_) -> loc + | RCast (loc,_,_) -> loc | RDynamic (loc,_) -> loc (**********************************************************************) diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index e5601705..546b36b0 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: rawterm.mli 9535 2007-01-26 09:26:08Z jforest $ i*) +(*i $Id: rawterm.mli 9976 2007-07-12 11:58:30Z msozeau $ i*) (*i*) open Util @@ -51,8 +51,8 @@ type 'a bindings = type 'a with_bindings = 'a * 'a bindings -type cast_type = - | CastConv of cast_kind +type 'a cast_type = + | CastConv of cast_kind * 'a | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *) type rawconstr = @@ -72,7 +72,7 @@ type rawconstr = rawconstr array * rawconstr array | RSort of loc * rawsort | RHole of (loc * Evd.hole_kind) - | RCast of loc * rawconstr * cast_type * rawconstr + | RCast of loc * rawconstr * rawconstr cast_type | RDynamic of loc * Dyn.t and rawdecl = name * rawconstr option * rawconstr diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 006e14b3..92617820 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacred.ml 8793 2006-05-05 17:41:41Z barras $ *) +(* $Id: tacred.ml 9762 2007-04-13 12:46:50Z herbelin $ *) open Pp open Util @@ -365,7 +365,7 @@ let contract_cofix_use_function f (bodynum,(_,names,bodies as typedbodies)) = | Some c -> c in (* match List.nth names j with Name id -> f id | _ -> assert false in*) let subbodies = list_tabulate make_Fi nbodies in - substl subbodies bodies.(bodynum) + substl (List.rev subbodies) bodies.(bodynum) let reduce_mind_case_use_function func env mia = match kind_of_term mia.mconstr with -- cgit v1.2.3