diff options
author | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-08-02 17:17:42 +0000 |
---|---|---|
committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-08-02 17:17:42 +0000 |
commit | 12965209478bd99dfbe57f07d5b525e51b903f22 (patch) | |
tree | 36a7f5e4802cd321caf02fed0be8349100be09fb /pretyping/recordops.ml | |
parent | 8b26fd6ba739d4f49fae99ed764b086022e44b50 (diff) |
Modules dans COQ\!\!\!\!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/recordops.ml')
-rwxr-xr-x | pretyping/recordops.ml | 75 |
1 files changed, 52 insertions, 23 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 6617a7a9b..e2d4036f4 100755 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -11,6 +11,7 @@ open Util open Pp open Names +open Libnames open Nametab open Term open Termops @@ -44,14 +45,22 @@ let structure_table = (ref [] : (inductive * struc_typ) list ref) let cache_structure (_,x) = structure_table := x :: (!structure_table) +let subst_structure (_,subst,((kn,i),struc as obj)) = + let kn' = subst_kn subst kn in + let proj' = list_smartmap + (option_smartmap (subst_kn subst)) + struc.s_PROJ + in + if proj' == struc.s_PROJ && kn' == kn then obj else + (kn',i),{struc with s_PROJ = proj'} + let (inStruc,outStruc) = - declare_object - ("STRUCTURE", { - load_function = (fun _ -> ()); - cache_function = cache_structure; - open_function = cache_structure; - export_function = (function x -> Some x) - }) + declare_object {(default_object "STRUCTURE") with + cache_function = cache_structure; + open_function = (fun i o -> if i=1 then cache_structure o); + subst_function = subst_structure; + classify_function = (fun (_,x) -> Substitute x); + export_function = (function x -> Some x) } let add_new_struc (s,c,n,l) = Lib.add_anonymous_leaf (inStruc (s,{s_CONST=c;s_PARAM=n;s_PROJ=l})) @@ -81,19 +90,42 @@ type obj_typ = { o_TPARAMS : constr list; (* dans l'ordre *) o_TCOMPS : constr list } (* dans l'ordre *) +let subst_obj subst obj = + let o_DEF' = subst_mps subst obj.o_DEF in + let o_TABS' = list_smartmap (subst_mps subst) obj.o_TABS in + let o_TPARAMS' = list_smartmap (subst_mps subst) obj.o_TPARAMS in + let o_TCOMPS' = list_smartmap (subst_mps subst) obj.o_TCOMPS in + if o_DEF' == obj.o_DEF + && o_TABS' == obj.o_TABS + && o_TPARAMS' == obj.o_TPARAMS + && o_TCOMPS' == obj.o_TCOMPS + then + obj + else + { o_DEF = o_DEF' ; + o_TABS = o_TABS' ; + o_TPARAMS = o_TPARAMS' ; + o_TCOMPS = o_TCOMPS' } + let object_table = (ref [] : ((global_reference * global_reference) * obj_typ) list ref) let cache_object (_,x) = object_table := x :: (!object_table) -let (inObjDef, outObjDef) = - declare_object - ("OBJDEF", { - load_function = (fun _ -> ()); - open_function = cache_object; - cache_function = cache_object; - export_function = (function x -> Some x) - }) +let subst_object (_,subst,((r1,r2),o as obj)) = + let r1' = subst_global subst r1 in + let r2' = subst_global subst r2 in + let o' = subst_obj subst o in + if r1' == r1 && r2' == r2 && o' == o then obj else + (r1',r2'),o' + +let (inObjDef,outObjDef) = + declare_object {(default_object "OBJDEF") with + open_function = (fun i o -> if i=1 then cache_object o); + cache_function = cache_object; + subst_function = subst_object; + classify_function = (fun (_,x) -> Substitute x); + export_function = (function x -> Some x) } let add_new_objdef (o,c,la,lp,l) = try @@ -104,14 +136,11 @@ let add_new_objdef (o,c,la,lp,l) = let cache_objdef1 (_,sp) = () -let (inObjDef1, outObjDef1) = - declare_object - ("OBJDEF1", { - load_function = (fun _ -> ()); - open_function = cache_objdef1; - cache_function = cache_objdef1; - export_function = (function x -> Some x) - }) +let (inObjDef1,outObjDef1) = + declare_object {(default_object "OBJDEF1") with + open_function = (fun i o -> if i=1 then cache_objdef1 o); + cache_function = cache_objdef1; + export_function = (function x -> Some x) } let objdef_info o = List.assoc o !object_table |