mise en place repertoire test-suite/, toplevel/, parsing/

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

7 files changed, 135 insertions, 12 deletions

diff --git a/.cvsignore b/.cvsignore
index 6443d52fdd..205dc23a31 100644
--- a/.cvsignore
+++ b/.cvsignore
@@ -1 +1,3 @@
 coqtop.byte
+coqtop
+minicoq
diff --git a/.depend b/.depend
index b674b479a8..d4a67cce11 100644
--- a/.depend
+++ b/.depend
@@ -2,8 +2,9 @@ kernel/abstraction.cmi: kernel/names.cmi kernel/term.cmi
 kernel/closure.cmi: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
     kernel/names.cmi lib/pp.cmi kernel/term.cmi 
 kernel/constant.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi 
-kernel/environ.cmi: kernel/constant.cmi kernel/evd.cmi kernel/inductive.cmi \
-    kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi 
+kernel/environ.cmi: kernel/abstraction.cmi kernel/constant.cmi kernel/evd.cmi \
+    kernel/inductive.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
+    kernel/univ.cmi 
 kernel/evd.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi 
 kernel/generic.cmi: kernel/names.cmi lib/util.cmi 
 kernel/indtypes.cmi: kernel/environ.cmi kernel/inductive.cmi kernel/names.cmi \
@@ -140,5 +141,11 @@ library/libobject.cmo: lib/dyn.cmi kernel/names.cmi lib/util.cmi \
     library/libobject.cmi 
 library/libobject.cmx: lib/dyn.cmx kernel/names.cmx lib/util.cmx \
     library/libobject.cmi 
-library/summary.cmo: kernel/names.cmi library/summary.cmi 
-library/summary.cmx: kernel/names.cmx library/summary.cmi 
+library/summary.cmo: lib/dyn.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \
+    library/summary.cmi 
+library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \
+    library/summary.cmi 
+parsing/lexer.cmo: lib/util.cmi 
+parsing/lexer.cmx: lib/util.cmx 
+toplevel/minicoq.cmo: kernel/generic.cmi kernel/names.cmi 
+toplevel/minicoq.cmx: kernel/generic.cmx kernel/names.cmx 
diff --git a/Makefile b/Makefile
index e062d39979..9b2060b3a0 100644
--- a/Makefile
+++ b/Makefile
@@ -20,6 +20,8 @@ INCLUDES=-I config -I lib -I kernel -I library
 
 # Objects files 
 
+CLIBS=unix.cma
+
 CONFIG=config/coq_config.cmo
 
 LIB=lib/pp_control.cmo lib/pp.cmo lib/util.cmo lib/hashcons.cmo \
@@ -35,13 +37,21 @@ KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \
 
 LIBRARY=library/libobject.cmo library/summary.cmo
 
-OBJS=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY)
+PARSING=parsing/lexer.cmo
+
+OBJS=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PARSING)
 
 # Targets
 
 world: $(OBJS)
 	#$(OCAMLC) -o coqtop.byte $(OBJS)
-	ocamlmktop -o coqtop $(OBJS)
+	ocamlmktop -o coqtop -custom $(CLIBS) $(OBJS) $(OSDEPLIBS)
+
+MINICOQOBJS=$(CONFIG) $(LIB) $(KERNEL) $(PARSING) toplevel/minicoq.cmo
+
+minicoq: $(OBJS) $(MINICOQOBJS)
+	$(OCAMLC) -o minicoq -custom $(CLIBS) $(OBJS) $(MINICOQOBJS) \
+	  $(OSDEPLIBS)
 
 # Literate programming (with ocamlweb)
 
@@ -69,7 +79,7 @@ tags:
 
 # Default rules
 
-.SUFFIXES: .ml .mli .cmo .cmi .cmx
+.SUFFIXES: .ml .mli .cmo .cmi .cmx .mll
 
 .ml.cmo:
 	$(OCAMLC) $(BYTEFLAGS) -c $<
@@ -80,6 +90,9 @@ tags:
 .ml.cmx:
 	$(OCAMLOPT) $(OPTFLAGS) -c $<
 
+.mll.ml:
+	ocamllex $<
+
 # Cleaning
 
 archclean::
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 67198e9f12..441d77a081 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -14,10 +14,16 @@ open Abstraction
 
 (* The type of environments. *)
 
+type import = string * time_stamp
+
+type global = Constant | Inductive | Abstraction
+
 type globals = {
   env_constants : constant_body Spmap.t;
   env_inductives : mutual_inductive_body Spmap.t;
-  env_abstractions : abstraction_body Spmap.t }
+  env_abstractions : abstraction_body Spmap.t;
+  env_locals : (global * section_path) list;
+  env_imports : import list }
 
 type 'a unsafe_env = {
   env_context : context;
@@ -31,7 +37,9 @@ let empty_env = {
   env_globals = {
     env_constants = Spmap.empty;
     env_inductives = Spmap.empty;
-    env_abstractions = Spmap.empty };
+    env_abstractions = Spmap.empty;
+    env_locals = [];
+    env_imports = [] };
   env_sigma = mt_evd;
   env_metamap = [];
   env_universes = initial_universes }
@@ -54,12 +62,29 @@ let set_universes g env =
 
 let add_constant sp cb env =
   let new_constants = Spmap.add sp cb env.env_globals.env_constants in
-  let new_globals = { env.env_globals with env_constants = new_constants } in
+  let new_locals = (Constant,sp)::env.env_globals.env_locals in
+  let new_globals = 
+    { env.env_globals with 
+	env_constants = new_constants; 
+	env_locals = new_locals } in
   { env with env_globals = new_globals }
 
 let add_mind sp mib env =
   let new_inds = Spmap.add sp mib env.env_globals.env_inductives in
