--- a/src/HOL/IsaMakefile Tue Dec 21 15:15:55 2010 +0100
+++ b/src/HOL/IsaMakefile Tue Dec 21 15:16:27 2010 +0100
@@ -1314,7 +1314,7 @@
Mirabelle/Tools/mirabelle_quickcheck.ML \
Mirabelle/Tools/mirabelle_refute.ML \
Mirabelle/Tools/mirabelle_sledgehammer.ML \
- Mirabelle/Tools/sledgehammer_tactic.ML
+ Mirabelle/Tools/sledgehammer_tactics.ML
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
--- a/src/HOL/Mirabelle/Mirabelle.thy Tue Dec 21 15:15:55 2010 +0100
+++ b/src/HOL/Mirabelle/Mirabelle.thy Tue Dec 21 15:16:27 2010 +0100
@@ -3,8 +3,9 @@
*)
theory Mirabelle
-imports Pure
+imports Sledgehammer
uses "Tools/mirabelle.ML"
+ "Tools/sledgehammer_tactics.ML"
begin
(* no multithreading, no parallel proofs *) (* FIXME *)
--- a/src/HOL/Mirabelle/Mirabelle_Test.thy Tue Dec 21 15:15:55 2010 +0100
+++ b/src/HOL/Mirabelle/Mirabelle_Test.thy Tue Dec 21 15:16:27 2010 +0100
@@ -13,7 +13,6 @@
"Tools/mirabelle_refute.ML"
"Tools/mirabelle_sledgehammer.ML"
"Tools/mirabelle_sledgehammer_filter.ML"
- "Tools/sledgehammer_tactic.ML"
begin
text {*
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Dec 21 15:15:55 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Dec 21 15:16:27 2010 +0100
@@ -13,6 +13,7 @@
val minimizeK = "minimize"
val minimize_timeoutK = "minimize_timeout"
val metis_ftK = "metis_ft"
+val reconstructorK = "reconstructor"
fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "
@@ -331,10 +332,13 @@
type locality = Sledgehammer_Filter.locality
(* hack *)
-fun reconstructor_from_msg msg =
- if String.isSubstring "metisFT" msg then "metisFT"
- else if String.isSubstring "metis" msg then "metis"
- else "smt"
+fun reconstructor_from_msg args msg =
+ (case AList.lookup (op =) args reconstructorK of
+ SOME name => name
+ | NONE =>
+ if String.isSubstring "metisFT" msg then "metisFT"
+ else if String.isSubstring "metis" msg then "metis"
+ else "smt")
local
@@ -445,7 +449,7 @@
change_data id (inc_sh_max_lems (length names));
change_data id (inc_sh_time_isa time_isa);
change_data id (inc_sh_time_prover time_prover);
- reconstructor := reconstructor_from_msg msg;
+ reconstructor := reconstructor_from_msg args msg;
named_thms := SOME (map_filter get_thms names);
log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
@@ -487,7 +491,7 @@
change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
if length named_thms' = n0
then log (minimize_tag id ^ "already minimal")
- else (reconstructor := reconstructor_from_msg msg;
+ else (reconstructor := reconstructor_from_msg args msg;
named_thms := SOME named_thms';
log (minimize_tag id ^ "succeeded:\n" ^ msg))
)
@@ -499,7 +503,11 @@
({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
let
fun do_reconstructor thms ctxt =
- (if !reconstructor = "smt" then
+ (if !reconstructor = "sledgehammer_tac" then
+ (fn ctxt => fn thms =>
+ Method.insert_tac thms THEN'
+ Sledgehammer_Tactics.sledgehammer_as_unsound_oracle_tac ctxt)
+ else if !reconstructor = "smt" then
SMT_Solver.smt_tac
else if full orelse !reconstructor = "metisFT" then
Metis_Tactics.metisFT_tac
--- a/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML Tue Dec 21 15:15:55 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,98 +0,0 @@
-(* Title: sledgehammer_tactics.ML
- Author: Jasmin Blanchette, TU Muenchen
- Copyright 2010
-
-Sledgehammer as a tactic.
-*)
-
-signature SLEDGEHAMMER_TACTICS =
-sig
- val sledgehammer_with_metis_tac : Proof.context -> int -> tactic
- val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic
-end;
-
-structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
-struct
-
-fun run_atp force_full_types timeout i n ctxt goal name =
- let
- val chained_ths = [] (* a tactic has no chained ths *)
- val params as {type_sys, relevance_thresholds, max_relevant, ...} =
- ((if force_full_types then [("full_types", "true")] else [])
- @ [("timeout", Int.toString (Time.toSeconds timeout))])
- @ [("overlord", "true")]
- |> Sledgehammer_Isar.default_params ctxt
- val prover = Sledgehammer_Provers.get_prover ctxt false name
- val default_max_relevant =
- Sledgehammer_Provers.default_max_relevant_for_prover ctxt name
- val is_built_in_const =
- Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
- val relevance_fudge =
- Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
- val relevance_override = {add = [], del = [], only = false}
- val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
- val no_dangerous_types =
- Sledgehammer_ATP_Translate.types_dangerous_types type_sys
- val facts =
- Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types
- relevance_thresholds
- (the_default default_max_relevant max_relevant) is_built_in_const
- relevance_fudge relevance_override chained_ths hyp_ts concl_t
- (* Check for constants other than the built-in HOL constants. If none of
- them appear (as should be the case for TPTP problems, unless "auto" or
- "simp" already did its "magic"), we can skip the relevance filter. *)
- val pure_goal =
- not (exists_Const (fn (s, _) => String.isSubstring "." s andalso
- not (String.isSubstring "HOL" s))
- (prop_of goal))
- val problem =
- {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
- facts = map Sledgehammer_Provers.Untranslated_Fact facts,
- smt_head = NONE}
- in
- (case prover params (K "") problem of
- {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
- | _ => NONE)
- handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
- end
-
-fun to_period ("." :: _) = []
- | to_period ("" :: ss) = to_period ss
- | to_period (s :: ss) = s :: to_period ss
- | to_period [] = []
-
-val atp = "e" (* or "vampire" *)
-
-fun thms_of_name ctxt name =
- let
- val lex = Keyword.get_lexicons
- val get = maps (ProofContext.get_fact ctxt o fst)
- in
- Source.of_string name
- |> Symbol.source
- |> Token.source {do_recover=SOME false} lex Position.start
- |> Token.source_proper
- |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
- |> Source.exhaust
- end
-
-fun sledgehammer_with_metis_tac ctxt i th =
- let
- val timeout = Time.fromSeconds 30
- in
- case run_atp false timeout i i ctxt th atp of
- SOME facts => Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th
- | NONE => Seq.empty
- end
-
-fun sledgehammer_as_oracle_tac ctxt i th =
- let
- val thy = ProofContext.theory_of ctxt
- val timeout = Time.fromSeconds 30
- val xs = run_atp true timeout i i ctxt th atp
- in
- if is_some xs then Skip_Proof.cheat_tac thy th
- else Seq.empty
- end
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML Tue Dec 21 15:16:27 2010 +0100
@@ -0,0 +1,101 @@
+(* Title: sledgehammer_tactics.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2010
+
+Sledgehammer as a tactic.
+*)
+
+signature SLEDGEHAMMER_TACTICS =
+sig
+ val sledgehammer_with_metis_tac : Proof.context -> int -> tactic
+ val sledgehammer_as_unsound_oracle_tac : Proof.context -> int -> tactic
+ val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic
+end;
+
+structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
+struct
+
+fun run_atp force_full_types timeout i n ctxt goal name =
+ let
+ val chained_ths = [] (* a tactic has no chained ths *)
+ val params as {type_sys, relevance_thresholds, max_relevant, ...} =
+ ((if force_full_types then [("full_types", "true")] else [])
+ @ [("timeout", Int.toString (Time.toSeconds timeout))])
+ (* @ [("overlord", "true")] *)
+ |> Sledgehammer_Isar.default_params ctxt
+ val prover = Sledgehammer_Provers.get_prover ctxt false name
+ val default_max_relevant =
+ Sledgehammer_Provers.default_max_relevant_for_prover ctxt name
+ val is_built_in_const =
+ Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
+ val relevance_fudge =
+ Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
+ val relevance_override = {add = [], del = [], only = false}
+ val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
+ val no_dangerous_types =
+ Sledgehammer_ATP_Translate.types_dangerous_types type_sys
+ val facts =
+ Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types
+ relevance_thresholds
+ (the_default default_max_relevant max_relevant) is_built_in_const
+ relevance_fudge relevance_override chained_ths hyp_ts concl_t
+ (* Check for constants other than the built-in HOL constants. If none of
+ them appear (as should be the case for TPTP problems, unless "auto" or
+ "simp" already did its "magic"), we can skip the relevance filter. *)
+ val pure_goal =
+ not (exists_Const (fn (s, _) => String.isSubstring "." s andalso
+ not (String.isSubstring "HOL" s))
+ (prop_of goal))
+ val problem =
+ {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
+ facts = map Sledgehammer_Provers.Untranslated_Fact facts,
+ smt_head = NONE}
+ in
+ (case prover params (K "") problem of
+ {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
+ | _ => NONE)
+ handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
+ end
+
+fun to_period ("." :: _) = []
+ | to_period ("" :: ss) = to_period ss
+ | to_period (s :: ss) = s :: to_period ss
+ | to_period [] = []
+
+val atp = "vampire" (* or "e" or "spass" etc. *)
+
+fun thms_of_name ctxt name =
+ let
+ val lex = Keyword.get_lexicons
+ val get = maps (ProofContext.get_fact ctxt o fst)
+ in
+ Source.of_string name
+ |> Symbol.source
+ |> Token.source {do_recover=SOME false} lex Position.start
+ |> Token.source_proper
+ |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
+ |> Source.exhaust
+ end
+
+fun sledgehammer_with_metis_tac ctxt i th =
+ let
+ val timeout = Time.fromSeconds 30
+ in
+ case run_atp false timeout i i ctxt th atp of
+ SOME facts =>
+ Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th
+ | NONE => Seq.empty
+ end
+
+fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val timeout = Time.fromSeconds 30
+ val xs = run_atp force_full_types timeout i i ctxt th atp
+ in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
+
+val sledgehammer_as_unsound_oracle_tac =
+ generic_sledgehammer_as_oracle_tac false
+val sledgehammer_as_oracle_tac = generic_sledgehammer_as_oracle_tac true
+
+end;
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Tue Dec 21 15:15:55 2010 +0100
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Tue Dec 21 15:16:27 2010 +0100
@@ -82,7 +82,7 @@
print SETUP_FILE "setup {* Mirabelle_$name.invoke [";
my $sep = "";
foreach (split(/,/, $settings_str)) {
- if (m/\s*(.*)\s*=\s*(.*)\s*/) {
+ if (m/\s*([^=]*)\s*=\s*(.*)\s*/) {
print SETUP_FILE "$sep(\"$1\", \"$2\")";
$sep = ", ";
}
--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy Tue Dec 21 15:15:55 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy Tue Dec 21 15:16:27 2010 +0100
@@ -51,7 +51,8 @@
theorem safe: "s \<in> reach \<Longrightarrow> safe s r \<Longrightarrow> g \<in> isin s r \<Longrightarrow> owns s r = Some g"
nitpick [card room = 1, card guest = 2, card "guest option" = 3,
- card key = 4, card state = 6, expect = genuine]
+ card key = 4, card state = 6, show_consts, format = 2,
+ expect = genuine]
(* nitpick [card room = 1, card guest = 2, expect = genuine] *)
oops
--- a/src/HOL/Tools/SMT/smt_builtin.ML Tue Dec 21 15:15:55 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_builtin.ML Tue Dec 21 15:16:27 2010 +0100
@@ -27,8 +27,8 @@
(string * typ) * bfunr option bfun -> Context.generic -> Context.generic
val add_builtin_fun': SMT_Utils.class -> term * string -> Context.generic ->
Context.generic
- val add_builtin_fun_ext: (string * typ) * bool bfun -> Context.generic ->
- Context.generic
+ val add_builtin_fun_ext: (string * typ) * term list bfun ->
+ Context.generic -> Context.generic
val add_builtin_fun_ext': string * typ -> Context.generic -> Context.generic
val add_builtin_fun_ext'': string -> Context.generic -> Context.generic
val dest_builtin_fun: Proof.context -> string * typ -> term list ->
@@ -39,6 +39,8 @@
val dest_builtin_conn: Proof.context -> string * typ -> term list ->
bfunr option
val dest_builtin: Proof.context -> string * typ -> term list -> bfunr option
+ val dest_builtin_ext: Proof.context -> string * typ -> term list ->
+ term list option
val is_builtin_fun: Proof.context -> string * typ -> term list -> bool
val is_builtin_fun_ext: Proof.context -> string * typ -> term list -> bool
end
@@ -148,7 +150,7 @@
structure Builtin_Funcs = Generic_Data
(
- type T = (bool bfun, bfunr option bfun) btab
+ type T = (term list bfun, bfunr option bfun) btab
val empty = Symtab.empty
val extend = I
val merge = merge_btab
@@ -167,8 +169,7 @@
fun add_builtin_fun_ext ((n, T), f) =
Builtin_Funcs.map (insert_btab SMT_Utils.basicC n T (Ext f))
-fun add_builtin_fun_ext' c =
- add_builtin_fun_ext (c, fn _ => fn _ => fn _ => true)
+fun add_builtin_fun_ext' c = add_builtin_fun_ext (c, fn _ => fn _ => I)
fun add_builtin_fun_ext'' n context =
let val thy = Context.theory_of context
@@ -210,12 +211,18 @@
| NONE => dest_builtin_fun ctxt c ts)
end
+fun dest_builtin_fun_ext ctxt (c as (_, T)) ts =
+ (case lookup_builtin_fun ctxt c of
+ SOME (_, Int f) => f ctxt T ts |> Option.map (fn (_, _, us, _) => us)
+ | SOME (_, Ext f) => SOME (f ctxt T ts)
+ | NONE => NONE)
+
+fun dest_builtin_ext ctxt c ts =
+ if is_builtin_num_ext ctxt (Term.list_comb (Const c, ts)) then SOME []
+ else dest_builtin_fun_ext ctxt c ts
+
fun is_builtin_fun ctxt c ts = is_some (dest_builtin_fun ctxt c ts)
-fun is_builtin_fun_ext ctxt (c as (_, T)) ts =
- (case lookup_builtin_fun ctxt c of
- SOME (_, Int f) => is_some (f ctxt T ts)
- | SOME (_, Ext f) => f ctxt T ts
- | NONE => false)
+fun is_builtin_fun_ext ctxt c ts = is_some (dest_builtin_fun_ext ctxt c ts)
end
--- a/src/HOL/Tools/hologic.ML Tue Dec 21 15:15:55 2010 +0100
+++ b/src/HOL/Tools/hologic.ML Tue Dec 21 15:16:27 2010 +0100
@@ -8,7 +8,7 @@
sig
val typeS: sort
val typeT: typ
- val mk_id: typ -> term
+ val id_const: typ -> term
val mk_comp: term * term -> term
val boolN: string
val boolT: typ
@@ -146,7 +146,7 @@
(* functions *)
-fun mk_id T = Const ("Fun.id", T --> T);
+fun id_const T = Const ("Fun.id", T --> T);
fun mk_comp (f, g) =
let
--- a/src/Pure/ML-Systems/polyml_common.ML Tue Dec 21 15:15:55 2010 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML Tue Dec 21 15:16:27 2010 +0100
@@ -3,6 +3,8 @@
Compatibility file for Poly/ML -- common part for 5.x.
*)
+fun op before (a, _: unit) = a;
+
exception Interrupt = SML90.Interrupt;
use "General/exn.ML";
--- a/src/Pure/System/isabelle_system.ML Tue Dec 21 15:15:55 2010 +0100
+++ b/src/Pure/System/isabelle_system.ML Tue Dec 21 15:16:27 2010 +0100
@@ -65,13 +65,13 @@
fun with_tmp_file name f =
let val path = fresh_path name
- in Exn.release (Exn.capture f path before try File.rm path) end;
+ in Exn.release (Exn.capture f path before ignore (try File.rm path)) end;
fun with_tmp_dir name f =
let
val path = fresh_path name;
val _ = mkdirs path;
- in Exn.release (Exn.capture f path before try rm_tree path) end;
+ in Exn.release (Exn.capture f path before ignore (try rm_tree path)) end;
end;
--- a/src/Tools/subtyping.ML Tue Dec 21 15:15:55 2010 +0100
+++ b/src/Tools/subtyping.ML Tue Dec 21 15:16:27 2010 +0100
@@ -6,7 +6,7 @@
signature SUBTYPING =
sig
- datatype variance = COVARIANT | CONTRAVARIANT | INVARIANT
+ datatype variance = COVARIANT | CONTRAVARIANT | INVARIANT | INVARIANT_TO of typ;
val coercion_enabled: bool Config.T
val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) ->
term list -> term list
@@ -21,7 +21,7 @@
(** coercions data **)
-datatype variance = COVARIANT | CONTRAVARIANT | INVARIANT
+datatype variance = COVARIANT | CONTRAVARIANT | INVARIANT | INVARIANT_TO of typ;
datatype data = Data of
{coes: term Symreltab.table, (*coercions table*)
@@ -83,9 +83,11 @@
| sort_of _ = NONE;
val is_typeT = fn (Type _) => true | _ => false;
+val is_stypeT = fn (Type (_, [])) => true | _ => false;
val is_compT = fn (Type (_, _ :: _)) => true | _ => false;
val is_freeT = fn (TFree _) => true | _ => false;
val is_fixedvarT = fn (TVar (xi, _)) => not (Type_Infer.is_param xi) | _ => false;
+val is_funtype = fn (Type ("fun", [_, _])) => true | _ => false;
(* unification *)
@@ -205,10 +207,6 @@
fun unif_failed msg =
"Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n";
-
-fun subtyping_err_appl_msg ctxt msg tye bs t T u U () =
- let val ([t', u'], [T', U']) = prep_output ctxt tye bs [t, u] [T, U]
- in msg ^ Type.appl_error (Syntax.pp ctxt) t' T' u' U' ^ "\n" end;
fun err_appl_msg ctxt msg tye bs t T u U () =
let val ([t', u'], [T', U']) = prep_output ctxt tye bs [t, u] [T, U]
@@ -264,7 +262,7 @@
val U = Type_Infer.mk_param idx [];
val V = Type_Infer.mk_param (idx + 1) [];
val tye_idx''= strong_unify ctxt (U --> V, T) (tye, idx + 2)
- handle NO_UNIFIER (msg, tye') => error (gen_msg err msg);
+ handle NO_UNIFIER (msg, _) => error (gen_msg err msg);
val error_pack = (bs, t $ u, U, V, U');
in (V, tye_idx'', ((U', U), error_pack) :: cs'') end;
in
@@ -291,12 +289,15 @@
(case pairself f (fst c) of
(false, false) => apsnd (cons c) (split_cs f cs)
| _ => apfst (cons c) (split_cs f cs));
+
+ fun unify_list (T :: Ts) tye_idx =
+ fold (fn U => fn tye_idx' => strong_unify ctxt (T, U) tye_idx') Ts tye_idx;
(* check whether constraint simplification will terminate using weak unification *)
- val _ = fold (fn (TU, error_pack) => fn tye_idx =>
- weak_unify ctxt TU tye_idx handle NO_UNIFIER (msg, tye) =>
+ val _ = fold (fn (TU, _) => fn tye_idx =>
+ weak_unify ctxt TU tye_idx handle NO_UNIFIER (msg, _) =>
error (gen_msg err ("weak unification of subtype constraints fails\n" ^ msg))) cs tye_idx;
@@ -315,9 +316,14 @@
(case variance of
COVARIANT => (constraint :: cs, tye_idx)
| CONTRAVARIANT => (swap constraint :: cs, tye_idx)
+ | INVARIANT_TO T => (cs, unify_list [T, fst constraint, snd constraint] tye_idx
+ handle NO_UNIFIER (msg, _) =>
+ err_list ctxt (gen_msg err
+ "failed to unify invariant arguments w.r.t. to the known map function")
+ (fst tye_idx) Ts)
| INVARIANT => (cs, strong_unify ctxt constraint tye_idx
- handle NO_UNIFIER (msg, tye) =>
- error (gen_msg err ("failed to unify invariant arguments\n" ^ msg))));
+ handle NO_UNIFIER (msg, _) =>
+ error (gen_msg err ("failed to unify invariant arguments" ^ msg))));
val (new, (tye', idx')) = apfst (fn cs => (cs ~~ replicate (length cs) error_pack))
(fold new_constraints (arg_var ~~ (Ts ~~ Us)) ([], (tye, idx)));
val test_update = is_compT orf is_freeT orf is_fixedvarT;
@@ -343,7 +349,7 @@
simplify done' ((new, error_pack) :: todo') (tye', idx + n)
end
(*TU is a pair of a parameter and a free/fixed variable*)
- and eliminate TU error_pack done todo tye idx =
+ and eliminate TU done todo tye idx =
let
val [TVar (xi, S)] = filter Type_Infer.is_paramT TU;
val [T] = filter_out Type_Infer.is_paramT TU;
@@ -376,7 +382,7 @@
if T = U then simplify done todo tye_idx
else if exists (is_freeT orf is_fixedvarT) [T, U] andalso
exists Type_Infer.is_paramT [T, U]
- then eliminate [T, U] error_pack done todo tye idx
+ then eliminate [T, U] done todo tye idx
else if exists (is_freeT orf is_fixedvarT) [T, U]
then error (gen_msg err "not eliminated free/fixed variables")
else simplify (((T, U), error_pack) :: done) todo tye_idx);
@@ -402,9 +408,6 @@
cs'
end;
- fun unify_list (T :: Ts) tye_idx =
- fold (fn U => fn tye_idx' => strong_unify ctxt (T, U) tye_idx') Ts tye_idx;
-
(*styps stands either for supertypes or for subtypes of a type T
in terms of the subtype-relation (excluding T itself)*)
fun styps super T =
@@ -467,7 +470,7 @@
val (tye, idx) =
fold
(fn cycle => fn tye_idx' => (unify_list cycle tye_idx'
- handle NO_UNIFIER (msg, tye) =>
+ handle NO_UNIFIER (msg, _) =>
err_bound ctxt
(gen_msg err ("constraint cycle not unifiable" ^ msg)) (fst tye_idx)
(find_cycle_packs cycle)))
@@ -572,7 +575,7 @@
in
fold
(fn Ts => fn tye_idx' => unify_list Ts tye_idx'
- handle NO_UNIFIER (msg, tye) => err_list ctxt (gen_msg err msg) (fst tye_idx) Ts)
+ handle NO_UNIFIER (msg, _) => err_list ctxt (gen_msg err msg) (fst tye_idx) Ts)
to_unify tye_idx
end;
@@ -605,8 +608,9 @@
fun inst t Ts =
Term.subst_vars
(((Term.add_tvar_namesT (fastype_of t) []) ~~ rev Ts), []) t;
- fun sub_co (COVARIANT, TU) = gen_coercion ctxt tye TU
- | sub_co (CONTRAVARIANT, TU) = gen_coercion ctxt tye (swap TU);
+ fun sub_co (COVARIANT, TU) = SOME (gen_coercion ctxt tye TU)
+ | sub_co (CONTRAVARIANT, TU) = SOME (gen_coercion ctxt tye (swap TU))
+ | sub_co (INVARIANT_TO T, _) = NONE;
fun ts_of [] = []
| ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs);
in
@@ -614,7 +618,7 @@
NONE => raise Fail ("No map function for " ^ a ^ " known")
| SOME tmap =>
let
- val used_coes = map sub_co ((snd tmap) ~~ (Ts ~~ Us));
+ val used_coes = map_filter sub_co ((snd tmap) ~~ (Ts ~~ Us));
in
Term.list_comb
(inst (fst tmap) (ts_of (map fastype_of used_coes)), used_coes)
@@ -735,36 +739,39 @@
val ctxt = Context.proof_of context;
val t = singleton (Variable.polymorphic ctxt) raw_t;
- fun err_str () = "\n\nthe general type signature for a map function is" ^
- "\nf1 => f2 => ... => fn => C [x1, ..., xn] => C [x1, ..., xn]" ^
+ fun err_str t = "\n\nThe provided function has the type\n" ^
+ Syntax.string_of_typ ctxt (fastype_of t) ^
+ "\n\nThe general type signature of a map function is" ^
+ "\nf1 => f2 => ... => fn => C [x1, ..., xn] => C [y1, ..., yn]" ^
"\nwhere C is a constructor and fi is of type (xi => yi) or (yi => xi)";
-
+
+ val ((fis, T1), T2) = apfst split_last (strip_type (fastype_of t))
+ handle Empty => error ("Not a proper map function:" ^ err_str t);
+
fun gen_arg_var ([], []) = []
| gen_arg_var ((T, T') :: Ts, (U, U') :: Us) =
- if T = U andalso T' = U' then COVARIANT :: gen_arg_var (Ts, Us)
+ if U = U' then
+ if is_stypeT U then INVARIANT_TO U :: gen_arg_var ((T, T') :: Ts, Us)
+ else error ("Invariant xi and yi should be base types:" ^ err_str t)
+ else if T = U andalso T' = U' then COVARIANT :: gen_arg_var (Ts, Us)
else if T = U' andalso T' = U then CONTRAVARIANT :: gen_arg_var (Ts, Us)
- else error ("Functions do not apply to arguments correctly:" ^ err_str ())
- | gen_arg_var (_, _) =
- error ("Different numbers of functions and arguments\n" ^ err_str ());
+ else error ("Functions do not apply to arguments correctly:" ^ err_str t)
+ | gen_arg_var (_, Ts) =
+ if forall (op = andf is_stypeT o fst) Ts
+ then map (INVARIANT_TO o fst) Ts
+ else error ("Different numbers of functions and variant arguments\n" ^ err_str t);
- (* TODO: This function is only needed to introde the fun type map
- function: "% f g h . g o h o f". There must be a better solution. *)
- fun balanced (Type (_, [])) (Type (_, [])) = true
- | balanced (Type (a, Ts)) (Type (b, Us)) =
- a = b andalso forall I (map2 balanced Ts Us)
- | balanced (TFree _) (TFree _) = true
- | balanced (TVar _) (TVar _) = true
- | balanced _ _ = false;
+ (*retry flag needed to adjust the type lists, when given a map over type constructor fun*)
+ fun check_map_fun fis (Type (C1, Ts)) (Type (C2, Us)) retry =
+ if C1 = C2 andalso not (null fis) andalso forall is_funtype fis
+ then ((map dest_funT fis, Ts ~~ Us), C1)
+ else error ("Not a proper map function:" ^ err_str t)
+ | check_map_fun fis T1 T2 true =
+ let val (fis', T') = split_last fis
+ in check_map_fun fis' T' (T1 --> T2) false end
+ | check_map_fun _ _ _ _ = error ("Not a proper map function:" ^ err_str t);
- fun check_map_fun (pairs, []) (Type ("fun", [T as Type (C, Ts), U as Type (_, Us)])) =
- if balanced T U
- then ((pairs, Ts ~~ Us), C)
- else if C = "fun"
- then check_map_fun (pairs @ [(hd Ts, hd (tl Ts))], []) U
- else error ("Not a proper map function:" ^ err_str ())
- | check_map_fun _ _ = error ("Not a proper map function:" ^ err_str ());
-
- val res = check_map_fun ([], []) (fastype_of t);
+ val res = check_map_fun fis T1 T2 true;
val res_av = gen_arg_var (fst res);
in
map_tmaps (Symtab.update (snd res, (t, res_av))) context