--- a/NEWS Tue Apr 05 15:04:55 2011 +0200
+++ b/NEWS Tue Apr 05 15:15:33 2011 +0200
@@ -49,7 +49,7 @@
* Sledgehammer:
- sledgehammer available_provers ~> sledgehammer supported_provers
INCOMPATIBILITY.
- - Added "monomorphize" and "monomorphize_limit" options.
+ - Added "monomorphize", "monomorphize_limit", and "type_sys" options.
* "try":
- Added "simp:", "intro:", and "elim:" options.
--- a/doc-src/Sledgehammer/sledgehammer.tex Tue Apr 05 15:04:55 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Apr 05 15:15:33 2011 +0200
@@ -476,7 +476,7 @@
\end{enum}
By default, Sledgehammer will run E, SPASS, Vampire, SInE-E, and Z3 (or whatever
-the SMT module's \emph{smt\_solver} configuration option is set to) in
+the SMT module's \textit{smt\_solver} configuration option is set to) in
parallel---either locally or remotely, depending on the number of processor
cores available. For historical reasons, the default value of this option can be
overridden using the option ``Sledgehammer: Provers'' from the ``Isabelle'' menu
@@ -536,6 +536,51 @@
tends to slow down the ATPs significantly. For historical reasons, the default
value of this option can be overridden using the option ``Sledgehammer: Full
Types'' from the ``Isabelle'' menu in Proof General.
+
+\opfalse{full\_types}{partial\_types}
+Specifies whether full-type information is encoded in ATP problems. Enabling
+this option can prevent the discovery of type-incorrect proofs, but it also
+tends to slow down the ATPs significantly. For historical reasons, the default
+value of this option can be overridden using the option ``Sledgehammer: Full
+Types'' from the ``Isabelle'' menu in Proof General.
+
+\opfalse{monomorphize}{dont\_monomorphize}
+Specifies whether the relevant facts should be monomorphized---i.e., whether
+their type variables should be instantiated with relevant ground types.
+Monomorphization is always performed for SMT solvers, irrespective of this
+option. Monomorphization can simplify reasoning but also leads to larger fact
+bases, which can slow down the ATPs.
+
+\opdefault{monomorphize\_limit}{int}{\upshape 4}
+Specifies the maximum number of iterations for the monomorphization fixpoint
+construction. The higher this limit is, the more monomorphic instances are
+potentially generated.
+
+\opdefault{type\_sys}{string}{smart}
+Specifies the type system to use in ATP problems. The option can take the
+following values:
+
+\begin{enum}
+\item[$\bullet$] \textbf{\textit{tags}:} Each term (and subterm) is tagged with
+its type.
+
+\item[$\bullet$] \textbf{\textit{args}:} Constants are annotated with
+their type parameters, which are passed as extra arguments. This value is
+ignored if \textit{full\_types} is enabled.
+
+\item[$\bullet$] \textbf{\textit{mangled}:} Types are mangled in constant names.
+This value is available only if \textit{monomorphize} is enabled and
+\textit{full\_types} is disabled.
+
+\item[$\bullet$] \textbf{\textit{none}:} No type information is supplied to the
+ATP. This value is ignored if \textit{full\_types} is enabled.
+
+\item[$\bullet$] \textbf{\textit{smart}:} If \textit{full\_types} is enabled,
+this is the same as \textit{tags}; otherwise, this is the
+same as \textit{args} otherwise.
+\end{enum}
+
+For SMT solvers, the type system is always \textit{mangled}.
\end{enum}
\subsection{Relevance Filter}
@@ -556,18 +601,6 @@
empirically found to be appropriate for the prover. A typical value would be
300.
-\opfalse{monomorphize}{dont\_monomorphize}
-Specifies whether the relevant facts should be monomorphized---i.e., whether
-their type variables should be instantiated with relevant ground types.
-Monomorphization is always performed for SMT solvers, irrespective of this
-option. Monomorphization can simplify reasoning but also leads to larger fact
-bases, which can slow down the ATPs.
-
-\opdefault{monomorphize\_limit}{int}{\upshape 4}
-Specifies the maximum number of iterations for the monomorphization fixpoint
-construction. The higher this limit is, the more monomorphic instances are
-potentially generated.
-
\end{enum}
\subsection{Output Format}
--- a/src/HOL/Fun.thy Tue Apr 05 15:04:55 2011 +0200
+++ b/src/HOL/Fun.thy Tue Apr 05 15:15:33 2011 +0200
@@ -770,7 +770,7 @@
subsection {* Cantor's Paradox *}
-lemma Cantors_paradox:
+lemma Cantors_paradox [no_atp]:
"\<not>(\<exists>f. f ` A = Pow A)"
proof clarify
fix f assume "f ` A = Pow A" hence *: "Pow A \<le> f ` A" by blast
--- a/src/HOL/Library/Code_Char.thy Tue Apr 05 15:04:55 2011 +0200
+++ b/src/HOL/Library/Code_Char.thy Tue Apr 05 15:15:33 2011 +0200
@@ -58,4 +58,7 @@
(Haskell "_")
(Scala "!(_.toList)")
+
+declare Quickcheck_Exhaustive.char.bounded_forall_char.simps [code del]
+
end
--- a/src/HOL/Quickcheck_Exhaustive.thy Tue Apr 05 15:04:55 2011 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy Tue Apr 05 15:15:33 2011 +0200
@@ -360,18 +360,6 @@
class bounded_forall =
fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> code_numeral \<Rightarrow> bool"
-
-instantiation nat :: bounded_forall
-begin
-
-fun bounded_forall_nat :: "(nat => bool) => code_numeral => bool"
-where
- "bounded_forall P d = ((P 0) \<and> (if d > 0 then bounded_forall (%n. P (Suc n)) (d - 1) else True))"
-
-instance ..
-
-end
-
subsection {* Defining combinators for any first-order data type *}
definition catch_match :: "term list option => term list option => term list option"
--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Apr 05 15:04:55 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Apr 05 15:15:33 2011 +0200
@@ -123,6 +123,16 @@
fun pool_map f xs =
pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
+val no_qualifiers =
+ let
+ fun skip [] = []
+ | skip (#"." :: cs) = skip cs
+ | skip (c :: cs) = if Char.isAlphaNum c then skip cs else c :: keep cs
+ and keep [] = []
+ | keep (#"." :: cs) = skip cs
+ | keep (c :: cs) = c :: keep cs
+ in String.explode #> rev #> keep #> rev #> String.implode end
+
(* "op" is also reserved, to avoid the unreadable "op_1", "op_2", etc., in the
problem files. "equal" is reserved by some ATPs. "eq" is reserved to ensure
that "HOL.eq" is correctly mapped to equality. *)
@@ -132,7 +142,7 @@
s
else
let
- val s = s |> Long_Name.base_name
+ val s = s |> no_qualifiers
|> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
in if member (op =) reserved_nice_names s then full_name else s end
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Tue Apr 05 15:04:55 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Tue Apr 05 15:15:33 2011 +0200
@@ -156,7 +156,7 @@
fun instantiate_exhaustive_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
let
- val _ = Datatype_Aux.message config "Creating exhaustive generators ...";
+ val _ = Datatype_Aux.message config "Creating exhaustive generators...";
val exhaustivesN = map (prefix (exhaustiveN ^ "_")) (names @ auxnames);
in
thy
@@ -170,6 +170,71 @@
"Creation of exhaustive generators failed because the datatype contains a function type";
thy)
+(* constructing bounded_forall instances on datatypes *)
+
+val bounded_forallN = "bounded_forall";
+
+fun bounded_forallT T = (T --> @{typ bool}) --> @{typ code_numeral} --> @{typ bool}
+
+fun mk_bounded_forall_equations descr vs tycos bounded_foralls (Ts, Us) =
+ let
+ fun mk_call T =
+ let
+ val bounded_forall =
+ Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"},
+ bounded_forallT T)
+ in
+ (T, (fn t => bounded_forall $ absdummy (T, t) $ size_pred))
+ end
+ fun mk_aux_call fTs (k, _) (tyco, Ts) =
+ let
+ val T = Type (tyco, Ts)
+ val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
+ in
+ (T, (fn t => nth bounded_foralls k $ absdummy (T, t) $ size_pred))
+ end
+ fun mk_consexpr simpleT (c, xs) =
+ let
+ val (Ts, fns) = split_list xs
+ val constr = Const (c, Ts ---> simpleT)
+ val bounds = map Bound (((length xs) - 1) downto 0)
+ val start_term = Free ("P", simpleT --> @{typ bool}) $ list_comb (constr, bounds)
+ in fold_rev (fn f => fn t => f t) fns start_term end
+ fun mk_rhs exprs =
+ @{term "If :: bool => bool => bool => bool"} $ size_ge_zero $
+ (foldr1 HOLogic.mk_disj exprs) $ @{term "True"}
+ val rhss =
+ Datatype_Aux.interpret_construction descr vs
+ { atyp = mk_call, dtyp = mk_aux_call }
+ |> (map o apfst) Type
+ |> map (fn (T, cs) => map (mk_consexpr T) cs)
+ |> map mk_rhs
+ val lhss =
+ map2 (fn t => fn T => t $ Free ("P", T --> @{typ bool}) $ size) bounded_foralls (Ts @ Us)
+ val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
+ in
+ eqs
+ end
+
+(* creating the bounded_forall instances *)
+
+fun instantiate_bounded_forall_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
+ let
+ val _ = Datatype_Aux.message config "Creating bounded universal quantifiers...";
+ val bounded_forallsN = map (prefix (bounded_forallN ^ "_")) (names @ auxnames);
+ in
+ thy
+ |> Class.instantiation (tycos, vs, @{sort bounded_forall})
+ |> Quickcheck_Common.define_functions
+ (fn bounded_foralls =>
+ mk_bounded_forall_equations descr vs tycos bounded_foralls (Ts, Us), NONE)
+ prfx ["P", "i"] bounded_forallsN (map bounded_forallT (Ts @ Us))
+ |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
+ end handle FUNCTION_TYPE =>
+ (Datatype_Aux.message config
+ "Creation of bounded universal quantifiers failed because the datatype contains a function type";
+ thy)
+
(** building and compiling generator expressions **)
fun mk_generator_expr ctxt (t, eval_terms) =
@@ -332,8 +397,10 @@
(** setup **)
val setup =
- Datatype.interpretation
- (Quickcheck_Common.ensure_sort_datatype (@{sort exhaustive}, instantiate_exhaustive_datatype))
+ Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
+ (((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype))
+ #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
+ (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))
#> setup_smart_quantifier
#> setup_quickcheck_pretty
#> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Tue Apr 05 15:04:55 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Tue Apr 05 15:15:33 2011 +0200
@@ -12,11 +12,12 @@
val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list
-> (string * sort -> string * sort) option
val ensure_sort_datatype:
- sort * (Datatype.config -> Datatype.descr -> (string * sort) list -> string list -> string ->
- string list * string list -> typ list * typ list -> theory -> theory)
+ ((sort * sort) * sort) * (Datatype.config -> Datatype.descr -> (string * sort) list
+ -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory)
-> Datatype.config -> string list -> theory -> theory
val gen_mk_parametric_generator_expr :
- (((Proof.context -> term * term list -> term) * term) * typ) -> Proof.context -> (term * term list) list -> term
+ (((Proof.context -> term * term list -> term) * term) * typ)
+ -> Proof.context -> (term * term list) list -> term
val post_process_term : term -> term
end;
@@ -86,25 +87,20 @@
in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
end handle Sorts.CLASS_ERROR _ => NONE;
-fun ensure_sort_datatype (sort, instantiate_datatype) config raw_tycos thy =
+fun ensure_sort_datatype (((sort_vs, aux_sort), sort), instantiate_datatype) config raw_tycos thy =
let
val algebra = Sign.classes_of thy;
- val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) =
- Datatype.the_descr thy raw_tycos;
- val typerep_vs = (map o apsnd)
- (curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
- val sort_insts = (map (rpair sort) o flat o maps snd o maps snd)
- (Datatype_Aux.interpret_construction descr typerep_vs
- { atyp = single, dtyp = (K o K o K) [] });
- val term_of_insts = (map (rpair @{sort term_of}) o flat o maps snd o maps snd)
- (Datatype_Aux.interpret_construction descr typerep_vs
- { atyp = K [], dtyp = K o K });
- val has_inst = exists (fn tyco =>
- can (Sorts.mg_domain algebra tyco) sort) tycos;
+ val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) = Datatype.the_descr thy raw_tycos
+ val vs = (map o apsnd) (curry (Sorts.inter_sort algebra) sort_vs) raw_vs
+ fun insts_of sort constr = (map (rpair sort) o flat o maps snd o maps snd)
+ (Datatype_Aux.interpret_construction descr vs constr)
+ val insts = insts_of sort { atyp = single, dtyp = (K o K o K) [] }
+ @ insts_of aux_sort { atyp = K [], dtyp = K o K }
+ val has_inst = exists (fn tyco => can (Sorts.mg_domain algebra tyco) sort) tycos;
in if has_inst then thy
- else case perhaps_constrain thy (sort_insts @ term_of_insts) typerep_vs
+ else case perhaps_constrain thy insts vs
of SOME constrain => instantiate_datatype config descr
- (map constrain typerep_vs) tycos prfx (names, auxnames)
+ (map constrain vs) tycos prfx (names, auxnames)
((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
| NONE => thy
end;
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Tue Apr 05 15:04:55 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Tue Apr 05 15:15:33 2011 +0200
@@ -442,7 +442,8 @@
(** setup **)
val setup =
- Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype (@{sort random}, instantiate_random_datatype))
+ Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
+ (((@{sort typerep}, @{sort term_of}), @{sort random}), instantiate_random_datatype))
#> Code_Target.extend_target (target, (Code_Runtime.target, K I))
#> Context.theory_map
(Quickcheck.add_generator ("random", compile_generator_expr));
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Tue Apr 05 15:04:55 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Tue Apr 05 15:15:33 2011 +0200
@@ -345,23 +345,23 @@
end
| SOME b =>
let
- val c = invert_const b
+ val (c, mangled_us) = b |> unmangled_const |>> invert_const
val num_ty_args = num_atp_type_args thy type_sys c
- val (type_us, term_us) = chop num_ty_args us
+ val (type_us, term_us) = chop num_ty_args us |>> append mangled_us
(* Extra args from "hAPP" come after any arguments given directly to
the constant. *)
val term_ts = map (aux NONE []) term_us
val extra_ts = map (aux NONE []) extra_us
- val t =
- Const (c, case opt_T of
- SOME T => map fastype_of term_ts ---> T
- | NONE =>
- if num_type_args thy c = length type_us then
- Sign.const_instance thy (c,
- map (type_from_fo_term tfrees) type_us)
- else
- HOLogic.typeT)
- in list_comb (t, term_ts @ extra_ts) end
+ val T =
+ case opt_T of
+ SOME T => map fastype_of term_ts ---> T
+ | NONE =>
+ if num_type_args thy c = length type_us then
+ Sign.const_instance thy (c,
+ map (type_from_fo_term tfrees) type_us)
+ else
+ HOLogic.typeT
+ in list_comb (Const (c, T), term_ts @ extra_ts) end
| NONE => (* a free or schematic variable *)
let
val ts = map (aux NONE []) (us @ extra_us)
@@ -399,7 +399,8 @@
| uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
| uncombine_term (t as Const (x as (s, _))) =
(case AList.lookup (op =) combinator_table s of
- SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd
+ SOME thm => thm |> prop_of |> specialize_type @{theory} x
+ |> Logic.dest_equals |> snd
| NONE => t)
| uncombine_term t = t
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue Apr 05 15:04:55 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue Apr 05 15:15:33 2011 +0200
@@ -8,13 +8,14 @@
signature SLEDGEHAMMER_ATP_TRANSLATE =
sig
+ type 'a fo_term = 'a ATP_Problem.fo_term
type 'a problem = 'a ATP_Problem.problem
type translated_formula
datatype type_system =
Tags of bool |
- Preds of bool |
- Const_Args |
+ Args |
+ Mangled |
No_Types
val precise_overloaded_args : bool Unsynchronized.ref
@@ -25,6 +26,7 @@
val translate_atp_fact :
Proof.context -> bool -> (string * 'a) * thm
-> translated_formula option * ((string * 'a) * thm)
+ val unmangled_const : string -> string * string fo_term list
val prepare_atp_problem :
Proof.context -> bool -> bool -> type_system -> bool -> term list -> term
-> (translated_formula option * ((string * 'a) * thm)) list
@@ -61,12 +63,11 @@
datatype type_system =
Tags of bool |
- Preds of bool |
- Const_Args |
+ Args |
+ Mangled |
No_Types
fun types_dangerous_types (Tags _) = true
- | types_dangerous_types (Preds _) = true
| types_dangerous_types _ = false
(* This is an approximation. If it returns "true" for a constant that isn't
@@ -82,12 +83,23 @@
fun needs_type_args thy type_sys s =
case type_sys of
Tags full_types => not full_types andalso is_overloaded thy s
- | Preds _ => is_overloaded thy s (* FIXME: could be more precise *)
- | Const_Args => is_overloaded thy s
+ | Args => is_overloaded thy s
+ | Mangled => true
| No_Types => false
+datatype type_arg_policy = No_Type_Args | Explicit_Type_Args | Mangled_Types
+
+fun type_arg_policy thy type_sys s =
+ if needs_type_args thy type_sys s then
+ if type_sys = Mangled then Mangled_Types else Explicit_Type_Args
+ else
+ No_Type_Args
+
fun num_atp_type_args thy type_sys s =
- if needs_type_args thy type_sys s then num_type_args thy s else 0
+ if type_arg_policy thy type_sys s = Explicit_Type_Args then
+ num_type_args thy s
+ else
+ 0
fun atp_type_literals_for_types type_sys Ts =
if type_sys = No_Types then [] else type_literals_for_types Ts
@@ -389,6 +401,42 @@
("c_implies", (2, ("c_fimplies", @{const_name Metis.fimplies}))),
("equal", (2, ("c_fequal", @{const_name Metis.fequal})))]
+(* We are crossing our fingers that it doesn't clash with anything else. *)
+val mangled_type_sep = "\000"
+
+fun mangled_combtyp f (CombTFree name) = f name
+ | mangled_combtyp f (CombTVar name) =
+ f name (* FIXME: shouldn't happen *)
+ (* raise Fail "impossible schematic type variable" *)
+ | mangled_combtyp f (CombType (name, tys)) =
+ "(" ^ commas (map (mangled_combtyp f) tys) ^ ")" ^ f name
+
+fun mangled_type_suffix f g tys =
+ fold_rev (curry (op ^) o g o prefix mangled_type_sep o mangled_combtyp f)
+ tys ""
+
+val parse_mangled_ident =
+ Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
+
+fun parse_mangled_type x =
+ ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")"
+ -- parse_mangled_ident >> (ATerm o swap)
+ || parse_mangled_ident >> (ATerm o rpair [])) x
+and parse_mangled_types x =
+ (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
+
+fun unmangled_type s =
+ s |> suffix ")" |> raw_explode
+ |> Scan.finite Symbol.stopper
+ (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
+ quote s)) parse_mangled_type))
+ |> fst
+
+fun unmangled_const s =
+ let val ss = space_explode mangled_type_sep s in
+ (hd ss, map unmangled_type (tl ss))
+ end
+
fun fo_term_for_combterm ctxt type_sys =
let
val thy = ProofContext.theory_of ctxt
@@ -411,11 +459,14 @@
case strip_prefix_and_unascii const_prefix s of
NONE => (name, ty_args)
| SOME s'' =>
- let
- val s'' = invert_const s''
- val ty_args =
- if needs_type_args thy type_sys s'' then ty_args else []
- in (name, ty_args) end)
+ let val s'' = invert_const s'' in
+ case type_arg_policy thy type_sys s'' of
+ No_Type_Args => (name, [])
+ | Explicit_Type_Args => (name, ty_args)
+ | Mangled_Types =>
+ ((s ^ mangled_type_suffix fst ascii_of ty_args,
+ s' ^ mangled_type_suffix snd I ty_args), [])
+ end)
| CombVar (name, _) => (name, [])
| CombApp _ => raise Fail "impossible \"CombApp\""
val t =
@@ -529,7 +580,9 @@
String.isPrefix class_prefix s then
16383 (* large number *)
else case strip_prefix_and_unascii const_prefix s of
- SOME s' => num_atp_type_args thy type_sys (invert_const s')
+ SOME s' =>
+ s' |> unmangled_const |> fst |> invert_const
+ |> num_atp_type_args thy type_sys
| NONE => 0)
| min_arity_of _ _ (SOME the_const_tab) s =
case Symtab.lookup the_const_tab s of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Apr 05 15:04:55 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Apr 05 15:15:33 2011 +0200
@@ -190,9 +190,6 @@
end)]
end
-val smart_full_type_sys = Tags true
-val smart_partial_type_sys = Const_Args
-
val infinity_time_in_secs = 60 * 60 * 24 * 365
val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
@@ -243,12 +240,13 @@
val type_sys =
case (lookup_string "type_sys", lookup_bool "full_types") of
("tags", full_types) => Tags full_types
- | ("preds", full_types) => Preds full_types
- | ("const_args", false) => Const_Args
+ | ("args", false) => Args
+ | ("mangled", false) => if monomorphize then Mangled else Args
| ("none", false) => No_Types
| (type_sys, full_types) =>
- if member (op =) ["const_args", "none", "smart"] type_sys then
- if full_types then smart_full_type_sys else smart_partial_type_sys
+ if member (op =) ["args", "mangled", "none", "smart"]
+ type_sys then
+ if full_types then Tags true else Args
else
error ("Unknown type system: " ^ quote type_sys ^ ".")
val explicit_apply = lookup_bool "explicit_apply"
--- a/src/Tools/Metis/README Tue Apr 05 15:04:55 2011 +0200
+++ b/src/Tools/Metis/README Tue Apr 05 15:15:33 2011 +0200
@@ -1,14 +1,12 @@
It's a good idea to update the Metis source code regularly, to benefit
from the latest developments, to avoid a permanent fork, and to detect
Metis problems early. This file explains how to update the source code
-for Metis with the latest Metis package. The procedure is
-unfortunately somewhat involved and frustrating, and hopefully
-temporary.
+for Metis with the latest Metis package.
1. The files "Makefile" and "script/mlpp" and the directory "src/"
were initially copied from Joe Hurd's official Metis package. The
package that was used when these notes where written was Metis 2.3
- (16 Sept. 2010).
+ (29 Dec. 2010).
2. The license in each source file will probably not be something we
can use in Isabelle. The "fix_metis_license" script can be run to
@@ -24,7 +22,7 @@
files. The ultimate way to track them down is to use Mercurial.
The command
- hg diff -rcffceed8e7fa: src
+ hg diff -r90c7c97f0c21: src
should do the trick. You might need to specify a different
revision number if somebody updated the Metis sources without
@@ -55,4 +53,4 @@
Good luck!
Jasmin Blanchette
- 17 Sept. 2010
+ 23 March 2011