From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001
From: Samuel Mimram <samuel.mimram@ens-lyon.org>
Date: Wed, 28 Jul 2004 21:54:47 +0000
Subject: Imported Upstream version 8.0pl1

---
 pretyping/recordops.ml | 176 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 176 insertions(+)
 create mode 100755 pretyping/recordops.ml

(limited to 'pretyping/recordops.ml')

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
new file mode 100755
index 00000000..f34d5624
--- /dev/null
+++ b/pretyping/recordops.ml
@@ -0,0 +1,176 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: recordops.ml,v 1.26.2.1 2004/07/16 19:30:46 herbelin Exp $ *)
+
+open Util
+open Pp
+open Names
+open Libnames
+open Nametab
+open Term
+open Termops
+open Typeops
+open Libobject
+open Library
+open Classops
+
+let nbimpl = ref 0
+let nbpathc = ref 0
+let nbcoer = ref 0
+let nbstruc = ref 0
+let nbimplstruc = ref 0
+
+let compter = ref false
+
+(*s Une structure S est un type inductif non récursif à un seul
+   constructeur (de nom par défaut Build_S) *)
+
+(* Table des structures: le nom de la structure (un [inductive]) donne
+   le nom du constructeur, le nombre de paramètres et pour chaque
+   argument réels du constructeur, le noms de la projection
+   correspondante, si valide *)
+
+type struc_typ = {
+  s_CONST : identifier; 
+  s_PARAM : int;
+  s_PROJ : constant option list }
+
+let structure_table = ref (Indmap.empty : struc_typ Indmap.t)
+let projection_table = ref KNmap.empty
+
+let option_fold_right f p e = match p with Some a -> f a e | None -> e
+
+let cache_structure (_,(ind,struc)) =
+  structure_table := Indmap.add ind struc !structure_table;
+  projection_table := 
+    List.fold_right (option_fold_right (fun proj -> KNmap.add proj struc))
+      struc.s_PROJ !projection_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 {(default_object "STRUCTURE") with 
+                    cache_function = cache_structure;
+		    load_function = (fun _ o -> 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}))
+
+let find_structure indsp = Indmap.find indsp !structure_table
+
+let find_projection_nparams = function
+  | ConstRef cst -> (KNmap.find cst !projection_table).s_PARAM
+  | _ -> raise Not_found
+
+(*s Un "object" est une fonction construisant une instance d'une structure *)
+
+(* Table des definitions "object" : pour chaque object c,
+
+  c := [x1:B1]...[xk:Bk](Build_R a1...am t1...t_n)
+
+  avec ti = (ci ui1...uir)
+
+  Pour tout ci, et Li, la ième projection de la structure R (si
+  définie), on déclare une "coercion"
+
+    o_DEF = c
+    o_TABS = B1...Bk
+    o_PARAMS = a1...am
+    o_TCOMP = ui1...uir
+*)
+
+type obj_typ = {
+  o_DEF : constr;
+  o_TABS : constr list;    (* dans l'ordre *)
+  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 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 (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
+
+let freeze () =
+  !structure_table, !projection_table, !object_table
+
+let unfreeze (s,p,o) = 
+  structure_table := s; projection_table := p; object_table := o
+
+let init () =
+  structure_table := Indmap.empty; projection_table := KNmap.empty;
+  object_table:=[]
+
+let _ = init()
+
+let _ = 
+  Summary.declare_summary "objdefs"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init;
+      Summary.survive_module = false;
+      Summary.survive_section = false }
-- 
cgit v1.2.3