renamed `keep_derivs' to `proofs', and made an integer;
authorwenzelm
Sat Sep 01 00:14:16 2001 +0200 (2001-09-01)
changeset 11543d61b913431c5
parent 11542 2afde2de26d6
child 11544 97305ee424a9
renamed `keep_derivs' to `proofs', and made an integer;
lib/Tools/usedir
src/HOL/ex/mesontest.ML
src/Pure/Isar/session.ML
src/Pure/Thy/thm_deps.ML
src/Pure/proofterm.ML
     1.1 --- a/lib/Tools/usedir	Fri Aug 31 22:46:23 2001 +0200
     1.2 +++ b/lib/Tools/usedir	Sat Sep 01 00:14:16 2001 +0200
     1.3 @@ -50,7 +50,7 @@
     1.4  MODES=""
     1.5  RESET=false
     1.6  SESSION=""
     1.7 -PROOF=MinDeriv
     1.8 +PROOFS=0
     1.9  
    1.10  function getoptions()
    1.11  {
    1.12 @@ -84,7 +84,7 @@
    1.13          fi
    1.14          ;;
    1.15        p)
    1.16 -        PROOF="$OPTARG"
    1.17 +        PROOFS="$OPTARG"
    1.18          ;;
    1.19        r)
    1.20          RESET=true
    1.21 @@ -158,7 +158,7 @@
    1.22    [ "$COMPRESS" = true ] && OPT_C="-c"
    1.23  
    1.24    "$ISABELLE" \
    1.25 -    -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOF;" \
    1.26 +    -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS;" \
    1.27      $OPT_C -q -w $LOGIC $NAME > "$LOG" 2>&1
    1.28    RC="$?"
    1.29  else
    1.30 @@ -167,7 +167,7 @@
    1.31    LOG="$LOGDIR/$ITEM"
    1.32  
    1.33    "$ISABELLE" \
    1.34 -    -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOF; quit();" \
    1.35 +    -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS; quit();" \
    1.36      -r -q "$LOGIC" > "$LOG" 2>&1
    1.37    RC="$?"
    1.38    cd ..
     2.1 --- a/src/HOL/ex/mesontest.ML	Fri Aug 31 22:46:23 2001 +0200
     2.2 +++ b/src/HOL/ex/mesontest.ML	Sat Sep 01 00:14:16 2001 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4  
     2.5  show_hyps := false;
     2.6  
     2.7 -keep_derivs := MinDeriv;
     2.8 +proofs := 0;
     2.9  by (rtac ccontr 1);
    2.10  val [prem] = gethyps 1;
    2.11  val nnf = make_nnf prem;
    2.12 @@ -23,7 +23,7 @@
    2.13  
    2.14  Goal "False";
    2.15  by (resolve_tac goes 1);
    2.16 -keep_derivs := FullDeriv;
    2.17 +proofs := 2;
    2.18  
    2.19  by (prolog_step_tac horns 1);
    2.20  by (iter_deepen_prolog_tac horns);
     3.1 --- a/src/Pure/Isar/session.ML	Fri Aug 31 22:46:23 2001 +0200
     3.2 +++ b/src/Pure/Isar/session.ML	Sat Sep 01 00:14:16 2001 +0200
     3.3 @@ -11,7 +11,7 @@
     3.4    val name: unit -> string
     3.5    val welcome: unit -> string
     3.6    val use_dir:
     3.7 -    string list -> bool -> bool -> string -> string -> string -> string -> string -> deriv_kind -> unit
     3.8 +    string list -> bool -> bool -> string -> string -> string -> string -> string -> int -> unit
     3.9    val finish: unit -> unit
    3.10  end;
    3.11  
    3.12 @@ -78,14 +78,14 @@
    3.13         rpath := Some (Url.unpack rpath_str);
    3.14     (!rpath, rpath_str <> ""));
    3.15  
    3.16 -fun use_dir modes reset info doc parent name dump rpath_str der =
    3.17 -  Library.setmp print_mode (modes @ ! print_mode) (fn () =>
    3.18 -    (init reset parent name;
    3.19 -     Present.init info doc (path ()) name
    3.20 -       (if dump = "" then None else Some (Path.unpack dump)) (get_rpath rpath_str);
    3.21 -     Proofterm.keep_derivs := der;
    3.22 -     File.symbol_use root_file;
    3.23 -     finish ())) ()
    3.24 +fun use_dir modes reset info doc parent name dump rpath_str level =
    3.25 +  Library.setmp print_mode (modes @ ! print_mode)
    3.26 +    (Library.setmp Proofterm.proofs level (fn () =>
    3.27 +      (init reset parent name;
    3.28 +       Present.init info doc (path ()) name
    3.29 +         (if dump = "" then None else Some (Path.unpack dump)) (get_rpath rpath_str);
    3.30 +       File.symbol_use root_file;
    3.31 +       finish ()))) ()
    3.32    handle exn => (writeln (Toplevel.exn_message exn); exit 1);
    3.33  
    3.34  
     4.1 --- a/src/Pure/Thy/thm_deps.ML	Fri Aug 31 22:46:23 2001 +0200
     4.2 +++ b/src/Pure/Thy/thm_deps.ML	Sat Sep 01 00:14:16 2001 +0200
     4.3 @@ -22,8 +22,8 @@
     4.4  
     4.5  open Proofterm;
     4.6  
     4.7 -fun enable () = keep_derivs := ThmDeriv;
     4.8 -fun disable () = keep_derivs := MinDeriv;
     4.9 +fun enable () = if ! proofs = 0 then proofs := 1 else ();
    4.10 +fun disable () = proofs := 0;
    4.11  
    4.12  fun dest_thm_axm (PThm (nt, prf, _, _)) = (nt, prf)
    4.13    | dest_thm_axm (PAxm (n, _, _)) = ((n ^ " (Ax)", []), MinProof [])
     5.1 --- a/src/Pure/proofterm.ML	Fri Aug 31 22:46:23 2001 +0200
     5.2 +++ b/src/Pure/proofterm.ML	Sat Sep 01 00:14:16 2001 +0200
     5.3 @@ -10,8 +10,7 @@
     5.4  
     5.5  signature BASIC_PROOFTERM =
     5.6  sig
     5.7 -  datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv;
     5.8 -  val keep_derivs : deriv_kind ref
     5.9 +  val proofs: int ref
    5.10  
    5.11    datatype proof =
    5.12       PBound of int
    5.13 @@ -171,25 +170,28 @@
    5.14  
    5.15  (** proof objects with different levels of detail **)
    5.16  
    5.17 -datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv;
    5.18 +val proofs = ref 2;
    5.19  
    5.20 -val keep_derivs = ref FullDeriv;
    5.21 +fun err_illegal_level i =
    5.22 +  error ("Illegal level of detail for proof objects: " ^ string_of_int i);
    5.23  
    5.24  fun if_ora b = if b then oracles_of_proof else K;
    5.25  
    5.26  fun infer_derivs f (ora1, prf1) (ora2, prf2) =
    5.27    (ora1 orelse ora2, 
    5.28 -   case !keep_derivs of
    5.29 -     FullDeriv => f prf1 prf2
    5.30 -   | ThmDeriv => MinProof (mk_min_proof (mk_min_proof ([], prf1), prf2))
    5.31 -   | MinDeriv => MinProof (if_ora ora2 (if_ora ora1 [] prf1) prf2));
    5.32 +   case !proofs of
    5.33 +     2 => f prf1 prf2
    5.34 +   | 1 => MinProof (mk_min_proof (mk_min_proof ([], prf1), prf2))
    5.35 +   | 0 => MinProof (if_ora ora2 (if_ora ora1 [] prf1) prf2)
    5.36 +   | i => err_illegal_level i);
    5.37  
    5.38  fun infer_derivs' f (ora, prf) =
    5.39    (ora,
    5.40 -   case !keep_derivs of
    5.41 -     FullDeriv => f prf
    5.42 -   | ThmDeriv => MinProof (mk_min_proof ([], prf))
    5.43 -   | MinDeriv => MinProof (if_ora ora [] prf));
    5.44 +   case !proofs of
    5.45 +     2 => f prf
    5.46 +   | 1 => MinProof (mk_min_proof ([], prf))
    5.47 +   | 0 => MinProof (if_ora ora [] prf)
    5.48 +   | i => err_illegal_level i);
    5.49  
    5.50  fun (prf %%% t) = prf %% Some t;
    5.51  
    5.52 @@ -978,7 +980,7 @@
    5.53      val args = map (fn (v as Var (ixn, _)) =>
    5.54          if ixn mem nvs then Some v else None) (vars_of prop) @
    5.55        map Some (sort (make_ord atless) (term_frees prop));
    5.56 -    val opt_prf = if !keep_derivs=FullDeriv then
    5.57 +    val opt_prf = if ! proofs = 2 then
    5.58          #4 (shrink [] 0 (rewrite_prf fst (!(ProofData.get_sg sign))
    5.59            (foldr (uncurry implies_intr_proof) (hyps', prf))))
    5.60        else MinProof (mk_min_proof ([], prf));