tuned;
authorwenzelm
Tue May 17 10:19:44 2005 +0200 (2005-05-17)
changeset 159735fd94d84470f
parent 15972 8ac3803c8f73
child 15974 cef3d89d49d4
tuned;
NEWS
src/Pure/Isar/attrib.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/method.ML
src/Pure/Isar/object_logic.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/rule_cases.ML
src/Pure/Isar/session.ML
src/Pure/Isar/toplevel.ML
src/Pure/Syntax/ast.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/axclass.ML
     1.1 --- a/NEWS	Tue May 17 10:19:43 2005 +0200
     1.2 +++ b/NEWS	Tue May 17 10:19:44 2005 +0200
     1.3 @@ -6,41 +6,6 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 -* ML: The type Library.option is no more, along with the exception
     1.8 -  Library.OPTION: Isabelle now uses the standard option type.  The
     1.9 -  functions the, is_some, is_none, etc. are still in Library, but
    1.10 -  the constructors are now SOME and NONE instead of Some and None.
    1.11 -  They raise the exception Option.
    1.12 -
    1.13 -* ML: The exception LIST is no more, the standard exceptions Empty and
    1.14 -  Subscript, as well as Library.UnequalLengths are used instead.  This
    1.15 -  means that function like Library.hd and Library.tl are gone, as the
    1.16 -  standard hd and tl functions suffice.
    1.17 -
    1.18 -  A number of basic functions are now no longer exported to the top ML
    1.19 -  level, as they are variants of standard functions.  The following
    1.20 -  suggests how one can translate existing code:
    1.21 -
    1.22 -    the x = valOf x
    1.23 -    if_none x y = getOpt(x,y)
    1.24 -    is_some x = isSome x
    1.25 -    apsome f x = Option.map f x
    1.26 -    rev_append xs ys = List.revAppend(xs,ys)
    1.27 -    nth_elem(i,xs) = List.nth(xs,i)
    1.28 -    last_elem xs = List.last xs
    1.29 -    flat xss = List.concat xss
    1.30 -    seq fs = app fs
    1.31 -    partition P xs = List.partition P xs
    1.32 -    filter P xs = List.filter P xs
    1.33 -    mapfilter f xs = List.mapPartial f xs
    1.34 -
    1.35 -  The final four functions, take, drop, foldl, and foldr, are somewhat
    1.36 -  more complicated (especially the semantics of take and drop differ
    1.37 -  from the standard).
    1.38 -
    1.39 -  A simple solution to broken code is to include "open Library" at the
    1.40 -  beginning of a structure.  Everything after that will be as before.
    1.41 -
    1.42  * Theory headers: the new header syntax for Isar theories is
    1.43  
    1.44    theory <name>
    1.45 @@ -381,6 +346,30 @@
    1.46  
    1.47  *** ML ***
    1.48  
    1.49 +* Pure/library.ML no longer defines its own option datatype, but uses
    1.50 +  that of the SML basis, which has constructors NONE and SOME instead
    1.51 +  of None and Some, as well as exception Option.Option instead of
    1.52 +  OPTION.  The functions the, if_none, is_some, is_none have been
    1.53 +  adapted accordingly, while Option.map replaces apsome.
    1.54 +
    1.55 +* The exception LIST is no more, the standard exceptions Empty and
    1.56 +  Subscript, as well as Library.UnequalLengths are used instead.  This
    1.57 +  means that function like Library.hd and Library.tl are gone, as the
    1.58 +  standard hd and tl functions suffice.
    1.59 +
    1.60 +  A number of basic functions are now no longer exported to the ML
    1.61 +  toplevel, as they are variants of standard functions.  The following
    1.62 +  suggests how one can translate existing code:
    1.63 +
    1.64 +    rev_append xs ys = List.revAppend (xs, ys)
    1.65 +    nth_elem (i, xs) = List.nth (xs, i)
    1.66 +    last_elem xs = List.last xs
    1.67 +    flat xss = List.concat xss
    1.68 +    seq fs = app fs
    1.69 +    partition P xs = List.partition P xs
    1.70 +    filter P xs = List.filter P xs
    1.71 +    mapfilter f xs = List.mapPartial f xs
    1.72 +
    1.73  * Pure: output via the Isabelle channels of writeln/warning/error
    1.74    etc. is now passed through Output.output, with a hook for arbitrary
    1.75    transformations depending on the print_mode (cf. Output.add_mode --
     2.1 --- a/src/Pure/Isar/attrib.ML	Tue May 17 10:19:43 2005 +0200
     2.2 +++ b/src/Pure/Isar/attrib.ML	Tue May 17 10:19:44 2005 +0200
     2.3 @@ -241,10 +241,10 @@
     2.4  
     2.5  fun error_var msg xi = error (msg ^ Syntax.string_of_vname xi);
     2.6  
     2.7 -fun the_sort sorts xi = valOf (sorts xi)
     2.8 +fun the_sort sorts xi = the (sorts xi)
     2.9    handle Option.Option => error_var "No such type variable in theorem: " xi;
    2.10  
    2.11 -fun the_type types xi = valOf (types xi)
    2.12 +fun the_type types xi = the (types xi)
    2.13    handle Option.Option => error_var "No such variable in theorem: " xi;
    2.14  
    2.15  fun unify_types sign types ((unifier, maxidx), (xi, u)) =
    2.16 @@ -339,9 +339,9 @@
    2.17  
    2.18      mixed_insts |> List.app (fn (arg, (xi, _)) =>
    2.19        if is_tvar xi then
    2.20 -        Args.assign (SOME (Args.Typ (valOf (assoc (type_insts''', xi))))) arg
    2.21 +        Args.assign (SOME (Args.Typ (the (assoc (type_insts''', xi))))) arg
    2.22        else
    2.23 -        Args.assign (SOME (Args.Term (valOf (assoc (term_insts''', xi))))) arg);
    2.24 +        Args.assign (SOME (Args.Term (the (assoc (term_insts''', xi))))) arg);
    2.25  
    2.26      (context, thm''' |> RuleCases.save thm)
    2.27    end;
     3.1 --- a/src/Pure/Isar/calculation.ML	Tue May 17 10:19:43 2005 +0200
     3.2 +++ b/src/Pure/Isar/calculation.ML	Tue May 17 10:19:44 2005 +0200
     3.3 @@ -189,7 +189,7 @@
     3.4        | SOME calc => (false, Seq.map single (combine (calc @ facts))));
     3.5    in
     3.6      err_if state (initial andalso final) "No calculation yet";
     3.7 -    err_if state (initial andalso isSome opt_rules) "Initial calculation -- no rules to be given";
     3.8 +    err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
     3.9      calculations |> Seq.map (fn calc => (print (Proof.context_of state) calc;
    3.10          state |> maintain_calculation final calc))
    3.11    end;
     4.1 --- a/src/Pure/Isar/context_rules.ML	Tue May 17 10:19:43 2005 +0200
     4.2 +++ b/src/Pure/Isar/context_rules.ML	Tue May 17 10:19:44 2005 +0200
     4.3 @@ -111,7 +111,7 @@
     4.4  fun print_rules prt x (Rules {rules, ...}) =
     4.5    let
     4.6      fun prt_kind (i, b) =
     4.7 -      Pretty.big_list (valOf (assoc (kind_names, (i, b))) ^ ":")
     4.8 +      Pretty.big_list (the (assoc (kind_names, (i, b))) ^ ":")
     4.9          (List.mapPartial (fn (_, (k, th)) => if k = (i, b) then SOME (prt x th) else NONE)
    4.10            (sort (Int.compare o pairself fst) rules));
    4.11    in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
     5.1 --- a/src/Pure/Isar/method.ML	Tue May 17 10:19:43 2005 +0200
     5.2 +++ b/src/Pure/Isar/method.ML	Tue May 17 10:19:44 2005 +0200
     5.3 @@ -154,7 +154,7 @@
     5.4  (* shuffle *)
     5.5  
     5.6  fun prefer i = METHOD (K (Tactic.defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1)));
     5.7 -fun defer opt_i = METHOD (K (Tactic.defer_tac (getOpt (opt_i,1))));
     5.8 +fun defer opt_i = METHOD (K (Tactic.defer_tac (if_none opt_i 1)));
     5.9  
    5.10  
    5.11  (* insert *)
    5.12 @@ -263,7 +263,7 @@
    5.13  in
    5.14  
    5.15  fun rules_tac ctxt opt_lim =
    5.16 -  SELECT_GOAL (DEEPEN (2, getOpt (opt_lim,20)) (intpr_tac ctxt [] 0) 4 1);
    5.17 +  SELECT_GOAL (DEEPEN (2, if_none opt_lim 20) (intpr_tac ctxt [] 0) 4 1);
    5.18  
    5.19  end;
    5.20  
    5.21 @@ -376,12 +376,12 @@
    5.22                  NONE => types (a, ~1)
    5.23                | some => some)
    5.24            | types' xi = types xi;
    5.25 -        fun internal x = isSome (types' (x, ~1));
    5.26 +        fun internal x = is_some (types' (x, ~1));
    5.27          val used = Drule.add_used thm (Drule.add_used st []);
    5.28          val (ts, envT) =
    5.29            ProofContext.read_termTs_schematic ctxt internal types' sorts used (ss ~~ Ts);
    5.30          val envT' = map (fn (ixn, T) =>
    5.31 -          (TVar (ixn, valOf (rsorts ixn)), T)) envT @ Tinsts_env;
    5.32 +          (TVar (ixn, the (rsorts ixn)), T)) envT @ Tinsts_env;
    5.33          val cenv =
    5.34            map
    5.35              (fn (xi, t) =>
    5.36 @@ -735,7 +735,7 @@
    5.37  fun proof opt_text state =
    5.38    state
    5.39    |> Proof.assert_backward
    5.40 -  |> refine (getOpt (opt_text,default_text))
    5.41 +  |> refine (if_none opt_text default_text)
    5.42    |> Seq.map (Proof.goal_facts (K []))
    5.43    |> Seq.map Proof.enter_forward;
    5.44  
     6.1 --- a/src/Pure/Isar/object_logic.ML	Tue May 17 10:19:43 2005 +0200
     6.2 +++ b/src/Pure/Isar/object_logic.ML	Tue May 17 10:19:44 2005 +0200
     6.3 @@ -47,7 +47,7 @@
     6.4  
     6.5    fun merge_judgment (SOME x, SOME y) =
     6.6          if x = y then SOME x else error "Attempt to merge different object-logics"
     6.7 -    | merge_judgment (j1, j2) = if isSome j1 then j1 else j2;
     6.8 +    | merge_judgment (j1, j2) = if is_some j1 then j1 else j2;
     6.9  
    6.10    fun merge ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) =
    6.11      (merge_judgment (judgment1, judgment2),
    6.12 @@ -117,7 +117,7 @@
    6.13      val c = judgment_name sg;
    6.14      val aT = TFree ("'a", []);
    6.15      val T =
    6.16 -      getOpt (Sign.const_type sg c, aT --> propT)
    6.17 +      if_none (Sign.const_type sg c) (aT --> propT)
    6.18        |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
    6.19      val U = Term.domain_type T handle Match => aT;
    6.20    in Const (c, T) $ Free (x, U) end;
     7.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue May 17 10:19:43 2005 +0200
     7.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue May 17 10:19:44 2005 +0200
     7.3 @@ -280,7 +280,7 @@
     7.4    Source.of_list toks
     7.5    |> toplevel_source false true true get_parser
     7.6    |> Source.exhaust
     7.7 -  |> map (fn tr => (Toplevel.name_of tr, valOf (Toplevel.source_of tr), tr));
     7.8 +  |> map (fn tr => (Toplevel.name_of tr, the (Toplevel.source_of tr), tr));
     7.9  
    7.10  
    7.11  (** read theory **)
    7.12 @@ -299,7 +299,7 @@
    7.13      val pos = Path.position path;
    7.14      val (name', parents, files) = ThyHeader.scan (src, pos);
    7.15      val ml_path = ThyLoad.ml_path name;
    7.16 -    val ml_file = if ml andalso isSome (ThyLoad.check_file NONE ml_path) then [ml_path] else [];
    7.17 +    val ml_file = if ml andalso is_some (ThyLoad.check_file NONE ml_path) then [ml_path] else [];
    7.18    in
    7.19      if name <> name' then
    7.20        error ("Filename " ^ quote (Path.pack path) ^
     8.1 --- a/src/Pure/Isar/proof.ML	Tue May 17 10:19:43 2005 +0200
     8.2 +++ b/src/Pure/Isar/proof.ML	Tue May 17 10:19:44 2005 +0200
     8.3 @@ -793,7 +793,7 @@
     8.4      |> setup_goal I ProofContext.bind_propp_schematic_i ProofContext.fix_frees
     8.5        (Theorem {kind = kind,
     8.6          theory_spec = (a, map (snd o fst) concl),
     8.7 -        locale_spec = (case raw_locale of NONE => NONE | SOME (_, x) => SOME (valOf opt_name, x)),
     8.8 +        locale_spec = (case raw_locale of NONE => NONE | SOME (_, x) => SOME (the opt_name, x)),
     8.9          view = view,
    8.10          export = export})
    8.11        (AfterQed (Seq.single, after_global))
     9.1 --- a/src/Pure/Isar/rule_cases.ML	Tue May 17 10:19:43 2005 +0200
     9.2 +++ b/src/Pure/Isar/rule_cases.ML	Tue May 17 10:19:44 2005 +0200
     9.3 @@ -73,7 +73,7 @@
     9.4  
     9.5  fun get thm =
     9.6    let
     9.7 -    val n = getOpt (lookup_consumes thm, 0);
     9.8 +    val n = if_none (lookup_consumes thm) 0;
     9.9      val ss =
    9.10        (case lookup_case_names thm of
    9.11          NONE => map Library.string_of_int (1 upto (Thm.nprems_of thm - n))
    10.1 --- a/src/Pure/Isar/session.ML	Tue May 17 10:19:43 2005 +0200
    10.2 +++ b/src/Pure/Isar/session.ML	Tue May 17 10:19:44 2005 +0200
    10.3 @@ -73,7 +73,7 @@
    10.4  
    10.5  fun get_rpath rpath_str =
    10.6    (if rpath_str = "" then () else
    10.7 -     if isSome (!rpath) then
    10.8 +     if is_some (! rpath) then
    10.9         error "Path for remote theory browsing information may only be set once"
   10.10       else
   10.11         rpath := SOME (Url.unpack rpath_str);
    11.1 --- a/src/Pure/Isar/toplevel.ML	Tue May 17 10:19:43 2005 +0200
    11.2 +++ b/src/Pure/Isar/toplevel.ML	Tue May 17 10:19:44 2005 +0200
    11.3 @@ -201,7 +201,7 @@
    11.4  
    11.5  fun interruptible f x =
    11.6    let val y = ref (NONE: node History.T option);
    11.7 -  in raise_interrupt (fn () => y := SOME (f x)) (); valOf (! y) end;
    11.8 +  in raise_interrupt (fn () => y := SOME (f x)) (); the (! y) end;
    11.9  
   11.10  val rollback = ERROR_MESSAGE "Stale signature encountered after succesful execution!";
   11.11  
   11.12 @@ -222,7 +222,7 @@
   11.13            (mk_state (transform_error (interruptible (trans f')) node), NONE)
   11.14              handle exn => (mk_state node, SOME exn);
   11.15        in
   11.16 -        if is_stale result then return (mk_state node, SOME (getOpt (opt_exn, rollback)))
   11.17 +        if is_stale result then return (mk_state node, SOME (if_none opt_exn rollback))
   11.18          else return (result, opt_exn)
   11.19        end;
   11.20  
    12.1 --- a/src/Pure/Syntax/ast.ML	Tue May 17 10:19:43 2005 +0200
    12.2 +++ b/src/Pure/Syntax/ast.ML	Tue May 17 10:19:44 2005 +0200
    12.3 @@ -210,7 +210,7 @@
    12.4      val changes = ref 0;
    12.5  
    12.6      fun subst _ (ast as Constant _) = ast
    12.7 -      | subst env (Variable x) = valOf (Symtab.lookup (env, x))
    12.8 +      | subst env (Variable x) = the (Symtab.lookup (env, x))
    12.9        | subst env (Appl asts) = Appl (map (subst env) asts);
   12.10  
   12.11      fun try_rules ((lhs, rhs) :: pats) ast =
    13.1 --- a/src/Pure/Syntax/printer.ML	Tue May 17 10:19:43 2005 +0200
    13.2 +++ b/src/Pure/Syntax/printer.ML	Tue May 17 10:19:44 2005 +0200
    13.3 @@ -186,14 +186,8 @@
    13.4  
    13.5  type prtabs = (string * ((symb list * int * int) list) Symtab.table) list;
    13.6  
    13.7 -
    13.8 -(*find tab for mode*)
    13.9 -fun get_tab prtabs mode =
   13.10 -  getOpt (assoc (prtabs, mode), Symtab.empty);
   13.11 -
   13.12 -(*collect tabs for mode hierarchy (default "")*)
   13.13 -fun tabs_of prtabs modes =
   13.14 -  List.mapPartial (fn mode => assoc (prtabs, mode)) (modes @ [""]);
   13.15 +fun mode_tab prtabs mode = if_none (assoc (prtabs, mode)) Symtab.empty;
   13.16 +fun mode_tabs prtabs modes = List.mapPartial (curry assoc prtabs) (modes @ [""]);
   13.17  
   13.18  
   13.19  (* xprod_to_fmt *)
   13.20 @@ -246,7 +240,7 @@
   13.21  fun change_prtabs f mode xprods prtabs =
   13.22    let
   13.23      val fmts = List.mapPartial xprod_to_fmt xprods;
   13.24 -    val tab = fold f fmts (get_tab prtabs mode);
   13.25 +    val tab = fold f fmts (mode_tab prtabs mode);
   13.26    in overwrite (prtabs, (mode, tab)) end;
   13.27  
   13.28  fun extend_prtabs m = change_prtabs (curry Symtab.update_multi) m;
   13.29 @@ -255,7 +249,7 @@
   13.30  fun merge_prtabs prtabs1 prtabs2 =
   13.31    let
   13.32      val modes = distinct (map fst (prtabs1 @ prtabs2));
   13.33 -    fun merge m = (m, Symtab.merge_multi' (op =) (get_tab prtabs1 m, get_tab prtabs2 m));
   13.34 +    fun merge m = (m, Symtab.merge_multi' (op =) (mode_tab prtabs1 m, mode_tab prtabs2 m));
   13.35    in map merge modes end;
   13.36  
   13.37  
   13.38 @@ -358,14 +352,14 @@
   13.39  (* pretty_term_ast *)
   13.40  
   13.41  fun pretty_term_ast curried prtabs trf tokentrf ast =
   13.42 -  Pretty.blk (0, pretty (tabs_of prtabs (! print_mode))
   13.43 +  Pretty.blk (0, pretty (mode_tabs prtabs (! print_mode))
   13.44      trf tokentrf false curried ast 0);
   13.45  
   13.46  
   13.47  (* pretty_typ_ast *)
   13.48  
   13.49  fun pretty_typ_ast _ prtabs trf tokentrf ast =
   13.50 -  Pretty.blk (0, pretty (tabs_of prtabs (! print_mode))
   13.51 +  Pretty.blk (0, pretty (mode_tabs prtabs (! print_mode))
   13.52      trf tokentrf true false ast 0);
   13.53  
   13.54  end;
    14.1 --- a/src/Pure/Syntax/syn_ext.ML	Tue May 17 10:19:43 2005 +0200
    14.2 +++ b/src/Pure/Syntax/syn_ext.ML	Tue May 17 10:19:44 2005 +0200
    14.3 @@ -216,7 +216,7 @@
    14.4      $$ "'" -- Scan.one Symbol.is_blank >> K NONE;
    14.5  
    14.6    val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (Scan.one (not_equal "'"));
    14.7 -  val read_symbs = List.mapPartial I o valOf o Scan.read Symbol.stopper scan_symbs;
    14.8 +  val read_symbs = List.mapPartial I o the o Scan.read Symbol.stopper scan_symbs;
    14.9  
   14.10    fun unique_index xsymbs =
   14.11      if length (List.filter is_index xsymbs) <= 1 then xsymbs
    15.1 --- a/src/Pure/axclass.ML	Tue May 17 10:19:43 2005 +0200
    15.2 +++ b/src/Pure/axclass.ML	Tue May 17 10:19:44 2005 +0200
    15.3 @@ -415,7 +415,7 @@
    15.4  
    15.5  fun prove mk_prop str_of sign prop thms usr_tac =
    15.6    (Tactic.prove sign [] [] (mk_prop prop)
    15.7 -      (K (axclass_tac thms THEN (getOpt (usr_tac, all_tac))))
    15.8 +      (K (axclass_tac thms THEN (if_none usr_tac all_tac)))
    15.9      handle ERROR => error ("The error(s) above occurred while trying to prove " ^
   15.10       quote (str_of sign prop))) |> Drule.standard;
   15.11