tuned;
authorwenzelm
Sat Apr 29 23:16:43 2006 +0200 (2006-04-29)
changeset 19502369cde91963d
parent 19501 9afa7183dfc2
child 19503 10921826b160
tuned;
src/Provers/Arith/fast_lin_arith.ML
src/Provers/blast.ML
src/Pure/IsaPlanner/term_lib.ML
src/Pure/Isar/find_theorems.ML
src/Pure/Tools/compute.ML
src/Pure/codegen.ML
src/Pure/consts.ML
src/Pure/meta_simplifier.ML
src/Pure/pattern.ML
src/Pure/proofterm.ML
     1.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Fri Apr 28 17:59:06 2006 +0200
     1.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Sat Apr 29 23:16:43 2006 +0200
     1.3 @@ -430,11 +430,10 @@
     1.4        fun addthms thm1 thm2 =
     1.5          case add2 thm1 thm2 of
     1.6            NONE => (case try_add ([thm1] RL inj_thms) thm2 of
     1.7 -                     NONE => ( valOf(try_add ([thm2] RL inj_thms) thm1)
     1.8 +                     NONE => (the (try_add ([thm2] RL inj_thms) thm1)
     1.9                                 handle Option =>
    1.10                                 (trace_thm "" thm1; trace_thm "" thm2;
    1.11 -                                sys_error "Lin.arith. failed to add thms")
    1.12 -                             )
    1.13 +                                sys_error "Lin.arith. failed to add thms"))
    1.14                     | SOME thm => thm)
    1.15          | SOME thm => thm;
    1.16  
     2.1 --- a/src/Provers/blast.ML	Fri Apr 28 17:59:06 2006 +0200
     2.2 +++ b/src/Provers/blast.ML	Sat Apr 29 23:16:43 2006 +0200
     2.3 @@ -650,7 +650,7 @@
     2.4            | 1 => immediate_output"\t1 variable UPDATED:"
     2.5            | n => immediate_output("\t" ^ Int.toString n ^ " variables UPDATED:");
     2.6         (*display the instantiations themselves, though no variable names*)
     2.7 -       List.app (fn v => immediate_output("   " ^ string_of sign 4 (valOf (!v))))
     2.8 +       List.app (fn v => immediate_output("   " ^ string_of sign 4 (the (!v))))
     2.9             (List.take(!trail, !ntrail-ntrl));
    2.10         writeln"")
    2.11      else ();
     3.1 --- a/src/Pure/IsaPlanner/term_lib.ML	Fri Apr 28 17:59:06 2006 +0200
     3.2 +++ b/src/Pure/IsaPlanner/term_lib.ML	Sat Apr 29 23:16:43 2006 +0200
     3.3 @@ -354,14 +354,9 @@
     3.4      if ty1 = ty2 then term_name_eq t1 t2 l
     3.5      else NONE
     3.6    | term_name_eq (ah $ at) (bh $ bt) l =
     3.7 -    let
     3.8 -      val lopt = (term_name_eq ah bh l)
     3.9 -    in
    3.10 -      if isSome lopt then
    3.11 -	      term_name_eq at bt (valOf lopt)
    3.12 -      else
    3.13 -        NONE
    3.14 -    end
    3.15 +      (case term_name_eq ah bh l of
    3.16 +        NONE => NONE
    3.17 +      | SOME l' => term_name_eq at bt l')
    3.18    | term_name_eq (Const(a,T)) (Const(b,U)) l =
    3.19      if a=b andalso T=U then SOME l
    3.20      else NONE
    3.21 @@ -380,12 +375,12 @@
    3.22   (* checks to see if the term in a name-equivalent member of the list of terms. *)
    3.23    fun get_name_eq_member a [] = NONE
    3.24      | get_name_eq_member a (h :: t) =
    3.25 -        if isSome (term_name_eq a h []) then SOME h
    3.26 +        if is_some (term_name_eq a h []) then SOME h
    3.27  				else get_name_eq_member a t;
    3.28  
    3.29    fun name_eq_member a [] = false
    3.30      | name_eq_member a (h :: t) =
    3.31 -        if isSome (term_name_eq a h []) then true
    3.32 +        if is_some (term_name_eq a h []) then true
    3.33  				else name_eq_member a t;
    3.34  
    3.35    (* true if term is a variable *)
     4.1 --- a/src/Pure/Isar/find_theorems.ML	Fri Apr 28 17:59:06 2006 +0200
     4.2 +++ b/src/Pure/Isar/find_theorems.ML	Sat Apr 29 23:16:43 2006 +0200
     4.3 @@ -204,7 +204,7 @@
     4.4    | filter_crit ctxt _ (Simp pat) = filter_simp ctxt pat
     4.5    | filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat;
     4.6  
     4.7 -fun opt_not x = if isSome x then NONE else SOME (0, 0);
     4.8 +fun opt_not x = if is_some x then NONE else SOME (0, 0);
     4.9  
    4.10  fun opt_add (SOME (a, x)) (SOME (b, y)) = SOME (Int.max (a, b), x + y : int)
    4.11   |  opt_add _ _ = NONE;
     5.1 --- a/src/Pure/Tools/compute.ML	Fri Apr 28 17:59:06 2006 +0200
     5.2 +++ b/src/Pure/Tools/compute.ML	Sat Apr 29 23:16:43 2006 +0200
     5.3 @@ -177,7 +177,7 @@
     5.4  
     5.5                  fun make_pattern table invtable n vars (var as AbstractMachine.Var v) =
     5.6                      let
     5.7 -                        val var' = valOf (AMTermTab.lookup invtable var)
     5.8 +                        val var' = the (AMTermTab.lookup invtable var)
     5.9                          val table = Termtab.delete var' table
    5.10                          val invtable = AMTermTab.delete var invtable
    5.11                          val vars = Inttab.update_new (v, n) vars handle Inttab.DUP _ =>
     6.1 --- a/src/Pure/codegen.ML	Fri Apr 28 17:59:06 2006 +0200
     6.2 +++ b/src/Pure/codegen.ML	Sat Apr 29 23:16:43 2006 +0200
     6.3 @@ -1011,8 +1011,9 @@
     6.4      val (gi, frees) = Logic.goal_params
     6.5        (prop_of (snd (snd (Proof.get_goal (Toplevel.proof_of st))))) i;
     6.6      val gi' = ObjectLogic.atomize_term thy (map_term_types
     6.7 -      (map_type_tfree (fn p as (s, _) => getOpt (AList.lookup (op =) tvinsts s,
     6.8 -        getOpt (default_type, TFree p)))) (subst_bounds (frees, strip gi)));
     6.9 +      (map_type_tfree (fn p as (s, _) =>
    6.10 +        the_default (the_default (TFree p) default_type)
    6.11 +          (AList.lookup (op =) tvinsts s))) (subst_bounds (frees, strip gi)));
    6.12    in case test_term (Toplevel.theory_of st) size iterations gi' of
    6.13        NONE => writeln "No counterexamples found."
    6.14      | SOME cex => writeln ("Counterexample found:\n" ^
    6.15 @@ -1189,8 +1190,7 @@
    6.16      (   parse_test_params >> (fn f => fn thy => apfst (f thy))
    6.17       || parse_tyinst) --| P.$$$ "]") -- Scan.optional P.nat 1 >>
    6.18      (fn (ps, g) => Toplevel.keep (fn st =>
    6.19 -      test_goal (app (getOpt (Option.map
    6.20 -          (map (fn f => f (Toplevel.theory_of st))) ps, []))
    6.21 +      test_goal (app (the_default [] (Option.map (map (fn f => f (Toplevel.theory_of st))) ps))
    6.22          (get_test_params (Toplevel.theory_of st), [])) g st)));
    6.23  
    6.24  val valueP =
     7.1 --- a/src/Pure/consts.ML	Fri Apr 28 17:59:06 2006 +0200
     7.2 +++ b/src/Pure/consts.ML	Sat Apr 29 23:16:43 2006 +0200
     7.3 @@ -236,7 +236,7 @@
     7.4      fun abbrev (xs, body) =
     7.5        let val vars = fold (fn (x, T) => cons (Var ((x, 0), T))) (Term.rename_wrt_term body xs) []
     7.6        in (Term.subst_bounds (rev vars, body), Term.list_comb (Const const, vars)) end;
     7.7 -  in map abbrev (rev (strip_abss (Envir.beta_eta_contract rhs))) end;
     7.8 +  in map abbrev (strip_abss (Envir.beta_eta_contract rhs)) end;
     7.9  
    7.10  in
    7.11  
    7.12 @@ -254,8 +254,7 @@
    7.13          val decls' = decls
    7.14            |> extend_decls naming (c, (((T, Abbreviation rhs'), early), stamp ()));
    7.15          val rev_abbrevs' = rev_abbrevs
    7.16 -          |> Symtab.default (mode, [])
    7.17 -          |> Symtab.map_entry mode (append (rev_abbrev (NameSpace.full naming c, T) rhs));
    7.18 +          |> fold (curry Symtab.update_list mode) (rev_abbrev (NameSpace.full naming c, T) rhs);
    7.19        in (decls', constraints, rev_abbrevs', expand_abbrevs) end)
    7.20    end;
    7.21  
     8.1 --- a/src/Pure/meta_simplifier.ML	Fri Apr 28 17:59:06 2006 +0200
     8.2 +++ b/src/Pure/meta_simplifier.ML	Sat Apr 29 23:16:43 2006 +0200
     8.3 @@ -552,7 +552,7 @@
     8.4        val (lhs, _) = Drule.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm))
     8.5          handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
     8.6      (*val lhs = Envir.eta_contract lhs;*)
     8.7 -      val a = valOf (cong_name (head_of (term_of lhs))) handle Option =>
     8.8 +      val a = the (cong_name (head_of (term_of lhs))) handle Option =>
     8.9          raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm);
    8.10        val (alist, weak) = congs;
    8.11        val alist2 = overwrite_warn (alist, (a, {lhs = lhs, thm = thm}))
    8.12 @@ -566,7 +566,7 @@
    8.13        val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ =>
    8.14          raise SIMPLIFIER ("Congruence not a meta-equality", thm);
    8.15      (*val lhs = Envir.eta_contract lhs;*)
    8.16 -      val a = valOf (cong_name (head_of lhs)) handle Option =>
    8.17 +      val a = the (cong_name (head_of lhs)) handle Option =>
    8.18          raise SIMPLIFIER ("Congruence must start with a constant", thm);
    8.19        val (alist, _) = congs;
    8.20        val alist2 = List.filter (fn (x, _) => x <> a) alist;
    8.21 @@ -1010,7 +1010,7 @@
    8.22      may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*)
    8.23                            (let
    8.24                               val thm = congc (prover ss) ss maxidx cong t0;
    8.25 -                             val t = getOpt (Option.map rhs_of thm, t0);
    8.26 +                             val t = the_default t0 (Option.map rhs_of thm);
    8.27                               val (cl, cr) = Thm.dest_comb t
    8.28                               val dVar = Var(("", 0), dummyT)
    8.29                               val skel =
    8.30 @@ -1062,12 +1062,12 @@
    8.31            let
    8.32              val ss' = add_rrules (rev rrss, rev asms) ss;
    8.33              val concl' =
    8.34 -              Drule.mk_implies (prem, getOpt (Option.map rhs_of eq, concl));
    8.35 +              Drule.mk_implies (prem, the_default concl (Option.map rhs_of eq));
    8.36              val dprem = Option.map (curry (disch false) prem)
    8.37            in case rewritec (prover, thy, maxidx) ss' concl' of
    8.38                NONE => rebuild prems concl' rrss asms ss (dprem eq)
    8.39              | SOME (eq', _) => transitive2 (Library.foldl (disch false o swap)
    8.40 -                  (valOf (transitive3 (dprem eq) eq'), prems))
    8.41 +                  (the (transitive3 (dprem eq) eq'), prems))
    8.42                  (mut_impc0 (rev prems) (rhs_of eq') (rev rrss) (rev asms) ss)
    8.43            end
    8.44  
    8.45 @@ -1112,7 +1112,7 @@
    8.46       and nonmut_impc ct ss =
    8.47         let val (prem, conc) = dest_implies ct;
    8.48             val thm1 = if simprem then botc skel0 ss prem else NONE;
    8.49 -           val prem1 = getOpt (Option.map rhs_of thm1, prem);
    8.50 +           val prem1 = the_default prem (Option.map rhs_of thm1);
    8.51             val ss1 = if not useprem then ss else add_rrules
    8.52               (apsnd single (apfst single (rules_of_prem ss prem1))) ss
    8.53         in (case botc skel0 ss1 conc of
     9.1 --- a/src/Pure/pattern.ML	Fri Apr 28 17:59:06 2006 +0200
     9.2 +++ b/src/Pure/pattern.ML	Sat Apr 29 23:16:43 2006 +0200
     9.3 @@ -153,7 +153,7 @@
     9.4  
     9.5  (* mk_proj_list(is) = [ |is| - k | 1 <= k <= |is| and is[k] >= 0 ] *)
     9.6  fun mk_proj_list is =
     9.7 -    let fun mk(i::is,j) = if isSome i then j :: mk(is,j-1) else mk(is,j-1)
     9.8 +    let fun mk(i::is,j) = if is_some i then j :: mk(is,j-1) else mk(is,j-1)
     9.9            | mk([],_)    = []
    9.10      in mk(is,length is - 1) end;
    9.11  
    10.1 --- a/src/Pure/proofterm.ML	Fri Apr 28 17:59:06 2006 +0200
    10.2 +++ b/src/Pure/proofterm.ML	Sat Apr 29 23:16:43 2006 +0200
    10.3 @@ -784,7 +784,7 @@
    10.4    abstract_rule_axm % NONE % NONE %% forall_intr_proof x a prf;
    10.5  
    10.6  fun check_comb (PAxm ("ProtoPure.combination", _, _) % f % g % _ % _ %% prf %% _) =
    10.7 -      isSome f orelse check_comb prf
    10.8 +      is_some f orelse check_comb prf
    10.9    | check_comb (PAxm ("ProtoPure.transitive", _, _) % _ % _ % _ %% prf1 %% prf2) =
   10.10        check_comb prf1 andalso check_comb prf2
   10.11    | check_comb (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% prf) = check_comb prf
   10.12 @@ -1099,27 +1099,27 @@
   10.13            if prf_loose_Pbvar1 prf' 0 then rew Ts prf
   10.14            else
   10.15              let val prf'' = incr_pboundvars (~1) 0 prf'
   10.16 -            in SOME (getOpt (rew Ts prf'', (prf'', skel0))) end
   10.17 +            in SOME (the_default (prf'', skel0) (rew Ts prf'')) end
   10.18        | rew0 Ts (prf as Abst (_, _, prf' % SOME (Bound 0))) =
   10.19            if prf_loose_bvar1 prf' 0 then rew Ts prf
   10.20            else
   10.21              let val prf'' = incr_pboundvars 0 (~1) prf'
   10.22 -            in SOME (getOpt (rew Ts prf'', (prf'', skel0))) end
   10.23 +            in SOME (the_default (prf'', skel0) (rew Ts prf'')) end
   10.24        | rew0 Ts prf = rew Ts prf;
   10.25  
   10.26      fun rew1 _ (Hyp (Var _)) _ = NONE
   10.27        | rew1 Ts skel prf = (case rew2 Ts skel prf of
   10.28            SOME prf1 => (case rew0 Ts prf1 of
   10.29 -              SOME (prf2, skel') => SOME (getOpt (rew1 Ts skel' prf2, prf2))
   10.30 +              SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts skel' prf2))
   10.31              | NONE => SOME prf1)
   10.32          | NONE => (case rew0 Ts prf of
   10.33 -              SOME (prf1, skel') => SOME (getOpt (rew1 Ts skel' prf1, prf1))
   10.34 +              SOME (prf1, skel') => SOME (the_default prf1 (rew1 Ts skel' prf1))
   10.35              | NONE => NONE))
   10.36  
   10.37      and rew2 Ts skel (prf % SOME t) = (case prf of
   10.38              Abst (_, _, body) =>
   10.39                let val prf' = prf_subst_bounds [t] body
   10.40 -              in SOME (getOpt (rew2 Ts skel0 prf', prf')) end
   10.41 +              in SOME (the_default prf' (rew2 Ts skel0 prf')) end
   10.42            | _ => (case rew1 Ts (case skel of skel' % _ => skel' | _ => skel0) prf of
   10.43                SOME prf' => SOME (prf' % SOME t)
   10.44              | NONE => NONE))
   10.45 @@ -1128,7 +1128,7 @@
   10.46        | rew2 Ts skel (prf1 %% prf2) = (case prf1 of
   10.47              AbsP (_, _, body) =>
   10.48                let val prf' = prf_subst_pbounds [prf2] body
   10.49 -              in SOME (getOpt (rew2 Ts skel0 prf', prf')) end
   10.50 +              in SOME (the_default prf' (rew2 Ts skel0 prf')) end
   10.51            | _ =>
   10.52              let val (skel1, skel2) = (case skel of
   10.53                  skel1 %% skel2 => (skel1, skel2)
   10.54 @@ -1141,7 +1141,7 @@
   10.55                      SOME prf2' => SOME (prf1 %% prf2')
   10.56                    | NONE => NONE)
   10.57              end)
   10.58 -      | rew2 Ts skel (Abst (s, T, prf)) = (case rew1 (getOpt (T,dummyT) :: Ts)
   10.59 +      | rew2 Ts skel (Abst (s, T, prf)) = (case rew1 (the_default dummyT T :: Ts)
   10.60                (case skel of Abst (_, _, skel') => skel' | _ => skel0) prf of
   10.61              SOME prf' => SOME (Abst (s, T, prf'))
   10.62            | NONE => NONE)
   10.63 @@ -1151,7 +1151,7 @@
   10.64            | NONE => NONE)
   10.65        | rew2 _ _ _ = NONE
   10.66  
   10.67 -  in getOpt (rew1 [] skel0 prf, prf) end;
   10.68 +  in the_default prf (rew1 [] skel0 prf) end;
   10.69  
   10.70  fun rewrite_proof thy = rewrite_prf (fn (tyenv, f) =>
   10.71    Sign.typ_match thy (f ()) tyenv handle Type.TYPE_MATCH => raise PMatch);