diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 2 | ||||
| -rwxr-xr-x | pretyping/recordops.ml | 66 | ||||
| -rwxr-xr-x | pretyping/recordops.mli | 13 |
3 files changed, 33 insertions, 48 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 93d9ba9064..35e17a07ba 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -113,7 +113,7 @@ let check_conv_record (t1,l1) (t2,l2) = let proji = reference_of_constr t1 in let cstr = reference_of_constr t2 in let { o_DEF = c; o_TABS = bs; o_TPARAMS = params; o_TCOMPS = us } = - objdef_info (proji, cstr) in + canonical_structure_info (proji, cstr) in let params1, c1, extra_args1 = match list_chop (List.length params) l1 with | params1, c1::extra_args1 -> params1, c1, extra_args1 diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 64d99d49fb..4cbd02ca4d 100755 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -114,50 +114,36 @@ let subst_obj subst obj = let object_table = (ref [] : ((global_reference * global_reference) * obj_typ) list ref) -let cache_object (_,x) = object_table := x :: (!object_table) +let cache_canonical_structure (_,(cst,lo)) = + List.iter (fun (o,_ as x) -> + if not (List.mem_assoc o !object_table) then + object_table := x :: (!object_table)) lo -let subst_object (_,subst,((r1,r2),o as obj)) = +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 - let _ = List.assoc o !object_table in () - with Not_found -> - Lib.add_anonymous_leaf - (inObjDef (o,{o_DEF=c;o_TABS=la;o_TPARAMS=lp;o_TCOMPS=l})) - -let cache_objdef1 (_,sp) = () - -let (inObjDef10,outObjDef10) = - 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 outObjDef1 obj = constant_of_kn (outObjDef10 obj) - -let inObjDef1 con = - (*CSC: Here I am cheating by violating the fact that "constant" is an ADT - and this is the only place in the whole Coq code. My feeling is that the - implementation of "Canonical Structure"s should be improved to avoid this - situation (that is avoided for all the other non-logical objects). *) - let mp,sp,l = repr_con con in - let kn = make_kn mp sp l in - inObjDef10 kn - -let objdef_info o = List.assoc o !object_table + if r1' == r1 && r2' == r2 && o' == o then obj + else (r1',r2'),o' + +let subst_canonical_structure (_,subst,(cst,lo as obj)) = + let cst' = subst_con subst cst in + let lo' = list_smartmap (subst_object subst) lo in + if cst' == cst & lo' == lo then obj else (cst',lo') + +let (inCanonStruc,outCanonStruct) = + declare_object {(default_object "CANONICAL-STRUCTURE") with + open_function = (fun i o -> if i=1 then cache_canonical_structure o); + cache_function = cache_canonical_structure; + subst_function = subst_canonical_structure; + classify_function = (fun (_,x) -> Substitute x); + export_function = (function x -> Some x) } + +let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x) + +let outCanonicalStructure x = fst (outCanonStruct x) + +let canonical_structure_info o = List.assoc o !object_table let freeze () = !structure_table, !projection_table, !object_table diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 949dc4e80d..128018d581 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -39,13 +39,12 @@ type obj_typ = { o_TPARAMS : constr list; (* dans l'ordre *) o_TCOMPS : constr list } (* dans l'ordre *) -val objdef_info : (global_reference * global_reference) -> obj_typ -val add_new_objdef : - (global_reference * global_reference) * Term.constr * Term.constr list * - Term.constr list * Term.constr list -> unit - +val canonical_structure_info : + (global_reference * global_reference) -> obj_typ +val add_canonical_structure : + constant * ((global_reference * global_reference) * obj_typ) list -> unit val inStruc : inductive * struc_typ -> obj val outStruc : obj -> inductive * struc_typ -val inObjDef1 : constant -> obj -val outObjDef1 : obj -> constant + +val outCanonicalStructure : obj -> constant |