--- a/src/HOL/Tools/SMT/smt_builtin.ML Tue Dec 21 13:57:35 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_builtin.ML Tue Dec 21 14:18:45 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/Pure/ML-Systems/polyml_common.ML Tue Dec 21 13:57:35 2010 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML Tue Dec 21 14:18:45 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 13:57:35 2010 +0100
+++ b/src/Pure/System/isabelle_system.ML Tue Dec 21 14:18:45 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/Code/code_preproc.ML Tue Dec 21 13:57:35 2010 +0100
+++ b/src/Tools/Code/code_preproc.ML Tue Dec 21 14:18:45 2010 +0100
@@ -29,9 +29,9 @@
val dynamic_value: theory -> ((term -> term) -> 'a -> 'a)
-> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
val static_conv: theory -> string list
- -> (code_algebra -> code_graph -> theory -> (string * sort) list -> term -> conv) -> conv
+ -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list
- -> (code_algebra -> code_graph -> theory -> (string * sort) list -> term -> 'a) -> term -> 'a
+ -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
val setup: theory -> theory
end
@@ -490,7 +490,7 @@
fun static_conv thy consts conv =
let
val (algebra, eqngr) = obtain true thy consts [];
- val conv' = conv algebra eqngr thy;
+ val conv' = conv algebra eqngr;
in
no_variables_conv ((preprocess_conv thy)
then_conv (fn ct => uncurry conv' (dest_cterm ct) ct)
@@ -504,7 +504,7 @@
in
preprocess_term thy
#-> (fn resubst => fn t => t
- |> evaluator' thy (Term.add_tfrees t [])
+ |> evaluator' (Term.add_tfrees t [])
|> postproc (postprocess_term thy o resubst))
end;
--- a/src/Tools/Code/code_runtime.ML Tue Dec 21 13:57:35 2010 +0100
+++ b/src/Tools/Code/code_runtime.ML Tue Dec 21 14:18:45 2010 +0100
@@ -86,25 +86,14 @@
val ctxt = ProofContext.init_global thy;
in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end;
-fun obtain_serializer thy some_target = Code_Target.produce_code_for thy
- (the_default target some_target) NONE "Code" [];
+fun obtain_evaluator thy some_target = Code_Target.evaluator thy (the_default target some_target);
-fun base_evaluator cookie serializer (naming : Code_Thingol.naming) thy program ((vs, ty), t) deps args =
+fun evaluation cookie thy evaluator vs_t args =
let
val ctxt = ProofContext.init_global thy;
- val _ = if Code_Thingol.contains_dict_var t then
- error "Term to be evaluated contains free dictionaries" else ();
- val v' = Name.variant (map fst vs) "a";
- val vs' = (v', []) :: vs;
- val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty];
- val value_name = "Value.value.value"
- val program' = program
- |> Graph.new_node (value_name,
- Code_Thingol.Fun (Term.dummy_patternN, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
- |> fold (curry Graph.add_edge value_name) deps;
- val (program_code, [SOME value_name']) = serializer naming program' [value_name];
+ val (program_code, value_name) = evaluator vs_t;
val value_code = space_implode " "
- (value_name' :: "()" :: map (enclose "(" ")") args);
+ (value_name :: "()" :: map (enclose "(" ")") args);
in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end;
fun partiality_as_none e = SOME (Exn.release e)
@@ -119,7 +108,7 @@
then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term_global thy t))
else ()
fun evaluator naming program ((_, vs_ty), t) deps =
- base_evaluator cookie (obtain_serializer thy some_target) naming thy program (vs_ty, t) deps args;
+ evaluation cookie thy (obtain_evaluator thy some_target naming program deps) (vs_ty, t) args;
in Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t end;
fun dynamic_value_strict cookie thy some_target postproc t args =
@@ -128,18 +117,20 @@
fun dynamic_value cookie thy some_target postproc t args =
partiality_as_none (dynamic_value_exn cookie thy some_target postproc t args);
-fun static_value_exn cookie thy some_target postproc consts =
+fun static_evaluator cookie thy some_target naming program consts' =
let
- val serializer = obtain_serializer thy some_target;
- fun evaluator naming program thy ((_, vs_ty), t) deps =
- base_evaluator cookie serializer naming thy program (vs_ty, t) deps [];
- in Code_Thingol.static_value thy (Exn.map_result o postproc) consts evaluator o reject_vars thy end;
+ val evaluator = obtain_evaluator thy some_target naming program consts'
+ in fn ((_, vs_ty), t) => fn _ => evaluation cookie thy evaluator (vs_ty, t) [] end;
-fun static_value_strict cookie thy some_target postproc consts t =
- Exn.release (static_value_exn cookie thy some_target postproc consts t);
+fun static_value_exn cookie thy some_target postproc consts =
+ Code_Thingol.static_value thy (Exn.map_result o postproc) consts
+ (static_evaluator cookie thy some_target) o reject_vars thy;
-fun static_value cookie thy some_target postproc consts t =
- partiality_as_none (static_value_exn cookie thy some_target postproc consts t);
+fun static_value_strict cookie thy some_target postproc consts =
+ Exn.release o static_value_exn cookie thy some_target postproc consts;
+
+fun static_value cookie thy some_target postproc consts =
+ partiality_as_none o static_value_exn cookie thy some_target postproc consts;
(* evaluation for truth or nothing *)
@@ -154,14 +145,16 @@
val reject_vars = fn thy => tap (reject_vars thy o Thm.term_of);
-fun check_holds serializer naming thy program vs_t deps ct =
+local
+
+fun check_holds thy evaluator vs_t deps ct =
let
val t = Thm.term_of ct;
val _ = if fastype_of t <> propT
then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t)
else ();
val iff = Thm.cterm_of thy (Term.Const ("==", propT --> propT --> propT));
- val result = case partiality_as_none (base_evaluator truth_cookie serializer naming thy program vs_t deps [])
+ val result = case partiality_as_none (evaluation truth_cookie thy evaluator vs_t [])
of SOME Holds => true
| _ => false;
in
@@ -170,23 +163,24 @@
val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
(Thm.add_oracle (Binding.name "holds_by_evaluation",
- fn (serializer, naming, thy, program, vs_t, deps, ct) => check_holds serializer naming thy program vs_t deps ct)));
+ fn (thy, evaluator, vs_t, deps, ct) => check_holds thy evaluator vs_t deps ct)));
-fun check_holds_oracle serializer naming thy program ((_, vs_ty), t) deps ct =
- raw_check_holds_oracle (serializer, naming, thy, program, (vs_ty, t), deps, ct);
+fun check_holds_oracle thy evaluator ((_, vs_ty), t) deps ct =
+ raw_check_holds_oracle (thy, evaluator, (vs_ty, t), deps, ct);
+
+in
fun dynamic_holds_conv thy = Code_Thingol.dynamic_conv thy
- (fn naming => check_holds_oracle (obtain_serializer thy NONE) naming thy)
- o reject_vars thy;
+ (fn naming => fn program => fn vs_t => fn deps =>
+ check_holds_oracle thy (obtain_evaluator thy NONE naming program deps) vs_t deps)
+ o reject_vars thy;
-fun static_holds_conv thy consts =
- let
- val serializer = obtain_serializer thy NONE;
- in
- Code_Thingol.static_conv thy consts
- (fn naming => fn program => fn thy => check_holds_oracle serializer naming thy program)
- o reject_vars thy
- end;
+fun static_holds_conv thy consts = Code_Thingol.static_conv thy consts
+ (fn naming => fn program => fn consts' =>
+ check_holds_oracle thy (obtain_evaluator thy NONE naming program consts'))
+ o reject_vars thy;
+
+end; (*local*)
(** instrumentalization **)
--- a/src/Tools/Code/code_simp.ML Tue Dec 21 13:57:35 2010 +0100
+++ b/src/Tools/Code/code_simp.ML Tue Dec 21 14:18:45 2010 +0100
@@ -68,7 +68,7 @@
fun static_conv thy some_ss consts =
Code_Thingol.static_conv_simple thy consts
- (fn program => fn thy => fn _ => fn _ => rewrite_modulo thy some_ss program);
+ (fn program => fn _ => fn _ => rewrite_modulo thy some_ss program);
fun static_tac thy some_ss consts = CONVERSION (static_conv thy some_ss consts)
THEN' conclude_tac thy some_ss;
--- a/src/Tools/Code/code_target.ML Tue Dec 21 13:57:35 2010 +0100
+++ b/src/Tools/Code/code_target.ML Tue Dec 21 14:18:45 2010 +0100
@@ -421,7 +421,7 @@
val program = prepared_program
|> Graph.new_node (value_name,
Code_Thingol.Fun (Term.dummy_patternN, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
- |> fold (curry Graph.add_edge value_name) deps;
+ |> fold (curry (perhaps o try o Graph.add_edge) value_name) deps;
val (program_code, deresolve) = produce (mounted_serializer program);
val value_name' = the (deresolve value_name);
in (program_code, value_name') end;
--- a/src/Tools/Code/code_thingol.ML Tue Dec 21 13:57:35 2010 +0100
+++ b/src/Tools/Code/code_thingol.ML Tue Dec 21 14:18:45 2010 +0100
@@ -100,14 +100,14 @@
val dynamic_value: theory -> ((term -> term) -> 'a -> 'a) -> (naming -> program
-> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
-> term -> 'a
- val static_conv: theory -> string list -> (naming -> program
- -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
+ val static_conv: theory -> string list -> (naming -> program -> string list
+ -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
-> conv
val static_conv_simple: theory -> string list
- -> (program -> theory -> (string * sort) list -> term -> conv) -> conv
+ -> (program -> (string * sort) list -> term -> conv) -> conv
val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list ->
- (naming -> program
- -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
+ (naming -> program -> string list
+ -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
-> term -> 'a
end;
@@ -916,27 +916,27 @@
let
fun generate_consts thy algebra eqngr =
fold_map (ensure_const thy algebra eqngr false);
- val (_, (naming, program)) = invoke_generation true thy (algebra, eqngr)
+ val (consts', (naming, program)) = invoke_generation true thy (algebra, eqngr)
generate_consts consts;
- in f algebra eqngr naming program end;
+ in f algebra eqngr naming program consts' end;
-fun static_evaluator evaluator algebra eqngr naming program thy vs t =
+fun static_evaluation thy evaluator algebra eqngr naming program consts' vs t =
let
val (((_, program'), (((vs', ty'), t'), deps)), _) =
ensure_value thy algebra eqngr t (NONE, (naming, program));
- in evaluator naming program' thy ((original_sorts vs vs', (vs', ty')), t') deps end;
+ in evaluator naming program' consts' ((original_sorts vs vs', (vs', ty')), t') deps end;
fun static_conv thy consts conv =
Code_Preproc.static_conv thy consts
- (provide_program thy consts (static_evaluator conv));
+ (provide_program thy consts (static_evaluation thy conv));
fun static_conv_simple thy consts conv =
Code_Preproc.static_conv thy consts
- (provide_program thy consts ((K o K o K) conv));
+ (provide_program thy consts (fn _ => fn _ => fn _ => fn program => fn _ => conv program));
fun static_value thy postproc consts evaluator =
Code_Preproc.static_value thy postproc consts
- (provide_program thy consts (static_evaluator evaluator));
+ (provide_program thy consts (static_evaluation thy evaluator));
(** diagnostic commands **)
--- a/src/Tools/nbe.ML Tue Dec 21 13:57:35 2010 +0100
+++ b/src/Tools/nbe.ML Tue Dec 21 14:18:45 2010 +0100
@@ -602,13 +602,13 @@
fun static_conv thy consts =
lift_triv_classes_conv thy (Code_Thingol.static_conv thy consts
- (K (fn program => let val nbe_program = compile true thy program
- in fn thy => oracle thy program nbe_program end)));
+ (K (fn program => fn _ => let val nbe_program = compile true thy program
+ in oracle thy program nbe_program end)));
fun static_value thy consts = lift_triv_classes_rew thy
(Code_Thingol.static_value thy I consts
- (K (fn program => let val nbe_program = compile true thy program
- in fn thy => eval_term thy program (compile false thy program) end)));
+ (K (fn program => fn _ => let val nbe_program = compile true thy program
+ in eval_term thy program (compile false thy program) end)));
(** setup **)
--- a/src/Tools/subtyping.ML Tue Dec 21 13:57:35 2010 +0100
+++ b/src/Tools/subtyping.ML Tue Dec 21 14:18:45 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