modules Bij, Gmapl, Stock

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@125 85f007b7-540e-0410-9357-904b9bb8a0f7

13 files changed, 322 insertions, 10 deletions

diff --git a/.depend b/.depend
index 1514e5b42..d3dd8367f 100644
--- a/.depend
+++ b/.depend
@@ -29,6 +29,7 @@ kernel/typing.cmi: kernel/constant.cmi kernel/environ.cmi \
     kernel/inductive.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \
     kernel/term.cmi kernel/typeops.cmi kernel/univ.cmi 
 kernel/univ.cmi: kernel/names.cmi lib/pp.cmi 
+lib/gmapl.cmi: lib/gmap.cmi 
 lib/pp.cmi: lib/pp_control.cmi 
 lib/util.cmi: lib/pp.cmi 
 library/declare.cmi: kernel/constant.cmi kernel/inductive.cmi \
@@ -39,6 +40,7 @@ library/global.cmi: kernel/constant.cmi kernel/environ.cmi \
 library/impargs.cmi: kernel/names.cmi 
 library/lib.cmi: library/libobject.cmi kernel/names.cmi library/summary.cmi 
 library/libobject.cmi: kernel/names.cmi 
+library/library.cmi: lib/pp.cmi 
 library/nametab.cmi: kernel/names.cmi 
 library/redinfo.cmi: kernel/names.cmi kernel/term.cmi 
 library/summary.cmi: kernel/names.cmi 
@@ -79,6 +81,7 @@ tactics/btermdn.cmi: kernel/generic.cmi kernel/term.cmi
 tactics/dn.cmi: lib/tlm.cmi 
 tactics/nbtermdn.cmi: tactics/btermdn.cmi kernel/generic.cmi kernel/term.cmi \
     tactics/termdn.cmi 
+tactics/stock.cmi: kernel/names.cmi 
 tactics/termdn.cmi: tactics/dn.cmi kernel/generic.cmi kernel/term.cmi 
 toplevel/errors.cmi: parsing/coqast.cmi lib/pp.cmi 
 toplevel/himsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
@@ -185,6 +188,8 @@ kernel/typing.cmx: kernel/constant.cmx kernel/environ.cmx kernel/evd.cmx \
     lib/util.cmx kernel/typing.cmi 
 kernel/univ.cmo: kernel/names.cmi lib/pp.cmi lib/util.cmi kernel/univ.cmi 
 kernel/univ.cmx: kernel/names.cmx lib/pp.cmx lib/util.cmx kernel/univ.cmi 
+lib/bij.cmo: lib/gmap.cmi lib/bij.cmi 
+lib/bij.cmx: lib/gmap.cmx lib/bij.cmi 
 lib/bstack.cmo: lib/util.cmi lib/bstack.cmi 
 lib/bstack.cmx: lib/util.cmx lib/bstack.cmi 
 lib/dyn.cmo: lib/util.cmi lib/dyn.cmi 
@@ -193,6 +198,8 @@ lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi
 lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi 
 lib/gmap.cmo: lib/gmap.cmi 
 lib/gmap.cmx: lib/gmap.cmi 
+lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi 
+lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi 
 lib/gset.cmo: lib/gset.cmi 
 lib/gset.cmx: lib/gset.cmi 
 lib/hashcons.cmo: lib/hashcons.cmi 
@@ -240,11 +247,11 @@ library/libobject.cmo: lib/dyn.cmi kernel/names.cmi lib/util.cmi \
 library/libobject.cmx: lib/dyn.cmx kernel/names.cmx lib/util.cmx \
     library/libobject.cmi 
 library/library.cmo: kernel/environ.cmi library/global.cmi library/lib.cmi \
-    library/libobject.cmi kernel/names.cmi lib/system.cmi lib/util.cmi \
-    library/library.cmi 
+    library/libobject.cmi kernel/names.cmi lib/pp.cmi lib/system.cmi \
+    lib/util.cmi library/library.cmi 
 library/library.cmx: kernel/environ.cmx library/global.cmx library/lib.cmx \