-  let new_globals = { env.env_globals with env_inductives = new_inds } in
+  let new_locals = (Inductive,sp)::env.env_globals.env_locals in
+  let new_globals = 
+    { env.env_globals with 
+	env_inductives = new_inds;
+	env_locals = new_locals } in
+  { env with env_globals = new_globals }
+
+let add_abstraction sp ab env =
+  let new_abs = Spmap.add sp ab env.env_globals.env_abstractions in
+  let new_locals = (Abstraction,sp)::env.env_globals.env_locals in
+  let new_globals = 
+    { env.env_globals with 
+	env_abstractions = new_abs;
+	env_locals = new_locals } in
   { env with env_globals = new_globals }
   
 let new_meta = 
@@ -220,7 +245,60 @@ let evaluable_const env k =
   with Not_found -> 
     false
 
-(* Judgments. *)
+(*s Modules (i.e. compiled environments). *)
+
+type compiled_env = {
+  cenv_id : string;
+  cenv_stamp : time_stamp;
+  cenv_needed : import list;
+  cenv_constants : (section_path * constant_body) list;
+  cenv_inductives : (section_path * mutual_inductive_body) list;
+  cenv_abstractions : (section_path * abstraction_body) list }
+
+let exported_objects env =
+  let gl = env.env_globals in
+  let separate (cst,ind,abs) = function
+    | (Constant,sp) -> (sp,Spmap.find sp gl.env_constants)::cst,ind,abs
+    | (Inductive,sp) -> cst,(sp,Spmap.find sp gl.env_inductives)::ind,abs
+    | (Abstraction,sp) -> cst,ind,(sp,Spmap.find sp gl.env_abstractions)::abs
+  in
+  List.fold_left separate ([],[],[]) gl.env_locals
+
+let export env id = 
+  let (cst,ind,abs) = exported_objects env in
+  { cenv_id = id;
+    cenv_stamp = get_time_stamp ();
+    cenv_needed = env.env_globals.env_imports;
+    cenv_constants = cst;
+    cenv_inductives = ind;
+    cenv_abstractions = abs }
+
+let check_imports env needed =
+  let imports = env.env_globals.env_imports in
+  let check (id,stamp) =
+    try
+      let actual_stamp = List.assoc id imports in
+      if compare_time_stamps stamp actual_stamp <> 0 then
+	error ("Inconsistent assumptions over module " ^ id)
+    with Not_found -> 
+      error ("Reference to unknown module " ^ id)
+  in
+  List.iter check needed
+
+let import cenv env =
+  check_imports env cenv.cenv_needed;
+  let add_list t = List.fold_left (fun t (sp,x) -> Spmap.add sp x t) t in
+  let gl = env.env_globals in
+  let new_globals = 
+    { env_constants = add_list gl.env_constants cenv.cenv_constants;
+      env_inductives = add_list gl.env_inductives cenv.cenv_inductives;
+      env_abstractions = add_list gl.env_abstractions cenv.cenv_abstractions;
+      env_locals = gl.env_locals;
+      env_imports = (cenv.cenv_id,cenv.cenv_stamp) :: gl.env_imports }
+  in
+  { env with env_globals = new_globals }
+
+(*s Judgments. *)
 
 type unsafe_judgment = { 
   uj_val : constr;
diff --git a/kernel/environ.mli b/kernel/environ.mli
index a1b7307e18..3e88fcfd15 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -6,6 +6,7 @@ open Names
 open Term
 open Constant
 open Inductive
+open Abstraction
 open Evd
 open Univ
 open Sign
@@ -32,6 +33,8 @@ val add_constant :
   section_path -> constant_body -> 'a unsafe_env -> 'a unsafe_env
 val add_mind : 
   section_path -> mutual_inductive_body -> 'a unsafe_env -> 'a unsafe_env
+val add_abstraction : 
+  section_path -> abstraction_body -> 'a unsafe_env -> 'a unsafe_env
 
 val new_meta : unit -> int
 
@@ -57,6 +60,13 @@ val evaluable_const : 'a unsafe_env -> constr -> bool
 
 val is_existential : constr -> bool
 
+(*s Modules. *)
+
+type compiled_env
+
+val export : 'a unsafe_env -> string -> compiled_env
+val import : compiled_env -> 'a unsafe_env -> 'a unsafe_env
+
 (*s Unsafe judgments. We introduce here the pre-type of judgments, which is
   actually only a datatype to store a term with its type and the type of its
   type. *)
diff --git a/lib/util.ml b/lib/util.ml
index 6983410978..fb50d1e4e5 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -259,6 +259,14 @@ type ('a,'b) union = Inl of 'a | Inr of 'b
 
 module Intset = Set.Make(struct type t = int let compare = compare end)
 
+type time_stamp = float
+
+let get_time_stamp () = Unix.time()
+
+let compare_time_stamps t1 t2 =
+  let dt = t2 -. t1 in
+  if dt < 0.0 then -1 else if dt = 0.0 then 0 else 1
+
 (* Pretty-printing *)
   
 let pr_spc () = [< 'sPC >];;
diff --git a/lib/util.mli b/lib/util.mli
index 2d764d4999..98296264f9 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -72,6 +72,11 @@ type ('a,'b) union = Inl of 'a | Inr of 'b
 
 module Intset : Set.S with type elt = int
 
+type time_stamp
+
+val get_time_stamp : unit -> time_stamp
+val compare_time_stamps : time_stamp -> time_stamp -> int
+
 (*s Pretty-printing. *)
 
 val pr_spc : unit -> std_ppcmds