--- a/src/Tools/Code/code_thingol.ML Thu Jan 30 22:42:29 2014 +0100
+++ b/src/Tools/Code/code_thingol.ML Thu Jan 30 22:55:52 2014 +0100
@@ -83,8 +83,8 @@
-> ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list
* ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list)) list
- val read_const_exprs: theory -> string list -> string list * string list
- val consts_program: theory -> bool -> string list -> program
+ val read_const_exprs: theory -> string list -> string list
+ val consts_program: theory -> string list -> program
val dynamic_conv: theory -> (program
-> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv)
-> conv
@@ -363,54 +363,61 @@
(* generic mechanisms *)
-fun ensure_stmt symbolize generate x (dep, program) =
+fun ensure_stmt symbolize generate x (deps, program) =
let
val sym = symbolize x;
- val add_dep = case dep of NONE => I
- | SOME dep => Code_Symbol.Graph.add_edge (dep, sym);
+ val add_dep = case deps of [] => I
+ | dep :: _ => Code_Symbol.Graph.add_edge (dep, sym);
in
if can (Code_Symbol.Graph.get_node program) sym
then
program
|> add_dep
- |> pair dep
+ |> pair deps
|> pair x
else
program
|> Code_Symbol.Graph.default_node (sym, NoStmt)
|> add_dep
- |> curry generate (SOME sym)
+ |> curry generate (sym :: deps)
||> snd
|-> (fn stmt => (Code_Symbol.Graph.map_node sym) (K stmt))
- |> pair dep
+ |> pair deps
|> pair x
end;
exception PERMISSIVE of unit;
-fun translation_error thy permissive some_thm msg sub_msg =
+fun translation_error thy program permissive some_thm deps msg sub_msg =
if permissive
then raise PERMISSIVE ()
else
let
- val err_thm =
- (case some_thm of
- SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")"
- | NONE => "");
- in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end;
+ val ctxt = Proof_Context.init_global thy;
+ val thm_msg =
+ Option.map (fn thm => "in code equation " ^ Display.string_of_thm ctxt thm) some_thm;
+ val dep_msg = if null (tl deps) then NONE
+ else SOME ("with dependency "
+ ^ space_implode " -> " (map (Code_Symbol.quote ctxt) (rev deps)));
+ val thm_dep_msg = case (thm_msg, dep_msg)
+ of (SOME thm_msg, SOME dep_msg) => "\n(" ^ thm_msg ^ ",\n" ^ dep_msg ^ ")"
+ | (SOME thm_msg, NONE) => "\n(" ^ thm_msg ^ ")"
+ | (NONE, SOME dep_msg) => "\n(" ^ dep_msg ^ ")"
+ | (NONE, NONE) => ""
+ in error (msg ^ thm_dep_msg ^ ":\n" ^ sub_msg) end;
fun maybe_permissive f prgrm =
f prgrm |>> SOME handle PERMISSIVE () => (NONE, prgrm);
-fun not_wellsorted thy permissive some_thm ty sort e =
+fun not_wellsorted thy program permissive some_thm deps ty sort e =
let
val err_class = Sorts.class_error (Context.pretty_global thy) e;
val err_typ =
"Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort " ^
Syntax.string_of_sort_global thy sort;
in
- translation_error thy permissive some_thm "Wellsortedness error"
- (err_typ ^ "\n" ^ err_class)
+ translation_error thy program permissive some_thm deps
+ "Wellsortedness error" (err_typ ^ "\n" ^ err_class)
end;
@@ -455,6 +462,32 @@
(annotate thy algbr eqngr (c, ty) args rhs, some_abs)))) eqns
+(* abstract dictionary construction *)
+
+datatype typarg_witness =
+ Weakening of (class * class) list * plain_typarg_witness
+and plain_typarg_witness =
+ Global of (string * class) * typarg_witness list list
+ | Local of string * (int * sort);
+
+fun construct_dictionaries thy (proj_sort, algebra) permissive some_thm (ty, sort) (deps, program) =
+ let
+ fun class_relation ((Weakening (classrels, x)), sub_class) super_class =
+ Weakening ((sub_class, super_class) :: classrels, x);
+ fun type_constructor (tyco, _) dss class =
+ Weakening ([], Global ((tyco, class), (map o map) fst dss));
+ fun type_variable (TFree (v, sort)) =
+ let
+ val sort' = proj_sort sort;
+ in map_index (fn (n, class) => (Weakening ([], Local (v, (n, sort'))), class)) sort' end;
+ val typarg_witnesses = Sorts.of_sort_derivation algebra
+ {class_relation = K (Sorts.classrel_derivation algebra class_relation),
+ type_constructor = type_constructor,
+ type_variable = type_variable} (ty, proj_sort sort)
+ handle Sorts.CLASS_ERROR e => not_wellsorted thy program permissive some_thm deps ty sort e;
+ in (typarg_witnesses, (deps, program)) end;
+
+
(* translation *)
fun ensure_tyco thy algbr eqngr permissive tyco =
@@ -589,13 +622,16 @@
#>> rpair (some_thm, proper)
and translate_eqns thy algbr eqngr permissive eqns =
maybe_permissive (fold_map (translate_eqn thy algbr eqngr permissive) eqns)
-and translate_const thy algbr eqngr permissive some_thm ((c, ty), some_abs) =
+and translate_const thy algbr eqngr permissive some_thm ((c, ty), some_abs) (deps, program) =
let
val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs))
andalso Code.is_abstr thy c
- then translation_error thy permissive some_thm
+ then translation_error thy program permissive some_thm deps
"Abstraction violation" ("constant " ^ Code.string_of_const thy c)
else ()
+ in translate_const_proper thy algbr eqngr permissive some_thm (c, ty) (deps, program) end
+and translate_const_proper thy algbr eqngr permissive some_thm (c, ty) =
+ let
val (annotate, ty') = dest_tagged_type ty;
val typargs = Sign.const_typargs thy (c, ty');
val sorts = Code_Preproc.sortargs eqngr c;
@@ -693,26 +729,8 @@
and translate_tyvar_sort thy (algbr as (proj_sort, _)) eqngr permissive (v, sort) =
fold_map (ensure_class thy algbr eqngr permissive) (proj_sort sort)
#>> (fn sort => (unprefix "'" v, sort))
-and translate_dicts thy (algbr as (proj_sort, algebra)) eqngr permissive some_thm (ty, sort) =
+and translate_dicts thy algbr eqngr permissive some_thm (ty, sort) =
let
- datatype typarg_witness =
- Weakening of (class * class) list * plain_typarg_witness
- and plain_typarg_witness =
- Global of (string * class) * typarg_witness list list
- | Local of string * (int * sort);
- fun class_relation ((Weakening (classrels, x)), sub_class) super_class =
- Weakening ((sub_class, super_class) :: classrels, x);
- fun type_constructor (tyco, _) dss class =
- Weakening ([], Global ((tyco, class), (map o map) fst dss));
- fun type_variable (TFree (v, sort)) =
- let
- val sort' = proj_sort sort;
- in map_index (fn (n, class) => (Weakening ([], Local (v, (n, sort'))), class)) sort' end;
- val typarg_witnesses = Sorts.of_sort_derivation algebra
- {class_relation = K (Sorts.classrel_derivation algebra class_relation),
- type_constructor = type_constructor,
- type_variable = type_variable} (ty, proj_sort sort)
- handle Sorts.CLASS_ERROR e => not_wellsorted thy permissive some_thm ty sort e;
fun mk_dict (Weakening (classrels, x)) =
fold_map (ensure_classrel thy algbr eqngr permissive) classrels
##>> mk_plain_dict x
@@ -723,7 +741,10 @@
#>> (fn (inst, dss) => Dict_Const (inst, dss))
| mk_plain_dict (Local (v, (n, sort))) =
pair (Dict_Var (unprefix "'" v, (n, length sort)))
- in fold_map mk_dict typarg_witnesses end;
+ in
+ construct_dictionaries thy algbr permissive some_thm (ty, sort)
+ #-> (fn typarg_witnesses => fold_map mk_dict typarg_witnesses)
+ end;
(* store *)
@@ -736,26 +757,32 @@
fun invoke_generation ignore_cache thy (algebra, eqngr) generate thing =
Program.change_yield (if ignore_cache then NONE else SOME thy)
- (fn program => (NONE, program)
+ (fn program => ([], program)
|> generate thy algebra eqngr thing
|-> (fn thing => fn (_, program) => (thing, program)));
(* program generation *)
-fun consts_program thy permissive consts =
+fun consts_program_internal thy permissive consts =
let
- fun project program =
- if permissive then program
- else Code_Symbol.Graph.restrict
- (member (op =) (Code_Symbol.Graph.all_succs program
- (map Constant consts))) program;
fun generate_consts thy algebra eqngr =
fold_map (ensure_const thy algebra eqngr permissive);
in
invoke_generation permissive thy (Code_Preproc.obtain false thy consts [])
generate_consts consts
|> snd
+ end;
+
+fun consts_program_permissive thy = consts_program_internal thy true;
+
+fun consts_program thy consts =
+ let
+ fun project program = Code_Symbol.Graph.restrict
+ (member (op =) (Code_Symbol.Graph.all_succs program
+ (map Constant consts))) program;
+ in
+ consts_program_internal thy false consts
|> project
end;
@@ -775,15 +802,15 @@
##>> translate_term thy algbr eqngr false NONE (t', NONE)
#>> (fn ((vs, ty), t) => Fun
(((vs, ty), [(([], t), (NONE, true))]), NONE));
- fun term_value (dep, program1) =
+ fun term_value (deps, program1) =
let
val Fun ((vs_ty, [(([], t), _)]), _) =
Code_Symbol.Graph.get_node program1 dummy_constant;
- val deps = Code_Symbol.Graph.immediate_succs program1 dummy_constant;
+ val deps' = Code_Symbol.Graph.immediate_succs program1 dummy_constant;
val program2 = Code_Symbol.Graph.del_node dummy_constant program1;
- val deps_all = Code_Symbol.Graph.all_succs program2 deps;
+ val deps_all = Code_Symbol.Graph.all_succs program2 deps';
val program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2;
- in ((program3, ((vs_ty, t), deps)), (dep, program2)) end;
+ in ((program3, ((vs_ty, t), deps')), (deps, program2)) end;
in
ensure_stmt Constant stmt_value @{const_name dummy_pattern}
#> snd
@@ -808,7 +835,7 @@
fun lift_evaluation thy evaluation' algebra eqngr program vs t =
let
val ((_, (((vs', ty'), t'), deps)), _) =
- ensure_value thy algebra eqngr t (NONE, program);
+ ensure_value thy algebra eqngr t ([], program);
in evaluation' ((original_sorts vs vs', (vs', ty')), t') deps end;
fun lift_evaluator thy evaluator' consts algebra eqngr =
@@ -838,9 +865,9 @@
Code_Preproc.static_value thy postproc consts (lift_evaluator thy evaluator consts);
-(** diagnostic commands **)
+(** constant expressions **)
-fun read_const_exprs thy =
+fun read_const_exprs_internal thy =
let
fun consts_of thy' = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
((snd o #constants o Consts.dest o Sign.consts_of) thy') [];
@@ -859,6 +886,17 @@
| NONE => ([Code.read_const thy str], []));
in pairself flat o split_list o map read_const_expr end;
+fun read_const_exprs_all thy = op @ o read_const_exprs_internal thy;
+
+fun read_const_exprs thy const_exprs =
+ let
+ val (consts, consts_permissive) = read_const_exprs_internal thy const_exprs;
+ val consts' = implemented_deps (consts_program_permissive thy consts_permissive);
+ in union (op =) consts' consts end;
+
+
+(** diagnostic commands **)
+
fun code_depgr thy consts =
let
val (_, eqngr) = Code_Preproc.obtain true thy consts [];
@@ -888,8 +926,8 @@
local
-fun code_thms_cmd thy = code_thms thy o op @ o read_const_exprs thy;
-fun code_deps_cmd thy = code_deps thy o op @ o read_const_exprs thy;
+fun code_thms_cmd thy = code_thms thy o read_const_exprs_all thy;
+fun code_deps_cmd thy = code_deps thy o read_const_exprs_all thy;
in