From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 14 Oct 2010 17:51:11 +0200 Subject: Imported Upstream version 8.3 --- pretyping/cases.ml | 34 ++++++++++++++-------------------- pretyping/pretyping.ml | 9 +++++++-- pretyping/recordops.mli | 3 +-- 3 files changed, 22 insertions(+), 24 deletions(-) (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 9027315e..09603d8b 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cases.ml 13329 2010-07-26 11:05:39Z herbelin $ *) +(* $Id: cases.ml 13511 2010-10-06 20:48:16Z herbelin $ *) open Util open Names @@ -1089,12 +1089,6 @@ let build_branch current deps (realnames,dep) pb arsign eqns const_info = let names = get_names pb.env cs_args eqns in let submat = List.map (fun (tms,eqn) -> prepend_pattern tms eqn) eqns in let typs = List.map2 (fun (_,c,t) na -> (na,c,t)) cs_args names in - let _,typs',_ = - List.fold_right - (fun (na,c,t as d) (env,typs,tms) -> - let tms = List.map List.tl tms in - (push_rel d env, (na,NotInd(c,t))::typs,tms)) - typs (pb.env,[],List.map fst eqns) in let dep_sign = find_dependencies_signature @@ -1114,9 +1108,10 @@ let build_branch current deps (realnames,dep) pb arsign eqns const_info = let pred_is_not_dep = noccur_predicate_between 1 (List.length realnames + 1) pb.pred tomatch in - let typs'' = + let typs' = list_map2_i - (fun i (na,t) deps -> + (fun i d deps -> + let (na,c,t) = map_rel_declaration (lift i) d in let dep = match dep with | Name _ as na',k -> (if na <> Anonymous then na else na'),k | Anonymous,KnownNotDep -> @@ -1125,15 +1120,13 @@ let build_branch current deps (realnames,dep) pb arsign eqns const_info = else (force_name na,KnownDep) | _,_ -> anomaly "Inconsistent dependency" in - ((mkRel i, lift_tomatch_type i t),deps,dep)) - 1 typs' (List.rev dep_sign) in + ((mkRel i, NotInd (c,t)),deps,dep)) + 1 typs (List.rev dep_sign) in let pred = - specialize_predicate typs'' (realnames,dep) arsign const_info tomatch pb.pred in - - let currents = List.map (fun x -> Pushed x) typs'' in + specialize_predicate typs' (realnames,dep) arsign const_info tomatch pb.pred in - let sign = List.map (fun (na,t) -> mkDeclTomatch na t) typs' in + let currents = List.map (fun x -> Pushed x) typs' in let ind = appvect ( @@ -1141,7 +1134,7 @@ let build_branch current deps (realnames,dep) pb arsign eqns const_info = List.map (lift const_info.cs_nargs) const_info.cs_params), const_info.cs_concl_realargs) in - let cur_alias = lift (List.length sign) current in + let cur_alias = lift (List.length typs) current in let currents = Alias (ci,cur_alias,alias_type,ind) :: currents in let tomatch = List.rev_append currents tomatch in @@ -1150,13 +1143,13 @@ let build_branch current deps (realnames,dep) pb arsign eqns const_info = raise_pattern_matching_error (dummy_loc, pb.env, NonExhaustive (complete_history history)); - sign, + typs, { pb with - env = push_rels sign pb.env; + env = push_rels typs pb.env; tomatch = tomatch; pred = pred; history = history; - mat = List.map (push_rels_eqn_with_names sign) submat } + mat = List.map (push_rels_eqn_with_names typs) submat } (********************************************************************** INVARIANT: @@ -1597,7 +1590,7 @@ let prepare_predicate_from_arsign_tycon loc tomatchs sign arsign c = | Rel n when signlen > 1 (* The term is of a dependent type, maybe some variable in its type appears in the tycon. *) -> (match tmtype with - NotInd _ -> (* len - signlen, subst*) assert false (* signlen > 1 *) + NotInd _ -> (subst, len - signlen) | IsInd (_, IndType(indf,realargs),_) -> let subst = if dependent tm c && List.for_all isRel realargs @@ -1707,6 +1700,7 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e (* We push the initial terms to match and push their alias to rhs' envs *) (* names of aliases will be recovered from patterns (hence Anonymous *) (* here) *) + let initial_pushed = List.map2 (fun tm na -> Pushed(tm,[],na)) tomatchs nal in (* A typing function that provides with a canonical term for absurd cases*) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 7b4b5e07..1c17ff88 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pretyping.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: pretyping.ml 13408 2010-09-11 19:19:04Z herbelin $ *) open Pp open Util @@ -235,6 +235,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct str " depends on pattern variable name " ++ pr_id id ++ str " which is not bound in current context.") + let protected_get_type_of env sigma c = + try Retyping.get_type_of env sigma c + with Anomaly _ -> + errorlabstrm "" (str "Cannot reinterpret " ++ quote (print_constr c) ++ str " in the current environment.") + let pretype_id loc env sigma (lvar,unbndltacvars) id = try let (n,_,typ) = lookup_rel_id id (rel_context env) in @@ -244,7 +249,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let (ids,c) = List.assoc id lvar in let subst = List.map (invert_ltac_bound_name env id) ids in let c = substl subst c in - { uj_val = c; uj_type = Retyping.get_type_of env sigma c } + { uj_val = c; uj_type = protected_get_type_of env sigma c } with Not_found -> try let (_,_,typ) = lookup_named id env in diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 3d97d8b2..78626854 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -6,14 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: recordops.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: recordops.mli 13447 2010-09-21 13:23:45Z letouzey $ i*) (*i*) open Names open Nametab open Term open Libnames -open Classops open Libobject open Library (*i*) -- cgit v1.2.3