diff options
| -rw-r--r-- | .depend | 17 | ||||
| -rw-r--r-- | Makefile | 40 | ||||
| -rw-r--r-- | dev/TODO | 7 | ||||
| -rw-r--r-- | kernel/names.ml | 4 | ||||
| -rw-r--r-- | kernel/names.mli | 3 | ||||
| -rw-r--r-- | kernel/reduction.ml | 2 | ||||
| -rw-r--r-- | kernel/typing.ml | 3 | ||||
| -rw-r--r-- | lib/system.ml | 80 | ||||
| -rw-r--r-- | lib/system.mli | 7 | ||||
| -rw-r--r-- | library/lib.ml | 167 | ||||
| -rw-r--r-- | library/lib.mli | 57 | ||||
| -rw-r--r-- | library/states.ml | 22 | ||||
| -rw-r--r-- | library/states.mli | 8 | ||||
| -rw-r--r-- | library/summary.ml | 2 | ||||
| -rw-r--r-- | library/summary.mli | 6 |
15 files changed, 395 insertions, 30 deletions
@@ -28,6 +28,9 @@ kernel/typing.cmi: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/univ.cmi: kernel/names.cmi lib/pp.cmi lib/pp.cmi: lib/pp_control.cmi lib/util.cmi: lib/pp.cmi +library/global.cmi: kernel/constant.cmi kernel/evd.cmi kernel/inductive.cmi \ + kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi +library/lib.cmi: library/libobject.cmi kernel/names.cmi library/summary.cmi library/libobject.cmi: kernel/names.cmi library/summary.cmi: kernel/names.cmi parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi parsing/pcoq.cmi lib/pp.cmi @@ -145,14 +148,24 @@ lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi lib/pp_control.cmo: lib/pp_control.cmi lib/pp_control.cmx: lib/pp_control.cmi -lib/system.cmo: lib/system.cmi -lib/system.cmx: lib/system.cmi +lib/system.cmo: lib/pp.cmi lib/util.cmi lib/system.cmi +lib/system.cmx: lib/pp.cmx lib/util.cmx lib/system.cmi lib/util.cmo: lib/pp.cmi lib/util.cmi lib/util.cmx: lib/pp.cmx lib/util.cmi +library/global.cmo: library/summary.cmi kernel/typing.cmi library/global.cmi +library/global.cmx: library/summary.cmx kernel/typing.cmx library/global.cmi +library/lib.cmo: library/libobject.cmi kernel/names.cmi library/summary.cmi \ + lib/util.cmi library/lib.cmi +library/lib.cmx: library/libobject.cmx kernel/names.cmx library/summary.cmx \ + lib/util.cmx library/lib.cmi 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/states.cmo: library/lib.cmi library/summary.cmi lib/system.cmi \ + library/states.cmi +library/states.cmx: library/lib.cmx library/summary.cmx lib/system.cmx \ + library/states.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 \ @@ -10,13 +10,13 @@ noargument: @echo " make cleanall" @echo or make archclean +INCLUDES=-I config -I lib -I kernel -I library -I parsing -I $(CAMLP4LIB) + BYTEFLAGS=$(INCLUDES) $(CAMLDEBUG) OPTFLAGS=$(INCLUDES) $(CAMLTIMEPROF) OCAMLDEP=ocamldep DEPFLAGS=$(INCLUDES) -INCLUDES=-I config -I lib -I kernel -I library -I parsing -I $(CAMLP4LIB) - CAMLP4EXTEND=camlp4o $(INCLUDES) pa_extend.cmo OCAMLC_P4O=$(OCAMLC) -pp camlp4o $(BYTEFLAGS) OCAMLOPT_P4O=$(OCAMLOPT) -pp camlp4o $(OPTFLAGS) @@ -29,8 +29,8 @@ CAMLP4OBJS=gramlib.cma CONFIG=config/coq_config.cmo -LIB=lib/pp_control.cmo lib/pp.cmo lib/system.cmo lib/util.cmo \ - lib/hashcons.cmo lib/dyn.cmo +LIB=lib/pp_control.cmo lib/pp.cmo lib/util.cmo \ + lib/hashcons.cmo lib/dyn.cmo lib/system.cmo KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \ kernel/sign.cmo kernel/evd.cmo kernel/constant.cmo \ @@ -40,8 +40,8 @@ KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \ kernel/type_errors.cmo kernel/typeops.cmo kernel/indtypes.cmo \ kernel/typing.cmo -LIBRARY=library/libobject.cmo library/summary.cmo \ - library/global.cmo +LIBRARY=library/libobject.cmo library/summary.cmo library/lib.cmo \ + library/global.cmo library/states.cmo PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \ parsing/g_prim.cmo parsing/g_basevernac.cmo parsing/g_vernac.cmo \ @@ -57,7 +57,7 @@ CMX=$(CMO:.cmo=.cmx) # Targets -world: minicoq coqtop doc dev/db_printers.cmo +world: minicoq coqtop.byte dev/db_printers.cmo # coqtop @@ -106,11 +106,16 @@ tags: "--regex=/val[ \t]+\([^ \t]+\)/\1/" \ "--regex=/module[ \t]+\([^ \t]+\)/\1/" -# Special rules +### Special rules + +# lexer (compiled with camlp4 to get optimized streams) parsing/lexer.cmo: parsing/lexer.ml $(OCAMLC_P4O) -c $< +cleanall:: + rm -f parsing/lexer.ml + beforedepend:: parsing/lexer.ml # grammar modules with camlp4 @@ -118,10 +123,13 @@ beforedepend:: parsing/lexer.ml parsing/q_coqast.cmo: parsing/q_coqast.ml4 $(OCAMLC) $(BYTEFLAGS) -c -pp "camlp4o q_MLast.cmo -impl" -impl $< +# the generic rules could be used for g_prim.ml4, but this implies +# circular dependencies between g_prim and grammar parsing/g_prim.cmo: parsing/g_prim.ml4 - $(OCAMLC) $(BYTEFLAGS) -c -pp "camlp4o pa_extend.cmo -impl" -impl $< + $(OCAMLC) $(BYTEFLAGS) -c -pp "$(CAMLP4EXTEND) -impl" -impl $< + parsing/g_prim.cmx: parsing/g_prim.ml4 - $(OCAMLOPT) $(OPTFLAGS) -c -pp "camlp4o pa_extend.cmo -impl" -impl $< + $(OCAMLOPT) $(OPTFLAGS) -c -pp "$(CAMLP4EXTEND) -impl" -impl $< GRAMMARCMO=./lib/pp_control.cmo ./lib/pp.cmo ./lib/util.cmo ./lib/dyn.cmo \ ./lib/hashcons.cmo ./parsing/coqast.cmo ./parsing/lexer.cmo \ @@ -130,11 +138,13 @@ GRAMMARCMO=./lib/pp_control.cmo ./lib/pp.cmo ./lib/util.cmo ./lib/dyn.cmo \ parsing/grammar.cma: $(GRAMMARCMO) $(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@ +CAMLP4GRAMMAR=camlp4o -I parsing pa_extend.cmo grammar.cma + parsing/g_%.cmo: parsing/g_%.ml4 parsing/grammar.cma - $(OCAMLC) $(BYTEFLAGS) -c -pp "camlp4o -I parsing pa_extend.cmo grammar.cma -impl" -impl $< + $(OCAMLC) $(BYTEFLAGS) -c -pp "$(CAMLP4GRAMMAR) -impl" -impl $< parsing/g_%.cmx: parsing/g_%.ml4 parsing/grammar.cma - $(OCAMLOPT) $(OPTFLAGS) -c -pp "camlp4o -I parsing pa_extend.cmo grammar.cma -impl" -impl $< + $(OCAMLOPT) $(OPTFLAGS) -c -pp "$(CAMLP4GRAMMAR) -impl" -impl $< beforedepend:: $(GRAMMARCMO) @@ -155,10 +165,10 @@ beforedepend:: $(GRAMMARCMO) ocamllex $< .ml4.cmo: - $(OCAMLC) $(BYTEFLAGS) -I $(CAMLP4LIB) -pp "$(CAMLP4EXTEND) -impl" -c -impl $< + $(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4EXTEND) -impl" -c -impl $< .ml4.cmx: - $(OCAMLOPT) $(OPTFLAGS) -I $(CAMLP4LIB) -pp "$(CAMLP4EXTEND) -impl" -c -impl $< + $(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4EXTEND) -impl" -c -impl $< # Cleaning @@ -175,7 +185,7 @@ cleanall:: archclean rm -f lib/*.cm[io] lib/*~ rm -f kernel/*.cm[io] kernel/*~ rm -f library/*.cm[io] library/*~ - rm -f parsing/*.cm[io] parsing/*~ + rm -f parsing/*.cm[io] parsing/*.ppo parsing/*~ cleanconfig:: rm -f config/Makefile config/coq_config.ml @@ -1,9 +1,6 @@ - o Himsg - en faire un foncteur qui prend en arguments des fonctions - sachant afficher les termes, et retournant des fonctions - expliquant les messages d'erreur (de typage, d'inductifs, de - convertibilité), retournant des std_ppcmds. + o Minicoq + utilisation de Himsg o Lexer à compléter diff --git a/kernel/names.ml b/kernel/names.ml index af07ba426..6e5835fbb 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -55,7 +55,7 @@ let print_id { atom = a; index = n } = | ("",n) -> [< 'sTR"[" ; 'iNT n ; 'sTR"]" >] | (s,n) -> [< 'sTR s ; (if n = (-1) then [< >] else [< 'iNT n >]) >] -let pr_idl idl = prlist_with_sep pr_spc print_id idl +let print_idl idl = prlist_with_sep pr_spc print_id idl let id_ord id1 id2 = let (s1,n1) = repr_ident id1 @@ -168,6 +168,8 @@ let path_of_string s = with | Invalid_argument _ -> invalid_arg "path_of_string" +let print_sp sp = [< 'sTR (string_of_path sp) >] + let coerce_path k { dirpath = p; basename = id } = { dirpath = p; basename = id; kind = k } diff --git a/kernel/names.mli b/kernel/names.mli index be26f0f32..c022a84a3 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -16,7 +16,7 @@ val id_of_string : string -> identifier val explode_id : identifier -> string list val print_id : identifier -> std_ppcmds -val pr_idl : identifier list -> std_ppcmds +val print_idl : identifier list -> std_ppcmds val atompart_of_id : identifier -> string val index_of_id : identifier -> int val id_ord : identifier -> identifier -> int @@ -51,6 +51,7 @@ val kind_of_path : section_path -> path_kind val path_of_string : string -> section_path val string_of_path : section_path -> string val string_of_path_mind : section_path -> identifier -> string +val print_sp : section_path -> std_ppcmds val coerce_path : path_kind -> section_path -> section_path val fwsp_of : section_path -> section_path diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 1e72c4033..f16fa0d8c 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -160,7 +160,7 @@ let subst_term_occ locs c t = (occ,[]) cl in (occ',DLAMV(n,Array.of_list (List.rev cl') )) - | _ -> occ,t + | _ -> occ,t in if locs = [] then subst_term c t diff --git a/kernel/typing.ml b/kernel/typing.ml index f3928b2fd..7cd127cf6 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -159,7 +159,8 @@ and execute_array mf env v = (Array.of_list jl, u1) and execute_list mf env = function - | [] -> ([], universes env) + | [] -> + ([], universes env) | c::r -> let (j,u') = execute mf env c in let (jr,u'') = execute_list mf (set_universes u' env) r in diff --git a/lib/system.ml b/lib/system.ml index fe0efa073..016a6f97e 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -1,6 +1,86 @@ (* $Id$ *) +open Pp +open Util + +(* Files and load path. *) + +let load_path = ref ([] : string list) + +let add_path dir = load_path := dir :: !load_path + +let del_path dir = + if List.mem dir !load_path then + load_path := List.filter (fun s -> s <> dir) !load_path + +(* TODO: rétablir glob (expansion ~user et $VAR) si on le juge nécessaire *) +let glob s = s + +let search_in_path path filename = + let rec search = function + | dir :: rem -> + let f = glob (Filename.concat dir filename) in + if Sys.file_exists f then f else search rem + | [] -> + raise Not_found + in + search path + +let find_file_in_path name = + let globname = glob name in + if not (Filename.is_relative globname) then + globname + else + try + search_in_path !load_path name + with Not_found -> + errorlabstrm "System.find_file_in_path" + (hOV 0 [< 'sTR"Can't find file" ; 'sPC ; 'sTR name ; 'sPC ; + 'sTR"on loadpath" >]) + +let make_suffix name suffix = + if Filename.check_suffix name suffix then name else (name ^ suffix) + +let open_trapping_failure open_fun name suffix = + let rname = make_suffix name suffix in + try open_fun rname with _ -> error ("Can't open " ^ rname) + +let (extern_intern : + int -> string -> ((string -> 'a -> unit) * (string -> 'a))) + = fun magic suffix -> + + let extern_state name val_0 = + try + let (expname,channel) = + open_trapping_failure (fun n -> n,open_out_bin n) name suffix in + try + output_binary_int channel magic; + output_value channel val_0; + close_out channel + with e -> begin + (try Sys.remove expname + with _ -> mSGNL [< 'sTR"Warning: " ; 'sTR"Could not remove file " ; + 'sTR expname ; 'sTR" which is corrupted !!" >]); + raise e + end + with Sys_error s -> error ("System error: " ^ s) + + and intern_state name = + try + let fname = find_file_in_path (make_suffix name suffix) in + let channel = open_in_bin fname in + if input_binary_int channel <> magic then + error (fname^" not compiled with the current version of Coq"); + let v = input_value(channel) in + close_in channel; + v + with Sys_error s -> error("System error: " ^ s) + + in + (extern_state,intern_state) + + (* Time stamps. *) type time_stamp = float diff --git a/lib/system.mli b/lib/system.mli index 13265d1d8..b887f5eb5 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -1,6 +1,13 @@ (* $Id$ *) +(*s Files and load path. *) + +val add_path : string -> unit +val del_path : string -> unit + +val extern_intern : int -> string -> (string -> 'a -> unit) * (string -> 'a) + (*s Time stamps. *) type time_stamp diff --git a/library/lib.ml b/library/lib.ml new file mode 100644 index 000000000..a8ab156c5 --- /dev/null +++ b/library/lib.ml @@ -0,0 +1,167 @@ + +(* $Id$ *) + +open Util +open Names +open Libobject +open Summary + +type node = + | Leaf of obj + | OpenedSection of string * module_p + | ClosedSection of string * module_p * library_segment + | FrozenState of Summary.frozen + +and library_segment = (section_path * node) list + +and module_p = bool + +type library_entry = section_path * node + + +(* We keep trace of operations in a stack [lib_stk]. + [path_prefix] is the current path of sections (in correct order). *) + +let lib_stk = ref ([] : (section_path * node) list) + +let path_prefix = ref ([] : string list) + +let recalc_path_prefix () = + let rec recalc = function + | (sp, OpenedSection _) :: _ -> + let (pl,id,_) = repr_path sp in pl@[string_of_id id] + | _::l -> recalc l + | [] -> [] + in + path_prefix := recalc !lib_stk + +let pop_path_prefix () = + let rec pop acc = function + | [] -> assert false + | [_] -> path_prefix := acc + | s::l -> pop (s::acc) l + in + pop [] !path_prefix + +let make_path id k = Names.make_path !path_prefix id k + +let cwd () = !path_prefix + +let find_entry_p p = + let rec find = function + | [] -> raise Not_found + | ent::l -> if p ent then ent else find l + in + find !lib_stk + +let split_lib sp = + let rec findrec acc = function + | ((sp',obj) as hd)::t -> + if sp = sp' then (acc,hd,t) else findrec (hd::acc) t + | [] -> error "no such entry" + in + findrec [] !lib_stk + + +(* Adding operations. *) + +let add_entry sp node = + lib_stk := (sp,node) :: !lib_stk + +let anonymous_id = + let n = ref 0 in + fun () -> incr n; id_of_string ("_" ^ (string_of_int !n)) + +let add_anonymous_entry node = + let sp = make_path (anonymous_id()) OBJ in + add_entry sp node + +let add_leaf id obj = + let sp = make_path id OBJ in + add_entry sp (Leaf obj); + sp + +let add_anonymous_leaf obj = + add_anonymous_entry (Leaf obj) + +let add_frozen_state () = + add_anonymous_entry (FrozenState (freeze_summaries())) + +let contents_after = function + | None -> !lib_stk + | Some sp -> let (after,_,_) = split_lib sp in after + + +(* Sections. *) + +let is_opened_section = function (_,OpenedSection _) -> true | _ -> false + +let check_single_module () = + try + let _ = find_entry_p is_opened_section in + error "a module or a section is already opened" + with Not_found -> () + +let open_section s modp = + if modp then check_single_module (); + let sp = make_path (id_of_string s) OBJ in + add_entry sp (OpenedSection (s,modp)); + path_prefix := !path_prefix @ [s]; + sp + +let close_section s = + let (sp,modp) = + try + match find_entry_p is_opened_section with + | sp,OpenedSection (s',modp) -> + if s <> s' then error "this is not the last opened section"; + (sp,modp) + | _ -> assert false + with Not_found -> + error "no opened section" + in + let (after,_,before) = split_lib sp in + lib_stk := before; + add_entry sp (ClosedSection (s,modp,after)); + add_frozen_state (); + pop_path_prefix () + + +(* Backtracking. *) + +let recache_decl = function + | (sp, Leaf o) -> cache_object (sp,o) + | _ -> () + +let recache_context ctx = + List.iter recache_decl ctx + +let is_frozen_state = function (_,FrozenState _) -> true | _ -> false + +let reset_to sp = + let (_,_,before) = split_lib sp in + lib_stk := before; + recalc_path_prefix (); + let (spf,frozen) = match find_entry_p is_frozen_state with + | (sp, FrozenState f) -> sp,f + | _ -> assert false + in + unfreeze_summaries frozen; + let (after,_,_) = split_lib spf in + recache_context (List.rev after) + + +(* State and initialization. *) + +type frozen = library_segment + +let freeze () = !lib_stk + +let unfreeze stk = + lib_stk := stk; + recalc_path_prefix () + +let init () = + lib_stk := []; + add_frozen_state (); + path_prefix := [] diff --git a/library/lib.mli b/library/lib.mli new file mode 100644 index 000000000..80f61ef40 --- /dev/null +++ b/library/lib.mli @@ -0,0 +1,57 @@ + +(* $Id$ *) + +(*i*) +open Names +open Libobject +open Summary +(*i*) + +(* This module provides a general mechanism to keep a trace of all operations + and to backtrack (undo) those operations. It provides also the section + mechanism (at a low level; discharge is not known at this step). *) + +type node = + | Leaf of obj + | OpenedSection of string * module_p + | ClosedSection of string * module_p * library_segment + | FrozenState of Summary.frozen + +and library_segment = (section_path * node) list + +and module_p = bool + +type library_entry = section_path * node + + +(*s Adding operations, and getting the current list of operations (most + recent ones come first). *) + +val add_leaf : identifier -> obj -> section_path +val add_anonymous_leaf : obj -> unit + +val contents_after : section_path option -> library_segment + + +(*s Opening and closing a section. *) + +val open_section : string -> bool -> section_path +val close_section : string -> unit + +val make_path : identifier -> path_kind -> section_path +val cwd : unit -> string list + + +(*s Backtracking (undo). *) + +val reset_to : section_path -> unit + + +(*s We can get and set the state of the operations (used in [States]). *) + +type frozen + +val freeze : unit -> frozen +val unfreeze : frozen -> unit + +val init : unit -> unit diff --git a/library/states.ml b/library/states.ml new file mode 100644 index 000000000..2e198e36f --- /dev/null +++ b/library/states.ml @@ -0,0 +1,22 @@ + +(* $Id$ *) + +open System +open Lib +open Summary + +type state = Lib.frozen * Summary.frozen + +let get_state () = + (Lib.freeze(), freeze_summaries()) + +let set_state (fl,fs) = + Lib.unfreeze fl; + unfreeze_summaries fs + +let state_magic_number = 19764 + +let (extern_state,intern_state) = + let (raw_extern, raw_intern) = extern_intern state_magic_number ".coq" in + (fun s -> raw_extern s (get_state())), + (fun s -> set_state (raw_intern s)) diff --git a/library/states.mli b/library/states.mli new file mode 100644 index 000000000..06a877802 --- /dev/null +++ b/library/states.mli @@ -0,0 +1,8 @@ + +(* $Id$ *) + +type state + +val intern_state : string -> unit +val extern_state : string -> unit + diff --git a/library/summary.ml b/library/summary.ml index f58917202..0ba07a737 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -28,7 +28,7 @@ let declare_summary sumname sdecl = [< 'sTR "Cannot declare a summary twice: " ; 'sTR sumname >]; Hashtbl.add summaries sumname ddecl -type frozen_summaries = Dyn.t Stringmap.t +type frozen = Dyn.t Stringmap.t let freeze_summaries () = let m = ref Stringmap.empty in diff --git a/library/summary.mli b/library/summary.mli index faa887f37..0d329a947 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -15,10 +15,10 @@ type 'a summary_declaration = { val declare_summary : string -> 'a summary_declaration -> unit -type frozen_summaries +type frozen -val freeze_summaries : unit -> frozen_summaries -val unfreeze_summaries : frozen_summaries -> unit +val freeze_summaries : unit -> frozen +val unfreeze_summaries : frozen -> unit val init_summaries : unit -> unit |