From 1f2ec6429da2b09b58480c35e175428e39c1c37b Mon Sep 17 00:00:00 2001 From: filliatr Date: Fri, 10 Dec 1999 14:51:04 +0000 Subject: - erreurs Pretype - Write / Restore State git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@230 85f007b7-540e-0410-9357-904b9bb8a0f7 --- config/Makefile.template | 3 +++ config/coq_config.mli | 2 ++ configure | 13 +++++++++---- library/states.ml | 3 ++- parsing/g_vernac.ml4 | 21 +++++++++------------ pretyping/pretype_errors.ml | 19 ++++++++++--------- pretyping/pretype_errors.mli | 2 -- proofs/pfedit.ml | 10 ---------- proofs/pfedit.mli | 2 -- toplevel/coqinit.ml | 16 ++++++++-------- toplevel/vernacentries.ml | 30 +++++++++++++++++++----------- 11 files changed, 62 insertions(+), 59 deletions(-) diff --git a/config/Makefile.template b/config/Makefile.template index 8194bec77..6ae9ca84a 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -15,6 +15,9 @@ # ############################################################################# +# Local use (no installation) +LOCAL=LOCALINSTALLATION + # Paths for true installation # BINDIR=path where coqtop, coqc, coqmktop, coq-tex, coqdep, gallina and # do_Makefile will reside diff --git a/config/coq_config.mli b/config/coq_config.mli index cfc3e29cb..4d3258e6a 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -1,6 +1,8 @@ (* $Id$ *) +val local : bool (* local use (no installation) *) + val bindir : string (* where the binaries are installed *) val coqlib : string (* where the std library is installed *) diff --git a/configure b/configure index 8e49f3738..0ca4c98ba 100755 --- a/configure +++ b/configure @@ -27,6 +27,7 @@ coq_debug_flag= coq_profile_flag= byte_opt_tools=opt +local=false bindir_spec=no libdir_spec=no mandir_spec=no @@ -49,8 +50,9 @@ while : ; do mandir_spec=yes mandir=$2/man shift;; - -local|--local) bindir_spec=yes - bindir=$COQTOP/bin/${arch-`arch`} + -local|--local) local=true + bindir_spec=yes + bindir=$COQTOP libdir_spec=yes libdir=$COQTOP mandir_spec=yes @@ -365,7 +367,8 @@ rm -f $COQTOP/config/Makefile case $ARCH in win32) - sed -e "s|COQTOPDIRECTORY|$COQTOP|" \ + sed -e "s|LOCALINSTALLATION|$local|" \ + -e "s|COQTOPDIRECTORY|$COQTOP|" \ -e "s|COQVERSION|$VERSION|" \ -e "s|BINDIRDIRECTORY|`echo $BINDIR |sed -e 's|\\\|/|g'`|" \ -e "s|COQLIBDIRECTORY|`echo $LIBDIR |sed -e 's|\\\|/|g'`|" \ @@ -389,7 +392,8 @@ case $ARCH in -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \ $COQTOP/config/Makefile.template > $COQTOP/config/Makefile;; *) - sed -e "s|COQTOPDIRECTORY|$COQTOP|" \ + sed -e "s|LOCALINSTALLATION|$local|" \ + -e "s|COQTOPDIRECTORY|$COQTOP|" \ -e "s|COQVERSION|$VERSION|" \ -e "s|BINDIRDIRECTORY|$BINDIR|" \ -e "s|COQLIBDIRECTORY|$LIBDIR|" \ @@ -423,6 +427,7 @@ rm -f $mlconfig_file cat << END_OF_COQ_CONFIG > $mlconfig_file (* DO NOT EDIT THIS FILE: automatically generated by ../configure *) +let local = $local let bindir = "$BINDIR" let coqlib = "$LIBDIR" let coqtop = "$COQTOP" diff --git a/library/states.ml b/library/states.ml index be1241a9a..0e60caecb 100644 --- a/library/states.ml +++ b/library/states.ml @@ -12,7 +12,8 @@ let get_state () = let set_state (fl,fs) = Lib.unfreeze fl; - unfreeze_summaries fs + unfreeze_summaries fs; + Lib.declare_initial_state() let state_magic_number = 19764 diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 96b226be4..4fb5380f5 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -311,26 +311,23 @@ GEXTEND Gram END -(* State management *) GEXTEND Gram vernac: [ [ - IDENT "Save"; IDENT "State"; id = identarg; "." -> - <:ast< (SaveState $id "") >> - | IDENT "Save"; IDENT "State"; id = identarg; s = stringarg; "." -> - <:ast< (SaveState $id $s) >> - | IDENT "Write"; IDENT "States"; id = identarg; "." -> - <:ast< (WriteStates $id) >> - | IDENT "Write"; IDENT "States"; id = stringarg; "." -> - <:ast< (WriteStates $id) >> + +(* State management *) + IDENT "Write"; IDENT "State"; id = identarg; "." -> + <:ast< (WriteState $id) >> + | IDENT "Write"; IDENT "State"; s = stringarg; "." -> + <:ast< (WriteState $s) >> | IDENT "Restore"; IDENT "State"; id = identarg; "." -> <:ast< (RestoreState $id) >> - | IDENT "Remove"; IDENT "State"; id = identarg; "." -> - <:ast< (RemoveState $id) >> + | IDENT "Restore"; IDENT "State"; s = stringarg; "." -> + <:ast< (RestoreState $s) >> + | IDENT "Reset"; id = identarg; "." -> <:ast< (ResetName $id) >> | IDENT "Reset"; IDENT "Initial"; "." -> <:ast< (ResetInitial) >> | IDENT "Reset"; IDENT "Section"; id = identarg; "." -> <:ast< (ResetSection $id) >> - | IDENT "Reset"; id = identarg; "." -> <:ast< (ResetName $id) >> (* Modules and Sections *) diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index a88eeb7e2..4067d0064 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -7,40 +7,41 @@ open Environ open Type_errors open Rawterm -exception PretypeError of loc * path_kind * context * type_error +let raise_pretype_error (loc,k,ctx,te) = + raise (Stdpp.Exc_located (loc, TypeError(k,ctx,te))) let error_var_not_found_loc loc k s = - raise (PretypeError (loc,k, Global.context() (*bidon*), VarNotFound s)) + raise_pretype_error (loc,k, Global.context() (*bidon*), VarNotFound s) let error_cant_find_case_type_loc loc env expr = - raise (PretypeError (loc,CCI,context env,CantFindCaseType expr)) + raise_pretype_error (loc,CCI,context env,CantFindCaseType expr) let error_ill_formed_branch k env c i actty expty = raise (TypeError (k, context env, IllFormedBranch (c,i,actty,expty))) let error_number_branches_loc loc k env c ct expn = - raise (PretypeError (loc, k, context env, NumberBranches (c,ct,expn))) + raise_pretype_error (loc, k, context env, NumberBranches (c,ct,expn)) let error_case_not_inductive_loc loc k env c ct = - raise (PretypeError (loc, k, context env, CaseNotInductive (c,ct))) + raise_pretype_error (loc, k, context env, CaseNotInductive (c,ct)) (* Pattern-matching errors *) let error_bad_constructor_loc loc k cstr ind = - raise (PretypeError (loc, k, Global.context(), BadConstructor (cstr,ind))) + raise_pretype_error (loc, k, Global.context(), BadConstructor (cstr,ind)) let error_wrong_numarg_constructor_loc loc k c n = - raise (PretypeError (loc, k, Global.context(), WrongNumargConstructor (c,n))) + raise_pretype_error (loc, k, Global.context(), WrongNumargConstructor (c,n)) let error_wrong_predicate_arity_loc loc k env c n1 n2 = - raise (PretypeError (loc, k, context env, WrongPredicateArity (c,n1,n2))) + raise_pretype_error (loc, k, context env, WrongPredicateArity (c,n1,n2)) let error_needs_inversion k env x t = raise (TypeError (k, context env, NeedsInversion (x,t))) let error_ill_formed_branch_loc loc k env c i actty expty = - raise (PretypeError (loc, k, context env, IllFormedBranch (c,i,actty,expty))) + raise_pretype_error (loc, k, context env, IllFormedBranch (c,i,actty,expty)) let error_occur_check k env ev c = raise (TypeError (k, context env, OccurCheck (ev,c))) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 4671d097d..1292ad75c 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -13,8 +13,6 @@ open Rawterm (* The type of errors raised by the pretyper *) -exception PretypeError of loc * path_kind * context * type_error - val error_var_not_found_loc : loc -> path_kind -> identifier -> 'a diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 6ff3deb70..ab2a0c513 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -228,16 +228,6 @@ let abort_refine f x = f x (* used to be: error "Must save or abort current goal first" *) -let reset_name = abort_refine reset_name -(*** TODO -and reset_keeping_name = abort_refine reset_keeping -and reset_section = abort_refine raw_reset_section -and save_state = abort_refine States.raw_save_state -and restore_state = abort_refine States.raw_restore_state -and restore_last_saved_state = abort_refine States.raw_restore_last_saved_state -***) -and reset_initial = abort_refine Lib.reset_initial - (*********************************************************************) (* Modifying the current prooftree *) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index ab9dc3e43..13f7b6c1c 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -51,8 +51,6 @@ val proof_term : unit -> constr val start_proof : string -> strength -> Coqast.t -> unit val start_proof_constr : string -> strength -> constr -> unit -val reset_name : identifier -> unit -val reset_initial : unit -> unit val save_named : bool -> unit val save_anonymous : bool -> string -> 'a -> unit diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 474b247a6..33ee012cf 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -56,19 +56,19 @@ let getenv_else s dft = try Sys.getenv s with Not_found -> dft (* Initializes the LoadPath according to COQLIB and Coq_config *) let init_load_path () = - (* default load path; only if COQLIB is defined *) - let coqlib = getenv_else "COQLIB" Coq_config.coqlib in - let coqtop = getenv_else "COQTOP" Coq_config.coqtop in - if coqlib = coqtop then - (* local installation *) + if Coq_config.local then + (* local use (no installation) *) List.iter - (fun s -> add_include (Filename.concat coqtop s)) + (fun s -> add_include (Filename.concat Coq_config.coqtop s)) ("states" :: "dev" :: (List.map (fun s -> Filename.concat "theories" (hm2 s)) Coq_config.theories_dirs)) - else - add_include coqlib; + else begin + (* default load path; only if COQLIB is defined *) + let coqlib = getenv_else "COQLIB" Coq_config.coqlib in + add_include coqlib + end; let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in add_include camlp4; add_include "."; diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index ce3b0e957..93a330316 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -219,25 +219,38 @@ let _ = (* Managing states *) let _ = - add "SaveState" + add "WriteState" (function | [VARG_STRING file] -> - (fun () -> States.extern_state file) + (fun () -> Pfedit.abort_refine States.extern_state file) + | [VARG_IDENTIFIER id] -> + let file = string_of_id id in + (fun () -> Pfedit.abort_refine States.extern_state file) | _ -> bad_vernac_args "SaveState") let _ = - add "LoadState" + add "RestoreState" (function | [VARG_STRING file] -> - (fun () -> States.intern_state file) - | _ -> bad_vernac_args "RestoreState") + (fun () -> Pfedit.abort_refine States.intern_state file) + | [VARG_IDENTIFIER id] -> + let file = string_of_id id in + (fun () -> Pfedit.abort_refine States.intern_state file) + | _ -> bad_vernac_args "LoadState") (* Resetting *) +let _ = + add "ResetName" + (function + | [VARG_IDENTIFIER id] -> + (fun () -> Pfedit.abort_refine Lib.reset_name id) + | _ -> bad_vernac_args "ResetName") + let _ = add "ResetInitial" (function - | [] -> (fun () -> reset_initial ()) + | [] -> (fun () -> Pfedit.abort_refine Lib.reset_initial ()) | _ -> bad_vernac_args "ResetInitial") (*** @@ -249,11 +262,6 @@ let _ = | _ -> bad_vernac_args "ResetSection") ***) -let _ = - add "ResetName" - (function - | [VARG_IDENTIFIER id] -> (fun () -> Pfedit.reset_name id) - | _ -> bad_vernac_args "ResetName") (* Modules *) -- cgit v1.2.3