--- a/NEWS Tue Jun 12 15:31:53 2012 +0200
+++ b/NEWS Tue Jun 12 15:32:14 2012 +0200
@@ -31,6 +31,10 @@
failures, enable the configuration option "z3_with_extensions".
Minor INCOMPATIBILITY.
+* Sledgehammer:
+
+ - Rationalized type encodings ("type_enc" option).
+
New in Isabelle2012 (May 2012)
------------------------------
--- a/doc-src/Sledgehammer/sledgehammer.tex Tue Jun 12 15:31:53 2012 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Jun 12 15:32:14 2012 +0200
@@ -1030,19 +1030,19 @@
\opdefault{type\_enc}{string}{smart}
Specifies the type encoding to use in ATP problems. Some of the type encodings
are unsound, meaning that they can give rise to spurious proofs
-(unreconstructible using \textit{metis}). The supported type encodings are
+(unreconstructible using \textit{metis}). The type encodings are
listed below, with an indication of their soundness in parentheses.
-An asterisk (*) means that the encoding is slightly incomplete for
+An asterisk (*) indicates that the encoding is slightly incomplete for
reconstruction with \textit{metis}, unless the \emph{strict} option (described
below) is enabled.
\begin{enum}
-\item[\labelitemi] \textbf{\textit{erased} (very unsound):} No type information is
+\item[\labelitemi] \textbf{\textit{erased} (unsound):} No type information is
supplied to the ATP, not even to resolve overloading. Types are simply erased.
\item[\labelitemi] \textbf{\textit{poly\_guards} (sound):} Types are encoded using
a predicate \const{g}$(\tau, t)$ that guards bound
-variables. Constants are annotated with their types, supplied as additional
+variables. Constants are annotated with their types, supplied as extra
arguments, to resolve overloading.
\item[\labelitemi] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is
@@ -1051,7 +1051,7 @@
\item[\labelitemi] \textbf{\textit{poly\_args} (unsound):}
Like for \textit{poly\_guards} constants are annotated with their types to
resolve overloading, but otherwise no type information is encoded. This
-coincides with the default encoding used by the \textit{metis} command.
+is the default encoding used by the \textit{metis} command.
\item[\labelitemi]
\textbf{%
@@ -1086,7 +1086,7 @@
monomorphized.
\item[\labelitemi] \textbf{\textit{poly\_native} (sound):} Exploits native
-polymorphic first-order types if the prover supports the TFF1 syntax; otherwise,
+first-order polymorphic types if the prover supports the TFF1 syntax; otherwise,
falls back on \textit{mono\_native}.
\item[\labelitemi]
@@ -1120,37 +1120,8 @@
\textit{metis} proof method, the `\hbox{@?}' suffix is replaced by
\hbox{``\textit{\_at\_query\/}''}.
-\item[\labelitemi]
-\textbf{%
-\textit{poly\_guards}!, \textit{poly\_tags}!, \textit{raw\_mono\_guards}!, \\
-\textit{raw\_mono\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \\
-\textit{mono\_native}!, \textit{mono\_native\_higher}! (mildly unsound):} \\
-The type encodings \textit{poly\_guards}, \textit{poly\_tags},
-\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
-\textit{mono\_tags}, \textit{mono\_native}, and \textit{mono\_native\_higher}
-also admit a mildly unsound (but very efficient) variant identified by an
-exclamation mark (`\hbox{!}') that detects and erases erases all types except
-those that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_native}
-and \textit{mono\_native\_higher}, the types are not actually erased but rather
-replaced by a shared uniform type of individuals.) As argument to the
-\textit{metis} proof method, the exclamation mark is replaced by the suffix
-\hbox{``\textit{\_bang\/}''}.
-
-\item[\labelitemi]
-\textbf{%
-\textit{poly\_guards}!!, \textit{poly\_tags}!!, \textit{raw\_mono\_guards}!!, \\
-\textit{raw\_mono\_tags}!!, \textit{mono\_guards}!!, \textit{mono\_tags}!! \\
-(mildly unsound):} \\
-Even lighter versions of the `\hbox{!}' encodings. As argument to the
-\textit{metis} proof method, the `\hbox{!!}' suffix is replaced by
-\hbox{``\textit{\_bang\_bang\/}''}.
-
-\item[\labelitemi]
-\textbf{%
-\textit{poly\_guards}@!, \textit{raw\_mono\_guards}@! (mildly unsound):} \\
-Alternative versions of the `\hbox{!!}' encodings. As argument to the
-\textit{metis} proof method, the `\hbox{@!}' suffix is replaced by
-\hbox{``\textit{\_at\_bang\/}''}.
+\item[\labelitemi] \textbf{\textit{poly\_args}?, \textit{raw\_mono\_args}? (unsound):} \\
+Lighter versions of \textit{poly\_args} and \textit{raw\_mono\_args}.
\item[\labelitemi] \textbf{\textit{smart}:} The actual encoding used depends on
the ATP and should be the most efficient sound encoding for that ATP.
--- a/src/HOL/HOL.thy Tue Jun 12 15:31:53 2012 +0200
+++ b/src/HOL/HOL.thy Tue Jun 12 15:32:14 2012 +0200
@@ -1903,7 +1903,7 @@
(SML "!(raise/ Fail/ \"undefined\")")
(OCaml "failwith/ \"undefined\"")
(Haskell "error/ \"undefined\"")
- (Scala "!error(\"undefined\")")
+ (Scala "!sys.error(\"undefined\")")
subsubsection {* Evaluation and normalization by evaluation *}
--- a/src/HOL/Imperative_HOL/Array.thy Tue Jun 12 15:31:53 2012 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy Tue Jun 12 15:32:14 2012 +0200
@@ -491,7 +491,7 @@
text {* Scala *}
code_type array (Scala "!collection.mutable.ArraySeq[_]")
-code_const Array (Scala "!error(\"bare Array\")")
+code_const Array (Scala "!sys.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((_))")
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jun 12 15:31:53 2012 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jun 12 15:32:14 2012 +0200
@@ -610,7 +610,7 @@
code_type Heap (Scala "Unit/ =>/ _")
code_const bind (Scala "Heap.bind")
code_const return (Scala "('_: Unit)/ =>/ _")
-code_const Heap_Monad.raise' (Scala "!error((_))")
+code_const Heap_Monad.raise' (Scala "!sys.error((_))")
subsubsection {* Target variants with less units *}
@@ -633,8 +633,12 @@
(*assumption: dummy values are not relevant for serialization*)
val (unitt, unitT) = case lookup_const naming @{const_name Unity}
of SOME unit' =>
- let val unitT = the (lookup_tyco naming @{type_name unit}) `%% []
- in (IConst (unit', ((([], []), ([], unitT)), false)), unitT) end
+ let
+ val unitT = the (lookup_tyco naming @{type_name unit}) `%% []
+ in
+ (IConst { name = unit', typargs = [], dicts = [], dom = [],
+ range = unitT, annotate = false }, unitT)
+ end
| NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants.");
fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
| dest_abs (t, ty) =
@@ -643,21 +647,21 @@
val v = singleton (Name.variant_list vs) "x";
val ty' = (hd o fst o unfold_fun) ty;
in ((SOME v, ty'), t `$ IVar (SOME v)) end;
- fun force (t as IConst (c, _) `$ t') = if is_return c
+ fun force (t as IConst { name = c, ... } `$ t') = if is_return c
then t' else t `$ unitt
| force t = t `$ unitt;
fun tr_bind'' [(t1, _), (t2, ty2)] =
let
val ((v, ty), t) = dest_abs (t2, ty2);
- in ICase (((force t1, ty), [(IVar v, tr_bind' t)]), dummy_case_term) end
+ in ICase { term = force t1, typ = ty, clauses = [(IVar v, tr_bind' t)], primitive = dummy_case_term } end
and tr_bind' t = case unfold_app t
- of (IConst (c, ((_, (ty1 :: ty2 :: _, _)), _)), [x1, x2]) => if is_bind c
+ of (IConst { name = c, dom = ty1 :: ty2 :: _, ... }, [x1, x2]) => if is_bind c
then tr_bind'' [(x1, ty1), (x2, ty2)]
else force t
| _ => force t;
- fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=> ICase (((IVar (SOME dummy_name), unitT),
- [(unitt, tr_bind'' ts)]), dummy_case_term)
- fun imp_monad_bind' (const as (c, ((_, (tys, _)), _))) ts = if is_bind c then case (ts, tys)
+ fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=>
+ ICase { term = IVar (SOME dummy_name), typ = unitT, clauses = [(unitt, tr_bind'' ts)], primitive = dummy_case_term }
+ fun imp_monad_bind' (const as { name = c, dom = dom, ... }) ts = if is_bind c then case (ts, dom)
of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
| ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
| (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))
@@ -668,10 +672,9 @@
of (IConst const, ts) => imp_monad_bind' const ts
| (t, ts) => imp_monad_bind t `$$ map imp_monad_bind ts)
| imp_monad_bind (v_ty `|=> t) = v_ty `|=> imp_monad_bind t
- | imp_monad_bind (ICase (((t, ty), pats), t0)) = ICase
- (((imp_monad_bind t, ty),
- (map o pairself) imp_monad_bind pats),
- imp_monad_bind t0);
+ | imp_monad_bind (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) =
+ ICase { term = imp_monad_bind t, typ = ty,
+ clauses = (map o pairself) imp_monad_bind clauses, primitive = imp_monad_bind t0 };
in (Graph.map o K o map_terms_stmt) imp_monad_bind end;
@@ -688,3 +691,4 @@
hide_const (open) Heap heap guard raise' fold_map
end
+
--- a/src/HOL/Imperative_HOL/Ref.thy Tue Jun 12 15:31:53 2012 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy Tue Jun 12 15:32:14 2012 +0200
@@ -313,7 +313,7 @@
text {* Scala *}
code_type ref (Scala "!Ref[_]")
-code_const Ref (Scala "!error(\"bare Ref\")")
+code_const Ref (Scala "!sys.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((_), (_))")
--- a/src/HOL/Library/Code_Integer.thy Tue Jun 12 15:31:53 2012 +0200
+++ b/src/HOL/Library/Code_Integer.thy Tue Jun 12 15:32:14 2012 +0200
@@ -111,7 +111,7 @@
(SML "!(raise/ Fail/ \"sub\")")
(OCaml "failwith/ \"sub\"")
(Haskell "error/ \"sub\"")
- (Scala "!error(\"sub\")")
+ (Scala "!sys.error(\"sub\")")
code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
(SML "IntInf.* ((_), (_))")
--- a/src/HOL/Library/Efficient_Nat.thy Tue Jun 12 15:31:53 2012 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Tue Jun 12 15:32:14 2012 +0200
@@ -228,7 +228,7 @@
(SML "!(raise/ Fail/ \"sub\")")
(OCaml "failwith/ \"sub\"")
(Haskell "error/ \"sub\"")
- (Scala "!error(\"sub\")")
+ (Scala "!sys.error(\"sub\")")
code_const "times \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
(SML "IntInf.*/ ((_),/ (_))")
@@ -269,7 +269,7 @@
(SML "!(raise/ Fail/ \"num'_of'_nat\")")
(OCaml "failwith/ \"num'_of'_nat\"")
(Haskell "error/ \"num'_of'_nat\"")
- (Scala "!error(\"num'_of'_nat\")")
+ (Scala "!sys.error(\"num'_of'_nat\")")
subsection {* Evaluation *}
--- a/src/HOL/Library/Target_Numeral.thy Tue Jun 12 15:31:53 2012 +0200
+++ b/src/HOL/Library/Target_Numeral.thy Tue Jun 12 15:32:14 2012 +0200
@@ -465,7 +465,7 @@
(SML "!(raise/ Fail/ \"sub\")")
(OCaml "failwith/ \"sub\"")
(Haskell "error/ \"sub\"")
- (Scala "!error(\"sub\")")
+ (Scala "!sys.error(\"sub\")")
code_const "times :: Target_Numeral.int \<Rightarrow> _ \<Rightarrow> _"
(SML "IntInf.* ((_), (_))")
@@ -661,30 +661,30 @@
by (simp add: Target_Numeral.int_eq_iff)
lemma [code abstract]:
- "Target_Numeral.of_nat (m + n) = Target_Numeral.of_nat m + Target_Numeral.of_nat n"
+ "Target_Numeral.of_nat (m + n) = of_nat m + of_nat n"
by (simp add: Target_Numeral.int_eq_iff)
lemma [code abstract]:
- "Target_Numeral.of_nat (Code_Nat.dup n) = Target_Numeral.dup (Target_Numeral.of_nat n)"
+ "Target_Numeral.of_nat (Code_Nat.dup n) = Target_Numeral.dup (of_nat n)"
by (simp add: Target_Numeral.int_eq_iff Code_Nat.dup_def)
lemma [code, code del]:
"Code_Nat.sub = Code_Nat.sub" ..
lemma [code abstract]:
- "Target_Numeral.of_nat (m - n) = max 0 (Target_Numeral.of_nat m - Target_Numeral.of_nat n)"
+ "Target_Numeral.of_nat (m - n) = max 0 (of_nat m - of_nat n)"
by (simp add: Target_Numeral.int_eq_iff)
lemma [code abstract]:
- "Target_Numeral.of_nat (m * n) = Target_Numeral.of_nat m * Target_Numeral.of_nat n"
+ "Target_Numeral.of_nat (m * n) = of_nat m * of_nat n"
by (simp add: Target_Numeral.int_eq_iff of_nat_mult)
lemma [code abstract]:
- "Target_Numeral.of_nat (m div n) = Target_Numeral.of_nat m div Target_Numeral.of_nat n"
+ "Target_Numeral.of_nat (m div n) = of_nat m div of_nat n"
by (simp add: Target_Numeral.int_eq_iff zdiv_int)
lemma [code abstract]:
- "Target_Numeral.of_nat (m mod n) = Target_Numeral.of_nat m mod Target_Numeral.of_nat n"
+ "Target_Numeral.of_nat (m mod n) = of_nat m mod of_nat n"
by (simp add: Target_Numeral.int_eq_iff zmod_int)
lemma [code]:
@@ -704,7 +704,7 @@
by (simp add: less_int_def)
lemma num_of_nat_code [code]:
- "num_of_nat = Target_Numeral.num_of_int \<circ> Target_Numeral.of_nat"
+ "num_of_nat = Target_Numeral.num_of_int \<circ> of_nat"
by (simp add: fun_eq_iff num_of_int_def of_nat_def)
lemma (in semiring_1) of_nat_code:
--- a/src/HOL/Metis_Examples/Type_Encodings.thy Tue Jun 12 15:31:53 2012 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy Tue Jun 12 15:32:14 2012 +0200
@@ -27,39 +27,27 @@
"poly_guards",
"poly_guards?",
"poly_guards??",
- (* "poly_guards@?", *)
- "poly_guards!",
- "poly_guards!!",
- (* "poly_guards@!", *)
+ "poly_guards@?",
"poly_tags",
"poly_tags?",
"poly_tags??",
- "poly_tags!",
- "poly_tags!!",
"poly_args",
+ "poly_args?",
"raw_mono_guards",
"raw_mono_guards?",
"raw_mono_guards??",
"raw_mono_guards@?",
- "raw_mono_guards!",
- "raw_mono_guards!!",
- "raw_mono_guards@!",
"raw_mono_tags",
"raw_mono_tags?",
"raw_mono_tags??",
- "raw_mono_tags!",
- "raw_mono_tags!!",
"raw_mono_args",
+ "raw_mono_args?",
"mono_guards",
"mono_guards?",
"mono_guards??",
- "mono_guards!",
- "mono_guards!!",
"mono_tags",
"mono_tags?",
"mono_tags??",
- "mono_tags!",
- "mono_tags!!",
"mono_args"]
fun metis_exhaust_tac ctxt ths =
@@ -85,8 +73,8 @@
lemma "x = y \<Longrightarrow> y = x"
by metis_exhaust
-lemma "[a] = [1 + 1] \<Longrightarrow> a = 1 + (1::int)"
-by (metis_exhaust last.simps)
+lemma "[a] = [Suc 0] \<Longrightarrow> a = 1"
+by (metis_exhaust last.simps One_nat_def)
lemma "map Suc [0] = [Suc 0]"
by (metis_exhaust map.simps)
@@ -102,7 +90,7 @@
lemma "P (null xs) \<Longrightarrow> null xs \<Longrightarrow> xs = []"
by (metis_exhaust null_def)
-lemma "(0::nat) + 0 = 0"
+lemma "(0\<Colon>nat) + 0 = 0"
by (metis_exhaust add_0_left)
end
--- a/src/HOL/TPTP/atp_problem_import.ML Tue Jun 12 15:31:53 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Tue Jun 12 15:32:14 2012 +0200
@@ -21,8 +21,8 @@
val freeze_problem_consts : theory -> term -> term
val make_conj : term list * term list -> term list -> term
val sledgehammer_tptp_file : theory -> int -> string -> unit
- val isabelle_demo_tptp_file : theory -> int -> string -> unit
- val isabelle_comp_tptp_file : theory -> int -> string -> unit
+ val isabelle_tptp_file : theory -> int -> string -> unit
+ val isabelle_hot_tptp_file : theory -> int -> string -> unit
val translate_tptp_file : string -> string -> string -> unit
end;
@@ -212,7 +212,7 @@
(prover ^
(if aggressivity > 0 then "(" ^ string_of_int aggressivity ^ ")"
else ""))
- (atp_tac ctxt aggressivity [] (timeout div frac) prover i)
+ (atp_tac ctxt aggressivity [] (mult * timeout div frac) prover i)
in
slice 2 0 ATP_Systems.spassN
ORELSE slice 2 0 ATP_Systems.vampireN
@@ -285,21 +285,23 @@
|> print_szs_from_success conjs
end
-fun isabelle_tptp_file demo thy timeout file_name =
+fun generic_isabelle_tptp_file demo thy timeout file_name =
let
val (conjs, assms, ctxt) =
read_tptp_file thy (freeze_problem_consts thy) file_name
val conj = make_conj assms conjs
- val last_hope = if demo then ATP_Systems.satallaxN else ATP_Systems.vampireN
+ val (last_hope_atp, last_hope_aggressive) =
+ if demo then (ATP_Systems.satallaxN, 0) else (ATP_Systems.vampireN, 2)
in
(can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) 1) conj orelse
- can_tac ctxt (atp_tac ctxt 2 [] timeout last_hope 1) conj)
+ can_tac ctxt (SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)")
+ (atp_tac ctxt last_hope_aggressive [] timeout last_hope_atp 1)) conj)
|> print_szs_from_success conjs
end
-val isabelle_demo_tptp_file = isabelle_tptp_file true
-val isabelle_comp_tptp_file = isabelle_tptp_file false
+val isabelle_tptp_file = generic_isabelle_tptp_file false
+val isabelle_hot_tptp_file = generic_isabelle_tptp_file true
(** Translator between TPTP(-like) file formats **)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle Tue Jun 12 15:32:14 2012 +0200
@@ -0,0 +1,33 @@
+#!/usr/bin/env bash
+#
+# Author: Jasmin Blanchette
+#
+# DESCRIPTION: Isabelle tactics for TPTP competitive division
+
+
+PRG="$(basename "$0")"
+
+function usage() {
+ echo
+ echo "Usage: isabelle $PRG TIMEOUT FILES"
+ echo
+ echo " Runs a combination of Isabelle tactics on TPTP problems."
+ echo " Each problem is allocated at most TIMEOUT seconds."
+ echo
+ exit 1
+}
+
+[ "$#" -eq 0 -o "$1" = "-?" ] && usage
+
+SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
+
+TIMEOUT=$1
+shift
+
+for FILE in "$@"
+do
+ echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
+ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
+ > /tmp/$SCRATCH.thy
+ "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
+done
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle_comp Tue Jun 12 15:31:53 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Jasmin Blanchette
-#
-# DESCRIPTION: Isabelle tactics for TPTP competitive division
-
-
-PRG="$(basename "$0")"
-
-function usage() {
- echo
- echo "Usage: isabelle $PRG TIMEOUT FILES"
- echo
- echo " Runs a combination of Isabelle tactics on TPTP problems."
- echo " Each problem is allocated at most TIMEOUT seconds."
- echo
- exit 1
-}
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
-
-TIMEOUT=$1
-shift
-
-for FILE in "$@"
-do
- echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
-ML {* ATP_Problem_Import.isabelle_comp_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
- > /tmp/$SCRATCH.thy
- "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
-done
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle_demo Tue Jun 12 15:31:53 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Jasmin Blanchette
-#
-# DESCRIPTION: Isabelle tactics for TPTP demo division
-
-
-PRG="$(basename "$0")"
-
-function usage() {
- echo
- echo "Usage: isabelle $PRG TIMEOUT FILES"
- echo
- echo " Runs a combination of Isabelle tactics on TPTP problems."
- echo " Each problem is allocated at most TIMEOUT seconds."
- echo
- exit 1
-}
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
-
-TIMEOUT=$1
-shift
-
-for FILE in "$@"
-do
- echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
-ML {* ATP_Problem_Import.isabelle_demo_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
- > /tmp/$SCRATCH.thy
- "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
-done
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot Tue Jun 12 15:32:14 2012 +0200
@@ -0,0 +1,33 @@
+#!/usr/bin/env bash
+#
+# Author: Jasmin Blanchette
+#
+# DESCRIPTION: Isabelle tactics for TPTP demo division
+
+
+PRG="$(basename "$0")"
+
+function usage() {
+ echo
+ echo "Usage: isabelle $PRG TIMEOUT FILES"
+ echo
+ echo " Runs a combination of Isabelle tactics on TPTP problems."
+ echo " Each problem is allocated at most TIMEOUT seconds."
+ echo
+ exit 1
+}
+
+[ "$#" -eq 0 -o "$1" = "-?" ] && usage
+
+SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
+
+TIMEOUT=$1
+shift
+
+for FILE in "$@"
+do
+ echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
+ML {* ATP_Problem_Import.isabelle_hot_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
+ > /tmp/$SCRATCH.thy
+ "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
+done
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 12 15:31:53 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 12 15:32:14 2012 +0200
@@ -24,12 +24,11 @@
datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
datatype strictness = Strict | Non_Strict
- datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
+ datatype granularity = All_Vars | Positively_Naked_Vars | Undercover_Vars
datatype type_level =
All_Types |
- Noninf_Nonmono_Types of strictness * granularity |
- Fin_Nonmono_Types of granularity |
- Const_Arg_Types |
+ Nonmono_Types of strictness * granularity |
+ Const_Types of bool (* "?" *) |
No_Types
type type_enc
@@ -89,8 +88,7 @@
val is_type_enc_higher_order : type_enc -> bool
val polymorphism_of_type_enc : type_enc -> polymorphism
val level_of_type_enc : type_enc -> type_level
- val is_type_enc_quasi_sound : type_enc -> bool
- val is_type_enc_fairly_sound : type_enc -> bool
+ val is_type_enc_sound : type_enc -> bool
val type_enc_from_string : strictness -> string -> type_enc
val adjust_type_enc : atp_format -> type_enc -> type_enc
val mk_aconns :
@@ -130,12 +128,11 @@
Higher_Order of thf_choice
datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
datatype strictness = Strict | Non_Strict
-datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
+datatype granularity = All_Vars | Positively_Naked_Vars | Undercover_Vars
datatype type_level =
All_Types |
- Noninf_Nonmono_Types of strictness * granularity |
- Fin_Nonmono_Types of granularity |
- Const_Arg_Types |
+ Nonmono_Types of strictness * granularity |
+ Const_Types of bool |
No_Types
datatype type_enc =
@@ -156,21 +153,15 @@
| level_of_type_enc (Guards (_, level)) = level
| level_of_type_enc (Tags (_, level)) = level
-fun granularity_of_type_level (Noninf_Nonmono_Types (_, grain)) = grain
- | granularity_of_type_level (Fin_Nonmono_Types grain) = grain
+fun granularity_of_type_level (Nonmono_Types (_, grain)) = grain
| granularity_of_type_level _ = All_Vars
-fun is_type_level_quasi_sound All_Types = true
- | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
- | is_type_level_quasi_sound _ = false
-val is_type_enc_quasi_sound = is_type_level_quasi_sound o level_of_type_enc
+fun is_type_level_sound All_Types = true
+ | is_type_level_sound (Nonmono_Types _) = true
+ | is_type_level_sound _ = false
+val is_type_enc_sound = is_type_level_sound o level_of_type_enc
-fun is_type_level_fairly_sound (Fin_Nonmono_Types _) = true
- | is_type_level_fairly_sound level = is_type_level_quasi_sound level
-val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
-
-fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true
- | is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true
+fun is_type_level_monotonicity_based (Nonmono_Types _) = true
| is_type_level_monotonicity_based _ = false
val no_lamsN = "no_lams" (* used internally; undocumented *)
@@ -183,8 +174,8 @@
val lam_liftingN = "lam_lifting" (* legacy *)
(* It's still unclear whether all TFF1 implementations will support type
- signatures such as "!>[A : $tType] : $o", with ghost type variables. *)
-val avoid_first_order_ghost_type_vars = false
+ signatures such as "!>[A : $tType] : $o", with phantom type variables. *)
+val avoid_first_order_phantom_type_vars = false
val bound_var_prefix = "B_"
val all_bound_var_prefix = "A_"
@@ -607,26 +598,13 @@
iterm_from_term thy type_enc ((s, (name, T)) :: bs) t
in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end
-(* "_query", "_bang", and "_at" are for the ASCII-challenged Metis and
- Mirabelle. *)
+(* "_query" and "_at" are for the ASCII-challenged Metis and Mirabelle. *)
val queries = ["?", "_query"]
-val bangs = ["!", "_bang"]
val ats = ["@", "_at"]
fun try_unsuffixes ss s =
fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
-fun try_nonmono constr suffixes fallback s =
- case try_unsuffixes suffixes s of
- SOME s =>
- (case try_unsuffixes suffixes s of
- SOME s => (constr Positively_Naked_Vars, s)
- | NONE =>
- case try_unsuffixes ats s of
- SOME s => (constr Ghost_Type_Arg_Vars, s)
- | NONE => (constr All_Vars, s))
- | NONE => fallback s
-
fun type_enc_from_string strictness s =
(case try (unprefix "poly_") s of
SOME s => (SOME Polymorphic, s)
@@ -637,9 +615,16 @@
case try (unprefix "mono_") s of
SOME s => (SOME Mangled_Monomorphic, s)
| NONE => (NONE, s))
- ||> (pair All_Types
- |> try_nonmono Fin_Nonmono_Types bangs
- |> try_nonmono (curry Noninf_Nonmono_Types strictness) queries)
+ ||> (fn s =>
+ case try_unsuffixes queries s of
+ SOME s =>
+ (case try_unsuffixes queries s of
+ SOME s => (Nonmono_Types (strictness, Positively_Naked_Vars), s)
+ | NONE =>
+ case try_unsuffixes ats s of
+ SOME s => (Nonmono_Types (strictness, Undercover_Vars), s)
+ | NONE => (Nonmono_Types (strictness, All_Vars), s))
+ | NONE => (All_Types, s))
|> (fn (poly, (level, core)) =>
case (core, (poly, level)) of
("native", (SOME poly, _)) =>
@@ -656,7 +641,7 @@
(case (poly, level) of
(Polymorphic, All_Types) =>
Native (Higher_Order THF_With_Choice, Polymorphic, All_Types)
- | (_, Noninf_Nonmono_Types _) => raise Same.SAME
+ | (_, Nonmono_Types _) => raise Same.SAME
| (Mangled_Monomorphic, _) =>
if granularity_of_type_level level = All_Vars then
Native (Higher_Order THF_With_Choice, Mangled_Monomorphic,
@@ -666,17 +651,20 @@
| _ => raise Same.SAME)
| ("guards", (SOME poly, _)) =>
if poly = Mangled_Monomorphic andalso
- granularity_of_type_level level = Ghost_Type_Arg_Vars then
+ granularity_of_type_level level = Undercover_Vars then
raise Same.SAME
else
Guards (poly, level)
| ("tags", (SOME poly, _)) =>
- if granularity_of_type_level level = Ghost_Type_Arg_Vars then
+ if granularity_of_type_level level = Undercover_Vars then
raise Same.SAME
else
Tags (poly, level)
| ("args", (SOME poly, All_Types (* naja *))) =>
- Guards (poly, Const_Arg_Types)
+ Guards (poly, Const_Types false)
+ | ("args", (SOME poly, Nonmono_Types (_, All_Vars) (* naja *))) =>
+ if poly = Mangled_Monomorphic then raise Same.SAME
+ else Guards (poly, Const_Types true)
| ("erased", (NONE, All_Types (* naja *))) =>
Guards (Polymorphic, No_Types)
| _ => raise Same.SAME)
@@ -701,7 +689,7 @@
| adjust_type_enc format (Native (_, poly, level)) =
adjust_type_enc format (Guards (poly, level))
| adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
- (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
+ (if is_type_enc_sound type_enc then Tags else Guards) stuff
| adjust_type_enc _ type_enc = type_enc
fun is_fol_term t =
@@ -840,32 +828,33 @@
(* The Booleans indicate whether all type arguments should be kept. *)
datatype type_arg_policy =
- Explicit_Type_Args of bool (* infer_from_term_args *) |
Mangled_Type_Args |
+ All_Type_Args |
+ Noninferable_Type_Args |
+ Constr_Type_Args |
No_Type_Args
-fun type_arg_policy monom_constrs type_enc s =
+fun type_arg_policy constrs type_enc s =
let val poly = polymorphism_of_type_enc type_enc in
if s = type_tag_name then
- if poly = Mangled_Monomorphic then Mangled_Type_Args
- else Explicit_Type_Args false
+ if poly = Mangled_Monomorphic then Mangled_Type_Args else All_Type_Args
else case type_enc of
- Native (_, Polymorphic, _) => Explicit_Type_Args false
+ Native (_, Polymorphic, _) => All_Type_Args
| Tags (_, All_Types) => No_Type_Args
| _ =>
let val level = level_of_type_enc type_enc in
if level = No_Types orelse s = @{const_name HOL.eq} orelse
- (s = app_op_name andalso level = Const_Arg_Types) then
+ (case level of Const_Types _ => s = app_op_name | _ => false) then
No_Type_Args
else if poly = Mangled_Monomorphic then
Mangled_Type_Args
- else if member (op =) monom_constrs s andalso
- granularity_of_type_level level = Positively_Naked_Vars then
- No_Type_Args
+ else if level = All_Types orelse
+ granularity_of_type_level level = Undercover_Vars then
+ Noninferable_Type_Args
+ else if member (op =) constrs s andalso level <> Const_Types false then
+ Constr_Type_Args
else
- Explicit_Type_Args
- (level = All_Types orelse
- granularity_of_type_level level = Ghost_Type_Arg_Vars)
+ All_Type_Args
end
end
@@ -889,7 +878,7 @@
AAtom (ATerm (class, arg ::
(case type_enc of
Native (First_Order, Polymorphic, _) =>
- if avoid_first_order_ghost_type_vars then [ATerm (TYPE_name, [arg])]
+ if avoid_first_order_phantom_type_vars then [ATerm (TYPE_name, [arg])]
else []
| _ => [])))
fun formulas_for_types type_enc add_sorts_on_typ Ts =
@@ -1131,42 +1120,38 @@
chop_fun (n - 1) ran_T |>> cons dom_T
| chop_fun _ T = ([], T)
-fun filter_const_type_args _ _ _ [] = []
- | filter_const_type_args thy s ary T_args =
+fun infer_type_args _ _ _ _ [] = []
+ | infer_type_args maybe_not thy s binders_of T_args =
let
val U = robust_const_type thy s
- val arg_U_vars = fold Term.add_tvarsT (U |> chop_fun ary |> fst) []
+ val arg_U_vars = fold Term.add_tvarsT (binders_of U) []
+ fun filt (U, T) =
+ if maybe_not (member (op =) arg_U_vars (dest_TVar U)) then dummyT else T
val U_args = (s, U) |> robust_const_typargs thy
- in
- U_args ~~ T_args
- |> map (fn (U, T) =>
- if member (op =) arg_U_vars (dest_TVar U) then dummyT else T)
- end
+ in map filt (U_args ~~ T_args) end
handle TYPE _ => T_args
fun filter_type_args_in_const _ _ _ _ _ [] = []
- | filter_type_args_in_const thy monom_constrs type_enc ary s T_args =
+ | filter_type_args_in_const thy constrs type_enc ary s T_args =
case unprefix_and_unascii const_prefix s of
NONE =>
if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then []
else T_args
| SOME s'' =>
- let
- val s'' = invert_const s''
- fun filter_T_args false = T_args
- | filter_T_args true = filter_const_type_args thy s'' ary T_args
- in
- case type_arg_policy monom_constrs type_enc s'' of
- Explicit_Type_Args infer_from_term_args =>
- filter_T_args infer_from_term_args
+ let val s'' = invert_const s'' in
+ case type_arg_policy constrs type_enc s'' of
+ Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol"
+ | All_Type_Args => T_args
+ | Noninferable_Type_Args =>
+ infer_type_args I thy s'' (fst o chop_fun ary) T_args
+ | Constr_Type_Args => infer_type_args not thy s'' binder_types T_args
| No_Type_Args => []
- | Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol"
end
-fun filter_type_args_in_iterm thy monom_constrs type_enc =
+fun filter_type_args_in_iterm thy constrs type_enc =
let
fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
| filt ary (IConst (name as (s, _), T, T_args)) =
- filter_type_args_in_const thy monom_constrs type_enc ary s T_args
+ filter_type_args_in_const thy constrs type_enc ary s T_args
|> (fn T_args => IConst (name, T, T_args))
| filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm)
| filt _ tm = tm
@@ -1302,17 +1287,16 @@
end
fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
- | s_not_prop _ = @{prop True} (* "t" is too meta for "metis" *)
-(*
| s_not_prop (@{const "==>"} $ t $ @{prop False}) = t
| s_not_prop t = @{const "==>"} $ t $ @{prop False}
-*)
fun make_conjecture ctxt format type_enc =
map (fn ((name, stature), (role, t)) =>
let
+ (* FIXME: The commented-out code is a hack to get decent performance
+ out of LEO-II on the TPTP THF benchmarks. *)
val role =
- if is_format_with_defs format andalso
+ if (* is_format_with_defs format andalso *)
role <> Conjecture andalso is_legitimate_tptp_def t then
Definition
else
@@ -1332,16 +1316,16 @@
| NONE => [])
handle TYPE _ => []
-fun ghost_type_args thy s ary =
+fun type_arg_cover thy s ary =
if is_tptp_equal s then
0 upto ary - 1
else
let
val footprint = tvar_footprint thy s ary
val eq = (s = @{const_name HOL.eq})
- fun ghosts _ [] = []
- | ghosts seen ((i, tvars) :: args) =
- ghosts (union (op =) seen tvars) args
+ fun cover _ [] = []
+ | cover seen ((i, tvars) :: args) =
+ cover (union (op =) seen tvars) args
|> (eq orelse exists (fn tvar => not (member (op =) seen tvar)) tvars)
? cons i
in
@@ -1350,7 +1334,7 @@
else
0 upto length footprint - 1 ~~ footprint
|> sort (rev_order o list_ord Term_Ord.indexname_ord o pairself snd)
- |> ghosts []
+ |> cover []
end
type monotonicity_info =
@@ -1376,25 +1360,15 @@
fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true
| should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
maybe_nonmono_Ts, ...}
- (Noninf_Nonmono_Types (strictness, grain)) T =
+ (Nonmono_Types (strictness, grain)) T =
let val thy = Proof_Context.theory_of ctxt in
- grain = Ghost_Type_Arg_Vars orelse
+ grain = Undercover_Vars orelse
(exists (type_intersect thy T) maybe_nonmono_Ts andalso
not (exists (type_instance thy T) surely_infinite_Ts orelse
(not (member (type_equiv thy) maybe_finite_Ts T) andalso
is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts
T)))
end
- | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
- maybe_nonmono_Ts, ...}
- (Fin_Nonmono_Types grain) T =
- let val thy = Proof_Context.theory_of ctxt in
- grain = Ghost_Type_Arg_Vars orelse
- (exists (type_intersect thy T) maybe_nonmono_Ts andalso
- (exists (type_generalization thy T) surely_finite_Ts orelse
- (not (member (type_equiv thy) maybe_infinite_Ts T) andalso
- is_type_surely_finite ctxt T)))
- end
| should_encode_type _ _ _ _ = false
fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
@@ -1624,7 +1598,7 @@
|> mangle_type_args_in_iterm type_enc
in list_app app [head, arg] end
-fun firstorderize_fact thy monom_constrs type_enc sym_tab uncurried_aliases
+fun firstorderize_fact thy constrs type_enc sym_tab uncurried_aliases
aggressive =
let
fun do_app arg head = mk_app_op type_enc head arg
@@ -1652,7 +1626,7 @@
val do_iterm =
not (is_type_enc_higher_order type_enc)
? (introduce_app_ops #> introduce_predicators)
- #> filter_type_args_in_iterm thy monom_constrs type_enc
+ #> filter_type_args_in_iterm thy constrs type_enc
in update_iformula (formula_map do_iterm) end
(** Helper facts **)
@@ -1771,11 +1745,10 @@
let
val thy = Proof_Context.theory_of ctxt
val unmangled_s = mangled_s |> unmangled_const_name |> hd
- fun dub needs_fairly_sound j k =
+ fun dub needs_sound j k =
ascii_of unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^
(if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
- (if needs_fairly_sound then typed_helper_suffix
- else untyped_helper_suffix)
+ (if needs_sound then typed_helper_suffix else untyped_helper_suffix)
fun specialize_helper t T =
if unmangled_s = app_op_name then
let
@@ -1784,27 +1757,25 @@
in monomorphic_term tyenv t end
else
specialize_type thy (invert_const unmangled_s, T) t
- fun dub_and_inst needs_fairly_sound ((status, t), j) =
+ fun dub_and_inst needs_sound ((status, t), j) =
(if should_specialize_helper type_enc t then
map_filter (try (specialize_helper t)) types
else
[t])
|> tag_list 1
- |> map (fn (k, t) =>
- ((dub needs_fairly_sound j k, (Global, status)), t))
+ |> map (fn (k, t) => ((dub needs_sound j k, (Global, status)), t))
val make_facts = map_filter (make_fact ctxt format type_enc false)
- val fairly_sound = is_type_enc_fairly_sound type_enc
+ val sound = is_type_enc_sound type_enc
val could_specialize = could_specialize_helpers type_enc
in
- fold (fn ((helper_s, needs_fairly_sound), ths) =>
- if (needs_fairly_sound andalso not fairly_sound) orelse
+ fold (fn ((helper_s, needs_sound), ths) =>
+ if (needs_sound andalso not sound) orelse
(helper_s <> unmangled_s andalso
(not aggressive orelse could_specialize)) then
I
else
ths ~~ (1 upto length ths)
- |> maps (dub_and_inst needs_fairly_sound
- o apfst (apsnd prop_of))
+ |> maps (dub_and_inst needs_sound o apfst (apsnd prop_of))
|> make_facts
|> union (op = o pairself #iformula))
(if aggressive then aggressive_helper_table else helper_table)
@@ -1901,9 +1872,8 @@
fact :: reorder [] skipped (* break cycle *)
| reorder skipped (fact :: facts) =
let val rhs_consts = consts_of_hs snd fact in
- if exists (exists (member (op =) rhs_consts o the_single
- o consts_of_hs fst))
- [skipped, facts] then
+ if exists (exists (exists (member (op =) rhs_consts)
+ o consts_of_hs fst)) [skipped, facts] then
reorder (fact :: skipped) facts
else
fact :: reorder [] (facts @ skipped)
@@ -1972,41 +1942,34 @@
accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
| is_var_positively_naked_in_term _ _ _ _ = true
-fun is_var_ghost_type_arg_in_term thy polym_constrs name pos tm accum =
+fun is_var_positively_naked_or_undercover_in_term thy name pos tm accum =
is_var_positively_naked_in_term name pos tm accum orelse
let
val var = ATerm (name, [])
- fun is_nasty_in_term (ATerm (_, [])) = false
- | is_nasty_in_term (ATerm ((s, _), tms)) =
+ fun is_undercover (ATerm (_, [])) = false
+ | is_undercover (ATerm ((s, _), tms)) =
let
val ary = length tms
- val polym_constr = member (op =) polym_constrs s
- val ghosts = ghost_type_args thy s ary
+ val cover = type_arg_cover thy s ary
in
- exists (fn (j, tm) =>
- if polym_constr then
- member (op =) ghosts j andalso
- (tm = var orelse is_nasty_in_term tm)
- else
- tm = var andalso member (op =) ghosts j)
- (0 upto ary - 1 ~~ tms)
- orelse (not polym_constr andalso exists is_nasty_in_term tms)
+ exists (fn (j, tm) => tm = var andalso member (op =) cover j)
+ (0 upto ary - 1 ~~ tms) orelse
+ exists is_undercover tms
end
- | is_nasty_in_term _ = true
- in is_nasty_in_term tm end
+ | is_undercover _ = true
+ in is_undercover tm end
-fun should_guard_var_in_formula thy polym_constrs level pos phi (SOME true)
- name =
+fun should_guard_var_in_formula thy level pos phi (SOME true) name =
(case granularity_of_type_level level of
All_Vars => true
| Positively_Naked_Vars =>
formula_fold pos (is_var_positively_naked_in_term name) phi false
- | Ghost_Type_Arg_Vars =>
- formula_fold pos (is_var_ghost_type_arg_in_term thy polym_constrs name) phi
- false)
- | should_guard_var_in_formula _ _ _ _ _ _ _ = true
+ | Undercover_Vars =>
+ formula_fold pos (is_var_positively_naked_or_undercover_in_term thy name)
+ phi false)
+ | should_guard_var_in_formula _ _ _ _ _ _ = true
-fun always_guard_var_in_formula _ _ _ _ _ _ _ = true
+fun always_guard_var_in_formula _ _ _ _ _ _ = true
fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
| should_generate_tag_bound_decl ctxt mono (Tags (_, level)) _ T =
@@ -2062,15 +2025,14 @@
t
end
in term (Top_Level pos) end
-and formula_from_iformula ctxt polym_constrs mono type_enc should_guard_var =
+and formula_from_iformula ctxt mono type_enc should_guard_var =
let
val thy = Proof_Context.theory_of ctxt
val level = level_of_type_enc type_enc
val do_term = ho_term_from_iterm ctxt mono type_enc
fun do_out_of_bound_type pos phi universal (name, T) =
if should_guard_type ctxt mono type_enc
- (fn () => should_guard_var thy polym_constrs level pos phi
- universal name) T then
+ (fn () => should_guard_var thy level pos phi universal name) T then
IVar (name, T)
|> type_guard_iterm type_enc T
|> do_term pos |> AAtom |> SOME
@@ -2104,12 +2066,12 @@
(* Each fact is given a unique fact number to avoid name clashes (e.g., because
of monomorphization). The TPTP explicitly forbids name clashes, and some of
the remote provers might care. *)
-fun formula_line_for_fact ctxt polym_constrs prefix encode freshen pos
- mono type_enc rank (j, {name, stature, role, iformula, atomic_types}) =
+fun formula_line_for_fact ctxt prefix encode freshen pos mono type_enc rank
+ (j, {name, stature, role, iformula, atomic_types}) =
(prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, role,
iformula
- |> formula_from_iformula ctxt polym_constrs mono type_enc
- should_guard_var_in_formula (if pos then SOME true else NONE)
+ |> formula_from_iformula ctxt mono type_enc should_guard_var_in_formula
+ (if pos then SOME true else NONE)
|> close_formula_universally
|> bound_tvars type_enc true atomic_types,
NONE,
@@ -2149,11 +2111,11 @@
(map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)),
NONE, isabelle_info inductiveN helper_rank)
-fun formula_line_for_conjecture ctxt polym_constrs mono type_enc
+fun formula_line_for_conjecture ctxt mono type_enc
({name, role, iformula, atomic_types, ...} : ifact) =
Formula (conjecture_prefix ^ name, role,
iformula
- |> formula_from_iformula ctxt polym_constrs mono type_enc
+ |> formula_from_iformula ctxt mono type_enc
should_guard_var_in_formula (SOME false)
|> close_formula_universally
|> bound_tvars type_enc true atomic_types, NONE, [])
@@ -2181,7 +2143,7 @@
Decl (sym_decl_prefix ^ s, name,
if order = First_Order then
ATyAbs ([tvar_a_name],
- if avoid_first_order_ghost_type_vars then
+ if avoid_first_order_phantom_type_vars then
AFun (a_itself_atype, bool_atype)
else
bool_atype)
@@ -2252,12 +2214,12 @@
end
in
Symtab.empty
- |> is_type_enc_fairly_sound type_enc
+ |> is_type_enc_sound type_enc
? (fold (fold add_fact_syms) [conjs, facts]
#> fold add_iterm_syms extra_tms
#> (case type_enc of
Native (First_Order, Polymorphic, _) =>
- if avoid_first_order_ghost_type_vars then add_TYPE_const ()
+ if avoid_first_order_phantom_type_vars then add_TYPE_const ()
else I
| Native _ => I
| _ => fold add_undefined_const (var_types ())))
@@ -2270,7 +2232,7 @@
maybe_infinite_Ts = known_infinite_types,
surely_infinite_Ts =
case level of
- Noninf_Nonmono_Types (Strict, _) => []
+ Nonmono_Types (Strict, _) => []
| _ => known_infinite_types,
maybe_nonmono_Ts = [@{typ bool}]}
@@ -2284,7 +2246,7 @@
let val thy = Proof_Context.theory_of ctxt in
if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
case level of
- Noninf_Nonmono_Types (strictness, _) =>
+ Nonmono_Types (strictness, _) =>
if exists (type_instance thy T) surely_infinite_Ts orelse
member (type_equiv thy) maybe_finite_Ts T then
mono
@@ -2301,22 +2263,6 @@
maybe_infinite_Ts = maybe_infinite_Ts,
surely_infinite_Ts = surely_infinite_Ts,
maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type thy I T}
- | Fin_Nonmono_Types _ =>
- if exists (type_instance thy T) surely_finite_Ts orelse
- member (type_equiv thy) maybe_infinite_Ts T then
- mono
- else if is_type_surely_finite ctxt T then
- {maybe_finite_Ts = maybe_finite_Ts,
- surely_finite_Ts = surely_finite_Ts |> insert_type thy I T,
- maybe_infinite_Ts = maybe_infinite_Ts,
- surely_infinite_Ts = surely_infinite_Ts,
- maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type thy I T}
- else
- {maybe_finite_Ts = maybe_finite_Ts,
- surely_finite_Ts = surely_finite_Ts,
- maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_equiv thy) T,
- surely_infinite_Ts = surely_infinite_Ts,
- maybe_nonmono_Ts = maybe_nonmono_Ts}
| _ => mono
else
mono
@@ -2348,7 +2294,7 @@
let val level = level_of_type_enc type_enc in
[] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
is_type_level_monotonicity_based level andalso
- granularity_of_type_level level <> Ghost_Type_Arg_Vars)
+ granularity_of_type_level level <> Undercover_Vars)
? fold (add_fact_monotonic_types ctxt mono type_enc) facts
end
@@ -2359,7 +2305,7 @@
IConst (`make_bound_var "X", T, [])
|> type_guard_iterm type_enc T
|> AAtom
- |> formula_from_iformula ctxt [] mono type_enc
+ |> formula_from_iformula ctxt mono type_enc
always_guard_var_in_formula (SOME true)
|> close_formula_universally
|> bound_tvars type_enc true (atomic_types_of T),
@@ -2417,16 +2363,10 @@
bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
val bound_Ts =
if exists (curry (op =) dummyT) T_args then
- case level_of_type_enc type_enc of
- All_Types => map SOME arg_Ts
- | level =>
- if granularity_of_type_level level = Ghost_Type_Arg_Vars then
- let val ghosts = ghost_type_args thy s ary in
- map2 (fn j => if member (op =) ghosts j then SOME else K NONE)
- (0 upto ary - 1) arg_Ts
- end
- else
- replicate ary NONE
+ let val cover = type_arg_cover thy s ary in
+ map2 (fn j => if member (op =) cover j then SOME else K NONE)
+ (0 upto ary - 1) arg_Ts
+ end
else
replicate ary NONE
in
@@ -2436,7 +2376,7 @@
|> fold (curry (IApp o swap)) bounds
|> type_guard_iterm type_enc res_T
|> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
- |> formula_from_iformula ctxt [] mono type_enc
+ |> formula_from_iformula ctxt mono type_enc
always_guard_var_in_formula (SOME true)
|> close_formula_universally
|> bound_tvars type_enc (n > 1) (atomic_types_of T)
@@ -2465,9 +2405,9 @@
if should_encode res_T then
let
val tagged_bounds =
- if grain = Ghost_Type_Arg_Vars then
- let val ghosts = ghost_type_args thy s ary in
- map2 (fn (j, arg_T) => member (op =) ghosts j ? tag_with arg_T)
+ if grain = Undercover_Vars then
+ let val cover = type_arg_cover thy s ary in
+ map2 (fn (j, arg_T) => member (op =) cover j ? tag_with arg_T)
(0 upto ary - 1 ~~ arg_Ts) bounds
end
else
@@ -2529,8 +2469,8 @@
fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
-fun do_uncurried_alias_lines_for_sym ctxt monom_constrs mono type_enc sym_tab0
- sym_tab base_s0 types in_conj =
+fun do_uncurried_alias_lines_for_sym ctxt constrs mono type_enc sym_tab0 sym_tab
+ base_s0 types in_conj =
let
fun do_alias ary =
let
@@ -2543,8 +2483,7 @@
mangle_type_args_in_const type_enc base_name T_args
val base_ary = min_ary_of sym_tab0 base_s
fun do_const name = IConst (name, T, T_args)
- val filter_ty_args =
- filter_type_args_in_iterm thy monom_constrs type_enc
+ val filter_ty_args = filter_type_args_in_iterm thy constrs type_enc
val ho_term_of = ho_term_from_iterm ctxt mono type_enc (SOME true)
val name1 as (s1, _) =
base_name |> ary - 1 > base_ary ? aliased_uncurried (ary - 1)
@@ -2574,7 +2513,7 @@
else pair_append (do_alias (ary - 1)))
end
in do_alias end
-fun uncurried_alias_lines_for_sym ctxt monom_constrs mono type_enc sym_tab0
+fun uncurried_alias_lines_for_sym ctxt constrs mono type_enc sym_tab0
sym_tab (s, {min_ary, types, in_conj, ...} : sym_info) =
case unprefix_and_unascii const_prefix s of
SOME mangled_s =>
@@ -2582,20 +2521,20 @@
let
val base_s0 = mangled_s |> unmangled_const_name |> hd |> invert_const
in
- do_uncurried_alias_lines_for_sym ctxt monom_constrs mono type_enc
- sym_tab0 sym_tab base_s0 types in_conj min_ary
+ do_uncurried_alias_lines_for_sym ctxt constrs mono type_enc sym_tab0
+ sym_tab base_s0 types in_conj min_ary
end
else
([], [])
| NONE => ([], [])
-fun uncurried_alias_lines_for_sym_table ctxt monom_constrs mono type_enc
+fun uncurried_alias_lines_for_sym_table ctxt constrs mono type_enc
uncurried_aliases sym_tab0 sym_tab =
([], [])
|> uncurried_aliases
? Symtab.fold_rev
(pair_append
- o uncurried_alias_lines_for_sym ctxt monom_constrs mono type_enc
- sym_tab0 sym_tab) sym_tab
+ o uncurried_alias_lines_for_sym ctxt constrs mono type_enc sym_tab0
+ sym_tab) sym_tab
val implicit_declsN = "Should-be-implicit typings"
val explicit_declsN = "Explicit typings"
@@ -2674,17 +2613,14 @@
(case U of Datatype.DtType (_, Us) => exists ex Us | _ => false)
in ex end
-fun is_poly_constr (_, Us) =
- exists (exists_subdtype (fn Datatype.DtTFree _ => true | _ => false)) Us
+val is_poly_constr =
+ exists_subdtype (fn Datatype.DtTFree _ => true | _ => false)
fun all_constrs_of_polymorphic_datatypes thy =
- Symtab.fold (snd
- #> #descr
- #> maps (snd #> #3)
- #> (fn cs => exists is_poly_constr cs ? append cs))
- (Datatype.get_all thy) []
- |> List.partition is_poly_constr
- |> pairself (map fst)
+ Symtab.fold (snd #> #descr #> maps (#3 o snd)
+ #> (fn cs => exists (exists is_poly_constr o snd) cs
+ ? append (map fst cs)))
+ (Datatype.get_all thy) []
val app_op_and_predicator_threshold = 50
@@ -2712,8 +2648,7 @@
val lam_trans =
if lam_trans = keep_lamsN andalso
not (is_type_enc_higher_order type_enc) then
- error ("Lambda translation scheme incompatible with first-order \
- \encoding.")
+ liftingN
else
lam_trans
val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses,
@@ -2723,17 +2658,15 @@
val (_, sym_tab0) =
sym_table_for_facts ctxt type_enc app_op_level conjs facts
val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
- val (polym_constrs, monom_constrs) =
- all_constrs_of_polymorphic_datatypes thy
- |>> map (make_fixed_const (SOME type_enc))
+ val constrs = all_constrs_of_polymorphic_datatypes thy
fun firstorderize in_helper =
- firstorderize_fact thy monom_constrs type_enc sym_tab0
+ firstorderize_fact thy constrs type_enc sym_tab0
(uncurried_aliases andalso not in_helper) aggressive
val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false))
val (ho_stuff, sym_tab) =
sym_table_for_facts ctxt type_enc Min_App_Op conjs facts
val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) =
- uncurried_alias_lines_for_sym_table ctxt monom_constrs mono type_enc
+ uncurried_alias_lines_for_sym_table ctxt constrs mono type_enc
uncurried_aliases sym_tab0 sym_tab
val (_, sym_tab) =
(ho_stuff, sym_tab)
@@ -2751,14 +2684,13 @@
|> problem_lines_for_sym_decl_table ctxt mono type_enc mono_Ts
val num_facts = length facts
val fact_lines =
- map (formula_line_for_fact ctxt polym_constrs fact_prefix
- ascii_of (not exporter) (not exporter) mono type_enc
- (rank_of_fact_num num_facts))
+ map (formula_line_for_fact ctxt fact_prefix ascii_of (not exporter)
+ (not exporter) mono type_enc (rank_of_fact_num num_facts))
(0 upto num_facts - 1 ~~ facts)
val helper_lines =
0 upto length helpers - 1 ~~ helpers
- |> map (formula_line_for_fact ctxt polym_constrs helper_prefix I false
- true mono type_enc (K default_rank))
+ |> map (formula_line_for_fact ctxt helper_prefix I false true mono
+ type_enc (K default_rank))
(* Reordering these might confuse the proof reconstruction code. *)
val problem =
[(explicit_declsN, class_decl_lines @ sym_decl_lines),
@@ -2769,9 +2701,7 @@
(aritiesN, map (formula_line_for_arity_clause type_enc) arity_clauses),
(helpersN, helper_lines),
(free_typesN, formula_lines_for_free_types type_enc (facts @ conjs)),
- (conjsN,
- map (formula_line_for_conjecture ctxt polym_constrs mono type_enc)
- conjs)]
+ (conjsN, map (formula_line_for_conjecture ctxt mono type_enc) conjs)]
val problem =
problem
|> (case format of
@@ -2785,10 +2715,8 @@
fun add_sym_ary (s, {min_ary, ...} : sym_info) =
min_ary > 0 ? Symtab.insert (op =) (s, min_ary)
in
- (problem,
- case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
- fact_names |> Vector.fromList,
- lifted,
+ (problem, pool |> Option.map snd |> the_default Symtab.empty,
+ fact_names |> Vector.fromList, lifted,
Symtab.empty |> Symtab.fold add_sym_ary sym_tab)
end
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Jun 12 15:31:53 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Jun 12 15:32:14 2012 +0200
@@ -201,9 +201,11 @@
isa_ext
fun add_all_defs fact_names accum =
- Vector.foldl (fn (facts, factss) =>
- filter (fn (_, (_, status)) => status = Def) facts @ factss)
- accum fact_names
+ Vector.foldl
+ (fn (facts, facts') =>
+ union (op =) (filter (fn (_, (_, status)) => status = Def) facts)
+ facts')
+ accum fact_names
fun add_fact ctxt fact_names (Inference_Step ((_, ss), _, rule, deps)) =
(if rule = leo2_ext then
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Jun 12 15:31:53 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Jun 12 15:32:14 2012 +0200
@@ -337,7 +337,10 @@
required_vars = [],
arguments =
fn _ => fn _ => fn _ => fn timeout => fn _ =>
- "--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout),
+ "--foatp e --atp e=\"$E_HOME\"/eprover \
+ \--atp epclextract=\"$E_HOME\"/epclextract \
+ \--proofoutput 1 --timeout " ^
+ string_of_int (to_secs 1 timeout),
proof_delims = tstp_proof_delims,
known_failures =
[(TimedOut, "CPU time limit exceeded, terminating"),
@@ -346,7 +349,7 @@
prem_role = Hypothesis,
best_slices =
(* FUDGE *)
- K [(1.0, (true, ((20, leo2_thf0, "mono_native_higher", keep_lamsN, false), "")))],
+ K [(1.0, (true, ((40, leo2_thf0, "mono_native_higher", keep_lamsN, false), "")))],
best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
best_max_new_mono_instances = default_max_new_mono_instances div 2 (* FUDGE *)}
@@ -596,7 +599,7 @@
remotify_atp satallax "Satallax" ["2.3", "2.2", "2"]
(K ((100, satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
val remote_vampire =
- remotify_atp vampire "Vampire" ["2.5", "1.8"]
+ remotify_atp vampire "Vampire" ["2.6", "2.5", "1.8"]
(K ((250, vampire_tff0, "mono_native", combs_or_liftingN, false), "") (* FUDGE *))
val remote_z3_tptp =
remotify_atp z3_tptp "Z3" ["3.0"]
--- a/src/HOL/Tools/Function/fun.ML Tue Jun 12 15:31:53 2012 +0200
+++ b/src/HOL/Tools/Function/fun.ML Tue Jun 12 15:32:14 2012 +0200
@@ -84,10 +84,10 @@
spec @ mk_catchall fixes arity_of
end
-fun warnings ctxt origs tss =
+fun further_checks ctxt origs tss =
let
- fun warn_redundant t =
- warning ("Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t))
+ fun fail_redundant t =
+ error (cat_lines ["Equation is redundant (covered by preceding clauses):", Syntax.string_of_term ctxt t])
fun warn_missing strs =
warning (cat_lines ("Missing patterns in function definition:" :: strs))
@@ -100,7 +100,7 @@
@ ["(" ^ string_of_int (length rest) ^ " more)"])
val _ = (origs ~~ tss')
- |> map (fn (t, ts) => if null ts then warn_redundant t else ())
+ |> map (fn (t, ts) => if null ts then fail_redundant t else ())
in
()
end
@@ -119,7 +119,7 @@
val compleqs = add_catchall ctxt fixes feqs (* Completion *)
val spliteqs = Function_Split.split_all_equations ctxt compleqs
- |> tap (warnings ctxt feqs)
+ |> tap (further_checks ctxt feqs)
fun restore_spec thms =
bnds ~~ take (length bnds) (unflat spliteqs thms)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Jun 12 15:31:53 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Jun 12 15:32:14 2012 +0200
@@ -38,8 +38,7 @@
let val n = length names in
string_of_int n ^ " fact" ^ plural_s n ^
(if n > 0 then
- ": " ^ (names |> map fst |> sort_distinct string_ord
- |> space_implode " ")
+ ": " ^ (names |> map fst |> sort string_ord |> space_implode " ")
else
"")
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 12 15:31:53 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 12 15:32:14 2012 +0200
@@ -679,7 +679,7 @@
val soundness = if strict then Strict else Non_Strict
val type_enc =
type_enc |> choose_type_enc soundness best_type_enc format
- val fairly_sound = is_type_enc_fairly_sound type_enc
+ val sound = is_type_enc_sound type_enc
val real_ms = Real.fromInt o Time.toMilliseconds
val slice_timeout =
((real_ms time_left
@@ -714,7 +714,7 @@
else
facts
|> map untranslated_fact
- |> not fairly_sound
+ |> not sound
? filter_out (is_dangerous_prop ctxt o prop_of o snd)
|> take num_facts
|> polymorphism_of_type_enc type_enc <> Polymorphic
@@ -764,11 +764,8 @@
SOME facts =>
let
val failure =
- if null facts then
- ProofIncomplete
- else
- UnsoundProof (is_type_enc_quasi_sound type_enc,
- facts)
+ if null facts then ProofIncomplete
+ else UnsoundProof (is_type_enc_sound type_enc, facts)
in
if debug then
(warning (string_for_failure failure); NONE)
--- a/src/HOL/Tools/list_code.ML Tue Jun 12 15:31:53 2012 +0200
+++ b/src/HOL/Tools/list_code.ML Tue Jun 12 15:32:14 2012 +0200
@@ -20,14 +20,14 @@
fun implode_list nil' cons' t =
let
- fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
+ fun dest_cons (IConst { name = c, ... } `$ t1 `$ t2) =
if c = cons'
then SOME (t1, t2)
else NONE
| dest_cons _ = NONE;
val (ts, t') = Code_Thingol.unfoldr dest_cons t;
in case t'
- of IConst (c, _) => if c = nil' then SOME ts else NONE
+ of IConst { name = c, ... } => if c = nil' then SOME ts else NONE
| _ => NONE
end;
--- a/src/HOL/Tools/numeral.ML Tue Jun 12 15:31:53 2012 +0200
+++ b/src/HOL/Tools/numeral.ML Tue Jun 12 15:32:14 2012 +0200
@@ -69,11 +69,11 @@
let
fun dest_numeral one' bit0' bit1' thm t =
let
- fun dest_bit (IConst (c, _)) = if c = bit0' then 0
+ fun dest_bit (IConst { name = c, ... }) = if c = bit0' then 0
else if c = bit1' then 1
else Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit"
| dest_bit _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit";
- fun dest_num (IConst (c, _)) = if c = one' then 1
+ fun dest_num (IConst { name = c, ... }) = if c = one' then 1
else Code_Printer.eqn_error thm "Illegal numeral expression: illegal leading digit"
| dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_bit t1
| dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
--- a/src/HOL/Tools/string_code.ML Tue Jun 12 15:31:53 2012 +0200
+++ b/src/HOL/Tools/string_code.ML Tue Jun 12 15:32:14 2012 +0200
@@ -23,13 +23,13 @@
| decode _ ~1 = NONE
| decode n m = SOME (chr (n * 16 + m));
in case tt
- of (IConst (c1, _), IConst (c2, _)) => decode (idx c1) (idx c2)
+ of (IConst { name = c1, ... }, IConst { name = c2, ... }) => decode (idx c1) (idx c2)
| _ => NONE
end;
fun implode_string char' nibbles' mk_char mk_string ts =
let
- fun implode_char (IConst (c, _) `$ t1 `$ t2) =
+ fun implode_char (IConst { name = c, ... } `$ t1 `$ t2) =
if c = char' then decode_char nibbles' (t1, t2) else NONE
| implode_char _ = NONE;
val ts' = map_filter implode_char ts;
--- a/src/Pure/Isar/code.ML Tue Jun 12 15:31:53 2012 +0200
+++ b/src/Pure/Isar/code.ML Tue Jun 12 15:32:14 2012 +0200
@@ -65,7 +65,8 @@
val get_type_of_constr_or_abstr: theory -> string -> (string * bool) option
val is_constr: theory -> string -> bool
val is_abstr: theory -> string -> bool
- val get_cert: theory -> ((thm * bool) list -> (thm * bool) list) -> string -> cert
+ val get_cert: theory -> { functrans: ((thm * bool) list -> (thm * bool) list option) list,
+ ss: simpset } -> string -> cert
val get_case_scheme: theory -> string -> (int * (int * string option list)) option
val get_case_cong: theory -> string -> thm option
val undefineds: theory -> string list
@@ -854,23 +855,39 @@
|> Option.map (snd o fst)
|> the_default empty_fun_spec
-fun get_cert thy f c = case retrieve_raw thy c
- of Default (_, eqns_lazy) => Lazy.force eqns_lazy
- |> (map o apfst) (Thm.transfer thy)
- |> f
- |> (map o apfst) (AxClass.unoverload thy)
- |> cert_of_eqns thy c
- | Eqns eqns => eqns
- |> (map o apfst) (Thm.transfer thy)
- |> f
- |> (map o apfst) (AxClass.unoverload thy)
- |> cert_of_eqns thy c
- | Proj (_, tyco) =>
- cert_of_proj thy c tyco
- | Abstr (abs_thm, tyco) => abs_thm
- |> Thm.transfer thy
- |> AxClass.unoverload thy
- |> cert_of_abs thy tyco c;
+fun eqn_conv conv ct =
+ let
+ fun lhs_conv ct = if can Thm.dest_comb ct
+ then Conv.combination_conv lhs_conv conv ct
+ else Conv.all_conv ct;
+ in Conv.combination_conv (Conv.arg_conv lhs_conv) conv ct end;
+
+fun rewrite_eqn thy conv ss =
+ let
+ val ctxt = Proof_Context.init_global thy;
+ val rewrite = Conv.fconv_rule (conv (Simplifier.rewrite ss));
+ in singleton (Variable.trade (K (map rewrite)) ctxt) end;
+
+fun cert_of_eqns_preprocess thy functrans ss c =
+ (map o apfst) (Thm.transfer thy)
+ #> perhaps (perhaps_loop (perhaps_apply functrans))
+ #> (map o apfst) (rewrite_eqn thy eqn_conv ss)
+ #> (map o apfst) (AxClass.unoverload thy)
+ #> cert_of_eqns thy c;
+
+fun get_cert thy { functrans, ss } c =
+ case retrieve_raw thy c
+ of Default (_, eqns_lazy) => Lazy.force eqns_lazy
+ |> cert_of_eqns_preprocess thy functrans ss c
+ | Eqns eqns => eqns
+ |> cert_of_eqns_preprocess thy functrans ss c
+ | Proj (_, tyco) =>
+ cert_of_proj thy c tyco
+ | Abstr (abs_thm, tyco) => abs_thm
+ |> Thm.transfer thy
+ |> rewrite_eqn thy Conv.arg_conv ss
+ |> AxClass.unoverload thy
+ |> cert_of_abs thy tyco c;
(* cases *)
--- a/src/Tools/Code/code_haskell.ML Tue Jun 12 15:31:53 2012 +0200
+++ b/src/Tools/Code/code_haskell.ML Tue Jun 12 15:32:14 2012 +0200
@@ -60,8 +60,8 @@
print_tyco_expr tyvars NOBR (tyco, map ITyVar vs);
fun print_typscheme tyvars (vs, ty) =
Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty);
- fun print_term tyvars some_thm vars fxy (IConst c) =
- print_app tyvars some_thm vars fxy (c, [])
+ fun print_term tyvars some_thm vars fxy (IConst const) =
+ print_app tyvars some_thm vars fxy (const, [])
| print_term tyvars some_thm vars fxy (t as (t1 `$ t2)) =
(case Code_Thingol.unfold_const_app t
of SOME app => print_app tyvars some_thm vars fxy app
@@ -79,15 +79,15 @@
val (binds, t') = Code_Thingol.unfold_pat_abs t;
val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars;
in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
- | print_term tyvars some_thm vars fxy (ICase (cases as (_, t0))) =
- (case Code_Thingol.unfold_const_app t0
- of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
- then print_case tyvars some_thm vars fxy cases
- else print_app tyvars some_thm vars fxy c_ts
- | NONE => print_case tyvars some_thm vars fxy cases)
- and print_app_expr tyvars some_thm vars ((c, ((_, (arg_tys, result_ty)), annotate)), ts) =
+ | print_term tyvars some_thm vars fxy (ICase case_expr) =
+ (case Code_Thingol.unfold_const_app (#primitive case_expr)
+ of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
+ then print_case tyvars some_thm vars fxy case_expr
+ else print_app tyvars some_thm vars fxy app
+ | NONE => print_case tyvars some_thm vars fxy case_expr)
+ and print_app_expr tyvars some_thm vars ({ name = c, dom, range, annotate, ... }, ts) =
let
- val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (arg_tys, result_ty)
+ val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (dom, range)
val printed_const =
if annotate then
brackets [(str o deresolve) c, str "::", print_typ tyvars NOBR ty]
@@ -98,9 +98,11 @@
end
and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
- and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
+ and print_case tyvars some_thm vars fxy { clauses = [], ... } =
+ (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""]
+ | print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) =
let
- val (binds, body) = Code_Thingol.unfold_let (ICase cases);
+ val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
fun print_match ((pat, _), t) vars =
vars
|> print_bind tyvars some_thm BR pat
@@ -110,7 +112,7 @@
ps
(concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body])
end
- | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
+ | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } =
let
fun print_select (pat, body) =
let
@@ -119,9 +121,7 @@
in Pretty.block_enclose
(concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
(map print_select clauses)
- end
- | print_case tyvars some_thm vars fxy ((_, []), _) =
- (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
+ end;
fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
let
val tyvars = intro_vars (map fst vs) reserved;
@@ -221,7 +221,7 @@
str "};"
) (map print_classparam classparams)
end
- | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
+ | print_stmt (_, Code_Thingol.Classinst { class, tyco, vs, inst_params, ... }) =
let
val tyvars = intro_vars (map fst vs) reserved;
fun requires_args classparam = case const_syntax classparam
@@ -237,14 +237,15 @@
]
| SOME k =>
let
- val (c, ((_, tys), _)) = const;
+ val { name = c, dom, range, ... } = const;
val (vs, rhs) = (apfst o map) fst
(Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
val s = if (is_some o const_syntax) c
then NONE else (SOME o Long_Name.base_name o deresolve) c;
val vars = reserved
|> intro_vars (map_filter I (s :: vs));
- val lhs = IConst (classparam, ((([], []), tys), false)) `$$ map IVar vs;
+ val lhs = IConst { name = classparam, typargs = [],
+ dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
(*dictionaries are not relevant at this late stage,
and these consts never need type annotations for disambiguation *)
in
@@ -264,7 +265,7 @@
str " where {"
],
str "};"
- ) (map print_classparam_instance classparam_instances)
+ ) (map print_classparam_instance inst_params)
end;
in print_stmt end;
@@ -407,7 +408,7 @@
of SOME ((pat, ty), t') =>
SOME ((SOME ((pat, ty), true), t1), t')
| NONE => NONE;
- fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) =
+ fun dest_monad c_bind_name (IConst { name = c, ... } `$ t1 `$ t2) =
if c = c_bind_name then dest_bind t1 t2
else NONE
| dest_monad _ t = case Code_Thingol.split_let t
--- a/src/Tools/Code/code_ml.ML Tue Jun 12 15:31:53 2012 +0200
+++ b/src/Tools/Code/code_ml.ML Tue Jun 12 15:32:14 2012 +0200
@@ -28,9 +28,10 @@
datatype ml_binding =
ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
- | ML_Instance of string * ((class * (string * (vname * sort) list))
- * ((class * (string * (string * dict list list))) list
- * (((string * const) * (thm * bool)) list * ((string * const) * (thm * bool)) list)));
+ | ML_Instance of string * { class: string, tyco: string, vs: (vname * sort) list,
+ superinsts: (class * (string * (string * dict list list))) list,
+ inst_params: ((string * const) * (thm * bool)) list,
+ superinst_params: ((string * const) * (thm * bool)) list };
datatype ml_stmt =
ML_Exc of string * (typscheme * int)
@@ -83,15 +84,15 @@
and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
(map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
- fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
- print_app is_pseudo_fun some_thm vars fxy (c, [])
+ fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
+ print_app is_pseudo_fun some_thm vars fxy (const, [])
| print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
str "_"
| print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
str (lookup_var vars v)
| print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
(case Code_Thingol.unfold_const_app t
- of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts
+ of SOME app => print_app is_pseudo_fun some_thm vars fxy app
| NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
print_term is_pseudo_fun some_thm vars BR t2])
| print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
@@ -102,15 +103,15 @@
#>> (fn p => concat [str "fn", p, str "=>"]);
val (ps, vars') = fold_map print_abs binds vars;
in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
- | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
- (case Code_Thingol.unfold_const_app t0
- of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
- then print_case is_pseudo_fun some_thm vars fxy cases
- else print_app is_pseudo_fun some_thm vars fxy c_ts
- | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
- and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (arg_tys, _)), _)), ts)) =
+ | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
+ (case Code_Thingol.unfold_const_app (#primitive case_expr)
+ of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
+ then print_case is_pseudo_fun some_thm vars fxy case_expr
+ else print_app is_pseudo_fun some_thm vars fxy app
+ | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
+ and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
if is_cons c then
- let val k = length arg_tys in
+ let val k = length dom in
if k < 2 orelse length ts = k
then (str o deresolve) c
:: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
@@ -118,14 +119,16 @@
end
else if is_pseudo_fun c
then (str o deresolve) c @@ str "()"
- else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
+ else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss
@ map (print_term is_pseudo_fun some_thm vars BR) ts
and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
(print_term is_pseudo_fun) const_syntax some_thm vars
and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
- and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
+ and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } =
+ (concat o map str) ["raise", "Fail", "\"empty case\""]
+ | print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) =
let
- val (binds, body) = Code_Thingol.unfold_let (ICase cases);
+ val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
fun print_match ((pat, _), t) vars =
vars
|> print_bind is_pseudo_fun some_thm NOBR pat
@@ -139,7 +142,7 @@
str "end"
]
end
- | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =
+ | print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } =
let
fun print_select delim (pat, body) =
let
@@ -154,9 +157,7 @@
:: print_select "of" clause
:: map (print_select "|") clauses
)
- end
- | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =
- (concat o map str) ["raise", "Fail", "\"empty case\""];
+ end;
fun print_val_decl print_typscheme (name, typscheme) = concat
[str "val", str (deresolve name), str ":", print_typscheme typscheme];
fun print_datatype_decl definer (tyco, (vs, cos)) =
@@ -206,7 +207,7 @@
))
end
| print_def is_pseudo_fun _ definer
- (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
+ (ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) =
let
fun print_super_instance (_, (classrel, x)) =
concat [
@@ -230,8 +231,8 @@
else print_dict_args vs)
@ str "="
:: enum "," "{" "}"
- (map print_super_instance super_instances
- @ map print_classparam_instance classparam_instances)
+ (map print_super_instance superinsts
+ @ map print_classparam_instance inst_params)
:: str ":"
@@ print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
))
@@ -386,15 +387,15 @@
and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
(map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
- fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
- print_app is_pseudo_fun some_thm vars fxy (c, [])
+ fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
+ print_app is_pseudo_fun some_thm vars fxy (const, [])
| print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
str "_"
| print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
str (lookup_var vars v)
| print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
(case Code_Thingol.unfold_const_app t
- of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts
+ of SOME app => print_app is_pseudo_fun some_thm vars fxy app
| NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
print_term is_pseudo_fun some_thm vars BR t2])
| print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
@@ -402,15 +403,15 @@
val (binds, t') = Code_Thingol.unfold_pat_abs t;
val (ps, vars') = fold_map (print_bind is_pseudo_fun some_thm BR o fst) binds vars;
in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
- | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
- (case Code_Thingol.unfold_const_app t0
- of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
- then print_case is_pseudo_fun some_thm vars fxy cases
- else print_app is_pseudo_fun some_thm vars fxy c_ts
- | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
- and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (tys, _)), _)), ts)) =
+ | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
+ (case Code_Thingol.unfold_const_app (#primitive case_expr)
+ of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
+ then print_case is_pseudo_fun some_thm vars fxy case_expr
+ else print_app is_pseudo_fun some_thm vars fxy app
+ | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
+ and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
if is_cons c then
- let val k = length tys in
+ let val k = length dom in
if length ts = k
then (str o deresolve) c
:: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
@@ -418,14 +419,16 @@
end
else if is_pseudo_fun c
then (str o deresolve) c @@ str "()"
- else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
+ else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss
@ map (print_term is_pseudo_fun some_thm vars BR) ts
and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
(print_term is_pseudo_fun) const_syntax some_thm vars
and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
- and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
+ and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } =
+ (concat o map str) ["failwith", "\"empty case\""]
+ | print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) =
let
- val (binds, body) = Code_Thingol.unfold_let (ICase cases);
+ val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
fun print_let ((pat, _), t) vars =
vars
|> print_bind is_pseudo_fun some_thm NOBR pat
@@ -436,7 +439,7 @@
brackify_block fxy (Pretty.chunks ps) []
(print_term is_pseudo_fun some_thm vars' NOBR body)
end
- | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =
+ | print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } =
let
fun print_select delim (pat, body) =
let
@@ -449,9 +452,7 @@
:: print_select "with" clause
:: map (print_select "|") clauses
)
- end
- | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =
- (concat o map str) ["failwith", "\"empty case\""];
+ end;
fun print_val_decl print_typscheme (name, typscheme) = concat
[str "val", str (deresolve name), str ":", print_typscheme typscheme];
fun print_datatype_decl definer (tyco, (vs, cos)) =
@@ -546,7 +547,7 @@
))
end
| print_def is_pseudo_fun _ definer
- (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
+ (ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) =
let
fun print_super_instance (_, (classrel, x)) =
concat [
@@ -570,8 +571,8 @@
else print_dict_args vs)
@ str "="
@@ brackets [
- enum_default "()" ";" "{" "}" (map print_super_instance super_instances
- @ map print_classparam_instance classparam_instances),
+ enum_default "()" ";" "{" "}" (map print_super_instance superinsts
+ @ map print_classparam_instance inst_params),
str ":",
print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
]
@@ -731,7 +732,7 @@
| _ => (eqs, NONE)
else (eqs, NONE)
in (ML_Function (name, (tysm, eqs')), some_value_name) end
- | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) =
+ | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as { vs, ... })) =
(ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
| ml_binding_of_stmt (name, _) =
error ("Binding block containing illegal statement: " ^ labelled_name name)
--- a/src/Tools/Code/code_preproc.ML Tue Jun 12 15:31:53 2012 +0200
+++ b/src/Tools/Code/code_preproc.ML Tue Jun 12 15:32:14 2012 +0200
@@ -14,7 +14,6 @@
val del_functrans: string -> theory -> theory
val simple_functrans: (theory -> thm list -> thm list option)
-> theory -> (thm * bool) list -> (thm * bool) list option
- val preprocess_functrans: theory -> (thm * bool) list -> (thm * bool) list
val print_codeproc: theory -> unit
type code_algebra
@@ -124,15 +123,6 @@
fun trans_conv_rule conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
-fun eqn_conv conv ct =
- let
- fun lhs_conv ct = if can Thm.dest_comb ct
- then Conv.combination_conv lhs_conv conv ct
- else Conv.all_conv ct;
- in Conv.combination_conv (Conv.arg_conv lhs_conv) conv ct end;
-
-val rewrite_eqn = Conv.fconv_rule o eqn_conv o Simplifier.rewrite;
-
fun term_of_conv thy conv =
Thm.cterm_of thy
#> conv
@@ -148,22 +138,6 @@
val resubst = curry (Term.betapplys o swap) all_vars;
in (resubst, term_of_conv thy conv (fold_rev lambda all_vars t)) end;
-
-fun preprocess_functrans thy =
- let
- val functrans = (map (fn (_, (_, f)) => f thy) o #functrans
- o the_thmproc) thy;
- in perhaps (perhaps_loop (perhaps_apply functrans)) end;
-
-fun preprocess thy =
- let
- val ctxt = Proof_Context.init_global thy;
- val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
- in
- preprocess_functrans thy
- #> (map o apfst) (singleton (Variable.trade (K (map (rewrite_eqn pre))) ctxt))
- end;
-
fun preprocess_conv thy =
let
val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
@@ -285,7 +259,10 @@
case try (Graph.get_node eqngr) c
of SOME (lhs, cert) => ((lhs, []), cert)
| NONE => let
- val cert = Code.get_cert thy (preprocess thy) c;
+ val functrans = (map (fn (_, (_, f)) => f thy)
+ o #functrans o the_thmproc) thy;
+ val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
+ val cert = Code.get_cert thy { functrans = functrans, ss = pre } c;
val (lhs, rhss) = Code.typargs_deps_of_cert thy cert;
in ((lhs, rhss), cert) end;
--- a/src/Tools/Code/code_printer.ML Tue Jun 12 15:31:53 2012 +0200
+++ b/src/Tools/Code/code_printer.ML Tue Jun 12 15:32:14 2012 +0200
@@ -315,7 +315,7 @@
|-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
- (app as ((c, ((_, (arg_tys, _)), _)), ts)) =
+ (app as ({ name = c, dom, ... }, ts)) =
case const_syntax c of
NONE => brackify fxy (print_app_expr some_thm vars app)
| SOME (Plain_const_syntax (_, s)) =>
@@ -323,7 +323,7 @@
| SOME (Complex_const_syntax (k, print)) =>
let
fun print' fxy ts =
- print (print_term some_thm) some_thm vars fxy (ts ~~ take k arg_tys);
+ print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom);
in
if k = length ts
then print' fxy ts
--- a/src/Tools/Code/code_scala.ML Tue Jun 12 15:31:53 2012 +0200
+++ b/src/Tools/Code/code_scala.ML Tue Jun 12 15:32:14 2012 +0200
@@ -46,8 +46,8 @@
fun constraint p1 p2 = Pretty.block [p1, str ":", Pretty.brk 1, p2];
fun print_var vars NONE = str "_"
| print_var vars (SOME v) = (str o lookup_var vars) v
- fun print_term tyvars is_pat some_thm vars fxy (IConst c) =
- print_app tyvars is_pat some_thm vars fxy (c, [])
+ fun print_term tyvars is_pat some_thm vars fxy (IConst const) =
+ print_app tyvars is_pat some_thm vars fxy (const, [])
| print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) =
(case Code_Thingol.unfold_const_app t
of SOME app => print_app tyvars is_pat some_thm vars fxy app
@@ -65,30 +65,30 @@
print_term tyvars false some_thm vars' NOBR t
]
end
- | print_term tyvars is_pat some_thm vars fxy (ICase (cases as (_, t0))) =
- (case Code_Thingol.unfold_const_app t0
- of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
- then print_case tyvars some_thm vars fxy cases
- else print_app tyvars is_pat some_thm vars fxy c_ts
- | NONE => print_case tyvars some_thm vars fxy cases)
+ | print_term tyvars is_pat some_thm vars fxy (ICase case_expr) =
+ (case Code_Thingol.unfold_const_app (#primitive case_expr)
+ of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
+ then print_case tyvars some_thm vars fxy case_expr
+ else print_app tyvars is_pat some_thm vars fxy app
+ | NONE => print_case tyvars some_thm vars fxy case_expr)
and print_app tyvars is_pat some_thm vars fxy
- (app as ((c, (((tys, _), (arg_tys, _)), _)), ts)) =
+ (app as ({ name = c, typargs, dom, ... }, ts)) =
let
val k = length ts;
- val tys' = if is_pat orelse
- (is_none (const_syntax c) andalso is_singleton_constr c) then [] else tys;
+ val typargs' = if is_pat orelse
+ (is_none (const_syntax c) andalso is_singleton_constr c) then [] else typargs;
val (l, print') = case const_syntax c
of NONE => (args_num c, fn fxy => fn ts => applify "(" ")"
(print_term tyvars is_pat some_thm vars NOBR) fxy
(applify "[" "]" (print_typ tyvars NOBR)
- NOBR ((str o deresolve) c) tys') ts)
+ NOBR ((str o deresolve) c) typargs') ts)
| SOME (Plain_const_syntax (k, s)) => (k, fn fxy => fn ts => applify "(" ")"
(print_term tyvars is_pat some_thm vars NOBR) fxy
(applify "[" "]" (print_typ tyvars NOBR)
- NOBR (str s) tys') ts)
+ NOBR (str s) typargs') ts)
| SOME (Complex_const_syntax (k, print)) =>
(k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
- (ts ~~ take k arg_tys))
+ (ts ~~ take k dom))
in if k = l then print' fxy ts
else if k < l then
print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
@@ -100,9 +100,11 @@
end end
and print_bind tyvars some_thm fxy p =
gen_print_bind (print_term tyvars true) some_thm fxy p
- and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
+ and print_case tyvars some_thm vars fxy { clauses = [], ... } =
+ (brackify fxy o Pretty.breaks o map str) ["sys.error(\"empty case\")"]
+ | print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) =
let
- val (bind :: binds, body) = Code_Thingol.unfold_let (ICase cases);
+ val (bind :: binds, body) = Code_Thingol.unfold_let (ICase case_expr);
fun print_match_val ((pat, ty), t) vars =
vars
|> print_bind tyvars some_thm BR pat
@@ -123,7 +125,7 @@
| insert_seps ((_, p) :: (seps_ps as (sep, _) :: _)) =
(if sep then Pretty.block [p, str ";"] else p) :: insert_seps seps_ps
in brackify_block fxy (str "{") (insert_seps all_seps_ps) (str "}") end
- | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
+ | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } =
let
fun print_select (pat, body) =
let
@@ -135,9 +137,7 @@
|> Pretty.block_enclose (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"], str "}")
|> single
|> enclose "(" ")"
- end
- | print_case tyvars some_thm vars fxy ((_, []), _) =
- (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"];
+ end;
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))
@@ -155,7 +155,7 @@
val vars = intro_vars params reserved;
in
concat [print_defhead tyvars vars name vs params tys ty',
- str ("error(\"" ^ name ^ "\")")]
+ str ("sys.error(\"" ^ name ^ "\")")]
end
| print_def name (vs, ty) eqs =
let
@@ -261,19 +261,19 @@
:: map print_classparam_def classparams
)
end
- | print_stmt (name, Code_Thingol.Classinst ((class, (tyco, vs)),
- (super_instances, (classparam_instances, further_classparam_instances)))) =
+ | print_stmt (name, Code_Thingol.Classinst
+ { class, tyco, vs, inst_params, superinst_params, ... }) =
let
val tyvars = intro_tyvars vs reserved;
val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
- fun print_classparam_instance ((classparam, const as (_, ((_, (tys, _)), _))), (thm, _)) =
+ fun print_classparam_instance ((classparam, const as { dom, ... }), (thm, _)) =
let
- val aux_tys = Name.invent_names (snd reserved) "a" tys;
- val auxs = map fst aux_tys;
+ val aux_dom = Name.invent_names (snd reserved) "a" dom;
+ val auxs = map fst aux_dom;
val vars = intro_vars auxs reserved;
val aux_abstr = if null auxs then [] else [enum "," "(" ")"
(map (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
- (print_typ tyvars NOBR ty)) aux_tys), str "=>"];
+ (print_typ tyvars NOBR ty)) aux_dom), str "=>"];
in
concat ([str "val", print_method classparam, str "="]
@ aux_abstr @| print_app tyvars false (SOME thm) vars NOBR
@@ -283,7 +283,7 @@
Pretty.block_enclose (concat [str "implicit def",
constraint (print_context tyvars vs name) (print_dicttyp tyvars classtyp),
str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
- (map print_classparam_instance (classparam_instances @ further_classparam_instances))
+ (map print_classparam_instance (inst_params @ superinst_params))
end;
in print_stmt end;
@@ -439,7 +439,7 @@
"true", "type", "val", "var", "while", "with", "yield"
]
#> fold (Code_Target.add_reserved target) [
- "apply", "error", "scala", "BigInt", "Nil", "List"
+ "apply", "sys", "scala", "BigInt", "Nil", "List"
];
end; (*struct*)
--- a/src/Tools/Code/code_simp.ML Tue Jun 12 15:31:53 2012 +0200
+++ b/src/Tools/Code/code_simp.ML Tue Jun 12 15:32:14 2012 +0200
@@ -38,8 +38,8 @@
fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss =
ss addsimps (map_filter (fst o snd)) eqs
|> fold Simplifier.add_cong (the_list some_cong)
- | add_stmt (Code_Thingol.Classinst (_, (_, (classparam_instances, _)))) ss =
- ss addsimps (map (fst o snd) classparam_instances)
+ | add_stmt (Code_Thingol.Classinst { inst_params, ... }) ss =
+ ss addsimps (map (fst o snd) inst_params)
| add_stmt _ ss = ss;
val add_program = Graph.fold (add_stmt o fst o snd);
--- a/src/Tools/Code/code_thingol.ML Tue Jun 12 15:31:53 2012 +0200
+++ b/src/Tools/Code/code_thingol.ML Tue Jun 12 15:32:14 2012 +0200
@@ -18,19 +18,18 @@
Dict of string list * plain_dict
and plain_dict =
Dict_Const of string * dict list list
- | Dict_Var of vname * (int * int)
+ | Dict_Var of vname * (int * int);
datatype itype =
`%% of string * itype list
| ITyVar of vname;
- type const = string * (((itype list * dict list list) * (itype list * itype)) * bool)
- (* (f [T1..Tn] {dicts} (_::S1) .. (_::Sm)) :: S =^= (f, ((([T1..Tn], dicts), ([S1..Sm], S)), ambiguous)) *)
+ type const = { name: string, typargs: itype list, dicts: dict list list,
+ dom: itype list, range: itype, annotate: bool };
datatype iterm =
IConst of const
| IVar of vname option
| `$ of iterm * iterm
| `|=> of (vname option * itype) * iterm
- | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
- (*((term, type), [(selector pattern, body term )]), primitive term)*)
+ | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm };
val `$$ : iterm * iterm list -> iterm;
val `|==> : (vname option * itype) list * iterm -> iterm;
type typscheme = (vname * sort) list * itype;
@@ -77,10 +76,10 @@
| Class of class * (vname * ((class * string) list * (string * itype) list))
| Classrel of class * class
| Classparam of string * class
- | Classinst of (class * (string * (vname * sort) list) (*class and arity*))
- * ((class * (string * (string * dict list list))) list (*super instances*)
- * (((string * const) * (thm * bool)) list (*class parameter instances*)
- * ((string * const) * (thm * bool)) list (*super class parameter instances*)))
+ | Classinst of { class: string, tyco: string, vs: (vname * sort) list,
+ superinsts: (class * (string * (string * dict list list))) list,
+ inst_params: ((string * const) * (thm * bool)) list,
+ superinst_params: ((string * const) * (thm * bool)) list };
type program = stmt Graph.T
val empty_funs: program -> string list
val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
@@ -126,7 +125,7 @@
case dest x
of NONE => ([], x)
| SOME (x1, x2) =>
- let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
+ let val (xs', x') = unfoldr dest x2 in (x1 :: xs', x') end;
(** language core - types, terms **)
@@ -137,21 +136,21 @@
Dict of string list * plain_dict
and plain_dict =
Dict_Const of string * dict list list
- | Dict_Var of vname * (int * int)
+ | Dict_Var of vname * (int * int);
datatype itype =
`%% of string * itype list
| ITyVar of vname;
-type const = string * (((itype list * dict list list) *
- (itype list (*types of arguments*) * itype (*result type*))) * bool (*requires type annotation*))
+type const = { name: string, typargs: itype list, dicts: dict list list,
+ dom: itype list, range: itype, annotate: bool };
datatype iterm =
IConst of const
| IVar of vname option
| `$ of iterm * iterm
| `|=> of (vname option * itype) * iterm
- | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
+ | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm };
(*see also signature*)
fun is_IVar (IVar _) = true
@@ -172,7 +171,7 @@
| _ => NONE);
val split_let =
- (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
+ (fn ICase { term = t, typ = ty, clauses = [(p, body)], ... } => SOME (((p, ty), t), body)
| _ => NONE);
val unfold_let = unfoldr split_let;
@@ -188,16 +187,16 @@
| fold' (IVar _) = I
| fold' (t1 `$ t2) = fold' t1 #> fold' t2
| fold' (_ `|=> t) = fold' t
- | fold' (ICase (((t, _), ds), _)) = fold' t
- #> fold (fn (pat, body) => fold' pat #> fold' body) ds
+ | fold' (ICase { term = t, clauses = clauses, ... }) = fold' t
+ #> fold (fn (p, body) => fold' p #> fold' body) clauses
in fold' end;
-val add_constnames = fold_constexprs (fn (c, _) => insert (op =) c);
+val add_constnames = fold_constexprs (fn { name = c, ... } => insert (op =) c);
fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys
| add_tycos (ITyVar _) = I;
-val add_tyconames = fold_constexprs (fn (_, (((tys, _), _), _)) => fold add_tycos tys);
+val add_tyconames = fold_constexprs (fn { typargs = tys, ... } => fold add_tycos tys);
fun fold_varnames f =
let
@@ -209,7 +208,7 @@
| fold_term vs (t1 `$ t2) = fold_term vs t1 #> fold_term vs t2
| fold_term vs ((SOME v, _) `|=> t) = fold_term (insert (op =) v vs) t
| fold_term vs ((NONE, _) `|=> t) = fold_term vs t
- | fold_term vs (ICase (((t, _), ds), _)) = fold_term vs t #> fold (fold_case vs) ds
+ | fold_term vs (ICase { term = t, clauses = clauses, ... }) = fold_term vs t #> fold (fold_case vs) clauses
and fold_case vs (p, t) = fold_term (add p vs) t;
in fold_term [] end;
fun add t = fold_aux add (insert (op =)) t;
@@ -219,9 +218,9 @@
fun split_pat_abs ((NONE, ty) `|=> t) = SOME ((IVar NONE, ty), t)
| split_pat_abs ((SOME v, ty) `|=> t) = SOME (case t
- of ICase (((IVar (SOME w), _), [(p, t')]), _) =>
- if v = w andalso (exists_var p v orelse not (exists_var t' v))
- then ((p, ty), t')
+ of ICase { term = IVar (SOME w), clauses = [(p, body)], ... } =>
+ if v = w andalso (exists_var p v orelse not (exists_var body v))
+ then ((p, ty), body)
else ((IVar (SOME v), ty), t)
| _ => ((IVar (SOME v), ty), t))
| split_pat_abs _ = NONE;
@@ -239,27 +238,27 @@
val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
-fun eta_expand k (c as (name, ((_, (tys, _)), _)), ts) =
+fun eta_expand k (const as { name = c, dom = tys, ... }, ts) =
let
val j = length ts;
val l = k - j;
val _ = if l > length tys
- then error ("Impossible eta-expansion for constant " ^ quote name) else ();
+ then error ("Impossible eta-expansion for constant " ^ quote c) else ();
val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
val vs_tys = (map o apfst) SOME
(Name.invent_names ctxt "a" ((take l o drop j) tys));
- in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
+ in vs_tys `|==> IConst const `$$ ts @ map (IVar o fst) vs_tys end;
fun contains_dict_var t =
let
fun cont_dict (Dict (_, d)) = cont_plain_dict d
and cont_plain_dict (Dict_Const (_, dss)) = (exists o exists) cont_dict dss
| cont_plain_dict (Dict_Var _) = true;
- fun cont_term (IConst (_, (((_, dss), _), _))) = (exists o exists) cont_dict dss
+ fun cont_term (IConst { dicts = dss, ... }) = (exists o exists) cont_dict dss
| cont_term (IVar _) = false
| cont_term (t1 `$ t2) = cont_term t1 orelse cont_term t2
| cont_term (_ `|=> t) = cont_term t
- | cont_term (ICase (_, t)) = cont_term t;
+ | cont_term (ICase { primitive = t, ... }) = cont_term t;
in cont_term t end;
@@ -427,11 +426,10 @@
| Class of class * (vname * ((class * string) list * (string * itype) list))
| Classrel of class * class
| Classparam of string * class
- | Classinst of (class * (string * (vname * sort) list))
- * ((class * (string * (string * dict list list))) list
- * (((string * const) * (thm * bool)) list
- * ((string * const) * (thm * bool)) list))
- (*see also signature*);
+ | Classinst of { class: string, tyco: string, vs: (vname * sort) list,
+ superinsts: (class * (string * (string * dict list list))) list,
+ inst_params: ((string * const) * (thm * bool)) list,
+ superinst_params: ((string * const) * (thm * bool)) list };
type program = stmt Graph.T;
@@ -444,9 +442,10 @@
(map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2)
| map_terms_bottom_up f ((v, ty) `|=> t) = f
((v, ty) `|=> map_terms_bottom_up f t)
- | map_terms_bottom_up f (ICase (((t, ty), ps), t0)) = f
- (ICase (((map_terms_bottom_up f t, ty), (map o pairself)
- (map_terms_bottom_up f) ps), map_terms_bottom_up f t0));
+ | map_terms_bottom_up f (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) = f
+ (ICase { term = map_terms_bottom_up f t, typ = ty,
+ clauses = (map o pairself) (map_terms_bottom_up f) clauses,
+ primitive = map_terms_bottom_up f t0 });
fun map_classparam_instances_as_term f =
(map o apfst o apsnd) (fn const => case f (IConst const) of IConst const' => const')
@@ -459,8 +458,11 @@
| map_terms_stmt f (stmt as Class _) = stmt
| map_terms_stmt f (stmt as Classrel _) = stmt
| map_terms_stmt f (stmt as Classparam _) = stmt
- | map_terms_stmt f (Classinst (arity, (super_instances, classparam_instances))) =
- Classinst (arity, (super_instances, (pairself o map_classparam_instances_as_term) f classparam_instances));
+ | map_terms_stmt f (Classinst { class, tyco, vs, superinsts,
+ inst_params, superinst_params }) =
+ Classinst { class = class, tyco = tyco, vs = vs, superinsts = superinsts,
+ inst_params = map_classparam_instances_as_term f inst_params,
+ superinst_params = map_classparam_instances_as_term f superinst_params };
fun is_cons program name = case Graph.get_node program name
of Datatypecons _ => true
@@ -484,7 +486,7 @@
quote (Proof_Context.extern_class ctxt sub ^ " < " ^ Proof_Context.extern_class ctxt super)
end
| Classparam (c, _) => quote (Code.string_of_const thy c)
- | Classinst ((class, (tyco, _)), _) =>
+ | Classinst { class, tyco, ... } =>
let
val Class (class, _) = Graph.get_node program class;
val Datatype (tyco, _) = Graph.get_node program tyco;
@@ -565,6 +567,9 @@
| NONE => "");
in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end;
+fun maybe_permissive f prgrm =
+ f prgrm |>> SOME handle PERMISSIVE () => (NONE, prgrm);
+
fun not_wellsorted thy permissive some_thm ty sort e =
let
val err_class = Sorts.class_error (Context.pretty_global thy) e;
@@ -576,6 +581,10 @@
(err_typ ^ "\n" ^ err_class)
end;
+fun undefineds thy (dep, (naming, program)) =
+ (map_filter (lookup_const naming) (Code.undefineds thy),
+ (dep, (naming, program)));
+
(* inference of type annotations for disambiguation with type classes *)
@@ -678,9 +687,9 @@
and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (class, tyco) =
let
val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
- val these_classparams = these o try (#params o AxClass.get_info thy);
- val classparams = these_classparams class;
- val further_classparams = maps these_classparams
+ val these_class_params = these o try (#params o AxClass.get_info thy);
+ val class_params = these_class_params class;
+ val superclass_params = maps these_class_params
((Sorts.complete_sort algebra o Sorts.super_classes algebra) class);
val vs = Name.invent_names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
@@ -710,12 +719,11 @@
##>> ensure_tyco thy algbr eqngr permissive tyco
##>> fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
##>> fold_map translate_super_instance super_classes
- ##>> fold_map translate_classparam_instance classparams
- ##>> fold_map translate_classparam_instance further_classparams
- #>> (fn (((((class, tyco), arity_args), super_instances),
- classparam_instances), further_classparam_instances) =>
- Classinst ((class, (tyco, arity_args)), (super_instances,
- (classparam_instances, further_classparam_instances))));
+ ##>> fold_map translate_classparam_instance class_params
+ ##>> fold_map translate_classparam_instance superclass_params
+ #>> (fn (((((class, tyco), vs), superinsts), inst_params), superinst_params) =>
+ Classinst { class = class, tyco = tyco, vs = vs,
+ superinsts = superinsts, inst_params = inst_params, superinst_params = superinst_params });
in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
and translate_typ thy algbr eqngr permissive (TFree (v, _)) =
pair (ITyVar (unprefix "'" v))
@@ -749,9 +757,9 @@
fold_map (translate_term thy algbr eqngr permissive some_thm) args
##>> translate_term thy algbr eqngr permissive some_thm (rhs, some_abs)
#>> rpair (some_thm, proper)
-and translate_eqns thy algbr eqngr permissive eqns prgrm =
- prgrm |> fold_map (translate_eqn thy algbr eqngr permissive) eqns
- handle PERMISSIVE () => ([], prgrm)
+and translate_eqns thy algbr eqngr permissive eqns =
+ maybe_permissive (fold_map (translate_eqn thy algbr eqngr permissive) eqns)
+ #>> these
and translate_const thy algbr eqngr permissive some_thm ((c, ty), some_abs) =
let
val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs))
@@ -759,17 +767,18 @@
then translation_error thy permissive some_thm
"Abstraction violation" ("constant " ^ Code.string_of_const thy c)
else ()
- val (annotate, ty') = dest_tagged_type ty
- val arg_typs = Sign.const_typargs thy (c, ty');
+ val (annotate, ty') = dest_tagged_type ty;
+ val typargs = Sign.const_typargs thy (c, ty');
val sorts = Code_Preproc.sortargs eqngr c;
- val (function_typs, body_typ) = Term.strip_type ty';
+ val (dom, range) = Term.strip_type ty';
in
ensure_const thy algbr eqngr permissive c
- ##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
- ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (arg_typs ~~ sorts)
- ##>> fold_map (translate_typ thy algbr eqngr permissive) (body_typ :: function_typs)
- #>> (fn (((c, arg_typs), dss), body_typ :: function_typs) =>
- IConst (c, (((arg_typs, dss), (function_typs, body_typ)), annotate)))
+ ##>> fold_map (translate_typ thy algbr eqngr permissive) typargs
+ ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (typargs ~~ sorts)
+ ##>> fold_map (translate_typ thy algbr eqngr permissive) (range :: dom)
+ #>> (fn (((c, typargs), dss), range :: dom) =>
+ IConst { name = c, typargs = typargs, dicts = dss,
+ dom = dom, range = range, annotate = annotate })
end
and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs)
@@ -788,26 +797,23 @@
val constrs =
if null case_pats then []
else map_filter I (map2 mk_constr case_pats (nth_drop t_pos ts));
- fun casify naming constrs ty ts =
+ fun casify undefineds constrs ty t_app ts =
let
- val undefineds = map_filter (lookup_const naming) (Code.undefineds thy);
fun collapse_clause vs_map ts body =
- let
- in case body
- of IConst (c, _) => if member (op =) undefineds c
+ case body
+ of IConst { name = c, ... } => if member (op =) undefineds c
then []
else [(ts, body)]
- | ICase (((IVar (SOME v), _), subclauses), _) =>
+ | ICase { term = IVar (SOME v), clauses = clauses, ... } =>
if forall (fn (pat', body') => exists_var pat' v
- orelse not (exists_var body' v)) subclauses
+ orelse not (exists_var body' v)) clauses
then case AList.lookup (op =) vs_map v
of SOME i => maps (fn (pat', body') =>
collapse_clause (AList.delete (op =) v vs_map)
- (nth_map i (K pat') ts) body') subclauses
+ (nth_map i (K pat') ts) body') clauses
| NONE => [(ts, body)]
else [(ts, body)]
- | _ => [(ts, body)]
- end;
+ | _ => [(ts, body)];
fun mk_clause mk tys t =
let
val (vs, body) = unfold_abs_eta tys t;
@@ -818,19 +824,20 @@
val ts_clause = nth_drop t_pos ts;
val clauses = if null case_pats
then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
- else maps (fn ((constr as IConst (_, ((_, (tys, _)), _)), n), t) =>
+ else maps (fn ((constr as IConst { dom = tys, ... }, n), t) =>
mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t)
(constrs ~~ (map_filter (fn (NONE, _) => NONE | (SOME _, t) => SOME t)
(case_pats ~~ ts_clause)));
- in ((t, ty), clauses) end;
+ in ICase { term = t, typ = ty, clauses = clauses, primitive = t_app `$$ ts } end;
in
translate_const thy algbr eqngr permissive some_thm (c_ty, NONE)
##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr permissive some_thm (constr, NONE)
#>> rpair n) constrs
##>> translate_typ thy algbr eqngr permissive ty
##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
- #-> (fn (((t, constrs), ty), ts) =>
- `(fn (_, (naming, _)) => ICase (casify naming constrs ty ts, t `$$ ts)))
+ ##>> undefineds thy
+ #>> (fn ((((t, constrs), ty), ts), undefineds) =>
+ casify undefineds constrs ty t ts)
end
and translate_app_case thy algbr eqngr permissive some_thm (case_scheme as (num_args, _)) ((c, ty), ts) =
if length ts < num_args then
--- a/src/Tools/nbe.ML Tue Jun 12 15:31:53 2012 +0200
+++ b/src/Tools/nbe.ML Tue Jun 12 15:32:14 2012 +0200
@@ -314,13 +314,13 @@
let
val (t', ts) = Code_Thingol.unfold_app t
in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
- and of_iapp match_cont (IConst (c, (((_, dss), _), _))) ts = constapp c dss ts
+ and of_iapp match_cont (IConst { name = c, dicts = dss, ... }) ts = constapp c dss ts
| of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts
| of_iapp match_cont ((v, _) `|=> t) ts =
nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts
- | of_iapp match_cont (ICase (((t, _), cs), t0)) ts =
+ | of_iapp match_cont (ICase { term = t, clauses = clauses, primitive = t0, ... }) ts =
nbe_apps (ml_cases (of_iterm NONE t)
- (map (fn (p, t) => (of_iterm NONE p, of_iterm match_cont t)) cs
+ (map (fn (p, t) => (of_iterm NONE p, of_iterm match_cont t)) clauses
@ [("_", case match_cont of SOME s => s | NONE => of_iterm NONE t0)])) ts
in of_iterm end;
@@ -345,7 +345,7 @@
|> subst_vars t1
||>> subst_vars t2
|>> (op `$)
- | subst_vars (ICase (_, t)) samepairs = subst_vars t samepairs;
+ | subst_vars (ICase { primitive = t, ... }) samepairs = subst_vars t samepairs;
val (args', _) = fold_map subst_vars args samepairs;
in (samepairs, args') end;
@@ -410,6 +410,10 @@
(* extract equations from statements *)
+fun dummy_const c dss =
+ IConst { name = c, typargs = [], dicts = dss,
+ dom = [], range = ITyVar "", annotate = false };
+
fun eqns_of_stmt (_, Code_Thingol.Fun (_, ((_, []), _))) =
[]
| eqns_of_stmt (const, Code_Thingol.Fun (_, (((vs, _), eqns), _))) =
@@ -424,17 +428,17 @@
val params = Name.invent Name.context "d" (length names);
fun mk (k, name) =
(name, ([(v, [])],
- [([IConst (class, ((([], []), ([], ITyVar "")), false)) `$$ map (IVar o SOME) params],
+ [([dummy_const class [] `$$ map (IVar o SOME) params],
IVar (SOME (nth params k)))]));
in map_index mk names end
| eqns_of_stmt (_, Code_Thingol.Classrel _) =
[]
| eqns_of_stmt (_, Code_Thingol.Classparam _) =
[]
- | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, (classparam_instances, _)))) =
- [(inst, (arity_args, [([], IConst (class, ((([], []), ([], ITyVar "")), false)) `$$
- map (fn (_, (_, (inst, dss))) => IConst (inst, ((([], dss), ([], ITyVar "")), false))) super_instances
- @ map (IConst o snd o fst) classparam_instances)]))];
+ | eqns_of_stmt (inst, Code_Thingol.Classinst { class, vs, superinsts, inst_params, ... }) =
+ [(inst, (vs, [([], dummy_const class [] `$$
+ map (fn (_, (_, (inst, dss))) => dummy_const inst dss) superinsts
+ @ map (IConst o snd o fst) inst_params)]))];
(* compile whole programs *)