From de0085539583f59dc7c4bf4e272e18711d565466 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Thu, 13 Jul 2006 14:28:31 +0000 Subject: Imported Upstream version 8.0pl3+8.1beta.2 --- pretyping/pattern.ml | 4 ++-- pretyping/pattern.mli | 4 ++-- pretyping/pretyping.ml | 3 ++- pretyping/rawterm.ml | 4 ++-- pretyping/rawterm.mli | 4 ++-- pretyping/recordops.ml | 15 +++++++++------ pretyping/recordops.mli | 15 +++++---------- 7 files changed, 24 insertions(+), 25 deletions(-) (limited to 'pretyping') diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index ef97250a..eb8a25eb 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pattern.ml 8755 2006-04-27 22:22:15Z herbelin $ *) +(* $Id: pattern.ml 8963 2006-06-19 18:54:49Z barras $ *) open Util open Names @@ -132,7 +132,7 @@ let map_pattern_with_binders g f l = function let map_pattern f = map_pattern_with_binders (fun () -> ()) (fun () -> f) () let rec instantiate_pattern lvar = function - | PVar id as x -> (try List.assoc id lvar with Not_found -> x) + | PVar id as x -> (try Lazy.force(List.assoc id lvar) with Not_found -> x) | (PFix _ | PCoFix _) -> error ("Not instantiable pattern") | c -> map_pattern (instantiate_pattern lvar) c diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index 1637fc5f..4102db9e 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pattern.mli 8755 2006-04-27 22:22:15Z herbelin $ i*) +(*i $Id: pattern.mli 8963 2006-06-19 18:54:49Z barras $ i*) (*i*) open Pp @@ -76,6 +76,6 @@ val pattern_of_rawconstr : rawconstr -> patvar list * constr_pattern val instantiate_pattern : - (identifier * constr_pattern) list -> constr_pattern -> constr_pattern + (identifier * constr_pattern Lazy.t) list -> constr_pattern -> constr_pattern val lift_pattern : int -> constr_pattern -> constr_pattern diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index ca797f97..e3cfe974 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pretyping.ml 8875 2006-05-29 19:59:11Z msozeau $ *) +(* $Id: pretyping.ml 8992 2006-06-27 21:29:18Z herbelin $ *) open Pp open Util @@ -482,6 +482,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct else error_cant_find_case_type_loc loc env (evars_of !isevars) cj.uj_val in + let ccl = refresh_universes ccl in let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in let v = let mis,_ = dest_ind_family indf in diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index e61bf2c3..ece536d1 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: rawterm.ml 8878 2006-05-30 16:44:25Z herbelin $ *) +(* $Id: rawterm.ml 8969 2006-06-22 12:51:04Z msozeau $ *) (*i*) open Util @@ -73,7 +73,7 @@ type rawconstr = and rawdecl = name * rawconstr option * rawconstr -and fix_recursion_order = RStructRec | RWfRec of rawconstr +and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr and fix_kind = | RFix of ((int option * fix_recursion_order) array * int) diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index b29cc7b6..89b13ff0 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 8878 2006-05-30 16:44:25Z herbelin $ i*) +(*i $Id: rawterm.mli 8969 2006-06-22 12:51:04Z msozeau $ i*) (*i*) open Util @@ -70,7 +70,7 @@ type rawconstr = and rawdecl = name * rawconstr option * rawconstr -and fix_recursion_order = RStructRec | RWfRec of rawconstr +and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr and fix_kind = | RFix of ((int option * fix_recursion_order) array * int) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 5d38f52c..74df5eea 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: recordops.ml 8752 2006-04-27 19:37:33Z herbelin $ *) +(* $Id: recordops.ml 9032 2006-07-07 16:30:34Z herbelin $ *) open Util open Pp @@ -32,7 +32,7 @@ open Mod_subst type struc_typ = { s_CONST : identifier; - s_PARAM : int; + s_EXPECTEDPARAM : int; s_PROJKIND : bool list; s_PROJ : constant option list } @@ -44,7 +44,7 @@ let option_fold_right f p e = match p with Some a -> f a e | None -> e let load_structure i (_,(ind,id,kl,projs)) = let n = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in let struc = - { s_CONST = id; s_PARAM = n; s_PROJ = projs; s_PROJKIND = kl } in + { s_CONST = id; s_EXPECTEDPARAM = n; s_PROJ = projs; s_PROJKIND = kl } in structure_table := Indmap.add ind struc !structure_table; projection_table := List.fold_right (option_fold_right (fun proj -> Cmap.add proj struc)) @@ -83,8 +83,10 @@ let declare_structure (s,c,_,kl,pl) = let lookup_structure indsp = Indmap.find indsp !structure_table +let lookup_projections indsp = (lookup_structure indsp).s_PROJ + let find_projection_nparams = function - | ConstRef cst -> (Cmap.find cst !projection_table).s_PARAM + | ConstRef cst -> (Cmap.find cst !projection_table).s_EXPECTEDPARAM | _ -> raise Not_found @@ -134,7 +136,7 @@ let compute_canonical_projections (con,ind) = let lt,t = Reductionops.splay_lambda (Global.env()) Evd.empty c in let lt = List.rev (List.map snd lt) in let args = snd (decompose_app t) in - let { s_PARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in + let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in let params, projs = list_chop p args in let lpj = keep_true_projections lpj kl in let lps = List.combine lpj projs in @@ -202,7 +204,8 @@ 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 - if s.s_PARAM + List.length s.s_PROJ > Array.length args then + 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 1e061dc6..91bc2ba1 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 6748 2005-02-18 22:17:50Z herbelin $ i*) +(*i $Id: recordops.mli 9032 2006-07-07 16:30:34Z herbelin $ i*) (*i*) open Names @@ -21,18 +21,13 @@ 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 : identifier; - s_PARAM : int; - s_PROJKIND : bool list; - s_PROJ : constant option list } - val declare_structure : inductive * identifier * int * bool list * constant option list -> unit -(* [lookup_structure isp] returns the infos associated to inductive path - [isp] if it corresponds to a structure, otherwise fails with [Not_found] *) -val lookup_structure : inductive -> struc_typ +(* [lookup_projections isp] returns the projections associated to the + inductive path [isp] if it corresponds to a structure, otherwise + it fails with [Not_found] *) +val lookup_projections : inductive -> constant option list (* raise [Not_found] if not a projection *) val find_projection_nparams : global_reference -> int -- cgit v1.2.3