-    library/libobject.cmx kernel/names.cmx lib/system.cmx lib/util.cmx \
-    library/library.cmi 
+    library/libobject.cmx kernel/names.cmx lib/pp.cmx lib/system.cmx \
+    lib/util.cmx library/library.cmi 
 library/nametab.cmo: kernel/names.cmi library/summary.cmi library/nametab.cmi 
 library/nametab.cmx: kernel/names.cmx library/summary.cmx library/nametab.cmi 
 library/redinfo.cmo: kernel/constant.cmi kernel/evd.cmi kernel/generic.cmi \
@@ -377,6 +384,10 @@ tactics/nbtermdn.cmo: tactics/btermdn.cmi kernel/generic.cmi lib/gmap.cmi \
 tactics/nbtermdn.cmx: tactics/btermdn.cmx kernel/generic.cmx lib/gmap.cmx \
     library/libobject.cmx library/library.cmx kernel/names.cmx \
     kernel/term.cmx tactics/termdn.cmx lib/util.cmx tactics/nbtermdn.cmi 
+tactics/stock.cmo: lib/bij.cmi lib/gmap.cmi lib/gmapl.cmi library/library.cmi \
+    kernel/names.cmi lib/pp.cmi lib/util.cmi tactics/stock.cmi 
+tactics/stock.cmx: lib/bij.cmx lib/gmap.cmx lib/gmapl.cmx library/library.cmx \
+    kernel/names.cmx lib/pp.cmx lib/util.cmx tactics/stock.cmi 
 tactics/termdn.cmo: tactics/dn.cmi kernel/generic.cmi kernel/term.cmi \
     lib/util.cmi tactics/termdn.cmi 
 tactics/termdn.cmx: tactics/dn.cmx kernel/generic.cmx kernel/term.cmx \
diff --git a/Makefile b/Makefile
index 0175de1c3..833b2b9cd 100644
--- a/Makefile
+++ b/Makefile
@@ -34,7 +34,7 @@ CONFIG=config/coq_config.cmo
 LIB=lib/pp_control.cmo lib/pp.cmo lib/util.cmo \
     lib/hashcons.cmo lib/dyn.cmo lib/system.cmo lib/options.cmo \
     lib/bstack.cmo lib/edit.cmo lib/stamps.cmo lib/gset.cmo lib/gmap.cmo \
-    lib/tlm.cmo
+    lib/tlm.cmo lib/bij.cmo lib/gmapl.cmo
 
 KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \
        kernel/sign.cmo kernel/constant.cmo \
@@ -55,7 +55,7 @@ PROOFS=proofs/typing_ev.cmo proofs/tacred.cmo \
        proofs/macros.cmo proofs/tacinterp.cmo # proofs/clenv.cmo
 
 TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \
-        tactics/nbtermdn.cmo
+        tactics/nbtermdn.cmo tactics/stock.cmo
 
 PRETYPING=pretyping/astterm.cmo
 
diff --git a/dev/changements.txt b/dev/changements.txt
index 543b0fa69..427ac393e 100644
--- a/dev/changements.txt
+++ b/dev/changements.txt
@@ -8,6 +8,7 @@ Changements d'organisation / modules :
     (les parties noms et signatures ont été séparées)
 
   Avm,Mavm,Fmavm,Mhm  ->  utiliser plutôt Map (et freeze alors gratuit)
+  Mhb                 ->  Bij
 
 
 Changements dans les types de données :
