signature BASIC_CODE_THINGOL = sig type vname = string datatype itype =
`%% ofstring * itype list
| ITyVar of vname datatype dict =
Dict of (class * class) list * plain_dict and plain_dict =
Dict_Const of (string * class) * (itype * dict list) list
| Dict_Var of { var: vname, index: int, length: int, class: class, unique: bool } typeconst = { sym: Code_Symbol.T, typargs: itype list, dictss: dict listlist,
dom: itype list, range: itype, annotation: itype option } datatype iterm =
IConst ofconst
| IVar of vname option
| `$ of iterm * iterm
| `|=> of (vname option * itype) * (iterm * itype)
| ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm } val `-> : itype * itype -> itype val `--> : itype list * itype -> itype val `$$ : iterm * iterm list -> iterm val `|==> : (vname option * itype) list * (iterm * itype) -> iterm type typscheme = (vname * sort) list * itype end;
signature CODE_THINGOL = sig
include BASIC_CODE_THINGOL val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a val unfold_fun: itype -> itype list * itype val unfold_fun_n: int -> itype -> itype list * itype val unfold_app: iterm -> iterm * iterm list val unfold_abs: iterm -> (vname option * itype) list * iterm val unfold_abs_typed: iterm -> ((vname option * itype) list * (iterm * itype)) option val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option val split_let_no_pat: iterm -> (((stringoption * itype) * iterm) * iterm) option val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm val unfold_let_no_pat: iterm -> ((stringoption * itype) * iterm) list * iterm val split_pat_abs: iterm -> ((iterm * itype) * iterm) option val unfold_pat_abs: iterm -> (iterm * itype) list * iterm val unfold_const_app: iterm -> (const * iterm list) option val is_IVar: iterm -> bool val is_IAbs: iterm -> bool val satisfied_application: int -> const * iterm list
-> ((vname option * itype) list * (iterm list * itype)) * iterm list val saturated_application: int -> const * iterm list -> iterm val contains_dict_var: iterm -> bool val unambiguous_dictss: dict listlist -> bool val add_constsyms: iterm -> Code_Symbol.T list -> Code_Symbol.T list val add_tyconames: iterm -> stringlist -> stringlist val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a val add_varnames: iterm -> stringlist -> stringlist
datatype stmt =
NoStmt
| Funof (typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option
| Datatypeof vname list *
((string * vname list(*type argument wrt. canonical order*)) * itype list) list
| Datatypecons ofstring
| Class of vname * ((class * class) list * (string * itype) list)
| Classrel of class * class
| Classparam of class
| Classinst of { class: string, tyco: string, vs: (vname * sort) list,
superinsts: (class * (itype * dict list) list) list,
inst_params: ((string * (const * int)) * (thm * bool)) list,
superinst_params: ((string * (const * int)) * (thm * bool)) list }; type program = stmt Code_Symbol.Graph.T val unimplemented: program -> stringlist val implemented_deps: program -> stringlist val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt val is_constr: program -> Code_Symbol.T -> bool val is_case: stmt -> bool val group_stmts: Proof.context -> program
-> ((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: Proof.context -> stringlist -> stringlist val consts_program: Proof.context -> stringlist -> program val dynamic_conv: Proof.context -> (program
-> typscheme * iterm -> Code_Symbol.T list -> conv)
-> conv val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> (program
-> term -> typscheme * iterm -> Code_Symbol.T list -> 'a)
-> term -> 'a val static_conv_thingol: { ctxt: Proof.context, consts: stringlist }
-> ({ program: program, deps: stringlist }
-> Proof.context -> typscheme * iterm -> Code_Symbol.T list -> conv)
-> Proof.context -> conv val static_conv_isa: { ctxt: Proof.context, consts: stringlist }
-> (program -> Proof.context -> term -> conv)
-> Proof.context -> conv val static_value: { ctxt: Proof.context, lift_postproc: ((term -> term) -> 'a -> 'a), consts: stringlist }
-> ({ program: program, deps: stringlist }
-> Proof.context -> term -> typscheme * iterm -> Code_Symbol.T list -> 'a)
-> Proof.context -> term -> 'a end;
structure Code_Thingol : CODE_THINGOL = struct
open Basic_Code_Symbol;
(** auxiliary **)
fun unfoldl dest x = case dest x of NONE => (x, [])
| SOME (x1, x2) => letval (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end;
fun unfoldr dest x = case dest x of NONE => ([], x)
| SOME (x1, x2) => letval (xs', x') = unfoldr dest x2 in (x1 :: xs', x') end;
(** language core - types, terms **)
type vname = string;
datatype itype =
`%% ofstring * itype list
| ITyVar of vname;
datatype dict =
Dict of (class * class) list * plain_dict and plain_dict =
Dict_Const of (string * class) * (itype * dict list) list
| Dict_Var of { var: vname, index: int, length: int, class: class, unique: bool };
fun ty1 `-> ty2 = "fun" `%% [ty1, ty2];
val op `--> = Library.foldr (op `->);
val unfold_fun = unfoldr
(fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2)
| _ => NONE);
fun unfold_fun_n n ty = let val (tys1, ty1) = unfold_fun ty; val (tys3, tys2) = chop n tys1; in (tys3, tys2 `--> ty1) end;
val op `$$ = Library.foldl (op `$); fun vs_tys `|==> body = Library.foldr
(fn (v_ty as (_, ty), body as (_, rty)) => (v_ty `|=> body, ty `-> rty)) (vs_tys, body)
|> fst;
val unfold_app = unfoldl
(fn op `$ t_t => SOME t_t
| _ => NONE);
val unfold_abs = unfoldr
(fn (v_ty `|=> (t, _)) => SOME (v_ty, t)
| _ => NONE);
fun fold_varnames f = let fun fold_aux add_vars f = let fun fold_term _ (IConst _) = I
| fold_term vs (IVar (SOME v)) = if member (op =) vs v then I else f v
| fold_term _ (IVar NONE) = I
| fold_term vs (t1 `$ t2) = fold_term vs t1 #> fold_term vs t2
| fold_term vs ((SOME v, _) `|=> (t, _)) = fold_term (insert (op =) v vs) t
| fold_term vs ((NONE, _) `|=> (t, _)) = fold_term vs t
| fold_term vs (ICase { term = t, clauses = clauses, ... }) =
fold_term vs t #> fold (fold_clause vs) clauses and fold_clause vs (p, t) = fold_term (add_vars p vs) t; in fold_term [] end fun add_vars t = fold_aux add_vars (insert (op =)) t; in fold_aux add_vars f end;
val add_varnames = fold_varnames (insert (op =));
val declare_varnames = fold_varnames Name.declare;
fun exists_var t v = fold_varnames (fn w => fn b => v = w orelse b) t false;
fun split_pat_abs ((NONE, ty) `|=> (t, _)) = SOME ((IVar NONE, ty), t)
| split_pat_abs ((SOME v, ty) `|=> (t, _)) = SOME (case t of ICase { term = IVar (SOME w), clauses = [(p, body)], ... } => if v = w andalso (exists_var p v orelse not (exists_var body v)) then ((p, ty), body) else ((IVar (SOME v), ty), t)
| _ => ((IVar (SOME v), ty), t))
| split_pat_abs _ = NONE;
val unfold_pat_abs = unfoldr split_pat_abs;
fun unfold_abs_eta [] t = ([], t)
| unfold_abs_eta (_ :: tys) ((v, _) `|=> (t, _)) = let val (vs, t') = unfold_abs_eta tys t; in (v :: vs, t') end
| unfold_abs_eta tys t = let val names = Name.build_context (declare_varnames t); val vs = map SOME (Name.invent names "a" (length tys)); in (vs, t `$$ map IVar vs) end;
fun satisfied_application wanted ({ dom, range, ... }, ts) = let val given = length ts; val delta = wanted - given; val rty = drop wanted dom `--> range; in if delta = 0 then
(([], (ts, rty)), []) elseif delta < 0 then let val (ts1, ts2) = chop wanted ts in (([], (ts1, rty)), ts2) end else let val names = Name.build_context (fold declare_varnames ts); val vs_tys = (map o apfst) SOME (Name.invent_names names "a" (take delta (drop given dom))); in ((vs_tys, (ts @ map (IVar o fst) vs_tys, rty)), []) end end
fun saturated_application wanted (const, ts) = let val ((vs_tys, (ts', rty)), []) = satisfied_application wanted (const, ts) in vs_tys `|==> (IConst const `$$ ts', rty) end
fun map_terms_bottom_up f (t as IConst _) = f t
| map_terms_bottom_up f (t as IVar _) = f t
| map_terms_bottom_up f (t1 `$ t2) = f
(map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2)
| map_terms_bottom_up f ((v, ty) `|=> (t, rty)) = f
((v, ty) `|=> (map_terms_bottom_up f t, rty))
| map_terms_bottom_up f (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) = f
(ICase { term = map_terms_bottom_up f t, typ = ty,
clauses = (map o apply2) (map_terms_bottom_up f) clauses,
primitive = map_terms_bottom_up f t0 });
fun distill_minimized_clause tys t = let fun restrict_vars_to vs =
map_terms_bottom_up (fn IVar (SOME v) =>
IVar (if member (op =) vs v then SOME v else NONE) | t => t); fun purge_unused_vars_in t =
restrict_vars_to (build (add_varnames t)); fun distill' vs_map pat_args v i clauses = let val pat_vs = build (fold add_varnames (nth_drop i pat_args)); fun varnames_disjunctive pat =
null (inter (op =) pat_vs (build (add_varnames pat))); in if forall (fn (pat', body') => varnames_disjunctive pat' (*prevent mingled scopes resulting in duplicated variables in pattern arguments*)
andalso (exists_var pat' v (*reducible if shadowed by pattern*)
orelse not (exists_var body' v))) clauses (*reducible if absent in body*) then clauses
|> maps (fn (pat', body') =>
distill vs_map
(nth_map i (K pat') pat_args |> map (purge_unused_vars_in body'))
body')
|> SOME else NONE end and distill vs_map pat_args
(body as ICase { term = IVar (SOME v), clauses = clauses, ... }) =
(case AList.lookup (op =) vs_map v of SOME i => distill' (AList.delete (op =) v vs_map) pat_args v i clauses
|> the_default [(pat_args, body)]
| NONE => [(pat_args, body)])
| distill vs_map pat_args body = [(pat_args, body)]; val (vs, body) = unfold_abs_eta tys t; val vs_map =
build (fold_index (fn (i, SOME v) => cons (v, i) | _ => I) vs); in distill vs_map (map IVar vs) body end;
fun exists_dict_var f (Dict (_, d)) = exists_plain_dict_var_pred f d and exists_plain_dict_var_pred f (Dict_Const (_, dictss)) = exists_dictss_var f (map snd dictss)
| exists_plain_dict_var_pred f (Dict_Var x) = f x and exists_dictss_var f = (exists o exists) (exists_dict_var f);
val unambiguous_dictss = not o exists_dictss_var (fn { unique, ... } => not unique);
(** statements, abstract programs **)
type typscheme = (vname * sort) list * itype; datatype stmt =
NoStmt
| Funof (typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option
| Datatypeof vname list * ((string * vname list) * itype list) list
| Datatypecons ofstring
| Class of vname * ((class * class) list * (string * itype) list)
| Classrel of class * class
| Classparam of class
| Classinst of { class: string, tyco: string, vs: (vname * sort) list,
superinsts: (class * (itype * dict list) list) list,
inst_params: ((string * (const * int)) * (thm * bool)) list,
superinst_params: ((string * (const * int)) * (thm * bool)) list };
type program = stmt Code_Symbol.Graph.T;
val unimplemented =
build o Code_Symbol.Graph.fold (fn (Constant c, (NoStmt, _)) => cons c | _ => I);
fun implemented_deps program =
Code_Symbol.Graph.keys program
|> subtract (op =) (Code_Symbol.Graph.all_preds program (map Constant (unimplemented program)))
|> map_filter (fn Constant c => SOME c | _ => NONE);
fun map_classparam_instances_as_term f =
(map o apfst o apsnd o apfst) (fn const => case f (IConst const) of IConst const' => const')
fun map_terms_stmt f NoStmt = NoStmt
| map_terms_stmt f (Fun ((tysm, eqs), case_cong)) = Fun ((tysm, (map o apfst)
(fn (ts, t) => (map f ts, f t)) eqs), case_cong)
| map_terms_stmt f (stmt as Datatype _) = stmt
| map_terms_stmt f (stmt as Datatypecons _) = stmt
| map_terms_stmt f (stmt as Class _) = stmt
| map_terms_stmt f (stmt as Classrel _) = stmt
| map_terms_stmt f (stmt as Classparam _) = stmt
| map_terms_stmt f (Classinst { class, tyco, vs, superinsts,
inst_params, superinst_params }) =
Classinst { class = class, tyco = tyco, vs = vs, superinsts = superinsts,
inst_params = map_classparam_instances_as_term f inst_params,
superinst_params = map_classparam_instances_as_term f superinst_params };
fun is_constr program sym = case Code_Symbol.Graph.get_node program sym of Datatypecons _ => true
| _ => false;
fun is_case (Fun (_, SOME _)) = true
| is_case _ = false;
fun linear_stmts program =
rev (Code_Symbol.Graph.strong_conn program)
|> map (AList.make (Code_Symbol.Graph.get_node program));
fun group_stmts ctxt program = let fun is_fun (_, Fun _) = true | is_fun _ = false; fun is_datatypecons (_, Datatypecons _) = true | is_datatypecons _ = false; fun is_datatype (_, Datatype _) = true | is_datatype _ = false; fun is_class (_, Class _) = true | is_class _ = false; fun is_classrel (_, Classrel _) = true | is_classrel _ = false; fun is_classparam (_, Classparam _) = true | is_classparam _ = false; fun is_classinst (_, Classinst _) = true | is_classinst _ = false; fun group stmts = if forall (is_datatypecons orf is_datatype) stmts then (filter is_datatype stmts, [], ([], [])) elseif forall (is_class orf is_classrel orf is_classparam) stmts then ([], filter is_class stmts, ([], [])) elseif forall (is_fun orf is_classinst) stmts then ([], [], List.partition is_fun stmts) else error ("Illegal mutual dependencies: " ^ (commas
o map (Code_Symbol.quote ctxt o fst)) stmts); in
linear_stmts program
|> map group end;
(** translation kernel **)
(* generic mechanisms *)
fun ensure_stmt symbolize generate x (deps, program) = let val sym = symbolize x; 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 deps
|> pair x else
program
|> Code_Symbol.Graph.default_node (sym, NoStmt)
|> add_dep
|> curry generate (sym :: deps)
||> snd
|-> (fn stmt => (Code_Symbol.Graph.map_node sym) (K stmt))
|> pair deps
|> pair x end;
exception PERMISSIVE of unit;
fun translation_error ctxt permissive some_thm deps msg sub_msg = if permissive thenraise PERMISSIVE () else let val thm_msg = Option.map (fn thm => "in code equation " ^ Thm.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 ctxt permissive some_thm deps ty sort e = let val err_class = Sorts.class_error (Context.Proof ctxt) e; val err_typ = "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^
Syntax.string_of_sort ctxt sort; in
translation_error ctxt permissive some_thm deps "Wellsortedness error" (err_typ ^ "\n" ^ err_class) end;
(* inference of type annotations for disambiguation with type classes *)
fun mk_tagged_type (true, T) = Type ("", [T])
| mk_tagged_type (false, T) = T;
fun dest_tagged_type (Type ("", [T])) = (true, T)
| dest_tagged_type T = (false, T);
val fastype_of_tagged_term = fastype_of o map_types (snd o dest_tagged_type);
fun tag_term (proj_sort, _) eqngr = let val has_sort_constraints = exists (not o null) o map proj_sort o Code_Preproc.sortargs eqngr; fun tag (Const (_, T')) (Const (c, T)) = Const (c,
mk_tagged_type (not (null (Term.add_tvarsT T' [])) andalso has_sort_constraints c, T))
| tag (t1 $ u1) (t $ u) = tag t1 t $ tag u1 u
| tag (Abs (_, _, t1)) (Abs (x, T, t)) = Abs (x, T, tag t1 t)
| tag (Free _) (t as Free _) = t
| tag (Var _) (t as Var _) = t
| tag (Bound _) (t as Bound _) = t; in tag end
fun annotate ctxt algbr eqngr (c, ty) args rhs = let val erase = map_types (fn _ => Type_Infer.anyT []); val reinfer = singleton (Type_Infer_Context.infer_types ctxt); val lhs = list_comb (Const (c, ty), map (Term.strip_sorts o snd) args); val reinferred_rhs = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase rhs)))); in tag_term algbr eqngr reinferred_rhs rhs end
fun annotate_eqns ctxt algbr eqngr (c, ty) eqns = let val ctxt' = ctxt |> Proof_Context.theory_of |> Proof_Context.init_global
|> Config.put Type_Infer_Context.const_sorts false; (*avoid spurious fixed variables: there is no eigen context for equations*) in map (apfst (fn (args, (some_abs, rhs)) => (args,
(some_abs, annotate ctxt' algbr eqngr (c, ty) args rhs)))) eqns end;
(* abstract dictionary construction *)
datatype typarg_witness =
Weakening of (class * class) list * plain_typarg_witness and plain_typarg_witness =
Global of (string * class) * (typ * typarg_witness list) list
| Local of { var: string, index: int, sort: sort, unique: bool };
fun brand_unique unique (w as Global _) = w
| brand_unique unique (Local { var, index, sort, unique = _ }) =
Local { var = var, index = index, sort = sort, unique = unique };
fun construct_dictionaries ctxt (proj_sort, algebra) permissive some_thm (ty, sort) (deps, program) = let fun class_relation unique (Weakening (classrels, x), sub_class) super_class =
Weakening ((sub_class, super_class) :: classrels, brand_unique unique x); fun type_constructor (tyco, typs) dictss class =
Weakening ([], Global ((tyco, class), typs ~~ (map o map) fst dictss)); fun type_variable (TFree (v, sort)) = let val sort' = proj_sort sort; in map_index (fn (n, class) => (Weakening ([], Local
{ var = v, index = n, sort = sort', unique = true }), class)) sort' end; val typarg_witnesses = Sorts.of_sort_derivation algebra
{class_relation = fn _ => fn unique =>
Sorts.classrel_derivation algebra (class_relation unique),
type_constructor = type_constructor,
type_variable = type_variable} (ty, proj_sort sort) handle Sorts.CLASS_ERROR e => not_wellsorted ctxt permissive some_thm deps ty sort e; in (typarg_witnesses, (deps, program)) end;
fun invoke_generation_for_consts'' ctxt algebra_eqngr =
invoke_generation_for_consts ctxt
{ ignore_cache = true, permissive = false }
algebra_eqngr
#> (fn (deps, program) => { deps = deps, program = program });
fun consts_program_permissive ctxt =
invoke_generation_for_consts' ctxt true;
fun consts_program ctxt consts = let fun project program = Code_Symbol.Graph.restrict
(member (op =) (Code_Symbol.Graph.all_succs program
(map Constant consts))) program; in
invoke_generation_for_consts' ctxt false consts
|> project end;
(* value evaluation *)
fun ensure_value ctxt algbr eqngr t = let val ty = fastype_of t; val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
o dest_TFree))) t []; val t' = annotate ctxt algbr eqngr (\<^const_name>\Pure.dummy_pattern\, ty) [] t; val dummy_constant = Constant \<^const_name>\<open>Pure.dummy_pattern\<close>; val stmt_value =
fold_map (translate_tyvar_sort ctxt algbr eqngr false) vs
##>> translate_typ ctxt algbr eqngr false ty
##>> translate_term ctxt algbr eqngr false NONE NONE t'
#>> (fn ((vs, ty), t) => Fun
(((vs, ty), [(([], t), (NONE, true))]), NONE)); fun term_value (_, program1) = let valFun ((vs_ty, [(([], t), _)]), _) =
Code_Symbol.Graph.get_node 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 program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2; in ((program3, ((vs_ty, t), deps')), (deps', program2)) end; in
ensure_stmt Constant stmt_value \<^const_name>\<open>Pure.dummy_pattern\<close>
#> snd
#> term_value end;
fun dynamic_evaluation comp ctxt algebra eqngr t = let val ((program, (vs_ty_t', deps)), _) =
Code_Preproc.timed "translating term" #ctxt
(fn { ctxt, algebra, eqngr, t } =>
invoke_generation false ctxt (ensure_value ctxt algebra eqngr) t)
{ ctxt = ctxt, algebra = algebra, eqngr = eqngr, t = t }; in comp program t vs_ty_t' deps end;
fun dynamic_conv ctxt conv =
Code_Preproc.dynamic_conv ctxt
(dynamic_evaluation (fn program => fn _ => conv program) ctxt);
fun static_evaluation_thingol ctxt consts (algebra_eqngr as { algebra, eqngr }) static_eval = let fun evaluation program dynamic_eval ctxt t = let val ((_, ((vs_ty', t'), deps)), _) =
Code_Preproc.timed "translating term" #ctxt
(fn { ctxt, t } =>
ensure_value ctxt algebra eqngr t ([], program))
{ ctxt = ctxt, t = t }; in dynamic_eval ctxt t (vs_ty', t') deps end; in
static_evaluation ctxt consts algebra_eqngr (fn program_deps =>
evaluation (#program program_deps) (static_eval program_deps)) end;
fun read_const_exprs_internal ctxt = let val thy = Proof_Context.theory_of ctxt; fun this_theory name = if Context.theory_base_name thy = name then thy else Context.get_theory {long = false} thy name;
fun consts_of thy' =
fold (fn (c, (_, NONE)) => cons c | _ => I)
(#constants (Consts.dest (Sign.consts_of thy'))) []
|> filter_out (Code.is_abstr thy); fun belongs_here thy' c = forall
(fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy'); fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy'); fun read_const_expr str =
(case Syntax.parse_input ctxt (K NONE) (K Markup.empty) (SOME o Symbol_Pos.implode o #1) str of
SOME "_" => ([], consts_of thy)
| SOME s =>
(casetry (unsuffix "._") s of
SOME name => ([], consts_of_select (this_theory name))
| NONE => ([Code.read_const ctxt str], []))
| NONE => ([Code.read_const ctxt str], [])); in apply2 flat o split_list o map read_const_expr end;
fun read_const_exprs_all ctxt = op @ o read_const_exprs_internal ctxt;
fun read_const_exprs ctxt const_exprs = let val (consts, consts_permissive) =
read_const_exprs_internal ctxt const_exprs; val consts' =
consts_program_permissive ctxt consts_permissive
|> implemented_deps
|> filter_out (Code.is_abstr (Proof_Context.theory_of ctxt)); in union (op =) consts' consts end;
(** diagnostic commands **)
fun code_depgr ctxt consts = let val { eqngr, ... } = Code_Preproc.obtain true
{ ctxt = ctxt, consts = consts, terms = [] }; val all_consts = Graph.all_succs eqngr consts; in Graph.restrict (member (op =) all_consts) eqngr end;
fun code_thms ctxt = Pretty.writeln o Code_Preproc.pretty ctxt o code_depgr ctxt;
fun coalesce_strong_conn gr = let val xss = Graph.strong_conn gr; val xss_ys = map (fn xs => (xs, commas xs)) xss; val y_for = the o AList.lookup (op =) (maps (fn (xs, y) => map (fn x => (x, y)) xs) xss_ys); fun coalesced_succs_for xs = maps (Graph.immediate_succs gr) xs
|> subtract (op =) xs
|> map y_for
|> distinct (op =); val succs = map (fn (xs, _) => (xs, coalesced_succs_for xs)) xss_ys; in map (fn (xs, y) => ((y, xs), (maps (Graph.get_node gr) xs, (the o AList.lookup (op =) succs) xs))) xss_ys end;
fun code_deps ctxt consts = let val thy = Proof_Context.theory_of ctxt; fun mk_entry ((name, consts), (ps, deps)) = let val label = commas (map (Code.string_of_const thy) consts); in ((name, Graph_Display.content_node label (Pretty.str label :: ps)), deps) end; in
code_depgr ctxt consts
|> Graph.map (K (Code.pretty_cert thy o snd))
|> coalesce_strong_conn
|> map mk_entry
|> Graph_Display.display_graph end;
local
fun code_thms_cmd ctxt = code_thms ctxt o read_const_exprs_all ctxt; fun code_deps_cmd ctxt = code_deps ctxt o read_const_exprs_all ctxt;
in
val _ =
Outer_Syntax.command \<^command_keyword>\<open>code_thms\<close> "print system of code equations for code"
(Scan.repeat1 Parse.term >> (fn cs =>
Toplevel.keep (fn st => code_thms_cmd (Toplevel.context_of st) cs)));
val _ =
Outer_Syntax.command \<^command_keyword>\<open>code_deps\<close> "visualize dependencies of code equations for code"
(Scan.repeat1 Parse.term >> (fn cs =>
Toplevel.keep (fn st => code_deps_cmd (Toplevel.context_of st) cs)));
