# HG changeset patch # User wenzelm # Date 1282906675 -7200 # Node ID abe92b33ac9f656d2b289f1489f2e42aa1438a37 # Parent c421cfe2eadae8c2731cddd33d753fe06f26d007# Parent d8da44a8dd2562fb8587a8dbdbdc6b095c11886a merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML; diff -r d8da44a8dd25 -r abe92b33ac9f NEWS --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Auth/Yahalom.thy --- 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: diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Boogie/Tools/boogie_loader.ML --- 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) || diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Boogie/Tools/boogie_tactics.ML --- 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] diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Boogie/Tools/boogie_vcs.ML --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Decision_Procs/Approximation.thy --- 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 \ real \ bool"} $ t1 $ t2) = [t1, t2] | calculated_subterms (@{term "op < :: real \ real \ bool"} $ t1 $ t2) = [t1, t2] | calculated_subterms (@{term "op : :: real \ real set \ bool"} $ t1 $ diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Decision_Procs/Cooper.thy --- 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 \ bool \ 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"}] diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Decision_Procs/Ferrack.thy --- 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 \ :: bool \ bool \ 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) diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Decision_Procs/MIR.thy --- 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 \ bool \ 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') diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- 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)) diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Decision_Procs/ferrante_rackoff.ML --- 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) diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Decision_Procs/langford.ML --- 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) diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/HOL.thy --- 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 ("\ _" [40] 40) and - "op &" (infixr "\" 35) and - "op |" (infixr "\" 30) and - "op -->" (infixr "\" 25) and + HOL.conj (infixr "\" 35) and + HOL.disj (infixr "\" 30) and + HOL.implies (infixr "\" 25) and not_equal (infix "\" 50) notation (HTML output) Not ("\ _" [40] 40) and - "op &" (infixr "\" 35) and - "op |" (infixr "\" 30) and + HOL.conj (infixr "\" 35) and + HOL.disj (infixr "\" 30) and not_equal (infix "\" 50) abbreviation (iff) @@ -184,7 +184,7 @@ finalconsts "op =" - "op -->" + HOL.implies The definition If :: "bool \ 'a \ 'a \ '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 (_))") diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Imperative_HOL/Array.thy --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Imperative_HOL/Heap_Monad.thy --- 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((_))") diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Imperative_HOL/Ref.thy --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Import/Generate-HOL/GenHOL4Base.thy --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Import/Generate-HOLLight/GenHOLLight.thy --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Import/HOL/bool.imp --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Import/HOLLight/hollight.imp --- 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" diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Import/hol4rews.ML --- 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 = diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Import/proof_kernel.ML --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Library/Code_Integer.thy --- 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 + \ int \ int \ int" diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Library/Code_Natural.thy --- 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} diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Library/Efficient_Nat.thy --- 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 *} diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML --- 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 => _"}, diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Library/positivstellensatz.ML --- 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) diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Multivariate_Analysis/Gauge_Measure.thy --- 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 "(\ f) has_gmeasure (setsum m f)" using assms proof induct case (insert x s) have *:"(x \ \s) = \{x \ y| y. y\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) diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Mutabelle/Mutabelle.thy --- 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"), diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Mutabelle/mutabelle_extra.ML --- 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"), *) diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Nominal/nominal_datatype.ML --- 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)) diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Nominal/nominal_inductive.ML --- 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, diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Nominal/nominal_inductive2.ML --- 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, diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Orderings.thy --- 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}; diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy --- 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 \ B \ 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Prolog/prolog.ML --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Set.thy --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Statespace/state_fun.ML --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/TLA/Intensional.thy --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/Datatype/datatype_aux.ML --- 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)); diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/Datatype/datatype_prop.ML --- 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))) diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/Datatype/datatype_realizer.ML --- 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))); diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/Function/termination.ML --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/Nitpick/minipick.ML --- 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) diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/Nitpick/nitpick_mono.ML --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/Nitpick/nitpick_nut.ML --- 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) diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/Nitpick/nitpick_preproc.ML --- 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)) diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/Predicate_Compile/code_prolog.ML --- 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) diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- 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 []; diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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] diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- 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}, diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- 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); diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/Qelim/cooper.ML --- 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) diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/Qelim/qelim.ML --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/Quotient/quotient_term.ML --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/SMT/smtlib_interface.ML --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/SMT/z3_interface.ML --- 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) diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/SMT/z3_proof_literals.ML --- 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} diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/SMT/z3_proof_reconstruction.ML --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/SMT/z3_proof_tools.ML --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/Sledgehammer/clausifier.ML --- 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; diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/Sledgehammer/metis_clauses.ML --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/TFL/dcterm.ML --- 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} diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/TFL/usyntax.ML --- 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} = diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/cnf_funcs.ML --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/groebner.ML --- 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) diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/hologic.ML --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/inductive_set.ML --- 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 = diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/lin_arith.ML --- 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]; diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/meson.ML --- 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; diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/prop_logic.ML --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/quickcheck_generators.ML --- 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) diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/refute.ML --- 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": *) diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/Tools/simpdata.ML --- 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}, []), diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/ex/Meson_Test.thy --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/ex/Numeral.thy --- 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 + \ int \ int \ int" diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/ex/SVC_Oracle.thy --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/HOL/ex/svc_funcs.ML --- 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]) diff -r d8da44a8dd25 -r abe92b33ac9f src/HOLCF/Tools/Domain/domain_library.ML --- 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; diff -r d8da44a8dd25 -r abe92b33ac9f src/Pure/Isar/locale.ML --- 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 diff -r d8da44a8dd25 -r abe92b33ac9f src/Tools/Code/code_haskell.ML --- 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, _))) = diff -r d8da44a8dd25 -r abe92b33ac9f src/Tools/Code/code_ml.ML --- 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 **) diff -r d8da44a8dd25 -r abe92b33ac9f src/Tools/Code/code_printer.ML --- 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); diff -r d8da44a8dd25 -r abe92b33ac9f src/Tools/Code/code_scala.ML --- 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 ( diff -r d8da44a8dd25 -r abe92b33ac9f src/Tools/Code/code_target.ML --- 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 *) diff -r d8da44a8dd25 -r abe92b33ac9f src/Tools/Code/code_thingol.ML --- 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 =