diff options
author | 2012-01-12 16:08:29 +0100 | |
---|---|---|
committer | 2012-01-12 16:08:29 +0100 | |
commit | 23a6061a81ffa0c214d521287b6af0a31bfa22f0 (patch) | |
tree | f1ca9ba9240b98b8695a9f1870e56602734cf97c /pretyping/recordops.ml | |
parent | de109d8c0c68f569b907e6e24271f259ba28888e (diff) | |
parent | 39efc41237ec906226a3a53d7396d51173495204 (diff) |
Merge commit 'upstream/8.4_beta+dfsg' into experimental/master
Diffstat (limited to 'pretyping/recordops.ml')
-rw-r--r-- | pretyping/recordops.ml | 39 |
1 files changed, 25 insertions, 14 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index e8c6073e..b3be7afd 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -1,12 +1,17 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: recordops.ml 14641 2011-11-06 11:59:10Z herbelin $ *) +(* Created by Amokrane Saïbi, Dec 1998 *) +(* Addition of products and sorts in canonical structures by Pierre + Corbineau, Feb 2008 *) + +(* This file registers properties of records: projections and + canonical structures *) open Util open Pp @@ -14,7 +19,6 @@ open Names open Libnames open Nametab open Term -open Termops open Typeops open Libobject open Library @@ -39,6 +43,12 @@ type struc_typ = { let structure_table = ref (Indmap.empty : struc_typ Indmap.t) let projection_table = ref Cmap.empty +(* TODO: could be unify struc_typ and struc_tuple ? in particular, + is the inductive always (fst constructor) ? It seems so... *) + +type struc_tuple = + inductive * constructor * (name * bool) list * constant option list + let load_structure i (_,(ind,id,kl,projs)) = let n = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in let struc = @@ -71,7 +81,7 @@ let discharge_structure (_,(ind,id,kl,projs)) = Some (Lib.discharge_inductive ind, discharge_constructor id, kl, List.map (Option.map Lib.discharge_con) projs) -let (inStruc,outStruc) = +let inStruc : struc_tuple -> obj = declare_object {(default_object "STRUCTURE") with cache_function = cache_structure; load_function = load_structure; @@ -130,7 +140,7 @@ open Libobject let load_method (_,(ty,id)) = meth_dnet := MethodsDnet.add ty id !meth_dnet -let (in_method,out_method) = +let in_method : constr * MethodsDnet.ident -> obj = declare_object { (default_object "RECMETHODS") with load_function = (fun _ -> load_method); @@ -201,7 +211,7 @@ let cs_pattern_of_constr t = _ -> raise Not_found end | Rel n -> Default_cs, pred n, [] - | Prod (_,a,b) when not (dependent (mkRel 1) b) -> Prod_cs, -1, [a;pop b] + | Prod (_,a,b) when not (Termops.dependent (mkRel 1) b) -> Prod_cs, -1, [a; Termops.pop b] | Sort s -> Sort_cs (family_of_sort s), -1, [] | _ -> begin @@ -235,7 +245,7 @@ let compute_canonical_projections (con,ind) = (let con_pp = Nametab.pr_global_env Idset.empty (ConstRef con) and proji_sp_pp = Nametab.pr_global_env Idset.empty (ConstRef proji_sp) in msg_warning (str "No global reference exists for projection value" - ++ print_constr t ++ str " in instance " + ++ Termops.print_constr t ++ str " in instance " ++ con_pp ++ str " of " ++ proji_sp_pp ++ str ", ignoring it.")); l end @@ -285,7 +295,7 @@ let subst_canonical_structure (subst,(cst,ind as obj)) = let discharge_canonical_structure (_,(cst,ind)) = Some (Lib.discharge_con cst,Lib.discharge_inductive ind) -let (inCanonStruc,outCanonStruct) = +let inCanonStruc : constant * inductive -> obj = declare_object {(default_object "CANONICAL-STRUCTURE") with open_function = open_canonical_structure; cache_function = cache_canonical_structure; @@ -323,16 +333,17 @@ let check_and_decompose_canonical_structure ref = let declare_canonical_structure ref = add_canonical_structure (check_and_decompose_canonical_structure ref) -let outCanonicalStructure x = fst (outCanonStruct x) - let lookup_canonical_conversion (proj,pat) = List.assoc pat (Refmap.find proj !object_table) -let is_open_canonical_projection sigma (c,args) = +let is_open_canonical_projection env sigma (c,args) = try - let l = Refmap.find (global_of_constr c) !object_table in - let n = (snd (List.hd l)).o_NPARAMS in - try isEvar_or_Meta (whd_evar sigma (List.nth args n)) with Failure _ -> false + let n = find_projection_nparams (global_of_constr c) in + try + let arg = whd_betadeltaiota env sigma (List.nth args n) in + let hd = match kind_of_term arg with App (hd, _) -> hd | _ -> arg in + not (isConstruct hd) + with Failure _ -> false with Not_found -> false let freeze () = |