From 74f6dceaab0146085e8ac48f9976665026099555 Mon Sep 17 00:00:00 2001 From: filliatr Date: Wed, 1 Dec 1999 17:34:36 +0000 Subject: poursuite de Vernacentries git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@178 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .depend | 110 +++++++++++++++++++++++++++++++++------------------- Makefile | 5 ++- kernel/typeops.ml | 24 ++++++++++++ kernel/typeops.mli | 1 + lib/options.ml | 9 +++++ lib/options.mli | 3 ++ lib/system.ml | 52 +++++++++++++++---------- lib/system.mli | 5 ++- lib/util.ml | 6 +++ lib/util.mli | 1 + library/declare.ml | 33 ++++++++++------ library/declare.mli | 11 ++++-- library/impargs.ml | 15 +++++++ library/impargs.mli | 4 +- proofs/pfedit.ml | 56 ++++++++++++++++---------- proofs/pfedit.mli | 33 +++++++++++++++- tactics/pattern.ml | 2 +- 17 files changed, 269 insertions(+), 101 deletions(-) diff --git a/.depend b/.depend index 654c9c5f2e..31deddb792 100644 --- a/.depend +++ b/.depend @@ -54,6 +54,8 @@ parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/names.cmi pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi parsing/coqast.cmi: lib/dyn.cmi +parsing/egrammar.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \ + parsing/pcoq.cmi parsing/esyntax.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \ lib/pp.cmi parsing/extend.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \ @@ -98,8 +100,9 @@ proofs/logic.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \ lib/pp.cmi proofs/proof_trees.cmi kernel/sign.cmi kernel/term.cmi proofs/macros.cmi: parsing/ast.cmi parsing/coqast.cmi kernel/names.cmi \ proofs/proof_trees.cmi proofs/tacmach.cmi -proofs/pfedit.cmi: library/declare.cmi lib/pp.cmi proofs/proof_trees.cmi \ - kernel/sign.cmi proofs/tacmach.cmi +proofs/pfedit.cmi: parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \ + lib/pp.cmi proofs/proof_trees.cmi kernel/sign.cmi proofs/tacmach.cmi \ + kernel/term.cmi proofs/proof_trees.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/names.cmi lib/pp.cmi kernel/sign.cmi lib/stamps.cmi \ kernel/term.cmi lib/util.cmi @@ -137,11 +140,16 @@ tactics/tactics.cmi: proofs/clenv.cmi kernel/evd.cmi kernel/names.cmi \ tactics/termdn.cmi: tactics/dn.cmi kernel/generic.cmi kernel/term.cmi tactics/wcclausenv.cmi: proofs/clenv.cmi kernel/evd.cmi kernel/names.cmi \ proofs/proof_trees.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi +toplevel/command.cmi: parsing/coqast.cmi library/declare.cmi kernel/names.cmi \ + proofs/tacred.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 \ kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi +toplevel/metasyntax.cmi: parsing/coqast.cmi parsing/extend.cmi toplevel/mltop.cmi: library/libobject.cmi toplevel/protectedtoplevel.cmi: lib/pp.cmi +toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \ + kernel/term.cmi toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi toplevel/vernacentries.cmi: kernel/names.cmi kernel/term.cmi \ @@ -262,8 +270,8 @@ lib/gset.cmo: lib/gset.cmi lib/gset.cmx: lib/gset.cmi lib/hashcons.cmo: lib/hashcons.cmi lib/hashcons.cmx: lib/hashcons.cmi -lib/options.cmo: lib/options.cmi -lib/options.cmx: lib/options.cmi +lib/options.cmo: lib/util.cmi lib/options.cmi +lib/options.cmx: lib/util.cmx lib/options.cmi 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 @@ -352,20 +360,28 @@ parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi lib/hashcons.cmi \ kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx lib/hashcons.cmx \ kernel/names.cmx parsing/pcoq.cmi lib/pp.cmx lib/util.cmx parsing/ast.cmi -parsing/astterm.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \ - kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \ - kernel/generic.cmi library/global.cmi library/impargs.cmi \ +parsing/astterm.cmo: parsing/ast.cmi toplevel/command.cmi parsing/coqast.cmi \ + library/declare.cmi kernel/environ.cmi pretyping/evarutil.cmi \ + kernel/evd.cmi kernel/generic.cmi library/global.cmi library/impargs.cmi \ kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi pretyping/pretyping.cmi \ - pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi \ - pretyping/typing.cmi lib/util.cmi toplevel/vernac.cmi parsing/astterm.cmi -parsing/astterm.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \ - kernel/environ.cmx pretyping/evarutil.cmx kernel/evd.cmx \ - kernel/generic.cmx library/global.cmx library/impargs.cmx \ + pretyping/rawterm.cmi kernel/reduction.cmi kernel/sign.cmi \ + kernel/term.cmi pretyping/typing.cmi lib/util.cmi toplevel/vernac.cmi \ + parsing/astterm.cmi +parsing/astterm.cmx: parsing/ast.cmx toplevel/command.cmi parsing/coqast.cmx \ + library/declare.cmx kernel/environ.cmx pretyping/evarutil.cmx \ + kernel/evd.cmx kernel/generic.cmx library/global.cmx library/impargs.cmx \ kernel/names.cmx parsing/pcoq.cmi lib/pp.cmx pretyping/pretyping.cmx \ - pretyping/rawterm.cmi kernel/sign.cmx kernel/term.cmx \ - pretyping/typing.cmx lib/util.cmx toplevel/vernac.cmx parsing/astterm.cmi + pretyping/rawterm.cmi kernel/reduction.cmx kernel/sign.cmx \ + kernel/term.cmx pretyping/typing.cmx lib/util.cmx toplevel/vernac.cmx \ + parsing/astterm.cmi parsing/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi parsing/coqast.cmi parsing/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx parsing/coqast.cmi +parsing/egrammar.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \ + parsing/lexer.cmi parsing/pcoq.cmi lib/pp.cmi lib/util.cmi \ + parsing/egrammar.cmi +parsing/egrammar.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmi \ + parsing/lexer.cmx parsing/pcoq.cmi lib/pp.cmx lib/util.cmx \ + parsing/egrammar.cmi parsing/esyntax.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \ lib/gmap.cmi lib/gmapl.cmi lib/pp.cmi lib/util.cmi parsing/esyntax.cmi parsing/esyntax.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmi \ @@ -512,14 +528,16 @@ proofs/macros.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \ library/libobject.cmx library/library.cmx kernel/names.cmx \ parsing/pcoq.cmi lib/pp.cmx proofs/proof_trees.cmx library/summary.cmx \ kernel/term.cmx lib/util.cmx proofs/macros.cmi -proofs/pfedit.cmo: kernel/constant.cmi library/declare.cmi lib/edit.cmi \ - kernel/evd.cmi kernel/generic.cmi library/global.cmi library/lib.cmi \ - kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi kernel/sign.cmi \ - proofs/tacmach.cmi kernel/term.cmi lib/util.cmi proofs/pfedit.cmi -proofs/pfedit.cmx: kernel/constant.cmx library/declare.cmx lib/edit.cmx \ - kernel/evd.cmx kernel/generic.cmx library/global.cmx library/lib.cmx \ - kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx kernel/sign.cmx \ - proofs/tacmach.cmx kernel/term.cmx lib/util.cmx proofs/pfedit.cmi +proofs/pfedit.cmo: parsing/astterm.cmi kernel/constant.cmi \ + library/declare.cmi lib/edit.cmi kernel/environ.cmi kernel/evd.cmi \ + kernel/generic.cmi library/global.cmi library/lib.cmi kernel/names.cmi \ + lib/pp.cmi proofs/proof_trees.cmi kernel/sign.cmi proofs/tacmach.cmi \ + kernel/term.cmi pretyping/typing.cmi lib/util.cmi proofs/pfedit.cmi +proofs/pfedit.cmx: parsing/astterm.cmx kernel/constant.cmx \ + library/declare.cmx lib/edit.cmx kernel/environ.cmx kernel/evd.cmx \ + kernel/generic.cmx library/global.cmx library/lib.cmx kernel/names.cmx \ + lib/pp.cmx proofs/proof_trees.cmx kernel/sign.cmx proofs/tacmach.cmx \ + kernel/term.cmx pretyping/typing.cmx lib/util.cmx proofs/pfedit.cmi proofs/proof_trees.cmo: parsing/ast.cmi parsing/coqast.cmi kernel/environ.cmi \ kernel/evd.cmi kernel/names.cmi lib/pp.cmi parsing/pretty.cmi \ parsing/printer.cmi kernel/sign.cmi lib/stamps.cmi kernel/term.cmi \ @@ -686,6 +704,14 @@ toplevel/himsg.cmo: kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \ toplevel/himsg.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \ lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \ kernel/type_errors.cmx lib/util.cmx toplevel/himsg.cmi +toplevel/metasyntax.cmo: parsing/ast.cmi parsing/coqast.cmi \ + parsing/egrammar.cmi parsing/esyntax.cmi parsing/extend.cmi \ + library/lib.cmi library/libobject.cmi library/library.cmi \ + parsing/pcoq.cmi lib/pp.cmi library/summary.cmi toplevel/metasyntax.cmi +toplevel/metasyntax.cmx: parsing/ast.cmx parsing/coqast.cmx \ + parsing/egrammar.cmx parsing/esyntax.cmx parsing/extend.cmi \ + library/lib.cmx library/libobject.cmx library/library.cmx \ + parsing/pcoq.cmi lib/pp.cmx library/summary.cmx toplevel/metasyntax.cmi toplevel/minicoq.cmo: kernel/constant.cmi parsing/g_minicoq.cmi \ kernel/generic.cmi toplevel/himsg.cmi kernel/inductive.cmi \ kernel/names.cmi lib/pp.cmi kernel/safe_typing.cmi kernel/sign.cmi \ @@ -722,26 +748,30 @@ toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \ lib/options.cmx parsing/pcoq.cmi proofs/pfedit.cmx lib/pp.cmx \ library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \ toplevel/vernac.cmi -toplevel/vernacentries.cmo: parsing/ast.cmi pretyping/class.cmi \ - pretyping/classops.cmi parsing/coqast.cmi library/declare.cmi \ - kernel/environ.cmi kernel/evd.cmi parsing/extend.cmi library/global.cmi \ - library/libobject.cmi library/library.cmi proofs/macros.cmi \ - kernel/names.cmi library/nametab.cmi lib/options.cmi parsing/pcoq.cmi \ - proofs/pfedit.cmi lib/pp.cmi lib/pp_control.cmi parsing/pretty.cmi \ +toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \ + pretyping/classops.cmi toplevel/command.cmi parsing/coqast.cmi \ + library/declare.cmi kernel/environ.cmi kernel/evd.cmi parsing/extend.cmi \ + library/global.cmi library/goptions.cmi library/impargs.cmi \ + library/lib.cmi library/libobject.cmi library/library.cmi \ + proofs/macros.cmi toplevel/metasyntax.cmi kernel/names.cmi \ + library/nametab.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \ + lib/pp.cmi lib/pp_control.cmi parsing/pretty.cmi parsing/printer.cmi \ proofs/proof_trees.cmi kernel/reduction.cmi proofs/refiner.cmi \ - lib/stamps.cmi library/states.cmi lib/system.cmi proofs/tacmach.cmi \ - kernel/term.cmi pretyping/typing.cmi toplevel/vernacinterp.cmi \ - toplevel/vernacentries.cmi -toplevel/vernacentries.cmx: parsing/ast.cmx pretyping/class.cmi \ - pretyping/classops.cmx parsing/coqast.cmx library/declare.cmx \ - kernel/environ.cmx kernel/evd.cmx parsing/extend.cmi library/global.cmx \ - library/libobject.cmx library/library.cmx proofs/macros.cmx \ - kernel/names.cmx library/nametab.cmx lib/options.cmx parsing/pcoq.cmi \ - proofs/pfedit.cmx lib/pp.cmx lib/pp_control.cmx parsing/pretty.cmx \ + toplevel/searchisos.cmi lib/stamps.cmi library/states.cmi lib/system.cmi \ + proofs/tacmach.cmi kernel/term.cmi kernel/typeops.cmi lib/util.cmi \ + toplevel/vernacinterp.cmi toplevel/vernacentries.cmi +toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \ + pretyping/classops.cmx toplevel/command.cmi parsing/coqast.cmx \ + library/declare.cmx kernel/environ.cmx kernel/evd.cmx parsing/extend.cmi \ + library/global.cmx library/goptions.cmx library/impargs.cmx \ + library/lib.cmx library/libobject.cmx library/library.cmx \ + proofs/macros.cmx toplevel/metasyntax.cmx kernel/names.cmx \ + library/nametab.cmx lib/options.cmx parsing/pcoq.cmi proofs/pfedit.cmx \ + lib/pp.cmx lib/pp_control.cmx parsing/pretty.cmx parsing/printer.cmx \ proofs/proof_trees.cmx kernel/reduction.cmx proofs/refiner.cmx \ - lib/stamps.cmx library/states.cmx lib/system.cmx proofs/tacmach.cmx \ - kernel/term.cmx pretyping/typing.cmx toplevel/vernacinterp.cmx \ - toplevel/vernacentries.cmi + toplevel/searchisos.cmi lib/stamps.cmx library/states.cmx lib/system.cmx \ + proofs/tacmach.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx \ + toplevel/vernacinterp.cmx toplevel/vernacentries.cmi toplevel/vernacinterp.cmo: parsing/ast.cmi parsing/coqast.cmi lib/dyn.cmi \ toplevel/himsg.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \ proofs/proof_trees.cmi proofs/tacinterp.cmi lib/util.cmi \ diff --git a/Makefile b/Makefile index 99d19a0aa6..c46f30851d 100644 --- a/Makefile +++ b/Makefile @@ -57,7 +57,8 @@ PRETYPING=pretyping/typing.cmo pretyping/classops.cmo pretyping/recordops.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 \ parsing/g_command.cmo parsing/g_tactic.cmo parsing/g_multiple_case.cmo\ - parsing/printer.cmo parsing/pretty.cmo parsing/astterm.cmo + parsing/printer.cmo parsing/pretty.cmo parsing/astterm.cmo \ + parsing/egrammar.cmo PROOFS=proofs/tacred.cmo \ proofs/proof_trees.cmo proofs/logic.cmo \ @@ -71,6 +72,7 @@ TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \ tactics/tacentries.cmo tactics/hiddentac.cmo tactics/elim.cmo TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernacinterp.cmo \ + toplevel/metasyntax.cmo \ toplevel/vernacentries.cmo toplevel/vernac.cmo toplevel/mltop.cmo \ toplevel/protectedtoplevel.cmo toplevel/toplevel.cmo @@ -91,6 +93,7 @@ link: $(LINK) ocamlc -custom $(INCLUDES) -o link $(CMA) $(LINK) $(OSDEPLIBS) rm -f link +lib: $(LIB) kernel: $(KERNEL) library: $(LIBRARY) proofs: $(PROOFS) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 0d2d5cba50..0824c192cf 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -937,3 +937,27 @@ let type_fixpoint env sigma lna lar vdefj = (Array.map (fun j -> j.uj_type) vdefj) (Array.map body_of_type lar) with IllBranch i -> error_ill_typed_rec_body CCI env i lna vdefj lar + + +(* A function which checks that a term well typed verifies both + syntaxic conditions *) + +let control_only_guard env sigma = + let rec control_rec = function + | Rel(p) -> () + | VAR _ -> () + | DOP0(_) -> () + | DOPN(CoFix(_),cl) as cofix -> + check_cofix env sigma cofix; + Array.iter control_rec cl + | DOPN(Fix(_),cl) as fix -> + check_fix env sigma fix; + Array.iter control_rec cl + | DOPN(_,cl) -> Array.iter control_rec cl + | DOPL(_,cl) -> List.iter control_rec cl + | DOP1(_,c) -> control_rec c + | DOP2(_,c1,c2) -> control_rec c1; control_rec c2 + | DLAM(_,c) -> control_rec c + | DLAMV(_,v) -> Array.iter control_rec v + in + control_rec diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 4f47bfd886..b935efd8c6 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -64,6 +64,7 @@ val apply_rel_list : val check_fix : env -> 'a evar_map -> constr -> unit val check_cofix : env -> 'a evar_map -> constr -> unit +val control_only_guard : env -> 'a evar_map -> constr -> unit val type_fixpoint : env -> 'a evar_map -> name list -> typed_type array -> unsafe_judgment array -> constraints diff --git a/lib/options.ml b/lib/options.ml index c4afa1e390..c0f14ee30b 100644 --- a/lib/options.ml +++ b/lib/options.ml @@ -1,6 +1,8 @@ (* $Id$ *) +open Util + let batch_mode = ref false let debug = ref false @@ -41,3 +43,10 @@ let without_mes_ambig f x = try make_mes_ambig false; let rslt = f x in (make_mes_ambig old; rslt) with e -> (make_mes_ambig old; raise e) + +(* A list of the areas of the system where "unsafe" operation + * has been requested *) +let unsafe_set = ref Stringset.empty +let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set +let is_unsafe s = Stringset.mem s !unsafe_set + diff --git a/lib/options.mli b/lib/options.mli index 528226360e..9137883523 100644 --- a/lib/options.mli +++ b/lib/options.mli @@ -22,3 +22,6 @@ val make_mes_ambig : bool -> unit val is_mes_ambig : unit -> bool val without_mes_ambig : ('a -> 'b) -> 'a -> 'b +val add_unsafe : string -> unit +val is_unsafe : string -> bool + diff --git a/lib/system.ml b/lib/system.ml index 0f005bd47f..9da302d302 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -3,6 +3,7 @@ open Pp open Util +open Unix (* Files and load path. *) @@ -14,6 +15,37 @@ let del_path dir = if List.mem dir !load_path then load_path := List.filter (fun s -> s <> dir) !load_path +let search_paths () = !load_path + +(* All subdirectories, recursively *) + +let all_subdirs dir = + let l = ref [] in + let add f = l := f :: !l in + let rec traverse dir = + Printf.printf "%s\n" dir; + let dirh = + try opendir dir with Unix_error _ -> invalid_arg "all_subdirs" + in + try + while true do + let f = readdir dirh in + if f <> "." && f <> ".." then + let file = Filename.concat dir f in + if (stat file).st_kind = S_DIR then begin + add file; + traverse file + end + done + with End_of_file -> + closedir dirh + in + traverse dir; List.rev !l + +let radd_path dir = List.iter add_path (all_subdirs dir) + + + (* TODO: rétablir glob (expansion ~user et $VAR) si on le juge nécessaire *) let glob s = s @@ -50,26 +82,6 @@ let is_in_path lpath filename = let make_suffix name suffix = if Filename.check_suffix name suffix then name else (name ^ suffix) -(*Gives the list of all the directories under dir*) -let alldir dir = - let ini = Unix.getcwd() - and tmp = Filename.temp_file "coq" "rec" - and lst = ref [] in - Unix.chdir dir; - let bse = Unix.getcwd() in - let _ = Sys.command ("find "^bse^" -type d >> "^tmp) in - let inf = open_in tmp in - try - while true do - lst := !lst @ [input_line inf] - done; - [] - with End_of_file -> - close_in inf; - Sys.remove tmp; - Unix.chdir ini; - !lst - 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) diff --git a/lib/system.mli b/lib/system.mli index 6f89901aa5..0c4bbd2284 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -3,7 +3,7 @@ (*s Files. *) -val alldir : string -> string list +val all_subdirs : string -> string list val is_in_path : string list -> string -> bool val where_in_path : string list -> string -> string @@ -15,6 +15,9 @@ val glob : string -> string val add_path : string -> unit val del_path : string -> unit +val radd_path : string -> unit + +val search_paths : unit -> string list val find_file_in_path : string -> string diff --git a/lib/util.ml b/lib/util.ml index 59f119a50c..0cab4540e2 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -207,6 +207,12 @@ let list_map_append f l = List.flatten (List.map f l) let list_map_append2 f l1 l2 = List.flatten (List.map2 f l1 l2) +let list_share_tails l1 l2 = + let rec shr_rev acc = function + | ((x1::l1), (x2::l2)) when x1 == x2 -> shr_rev (x1::acc) (l1,l2) + | (l1,l2) -> (List.rev l1, List.rev l2, acc) + in + shr_rev [] (List.rev l1, List.rev l2) (* Arrays *) diff --git a/lib/util.mli b/lib/util.mli index b8b72da090..a3a20aaacf 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -62,6 +62,7 @@ val list_prefix_of : 'a list -> 'a list -> bool val list_map_append : ('a -> 'b list) -> 'a list -> 'b list (* raises [Invalid_argument] if the two lists don't have the same length *) val list_map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list +val list_share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list (*s Arrays. *) diff --git a/library/declare.ml b/library/declare.ml index 067274aa73..7dca2b1c8a 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -22,18 +22,29 @@ let make_strength = function | [] -> NeverDischarge | l -> DischargeAt (sp_of_wd l) +let make_strength_0 () = make_strength (Lib.cwd()) + +let make_strength_1 () = + let path = try List.tl (List.tl (Lib.cwd())) with Failure _ -> [] in + make_strength path + +let make_strength_2 () = + let path = try List.tl (Lib.cwd()) with Failure _ -> [] in + make_strength path + + (* Variables. *) -type variable_declaration = identifier * constr * strength * bool +type variable_declaration = constr * strength * bool -let vartab = ref (Spmap.empty : variable_declaration Spmap.t) +let vartab = ref (Spmap.empty : (identifier * variable_declaration) Spmap.t) let _ = Summary.declare_summary "VARIABLE" { Summary.freeze_function = (fun () -> !vartab); Summary.unfreeze_function = (fun ft -> vartab := ft); Summary.init_function = (fun () -> vartab := Spmap.empty) } -let cache_variable (sp,((id,ty,_,_) as vd)) = +let cache_variable (sp,(id,(ty,_,_) as vd)) = Global.push_var (id,ty); Nametab.push id sp; vartab := Spmap.add sp vd !vartab @@ -55,9 +66,9 @@ let (in_variable, out_variable) = specification_function = specification_variable } in declare_object ("VARIABLE", od) -let declare_variable ((id,ty,_,_) as obj) = +let declare_variable id ((ty,_,_) as obj) = Global.push_var (id,ty); - let sp = add_leaf id CCI (in_variable obj) in + let sp = add_leaf id CCI (in_variable (id,obj)) in Nametab.push id sp (* Parameters. *) @@ -86,7 +97,7 @@ let declare_parameter id c = (* Constants. *) -type constant_declaration = identifier * constant_entry * strength * bool +type constant_declaration = constant_entry * strength * bool let csttab = ref (Spmap.empty : constant_declaration Spmap.t) @@ -114,7 +125,7 @@ let (in_constant, out_constant) = specification_function = specification_constant } in declare_object ("CONSTANT", od) -let declare_constant ((id,ce,_,_) as cd) = +let declare_constant id ((ce,_,_) as cd) = let sp = add_leaf id CCI (in_constant ce) in Global.add_constant sp ce; Nametab.push (basename sp) sp; @@ -204,13 +215,13 @@ let is_variable id = let sp = Nametab.sp_of_id CCI id in Spmap.mem sp !vartab let out_variable sp = - let (id,_,str,sticky) = Spmap.find sp !vartab in + let (id,(_,str,sticky)) = Spmap.find sp !vartab in let (_,ty) = Global.lookup_var id in (id,ty,str,sticky) let variable_strength id = let sp = Nametab.sp_of_id CCI id in - let (_,_,str,_) = Spmap.find sp !vartab in + let _,(_,str,_) = Spmap.find sp !vartab in str (* Global references. *) @@ -293,8 +304,8 @@ let declare_eliminations sp = let redmind = minductype_spec env sigma mind in let mindstr = string_of_id mindid in let declare na c = - declare_constant - (id_of_string na, { const_entry_body = c; const_entry_type = None }, + declare_constant (id_of_string na) + ({ const_entry_body = c; const_entry_type = None }, false, NeverDischarge) in let mispec = Global.lookup_mind_specif redmind in diff --git a/library/declare.mli b/library/declare.mli index 952fa0500b..1a9a0fac21 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -20,14 +20,14 @@ type strength = | DischargeAt of section_path | NeverDischarge -type variable_declaration = identifier * constr * strength * bool +type variable_declaration = constr * strength * bool -val declare_variable : variable_declaration -> unit +val declare_variable : identifier -> variable_declaration -> unit -type constant_declaration = identifier * constant_entry * strength * bool +type constant_declaration = constant_entry * strength * bool -val declare_constant : constant_declaration -> unit +val declare_constant : identifier -> constant_declaration -> unit val declare_parameter : identifier -> constr -> unit @@ -41,6 +41,9 @@ val declare_eliminations : section_path -> unit val declare_syntax_constant : identifier -> constr -> unit val make_strength : string list -> strength +val make_strength_0 : unit -> strength +val make_strength_1 : unit -> strength +val make_strength_2 : unit -> strength (*s Corresponding test and access functions. *) diff --git a/library/impargs.ml b/library/impargs.ml index 2cc34c3cb4..cd9a5ef4e1 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -15,6 +15,21 @@ type implicits = let implicit_args = ref false +let make_implicit_args flag = implicit_args := flag +let is_implicit_args () = !implicit_args + +let implicitely f x = + let oimplicit = !implicit_args in + try + implicit_args := true; + let rslt = f x in + implicit_args := oimplicit; + rslt + with e -> begin + implicit_args := oimplicit; + raise e + end + let auto_implicits ty = if !implicit_args then let genv = Global.env() in diff --git a/library/impargs.mli b/library/impargs.mli index 51ada5845a..8a598ef7e8 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -14,7 +14,9 @@ type implicits = | Impl_manual of int list | No_impl -val implicit_args : bool ref +val make_implicit_args : bool -> unit +val is_implicit_args : unit -> bool +val implicitely : ('a -> 'b) -> 'a -> 'b val list_of_implicits : implicits -> int list diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 18a9b09a74..a9a8e0d3b6 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -8,14 +8,17 @@ open Sign open Generic open Term open Constant +open Environ open Evd open Declare +open Typing open Tacmach open Proof_trees open Lib +open Astterm type proof_topstate = { - top_hyps : var_context * var_context; + top_hyps : env * env; top_goal : goal; top_strength : strength } @@ -61,8 +64,8 @@ let get_evmap_sign og = None in match og with - | Some goal -> (project goal, pf_hyps goal) - | _ -> (Evd.empty, Global.var_context()) + | Some goal -> (project goal, pf_env goal) + | _ -> (Evd.empty, Global.env()) let set_proof s = try @@ -171,8 +174,9 @@ let save_named opacity = let {evar_concl=concl} = ts.top_goal and strength = ts.top_strength in let pfterm = extract_pftreestate pfs in - declare_constant (id_of_string ident) (*** opacity strength ***) - { const_entry_body = pfterm; const_entry_type = Some concl }; + declare_constant (id_of_string ident) + ({ const_entry_body = pfterm; const_entry_type = Some concl }, + strength, opacity); del_proof ident; message(ident ^ " is defined") @@ -183,12 +187,14 @@ let save_anonymous opacity save_ident n = and strength = ts.top_strength in let pfterm = extract_pftreestate pfs in if ident = "Unnamed_thm" then - declare_constant (id_of_string save_ident) (*** opacity,strength ***) - { const_entry_body = pfterm; const_entry_type = Some concl } + declare_constant (id_of_string save_ident) + ({ const_entry_body = pfterm; const_entry_type = Some concl }, + strength, opacity) else begin message("Overriding name " ^ ident ^ " and using " ^ save_ident); - declare_constant (id_of_string save_ident) (*** opacity,strength ***) - { const_entry_body = pfterm; const_entry_type = Some concl } + declare_constant (id_of_string save_ident) + ({ const_entry_body = pfterm; const_entry_type = Some concl }, + strength, opacity) end; del_proof ident; message(save_ident ^ " is defined") @@ -241,10 +247,10 @@ and reset_initial () = restore_state "Initial" (* Modifying the current prooftree *) (*********************************************************************) -let start_proof_with_type na str sign fsign concl = - let top_goal = mk_goal (mt_ctxt Intset.empty) sign concl in +let start_proof_with_type na str env concl = + let top_goal = mk_goal (mt_ctxt Intset.empty) env concl in let ts = { - top_hyps = (sign,fsign); + top_hyps = (env,empty_env); top_goal = top_goal; top_strength = str } in @@ -252,14 +258,16 @@ let start_proof_with_type na str sign fsign concl = set_proof (Some na) let start_proof na str concl_com = - let (sigma,(sign,fsign)) = initial_sigma_assumptions() in - let concl = fconstruct_type sigma sign concl_com in - start_proof_with_type na str sign fsign concl.body + let sigma = Evd.empty in + let env = Global.env() in + let concl = fconstruct_type sigma (Environ.context env) concl_com in + start_proof_with_type na str env concl.body let start_proof_constr na str concl = - let (sigma,(sign,fsign)) = initial_sigma_assumptions() in - let _ = type_of_type sigma sign concl in - start_proof_with_type na str sign fsign concl + let sigma = Evd.empty in + let env = Global.env() in + let _ = execute_type env sigma concl in + start_proof_with_type na str env concl let solve_nth k tac = let pft = get_pftreestate() in @@ -301,7 +309,7 @@ let traverse n = rev_mutate (traverse n) let rec nth_cdr = function | 0 -> (function l -> l) - | n -> (comp List.tl (nth_cdr (n - 1))) + | n -> (compose List.tl (nth_cdr (n - 1))) let rec common_ancestor_equal_length = function | ((a::l1), (b::l2)) -> @@ -319,7 +327,7 @@ let rec common_ancestor_equal_length = function let common_ancestor l1 l2 = let diff_lengths = (List.length l1) - (List.length l2) in if diff_lengths > 0 then - let head,tail = chop_list diff_lengths l1 in + let head,tail = list_chop diff_lengths l1 in let (prefx,n) = common_ancestor_equal_length (tail,l2) in (head@prefx),n else if diff_lengths < 0 then @@ -347,3 +355,11 @@ let traverse_to path = (* traverse the proof tree until it reach the nth subgoal *) let traverse_nth_goal n = mutate (nth_unproven n) + +(* The goal focused on *) +let focus_n = ref 0 +let make_focus n = focus_n := n +let focus () = !focus_n +let focused_goal () = let n = !focus_n in if n=0 then 1 else n + + diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 7a953dff6e..3e86b38624 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -3,7 +3,9 @@ (*i*) open Pp +open Term open Sign +open Environ open Declare open Proof_trees open Tacmach @@ -11,21 +13,27 @@ open Tacmach val proof_prompt : unit -> string val refining : unit -> bool +val abort_goal : string -> unit +val abort_cur_goal : unit -> unit +val abort_goals : unit -> unit +val abort_refine : ('a -> 'b) -> 'a -> 'b val msg_proofs : bool -> std_ppcmds val undo_limit : int ref val set_undo : int -> unit val unset_undo : unit -> unit +val undo : int -> unit +val resume_last : unit -> unit type proof_topstate = { - top_hyps : context * context; + top_hyps : env * env; top_goal : goal; top_strength : strength } val get_state : unit -> pftreestate * proof_topstate val get_topstate : unit -> proof_topstate val get_pftreestate : unit -> pftreestate -val get_evmap_sign : int option -> evar_declarations * context +val get_evmap_sign : int option -> evar_declarations * env val set_proof : string option -> unit val get_proof : unit -> string val list_proofs : unit -> string list @@ -33,6 +41,27 @@ val add_proof : string * pftreestate * proof_topstate -> unit val del_proof : string -> unit val init_proofs : unit -> unit +val mutate : (pftreestate -> pftreestate) -> unit +val rev_mutate : (pftreestate -> pftreestate) -> unit +val start : string * proof_topstate -> unit +val restart : unit -> unit +val proof_prompt : unit -> string +val proof_term : unit -> constr + +val start_proof : string -> strength -> Coqast.t -> unit +val start_proof_constr : string -> strength -> constr -> unit + +val save_named : bool -> unit +val save_anonymous : bool -> string -> 'a -> unit +val save_anonymous_thm : bool -> string -> unit +val save_anonymous_remark : bool -> string -> unit + +val solve_nth : int -> tactic -> unit +val by : tactic -> unit +val traverse : int -> unit +val traverse_nth_goal : int -> unit +val traverse_to : int list -> unit + val make_focus : int -> unit val focus : unit -> int val focused_goal : unit -> int diff --git a/tactics/pattern.ml b/tactics/pattern.ml index 297b26bb8e..52b6586b5c 100644 --- a/tactics/pattern.ml +++ b/tactics/pattern.ml @@ -31,7 +31,7 @@ let rec whd_replmeta = function let raw_sopattern_of_compattern sign com = failwith "raw_sopattern_of_compattern: TODO" (*** - let c = Astterm.raw_constr_of_compattern empty_evd (gLOB sign) com in + let c = Astterm.raw_constr_of_compattern Evd.empty (gLOB sign) com in strong whd_replmeta c ***) -- cgit v1.2.3