diff --git a/lib/bij.ml b/lib/bij.ml
new file mode 100644
index 000000000..cd0acbabb
--- /dev/null
+++ b/lib/bij.ml
@@ -0,0 +1,35 @@
+
+(* $Id$ *)
+
+type ('a,'b) t = { 
+  f : ('a,'b) Gmap.t;
+  finv : ('b,'a) Gmap.t }
+
+let empty = { f = Gmap.empty; finv = Gmap.empty }
+
+let map b x = Gmap.find x b.f
+
+let pam b y = Gmap.find y b.finv
+
+let dom b = Gmap.dom b.f
+
+let rng b = Gmap.dom b.finv
+
+let in_dom b x = Gmap.mem x b.f
+
+let in_rng b y = Gmap.mem y b.finv
+
+let add b (x,y) =
+  if in_dom b x || in_rng b y then failwith "Bij.add";
+  { f = Gmap.add x y b.f;
+    finv = Gmap.add y x b.finv }
+
+let remove b x =
+  let y = try map b x with Not_found -> failwith "Bij.remove" in
+  { f = Gmap.remove x b.f; finv = Gmap.remove y b.finv }
+
+let app f b = Gmap.iter f b.f
+
+let to_list b = Gmap.to_list b.f
+
+
diff --git a/lib/bij.mli b/lib/bij.mli
new file mode 100644
index 000000000..65bae1eec
--- /dev/null
+++ b/lib/bij.mli
@@ -0,0 +1,19 @@
+
+(* $Id$ *)
+
+(* Bijections. *)
+
+type ('a,'b) t
+
+val empty : ('a,'b) t
+val map : ('a,'b) t -> 'a -> 'b
+val pam : ('a,'b) t -> 'b -> 'a
+val dom : ('a,'b) t -> 'a list
+val rng : ('a,'b) t -> 'b list
+val in_dom : ('a,'b) t -> 'a -> bool
+val in_rng : ('a,'b) t -> 'b -> bool
+val app : ('a -> 'b -> unit) -> ('a,'b) t -> unit
+val to_list : ('a,'b) t -> ('a * 'b) list
+
+val add : ('a,'b) t -> 'a * 'b -> ('a,'b) t
+val remove : ('a,'b) t -> 'a -> ('a,'b) t
diff --git a/lib/gmapl.ml b/lib/gmapl.ml
new file mode 100644
index 000000000..6295c4099
--- /dev/null
+++ b/lib/gmapl.ml
@@ -0,0 +1,28 @@
+
+(* $Id$ *)
+
+open Util
+
+type ('a,'b) t = ('a,'b list) Gmap.t
+
+let empty = Gmap.empty
+let mem = Gmap.mem
+let iter = Gmap.iter
+let map = Gmap.map
+let fold = Gmap.fold
+
+let add x y m =
+  try
+    let l = Gmap.find x m in
+    Gmap.add x (if List.mem y l then l else y::l) m
+  with Not_found ->
+    Gmap.add x [y] m
+
+let find x m =
+  try Gmap.find x m with Not_found -> []
+
+let remove x y m =
+  let l = Gmap.find x m in
+  Gmap.add x (if List.mem y l then list_subtract l [y] else l) m
+
+  
diff --git a/lib/gmapl.mli b/lib/gmapl.mli
new file mode 100644
index 000000000..27b465f83
--- /dev/null
+++ b/lib/gmapl.mli
@@ -0,0 +1,16 @@
+
+(* $Id$ *)
+
+(* Maps from ['a] to lists of ['b]. *)
+
+type ('a,'b) t = ('a,'b list) Gmap.t
+
+val empty : ('a,'b) t
+val mem :  'a -> ('a,'b) t -> bool
+val iter : ('a -> 'b list -> unit) -> ('a,'b) t -> unit
+val map : ('b list -> 'c list) -> ('a,'b) t -> ('a,'c) t
+val fold : ('a -> 'b list -> 'c -> 'c) -> ('a,'b) t -> 'c -> 'c
+
+val add : 'a -> 'b -> ('a,'b) t -> ('a,'b) t
+val find : 'a -> ('a,'b) t -> 'b list
+val remove : 'a -> 'b -> ('a,'b) t -> ('a,'b) t
diff --git a/lib/util.ml b/lib/util.ml
index 30f1cbeb6..bb5023886 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -91,10 +91,6 @@ let list_assign l n e =
   in 
   assrec [] (l,n)
 
-let rec list_distinct = function
-  | h::t -> (not (List.mem h t)) && list_distinct t
-  | [] -> true
-
 let list_map_i f = 
   let rec map_i_rec i = function
     | [] -> [] 
@@ -154,6 +150,15 @@ let rec list_distinct = function
   | h::t -> (not (List.mem h t)) && list_distinct t
   | _ -> true
 
+let list_subset l1 l2 =
+  let t2 = Hashtbl.create 151 in
+  List.iter (fun x -> Hashtbl.add t2 x ()) l2;
+  let rec look = function
+    | [] -> true
+    | x::ll -> try Hashtbl.find t2 x; look ll with Not_found -> false
+  in 
+  look l1
+
 (* Arrays *)
 
 let array_exists f v = 
