merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML;
--- a/NEWS Fri Aug 27 12:40:20 2010 +0200
+++ b/NEWS Fri Aug 27 12:57:55 2010 +0200
@@ -120,6 +120,9 @@
Trueprop ~> HOL.Trueprop
True ~> HOL.True
False ~> HOL.False
+ op & ~> HOL.conj
+ op | ~> HOL.disj
+ op --> ~> HOL.implies
Not ~> HOL.Not
The ~> HOL.The
All ~> HOL.All
--- a/src/HOL/Auth/Yahalom.thy Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Auth/Yahalom.thy Fri Aug 27 12:57:55 2010 +0200
@@ -197,6 +197,7 @@
apply (erule yahalom.induct,
drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast)
apply (simp only: Says_Server_not_range analz_image_freshK_simps)
+apply safe
done
lemma analz_insert_freshK:
--- a/src/HOL/Boogie/Tools/boogie_loader.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML Fri Aug 27 12:57:55 2010 +0200
@@ -504,7 +504,7 @@
in
Const (@{const_name If}, [@{typ bool}, T, T] ---> T) $ c $ t1 $ t2
end) ||
- binexp "implies" (binop @{term "op -->"}) ||
+ binexp "implies" (binop @{term HOL.implies}) ||
scan_line "distinct" num :|-- scan_count exp >>
(fn [] => @{term True}
| ts as (t :: _) => mk_distinct (Term.fastype_of t) ts) ||
--- a/src/HOL/Boogie/Tools/boogie_tactics.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_tactics.ML Fri Aug 27 12:57:55 2010 +0200
@@ -50,11 +50,11 @@
local
- fun explode_conj (@{term "op &"} $ t $ u) = explode_conj t @ explode_conj u
+ fun explode_conj (@{term HOL.conj} $ t $ u) = explode_conj t @ explode_conj u
| explode_conj t = [t]
- fun splt (ts, @{term "op -->"} $ t $ u) = splt (ts @ explode_conj t, u)
- | splt (ts, @{term "op &"} $ t $ u) = splt (ts, t) @ splt (ts, u)
+ fun splt (ts, @{term HOL.implies} $ t $ u) = splt (ts @ explode_conj t, u)
+ | splt (ts, @{term HOL.conj} $ t $ u) = splt (ts, t) @ splt (ts, u)
| splt (ts, @{term assert_at} $ _ $ t) = [(ts, t)]
| splt (_, @{term True}) = []
| splt tp = [tp]
--- a/src/HOL/Boogie/Tools/boogie_vcs.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_vcs.ML Fri Aug 27 12:57:55 2010 +0200
@@ -59,12 +59,12 @@
fun vc_of @{term True} = NONE
| vc_of (@{term assert_at} $ Free (n, _) $ t) =
SOME (Assert ((n, t), True))
- | vc_of (@{term "op -->"} $ @{term True} $ u) = vc_of u
- | vc_of (@{term "op -->"} $ t $ u) =
+ | vc_of (@{term HOL.implies} $ @{term True} $ u) = vc_of u
+ | vc_of (@{term HOL.implies} $ t $ u) =
vc_of u |> Option.map (assume t)
- | vc_of (@{term "op &"} $ (@{term assert_at} $ Free (n, _) $ t) $ u) =
+ | vc_of (@{term HOL.conj} $ (@{term assert_at} $ Free (n, _) $ t) $ u) =
SOME (vc_of u |> the_default True |> assert (n, t))
- | vc_of (@{term "op &"} $ t $ u) =
+ | vc_of (@{term HOL.conj} $ t $ u) =
(case (vc_of t, vc_of u) of
(NONE, r) => r
| (l, NONE) => l
@@ -74,9 +74,9 @@
val prop_of_vc =
let
- fun mk_conj t u = @{term "op &"} $ t $ u
+ fun mk_conj t u = @{term HOL.conj} $ t $ u
- fun term_of (Assume (t, v)) = @{term "op -->"} $ t $ term_of v
+ fun term_of (Assume (t, v)) = @{term HOL.implies} $ t $ term_of v
| term_of (Assert ((n, t), v)) =
mk_conj (@{term assert_at} $ Free (n, @{typ bool}) $ t) (term_of v)
| term_of (Ignore v) = term_of v
--- a/src/HOL/Decision_Procs/Approximation.thy Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Fri Aug 27 12:57:55 2010 +0200
@@ -3422,7 +3422,7 @@
ML {*
fun calculated_subterms (@{const Trueprop} $ t) = calculated_subterms t
- | calculated_subterms (@{const "op -->"} $ _ $ t) = calculated_subterms t
+ | calculated_subterms (@{const HOL.implies} $ _ $ t) = calculated_subterms t
| calculated_subterms (@{term "op <= :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = [t1, t2]
| calculated_subterms (@{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = [t1, t2]
| calculated_subterms (@{term "op : :: real \<Rightarrow> real set \<Rightarrow> bool"} $ t1 $
--- a/src/HOL/Decision_Procs/Cooper.thy Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Fri Aug 27 12:57:55 2010 +0200
@@ -1952,11 +1952,11 @@
| NONE => error "num_of_term: unsupported dvd")
| fm_of_term ps vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
@{code Iff} (fm_of_term ps vs t1, fm_of_term ps vs t2)
- | fm_of_term ps vs (@{term "op &"} $ t1 $ t2) =
+ | fm_of_term ps vs (@{term HOL.conj} $ t1 $ t2) =
@{code And} (fm_of_term ps vs t1, fm_of_term ps vs t2)
- | fm_of_term ps vs (@{term "op |"} $ t1 $ t2) =
+ | fm_of_term ps vs (@{term HOL.disj} $ t1 $ t2) =
@{code Or} (fm_of_term ps vs t1, fm_of_term ps vs t2)
- | fm_of_term ps vs (@{term "op -->"} $ t1 $ t2) =
+ | fm_of_term ps vs (@{term HOL.implies} $ t1 $ t2) =
@{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2)
| fm_of_term ps vs (@{term "Not"} $ t') =
@{code NOT} (fm_of_term ps vs t')
@@ -2016,7 +2016,7 @@
fun term_bools acc t =
let
- val is_op = member (op =) [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
+ val is_op = member (op =) [@{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies}, @{term "op = :: bool => _"},
@{term "op = :: int => _"}, @{term "op < :: int => _"},
@{term "op <= :: int => _"}, @{term "Not"}, @{term "All :: (int => _) => _"},
@{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}]
--- a/src/HOL/Decision_Procs/Ferrack.thy Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Fri Aug 27 12:57:55 2010 +0200
@@ -1996,9 +1996,9 @@
@{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
| fm_of_term vs (@{term "op \<longleftrightarrow> :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
@{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (@{term "op &"} $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (@{term "op |"} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (@{term "op -->"} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
+ | fm_of_term vs (@{term HOL.conj} $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
+ | fm_of_term vs (@{term HOL.disj} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
+ | fm_of_term vs (@{term HOL.implies} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t')
| fm_of_term vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
@{code E} (fm_of_term (("", dummyT) :: vs) p)
--- a/src/HOL/Decision_Procs/MIR.thy Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Fri Aug 27 12:57:55 2010 +0200
@@ -5837,11 +5837,11 @@
@{code Dvd} (HOLogic.dest_numeral t1, num_of_term vs t2)
| fm_of_term vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
@{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (@{term "op &"} $ t1 $ t2) =
+ | fm_of_term vs (@{term HOL.conj} $ t1 $ t2) =
@{code And} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (@{term "op |"} $ t1 $ t2) =
+ | fm_of_term vs (@{term HOL.disj} $ t1 $ t2) =
@{code Or} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (@{term "op -->"} $ t1 $ t2) =
+ | fm_of_term vs (@{term HOL.implies} $ t1 $ t2) =
@{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "Not"} $ t') =
@{code NOT} (fm_of_term vs t')
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Aug 27 12:57:55 2010 +0200
@@ -2954,9 +2954,9 @@
fun powt rT = Const(@{const_name "power"}, [rT,@{typ "nat"}] ---> rT);
val brT = [bT, bT] ---> bT;
val nott = @{term "Not"};
-val conjt = @{term "op &"};
-val disjt = @{term "op |"};
-val impt = @{term "op -->"};
+val conjt = @{term HOL.conj};
+val disjt = @{term HOL.disj};
+val impt = @{term HOL.implies};
val ifft = @{term "op = :: bool => _"}
fun llt rT = Const(@{const_name Orderings.less},rrT rT);
fun lle rT = Const(@{const_name Orderings.less},rrT rT);
@@ -3018,9 +3018,9 @@
Const(@{const_name True},_) => @{code T}
| Const(@{const_name False},_) => @{code F}
| Const(@{const_name Not},_)$p => @{code NOT} (fm_of_term m m' p)
- | Const(@{const_name "op &"},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
- | Const(@{const_name "op |"},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
- | Const(@{const_name "op -->"},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
+ | Const(@{const_name HOL.conj},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
+ | Const(@{const_name HOL.disj},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
+ | Const(@{const_name HOL.implies},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
| Const(@{const_name "op ="},ty)$p$q =>
if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)
else @{code Eq} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Fri Aug 27 12:57:55 2010 +0200
@@ -33,12 +33,12 @@
{isolate_conv = icv, whatis = wi, simpset = simpset}):entry) =
let
fun uset (vars as (x::vs)) p = case term_of p of
- Const(@{const_name "op &"}, _)$ _ $ _ =>
+ Const(@{const_name HOL.conj}, _)$ _ $ _ =>
let
val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
val (lS,lth) = uset vars l val (rS, rth) = uset vars r
in (lS@rS, Drule.binop_cong_rule b lth rth) end
- | Const(@{const_name "op |"}, _)$ _ $ _ =>
+ | Const(@{const_name HOL.disj}, _)$ _ $ _ =>
let
val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
val (lS,lth) = uset vars l val (rS, rth) = uset vars r
@@ -122,12 +122,12 @@
fun decomp_mpinf fm =
case term_of fm of
- Const(@{const_name "op &"},_)$_$_ =>
+ Const(@{const_name HOL.conj},_)$_$_ =>
let val (p,q) = Thm.dest_binop fm
in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj)
(Thm.cabs x p) (Thm.cabs x q))
end
- | Const(@{const_name "op |"},_)$_$_ =>
+ | Const(@{const_name HOL.disj},_)$_$_ =>
let val (p,q) = Thm.dest_binop fm
in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj)
(Thm.cabs x p) (Thm.cabs x q))
@@ -181,9 +181,9 @@
| Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
| Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
| Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
- | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
- | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
| Const ("==>", _) $ _ $ _ => find_args bounds tm
| Const ("==", _) $ _ $ _ => find_args bounds tm
| Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
--- a/src/HOL/Decision_Procs/langford.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Decision_Procs/langford.ML Fri Aug 27 12:57:55 2010 +0200
@@ -69,28 +69,28 @@
val all_conjuncts =
let fun h acc ct =
case term_of ct of
- @{term "op &"}$_$_ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
+ @{term HOL.conj}$_$_ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
| _ => ct::acc
in h [] end;
fun conjuncts ct =
case term_of ct of
- @{term "op &"}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
+ @{term HOL.conj}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
| _ => [ct];
fun fold1 f = foldr1 (uncurry f);
-val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm "op &"} c) c') ;
+val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm HOL.conj} c) c') ;
fun mk_conj_tab th =
let fun h acc th =
case prop_of th of
- @{term "Trueprop"}$(@{term "op &"}$p$q) =>
+ @{term "Trueprop"}$(@{term HOL.conj}$p$q) =>
h (h acc (th RS conjunct2)) (th RS conjunct1)
| @{term "Trueprop"}$p => (p,th)::acc
in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
-fun is_conj (@{term "op &"}$_$_) = true
+fun is_conj (@{term HOL.conj}$_$_) = true
| is_conj _ = false;
fun prove_conj tab cjs =
@@ -183,9 +183,9 @@
| Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
| Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
| Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
- | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
- | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
| Const ("==>", _) $ _ $ _ => find_args bounds tm
| Const ("==", _) $ _ $ _ => find_args bounds tm
| Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
--- a/src/HOL/HOL.thy Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/HOL.thy Fri Aug 27 12:57:55 2010 +0200
@@ -57,13 +57,13 @@
False :: bool
Not :: "bool => bool" ("~ _" [40] 40)
+ conj :: "[bool, bool] => bool" (infixr "&" 35)
+ disj :: "[bool, bool] => bool" (infixr "|" 30)
+ implies :: "[bool, bool] => bool" (infixr "-->" 25)
+
setup Sign.root_path
consts
- "op &" :: "[bool, bool] => bool" (infixr "&" 35)
- "op |" :: "[bool, bool] => bool" (infixr "|" 30)
- "op -->" :: "[bool, bool] => bool" (infixr "-->" 25)
-
"op =" :: "['a, 'a] => bool" (infixl "=" 50)
setup Sign.local_path
@@ -89,15 +89,15 @@
notation (xsymbols)
Not ("\<not> _" [40] 40) and
- "op &" (infixr "\<and>" 35) and
- "op |" (infixr "\<or>" 30) and
- "op -->" (infixr "\<longrightarrow>" 25) and
+ HOL.conj (infixr "\<and>" 35) and
+ HOL.disj (infixr "\<or>" 30) and
+ HOL.implies (infixr "\<longrightarrow>" 25) and
not_equal (infix "\<noteq>" 50)
notation (HTML output)
Not ("\<not> _" [40] 40) and
- "op &" (infixr "\<and>" 35) and
- "op |" (infixr "\<or>" 30) and
+ HOL.conj (infixr "\<and>" 35) and
+ HOL.disj (infixr "\<or>" 30) and
not_equal (infix "\<noteq>" 50)
abbreviation (iff)
@@ -184,7 +184,7 @@
finalconsts
"op ="
- "op -->"
+ HOL.implies
The
definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10) where
@@ -1578,7 +1578,7 @@
val atomize_conjL = @{thm atomize_conjL}
val atomize_disjL = @{thm atomize_disjL}
val operator_names =
- [@{const_name "op |"}, @{const_name "op &"}, @{const_name Ex}]
+ [@{const_name HOL.disj}, @{const_name HOL.conj}, @{const_name Ex}]
);
*}
@@ -1737,8 +1737,8 @@
"True" ("true")
"False" ("false")
"Not" ("Bool.not")
- "op |" ("(_ orelse/ _)")
- "op &" ("(_ andalso/ _)")
+ HOL.disj ("(_ orelse/ _)")
+ HOL.conj ("(_ andalso/ _)")
"If" ("(if _/ then _/ else _)")
setup {*
@@ -1914,7 +1914,7 @@
(Haskell "Bool")
(Scala "Boolean")
-code_const True and False and Not and "op &" and "op |" and If
+code_const True and False and Not and HOL.conj and HOL.disj and If
(SML "true" and "false" and "not"
and infixl 1 "andalso" and infixl 0 "orelse"
and "!(if (_)/ then (_)/ else (_))")
@@ -1924,7 +1924,7 @@
(Haskell "True" and "False" and "not"
and infixl 3 "&&" and infixl 2 "||"
and "!(if (_)/ then (_)/ else (_))")
- (Scala "true" and "false" and "'!/ _"
+ (Scala "true" and "false" and "'! _"
and infixl 3 "&&" and infixl 1 "||"
and "!(if ((_))/ (_)/ else (_))")
--- a/src/HOL/Imperative_HOL/Array.thy Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy Fri Aug 27 12:57:55 2010 +0200
@@ -484,11 +484,11 @@
code_type array (Scala "!collection.mutable.ArraySeq[_]")
code_const Array (Scala "!error(\"bare Array\")")
-code_const Array.new' (Scala "('_: Unit)/ => / Array.alloc((_))((_))")
-code_const Array.make' (Scala "('_: Unit)/ =>/ Array.make((_))((_))")
-code_const Array.len' (Scala "('_: Unit)/ =>/ Array.len((_))")
-code_const Array.nth' (Scala "('_: Unit)/ =>/ Array.nth((_), (_))")
-code_const Array.upd' (Scala "('_: Unit)/ =>/ Array.upd((_), (_), (_))")
-code_const Array.freeze (Scala "('_: Unit)/ =>/ Array.freeze((_))")
+code_const Array.new' (Scala "('_: Unit)/ => / Heap.Array.alloc((_))((_))")
+code_const Array.make' (Scala "('_: Unit)/ =>/ Heap.Array.make((_))((_))")
+code_const Array.len' (Scala "('_: Unit)/ =>/ Heap.Array.len((_))")
+code_const Array.nth' (Scala "('_: Unit)/ =>/ Heap.Array.nth((_), (_))")
+code_const Array.upd' (Scala "('_: Unit)/ =>/ Heap.Array.upd((_), (_), (_))")
+code_const Array.freeze (Scala "('_: Unit)/ =>/ Heap.Array.freeze((_))")
end
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Aug 27 12:57:55 2010 +0200
@@ -478,7 +478,6 @@
code_include Scala "Heap"
{*import collection.mutable.ArraySeq
-import Natural._
def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
@@ -487,24 +486,33 @@
}
object Ref {
- def apply[A](x: A): Ref[A] = new Ref[A](x)
- def lookup[A](r: Ref[A]): A = r.value
- def update[A](r: Ref[A], x: A): Unit = { r.value = x }
+ def apply[A](x: A): Ref[A] =
+ new Ref[A](x)
+ def lookup[A](r: Ref[A]): A =
+ r.value
+ def update[A](r: Ref[A], x: A): Unit =
+ { r.value = x }
}
object Array {
- def alloc[A](n: Natural)(x: A): ArraySeq[A] = ArraySeq.fill(n.as_Int)(x)
- def make[A](n: Natural)(f: Natural => A): ArraySeq[A] = ArraySeq.tabulate(n.as_Int)((k: Int) => f(Natural(k)))
- def len[A](a: ArraySeq[A]): Natural = Natural(a.length)
- def nth[A](a: ArraySeq[A], n: Natural): A = a(n.as_Int)
- def upd[A](a: ArraySeq[A], n: Natural, x: A): Unit = a.update(n.as_Int, x)
- def freeze[A](a: ArraySeq[A]): List[A] = a.toList
+ def alloc[A](n: Natural.Nat)(x: A): ArraySeq[A] =
+ ArraySeq.fill(n.as_Int)(x)
+ def make[A](n: Natural.Nat)(f: Natural.Nat => A): ArraySeq[A] =
+ ArraySeq.tabulate(n.as_Int)((k: Int) => f(Natural.Nat(k)))
+ def len[A](a: ArraySeq[A]): Natural.Nat =
+ Natural.Nat(a.length)
+ def nth[A](a: ArraySeq[A], n: Natural.Nat): A =
+ a(n.as_Int)
+ def upd[A](a: ArraySeq[A], n: Natural.Nat, x: A): Unit =
+ a.update(n.as_Int, x)
+ def freeze[A](a: ArraySeq[A]): List[A] =
+ a.toList
}*}
code_reserved Scala bind Ref Array
code_type Heap (Scala "Unit/ =>/ _")
-code_const bind (Scala "bind")
+code_const bind (Scala "Heap.bind")
code_const return (Scala "('_: Unit)/ =>/ _")
code_const Heap_Monad.raise' (Scala "!error((_))")
--- a/src/HOL/Imperative_HOL/Ref.thy Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy Fri Aug 27 12:57:55 2010 +0200
@@ -306,10 +306,10 @@
text {* Scala *}
-code_type ref (Scala "!Ref[_]")
+code_type ref (Scala "!Heap.Ref[_]")
code_const Ref (Scala "!error(\"bare Ref\")")
-code_const ref' (Scala "('_: Unit)/ =>/ Ref((_))")
-code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))")
-code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))")
+code_const ref' (Scala "('_: Unit)/ =>/ Heap.Ref((_))")
+code_const Ref.lookup (Scala "('_: Unit)/ =>/ Heap.Ref.lookup((_))")
+code_const Ref.update (Scala "('_: Unit)/ =>/ Heap.Ref.update((_), (_))")
end
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Fri Aug 27 12:57:55 2010 +0200
@@ -17,8 +17,8 @@
T > True
F > False
"!" > All
- "/\\" > "op &"
- "\\/" > "op |"
+ "/\\" > HOL.conj
+ "\\/" > HOL.disj
"?" > Ex
"?!" > Ex1
"~" > Not
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Fri Aug 27 12:57:55 2010 +0200
@@ -54,9 +54,9 @@
ONE_ONE > HOL4Setup.ONE_ONE
ONTO > Fun.surj
"=" > "op ="
- "==>" > "op -->"
- "/\\" > "op &"
- "\\/" > "op |"
+ "==>" > HOL.implies
+ "/\\" > HOL.conj
+ "\\/" > HOL.disj
"!" > All
"?" > Ex
"?!" > Ex1
--- a/src/HOL/Import/HOL/bool.imp Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Import/HOL/bool.imp Fri Aug 27 12:57:55 2010 +0200
@@ -14,7 +14,7 @@
const_maps
"~" > "HOL.Not"
"bool_case" > "Datatype.bool.bool_case"
- "\\/" > "op |"
+ "\\/" > HOL.disj
"TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION"
"T" > "HOL.True"
"RES_SELECT" > "HOL4Base.bool.RES_SELECT"
@@ -30,7 +30,7 @@
"ARB" > "HOL4Base.bool.ARB"
"?!" > "HOL.Ex1"
"?" > "HOL.Ex"
- "/\\" > "op &"
+ "/\\" > HOL.conj
"!" > "HOL.All"
thm_maps
--- a/src/HOL/Import/HOLLight/hollight.imp Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp Fri Aug 27 12:57:55 2010 +0200
@@ -115,7 +115,7 @@
"_10303" > "HOLLight.hollight._10303"
"_10302" > "HOLLight.hollight._10302"
"_0" > "0" :: "nat"
- "\\/" > "op |"
+ "\\/" > HOL.disj
"ZRECSPACE" > "HOLLight.hollight.ZRECSPACE"
"ZIP" > "HOLLight.hollight.ZIP"
"ZCONSTR" > "HOLLight.hollight.ZCONSTR"
@@ -233,11 +233,11 @@
"?" > "HOL.Ex"
">=" > "HOLLight.hollight.>="
">" > "HOLLight.hollight.>"
- "==>" > "op -->"
+ "==>" > HOL.implies
"=" > "op ="
"<=" > "HOLLight.hollight.<="
"<" > "HOLLight.hollight.<"
- "/\\" > "op &"
+ "/\\" > HOL.conj
"-" > "Groups.minus" :: "nat => nat => nat"
"," > "Product_Type.Pair"
"+" > "Groups.plus" :: "nat => nat => nat"
--- a/src/HOL/Import/hol4rews.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Import/hol4rews.ML Fri Aug 27 12:57:55 2010 +0200
@@ -628,7 +628,7 @@
|> add_hol4_type_mapping "min" "fun" false "fun"
|> add_hol4_type_mapping "min" "ind" false @{type_name ind}
|> add_hol4_const_mapping "min" "=" false @{const_name "op ="}
- |> add_hol4_const_mapping "min" "==>" false @{const_name "op -->"}
+ |> add_hol4_const_mapping "min" "==>" false @{const_name HOL.implies}
|> add_hol4_const_mapping "min" "@" false @{const_name "Eps"}
in
val hol4_setup =
--- a/src/HOL/Import/proof_kernel.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML Fri Aug 27 12:57:55 2010 +0200
@@ -1205,7 +1205,7 @@
fun non_trivial_term_consts t = fold_aterms
(fn Const (c, _) =>
if c = @{const_name Trueprop} orelse c = @{const_name All}
- orelse c = @{const_name "op -->"} orelse c = @{const_name "op &"} orelse c = @{const_name "op ="}
+ orelse c = @{const_name HOL.implies} orelse c = @{const_name HOL.conj} orelse c = @{const_name "op ="}
then I else insert (op =) c
| _ => I) t [];
@@ -1214,10 +1214,10 @@
fun add_consts (Const (c, _), cs) =
(case c of
@{const_name "op ="} => insert (op =) "==" cs
- | @{const_name "op -->"} => insert (op =) "==>" cs
+ | @{const_name HOL.implies} => insert (op =) "==>" cs
| @{const_name All} => cs
| "all" => cs
- | @{const_name "op &"} => cs
+ | @{const_name HOL.conj} => cs
| @{const_name Trueprop} => cs
| _ => insert (op =) c cs)
| add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
@@ -1521,7 +1521,7 @@
val th1 = norm_hyps th1
val th2 = norm_hyps th2
val (l,r) = case concl_of th of
- _ $ (Const(@{const_name "op |"},_) $ l $ r) => (l,r)
+ _ $ (Const(@{const_name HOL.disj},_) $ l $ r) => (l,r)
| _ => raise ERR "DISJ_CASES" "Conclusion not a disjunction"
val th1' = rearrange thy (HOLogic.mk_Trueprop l) th1
val th2' = rearrange thy (HOLogic.mk_Trueprop r) th2
@@ -1860,7 +1860,7 @@
val _ = if_debug pth hth
val th1 = implies_elim_all (beta_eta_thm th)
val a = case concl_of th1 of
- _ $ (Const(@{const_name "op -->"},_) $ a $ Const(@{const_name False},_)) => a
+ _ $ (Const(@{const_name HOL.implies},_) $ a $ Const(@{const_name False},_)) => a
| _ => raise ERR "NOT_INTRO" "Conclusion of bad form"
val ca = cterm_of thy a
val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1
--- a/src/HOL/Library/Code_Integer.thy Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Library/Code_Integer.thy Fri Aug 27 12:57:55 2010 +0200
@@ -51,14 +51,14 @@
(SML "IntInf.- ((_), 1)")
(OCaml "Big'_int.pred'_big'_int")
(Haskell "!(_/ -/ 1)")
- (Scala "!(_/ -/ 1)")
+ (Scala "!(_ -/ 1)")
(Eval "!(_/ -/ 1)")
code_const Int.succ
(SML "IntInf.+ ((_), 1)")
(OCaml "Big'_int.succ'_big'_int")
(Haskell "!(_/ +/ 1)")
- (Scala "!(_/ +/ 1)")
+ (Scala "!(_ +/ 1)")
(Eval "!(_/ +/ 1)")
code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
--- a/src/HOL/Library/Code_Natural.thy Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Library/Code_Natural.thy Fri Aug 27 12:57:55 2010 +0200
@@ -9,9 +9,7 @@
section {* Alternative representation of @{typ code_numeral} for @{text Haskell} and @{text Scala} *}
code_include Haskell "Natural"
-{*import Data.Array.ST;
-
-newtype Natural = Natural Integer deriving (Eq, Show, Read);
+{*newtype Natural = Natural Integer deriving (Eq, Show, Read);
instance Num Natural where {
fromInteger k = Natural (if k >= 0 then k else 0);
@@ -54,48 +52,48 @@
code_reserved Haskell Natural
-code_include Scala "Natural" {*
-import scala.Math
+code_include Scala "Natural"
+{*import scala.Math
-object Natural {
+object Nat {
- def apply(numeral: BigInt): Natural = new Natural(numeral max 0)
- def apply(numeral: Int): Natural = Natural(BigInt(numeral))
- def apply(numeral: String): Natural = Natural(BigInt(numeral))
+ def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
+ def apply(numeral: Int): Nat = Nat(BigInt(numeral))
+ def apply(numeral: String): Nat = Nat(BigInt(numeral))
}
-class Natural private(private val value: BigInt) {
+class Nat private(private val value: BigInt) {
override def hashCode(): Int = this.value.hashCode()
override def equals(that: Any): Boolean = that match {
- case that: Natural => this equals that
+ case that: Nat => this equals that
case _ => false
}
override def toString(): String = this.value.toString
- def equals(that: Natural): Boolean = this.value == that.value
+ def equals(that: Nat): Boolean = this.value == that.value
def as_BigInt: BigInt = this.value
def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
this.value.intValue
else error("Int value out of range: " + this.value.toString)
- def +(that: Natural): Natural = new Natural(this.value + that.value)
- def -(that: Natural): Natural = Natural(this.value - that.value)
- def *(that: Natural): Natural = new Natural(this.value * that.value)
+ def +(that: Nat): Nat = new Nat(this.value + that.value)
+ def -(that: Nat): Nat = Nat(this.value - that.value)
+ def *(that: Nat): Nat = new Nat(this.value * that.value)
- def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
+ def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)
else {
val (k, l) = this.value /% that.value
- (new Natural(k), new Natural(l))
+ (new Nat(k), new Nat(l))
}
- def <=(that: Natural): Boolean = this.value <= that.value
+ def <=(that: Nat): Boolean = this.value <= that.value
- def <(that: Natural): Boolean = this.value < that.value
+ def <(that: Nat): Boolean = this.value < that.value
}
*}
@@ -104,7 +102,7 @@
code_type code_numeral
(Haskell "Natural.Natural")
- (Scala "Natural")
+ (Scala "Natural.Nat")
setup {*
fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
--- a/src/HOL/Library/Efficient_Nat.thy Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Fri Aug 27 12:57:55 2010 +0200
@@ -242,8 +242,8 @@
and @{typ int}.
*}
-code_include Haskell "Nat" {*
-newtype Nat = Nat Integer deriving (Eq, Show, Read);
+code_include Haskell "Nat"
+{*newtype Nat = Nat Integer deriving (Eq, Show, Read);
instance Num Nat where {
fromInteger k = Nat (if k >= 0 then k else 0);
@@ -280,8 +280,8 @@
code_reserved Haskell Nat
-code_include Scala "Nat" {*
-import scala.Math
+code_include Scala "Nat"
+{*import scala.Math
object Nat {
@@ -330,7 +330,7 @@
code_type nat
(Haskell "Nat.Nat")
- (Scala "Nat")
+ (Scala "Nat.Nat")
code_instance nat :: eq
(Haskell -)
@@ -397,7 +397,7 @@
code_const int and nat
(Haskell "toInteger" and "fromInteger")
- (Scala "!_.as'_BigInt" and "Nat")
+ (Scala "!_.as'_BigInt" and "Nat.Nat")
text {* Conversion from and to code numerals. *}
@@ -405,14 +405,14 @@
(SML "IntInf.toInt")
(OCaml "_")
(Haskell "!(fromInteger/ ./ toInteger)")
- (Scala "!Natural(_.as'_BigInt)")
+ (Scala "!Natural.Nat(_.as'_BigInt)")
(Eval "_")
code_const Code_Numeral.nat_of
(SML "IntInf.fromInt")
(OCaml "_")
(Haskell "!(fromInteger/ ./ toInteger)")
- (Scala "!Nat(_.as'_BigInt)")
+ (Scala "!Nat.Nat(_.as'_BigInt)")
(Eval "_")
text {* Using target language arithmetic operations whenever appropriate *}
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri Aug 27 12:57:55 2010 +0200
@@ -1356,7 +1356,7 @@
val known_sos_constants =
[@{term "op ==>"}, @{term "Trueprop"},
- @{term "op -->"}, @{term "op &"}, @{term "op |"},
+ @{term HOL.implies}, @{term HOL.conj}, @{term HOL.disj},
@{term "Not"}, @{term "op = :: bool => _"},
@{term "All :: (real => _) => _"}, @{term "Ex :: (real => _) => _"},
@{term "op = :: real => _"}, @{term "op < :: real => _"},
--- a/src/HOL/Library/positivstellensatz.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Fri Aug 27 12:57:55 2010 +0200
@@ -439,8 +439,8 @@
val is_req = is_binop @{cterm "op =:: real => _"}
val is_ge = is_binop @{cterm "op <=:: real => _"}
val is_gt = is_binop @{cterm "op <:: real => _"}
- val is_conj = is_binop @{cterm "op &"}
- val is_disj = is_binop @{cterm "op |"}
+ val is_conj = is_binop @{cterm HOL.conj}
+ val is_disj = is_binop @{cterm HOL.disj}
fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
fun disj_cases th th1 th2 =
let val (p,q) = Thm.dest_binop (concl th)
@@ -484,7 +484,7 @@
val th_p = poly_conv(Thm.dest_arg(Thm.dest_arg1(Thm.rhs_of th)))
val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p
val th_n = fconv_rule (arg_conv poly_neg_conv) th_x
- val th' = Drule.binop_cong_rule @{cterm "op |"}
+ val th' = Drule.binop_cong_rule @{cterm HOL.disj}
(Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p)
(Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n)
in Thm.transitive th th'
@@ -542,12 +542,12 @@
let
val nnf_norm_conv' =
nnf_conv then_conv
- literals_conv [@{term "op &"}, @{term "op |"}] []
+ literals_conv [@{term HOL.conj}, @{term HOL.disj}] []
(Conv.cache_conv
(first_conv [real_lt_conv, real_le_conv,
real_eq_conv, real_not_lt_conv,
real_not_le_conv, real_not_eq_conv, all_conv]))
- fun absremover ct = (literals_conv [@{term "op &"}, @{term "op |"}] []
+ fun absremover ct = (literals_conv [@{term HOL.conj}, @{term HOL.disj}] []
(try_conv (absconv1 then_conv binop_conv (arg_conv poly_conv))) then_conv
try_conv (absconv2 then_conv nnf_norm_conv' then_conv binop_conv absremover)) ct
val nct = Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"} ct)
--- a/src/HOL/Multivariate_Analysis/Gauge_Measure.thy Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Gauge_Measure.thy Fri Aug 27 12:57:55 2010 +0200
@@ -311,7 +311,7 @@
shows "(\<Union> f) has_gmeasure (setsum m f)" using assms
proof induct case (insert x s)
have *:"(x \<inter> \<Union>s) = \<Union>{x \<inter> y| y. y\<in>s}"by auto
- show ?case unfolding Union_insert ring_class.setsum.insert[OF insert(1-2)]
+ show ?case unfolding Union_insert setsum.insert [OF insert(1-2)]
apply(rule has_gmeasure_negligible_union) unfolding *
apply(rule insert) defer apply(rule insert) apply(rule insert) defer
apply(rule insert) prefer 4 apply(rule negligible_unions)
--- a/src/HOL/Mutabelle/Mutabelle.thy Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Mutabelle/Mutabelle.thy Fri Aug 27 12:57:55 2010 +0200
@@ -4,7 +4,7 @@
begin
ML {*
-val comms = [@{const_name "op ="}, @{const_name "op |"}, @{const_name "op &"}];
+val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}];
val forbidden =
[(@{const_name Power.power}, "'a"),
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Aug 27 12:57:55 2010 +0200
@@ -187,7 +187,7 @@
val nitpick_mtd = ("nitpick", invoke_nitpick)
*)
-val comms = [@{const_name "op ="}, @{const_name "op |"}, @{const_name "op &"}]
+val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}]
val forbidden =
[(* (@{const_name "power"}, "'a"), *)
--- a/src/HOL/Nominal/nominal_datatype.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Fri Aug 27 12:57:55 2010 +0200
@@ -1200,7 +1200,7 @@
(constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs);
val tnames = Datatype_Prop.make_tnames recTs;
val zs = Name.variant_list tnames (replicate (length descr'') "z");
- val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
+ val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
(map (fn ((((i, _), T), tname), z) =>
make_pred fsT i T $ Free (z, fsT) $ Free (tname, T))
(descr'' ~~ recTs ~~ tnames ~~ zs)));
@@ -1215,7 +1215,7 @@
map (make_ind_prem fsT' (fn T => fn t => fn u => HOLogic.Not $
HOLogic.mk_mem (t, the (AList.lookup op = fresh_fs T) $ u)) i T)
(constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs);
- val ind_concl' = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
+ val ind_concl' = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
(map (fn ((((i, _), T), tname), z) =>
make_pred fsT' i T $ Free (z, fsT') $ Free (tname, T))
(descr'' ~~ recTs ~~ tnames ~~ zs)));
@@ -1225,7 +1225,7 @@
(Datatype_Prop.indexify_names (replicate (length dt_atomTs) "pi") ~~
map mk_permT dt_atomTs) @ [("z", fsT')];
val aux_ind_Ts = rev (map snd aux_ind_vars);
- val aux_ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
+ val aux_ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
(map (fn (((i, _), T), tname) =>
HOLogic.list_all (aux_ind_vars, make_pred fsT' i T $ Bound 0 $
fold_rev (mk_perm aux_ind_Ts) (map Bound (length dt_atomTs downto 1))
--- a/src/HOL/Nominal/nominal_inductive.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Fri Aug 27 12:57:55 2010 +0200
@@ -71,7 +71,7 @@
| add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs
| add_binders thy i _ bs = bs;
-fun split_conj f names (Const (@{const_name "op &"}, _) $ p $ q) _ = (case head_of p of
+fun split_conj f names (Const (@{const_name HOL.conj}, _) $ p $ q) _ = (case head_of p of
Const (name, _) =>
if member (op =) names name then SOME (f p q) else NONE
| _ => NONE)
@@ -89,7 +89,7 @@
(* where "id" protects the subformula from simplification *)
(*********************************************************************)
-fun inst_conj_all names ps pis (Const (@{const_name "op &"}, _) $ p $ q) _ =
+fun inst_conj_all names ps pis (Const (@{const_name HOL.conj}, _) $ p $ q) _ =
(case head_of p of
Const (name, _) =>
if member (op =) names name then SOME (HOLogic.mk_conj (p,
--- a/src/HOL/Nominal/nominal_inductive2.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Fri Aug 27 12:57:55 2010 +0200
@@ -76,7 +76,7 @@
| add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs
| add_binders thy i _ bs = bs;
-fun split_conj f names (Const (@{const_name "op &"}, _) $ p $ q) _ = (case head_of p of
+fun split_conj f names (Const (@{const_name HOL.conj}, _) $ p $ q) _ = (case head_of p of
Const (name, _) =>
if member (op =) names name then SOME (f p q) else NONE
| _ => NONE)
@@ -94,7 +94,7 @@
(* where "id" protects the subformula from simplification *)
(*********************************************************************)
-fun inst_conj_all names ps pis (Const (@{const_name "op &"}, _) $ p $ q) _ =
+fun inst_conj_all names ps pis (Const (@{const_name HOL.conj}, _) $ p $ q) _ =
(case head_of p of
Const (name, _) =>
if member (op =) names name then SOME (HOLogic.mk_conj (p,
--- a/src/HOL/Orderings.thy Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Orderings.thy Fri Aug 27 12:57:55 2010 +0200
@@ -640,8 +640,8 @@
let
val All_binder = Syntax.binder_name @{const_syntax All};
val Ex_binder = Syntax.binder_name @{const_syntax Ex};
- val impl = @{const_syntax "op -->"};
- val conj = @{const_syntax "op &"};
+ val impl = @{const_syntax HOL.implies};
+ val conj = @{const_syntax HOL.conj};
val less = @{const_syntax less};
val less_eq = @{const_syntax less_eq};
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Fri Aug 27 12:57:55 2010 +0200
@@ -4,13 +4,24 @@
section {* Example append *}
+
inductive append
where
"append [] ys ys"
| "append xs ys zs ==> append (x # xs) ys (x # zs)"
+ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *}
+
+values "{(x, y, z). append x y z}"
+
values 3 "{(x, y, z). append x y z}"
+ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.YAP} *}
+
+values "{(x, y, z). append x y z}"
+
+ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *}
+
section {* Example queens *}
@@ -172,7 +183,7 @@
where
"y \<noteq> B \<Longrightarrow> notB y"
-ML {* Code_Prolog.options := {ensure_groundness = true} *}
+ML {* Code_Prolog.options := {ensure_groundness = true, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *}
values 2 "{y. notB y}"
@@ -187,7 +198,7 @@
inductive equals :: "abc => abc => bool"
where
"equals y' y'"
-ML {* set Code_Prolog.trace *}
+
values 1 "{(y, z). equals y z}"
end
--- a/src/HOL/Prolog/prolog.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Prolog/prolog.ML Fri Aug 27 12:57:55 2010 +0200
@@ -11,12 +11,12 @@
fun isD t = case t of
Const(@{const_name Trueprop},_)$t => isD t
- | Const(@{const_name "op &"} ,_)$l$r => isD l andalso isD r
- | Const(@{const_name "op -->"},_)$l$r => isG l andalso isD r
+ | Const(@{const_name HOL.conj} ,_)$l$r => isD l andalso isD r
+ | Const(@{const_name HOL.implies},_)$l$r => isG l andalso isD r
| Const( "==>",_)$l$r => isG l andalso isD r
| Const(@{const_name All},_)$Abs(s,_,t) => isD t
| Const("all",_)$Abs(s,_,t) => isD t
- | Const(@{const_name "op |"},_)$_$_ => false
+ | Const(@{const_name HOL.disj},_)$_$_ => false
| Const(@{const_name Ex} ,_)$_ => false
| Const(@{const_name Not},_)$_ => false
| Const(@{const_name True},_) => false
@@ -30,9 +30,9 @@
and
isG t = case t of
Const(@{const_name Trueprop},_)$t => isG t
- | Const(@{const_name "op &"} ,_)$l$r => isG l andalso isG r
- | Const(@{const_name "op |"} ,_)$l$r => isG l andalso isG r
- | Const(@{const_name "op -->"},_)$l$r => isD l andalso isG r
+ | Const(@{const_name HOL.conj} ,_)$l$r => isG l andalso isG r
+ | Const(@{const_name HOL.disj} ,_)$l$r => isG l andalso isG r
+ | Const(@{const_name HOL.implies},_)$l$r => isD l andalso isG r
| Const( "==>",_)$l$r => isD l andalso isG r
| Const(@{const_name All},_)$Abs(_,_,t) => isG t
| Const("all",_)$Abs(_,_,t) => isG t
@@ -53,8 +53,8 @@
fun at thm = case concl_of thm of
_$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS
(read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
- | _$(Const(@{const_name "op &"},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
- | _$(Const(@{const_name "op -->"},_)$_$_) => at(thm RS mp)
+ | _$(Const(@{const_name HOL.conj},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
+ | _$(Const(@{const_name HOL.implies},_)$_$_) => at(thm RS mp)
| _ => [thm]
in map zero_var_indexes (at thm) end;
@@ -72,7 +72,7 @@
-- is nice, but cannot instantiate unknowns in the assumptions *)
fun hyp_resolve_tac i st = let
fun ap (Const(@{const_name All},_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a ,t))
- | ap (Const(@{const_name "op -->"},_)$_$t) =(case ap t of (k,_,t) => (k,true ,t))
+ | ap (Const(@{const_name HOL.implies},_)$_$t) =(case ap t of (k,_,t) => (k,true ,t))
| ap t = (0,false,t);
(*
fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
--- a/src/HOL/Set.thy Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Set.thy Fri Aug 27 12:57:55 2010 +0200
@@ -219,8 +219,8 @@
val Type (set_type, _) = @{typ "'a set"}; (* FIXME 'a => bool (!?!) *)
val All_binder = Syntax.binder_name @{const_syntax All};
val Ex_binder = Syntax.binder_name @{const_syntax Ex};
- val impl = @{const_syntax "op -->"};
- val conj = @{const_syntax "op &"};
+ val impl = @{const_syntax HOL.implies};
+ val conj = @{const_syntax HOL.conj};
val sbset = @{const_syntax subset};
val sbset_eq = @{const_syntax subset_eq};
@@ -269,7 +269,7 @@
fun setcompr_tr [e, idts, b] =
let
val eq = Syntax.const @{const_syntax "op ="} $ Bound (nvars idts) $ e;
- val P = Syntax.const @{const_syntax "op &"} $ eq $ b;
+ val P = Syntax.const @{const_syntax HOL.conj} $ eq $ b;
val exP = ex_tr [idts, P];
in Syntax.const @{const_syntax Collect} $ Term.absdummy (dummyT, exP) end;
@@ -288,7 +288,7 @@
fun setcompr_tr' [Abs (abs as (_, _, P))] =
let
fun check (Const (@{const_syntax Ex}, _) $ Abs (_, _, P), n) = check (P, n + 1)
- | check (Const (@{const_syntax "op &"}, _) $
+ | check (Const (@{const_syntax HOL.conj}, _) $
(Const (@{const_syntax "op ="}, _) $ Bound m $ e) $ P, n) =
n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
subset (op =) (0 upto (n - 1), add_loose_bnos (e, 0, []))
@@ -305,7 +305,7 @@
val M = Syntax.const @{syntax_const "_Coll"} $ x $ t;
in
case t of
- Const (@{const_syntax "op &"}, _) $
+ Const (@{const_syntax HOL.conj}, _) $
(Const (@{const_syntax Set.member}, _) $
(Const (@{syntax_const "_bound"}, _) $ Free (yN, _)) $ A) $ P =>
if xN = yN then Syntax.const @{syntax_const "_Collect"} $ x $ A $ P else M
--- a/src/HOL/Statespace/state_fun.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Statespace/state_fun.ML Fri Aug 27 12:57:55 2010 +0200
@@ -53,7 +53,7 @@
val lazy_conj_simproc =
Simplifier.simproc_global @{theory HOL} "lazy_conj_simp" ["P & Q"]
(fn thy => fn ss => fn t =>
- (case t of (Const (@{const_name "op &"},_)$P$Q) =>
+ (case t of (Const (@{const_name HOL.conj},_)$P$Q) =>
let
val P_P' = Simplifier.rewrite ss (cterm_of thy P);
val P' = P_P' |> prop_of |> Logic.dest_equals |> #2
--- a/src/HOL/TLA/Intensional.thy Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/TLA/Intensional.thy Fri Aug 27 12:57:55 2010 +0200
@@ -279,7 +279,7 @@
fun hflatten t =
case (concl_of t) of
- Const _ $ (Const (@{const_name "op -->"}, _) $ _ $ _) => hflatten (t RS mp)
+ Const _ $ (Const (@{const_name HOL.implies}, _) $ _ $ _) => hflatten (t RS mp)
| _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t
in
hflatten t
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Fri Aug 27 12:57:55 2010 +0200
@@ -120,8 +120,8 @@
fun split_conj_thm th =
((th RS conjunct1)::(split_conj_thm (th RS conjunct2))) handle THM _ => [th];
-val mk_conj = foldr1 (HOLogic.mk_binop @{const_name "op &"});
-val mk_disj = foldr1 (HOLogic.mk_binop @{const_name "op |"});
+val mk_conj = foldr1 (HOLogic.mk_binop @{const_name HOL.conj});
+val mk_disj = foldr1 (HOLogic.mk_binop @{const_name HOL.disj});
fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0));
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Fri Aug 27 12:57:55 2010 +0200
@@ -70,7 +70,7 @@
val frees' = map Free ((map ((op ^) o (rpair "'")) tnames) ~~ Ts);
in cons (HOLogic.mk_Trueprop (HOLogic.mk_eq
(HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),
- foldr1 (HOLogic.mk_binop @{const_name "op &"})
+ foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
(map HOLogic.mk_eq (frees ~~ frees')))))
end;
in
@@ -149,7 +149,7 @@
val prems = maps (fn ((i, (_, _, constrs)), T) =>
map (make_ind_prem i T) constrs) (descr' ~~ recTs);
val tnames = make_tnames recTs;
- val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name "op &"})
+ val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
(map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T))
(descr' ~~ recTs ~~ tnames)))
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Fri Aug 27 12:57:55 2010 +0200
@@ -99,7 +99,7 @@
if member (op =) is i then SOME
(list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T))
else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames));
- val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name "op &"})
+ val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
(map (fn ((((i, _), T), U), tname) =>
make_pred i U T (mk_proj i is r) (Free (tname, T)))
(descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
--- a/src/HOL/Tools/Function/termination.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Function/termination.ML Fri Aug 27 12:57:55 2010 +0200
@@ -148,7 +148,7 @@
val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
let
- val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
+ val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
= Term.strip_qnt_body @{const_name Ex} c
in cons r o cons l end
in
@@ -185,7 +185,7 @@
val vs = Term.strip_qnt_vars @{const_name Ex} c
(* FIXME: throw error "dest_call" for malformed terms *)
- val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
+ val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
= Term.strip_qnt_body @{const_name Ex} c
val (p, l') = dest_inj sk l
val (q, r') = dest_inj sk r
--- a/src/HOL/Tools/Nitpick/minipick.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Nitpick/minipick.ML Fri Aug 27 12:57:55 2010 +0200
@@ -130,9 +130,9 @@
[Type (@{type_name fun}, [_, @{typ bool}]), _]))
$ t1 $ t2 =>
Subset (to_R_rep Ts t1, to_R_rep Ts t2)
- | @{const "op &"} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
- | @{const "op |"} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
- | @{const "op -->"} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
+ | @{const HOL.conj} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
+ | @{const HOL.disj} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
+ | @{const HOL.implies} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
| t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
| Free _ => raise SAME ()
| Term.Var _ => raise SAME ()
@@ -173,12 +173,12 @@
to_R_rep Ts (eta_expand Ts t 1)
| Const (@{const_name ord_class.less_eq}, _) =>
to_R_rep Ts (eta_expand Ts t 2)
- | @{const "op &"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
- | @{const "op &"} => to_R_rep Ts (eta_expand Ts t 2)
- | @{const "op |"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
- | @{const "op |"} => to_R_rep Ts (eta_expand Ts t 2)
- | @{const "op -->"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
- | @{const "op -->"} => to_R_rep Ts (eta_expand Ts t 2)
+ | @{const HOL.conj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
+ | @{const HOL.conj} => to_R_rep Ts (eta_expand Ts t 2)
+ | @{const HOL.disj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
+ | @{const HOL.disj} => to_R_rep Ts (eta_expand Ts t 2)
+ | @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
+ | @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
| Const (@{const_name bot_class.bot},
T as Type (@{type_name fun}, [_, @{typ bool}])) =>
empty_n_ary_rel (arity_of RRep card T)
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Aug 27 12:57:55 2010 +0200
@@ -386,13 +386,13 @@
if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
| strip_connective _ t = [t]
fun strip_any_connective (t as (t0 $ _ $ _)) =
- if t0 = @{const "op &"} orelse t0 = @{const "op |"} then
+ if t0 = @{const HOL.conj} orelse t0 = @{const HOL.disj} then
(strip_connective t0 t, t0)
else
([t], @{const Not})
| strip_any_connective t = ([t], @{const Not})
-val conjuncts_of = strip_connective @{const "op &"}
-val disjuncts_of = strip_connective @{const "op |"}
+val conjuncts_of = strip_connective @{const HOL.conj}
+val disjuncts_of = strip_connective @{const HOL.disj}
(* When you add constants to these lists, make sure to handle them in
"Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
@@ -409,9 +409,9 @@
(@{const_name All}, 1),
(@{const_name Ex}, 1),
(@{const_name "op ="}, 1),
- (@{const_name "op &"}, 2),
- (@{const_name "op |"}, 2),
- (@{const_name "op -->"}, 2),
+ (@{const_name HOL.conj}, 2),
+ (@{const_name HOL.disj}, 2),
+ (@{const_name HOL.implies}, 2),
(@{const_name If}, 3),
(@{const_name Let}, 2),
(@{const_name Pair}, 2),
@@ -1454,7 +1454,7 @@
| @{const Trueprop} $ t1 => lhs_of_equation t1
| Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1
| Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1
- | @{const "op -->"} $ _ $ t2 => lhs_of_equation t2
+ | @{const HOL.implies} $ _ $ t2 => lhs_of_equation t2
| _ => NONE
fun is_constr_pattern _ (Bound _) = true
| is_constr_pattern _ (Var _) = true
@@ -2148,8 +2148,8 @@
fun repair_rec j (Const (@{const_name Ex}, T1) $ Abs (s2, T2, t2')) =
Const (@{const_name Ex}, T1)
$ Abs (s2, T2, repair_rec (j + 1) t2')
- | repair_rec j (@{const "op &"} $ t1 $ t2) =
- @{const "op &"} $ repair_rec j t1 $ repair_rec j t2
+ | repair_rec j (@{const HOL.conj} $ t1 $ t2) =
+ @{const HOL.conj} $ repair_rec j t1 $ repair_rec j t2
| repair_rec j t =
let val (head, args) = strip_comb t in
if head = Bound j then
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Aug 27 12:57:55 2010 +0200
@@ -774,10 +774,10 @@
(MAbs (s, T, M, S Minus, m'), accum |>> pop_bound)
end))
| (t0 as Const (@{const_name All}, _))
- $ Abs (s', T', (t10 as @{const "op -->"}) $ (t11 $ Bound 0) $ t12) =>
+ $ Abs (s', T', (t10 as @{const HOL.implies}) $ (t11 $ Bound 0) $ t12) =>
do_bounded_quantifier t0 s' T' t10 t11 t12 accum
| (t0 as Const (@{const_name Ex}, _))
- $ Abs (s', T', (t10 as @{const "op &"}) $ (t11 $ Bound 0) $ t12) =>
+ $ Abs (s', T', (t10 as @{const HOL.conj}) $ (t11 $ Bound 0) $ t12) =>
do_bounded_quantifier t0 s' T' t10 t11 t12 accum
| Const (@{const_name Let}, _) $ t1 $ t2 =>
do_term (betapply (t2, t1)) accum
@@ -883,12 +883,12 @@
| (t0 as Const (s0, _)) $ t1 $ t2 =>
if s0 = @{const_name "==>"} orelse
s0 = @{const_name Pure.conjunction} orelse
- s0 = @{const_name "op &"} orelse
- s0 = @{const_name "op |"} orelse
- s0 = @{const_name "op -->"} then
+ s0 = @{const_name HOL.conj} orelse
+ s0 = @{const_name HOL.disj} orelse
+ s0 = @{const_name HOL.implies} then
let
val impl = (s0 = @{const_name "==>"} orelse
- s0 = @{const_name "op -->"})
+ s0 = @{const_name HOL.implies})
val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
val (m2, accum) = do_formula sn t2 accum
in
@@ -975,8 +975,8 @@
do_all t0 s0 T1 t1 accum
| Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
consider_general_equals mdata true x t1 t2 accum
- | (t0 as @{const "op &"}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
- | (t0 as @{const "op -->"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
+ | (t0 as @{const HOL.conj}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
+ | (t0 as @{const HOL.implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
| _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
\do_formula", [t])
in do_formula t end
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Aug 27 12:57:55 2010 +0200
@@ -518,11 +518,11 @@
| (Const (@{const_name "op ="}, T), [t1]) =>
Op1 (SingletonSet, range_type T, Any, sub t1)
| (Const (@{const_name "op ="}, T), [t1, t2]) => sub_equals T t1 t2
- | (Const (@{const_name "op &"}, _), [t1, t2]) =>
+ | (Const (@{const_name HOL.conj}, _), [t1, t2]) =>
Op2 (And, bool_T, Any, sub' t1, sub' t2)
- | (Const (@{const_name "op |"}, _), [t1, t2]) =>
+ | (Const (@{const_name HOL.disj}, _), [t1, t2]) =>
Op2 (Or, bool_T, Any, sub t1, sub t2)
- | (Const (@{const_name "op -->"}, _), [t1, t2]) =>
+ | (Const (@{const_name HOL.implies}, _), [t1, t2]) =>
Op2 (Or, bool_T, Any, Op1 (Not, bool_T, Any, sub t1), sub' t2)
| (Const (@{const_name If}, T), [t1, t2, t3]) =>
Op3 (If, nth_range_type 3 T, Any, sub t1, sub t2, sub t3)
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Aug 27 12:57:55 2010 +0200
@@ -43,7 +43,7 @@
| aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2
| aux def (Const (@{const_name "op ="}, _) $ t1 $ t2) =
aux def t1 andalso aux false t2
- | aux def (@{const "op -->"} $ t1 $ t2) = aux false t1 andalso aux def t2
+ | aux def (@{const HOL.implies} $ t1 $ t2) = aux false t1 andalso aux def t2
| aux def (t1 $ t2) = aux def t1 andalso aux def t2
| aux def (t as Const (s, _)) =
(not def orelse t <> @{const Suc}) andalso
@@ -211,14 +211,14 @@
do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
| Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
do_equals new_Ts old_Ts s0 T0 t1 t2
- | @{const "op &"} $ t1 $ t2 =>
- @{const "op &"} $ do_term new_Ts old_Ts polar t1
+ | @{const HOL.conj} $ t1 $ t2 =>
+ @{const HOL.conj} $ do_term new_Ts old_Ts polar t1
$ do_term new_Ts old_Ts polar t2
- | @{const "op |"} $ t1 $ t2 =>
- @{const "op |"} $ do_term new_Ts old_Ts polar t1
+ | @{const HOL.disj} $ t1 $ t2 =>
+ @{const HOL.disj} $ do_term new_Ts old_Ts polar t1
$ do_term new_Ts old_Ts polar t2
- | @{const "op -->"} $ t1 $ t2 =>
- @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
+ | @{const HOL.implies} $ t1 $ t2 =>
+ @{const HOL.implies} $ do_term new_Ts old_Ts (flip_polarity polar) t1
$ do_term new_Ts old_Ts polar t2
| Const (x as (s, T)) =>
if is_descr s then
@@ -334,7 +334,7 @@
if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
| (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
do_eq_or_imp Ts true def t0 t1 t2 seen
- | (t0 as @{const "op -->"}) $ t1 $ t2 =>
+ | (t0 as @{const HOL.implies}) $ t1 $ t2 =>
do_eq_or_imp Ts false def t0 t1 t2 seen
| Abs (s, T, t') =>
let val (t', seen) = do_term (T :: Ts) def t' [] seen in
@@ -401,7 +401,7 @@
t0 $ aux false t1 $ aux careful t2
| aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
aux_eq careful true t0 t1 t2
- | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) =
+ | aux careful ((t0 as @{const HOL.implies}) $ t1 $ t2) =
t0 $ aux false t1 $ aux careful t2
| aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
| aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
@@ -449,7 +449,7 @@
(** Destruction of universal and existential equalities **)
fun curry_assms (@{const "==>"} $ (@{const Trueprop}
- $ (@{const "op &"} $ t1 $ t2)) $ t3) =
+ $ (@{const HOL.conj} $ t1 $ t2)) $ t3) =
curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
| curry_assms (@{const "==>"} $ t1 $ t2) =
@{const "==>"} $ curry_assms t1 $ curry_assms t2
@@ -604,12 +604,12 @@
do_quantifier s0 T0 s1 T1 t1
| Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
do_quantifier s0 T0 s1 T1 t1
- | @{const "op &"} $ t1 $ t2 =>
+ | @{const HOL.conj} $ t1 $ t2 =>
s_conj (pairself (aux ss Ts js skolemizable polar) (t1, t2))
- | @{const "op |"} $ t1 $ t2 =>
+ | @{const HOL.disj} $ t1 $ t2 =>
s_disj (pairself (aux ss Ts js skolemizable polar) (t1, t2))
- | @{const "op -->"} $ t1 $ t2 =>
- @{const "op -->"} $ aux ss Ts js skolemizable (flip_polarity polar) t1
+ | @{const HOL.implies} $ t1 $ t2 =>
+ @{const HOL.implies} $ aux ss Ts js skolemizable (flip_polarity polar) t1
$ aux ss Ts js skolemizable polar t2
| (t0 as Const (@{const_name Let}, _)) $ t1 $ t2 =>
t0 $ t1 $ aux ss Ts js skolemizable polar t2
@@ -620,8 +620,8 @@
let
val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
val (pref, connective) =
- if gfp then (lbfp_prefix, @{const "op |"})
- else (ubfp_prefix, @{const "op &"})
+ if gfp then (lbfp_prefix, @{const HOL.disj})
+ else (ubfp_prefix, @{const HOL.conj})
fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
|> aux ss Ts js skolemizable polar
fun neg () = Const (pref ^ s, T)
@@ -1105,7 +1105,7 @@
case t of
(t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) =>
(case t1 of
- (t10 as @{const "op &"}) $ t11 $ t12 =>
+ (t10 as @{const HOL.conj}) $ t11 $ t12 =>
t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
$ distribute_quantifiers (t0 $ Abs (s, T1, t12))
| (t10 as @{const Not}) $ t11 =>
@@ -1118,10 +1118,10 @@
t0 $ Abs (s, T1, distribute_quantifiers t1))
| (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) =>
(case distribute_quantifiers t1 of
- (t10 as @{const "op |"}) $ t11 $ t12 =>
+ (t10 as @{const HOL.disj}) $ t11 $ t12 =>
t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
$ distribute_quantifiers (t0 $ Abs (s, T1, t12))
- | (t10 as @{const "op -->"}) $ t11 $ t12 =>
+ | (t10 as @{const HOL.implies}) $ t11 $ t12 =>
t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
$ Abs (s, T1, t11))
$ distribute_quantifiers (t0 $ Abs (s, T1, t12))
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Aug 27 12:57:55 2010 +0200
@@ -6,7 +6,9 @@
signature CODE_PROLOG =
sig
- type code_options = {ensure_groundness : bool}
+ datatype prolog_system = SWI_PROLOG | YAP
+ type code_options =
+ {ensure_groundness : bool, limited_types : (typ * int) list, prolog_system : prolog_system}
val options : code_options ref
datatype arith_op = Plus | Minus
@@ -21,10 +23,10 @@
type clause = ((string * prol_term list) * prem);
type logic_program = clause list;
type constant_table = (string * string) list
-
- val generate : code_options -> Proof.context -> string -> (logic_program * constant_table)
+
+ val generate : bool -> Proof.context -> string -> (logic_program * constant_table)
val write_program : logic_program -> string
- val run : logic_program -> string -> string list -> int option -> prol_term list list
+ val run : prolog_system -> logic_program -> string -> string list -> int option -> prol_term list list
val quickcheck : Proof.context -> bool -> term -> int -> term list option * (bool list * bool)
@@ -42,9 +44,13 @@
(* code generation options *)
-type code_options = {ensure_groundness : bool}
+datatype prolog_system = SWI_PROLOG | YAP
-val options = Unsynchronized.ref {ensure_groundness = false};
+type code_options =
+ {ensure_groundness : bool, limited_types : (typ * int) list, prolog_system : prolog_system}
+
+val options = Unsynchronized.ref {ensure_groundness = false, limited_types = [],
+ prolog_system = SWI_PROLOG};
(* general string functions *)
@@ -190,10 +196,10 @@
fun mk_groundness_prems t = map Ground (Term.add_frees t [])
-fun translate_prem options ctxt constant_table t =
+fun translate_prem ensure_groundness ctxt constant_table t =
case try HOLogic.dest_not t of
SOME t =>
- if #ensure_groundness options then
+ if ensure_groundness then
Conj (mk_groundness_prems t @ [NegRel_of (translate_literal ctxt constant_table t)])
else
NegRel_of (translate_literal ctxt constant_table t)
@@ -215,7 +221,7 @@
(Trueprop_conv (Conv.try_conv (Conv.rewr_conv @{thm Predicate.eq_is_eq}))))
(Thm.transfer thy rule)
-fun translate_intros options ctxt gr const constant_table =
+fun translate_intros ensure_groundness ctxt gr const constant_table =
let
val intros = map (preprocess_intro (ProofContext.theory_of ctxt)) (Graph.get_node gr const)
val (intros', ctxt') = Variable.import_terms true (map prop_of intros) ctxt
@@ -225,33 +231,11 @@
let
val head = HOLogic.dest_Trueprop (Logic.strip_imp_concl intro)
val prems = map HOLogic.dest_Trueprop (Logic.strip_imp_prems intro)
- val prems' = Conj (map (translate_prem options ctxt' constant_table') prems)
+ val prems' = Conj (map (translate_prem ensure_groundness ctxt' constant_table') prems)
val clause = (dest_Rel (translate_literal ctxt' constant_table' head), prems')
in clause end
in (map translate_intro intros', constant_table') end
-val preprocess_options = Predicate_Compile_Aux.Options {
- expected_modes = NONE,
- proposed_modes = NONE,
- proposed_names = [],
- show_steps = false,
- show_intermediate_results = false,
- show_proof_trace = false,
- show_modes = false,
- show_mode_inference = false,
- show_compilation = false,
- show_caught_failures = false,
- skip_proof = true,
- no_topmost_reordering = false,
- function_flattening = true,
- specialise = false,
- fail_safe_function_flattening = false,
- no_higher_order_predicate = [],
- inductify = false,
- detect_switches = true,
- compilation = Predicate_Compile_Aux.Pred
-}
-
fun depending_preds_of (key, intros) =
fold Term.add_const_names (map Thm.prop_of intros) []
@@ -272,7 +256,7 @@
fst (extend' key (G, []))
end
-fun generate options ctxt const =
+fun generate ensure_groundness ctxt const =
let
fun strong_conn_of gr keys =
Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
@@ -281,10 +265,11 @@
val scc = strong_conn_of gr' [const]
val constant_table = mk_constant_table (flat scc)
in
- apfst flat (fold_map (translate_intros options ctxt gr) (flat scc) constant_table)
+ apfst flat (fold_map (translate_intros ensure_groundness ctxt gr) (flat scc) constant_table)
end
-(* add implementation for ground predicates *)
+(* implementation for fully enumerating predicates and
+ for size-limited predicates for enumerating the values of a datatype upto a specific size *)
fun add_ground_typ (Conj prems) = fold add_ground_typ prems
| add_ground_typ (Ground (_, T)) = insert (op =) T
@@ -294,34 +279,58 @@
first_lower (Long_Name.base_name Tcon) ^ space_implode "_" (map mk_relname Targs)
| mk_relname _ = raise Fail "unexpected type"
+fun mk_lim_relname T = "lim_" ^ mk_relname T
+
(* This is copied from "pat_completeness.ML" *)
fun inst_constrs_of thy (T as Type (name, _)) =
map (fn (Cn,CT) =>
Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
(the (Datatype.get_constrs thy name))
| inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], [])
+
+fun is_recursive_constr T (Const (constr_name, T')) = member (op =) (binder_types T') T
-fun mk_ground_impl ctxt (T as Type (Tcon, Targs)) (seen, constant_table) =
+fun mk_ground_impl ctxt limited_types (T as Type (Tcon, Targs)) (seen, constant_table) =
if member (op =) seen T then ([], (seen, constant_table))
else
let
- val rel_name = mk_relname T
- fun mk_impl (Const (constr_name, T)) (seen, constant_table) =
+ val (limited, size) = case AList.lookup (op =) limited_types T of
+ SOME s => (true, s)
+ | NONE => (false, 0)
+ val rel_name = (if limited then mk_lim_relname else mk_relname) T
+ fun mk_impl (Const (constr_name, cT), recursive) (seen, constant_table) =
let
val constant_table' = declare_consts [constr_name] constant_table
+ val Ts = binder_types cT
val (rec_clauses, (seen', constant_table'')) =
- fold_map (mk_ground_impl ctxt) (binder_types T) (seen, constant_table')
- val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto (length (binder_types T)))
- fun mk_prem v T = Rel (mk_relname T, [v])
+ fold_map (mk_ground_impl ctxt limited_types) Ts (seen, constant_table')
+ val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto (length Ts))
+ val lim_var =
+ if limited then
+ if recursive then [AppF ("suc", [Var "Lim"])]
+ else [Var "Lim"]
+ else []
+ fun mk_prem v T' =
+ if limited andalso T' = T then Rel (mk_lim_relname T', [Var "Lim", v])
+ else Rel (mk_relname T', [v])
val clause =
- ((rel_name, [maybe_AppF (translate_const constant_table'' constr_name, vars)]),
- Conj (map2 mk_prem vars (binder_types T)))
+ ((rel_name, lim_var @ [maybe_AppF (translate_const constant_table'' constr_name, vars)]),
+ Conj (map2 mk_prem vars Ts))
in
(clause :: flat rec_clauses, (seen', constant_table''))
end
val constrs = inst_constrs_of (ProofContext.theory_of ctxt) T
- in apfst flat (fold_map mk_impl constrs (T :: seen, constant_table)) end
- | mk_ground_impl ctxt T (seen, constant_table) =
+ val constrs' = (constrs ~~ map (is_recursive_constr T) constrs)
+ |> (fn cs => filter_out snd cs @ filter snd cs)
+ val (clauses, constant_table') =
+ apfst flat (fold_map mk_impl constrs' (T :: seen, constant_table))
+ val size_term = funpow size (fn t => AppF ("suc", [t])) (Cons "zero")
+ in
+ ((if limited then
+ cons ((mk_relname T, [Var "x"]), Rel (mk_lim_relname T, [size_term, Var "x"]))
+ else I) clauses, constant_table')
+ end
+ | mk_ground_impl ctxt _ T (seen, constant_table) =
raise Fail ("unexpected type :" ^ Syntax.string_of_typ ctxt T)
fun replace_ground (Conj prems) = Conj (map replace_ground prems)
@@ -329,15 +338,16 @@
Rel (mk_relname T, [Var x])
| replace_ground p = p
-fun add_ground_predicates ctxt (p, constant_table) =
+fun add_ground_predicates ctxt limited_types (p, constant_table) =
let
val ground_typs = fold (add_ground_typ o snd) p []
- val (grs, (_, constant_table')) = fold_map (mk_ground_impl ctxt) ground_typs ([], constant_table)
+ val (grs, (_, constant_table')) = fold_map (mk_ground_impl ctxt limited_types) ground_typs ([], constant_table)
val p' = map (apsnd replace_ground) p
in
((flat grs) @ p', constant_table')
end
-
+
+
(* rename variables to prolog-friendly names *)
fun rename_vars_term renaming = map_vars (fn v => the (AList.lookup (op =) renaming v))
@@ -396,14 +406,16 @@
fun write_program p =
cat_lines (map write_clause p)
-(** query templates **)
+(* query templates *)
-fun query_first rel vnames =
+(** query and prelude for swi-prolog **)
+
+fun swi_prolog_query_first rel vnames =
"eval :- once(" ^ rel ^ "(" ^ space_implode ", " vnames ^ ")),\n" ^
"writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^
"\\n', [" ^ space_implode ", " vnames ^ "]).\n"
-fun query_firstn n rel vnames =
+fun swi_prolog_query_firstn n rel vnames =
"eval :- findnsols(" ^ string_of_int n ^ ", (" ^ space_implode ", " vnames ^ "), " ^
rel ^ "(" ^ space_implode ", " vnames ^ "), Sols), writelist(Sols).\n" ^
"writelist([]).\n" ^
@@ -411,7 +423,7 @@
"writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^
"\\n', [" ^ space_implode ", " vnames ^ "]), writelist(T).\n"
-val prelude =
+val swi_prolog_prelude =
"#!/usr/bin/swipl -q -t main -f\n\n" ^
":- use_module(library('dialect/ciao/aggregates')).\n" ^
":- style_check(-singleton).\n" ^
@@ -420,7 +432,38 @@
"main :- catch(eval, E, (print_message(error, E), fail)), halt.\n" ^
"main :- halt(1).\n"
+(** query and prelude for yap **)
+
+fun yap_query_first rel vnames =
+ "eval :- once(" ^ rel ^ "(" ^ space_implode ", " vnames ^ ")),\n" ^
+ "format('" ^ space_implode ";" (map (fn v => v ^ " = ~w") vnames) ^
+ "\\n', [" ^ space_implode ", " vnames ^ "]).\n"
+
+val yap_prelude =
+ "#!/usr/bin/yap -L\n\n" ^
+ ":- initialization(eval).\n"
+
+(* system-dependent query, prelude and invocation *)
+
+fun query system nsols =
+ case system of
+ SWI_PROLOG =>
+ (case nsols of NONE => swi_prolog_query_first | SOME n => swi_prolog_query_firstn n)
+ | YAP =>
+ case nsols of NONE => yap_query_first | SOME n =>
+ error "No support for querying multiple solutions in the prolog system yap"
+
+fun prelude system =
+ case system of SWI_PROLOG => swi_prolog_prelude | YAP => yap_prelude
+
+fun invoke system file_name =
+ let
+ val cmd =
+ case system of SWI_PROLOG => "/usr/local/bin/swipl -f " | YAP => "/usr/local/bin/yap -L "
+ in bash_output (cmd ^ file_name) end
+
(* parsing prolog solution *)
+
val scan_number =
Scan.many1 Symbol.is_ascii_digit
@@ -471,26 +514,25 @@
(* calling external interpreter and getting results *)
-fun run p query_rel vnames nsols =
+fun run system p query_rel vnames nsols =
let
val cmd = Path.named_root
- val query = case nsols of NONE => query_first | SOME n => query_firstn n
val p' = rename_vars_program p
val _ = tracing "Renaming variable names..."
val renaming = fold mk_renaming vnames []
val vnames' = map (fn v => the (AList.lookup (op =) renaming v)) vnames
- val prog = prelude ^ query query_rel vnames' ^ write_program p'
+ val prog = prelude system ^ query system nsols query_rel vnames' ^ write_program p'
val _ = tracing ("Generated prolog program:\n" ^ prog)
val prolog_file = File.tmp_path (Path.basic "prolog_file")
val _ = File.write prolog_file prog
- val (solution, _) = bash_output ("/usr/local/bin/swipl -f " ^ File.shell_path prolog_file)
+ val (solution, _) = invoke system (File.shell_path prolog_file)
val _ = tracing ("Prolog returned solution(s):\n" ^ solution)
val tss = parse_solutions solution
in
tss
end
-(* values command *)
+(* restoring types in terms *)
fun restore_term ctxt constant_table (Var s, T) = Free (s, T)
| restore_term ctxt constant_table (Number n, @{typ "int"}) = HOLogic.mk_number @{typ "int"} n
@@ -509,6 +551,30 @@
map (restore_term ctxt constant_table) (args ~~ argsT'))
end
+(* values command *)
+
+val preprocess_options = Predicate_Compile_Aux.Options {
+ expected_modes = NONE,
+ proposed_modes = NONE,
+ proposed_names = [],
+ show_steps = false,
+ show_intermediate_results = false,
+ show_proof_trace = false,
+ show_modes = false,
+ show_mode_inference = false,
+ show_compilation = false,
+ show_caught_failures = false,
+ skip_proof = true,
+ no_topmost_reordering = false,
+ function_flattening = true,
+ specialise = false,
+ fail_safe_function_flattening = false,
+ no_higher_order_predicate = [],
+ inductify = false,
+ detect_switches = true,
+ compilation = Predicate_Compile_Aux.Pred
+}
+
fun values ctxt soln t_compr =
let
val options = !options
@@ -535,10 +601,13 @@
|> Predicate_Compile.preprocess preprocess_options t
val ctxt' = ProofContext.init_global thy'
val _ = tracing "Generating prolog program..."
- val (p, constant_table) = generate options ctxt' name
- |> (if #ensure_groundness options then add_ground_predicates ctxt' else I)
+ val (p, constant_table) = generate (#ensure_groundness options) ctxt' name
+ |> (if #ensure_groundness options then
+ add_ground_predicates ctxt' (#limited_types options)
+ else I)
val _ = tracing "Running prolog program..."
- val tss = run p (translate_const constant_table name) (map first_upper vnames) soln
+ val tss = run (#prolog_system options)
+ p (translate_const constant_table name) (map first_upper vnames) soln
val _ = tracing "Restoring terms..."
val empty = Const("Orderings.bot_class.bot", fastype_of t_compr)
fun mk_insert x S =
@@ -596,10 +665,10 @@
(* FIXME: large copy of Predicate_Compile_Quickcheck - refactor out commons *)
-fun strip_imp_prems (Const(@{const_name "op -->"}, _) $ A $ B) = A :: strip_imp_prems B
+fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
| strip_imp_prems _ = [];
-fun strip_imp_concl (Const(@{const_name "op -->"}, _) $ A $ B) = strip_imp_concl B
+fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
| strip_imp_concl A = A : term;
fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
@@ -626,11 +695,11 @@
val thy3 = Predicate_Compile.preprocess preprocess_options const thy2
val ctxt' = ProofContext.init_global thy3
val _ = tracing "Generating prolog program..."
- val (p, constant_table) = generate {ensure_groundness = true} ctxt' full_constname
- |> add_ground_predicates ctxt'
+ val (p, constant_table) = generate true ctxt' full_constname
+ |> add_ground_predicates ctxt' (#limited_types (!options))
val _ = tracing "Running prolog program..."
- val [ts] = run p (translate_const constant_table full_constname) (map fst vs')
- (SOME 1)
+ val [ts] = run (#prolog_system (!options))
+ p (translate_const constant_table full_constname) (map fst vs') (SOME 1)
val _ = tracing "Restoring terms..."
val res = SOME (map (restore_term ctxt' constant_table) (ts ~~ Ts))
val empty_report = ([], false)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Aug 27 12:57:55 2010 +0200
@@ -405,7 +405,7 @@
(* general syntactic functions *)
(*Like dest_conj, but flattens conjunctions however nested*)
-fun conjuncts_aux (Const (@{const_name "op &"}, _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
+fun conjuncts_aux (Const (@{const_name HOL.conj}, _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
| conjuncts_aux t conjs = t::conjs;
fun conjuncts t = conjuncts_aux t [];
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Aug 27 12:57:55 2010 +0200
@@ -524,7 +524,7 @@
fun dest_conjunct_prem th =
case HOLogic.dest_Trueprop (prop_of th) of
- (Const (@{const_name "op &"}, _) $ t $ t') =>
+ (Const (@{const_name HOL.conj}, _) $ t $ t') =>
dest_conjunct_prem (th RS @{thm conjunct1})
@ dest_conjunct_prem (th RS @{thm conjunct2})
| _ => [th]
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Aug 27 12:57:55 2010 +0200
@@ -218,11 +218,11 @@
@{const_name Trueprop},
@{const_name Not},
@{const_name "op ="},
- @{const_name "op -->"},
+ @{const_name HOL.implies},
@{const_name All},
@{const_name Ex},
- @{const_name "op &"},
- @{const_name "op |"}]
+ @{const_name HOL.conj},
+ @{const_name HOL.disj}]
fun special_cases (c, T) = member (op =) [
@{const_name Product_Type.Unity},
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Aug 27 12:57:55 2010 +0200
@@ -89,8 +89,8 @@
fun is_compound ((Const (@{const_name Not}, _)) $ t) =
error "is_compound: Negation should not occur; preprocessing is defect"
| is_compound ((Const (@{const_name Ex}, _)) $ _) = true
- | is_compound ((Const (@{const_name "op |"}, _)) $ _ $ _) = true
- | is_compound ((Const (@{const_name "op &"}, _)) $ _ $ _) =
+ | is_compound ((Const (@{const_name HOL.disj}, _)) $ _ $ _) = true
+ | is_compound ((Const (@{const_name HOL.conj}, _)) $ _ $ _) =
error "is_compound: Conjunction should not occur; preprocessing is defect"
| is_compound _ = false
@@ -250,7 +250,7 @@
fun split_conjs thy t =
let
- fun split_conjunctions (Const (@{const_name "op &"}, _) $ t1 $ t2) =
+ fun split_conjunctions (Const (@{const_name HOL.conj}, _) $ t1 $ t2) =
(split_conjunctions t1) @ (split_conjunctions t2)
| split_conjunctions t = [t]
in
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Aug 27 12:57:55 2010 +0200
@@ -168,10 +168,10 @@
mk_split_lambda' xs t
end;
-fun strip_imp_prems (Const(@{const_name "op -->"}, _) $ A $ B) = A :: strip_imp_prems B
+fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
| strip_imp_prems _ = [];
-fun strip_imp_concl (Const(@{const_name "op -->"}, _) $ A $ B) = strip_imp_concl B
+fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
| strip_imp_concl A = A : term;
fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
--- a/src/HOL/Tools/Qelim/cooper.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Fri Aug 27 12:57:55 2010 +0200
@@ -28,7 +28,7 @@
@{term "op * :: int => _"}, @{term "op * :: nat => _"},
@{term "op div :: int => _"}, @{term "op div :: nat => _"},
@{term "op mod :: int => _"}, @{term "op mod :: nat => _"},
- @{term "op &"}, @{term "op |"}, @{term "op -->"},
+ @{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies},
@{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"},
@{term "op < :: int => _"}, @{term "op < :: nat => _"},
@{term "op <= :: int => _"}, @{term "op <= :: nat => _"},
@@ -120,8 +120,8 @@
fun whatis x ct =
( case (term_of ct) of
- Const(@{const_name "op &"},_)$_$_ => And (Thm.dest_binop ct)
-| Const (@{const_name "op |"},_)$_$_ => Or (Thm.dest_binop ct)
+ Const(@{const_name HOL.conj},_)$_$_ => And (Thm.dest_binop ct)
+| Const (@{const_name HOL.disj},_)$_$_ => Or (Thm.dest_binop ct)
| Const (@{const_name "op ="},_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
| Const (@{const_name Not},_) $ (Const (@{const_name "op ="},_)$y$_) =>
if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
@@ -353,8 +353,8 @@
then (ins (dest_number c) acc, dacc) else (acc,dacc)
| Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_) =>
if x aconv y then (acc,ins (dest_number c) dacc) else (acc,dacc)
- | Const(@{const_name "op &"},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
- | Const(@{const_name "op |"},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
+ | Const(@{const_name HOL.conj},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
+ | Const(@{const_name HOL.disj},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
| Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t)
| _ => (acc, dacc)
val (cs,ds) = h ([],[]) p
@@ -382,8 +382,8 @@
end
fun unit_conv t =
case (term_of t) of
- Const(@{const_name "op &"},_)$_$_ => Conv.binop_conv unit_conv t
- | Const(@{const_name "op |"},_)$_$_ => Conv.binop_conv unit_conv t
+ Const(@{const_name HOL.conj},_)$_$_ => Conv.binop_conv unit_conv t
+ | Const(@{const_name HOL.disj},_)$_$_ => Conv.binop_conv unit_conv t
| Const (@{const_name Not},_)$_ => Conv.arg_conv unit_conv t
| Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
if x=y andalso member (op =)
@@ -569,7 +569,7 @@
fun add_bools t =
let
val ops = [@{term "op = :: int => _"}, @{term "op < :: int => _"}, @{term "op <= :: int => _"},
- @{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
+ @{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies}, @{term "op = :: bool => _"},
@{term "Not"}, @{term "All :: (int => _) => _"},
@{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}];
val is_op = member (op =) ops;
@@ -612,11 +612,11 @@
fun fm_of_term ps vs (Const (@{const_name True}, _)) = Proc.T
| fm_of_term ps vs (Const (@{const_name False}, _)) = Proc.F
- | fm_of_term ps vs (Const (@{const_name "op &"}, _) $ t1 $ t2) =
+ | fm_of_term ps vs (Const (@{const_name HOL.conj}, _) $ t1 $ t2) =
Proc.And (fm_of_term ps vs t1, fm_of_term ps vs t2)
- | fm_of_term ps vs (Const (@{const_name "op |"}, _) $ t1 $ t2) =
+ | fm_of_term ps vs (Const (@{const_name HOL.disj}, _) $ t1 $ t2) =
Proc.Or (fm_of_term ps vs t1, fm_of_term ps vs t2)
- | fm_of_term ps vs (Const (@{const_name "op -->"}, _) $ t1 $ t2) =
+ | fm_of_term ps vs (Const (@{const_name HOL.implies}, _) $ t1 $ t2) =
Proc.Imp (fm_of_term ps vs t1, fm_of_term ps vs t2)
| fm_of_term ps vs (@{term "op = :: bool => _ "} $ t1 $ t2) =
Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2)
@@ -687,7 +687,7 @@
fun strip_objimp ct =
(case Thm.term_of ct of
- Const (@{const_name "op -->"}, _) $ _ $ _ =>
+ Const (@{const_name HOL.implies}, _) $ _ $ _ =>
let val (A, B) = Thm.dest_binop ct
in A :: strip_objimp B end
| _ => [ct]);
@@ -712,7 +712,7 @@
val qs = filter P ps
val q = if P c then c else @{cterm "False"}
val ng = fold_rev (fn (a,v) => fn t => Thm.capply a (Thm.cabs v t)) qvs
- (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm "op -->"} p) q) qs q)
+ (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm HOL.implies} p) q) qs q)
val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p'
val ntac = (case qs of [] => q aconvc @{cterm "False"}
| _ => false)
--- a/src/HOL/Tools/Qelim/qelim.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML Fri Aug 27 12:57:55 2010 +0200
@@ -25,8 +25,8 @@
case (term_of p) of
Const(s,T)$_$_ =>
if domain_type T = HOLogic.boolT
- andalso member (op =) [@{const_name "op &"}, @{const_name "op |"},
- @{const_name "op -->"}, @{const_name "op ="}] s
+ andalso member (op =) [@{const_name HOL.conj}, @{const_name HOL.disj},
+ @{const_name HOL.implies}, @{const_name "op ="}] s
then binop_conv (conv env) p
else atcv env p
| Const(@{const_name Not},_)$_ => arg_conv (conv env) p
--- a/src/HOL/Tools/Quotient/quotient_term.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Aug 27 12:57:55 2010 +0200
@@ -485,7 +485,7 @@
end
| (Const (@{const_name Ex1}, ty) $ (Abs (_, _,
- (Const (@{const_name "op &"}, _) $ (Const (@{const_name Set.member}, _) $ _ $
+ (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name Set.member}, _) $ _ $
(Const (@{const_name Respects}, _) $ resrel)) $ (t $ _)))),
Const (@{const_name Ex1}, ty') $ t') =>
let
--- a/src/HOL/Tools/SMT/smtlib_interface.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Fri Aug 27 12:57:55 2010 +0200
@@ -159,9 +159,9 @@
fun conn @{const_name True} = SOME "true"
| conn @{const_name False} = SOME "false"
| conn @{const_name Not} = SOME "not"
- | conn @{const_name "op &"} = SOME "and"
- | conn @{const_name "op |"} = SOME "or"
- | conn @{const_name "op -->"} = SOME "implies"
+ | conn @{const_name HOL.conj} = SOME "and"
+ | conn @{const_name HOL.disj} = SOME "or"
+ | conn @{const_name HOL.implies} = SOME "implies"
| conn @{const_name "op ="} = SOME "iff"
| conn @{const_name If} = SOME "if_then_else"
| conn _ = NONE
--- a/src/HOL/Tools/SMT/z3_interface.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML Fri Aug 27 12:57:55 2010 +0200
@@ -170,7 +170,7 @@
val mk_true = @{cterm "~False"}
val mk_false = @{cterm False}
val mk_not = Thm.capply @{cterm Not}
-val mk_implies = Thm.mk_binop @{cterm "op -->"}
+val mk_implies = Thm.mk_binop @{cterm HOL.implies}
val mk_iff = Thm.mk_binop @{cterm "op = :: bool => _"}
fun mk_nary _ cu [] = cu
@@ -216,8 +216,8 @@
(Sym ("true", _), []) => SOME mk_true
| (Sym ("false", _), []) => SOME mk_false
| (Sym ("not", _), [ct]) => SOME (mk_not ct)
- | (Sym ("and", _), _) => SOME (mk_nary @{cterm "op &"} mk_true cts)
- | (Sym ("or", _), _) => SOME (mk_nary @{cterm "op |"} mk_false cts)
+ | (Sym ("and", _), _) => SOME (mk_nary @{cterm HOL.conj} mk_true cts)
+ | (Sym ("or", _), _) => SOME (mk_nary @{cterm HOL.disj} mk_false cts)
| (Sym ("implies", _), [ct, cu]) => SOME (mk_implies ct cu)
| (Sym ("iff", _), [ct, cu]) => SOME (mk_iff ct cu)
| (Sym ("~", _), [ct, cu]) => SOME (mk_iff ct cu)
--- a/src/HOL/Tools/SMT/z3_proof_literals.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_literals.ML Fri Aug 27 12:57:55 2010 +0200
@@ -62,14 +62,14 @@
val is_neg = (fn @{term Not} $ _ => true | _ => false)
fun is_neg' f = (fn @{term Not} $ t => f t | _ => false)
val is_dneg = is_neg' is_neg
-val is_conj = (fn @{term "op &"} $ _ $ _ => true | _ => false)
-val is_disj = (fn @{term "op |"} $ _ $ _ => true | _ => false)
+val is_conj = (fn @{term HOL.conj} $ _ $ _ => true | _ => false)
+val is_disj = (fn @{term HOL.disj} $ _ $ _ => true | _ => false)
fun dest_disj_term' f = (fn
- @{term Not} $ (@{term "op |"} $ t $ u) => SOME (f t, f u)
+ @{term Not} $ (@{term HOL.disj} $ t $ u) => SOME (f t, f u)
| _ => NONE)
-val dest_conj_term = (fn @{term "op &"} $ t $ u => SOME (t, u) | _ => NONE)
+val dest_conj_term = (fn @{term HOL.conj} $ t $ u => SOME (t, u) | _ => NONE)
val dest_disj_term =
dest_disj_term' (fn @{term Not} $ t => t | t => @{term Not} $ t)
@@ -202,11 +202,11 @@
| comp_disj ((true, thm1), (false, thm2)) = comp2 disj3 thm1 thm2
| comp_disj ((true, thm1), (true, thm2)) = comp2 disj4 thm1 thm2
- fun dest_conj (@{term "op &"} $ t $ u) = ((false, t), (false, u))
+ fun dest_conj (@{term HOL.conj} $ t $ u) = ((false, t), (false, u))
| dest_conj t = raise TERM ("dest_conj", [t])
val neg = (fn @{term Not} $ t => (true, t) | t => (false, @{term Not} $ t))
- fun dest_disj (@{term Not} $ (@{term "op |"} $ t $ u)) = (neg t, neg u)
+ fun dest_disj (@{term Not} $ (@{term HOL.disj} $ t $ u)) = (neg t, neg u)
| dest_disj t = raise TERM ("dest_disj", [t])
val dnegE = T.precompose (single o d2 o d1) @{thm notnotD}
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri Aug 27 12:57:55 2010 +0200
@@ -298,13 +298,13 @@
let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct)
in
(case Thm.term_of ct1 of
- @{term Not} $ (@{term "op &"} $ _ $ _) =>
+ @{term Not} $ (@{term HOL.conj} $ _ $ _) =>
prove disjI1 (Thm.dest_arg ct1, true) (ct2, true)
- | @{term "op &"} $ _ $ _ =>
+ | @{term HOL.conj} $ _ $ _ =>
prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, true)
- | @{term Not} $ (@{term "op |"} $ _ $ _) =>
+ | @{term Not} $ (@{term HOL.disj} $ _ $ _) =>
prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, false)
- | @{term "op |"} $ _ $ _ =>
+ | @{term HOL.disj} $ _ $ _ =>
prove disjI2 (Thm.capply @{cterm Not} ct1, false) (ct2, true)
| Const (@{const_name distinct}, _) $ _ =>
let
@@ -477,8 +477,8 @@
fun mono f (cp as (cl, _)) =
(case Term.head_of (Thm.term_of cl) of
- @{term "op &"} => prove_nary L.is_conj (prove_eq_exn f)
- | @{term "op |"} => prove_nary L.is_disj (prove_eq_exn f)
+ @{term HOL.conj} => prove_nary L.is_conj (prove_eq_exn f)
+ | @{term HOL.disj} => prove_nary L.is_disj (prove_eq_exn f)
| Const (@{const_name distinct}, _) => prove_distinct (prove_eq_safe f)
| _ => prove (prove_eq_safe f)) cp
in
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Fri Aug 27 12:57:55 2010 +0200
@@ -196,9 +196,9 @@
| @{term True} => pair ct
| @{term False} => pair ct
| @{term Not} $ _ => abstr1 cvs ct
- | @{term "op &"} $ _ $ _ => abstr2 cvs ct
- | @{term "op |"} $ _ $ _ => abstr2 cvs ct
- | @{term "op -->"} $ _ $ _ => abstr2 cvs ct
+ | @{term HOL.conj} $ _ $ _ => abstr2 cvs ct
+ | @{term HOL.disj} $ _ $ _ => abstr2 cvs ct
+ | @{term HOL.implies} $ _ $ _ => abstr2 cvs ct
| Const (@{const_name "op ="}, _) $ _ $ _ => abstr2 cvs ct
| Const (@{const_name distinct}, _) $ _ =>
if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Fri Aug 27 12:57:55 2010 +0200
@@ -68,8 +68,8 @@
(*Universal quant: insert a free variable into body and continue*)
let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
in dec_sko (subst_bound (Free(fname,T), p)) rhss end
- | dec_sko (@{const "op &"} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
- | dec_sko (@{const "op |"} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
+ | dec_sko (@{const HOL.conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
+ | dec_sko (@{const HOL.disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
| dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss
| dec_sko _ rhss = rhss
in dec_sko (prop_of th) [] end;
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Fri Aug 27 12:57:55 2010 +0200
@@ -95,9 +95,9 @@
Symtab.make [(@{type_name Product_Type.prod}, "prod"),
(@{type_name Sum_Type.sum}, "sum"),
(@{const_name "op ="}, "equal"),
- (@{const_name "op &"}, "and"),
- (@{const_name "op |"}, "or"),
- (@{const_name "op -->"}, "implies"),
+ (@{const_name HOL.conj}, "and"),
+ (@{const_name HOL.disj}, "or"),
+ (@{const_name HOL.implies}, "implies"),
(@{const_name Set.member}, "member"),
(@{const_name fequal}, "fequal"),
(@{const_name COMBI}, "COMBI"),
@@ -430,7 +430,7 @@
fun literals_of_term1 args thy (@{const Trueprop} $ P) =
literals_of_term1 args thy P
- | literals_of_term1 args thy (@{const "op |"} $ P $ Q) =
+ | literals_of_term1 args thy (@{const HOL.disj} $ P $ Q) =
literals_of_term1 (literals_of_term1 args thy P) thy Q
| literals_of_term1 (lits, ts) thy P =
let val ((pred, ts'), pol) = predicate_of thy (P, true) in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Aug 27 12:57:55 2010 +0200
@@ -159,9 +159,9 @@
do_quantifier (pos = SOME false) body_t
| Const (@{const_name Ex}, _) $ Abs (_, _, body_t) =>
do_quantifier (pos = SOME true) body_t
- | @{const "op &"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
- | @{const "op |"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
- | @{const "op -->"} $ t1 $ t2 =>
+ | @{const HOL.conj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
+ | @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
+ | @{const HOL.implies} $ t1 $ t2 =>
do_formula (flip pos) t1 #> do_formula pos t2
| Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 =>
fold (do_term_or_formula T) [t1, t2]
@@ -541,12 +541,12 @@
| (_, @{const "==>"} $ t1 $ t2) =>
do_formula (not pos) t1 andalso
(t2 = @{prop False} orelse do_formula pos t2)
- | (_, @{const "op -->"} $ t1 $ t2) =>
+ | (_, @{const HOL.implies} $ t1 $ t2) =>
do_formula (not pos) t1 andalso
(t2 = @{const False} orelse do_formula pos t2)
| (_, @{const Not} $ t1) => do_formula (not pos) t1
- | (true, @{const "op |"} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
- | (false, @{const "op &"} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
+ | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
+ | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
| (true, Const (@{const_name "op ="}, _) $ t1 $ t2) => do_equals t1 t2
| (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
| _ => false
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Aug 27 12:57:55 2010 +0200
@@ -69,12 +69,12 @@
Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
| negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
- | negate_term (@{const "op -->"} $ t1 $ t2) =
- @{const "op &"} $ t1 $ negate_term t2
- | negate_term (@{const "op &"} $ t1 $ t2) =
- @{const "op |"} $ negate_term t1 $ negate_term t2
- | negate_term (@{const "op |"} $ t1 $ t2) =
- @{const "op &"} $ negate_term t1 $ negate_term t2
+ | negate_term (@{const HOL.implies} $ t1 $ t2) =
+ @{const HOL.conj} $ t1 $ negate_term t2
+ | negate_term (@{const HOL.conj} $ t1 $ t2) =
+ @{const HOL.disj} $ negate_term t1 $ negate_term t2
+ | negate_term (@{const HOL.disj} $ t1 $ t2) =
+ @{const HOL.conj} $ negate_term t1 $ negate_term t2
| negate_term (@{const Not} $ t) = t
| negate_term t = @{const Not} $ t
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Fri Aug 27 12:57:55 2010 +0200
@@ -70,9 +70,9 @@
do_quant bs AForall s T t'
| Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
do_quant bs AExists s T t'
- | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2
- | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2
- | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2
+ | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
+ | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
+ | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
| Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
do_conn bs AIff t1 t2
| _ => (fn ts => do_term bs (Envir.eta_contract t)
@@ -125,9 +125,9 @@
t0 $ Abs (s, T, aux (T :: Ts) t')
| (t0 as Const (@{const_name Ex}, _)) $ t1 =>
aux Ts (t0 $ eta_expand Ts t1 1)
- | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
| (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
$ t1 $ t2 =>
t0 $ aux Ts t1 $ aux Ts t2
--- a/src/HOL/Tools/TFL/dcterm.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/TFL/dcterm.ML Fri Aug 27 12:57:55 2010 +0200
@@ -79,11 +79,11 @@
in capply c (uncurry cabs r) end;
-local val c = mk_hol_const(@{const_name "op &"}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+local val c = mk_hol_const(@{const_name HOL.conj}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
end;
-local val c = mk_hol_const(@{const_name "op |"}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+local val c = mk_hol_const(@{const_name HOL.disj}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2
end;
@@ -128,9 +128,9 @@
val dest_neg = dest_monop @{const_name Not}
val dest_pair = dest_binop @{const_name Pair}
val dest_eq = dest_binop @{const_name "op ="}
-val dest_imp = dest_binop @{const_name "op -->"}
-val dest_conj = dest_binop @{const_name "op &"}
-val dest_disj = dest_binop @{const_name "op |"}
+val dest_imp = dest_binop @{const_name HOL.implies}
+val dest_conj = dest_binop @{const_name HOL.conj}
+val dest_disj = dest_binop @{const_name HOL.disj}
val dest_select = dest_binder @{const_name Eps}
val dest_exists = dest_binder @{const_name Ex}
val dest_forall = dest_binder @{const_name All}
--- a/src/HOL/Tools/TFL/usyntax.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML Fri Aug 27 12:57:55 2010 +0200
@@ -159,7 +159,7 @@
fun mk_imp{ant,conseq} =
- let val c = Const(@{const_name "op -->"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+ let val c = Const(@{const_name HOL.implies},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in list_comb(c,[ant,conseq])
end;
@@ -183,12 +183,12 @@
fun mk_conj{conj1,conj2} =
- let val c = Const(@{const_name "op &"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+ let val c = Const(@{const_name HOL.conj},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in list_comb(c,[conj1,conj2])
end;
fun mk_disj{disj1,disj2} =
- let val c = Const(@{const_name "op |"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+ let val c = Const(@{const_name HOL.disj},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in list_comb(c,[disj1,disj2])
end;
@@ -247,7 +247,7 @@
fun dest_eq(Const(@{const_name "op ="},_) $ M $ N) = {lhs=M, rhs=N}
| dest_eq _ = raise USYN_ERR "dest_eq" "not an equality";
-fun dest_imp(Const(@{const_name "op -->"},_) $ M $ N) = {ant=M, conseq=N}
+fun dest_imp(Const(@{const_name HOL.implies},_) $ M $ N) = {ant=M, conseq=N}
| dest_imp _ = raise USYN_ERR "dest_imp" "not an implication";
fun dest_forall(Const(@{const_name All},_) $ (a as Abs _)) = fst (dest_abs [] a)
@@ -259,10 +259,10 @@
fun dest_neg(Const(@{const_name Not},_) $ M) = M
| dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
-fun dest_conj(Const(@{const_name "op &"},_) $ M $ N) = {conj1=M, conj2=N}
+fun dest_conj(Const(@{const_name HOL.conj},_) $ M $ N) = {conj1=M, conj2=N}
| dest_conj _ = raise USYN_ERR "dest_conj" "not a conjunction";
-fun dest_disj(Const(@{const_name "op |"},_) $ M $ N) = {disj1=M, disj2=N}
+fun dest_disj(Const(@{const_name HOL.disj},_) $ M $ N) = {disj1=M, disj2=N}
| dest_disj _ = raise USYN_ERR "dest_disj" "not a disjunction";
fun mk_pair{fst,snd} =
--- a/src/HOL/Tools/cnf_funcs.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Fri Aug 27 12:57:55 2010 +0200
@@ -95,9 +95,9 @@
fun is_atom (Const (@{const_name False}, _)) = false
| is_atom (Const (@{const_name True}, _)) = false
- | is_atom (Const (@{const_name "op &"}, _) $ _ $ _) = false
- | is_atom (Const (@{const_name "op |"}, _) $ _ $ _) = false
- | is_atom (Const (@{const_name "op -->"}, _) $ _ $ _) = false
+ | is_atom (Const (@{const_name HOL.conj}, _) $ _ $ _) = false
+ | is_atom (Const (@{const_name HOL.disj}, _) $ _ $ _) = false
+ | is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _) = false
| is_atom (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ _ $ _) = false
| is_atom (Const (@{const_name Not}, _) $ _) = false
| is_atom _ = true;
@@ -105,7 +105,7 @@
fun is_literal (Const (@{const_name Not}, _) $ x) = is_atom x
| is_literal x = is_atom x;
-fun is_clause (Const (@{const_name "op |"}, _) $ x $ y) = is_clause x andalso is_clause y
+fun is_clause (Const (@{const_name HOL.disj}, _) $ x $ y) = is_clause x andalso is_clause y
| is_clause x = is_literal x;
(* ------------------------------------------------------------------------- *)
@@ -184,21 +184,21 @@
(* Theory.theory -> Term.term -> Thm.thm *)
-fun make_nnf_thm thy (Const (@{const_name "op &"}, _) $ x $ y) =
+fun make_nnf_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy y
in
conj_cong OF [thm1, thm2]
end
- | make_nnf_thm thy (Const (@{const_name "op |"}, _) $ x $ y) =
+ | make_nnf_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy y
in
disj_cong OF [thm1, thm2]
end
- | make_nnf_thm thy (Const (@{const_name "op -->"}, _) $ x $ y) =
+ | make_nnf_thm thy (Const (@{const_name HOL.implies}, _) $ x $ y) =
let
val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
val thm2 = make_nnf_thm thy y
@@ -218,21 +218,21 @@
make_nnf_not_false
| make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) =
make_nnf_not_true
- | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op &"}, _) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.conj}, _) $ x $ y)) =
let
val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
in
make_nnf_not_conj OF [thm1, thm2]
end
- | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op |"}, _) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.disj}, _) $ x $ y)) =
let
val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
in
make_nnf_not_disj OF [thm1, thm2]
end
- | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op -->"}, _) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.implies}, _) $ x $ y)) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
@@ -276,7 +276,7 @@
(* Theory.theory -> Term.term -> Thm.thm *)
-fun simp_True_False_thm thy (Const (@{const_name "op &"}, _) $ x $ y) =
+fun simp_True_False_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) =
let
val thm1 = simp_True_False_thm thy x
val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
@@ -298,7 +298,7 @@
conj_cong OF [thm1, thm2] (* (x & y) = (x' & y') *)
end
end
- | simp_True_False_thm thy (Const (@{const_name "op |"}, _) $ x $ y) =
+ | simp_True_False_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) =
let
val thm1 = simp_True_False_thm thy x
val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
@@ -334,24 +334,24 @@
fun make_cnf_thm thy t =
let
(* Term.term -> Thm.thm *)
- fun make_cnf_thm_from_nnf (Const (@{const_name "op &"}, _) $ x $ y) =
+ fun make_cnf_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) =
let
val thm1 = make_cnf_thm_from_nnf x
val thm2 = make_cnf_thm_from_nnf y
in
conj_cong OF [thm1, thm2]
end
- | make_cnf_thm_from_nnf (Const (@{const_name "op |"}, _) $ x $ y) =
+ | make_cnf_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) =
let
(* produces a theorem "(x' | y') = t'", where x', y', and t' are in CNF *)
- fun make_cnf_disj_thm (Const (@{const_name "op &"}, _) $ x1 $ x2) y' =
+ fun make_cnf_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' =
let
val thm1 = make_cnf_disj_thm x1 y'
val thm2 = make_cnf_disj_thm x2 y'
in
make_cnf_disj_conj_l OF [thm1, thm2] (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
end
- | make_cnf_disj_thm x' (Const (@{const_name "op &"}, _) $ y1 $ y2) =
+ | make_cnf_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) =
let
val thm1 = make_cnf_disj_thm x' y1
val thm2 = make_cnf_disj_thm x' y2
@@ -403,27 +403,27 @@
val var_id = Unsynchronized.ref 0 (* properly initialized below *)
fun new_free () =
Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT)
- fun make_cnfx_thm_from_nnf (Const (@{const_name "op &"}, _) $ x $ y) : thm =
+ fun make_cnfx_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) : thm =
let
val thm1 = make_cnfx_thm_from_nnf x
val thm2 = make_cnfx_thm_from_nnf y
in
conj_cong OF [thm1, thm2]
end
- | make_cnfx_thm_from_nnf (Const (@{const_name "op |"}, _) $ x $ y) =
+ | make_cnfx_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) =
if is_clause x andalso is_clause y then
inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl
else if is_literal y orelse is_literal x then let
(* produces a theorem "(x' | y') = t'", where x', y', and t' are *)
(* almost in CNF, and x' or y' is a literal *)
- fun make_cnfx_disj_thm (Const (@{const_name "op &"}, _) $ x1 $ x2) y' =
+ fun make_cnfx_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' =
let
val thm1 = make_cnfx_disj_thm x1 y'
val thm2 = make_cnfx_disj_thm x2 y'
in
make_cnf_disj_conj_l OF [thm1, thm2] (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
end
- | make_cnfx_disj_thm x' (Const (@{const_name "op &"}, _) $ y1 $ y2) =
+ | make_cnfx_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) =
let
val thm1 = make_cnfx_disj_thm x' y1
val thm2 = make_cnfx_disj_thm x' y2
--- a/src/HOL/Tools/groebner.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/groebner.ML Fri Aug 27 12:57:55 2010 +0200
@@ -395,7 +395,7 @@
fun refute_disj rfn tm =
case term_of tm of
- Const(@{const_name "op |"},_)$l$r =>
+ Const(@{const_name HOL.disj},_)$l$r =>
compose_single(refute_disj rfn (dest_arg tm),2,compose_single(refute_disj rfn (dest_arg1 tm),2,disjE))
| _ => rfn tm ;
@@ -454,7 +454,7 @@
val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
val cTrp = @{cterm "Trueprop"};
-val cConj = @{cterm "op &"};
+val cConj = @{cterm HOL.conj};
val (cNot,false_tm) = (@{cterm "Not"}, @{cterm "False"});
val assume_Trueprop = mk_comb cTrp #> assume;
val list_mk_conj = list_mk_binop cConj;
@@ -479,22 +479,22 @@
(* FIXME : copied from cqe.ML -- complex QE*)
fun conjuncts ct =
case term_of ct of
- @{term "op &"}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
+ @{term HOL.conj}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
| _ => [ct];
fun fold1 f = foldr1 (uncurry f);
-val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm "op &"} c) c') ;
+val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm HOL.conj} c) c') ;
fun mk_conj_tab th =
let fun h acc th =
case prop_of th of
- @{term "Trueprop"}$(@{term "op &"}$p$q) =>
+ @{term "Trueprop"}$(@{term HOL.conj}$p$q) =>
h (h acc (th RS conjunct2)) (th RS conjunct1)
| @{term "Trueprop"}$p => (p,th)::acc
in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
-fun is_conj (@{term "op &"}$_$_) = true
+fun is_conj (@{term HOL.conj}$_$_) = true
| is_conj _ = false;
fun prove_conj tab cjs =
@@ -852,14 +852,14 @@
fun unwind_polys_conv tm =
let
val (vars,bod) = strip_exists tm
- val cjs = striplist (dest_binary @{cterm "op &"}) bod
+ val cjs = striplist (dest_binary @{cterm HOL.conj}) bod
val th1 = (the (get_first (try (isolate_variable vars)) cjs)
handle Option => raise CTERM ("unwind_polys_conv",[tm]))
val eq = Thm.lhs_of th1
- val bod' = list_mk_binop @{cterm "op &"} (eq::(remove op aconvc eq cjs))
+ val bod' = list_mk_binop @{cterm HOL.conj} (eq::(remove op aconvc eq cjs))
val th2 = conj_ac_rule (mk_eq bod bod')
val th3 = transitive th2
- (Drule.binop_cong_rule @{cterm "op &"} th1
+ (Drule.binop_cong_rule @{cterm HOL.conj} th1
(reflexive (Thm.dest_arg (Thm.rhs_of th2))))
val v = Thm.dest_arg1(Thm.dest_arg1(Thm.rhs_of th3))
val vars' = (remove op aconvc v vars) @ [v]
@@ -929,9 +929,9 @@
| Const (@{const_name Not}, _) $ _ => find_term bounds (dest_arg tm)
| Const (@{const_name All}, _) $ _ => find_body bounds (dest_arg tm)
| Const (@{const_name Ex}, _) $ _ => find_body bounds (dest_arg tm)
- | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
- | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
- | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
| @{term "op ==>"} $_$_ => find_args bounds tm
| Const("op ==",_)$_$_ => find_args bounds tm
| @{term Trueprop}$_ => find_term bounds (dest_arg tm)
--- a/src/HOL/Tools/hologic.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/hologic.ML Fri Aug 27 12:57:55 2010 +0200
@@ -208,29 +208,29 @@
let val (th1, th2) = conj_elim th
in conj_elims th1 @ conj_elims th2 end handle THM _ => [th];
-val conj = @{term "op &"}
-and disj = @{term "op |"}
-and imp = @{term "op -->"}
-and Not = @{term "Not"};
+val conj = @{term HOL.conj}
+and disj = @{term HOL.disj}
+and imp = @{term implies}
+and Not = @{term Not};
fun mk_conj (t1, t2) = conj $ t1 $ t2
and mk_disj (t1, t2) = disj $ t1 $ t2
and mk_imp (t1, t2) = imp $ t1 $ t2
and mk_not t = Not $ t;
-fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
+fun dest_conj (Const ("HOL.conj", _) $ t $ t') = t :: dest_conj t'
| dest_conj t = [t];
-fun dest_disj (Const ("op |", _) $ t $ t') = t :: dest_disj t'
+fun dest_disj (Const ("HOL.disj", _) $ t $ t') = t :: dest_disj t'
| dest_disj t = [t];
(*Like dest_disj, but flattens disjunctions however nested*)
-fun disjuncts_aux (Const ("op |", _) $ t $ t') disjs = disjuncts_aux t (disjuncts_aux t' disjs)
+fun disjuncts_aux (Const ("HOL.disj", _) $ t $ t') disjs = disjuncts_aux t (disjuncts_aux t' disjs)
| disjuncts_aux t disjs = t::disjs;
fun disjuncts t = disjuncts_aux t [];
-fun dest_imp (Const ("op -->", _) $ A $ B) = (A, B)
+fun dest_imp (Const ("HOL.implies", _) $ A $ B) = (A, B)
| dest_imp t = raise TERM ("dest_imp", [t]);
fun dest_not (Const ("HOL.Not", _) $ t) = t
--- a/src/HOL/Tools/inductive_set.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/inductive_set.ML Fri Aug 27 12:57:55 2010 +0200
@@ -74,9 +74,9 @@
in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
(p (fold (Logic.all o Var) vs t) f)
end;
- fun mkop @{const_name "op &"} T x =
+ fun mkop @{const_name HOL.conj} T x =
SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x)
- | mkop @{const_name "op |"} T x =
+ | mkop @{const_name HOL.disj} T x =
SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x)
| mkop _ _ _ = NONE;
fun mk_collect p T t =
--- a/src/HOL/Tools/lin_arith.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML Fri Aug 27 12:57:55 2010 +0200
@@ -45,7 +45,7 @@
val mk_Trueprop = HOLogic.mk_Trueprop;
fun atomize thm = case Thm.prop_of thm of
- Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op &"}, _) $ _ $ _) =>
+ Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.conj}, _) $ _ $ _) =>
atomize (thm RS conjunct1) @ atomize (thm RS conjunct2)
| _ => [thm];
--- a/src/HOL/Tools/meson.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/meson.ML Fri Aug 27 12:57:55 2010 +0200
@@ -151,8 +151,8 @@
let fun has (Const(a,_)) = false
| has (Const(@{const_name Trueprop},_) $ p) = has p
| has (Const(@{const_name Not},_) $ p) = has p
- | has (Const(@{const_name "op |"},_) $ p $ q) = member (op =) bs @{const_name "op |"} orelse has p orelse has q
- | has (Const(@{const_name "op &"},_) $ p $ q) = member (op =) bs @{const_name "op &"} orelse has p orelse has q
+ | has (Const(@{const_name HOL.disj},_) $ p $ q) = member (op =) bs @{const_name HOL.disj} orelse has p orelse has q
+ | has (Const(@{const_name HOL.conj},_) $ p $ q) = member (op =) bs @{const_name HOL.conj} orelse has p orelse has q
| has (Const(@{const_name All},_) $ Abs(_,_,p)) = member (op =) bs @{const_name All} orelse has p
| has (Const(@{const_name Ex},_) $ Abs(_,_,p)) = member (op =) bs @{const_name Ex} orelse has p
| has _ = false
@@ -162,7 +162,7 @@
(**** Clause handling ****)
fun literals (Const(@{const_name Trueprop},_) $ P) = literals P
- | literals (Const(@{const_name "op |"},_) $ P $ Q) = literals P @ literals Q
+ | literals (Const(@{const_name HOL.disj},_) $ P $ Q) = literals P @ literals Q
| literals (Const(@{const_name Not},_) $ P) = [(false,P)]
| literals P = [(true,P)];
@@ -172,7 +172,7 @@
(*** Tautology Checking ***)
-fun signed_lits_aux (Const (@{const_name "op |"}, _) $ P $ Q) (poslits, neglits) =
+fun signed_lits_aux (Const (@{const_name HOL.disj}, _) $ P $ Q) (poslits, neglits) =
signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
| signed_lits_aux (Const(@{const_name Not},_) $ P) (poslits, neglits) = (poslits, P::neglits)
| signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
@@ -208,16 +208,16 @@
fun refl_clause_aux 0 th = th
| refl_clause_aux n th =
case HOLogic.dest_Trueprop (concl_of th) of
- (Const (@{const_name "op |"}, _) $ (Const (@{const_name "op |"}, _) $ _ $ _) $ _) =>
+ (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _) =>
refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*)
- | (Const (@{const_name "op |"}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ t $ u)) $ _) =>
+ | (Const (@{const_name HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ t $ u)) $ _) =>
if eliminable(t,u)
then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*)
else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*)
- | (Const (@{const_name "op |"}, _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
+ | (Const (@{const_name HOL.disj}, _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
| _ => (*not a disjunction*) th;
-fun notequal_lits_count (Const (@{const_name "op |"}, _) $ P $ Q) =
+fun notequal_lits_count (Const (@{const_name HOL.disj}, _) $ P $ Q) =
notequal_lits_count P + notequal_lits_count Q
| notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ _ $ _)) = 1
| notequal_lits_count _ = 0;
@@ -268,13 +268,13 @@
(*Estimate the number of clauses in order to detect infeasible theorems*)
fun signed_nclauses b (Const(@{const_name Trueprop},_) $ t) = signed_nclauses b t
| signed_nclauses b (Const(@{const_name Not},_) $ t) = signed_nclauses (not b) t
- | signed_nclauses b (Const(@{const_name "op &"},_) $ t $ u) =
+ | signed_nclauses b (Const(@{const_name HOL.conj},_) $ t $ u) =
if b then sum (signed_nclauses b t) (signed_nclauses b u)
else prod (signed_nclauses b t) (signed_nclauses b u)
- | signed_nclauses b (Const(@{const_name "op |"},_) $ t $ u) =
+ | signed_nclauses b (Const(@{const_name HOL.disj},_) $ t $ u) =
if b then prod (signed_nclauses b t) (signed_nclauses b u)
else sum (signed_nclauses b t) (signed_nclauses b u)
- | signed_nclauses b (Const(@{const_name "op -->"},_) $ t $ u) =
+ | signed_nclauses b (Const(@{const_name HOL.implies},_) $ t $ u) =
if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
else sum (signed_nclauses (not b) t) (signed_nclauses b u)
| signed_nclauses b (Const(@{const_name "op ="}, Type ("fun", [T, _])) $ t $ u) =
@@ -330,10 +330,10 @@
let val ctxtr = Unsynchronized.ref ctxt (* FIXME ??? *)
fun cnf_aux (th,ths) =
if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
- else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name "op &"}] (prop_of th))
+ else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name HOL.conj}] (prop_of th))
then nodups ctxt th :: ths (*no work to do, terminate*)
else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
- Const (@{const_name "op &"}, _) => (*conjunction*)
+ Const (@{const_name HOL.conj}, _) => (*conjunction*)
cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
| Const (@{const_name All}, _) => (*universal quantifier*)
let val (th',ctxt') = freeze_spec th (!ctxtr)
@@ -341,7 +341,7 @@
| Const (@{const_name Ex}, _) =>
(*existential quantifier: Insert Skolem functions*)
cnf_aux (apply_skolem_theorem (th, skolem_ths), ths)
- | Const (@{const_name "op |"}, _) =>
+ | Const (@{const_name HOL.disj}, _) =>
(*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
all combinations of converting P, Q to CNF.*)
let val tac =
@@ -365,7 +365,7 @@
(**** Generation of contrapositives ****)
fun is_left (Const (@{const_name Trueprop}, _) $
- (Const (@{const_name "op |"}, _) $ (Const (@{const_name "op |"}, _) $ _ $ _) $ _)) = true
+ (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _)) = true
| is_left _ = false;
(*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
@@ -400,8 +400,8 @@
(*Is the string the name of a connective? Really only | and Not can remain,
since this code expects to be called on a clause form.*)
val is_conn = member (op =)
- [@{const_name Trueprop}, @{const_name "op &"}, @{const_name "op |"},
- @{const_name "op -->"}, @{const_name Not},
+ [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj},
+ @{const_name HOL.implies}, @{const_name Not},
@{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}];
(*True if the term contains a function--not a logical connective--where the type
@@ -429,7 +429,7 @@
fun rigid t = not (is_Var (head_of t));
-fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name "op |"}, _) $ t $ _)) = rigid t
+fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name HOL.disj}, _) $ t $ _)) = rigid t
| ok4horn (Const (@{const_name Trueprop},_) $ t) = rigid t
| ok4horn _ = false;
--- a/src/HOL/Tools/prop_logic.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/prop_logic.ML Fri Aug 27 12:57:55 2010 +0200
@@ -397,14 +397,14 @@
(False, table)
| aux (Const (@{const_name Not}, _) $ x) table =
apfst Not (aux x table)
- | aux (Const (@{const_name "op |"}, _) $ x $ y) table =
+ | aux (Const (@{const_name HOL.disj}, _) $ x $ y) table =
let
val (fm1, table1) = aux x table
val (fm2, table2) = aux y table1
in
(Or (fm1, fm2), table2)
end
- | aux (Const (@{const_name "op &"}, _) $ x $ y) table =
+ | aux (Const (@{const_name HOL.conj}, _) $ x $ y) table =
let
val (fm1, table1) = aux x table
val (fm2, table2) = aux y table1
--- a/src/HOL/Tools/quickcheck_generators.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Fri Aug 27 12:57:55 2010 +0200
@@ -342,7 +342,7 @@
val bound_max = length Ts - 1;
val bounds = map_index (fn (i, ty) =>
(2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
- fun strip_imp (Const(@{const_name "op -->"},_) $ A $ B) = apfst (cons A) (strip_imp B)
+ fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
| strip_imp A = ([], A)
val prop' = betapplys (prop, map (fn (i, _, _, _) => Bound i) bounds);
val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds)
--- a/src/HOL/Tools/refute.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/refute.ML Fri Aug 27 12:57:55 2010 +0200
@@ -648,9 +648,9 @@
| Const (@{const_name All}, _) => t
| Const (@{const_name Ex}, _) => t
| Const (@{const_name "op ="}, _) => t
- | Const (@{const_name "op &"}, _) => t
- | Const (@{const_name "op |"}, _) => t
- | Const (@{const_name "op -->"}, _) => t
+ | Const (@{const_name HOL.conj}, _) => t
+ | Const (@{const_name HOL.disj}, _) => t
+ | Const (@{const_name HOL.implies}, _) => t
(* sets *)
| Const (@{const_name Collect}, _) => t
| Const (@{const_name Set.member}, _) => t
@@ -824,9 +824,9 @@
| Const (@{const_name All}, T) => collect_type_axioms T axs
| Const (@{const_name Ex}, T) => collect_type_axioms T axs
| Const (@{const_name "op ="}, T) => collect_type_axioms T axs
- | Const (@{const_name "op &"}, _) => axs
- | Const (@{const_name "op |"}, _) => axs
- | Const (@{const_name "op -->"}, _) => axs
+ | Const (@{const_name HOL.conj}, _) => axs
+ | Const (@{const_name HOL.disj}, _) => axs
+ | Const (@{const_name HOL.implies}, _) => axs
(* sets *)
| Const (@{const_name Collect}, T) => collect_type_axioms T axs
| Const (@{const_name Set.member}, T) => collect_type_axioms T axs
@@ -1861,7 +1861,7 @@
SOME (interpret thy model args (eta_expand t 1))
| Const (@{const_name "op ="}, _) =>
SOME (interpret thy model args (eta_expand t 2))
- | Const (@{const_name "op &"}, _) $ t1 $ t2 =>
+ | Const (@{const_name HOL.conj}, _) $ t1 $ t2 =>
(* 3-valued logic *)
let
val (i1, m1, a1) = interpret thy model args t1
@@ -1871,14 +1871,14 @@
in
SOME (Leaf [fmTrue, fmFalse], m2, a2)
end
- | Const (@{const_name "op &"}, _) $ t1 =>
+ | Const (@{const_name HOL.conj}, _) $ t1 =>
SOME (interpret thy model args (eta_expand t 1))
- | Const (@{const_name "op &"}, _) =>
+ | Const (@{const_name HOL.conj}, _) =>
SOME (interpret thy model args (eta_expand t 2))
(* this would make "undef" propagate, even for formulae like *)
(* "False & undef": *)
(* SOME (Node [Node [TT, FF], Node [FF, FF]], model, args) *)
- | Const (@{const_name "op |"}, _) $ t1 $ t2 =>
+ | Const (@{const_name HOL.disj}, _) $ t1 $ t2 =>
(* 3-valued logic *)
let
val (i1, m1, a1) = interpret thy model args t1
@@ -1888,14 +1888,14 @@
in
SOME (Leaf [fmTrue, fmFalse], m2, a2)
end
- | Const (@{const_name "op |"}, _) $ t1 =>
+ | Const (@{const_name HOL.disj}, _) $ t1 =>
SOME (interpret thy model args (eta_expand t 1))
- | Const (@{const_name "op |"}, _) =>
+ | Const (@{const_name HOL.disj}, _) =>
SOME (interpret thy model args (eta_expand t 2))
(* this would make "undef" propagate, even for formulae like *)
(* "True | undef": *)
(* SOME (Node [Node [TT, TT], Node [TT, FF]], model, args) *)
- | Const (@{const_name "op -->"}, _) $ t1 $ t2 => (* similar to "==>" (Pure) *)
+ | Const (@{const_name HOL.implies}, _) $ t1 $ t2 => (* similar to "==>" (Pure) *)
(* 3-valued logic *)
let
val (i1, m1, a1) = interpret thy model args t1
@@ -1905,9 +1905,9 @@
in
SOME (Leaf [fmTrue, fmFalse], m2, a2)
end
- | Const (@{const_name "op -->"}, _) $ t1 =>
+ | Const (@{const_name HOL.implies}, _) $ t1 =>
SOME (interpret thy model args (eta_expand t 1))
- | Const (@{const_name "op -->"}, _) =>
+ | Const (@{const_name HOL.implies}, _) =>
SOME (interpret thy model args (eta_expand t 2))
(* this would make "undef" propagate, even for formulae like *)
(* "False --> undef": *)
--- a/src/HOL/Tools/simpdata.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/Tools/simpdata.ML Fri Aug 27 12:57:55 2010 +0200
@@ -12,9 +12,9 @@
(*abstract syntax*)
fun dest_eq ((c as Const(@{const_name "op ="},_)) $ s $ t) = SOME (c, s, t)
| dest_eq _ = NONE;
- fun dest_conj ((c as Const(@{const_name "op &"},_)) $ s $ t) = SOME (c, s, t)
+ fun dest_conj ((c as Const(@{const_name HOL.conj},_)) $ s $ t) = SOME (c, s, t)
| dest_conj _ = NONE;
- fun dest_imp ((c as Const(@{const_name "op -->"},_)) $ s $ t) = SOME (c, s, t)
+ fun dest_imp ((c as Const(@{const_name HOL.implies},_)) $ s $ t) = SOME (c, s, t)
| dest_imp _ = NONE;
val conj = HOLogic.conj
val imp = HOLogic.imp
@@ -159,8 +159,8 @@
(Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())");
val mksimps_pairs =
- [(@{const_name "op -->"}, [@{thm mp}]),
- (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
+ [(@{const_name HOL.implies}, [@{thm mp}]),
+ (@{const_name HOL.conj}, [@{thm conjunct1}, @{thm conjunct2}]),
(@{const_name All}, [@{thm spec}]),
(@{const_name True}, []),
(@{const_name False}, []),
--- a/src/HOL/ex/Meson_Test.thy Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/ex/Meson_Test.thy Fri Aug 27 12:57:55 2010 +0200
@@ -10,7 +10,7 @@
below and constants declared in HOL!
*}
-hide_const (open) subset quotient union inter sum
+hide_const (open) implies union inter subset sum quotient
text {*
Test data for the MESON proof procedure
--- a/src/HOL/ex/Numeral.thy Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/ex/Numeral.thy Fri Aug 27 12:57:55 2010 +0200
@@ -1033,14 +1033,14 @@
(SML "IntInf.- ((_), 1)")
(OCaml "Big'_int.pred'_big'_int")
(Haskell "!(_/ -/ 1)")
- (Scala "!(_/ -/ 1)")
+ (Scala "!(_ -/ 1)")
(Eval "!(_/ -/ 1)")
code_const Int.succ
(SML "IntInf.+ ((_), 1)")
(OCaml "Big'_int.succ'_big'_int")
(Haskell "!(_/ +/ 1)")
- (Scala "!(_/ +/ 1)")
+ (Scala "!(_ +/ 1)")
(Eval "!(_/ +/ 1)")
code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
--- a/src/HOL/ex/SVC_Oracle.thy Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy Fri Aug 27 12:57:55 2010 +0200
@@ -88,9 +88,9 @@
else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
else replace (c $ x $ y) (*non-numeric comparison*)
(*abstraction of a formula*)
- and fm ((c as Const(@{const_name "op &"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
- | fm ((c as Const(@{const_name "op |"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
- | fm ((c as Const(@{const_name "op -->"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
+ and fm ((c as Const(@{const_name HOL.conj}, _)) $ p $ q) = c $ (fm p) $ (fm q)
+ | fm ((c as Const(@{const_name HOL.disj}, _)) $ p $ q) = c $ (fm p) $ (fm q)
+ | fm ((c as Const(@{const_name HOL.implies}, _)) $ p $ q) = c $ (fm p) $ (fm q)
| fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
| fm ((c as Const(@{const_name True}, _))) = c
| fm ((c as Const(@{const_name False}, _))) = c
--- a/src/HOL/ex/svc_funcs.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOL/ex/svc_funcs.ML Fri Aug 27 12:57:55 2010 +0200
@@ -89,9 +89,9 @@
let fun tag t =
let val (c,ts) = strip_comb t
in case c of
- Const(@{const_name "op &"}, _) => apply c (map tag ts)
- | Const(@{const_name "op |"}, _) => apply c (map tag ts)
- | Const(@{const_name "op -->"}, _) => apply c (map tag ts)
+ Const(@{const_name HOL.conj}, _) => apply c (map tag ts)
+ | Const(@{const_name HOL.disj}, _) => apply c (map tag ts)
+ | Const(@{const_name HOL.implies}, _) => apply c (map tag ts)
| Const(@{const_name Not}, _) => apply c (map tag ts)
| Const(@{const_name True}, _) => (c, false)
| Const(@{const_name False}, _) => (c, false)
@@ -183,11 +183,11 @@
| tm t = Int (lit t)
handle Match => var (t,[])
(*translation of a formula*)
- and fm pos (Const(@{const_name "op &"}, _) $ p $ q) =
+ and fm pos (Const(@{const_name HOL.conj}, _) $ p $ q) =
Buildin("AND", [fm pos p, fm pos q])
- | fm pos (Const(@{const_name "op |"}, _) $ p $ q) =
+ | fm pos (Const(@{const_name HOL.disj}, _) $ p $ q) =
Buildin("OR", [fm pos p, fm pos q])
- | fm pos (Const(@{const_name "op -->"}, _) $ p $ q) =
+ | fm pos (Const(@{const_name HOL.implies}, _) $ p $ q) =
Buildin("=>", [fm (not pos) p, fm pos q])
| fm pos (Const(@{const_name Not}, _) $ p) =
Buildin("NOT", [fm (not pos) p])
--- a/src/HOLCF/Tools/Domain/domain_library.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_library.ML Fri Aug 27 12:57:55 2010 +0200
@@ -121,7 +121,7 @@
val r_inst = read_instantiate ctxt;
fun at thm =
case concl_of thm of
- _$(Const(@{const_name "op &"},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
+ _$(Const(@{const_name HOL.conj},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
| _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
| _ => [thm];
in map zero_var_indexes (at thm) end;
--- a/src/Pure/Isar/locale.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/Pure/Isar/locale.ML Fri Aug 27 12:57:55 2010 +0200
@@ -483,7 +483,7 @@
val thy' = (change_locale loc o apsnd) (cons ((name, (morph, export)), serial ())) thy;
val context' = Context.Theory thy';
val (_, regs) = fold_rev (roundup thy' cons export)
- (all_registrations context') (get_idents (context'), []);
+ (registrations_of context' loc) (get_idents (context'), []);
in
thy'
|> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs
--- a/src/Tools/Code/code_haskell.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Fri Aug 27 12:57:55 2010 +0200
@@ -261,9 +261,8 @@
end;
in print_stmt end;
-fun haskell_program_of_program labelled_name module_name module_prefix reserved raw_module_alias program =
+fun haskell_program_of_program labelled_name module_prefix reserved module_alias program =
let
- val module_alias = if is_some module_name then K module_name else raw_module_alias;
val reserved = Name.make_context reserved;
val mk_name_module = mk_name_module reserved module_prefix module_alias program;
fun add_stmt (name, (stmt, deps)) =
@@ -314,15 +313,14 @@
handle Option => error ("Unknown statement name: " ^ labelled_name name);
in (deresolver, hs_program) end;
-fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
- raw_reserved includes raw_module_alias
- syntax_class syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
+fun serialize_haskell module_prefix module_name string_classes labelled_name
+ raw_reserved includes module_alias
+ syntax_class syntax_tyco syntax_const (code_of_pretty, code_writeln) program
+ (stmt_names, presentation_stmt_names) destination =
let
- val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
- val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
val reserved = fold (insert (op =) o fst) includes raw_reserved;
val (deresolver, hs_program) = haskell_program_of_program labelled_name
- module_name module_prefix reserved raw_module_alias program;
+ module_prefix reserved module_alias program;
val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
fun deriving_show tyco =
let
@@ -344,11 +342,9 @@
contr_classparam_typs
(if string_classes then deriving_show else K false);
fun print_module name content =
- (name, Pretty.chunks [
+ (name, Pretty.chunks2 [
str ("module " ^ name ^ " where {"),
- str "",
content,
- str "",
str "}"
]);
fun serialize_module1 (module_name', (deps, (stmts, _))) =
--- a/src/Tools/Code/code_ml.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Fri Aug 27 12:57:55 2010 +0200
@@ -489,7 +489,7 @@
|> intro_vars ((fold o Code_Thingol.fold_varnames)
(insert (op =)) ts []);
in concat [
- (Pretty.block o Pretty.commas)
+ (Pretty.block o commas)
(map (print_term is_pseudo_fun some_thm vars NOBR) ts),
str "->",
print_term is_pseudo_fun some_thm vars NOBR t
@@ -535,7 +535,7 @@
:: Pretty.brk 1
:: str "match"
:: Pretty.brk 1
- :: (Pretty.block o Pretty.commas) dummy_parms
+ :: (Pretty.block o commas) dummy_parms
:: Pretty.brk 1
:: str "with"
:: Pretty.brk 1
@@ -722,9 +722,8 @@
in
-fun ml_node_of_program labelled_name module_name reserved raw_module_alias program =
+fun ml_node_of_program labelled_name module_name reserved module_alias program =
let
- val module_alias = if is_some module_name then K module_name else raw_module_alias;
val reserved = Name.make_context reserved;
val empty_module = ((reserved, reserved), Graph.empty);
fun map_node [] f = f
@@ -813,7 +812,7 @@
) stmts
#>> (split_list #> apsnd (map_filter I
#> (fn [] => error ("Datatype block without data statement: "
- ^ (commas o map (labelled_name o fst)) stmts)
+ ^ (Library.commas o map (labelled_name o fst)) stmts)
| stmts => ML_Datas stmts)));
fun add_class stmts =
fold_map
@@ -828,7 +827,7 @@
) stmts
#>> (split_list #> apsnd (map_filter I
#> (fn [] => error ("Class block without class statement: "
- ^ (commas o map (labelled_name o fst)) stmts)
+ ^ (Library.commas o map (labelled_name o fst)) stmts)
| [stmt] => ML_Class stmt)));
fun add_stmts ([stmt as (name, Code_Thingol.Fun _)]) =
add_fun stmt
@@ -849,7 +848,7 @@
| add_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
add_funs stmts
| add_stmts stmts = error ("Illegal mutual dependencies: " ^
- (commas o map (labelled_name o fst)) stmts);
+ (Library.commas o map (labelled_name o fst)) stmts);
fun add_stmts' stmts nsp_nodes =
let
val names as (name :: names') = map fst stmts;
@@ -858,9 +857,9 @@
val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
handle Empty =>
error ("Different namespace prefixes for mutual dependencies:\n"
- ^ commas (map labelled_name names)
+ ^ Library.commas (map labelled_name names)
^ "\n"
- ^ commas module_names);
+ ^ Library.commas module_names);
val module_name_path = Long_Name.explode module_name;
fun add_dep name name' =
let
@@ -907,15 +906,14 @@
error ("Unknown statement name: " ^ labelled_name name);
in (deresolver, nodes) end;
-fun serialize_ml target print_module print_stmt raw_module_name with_signatures labelled_name
- reserved includes raw_module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
+fun serialize_ml target print_module print_stmt module_name with_signatures labelled_name
+ reserved includes module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program
+ (stmt_names, presentation_stmt_names) =
let
val is_cons = Code_Thingol.is_cons program;
- val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
val is_presentation = not (null presentation_stmt_names);
- val module_name = if is_presentation then SOME "Code" else raw_module_name;
val (deresolver, nodes) = ml_node_of_program labelled_name module_name
- reserved raw_module_alias program;
+ reserved module_alias program;
val reserved = make_vars reserved;
fun print_node prefix (Dummy _) =
NONE
@@ -939,7 +937,7 @@
in
Code_Target.mk_serialization target
(fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
- (rpair stmt_names' o code_of_pretty) p destination
+ (rpair stmt_names' o code_of_pretty) p
end;
end; (*local*)
@@ -948,8 +946,8 @@
(** for instrumentalization **)
fun evaluation_code_of thy target struct_name =
- Code_Target.serialize_custom thy (target, fn _ => fn [] =>
- serialize_ml target print_sml_module print_sml_stmt (SOME struct_name) true);
+ Code_Target.serialize_custom thy (target, fn module_name => fn [] =>
+ serialize_ml target print_sml_module print_sml_stmt module_name true) (SOME struct_name);
(** Isar setup **)
--- a/src/Tools/Code/code_printer.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Fri Aug 27 12:57:55 2010 +0200
@@ -19,6 +19,7 @@
val concat: Pretty.T list -> Pretty.T
val brackets: Pretty.T list -> Pretty.T
val enclose: string -> string -> Pretty.T list -> Pretty.T
+ val commas: Pretty.T list -> Pretty.T list
val enum: string -> string -> string -> Pretty.T list -> Pretty.T
val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
val semicolon: Pretty.T list -> Pretty.T
@@ -112,6 +113,7 @@
fun xs @| y = xs @ [y];
val str = Print_Mode.setmp [] Pretty.str;
val concat = Pretty.block o Pretty.breaks;
+val commas = Print_Mode.setmp [] Pretty.commas;
fun enclose l r = Print_Mode.setmp [] (Pretty.enclose l r);
val brackets = enclose "(" ")" o Pretty.breaks;
fun enum sep l r = Print_Mode.setmp [] (Pretty.enum sep l r);
--- a/src/Tools/Code/code_scala.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Fri Aug 27 12:57:55 2010 +0200
@@ -25,7 +25,7 @@
(** Scala serializer **)
fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved
- args_num is_singleton_constr deresolve =
+ args_num is_singleton_constr (deresolve, deresolve_full) =
let
val deresolve_base = Long_Name.base_name o deresolve;
fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
@@ -135,7 +135,7 @@
fun print_context tyvars vs name = applify "[" "]"
(fn (v, sort) => (Pretty.block o map str)
(lookup_tyvar tyvars v :: maps (fn sort => [": ", deresolve sort]) sort))
- NOBR ((str o deresolve) name) vs;
+ NOBR ((str o deresolve_base) name) vs;
fun print_defhead tyvars vars name vs params tys ty =
Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) =>
constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
@@ -194,7 +194,8 @@
str "match", str "{"], str "}")
(map print_clause eqs)
end;
- val print_method = (str o Library.enclose "`" "+`" o deresolve_base);
+ val print_method = str o Library.enclose "`" "`" o space_implode "+"
+ o Long_Name.explode o deresolve_full;
fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
print_def name (vs, ty) (filter (snd o snd) raw_eqs)
| print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
@@ -240,7 +241,7 @@
in
concat [str "def", constraint (Pretty.block [applify "(" ")"
(fn (aux, ty) => constraint ((str o lookup_var vars) aux)
- (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve classparam))
+ (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_base classparam))
(auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
add_typarg (deresolve name), str ")"]) (print_typ tyvars NOBR ty), str "=",
applify "(" ")" (str o lookup_var vars) NOBR
@@ -281,67 +282,137 @@
end;
in print_stmt end;
-fun scala_program_of_program labelled_name module_name reserved raw_module_alias program =
+local
+
+(* hierarchical module name space *)
+
+datatype node =
+ Dummy
+ | Stmt of Code_Thingol.stmt
+ | Module of ((Name.context * Name.context) * Name.context) * (string list * (string * node) Graph.T);
+
+in
+
+fun scala_program_of_program labelled_name reserved module_alias program =
let
- val the_module_name = the_default "Program" module_name;
- val module_alias = K (SOME the_module_name);
- val reserved = Name.make_context reserved;
- fun prepare_stmt (name, stmt) (nsps, stmts) =
+
+ (* building module name hierarchy *)
+ fun alias_fragments name = case module_alias name
+ of SOME name' => Long_Name.explode name'
+ | NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
+ (Long_Name.explode name);
+ val module_names = Graph.fold (insert (op =) o fst o dest_name o fst) program [];
+ val fragments_tab = fold (fn name => Symtab.update
+ (name, alias_fragments name)) module_names Symtab.empty;
+ val dest_name = Code_Printer.dest_name #>> (the o Symtab.lookup fragments_tab);
+
+ (* building empty module hierarchy *)
+ val empty_module = (((reserved, reserved), reserved), ([], Graph.empty));
+ fun map_module f (Module content) = Module (f content);
+ fun declare_module name_fragement ((nsp_class, nsp_object), nsp_common) =
let
- val (_, base) = Code_Printer.dest_name name;
- val mk_name_stmt = yield_singleton Name.variants;
- fun add_class ((nsp_class, nsp_object), nsp_common) =
- let
- val (base', nsp_class') = mk_name_stmt base nsp_class
- in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
- fun add_object ((nsp_class, nsp_object), nsp_common) =
- let
- val (base', nsp_object') = mk_name_stmt base nsp_object
- in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
- fun add_common upper ((nsp_class, nsp_object), nsp_common) =
+ val declare = Name.declare name_fragement;
+ in ((declare nsp_class, declare nsp_object), declare nsp_common) end;
+ fun ensure_module name_fragement (nsps, (implicits, nodes)) =
+ if can (Graph.get_node nodes) name_fragement then (nsps, (implicits, nodes))
+ else
+ (nsps |> declare_module name_fragement, (implicits,
+ nodes |> Graph.new_node (name_fragement, (name_fragement, Module empty_module))));
+ fun allocate_module [] = I
+ | allocate_module (name_fragment :: name_fragments) =
+ ensure_module name_fragment
+ #> (apsnd o apsnd o Graph.map_node name_fragment o apsnd o map_module o allocate_module) name_fragments;
+ val empty_program = Symtab.fold (fn (_, fragments) => allocate_module fragments)
+ fragments_tab empty_module;
+ fun change_module [] = I
+ | change_module (name_fragment :: name_fragments) =
+ apsnd o apsnd o Graph.map_node name_fragment o apsnd o map_module
+ o change_module name_fragments;
+
+ (* statement declaration *)
+ fun namify_class base ((nsp_class, nsp_object), nsp_common) =
+ let
+ val (base', nsp_class') = yield_singleton Name.variants base nsp_class
+ in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
+ fun namify_object base ((nsp_class, nsp_object), nsp_common) =
+ let
+ val (base', nsp_object') = yield_singleton Name.variants base nsp_object
+ in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
+ fun namify_common upper base ((nsp_class, nsp_object), nsp_common) =
+ let
+ val (base', nsp_common') =
+ yield_singleton Name.variants (if upper then first_upper base else base) nsp_common
+ in
+ (base',
+ ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
+ end;
+ fun declare_stmt name stmt =
+ let
+ val (name_fragments, base) = dest_name name;
+ val namify = case stmt
+ of Code_Thingol.Fun _ => namify_object
+ | Code_Thingol.Datatype _ => namify_class
+ | Code_Thingol.Datatypecons _ => namify_common true
+ | Code_Thingol.Class _ => namify_class
+ | Code_Thingol.Classrel _ => namify_object
+ | Code_Thingol.Classparam _ => namify_object
+ | Code_Thingol.Classinst _ => namify_common false;
+ val stmt' = case stmt
+ of Code_Thingol.Datatypecons _ => Dummy
+ | Code_Thingol.Classrel _ => Dummy
+ | Code_Thingol.Classparam _ => Dummy
+ | _ => Stmt stmt;
+ fun is_classinst stmt = case stmt
+ of Code_Thingol.Classinst _ => true
+ | _ => false;
+ val implicit_deps = filter (is_classinst o Graph.get_node program)
+ (Graph.imm_succs program name);
+ fun declaration (nsps, (implicits, nodes)) =
let
- val (base', nsp_common') =
- mk_name_stmt (if upper then first_upper base else base) nsp_common
- in
- (base',
- ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
- end;
- val add_name = case stmt
- of Code_Thingol.Fun _ => add_object
- | Code_Thingol.Datatype _ => add_class
- | Code_Thingol.Datatypecons _ => add_common true
- | Code_Thingol.Class _ => add_class
- | Code_Thingol.Classrel _ => add_object
- | Code_Thingol.Classparam _ => add_object
- | Code_Thingol.Classinst _ => add_common false;
- fun add_stmt base' = case stmt
- of Code_Thingol.Datatypecons _ => cons (name, (base', NONE))
- | Code_Thingol.Classrel _ => cons (name, (base', NONE))
- | Code_Thingol.Classparam _ => cons (name, (base', NONE))
- | _ => cons (name, (base', SOME stmt));
- in
- nsps
- |> add_name
- |-> (fn base' => rpair (add_stmt base' stmts))
- end;
- val stmts = AList.make (Graph.get_node program) (Graph.strong_conn program |> flat)
- |> filter_out (Code_Thingol.is_case o snd);
- val (_, sca_program) = fold prepare_stmt stmts (((reserved, reserved), reserved), []);
- fun deresolver name = (fst o the o AList.lookup (op =) sca_program) name
- handle Option => error ("Unknown statement name: " ^ labelled_name name);
- in (deresolver, (the_module_name, sca_program)) end;
+ val (base', nsps') = namify base nsps;
+ val implicits' = union (op =) implicit_deps implicits;
+ val nodes' = Graph.new_node (name, (base', stmt')) nodes;
+ in (nsps', (implicits', nodes')) end;
+ in change_module name_fragments declaration end;
+
+ (* dependencies *)
+ fun add_dependency name name' =
+ let
+ val (name_fragments, base) = dest_name name;
+ val (name_fragments', base') = dest_name name';
+ val (name_fragments_common, (diff, diff')) =
+ chop_prefix (op =) (name_fragments, name_fragments');
+ val dep = if null diff then (name, name') else (hd diff, hd diff')
+ in (change_module name_fragments_common o apsnd o apsnd) (Graph.add_edge dep) end;
+
+ (* producing program *)
+ val (_, (_, sca_program)) = empty_program
+ |> Graph.fold (fn (name, (stmt, _)) => declare_stmt name stmt) program
+ |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
-fun serialize_scala raw_module_name labelled_name
- raw_reserved includes raw_module_alias
+ (* deresolving *)
+ fun deresolve name =
+ let
+ val (name_fragments, _) = dest_name name;
+ val nodes = fold (fn name_fragement => fn nodes => case Graph.get_node nodes name_fragement
+ of (_, Module (_, (_, nodes))) => nodes) name_fragments sca_program;
+ val (base', _) = Graph.get_node nodes name;
+ in Long_Name.implode (name_fragments @ [base']) end
+ handle Graph.UNDEF _ => error ("Unknown statement name: " ^ labelled_name name);
+
+ in (deresolve, sca_program) end;
+
+fun serialize_scala labelled_name raw_reserved includes module_alias
_ syntax_tyco syntax_const (code_of_pretty, code_writeln)
- program stmt_names destination =
+ program (stmt_names, presentation_stmt_names) destination =
let
- val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
- val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
+
+ (* preprocess program *)
val reserved = fold (insert (op =) o fst) includes raw_reserved;
- val (deresolver, (the_module_name, sca_program)) = scala_program_of_program labelled_name
- module_name reserved raw_module_alias program;
- val reserved = make_vars reserved;
+ val (deresolve, sca_program) = scala_program_of_program labelled_name
+ (Name.make_context reserved) module_alias program;
+
+ (* print statements *)
fun lookup_constr tyco constr = case Graph.get_node program tyco
of Code_Thingol.Datatype (_, (_, constrs)) =>
the (AList.lookup (op = o apsnd fst) constrs constr);
@@ -359,44 +430,49 @@
of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
| _ => false;
val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
- reserved args_num is_singleton_constr deresolver;
- fun print_module name imports content =
- (name, Pretty.chunks (
- str ("object " ^ name ^ " {")
- :: (if null imports then []
- else str "" :: map (fn name => str ("import " ^ name ^ "._")) imports)
- @ [str "",
- content,
- str "",
- str "}"]
- ));
- fun serialize_module the_module_name sca_program =
+ (make_vars reserved) args_num is_singleton_constr
+ (deresolve, Long_Name.implode o fst o split_last o Long_Name.explode (*FIXME full*));
+
+ (* print nodes *)
+ fun print_implicit implicit =
let
- val content = Pretty.chunks2 (map_filter
- (fn (name, (_, SOME stmt)) => SOME (print_stmt (name, stmt))
- | (_, (_, NONE)) => NONE) sca_program);
- in print_module the_module_name (map fst includes) content end;
- fun check_destination destination =
- (File.check destination; destination);
- fun write_module destination (modlname, content) =
- let
- val filename = case modlname
- of "" => Path.explode "Main.scala"
- | _ => (Path.ext "scala" o Path.explode o implode o separate "/"
- o Long_Name.explode) modlname;
- val pathname = Path.append destination filename;
- val _ = File.mkdir_leaf (Path.dir pathname);
- in File.write pathname (code_of_pretty content) end
+ val s = deresolve implicit;
+ in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
+ fun print_implicits implicits = case map_filter print_implicit implicits
+ of [] => NONE
+ | ps => (SOME o Pretty.block)
+ (str "import /*implicits*/" :: Pretty.brk 1 :: commas ps);
+ fun print_module base implicits p = Pretty.chunks2
+ ([str ("object " ^ base ^ " {")] @ the_list (print_implicits implicits)
+ @ [p, str ("} /* object " ^ base ^ " */")]);
+ fun print_node (_, Dummy) = NONE
+ | print_node (name, Stmt stmt) = if null presentation_stmt_names
+ orelse member (op =) presentation_stmt_names name
+ then SOME (print_stmt (name, stmt))
+ else NONE
+ | print_node (name, Module (_, (implicits, nodes))) = if null presentation_stmt_names
+ then case print_nodes nodes
+ of NONE => NONE
+ | SOME p => SOME (print_module (Long_Name.base_name name) implicits p)
+ else print_nodes nodes
+ and print_nodes nodes = let
+ val ps = map_filter (fn name => print_node (name,
+ snd (Graph.get_node nodes name)))
+ ((rev o flat o Graph.strong_conn) nodes);
+ in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
+
+ (* serialization *)
+ val p_includes = if null presentation_stmt_names
+ then map (fn (base, p) => print_module base [] p) includes else [];
+ val p = Pretty.chunks2 (p_includes @ the_list (print_nodes sca_program));
in
Code_Target.mk_serialization target
- (fn NONE => K () o map (code_writeln o snd) | SOME file => K () o map
- (write_module (check_destination file)))
- (rpair [] o cat_lines o map (code_of_pretty o snd))
- (map (fn (name, content) => print_module name [] content) includes
- @| serialize_module the_module_name sca_program)
- destination
+ (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
+ (rpair [] o code_of_pretty) p destination
end;
+end; (*local*)
+
val literals = let
fun char_scala c = if c = "'" then "\\'"
else if c = "\"" then "\\\""
@@ -412,8 +488,8 @@
literal_char = Library.enclose "'" "'" o char_scala,
literal_string = quote o translate_string char_scala,
literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
- literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")",
- literal_alternative_numeral = fn k => "Natural(" ^ numeral_scala k ^ ")",
+ literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
+ literal_alternative_numeral = fn k => "Natural.Nat(" ^ numeral_scala k ^ ")",
literal_naive_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
infix_cons = (6, "::")
@@ -422,17 +498,17 @@
(** Isar setup **)
-fun isar_serializer module_name =
+fun isar_serializer _ =
Code_Target.parse_args (Scan.succeed ())
- #> (fn () => serialize_scala module_name);
+ #> (fn () => serialize_scala);
val setup =
Code_Target.add_target
(target, { serializer = isar_serializer, literals = literals,
- check = { env_var = "SCALA_HOME", make_destination = I,
+ check = { env_var = "SCALA_HOME", make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
make_command = fn scala_home => fn p => fn _ =>
"export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "
- ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " *.scala" } })
+ ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " " ^ File.shell_path p } })
#> Code_Target.add_syntax_tyco target "fun"
(SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
--- a/src/Tools/Code/code_target.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/Tools/Code/code_target.ML Fri Aug 27 12:57:55 2010 +0200
@@ -28,7 +28,7 @@
-> 'a -> serialization
val serialize: theory -> string -> int option -> string option -> Token.T list
-> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
- val serialize_custom: theory -> string * serializer
+ val serialize_custom: theory -> string * serializer -> string option
-> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
val the_literals: theory -> string -> literals
val export: serialization -> unit
@@ -111,7 +111,7 @@
-> (string -> Code_Printer.activated_const_syntax option)
-> ((Pretty.T -> string) * (Pretty.T -> unit))
-> Code_Thingol.program
- -> string list (*selected statements*)
+ -> (string list * string list) (*selected statements*)
-> serialization;
datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals,
@@ -254,7 +254,7 @@
|>> map_filter I;
fun invoke_serializer thy abortable serializer literals reserved abs_includes
- module_alias class instance tyco const module width args naming program2 names1 =
+ module_alias class instance tyco const module_name width args naming program2 (names1, presentation_names) =
let
val (names_class, class') =
activate_syntax (Code_Thingol.lookup_class naming) class;
@@ -275,14 +275,14 @@
val _ = if null empty_funs then () else error ("No code equations for "
^ commas (map (Sign.extern_const thy) empty_funs));
in
- serializer module args (Code_Thingol.labelled_name thy program2) reserved includes
- (Symtab.lookup module_alias) (Symtab.lookup class')
- (Symtab.lookup tyco') (Symtab.lookup const')
+ serializer module_name args (Code_Thingol.labelled_name thy program2) reserved includes
+ (if is_some module_name then K module_name else Symtab.lookup module_alias)
+ (Symtab.lookup class') (Symtab.lookup tyco') (Symtab.lookup const')
(Code_Printer.string_of_pretty width, Code_Printer.writeln_pretty width)
- program4 names1
+ program4 (names1, presentation_names)
end;
-fun mount_serializer thy alt_serializer target some_width module args naming program names =
+fun mount_serializer thy alt_serializer target some_width raw_module_name args naming program names destination =
let
val ((targets, abortable), default_width) = Targets.get thy;
fun collapse_hierarchy target =
@@ -299,6 +299,9 @@
val (modify, data) = collapse_hierarchy target;
val serializer = the_default (case the_description data
of Fundamental seri => #serializer seri) alt_serializer;
+ val presentation_names = stmt_names_of_destination destination;
+ val module_name = if null presentation_names
+ then raw_module_name else SOME "Code";
val reserved = the_reserved data;
fun select_include names_all (name, (content, cs)) =
if null cs then SOME (name, content)
@@ -308,13 +311,14 @@
then SOME (name, content) else NONE;
fun includes names_all = map_filter (select_include names_all)
((Symtab.dest o the_includes) data);
- val module_alias = the_module_alias data;
+ val module_alias = the_module_alias data
val { class, instance, tyco, const } = the_name_syntax data;
val literals = the_literals thy target;
val width = the_default default_width some_width;
in
invoke_serializer thy abortable serializer literals reserved
- includes module_alias class instance tyco const module width args naming (modify program) names
+ includes module_alias class instance tyco const module_name width args
+ naming (modify program) (names, presentation_names) destination
end;
in
@@ -344,8 +348,8 @@
else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
end;
-fun serialize_custom thy (target_name, seri) naming program names =
- mount_serializer thy (SOME seri) target_name NONE NONE [] naming program names (String [])
+fun serialize_custom thy (target_name, seri) module_name naming program names =
+ mount_serializer thy (SOME seri) target_name NONE module_name [] naming program names (String [])
|> the;
end; (* local *)
--- a/src/Tools/Code/code_thingol.ML Fri Aug 27 12:40:20 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML Fri Aug 27 12:57:55 2010 +0200
@@ -271,9 +271,6 @@
of SOME (tyco, _) => Codegen.thyname_of_type thy tyco
| NONE => Codegen.thyname_of_const thy c);
fun purify_base "==>" = "follows"
- | purify_base "op &" = "and"
- | purify_base "op |" = "or"
- | purify_base "op -->" = "implies"
| purify_base "op =" = "eq"
| purify_base s = Name.desymbolize false s;
fun namify thy get_basename get_thyname name =