haftmann@24219: (*  Title:      Tools/code/code_package.ML
haftmann@24219:     ID:         $Id$
haftmann@24219:     Author:     Florian Haftmann, TU Muenchen
haftmann@24219: 
haftmann@24918: Code generator interfaces and Isar setup.
haftmann@24219: *)
haftmann@24219: 
haftmann@24219: signature CODE_PACKAGE =
haftmann@24219: sig
haftmann@26011:   val evaluate_conv: theory
haftmann@26740:     -> (term -> term * (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm
haftmann@26740:        -> string list -> thm))
haftmann@24283:     -> cterm -> thm;
haftmann@26011:   val evaluate_term: theory
haftmann@26740:     -> (term -> term * (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm
haftmann@26740:        -> string list -> 'a))
haftmann@24835:     -> term -> 'a;
haftmann@26011:   val eval_conv: string * (unit -> thm) option ref
haftmann@26011:     -> theory -> cterm -> string list -> thm;
haftmann@26011:   val eval_term: string * (unit -> 'a) option ref
haftmann@26011:     -> theory -> term -> string list -> 'a;
haftmann@26011:   val satisfies: theory -> term -> string list -> bool;
haftmann@24585:   val satisfies_ref: (unit -> bool) option ref;
haftmann@25611:   val codegen_shell_command: string (*theory name*) -> string (*cg expr*) -> unit;
haftmann@24219: end;
haftmann@24219: 
haftmann@24219: structure CodePackage : CODE_PACKAGE =
haftmann@24219: struct
haftmann@24219: 
haftmann@24844: (** code theorems **)
haftmann@24219: 
haftmann@24283: fun code_depgr thy [] = CodeFuncgr.make thy []
haftmann@24219:   | code_depgr thy consts =
haftmann@24219:       let
haftmann@24283:         val gr = CodeFuncgr.make thy consts;
haftmann@24423:         val select = Graph.all_succs gr consts;
haftmann@24219:       in
haftmann@24423:         gr
haftmann@24423:         |> Graph.subgraph (member (op =) select) 
haftmann@25597:         |> Graph.map_nodes ((apsnd o map) (AxClass.overload thy))
haftmann@24219:       end;
haftmann@24219: 
haftmann@24219: fun code_thms thy =
haftmann@24219:   Pretty.writeln o CodeFuncgr.pretty thy o code_depgr thy;
haftmann@24219: 
haftmann@24219: fun code_deps thy consts =
haftmann@24219:   let
haftmann@24219:     val gr = code_depgr thy consts;
haftmann@24219:     fun mk_entry (const, (_, (_, parents))) =
haftmann@24219:       let
haftmann@24219:         val name = CodeUnit.string_of_const thy const;
haftmann@24219:         val nameparents = map (CodeUnit.string_of_const thy) parents;
haftmann@24219:       in { name = name, ID = name, dir = "", unfold = true,
haftmann@24219:         path = "", parents = nameparents }
haftmann@24219:       end;
haftmann@24423:     val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr [];
haftmann@24219:   in Present.display_graph prgr end;
haftmann@24219: 
haftmann@24844: 
haftmann@24918: (** code generation interfaces **)
haftmann@24918: 
haftmann@24918: (* code data *)
haftmann@24844: 
haftmann@24219: structure Program = CodeDataFun
haftmann@24219: (
haftmann@24219:   type T = CodeThingol.code;
haftmann@24219:   val empty = CodeThingol.empty_code;
haftmann@24219:   fun merge _ = CodeThingol.merge_code;
haftmann@24219:   fun purge _ NONE _ = CodeThingol.empty_code
haftmann@24219:     | purge NONE _ _ = CodeThingol.empty_code
haftmann@24219:     | purge (SOME thy) (SOME cs) code =
haftmann@24219:         let
haftmann@24219:           val cs_exisiting =
haftmann@24219:             map_filter (CodeName.const_rev thy) (Graph.keys code);
haftmann@24219:           val dels = (Graph.all_preds code
haftmann@24219:               o map (CodeName.const thy)
haftmann@24423:               o filter (member (op =) cs_exisiting)
haftmann@24219:             ) cs;
haftmann@24219:         in Graph.del_nodes dels code end;
haftmann@24219: );
haftmann@24219: 
haftmann@24918: (* generic generation combinators *)
haftmann@24811: 
haftmann@24918: val ensure_const = CodeThingol.ensure_const;
haftmann@24219: 
haftmann@24918: fun perhaps_const thy algbr funcgr c trns =
haftmann@24918:   case try (CodeThingol.ensure_const thy algbr funcgr c) trns
haftmann@24219:    of SOME (c, trns) => (SOME c, trns)
haftmann@24219:     | NONE => (NONE, trns);
haftmann@24219: 
haftmann@25969: fun generate thy funcgr f x =
haftmann@25969:   Program.change_yield thy (CodeThingol.transact thy funcgr
haftmann@25969:     (fn thy => fn funcgr => fn algbr => f thy funcgr algbr x));
haftmann@24219: 
haftmann@26113: (* export_code functionality *)
haftmann@26113: 
haftmann@24436: fun code thy permissive cs seris =
haftmann@24436:   let
haftmann@24436:     val code = Program.get thy;
haftmann@27000:     fun mk_seri_dest file = case file
haftmann@27000:      of NONE => CodeTarget.compile
haftmann@27000:       | SOME "-" => writeln o CodeTarget.string
haftmann@27000:       | SOME f => CodeTarget.file (Path.explode f)
haftmann@27000:     val _ = map (fn (((target, module), file), args) =>
haftmann@27000:       (mk_seri_dest file (CodeTarget.serialize thy target permissive module args code cs))) seris;
haftmann@27000:   in () end;
haftmann@24436: 
haftmann@26113: (* evaluation machinery *)
haftmann@26113: 
haftmann@26740: fun evaluate eval_kind thy evaluator =
haftmann@24250:   let
haftmann@26740:     fun evaluator'' evaluator''' funcgr t =
haftmann@26740:       let
haftmann@26740:         val ((code, (vs_ty_t, deps)), _) =
haftmann@26740:           generate thy funcgr CodeThingol.ensure_value t;
haftmann@26740:       in evaluator''' code vs_ty_t deps end;
haftmann@26740:     fun evaluator' t =
haftmann@26740:       let
haftmann@26740:         val (t', evaluator''') = evaluator t;
haftmann@26740:       in (t', evaluator'' evaluator''') end;
haftmann@26740:   in eval_kind thy evaluator' end
haftmann@26011: 
haftmann@26740: fun evaluate_conv thy = evaluate CodeFuncgr.eval_conv thy;
haftmann@26740: fun evaluate_term thy = evaluate CodeFuncgr.eval_term thy;
haftmann@26011: 
haftmann@26740: fun eval_ml reff args thy code ((vs, ty), t) deps =
haftmann@26011:   CodeTarget.eval thy reff code (t, ty) args;
haftmann@24219: 
haftmann@26011: fun eval evaluate term_of reff thy ct args =
haftmann@26011:   let
haftmann@26011:     val _ = if null (term_frees (term_of ct)) then () else error ("Term "
wenzelm@26939:       ^ quote (Syntax.string_of_term_global thy (term_of ct))
haftmann@26740:       ^ " to be evaluated contains free variables");
haftmann@26740:   in evaluate thy (fn t => (t, eval_ml reff args thy)) ct end;
haftmann@26011: 
haftmann@26011: fun eval_conv reff = eval evaluate_conv Thm.term_of reff;
haftmann@26011: fun eval_term reff = eval evaluate_term I reff;
haftmann@24219: 
haftmann@24585: val satisfies_ref : (unit -> bool) option ref = ref NONE;
haftmann@24219: 
haftmann@26011: val satisfies = eval_term ("CodePackage.satisfies_ref", satisfies_ref);
haftmann@24219: 
haftmann@26113: (* code antiquotation *)
haftmann@26113: 
haftmann@26113: fun code_antiq (ctxt, args) = 
haftmann@26113:   let
haftmann@26113:     val thy = Context.theory_of ctxt;
haftmann@26113:     val (ts, (ctxt', args')) = Scan.repeat1 Args.term (ctxt, args);
haftmann@26113:     val cs = map (CodeUnit.check_const thy) ts;
haftmann@26113:     val (cs', code') = generate thy (CodeFuncgr.make thy cs)
haftmann@26113:       (fold_map ooo ensure_const) cs;
haftmann@27000:     val code'' = CodeTarget.sml_of thy code' cs' ^ " ()";
haftmann@26113:   in (("codevals", code''), (ctxt', args')) end;
haftmann@26113: 
haftmann@26113: 
haftmann@26113: (* const expressions *)
haftmann@26113: 
wenzelm@26615: local
wenzelm@26615: 
wenzelm@26615: fun consts_of thy some_thyname =
wenzelm@26615:   let
wenzelm@26615:     val this_thy = Option.map ThyInfo.get_theory some_thyname |> the_default thy;
wenzelm@26615:     val raw_cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
wenzelm@26615:       ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) this_thy) [];
wenzelm@26615:     val cs = map (CodeUnit.subst_alias thy) raw_cs;
wenzelm@26615:     fun belongs_here thyname c =
wenzelm@26615:       not (exists (fn thy' => Sign.declared_const thy' c) (Theory.parents_of this_thy))
wenzelm@26615:   in case some_thyname
wenzelm@26615:    of NONE => cs
wenzelm@26615:     | SOME thyname => filter (belongs_here thyname) cs
wenzelm@26615:   end;
wenzelm@26615: 
wenzelm@26615: fun read_const_expr thy "*" = ([], consts_of thy NONE)
wenzelm@26615:   | read_const_expr thy s = if String.isSuffix ".*" s
wenzelm@26615:       then ([], consts_of thy (SOME (unsuffix ".*" s)))
wenzelm@26615:       else ([CodeUnit.read_const thy s], []);
wenzelm@26615: 
wenzelm@26615: in
wenzelm@26615: 
wenzelm@26615: fun read_const_exprs thy select exprs =
wenzelm@26615:   case (pairself flat o split_list o map (read_const_expr thy)) exprs
wenzelm@26615:    of (consts, []) => (false, consts)
wenzelm@26615:     | (consts, consts') => (true, consts @ select consts');
wenzelm@26615: 
wenzelm@26615: end; (*local*)
wenzelm@26615: 
haftmann@24219: fun filter_generatable thy consts =
haftmann@24219:   let
haftmann@24283:     val (consts', funcgr) = CodeFuncgr.make_consts thy consts;
haftmann@24918:     val (consts'', _) = generate thy funcgr (fold_map ooo perhaps_const) consts';
haftmann@24219:     val consts''' = map_filter (fn (const, SOME _) => SOME const | (_, NONE) => NONE)
haftmann@24219:       (consts' ~~ consts'');
haftmann@24219:   in consts''' end;
haftmann@24219: 
haftmann@24436: fun generate_const_exprs thy raw_cs =
haftmann@24436:   let
wenzelm@26615:     val (perm1, cs) = read_const_exprs thy
haftmann@24436:       (filter_generatable thy) raw_cs;
haftmann@24436:     val (perm2, cs') = case generate thy (CodeFuncgr.make thy cs)
haftmann@24918:       (fold_map ooo ensure_const) cs
haftmann@24918:      of ([], _) => (true, NONE)
haftmann@24918:       | (cs, _) => (false, SOME cs);
haftmann@24436:   in (perm1 orelse perm2, cs') end;
haftmann@24436: 
haftmann@24436: 
haftmann@24436: (** code properties **)
haftmann@24436: 
haftmann@24436: fun mk_codeprops thy all_cs sel_cs =
haftmann@24436:   let
wenzelm@24976:     fun select (thmref, thm) = case try (Thm.unvarify o Drule.zero_var_indexes) thm
haftmann@24436:      of NONE => NONE
haftmann@24436:       | SOME thm => let
haftmann@24436:           val t = (ObjectLogic.drop_judgment thy o Thm.prop_of) thm;
haftmann@24436:           val cs = fold_aterms (fn Const (c, ty) =>
haftmann@25597:             cons (AxClass.unoverload_const thy (c, ty)) | _ => I) t [];
haftmann@24436:         in if exists (member (op =) sel_cs) cs
haftmann@24436:           andalso forall (member (op =) all_cs) cs
haftmann@24436:           then SOME (thmref, thm) else NONE end;
haftmann@24436:     fun mk_codeprop (thmref, thm) =
haftmann@24436:       let
haftmann@24436:         val t = ObjectLogic.drop_judgment thy (Thm.prop_of thm);
haftmann@24436:         val ty_judg = fastype_of t;
haftmann@24436:         val tfrees1 = fold_aterms (fn Const (c, ty) =>
haftmann@24436:           Term.add_tfreesT ty | _ => I) t [];
haftmann@24436:         val vars = Term.add_frees t [];
haftmann@24436:         val tfrees2 = fold (Term.add_tfreesT o snd) vars [];
haftmann@24436:         val tfrees' = subtract (op =) tfrees2 tfrees1 |> map TFree;
haftmann@24436:         val ty = map Term.itselfT tfrees' @ map snd vars ---> ty_judg;
haftmann@24436:         val tfree_vars = map Logic.mk_type tfrees';
wenzelm@26336:         val c = Facts.string_of_ref thmref
haftmann@24436:           |> NameSpace.explode
haftmann@24436:           |> (fn [x] => [x] | (x::xs) => xs)
haftmann@24436:           |> space_implode "_"
haftmann@24436:         val propdef = (((c, ty), tfree_vars @ map Free vars), t);
haftmann@24436:       in if c = "" then NONE else SOME (thmref, propdef) end;
haftmann@24436:   in
wenzelm@26690:     Facts.dest_static (PureThy.facts_of thy)
wenzelm@26336:     |> maps Facts.selections
haftmann@24436:     |> map_filter select
haftmann@24436:     |> map_filter mk_codeprop
haftmann@24436:   end;
haftmann@24436: 
haftmann@24436: fun add_codeprops all_cs sel_cs thy =
haftmann@24436:   let
haftmann@24436:     val codeprops = mk_codeprops thy all_cs sel_cs;
haftmann@24436:     fun lift_name_yield f x = (Name.context, x) |> f ||> snd;
haftmann@24436:     fun add (thmref, (((raw_c, ty), ts), t)) (names, thy) =
haftmann@24436:       let
wenzelm@26336:         val _ = warning ("Adding theorem " ^ quote (Facts.string_of_ref thmref)
haftmann@24436:           ^ " as code property " ^ quote raw_c);
haftmann@24436:         val ([raw_c'], names') = Name.variants [raw_c] names;
wenzelm@24971:         val (const as Const (c, _), thy') = thy |> Sign.declare_const [] (raw_c', ty, NoSyn);
wenzelm@24971:         val eq = Logic.mk_equals (list_comb (const, ts), t);
wenzelm@24971:         val ([def], thy'') = thy' |> PureThy.add_defs_i false [((Thm.def_name raw_c', eq), [])];
wenzelm@24971:       in ((c, def), (names', thy'')) end;
haftmann@24436:   in
haftmann@24436:     thy
haftmann@24436:     |> Sign.sticky_prefix "codeprop"
haftmann@24436:     |> lift_name_yield (fold_map add codeprops)
haftmann@24436:     ||> Sign.restore_naming thy
haftmann@24621:     |-> (fn c_thms => fold (Code.add_func o snd) c_thms #> pair c_thms)
haftmann@24436:   end;
haftmann@24436: 
haftmann@24436: 
haftmann@24918: (** interfaces and Isar setup **)
haftmann@24219: 
haftmann@24219: local
haftmann@24219: 
haftmann@24219: structure P = OuterParse
haftmann@24219: and K = OuterKeyword
haftmann@24219: 
haftmann@24436: fun code_cmd raw_cs seris thy =
haftmann@24219:   let
haftmann@24436:     val (permissive, cs) = generate_const_exprs thy raw_cs;
haftmann@24436:     val _ = code thy permissive cs seris;
haftmann@24436:   in () end;
haftmann@24219: 
haftmann@24219: fun code_thms_cmd thy =
wenzelm@26615:   code_thms thy o snd o read_const_exprs thy (fst o CodeFuncgr.make_consts thy);
haftmann@24219: 
haftmann@24219: fun code_deps_cmd thy =
wenzelm@26615:   code_deps thy o snd o read_const_exprs thy (fst o CodeFuncgr.make_consts thy);
haftmann@24219: 
haftmann@24436: fun code_props_cmd raw_cs seris thy =
haftmann@24436:   let
haftmann@24436:     val (_, all_cs) = generate_const_exprs thy ["*"];
haftmann@24436:     val (permissive, cs) = generate_const_exprs thy raw_cs;
haftmann@24436:     val (c_thms, thy') = add_codeprops (map (the o CodeName.const_rev thy) (these all_cs))
haftmann@24436:       (map (the o CodeName.const_rev thy) (these cs)) thy;
haftmann@24436:     val prop_cs = (filter_generatable thy' o map fst) c_thms;
haftmann@24918:     val _ = if null seris then () else (generate thy' (CodeFuncgr.make thy' prop_cs)
haftmann@24918:       (fold_map ooo ensure_const) prop_cs; ());
haftmann@24436:     val _ = if null seris then () else code thy' permissive
haftmann@24436:       (SOME (map (CodeName.const thy') prop_cs)) seris;
haftmann@24436:   in thy' end;
haftmann@24436: 
haftmann@24250: val (inK, module_nameK, fileK) = ("in", "module_name", "file");
haftmann@24219: 
haftmann@24436: fun code_exprP cmd =
haftmann@24219:   (Scan.repeat P.term
haftmann@24219:   -- Scan.repeat (P.$$$ inK |-- P.name
haftmann@24250:      -- Scan.option (P.$$$ module_nameK |-- P.name)
haftmann@24219:      -- Scan.option (P.$$$ fileK |-- P.name)
haftmann@24219:      -- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") []
haftmann@24436:   ) >> (fn (raw_cs, seris) => cmd raw_cs seris));
haftmann@24219: 
wenzelm@24867: val _ = OuterSyntax.keywords [inK, module_nameK, fileK];
haftmann@24219: 
haftmann@24436: val (codeK, code_thmsK, code_depsK, code_propsK) =
haftmann@24436:   ("export_code", "code_thms", "code_deps", "code_props");
haftmann@24219: 
haftmann@24219: in
haftmann@24219: 
wenzelm@24867: val _ =
wenzelm@25110:   OuterSyntax.command codeK "generate executable code for constants"
haftmann@24436:     K.diag (P.!!! (code_exprP code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
haftmann@24219: 
wenzelm@26604: fun codegen_shell_command thyname cmd = Toplevel.program (fn _ =>
haftmann@25611:   (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! (code_exprP code_cmd)) ((filter OuterLex.is_proper o OuterSyntax.scan) cmd)
haftmann@25611:    of SOME f => (writeln "Now generating code..."; f (theory thyname))
haftmann@25611:     | NONE => error ("Bad directive " ^ quote cmd)))
haftmann@25611:   handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
haftmann@24219: 
wenzelm@24867: val _ =
haftmann@24219:   OuterSyntax.improper_command code_thmsK "print system of defining equations for code" OuterKeyword.diag
haftmann@24219:     (Scan.repeat P.term
haftmann@24219:       >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
haftmann@24219:         o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
haftmann@24219: 
wenzelm@24867: val _ =
haftmann@24219:   OuterSyntax.improper_command code_depsK "visualize dependencies of defining equations for code" OuterKeyword.diag
haftmann@24219:     (Scan.repeat P.term
haftmann@24219:       >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
haftmann@24219:         o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
haftmann@24219: 
wenzelm@24867: val _ =
haftmann@24436:   OuterSyntax.command code_propsK "generate characteristic properties for executable constants"
haftmann@24436:     K.thy_decl (P.!!! (code_exprP code_props_cmd) >> Toplevel.theory);
haftmann@24219: 
haftmann@26113: val _ = ML_Context.value_antiq "code" code_antiq;
haftmann@26113: 
haftmann@24436: end; (*local*)
haftmann@24436: 
haftmann@24436: end; (*struct*)