diff --git a/lib/util.mli b/lib/util.mli
index a40a24ba4..3975cdfc6 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -46,6 +46,7 @@ val list_sep_last : 'a list -> 'a * 'a list
 val list_try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
 val list_uniquize : 'a list -> 'a list
 val list_distinct : 'a list -> bool
+val list_subset : 'a list -> 'a list -> bool
 
 (*s Arrays. *)
 
diff --git a/library/library.ml b/library/library.ml
index 1f040984a..6edc044a4 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -1,6 +1,7 @@
 
 (* $Id$ *)
 
+open Pp
 open Util
 open Names
 open Environ
@@ -43,6 +44,16 @@ let module_is_loaded s =
 let module_is_opened s =
   (find_module s).module_opened
 
+let loaded_modules () =
+  let l = ref [] in
+  Hashtbl.iter (fun s _ -> l := s :: !l) modules_table;
+  !l
+
+let opened_modules () =
+  let l = ref [] in
+  Hashtbl.iter (fun s m -> if m.module_opened then l := s :: !l) modules_table;
+  !l
+
 let vo_magic_number = 0700
 
 let (raw_extern_module, raw_intern_module) =
@@ -149,3 +160,12 @@ let save_module_to s f =
   close_out ch
 
 
+(* Pretty-printing of modules state. *)
+
+let fmt_modules_state () =
+  let opened = opened_modules ()
+  and loaded = loaded_modules () in
+  [< 'sTR "Imported (open) Modules: " ;
+     prlist_with_sep pr_spc (fun s -> [< 'sTR s >]) opened ; 'fNL ;
+     'sTR "Loaded Modules: " ;
+     prlist_with_sep pr_spc (fun s -> [< 'sTR s >]) loaded ; 'fNL >]
diff --git a/library/library.mli b/library/library.mli
index dc34de8a0..f3899250e 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -14,6 +14,11 @@ val open_module : string -> unit
 val module_is_loaded : string -> bool
 val module_is_opened : string -> bool
 
+val loaded_modules : unit -> string list
+val opened_modules : unit -> string list
+
+val fmt_modules_state : unit -> Pp.std_ppcmds
+
 (*s Require. The command [require_module spec m file export] loads and opens
   a module [m]. [file] specifies the filename, if not [None]. [spec]
   specifies to look for a specification ([true]) or for an implementation
diff --git a/tactics/stock.ml b/tactics/stock.ml
new file mode 100644
index 000000000..b0fa6d0e8
--- /dev/null
+++ b/tactics/stock.ml
@@ -0,0 +1,147 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Library
+
+(* The pattern table for tactics. *)
+
+(* The idea is that we want to write tactic files which are only
+   "activated" when certain modules are loaded and imported.  Already,
+   the question of how to store the tactics is hard, and we will not
+   address that here.  However, the question arises of how to store
+   the patterns that we will want to use for term-destructuring, and
+   the solution proposed is that we will store patterns with a
+   "module-marker", telling us which modules have to be open in order
+   to use the pattern.  So we will write:
+
+   let mark = make_module_marker ["<module-name>";<module-name>;...]
+
+   let p1 = put_pat mark "<parseable pattern goes here>"
+
+   And now, we can use:
+
+             (get p1)
+
+   to get the term which corresponds to this pattern, already parsed
+   and with the global names adjusted.
+
+   In other words, we will have the term which we would have had if we
+   had done an:
+
+        constr_of_com mt_ctxt (initial_sign()) "<text here>"
+
+   except that it will be computed at module-opening time, rather than
+   at tactic-application time.  The ONLY difference will be that
+   no implicit syntax resolution will happen.
+
+   So the entries we provide are:
+
+   type module_mark
+
+   value make_module_marker : string list -> module_mark
+
+   type marked_term
+
+   value put_pat : module_mark -> string -> marked_term
+
+   value get_pat : marked_term -> constr
+
+ *)
+
+type module_mark = Mmk of int
+
+let path_mark_bij = ref (Bij.empty : (string list,module_mark) Bij.t)
+
+let mmk_ctr = ref 0
+
+let new_mmk () = (incr mmk_ctr; !mmk_ctr)
+
+let make_module_marker stock sl =
+  let sorted_sl = Sort.list (<) sl in 
+  try 
+    Bij.map !path_mark_bij sorted_sl
+  with Not_found -> begin
+    let mmk = Mmk(new_mmk()) in 
+    path_mark_bij := Bij.add !path_mark_bij (sorted_sl,mmk);
+    mmk
+  end
+      
+let mark_satisfied mmk =
+  let spl = Bij.pam !path_mark_bij mmk in 
+  list_subset spl (loaded_modules())
+
+(* src_tab: for each module_mark, stores the tickets of objects which
+   need to be compiled when that mark becomes active.
+
+   obj_tab: for each ticket, stores the (possibly nonexistent)
+   compiled object
+
+   ticket_tab: for each ticket, stores its module_mark and the string
+   (source)
+
+   string_tab: for each string * module_mark, stores the ticket. *)
+
+type 'a stock_args = {
+  name : string;
+  proc : string -> 'a }
+
+type 'a stock = {
+  mutable src_tab : (module_mark,int) Gmapl.t;
+  mutable obj_tab : (int,'a) Gmap.t;
+  mutable ticket_string_bij : (int,string * module_mark) Bij.t;
+  args : 'a stock_args }
+
+type 'a stocked = int
+
+let stock_ctr = ref 0
+
+let new_stock () = (incr stock_ctr; !stock_ctr)
+
+let make_stock args =
+  { src_tab = Gmapl.empty;
+    obj_tab = Gmap.empty;
+    ticket_string_bij = Bij.empty;
+    args = args }
+  
+let stock stock mmk s =
+  try 
+    Bij.pam stock.ticket_string_bij (s,mmk)
+  with Not_found -> begin
+    let idx = new_stock() in 
+    stock.src_tab <- Gmapl.add mmk idx stock.src_tab;
+    stock.ticket_string_bij <- Bij.add stock.ticket_string_bij (idx,(s,mmk));
+    idx
+  end
+
+let pr_mm mm =
+  let sl = Bij.pam !path_mark_bij mm in
+  prlist_with_sep pr_spc (fun s -> [< 'sTR s >]) sl
+
+(* TODO: traiter a part les erreurs provenant de stock.args.proc
+   ( = parsing quand [so]pattern appelle retrieve)
+    -> eviter d'avoir l'erreur stocked datum *)
+
+let retrieve stock idx =
+  try 
+    Gmap.find idx stock.obj_tab
+  with Not_found ->
+    let (s,mmk) = Bij.map stock.ticket_string_bij idx in 
+    if mark_satisfied mmk then
+      try
+        let c = stock.args.proc s in 
+	stock.obj_tab <- Gmap.add idx c stock.obj_tab;
+        c
+      with e -> begin
+        mSGNL [< 'sTR"Processing of the stocked datum " ; 'sTR s ;
+                 'sTR" failed." ; 'fNL;
+                 Library.fmt_modules_state() >];
+	raise e
+      end
+    else
+      errorlabstrm "Stock.retrieve"
+        [< 'sTR"The stocked object "; 'sTR s; 'sTR" was not compilable"; 
+	   'fNL; 'sTR"Its module mark was: "; pr_mm mmk ; 'fNL ;
+           Library.fmt_modules_state() >]
diff --git a/tactics/stock.mli b/tactics/stock.mli
new file mode 100644
index 000000000..5c3b44eb9
--- /dev/null
+++ b/tactics/stock.mli
@@ -0,0 +1,24 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+(*i*)
+
+(* The pattern table for tactics. *)
+
+type 'a stock
+
+type module_mark
+
+type 'a stocked
+
+type 'a stock_args = {
+  name : string;
+  proc : string -> 'a }
+
+val make_stock : 'a stock_args -> 'a stock
+val make_module_marker : 'a stock -> string list -> module_mark
+val stock : 'a stock -> module_mark -> string -> 'a stocked
+val retrieve : 'a stock -> 'a stocked -> 'a
+