# HG changeset patch # User wenzelm # Date 1302009333 -7200 # Node ID e48baf91aeabfe1afe8ff93fa19b0695b2bd3450 # Parent d53dccb38dd1cb93e511e8567a81d8fabd5aaefe# Parent cb650789f2f0f6bcc98d43ecd37b74e63cc9c2c9 merged diff -r cb650789f2f0 -r e48baf91aeab NEWS --- 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. diff -r cb650789f2f0 -r e48baf91aeab doc-src/Sledgehammer/sledgehammer.tex --- 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} diff -r cb650789f2f0 -r e48baf91aeab src/HOL/Fun.thy --- 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]: "\(\f. f ` A = Pow A)" proof clarify fix f assume "f ` A = Pow A" hence *: "Pow A \ f ` A" by blast diff -r cb650789f2f0 -r e48baf91aeab src/HOL/Library/Code_Char.thy --- 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 diff -r cb650789f2f0 -r e48baf91aeab src/HOL/Quickcheck_Exhaustive.thy --- 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 \ bool) \ code_numeral \ bool" - -instantiation nat :: bounded_forall -begin - -fun bounded_forall_nat :: "(nat => bool) => code_numeral => bool" -where - "bounded_forall P d = ((P 0) \ (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" diff -r cb650789f2f0 -r e48baf91aeab src/HOL/Tools/ATP/atp_problem.ML --- 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 diff -r cb650789f2f0 -r e48baf91aeab src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- 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)) diff -r cb650789f2f0 -r e48baf91aeab src/HOL/Tools/Quickcheck/quickcheck_common.ML --- 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; diff -r cb650789f2f0 -r e48baf91aeab src/HOL/Tools/Quickcheck/random_generators.ML --- 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)); diff -r cb650789f2f0 -r e48baf91aeab src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- 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 diff -r cb650789f2f0 -r e48baf91aeab src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- 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 diff -r cb650789f2f0 -r e48baf91aeab src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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" diff -r cb650789f2f0 -r e48baf91aeab src/Tools/Metis/README --- 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