# HG changeset patch # User Andreas Lochbihler # Date 1339507934 -7200 # Node ID 1b9796b7ab03bf5ed57e4c9d32a6659c9d7630ad # Parent 0122ba071e1a6dbc7a1518b2087d8f48a52f8c42# Parent e7e647949c95116d1315f9f221e57a40e199ac75 merged diff -r 0122ba071e1a -r 1b9796b7ab03 NEWS --- 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) ------------------------------ diff -r 0122ba071e1a -r 1b9796b7ab03 doc-src/Sledgehammer/sledgehammer.tex --- 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. diff -r 0122ba071e1a -r 1b9796b7ab03 src/HOL/HOL.thy --- 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 *} diff -r 0122ba071e1a -r 1b9796b7ab03 src/HOL/Imperative_HOL/Array.thy --- 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((_))") diff -r 0122ba071e1a -r 1b9796b7ab03 src/HOL/Imperative_HOL/Heap_Monad.thy --- 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 + diff -r 0122ba071e1a -r 1b9796b7ab03 src/HOL/Imperative_HOL/Ref.thy --- 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((_), (_))") diff -r 0122ba071e1a -r 1b9796b7ab03 src/HOL/Library/Code_Integer.thy --- 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 * \ int \ int \ int" (SML "IntInf.* ((_), (_))") diff -r 0122ba071e1a -r 1b9796b7ab03 src/HOL/Library/Efficient_Nat.thy --- 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 \ nat \ nat \ 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 *} diff -r 0122ba071e1a -r 1b9796b7ab03 src/HOL/Library/Target_Numeral.thy --- 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 \ _ \ _" (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 \ Target_Numeral.of_nat" + "num_of_nat = Target_Numeral.num_of_int \ of_nat" by (simp add: fun_eq_iff num_of_int_def of_nat_def) lemma (in semiring_1) of_nat_code: diff -r 0122ba071e1a -r 1b9796b7ab03 src/HOL/Metis_Examples/Type_Encodings.thy --- 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 \ y = x" by metis_exhaust -lemma "[a] = [1 + 1] \ a = 1 + (1::int)" -by (metis_exhaust last.simps) +lemma "[a] = [Suc 0] \ 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) \ null xs \ xs = []" by (metis_exhaust null_def) -lemma "(0::nat) + 0 = 0" +lemma "(0\nat) + 0 = 0" by (metis_exhaust add_0_left) end diff -r 0122ba071e1a -r 1b9796b7ab03 src/HOL/TPTP/atp_problem_import.ML --- 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 **) diff -r 0122ba071e1a -r 1b9796b7ab03 src/HOL/TPTP/lib/Tools/tptp_isabelle --- /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 diff -r 0122ba071e1a -r 1b9796b7ab03 src/HOL/TPTP/lib/Tools/tptp_isabelle_comp --- 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 diff -r 0122ba071e1a -r 1b9796b7ab03 src/HOL/TPTP/lib/Tools/tptp_isabelle_demo --- 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 diff -r 0122ba071e1a -r 1b9796b7ab03 src/HOL/TPTP/lib/Tools/tptp_isabelle_hot --- /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 diff -r 0122ba071e1a -r 1b9796b7ab03 src/HOL/Tools/ATP/atp_problem_generate.ML --- 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 diff -r 0122ba071e1a -r 1b9796b7ab03 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- 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 diff -r 0122ba071e1a -r 1b9796b7ab03 src/HOL/Tools/ATP/atp_systems.ML --- 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"] diff -r 0122ba071e1a -r 1b9796b7ab03 src/HOL/Tools/Function/fun.ML --- 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) diff -r 0122ba071e1a -r 1b9796b7ab03 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- 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 diff -r 0122ba071e1a -r 1b9796b7ab03 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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) diff -r 0122ba071e1a -r 1b9796b7ab03 src/HOL/Tools/list_code.ML --- 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; diff -r 0122ba071e1a -r 1b9796b7ab03 src/HOL/Tools/numeral.ML --- 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"; diff -r 0122ba071e1a -r 1b9796b7ab03 src/HOL/Tools/string_code.ML --- 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; diff -r 0122ba071e1a -r 1b9796b7ab03 src/Pure/Isar/code.ML --- 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 *) diff -r 0122ba071e1a -r 1b9796b7ab03 src/Tools/Code/code_haskell.ML --- 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 diff -r 0122ba071e1a -r 1b9796b7ab03 src/Tools/Code/code_ml.ML --- 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) diff -r 0122ba071e1a -r 1b9796b7ab03 src/Tools/Code/code_preproc.ML --- 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; diff -r 0122ba071e1a -r 1b9796b7ab03 src/Tools/Code/code_printer.ML --- 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 diff -r 0122ba071e1a -r 1b9796b7ab03 src/Tools/Code/code_scala.ML --- 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*) diff -r 0122ba071e1a -r 1b9796b7ab03 src/Tools/Code/code_simp.ML --- 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); diff -r 0122ba071e1a -r 1b9796b7ab03 src/Tools/Code/code_thingol.ML --- 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 diff -r 0122ba071e1a -r 1b9796b7ab03 src/Tools/nbe.ML --- 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 *)