haftmann@37745: (*  Title:      Tools/Code/code_target.ML
haftmann@24219:     Author:     Florian Haftmann, TU Muenchen
haftmann@24219: 
haftmann@38910: Generic infrastructure for target language data.
haftmann@24219: *)
haftmann@24219: 
haftmann@24219: signature CODE_TARGET =
haftmann@24219: sig
haftmann@55757:   val cert_tyco: Proof.context -> string -> string
haftmann@55757:   val read_tyco: Proof.context -> string -> string
haftmann@36471: 
haftmann@55757:   val export_code_for: Proof.context -> Path.T option -> string -> int option -> string -> Token.T list
haftmann@55683:     -> Code_Thingol.program -> bool -> Code_Symbol.T list -> unit
haftmann@55757:   val produce_code_for: Proof.context -> string -> int option -> string -> Token.T list
haftmann@55683:     -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string * string) list * string option list
haftmann@55757:   val present_code_for: Proof.context -> string -> int option -> string -> Token.T list
haftmann@55150:     -> Code_Thingol.program -> Code_Symbol.T list * Code_Symbol.T list -> string
haftmann@55757:   val check_code_for: Proof.context -> string -> bool -> Token.T list
haftmann@55683:     -> Code_Thingol.program -> bool -> Code_Symbol.T list -> unit
haftmann@38918: 
haftmann@55757:   val export_code: Proof.context -> bool -> string list
haftmann@38933:     -> (((string * string) * Path.T option) * Token.T list) list -> unit
haftmann@55757:   val produce_code: Proof.context -> bool -> string list
haftmann@48568:     -> string -> int option -> string -> Token.T list -> (string * string) list * string option list
haftmann@55757:   val present_code: Proof.context -> string list -> Code_Symbol.T list
haftmann@38933:     -> string -> int option -> string -> Token.T list -> string
haftmann@55757:   val check_code: Proof.context -> bool -> string list
haftmann@38918:     -> ((string * bool) * Token.T list) list -> unit
haftmann@38918: 
haftmann@48568:   val generatedN: string
haftmann@55757:   val evaluator: Proof.context -> string -> Code_Thingol.program
haftmann@55684:     -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
haftmann@48568:     -> (string * string) list * string
haftmann@41344: 
haftmann@28054:   type serializer
haftmann@34152:   type literals = Code_Printer.literals
haftmann@59104:   type language
haftmann@59104:   type ancestry
haftmann@59479:   val assert_target: theory -> string -> string
haftmann@59104:   val add_language: string * language -> theory -> theory
haftmann@59104:   val add_derived_target: string * ancestry -> theory -> theory
haftmann@55757:   val the_literals: Proof.context -> string -> literals
haftmann@28054:   type serialization
wenzelm@36959:   val parse_args: 'a parser -> Token.T list -> 'a
haftmann@38916:   val serialization: (int -> Path.T option -> 'a -> unit)
haftmann@55150:     -> (Code_Symbol.T list -> int -> 'a -> (string * string) list * (Code_Symbol.T -> string option))
haftmann@38925:     -> 'a -> serialization
haftmann@59324:   val default_code_width: int Config.T
haftmann@38917: 
haftmann@52137:   type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl
haftmann@52138:   val set_identifiers: (string, string, string, string, string, string) symbol_attr_decl
haftmann@52138:     -> theory -> theory
haftmann@55372:   val set_printings: (Code_Printer.raw_const_syntax, Code_Printer.tyco_syntax, string, unit, unit, (string * string list)) symbol_attr_decl
haftmann@52137:     -> theory -> theory
haftmann@28054:   val add_reserved: string -> string -> theory -> theory
haftmann@24219: end;
haftmann@24219: 
haftmann@28054: structure Code_Target : CODE_TARGET =
haftmann@24219: struct
haftmann@24219: 
haftmann@55150: open Basic_Code_Symbol;
haftmann@28054: open Basic_Code_Thingol;
haftmann@34152: 
haftmann@34152: type literals = Code_Printer.literals;
haftmann@52137: type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl =
haftmann@52137:   (string * (string * 'a option) list, string * (string * 'b option) list,
haftmann@52137:     class * (string * 'c option) list, (class * class) * (string * 'd option) list,
haftmann@52137:     (class * string) * (string * 'e option) list,
haftmann@52137:     string * (string * 'f option) list) Code_Symbol.attr;
haftmann@52137: 
haftmann@34152: type tyco_syntax = Code_Printer.tyco_syntax;
haftmann@55153: type raw_const_syntax = Code_Printer.raw_const_syntax;
haftmann@34152: 
haftmann@24219: 
haftmann@52377: (** checking and parsing of symbols **)
haftmann@52377: 
haftmann@55757: fun cert_const ctxt const =
haftmann@52377:   let
haftmann@55757:     val _ = if Sign.declared_const (Proof_Context.theory_of ctxt) const then ()
haftmann@52377:       else error ("No such constant: " ^ quote const);
haftmann@52377:   in const end;
haftmann@52377: 
haftmann@55757: fun read_const ctxt = Code.read_const (Proof_Context.theory_of ctxt);
haftmann@55757: 
haftmann@55757: fun cert_tyco ctxt tyco =
haftmann@52377:   let
haftmann@55757:     val _ = if Sign.declared_tyname (Proof_Context.theory_of ctxt) tyco then ()
haftmann@52377:       else error ("No such type constructor: " ^ quote tyco);
haftmann@52377:   in tyco end;
haftmann@52377: 
wenzelm@55951: fun read_tyco ctxt =
wenzelm@56002:   #1 o dest_Type o Proof_Context.read_type_name {proper = true, strict = true} ctxt;
haftmann@52377: 
haftmann@55757: fun cert_class ctxt class =
haftmann@52377:   let
haftmann@55757:     val _ = Axclass.get_info (Proof_Context.theory_of ctxt) class;
haftmann@52377:   in class end;
haftmann@52377: 
haftmann@52377: val parse_classrel_ident = Parse.class --| @{keyword "<"} -- Parse.class;
haftmann@52377: 
haftmann@55757: fun cert_inst ctxt (class, tyco) =
haftmann@55757:   (cert_class ctxt class, cert_tyco ctxt tyco);
haftmann@52377: 
haftmann@55757: fun read_inst ctxt (raw_tyco, raw_class) =
haftmann@55757:   (read_tyco ctxt raw_tyco, Proof_Context.read_class ctxt raw_class);
haftmann@52377: 
haftmann@52377: val parse_inst_ident = Parse.xname --| @{keyword "::"} -- Parse.class;
haftmann@52377: 
haftmann@55757: fun cert_syms ctxt =
haftmann@55757:   Code_Symbol.map_attr (apfst (cert_const ctxt)) (apfst (cert_tyco ctxt))
wenzelm@59058:     (apfst (cert_class ctxt)) ((apfst o apply2) (cert_class ctxt)) (apfst (cert_inst ctxt)) I;
haftmann@52377: 
haftmann@55757: fun read_syms ctxt =
haftmann@55757:   Code_Symbol.map_attr (apfst (read_const ctxt)) (apfst (read_tyco ctxt))
wenzelm@59058:     (apfst (Proof_Context.read_class ctxt)) ((apfst o apply2) (Proof_Context.read_class ctxt)) (apfst (read_inst ctxt)) I;
haftmann@52377: 
haftmann@52377: fun check_name is_module s =
haftmann@52377:   let
haftmann@52377:     val _ = if s = "" then error "Bad empty code name" else ();
haftmann@52377:     val xs = Long_Name.explode s;
haftmann@52377:     val xs' = if is_module
haftmann@56826:         then map (Name.desymbolize NONE) xs
haftmann@52377:       else if length xs < 2
haftmann@52377:         then error ("Bad code name without module component: " ^ quote s)
haftmann@52377:       else
haftmann@52377:         let
haftmann@52377:           val (ys, y) = split_last xs;
haftmann@56826:           val ys' = map (Name.desymbolize NONE) ys;
haftmann@56826:           val y' = Name.desymbolize NONE y;
haftmann@52377:         in ys' @ [y'] end;
haftmann@52377:   in if xs' = xs
haftmann@55291:     then if is_module then (xs, "") else split_last xs
haftmann@52377:     else error ("Invalid code name: " ^ quote s ^ "\n"
haftmann@52377:       ^ "better try " ^ quote (Long_Name.implode xs'))
haftmann@52377:   end;
haftmann@52377: 
haftmann@52377: 
haftmann@52137: (** serializations and serializer **)
haftmann@52137: 
haftmann@52137: (* serialization: abstract nonsense to cover different destinies for generated code *)
haftmann@24219: 
haftmann@55150: datatype destination = Export of Path.T option | Produce | Present of Code_Symbol.T list;
haftmann@55150: type serialization = int -> destination -> ((string * string) list * (Code_Symbol.T -> string option)) option;
haftmann@27014: 
haftmann@39659: fun serialization output _ content width (Export some_path) =
haftmann@39661:       (output width some_path content; NONE)
haftmann@39661:   | serialization _ string content width Produce =
haftmann@39661:       string [] width content |> SOME
haftmann@55147:   | serialization _ string content width (Present syms) =
haftmann@55147:      string syms width content
wenzelm@59430:      |> (apfst o map o apsnd) Output.output
haftmann@39661:      |> SOME;
haftmann@39659: 
haftmann@39661: fun export some_path f = (f (Export some_path); ());
haftmann@39661: fun produce f = the (f Produce);
haftmann@55147: fun present syms f = space_implode "\n\n" (map snd (fst (the (f (Present syms)))));
haftmann@38917: 
haftmann@24219: 
haftmann@52137: (* serializers: functions producing serializations *)
haftmann@28054: 
haftmann@39142: type serializer = Token.T list
haftmann@52138:   -> Proof.context
haftmann@39142:   -> {
haftmann@52138:     module_name: string,
haftmann@38926:     reserved_syms: string list,
haftmann@59103:     identifiers: Code_Printer.identifiers,
haftmann@38926:     includes: (string * Pretty.T) list,
haftmann@38926:     class_syntax: string -> string option,
haftmann@38926:     tyco_syntax: string -> Code_Printer.tyco_syntax option,
haftmann@55153:     const_syntax: string -> Code_Printer.const_syntax option }
haftmann@55683:   -> Code_Symbol.T list
haftmann@41342:   -> Code_Thingol.program
haftmann@28054:   -> serialization;
haftmann@27000: 
haftmann@59102:   
haftmann@52137: (** theory data **)
haftmann@52137: 
haftmann@59102: type language = { serializer: serializer, literals: literals,
haftmann@59102:   check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } }; 
haftmann@59102: 
haftmann@59103: type ancestry = (string * (Code_Thingol.program -> Code_Thingol.program)) list;
haftmann@27103: 
haftmann@59103: val merge_ancestry : ancestry * ancestry -> ancestry = AList.join (op =) (K snd);
haftmann@27103: 
haftmann@59103: type target = { serial: serial, language: language, ancestry: ancestry };
haftmann@27437: 
haftmann@34248: structure Targets = Theory_Data
haftmann@34071: (
haftmann@59324:   type T = (target * Code_Printer.data) Symtab.table;
haftmann@59324:   val empty = Symtab.empty;
haftmann@34071:   val extend = I;
haftmann@59324:   fun merge (targets1, targets2) : T =
haftmann@59324:     Symtab.join (fn target_name => fn ((target1, data1), (target2, data2)) =>
haftmann@59103:       if #serial target1 = #serial target2 then
haftmann@59103:       ({ serial = #serial target1, language = #language target1,
haftmann@59103:         ancestry = merge_ancestry (#ancestry target1, #ancestry target2)},
haftmann@59103:         Code_Printer.merge_data (data1, data2))
haftmann@59102:       else error ("Incompatible targets: " ^ quote target_name) 
haftmann@59324:     ) (targets1, targets2)
haftmann@34071: );
haftmann@27436: 
haftmann@59324: fun exists_target thy = Symtab.defined (Targets.get thy);
haftmann@59324: fun lookup_target_data thy = Symtab.lookup (Targets.get thy);
haftmann@59479: fun assert_target thy target_name =
haftmann@59479:   if exists_target thy target_name
haftmann@59479:   then target_name
haftmann@59479:   else error ("Unknown code target language: " ^ quote target_name);
haftmann@59100: 
haftmann@59104: fun fold1 f xs = fold f (tl xs) (hd xs);
haftmann@59104: 
haftmann@59101: fun join_ancestry thy target_name =
haftmann@59101:   let
haftmann@59479:     val _ = assert_target thy target_name; 
haftmann@59103:     val the_target_data = the o lookup_target_data thy;
haftmann@59103:     val (target, this_data) = the_target_data target_name;
haftmann@59103:     val ancestry = #ancestry target;
haftmann@59102:     val modifies = rev (map snd ancestry);
haftmann@59102:     val modify = fold (curry (op o)) modifies I;
haftmann@59103:     val datas = rev (map (snd o the_target_data o fst) ancestry) @ [this_data];
haftmann@59104:     val data = fold1 (fn data' => fn data => Code_Printer.merge_data (data, data')) datas;
haftmann@59103:   in (modify, (target, data)) end;
haftmann@59101: 
haftmann@59479:   fun allocate_target target_name target thy =
haftmann@27304:   let
haftmann@59101:     val _ = if exists_target thy target_name
haftmann@59101:       then error ("Attempt to overwrite existing target " ^ quote target_name)
wenzelm@43564:       else ();
haftmann@28054:   in
haftmann@28054:     thy
haftmann@59324:     |> (Targets.map o Symtab.update) (target_name, (target, Code_Printer.empty_data))  
haftmann@28054:   end;
haftmann@27436: 
haftmann@59104: fun add_language (target_name, language) =
haftmann@59102:   allocate_target target_name { serial = serial (), language = language, ancestry = [] };
haftmann@27436: 
haftmann@59104: fun add_derived_target (target_name, initial_ancestry) thy =
haftmann@59101:   let
haftmann@59104:     val _ = if null initial_ancestry
haftmann@59104:       then error "Must derive from existing target(s)" else ();
haftmann@59104:     fun the_target_data target_name' = case lookup_target_data thy target_name' of
haftmann@59104:       NONE => error ("Unknown code target language: " ^ quote target_name')
haftmann@59104:     | SOME target_data' => target_data';
haftmann@59104:     val targets = rev (map (fst o the_target_data o fst) initial_ancestry);
haftmann@59104:     val supremum = fold1 (fn target' => fn target =>
haftmann@59104:       if #serial target = #serial target'
haftmann@59104:       then target else error "Incompatible targets") targets;
haftmann@59104:     val ancestries = map #ancestry targets @ [initial_ancestry];
haftmann@59104:     val ancestry = fold1 (fn ancestry' => fn ancestry =>
haftmann@59104:       merge_ancestry (ancestry, ancestry')) ancestries;
haftmann@59101:   in
haftmann@59104:     allocate_target target_name { serial = #serial supremum, language = #language supremum,
haftmann@59104:       ancestry = ancestry } thy 
haftmann@59101:   end;
haftmann@59101:   
haftmann@59102: fun map_data target_name f thy =
haftmann@27436:   let
haftmann@59479:     val _ = assert_target thy target_name;
haftmann@28054:   in
haftmann@28054:     thy
haftmann@59324:     |> (Targets.map o Symtab.map_entry target_name o apsnd o Code_Printer.map_data) f
haftmann@28054:   end;
haftmann@27304: 
haftmann@59099: fun map_reserved target_name =
haftmann@59102:   map_data target_name o @{apply 3 (1)};
haftmann@59099: fun map_identifiers target_name =
haftmann@59102:   map_data target_name o @{apply 3 (2)};
haftmann@59099: fun map_printings target_name =
haftmann@59102:   map_data target_name o @{apply 3 (3)};
haftmann@27000: 
haftmann@27000: 
haftmann@34021: (** serializer usage **)
haftmann@34021: 
haftmann@59324: (* technical aside: pretty printing width *)
haftmann@59324: 
haftmann@59324: val default_code_width = Attrib.setup_config_int @{binding "default_code_width"} (K 80);
haftmann@59324: 
haftmann@59324: 
haftmann@34021: (* montage *)
haftmann@34021: 
haftmann@59102: fun the_language ctxt =
haftmann@59103:   #language o fst o the o lookup_target_data (Proof_Context.theory_of ctxt);
haftmann@37822: 
haftmann@59102: fun the_literals ctxt = #literals o the_language ctxt;
haftmann@34021: 
haftmann@39817: local
haftmann@39817: 
haftmann@59099: fun activate_target ctxt target_name =
haftmann@39817:   let
haftmann@59324:     val thy = Proof_Context.theory_of ctxt;
haftmann@59103:     val (modify, target_data) = join_ancestry thy target_name;
haftmann@59324:   in (target_data, modify) end;
haftmann@38927: 
haftmann@55757: fun project_program ctxt syms_hidden syms1 program2 =
haftmann@38927:   let
haftmann@55147:     val syms2 = subtract (op =) syms_hidden syms1;
haftmann@55147:     val program3 = Code_Symbol.Graph.restrict (not o member (op =) syms_hidden) program2;
haftmann@55147:     val syms4 = Code_Symbol.Graph.all_succs program3 syms2;
haftmann@54890:     val unimplemented = Code_Thingol.unimplemented program3;
wenzelm@42359:     val _ =
haftmann@54889:       if null unimplemented then ()
wenzelm@42359:       else error ("No code equations for " ^
wenzelm@55304:         commas (map (Proof_Context.markup_const ctxt) unimplemented));
haftmann@55147:     val program4 = Code_Symbol.Graph.restrict (member (op =) syms4) program3;
haftmann@55147:   in (syms4, program4) end;
haftmann@38927: 
haftmann@55757: fun prepare_serializer ctxt (serializer : serializer) reserved identifiers
haftmann@55147:     printings module_name args proto_program syms =
haftmann@38927:   let
haftmann@55149:     val syms_hidden = Code_Symbol.symbols_of printings;
haftmann@55757:     val (syms_all, program) = project_program ctxt syms_hidden syms proto_program;
haftmann@39484:     fun select_include (name, (content, cs)) =
haftmann@55150:       if null cs orelse exists (fn c => member (op =) syms_all (Constant c)) cs
haftmann@39484:       then SOME (name, content) else NONE;
haftmann@52137:     val includes = map_filter select_include (Code_Symbol.dest_module_data printings);
haftmann@34021:   in
haftmann@55757:     (serializer args ctxt {
haftmann@52138:       module_name = module_name,
haftmann@38926:       reserved_syms = reserved,
haftmann@52138:       identifiers = identifiers,
haftmann@38926:       includes = includes,
haftmann@55149:       const_syntax = Code_Symbol.lookup_constant_data printings,
haftmann@55149:       tyco_syntax = Code_Symbol.lookup_type_constructor_data printings,
haftmann@55149:       class_syntax = Code_Symbol.lookup_type_class_data printings },
haftmann@55776:       (subtract (op =) syms_hidden syms, program))
haftmann@34021:   end;
haftmann@34021: 
haftmann@59099: fun mount_serializer ctxt target_name some_width module_name args program syms =
haftmann@34021:   let
haftmann@59324:     val default_width = Config.get ctxt default_code_width;
haftmann@59324:     val ((target, data), modify) = activate_target ctxt target_name;
haftmann@59103:     val serializer = (#serializer o #language) target;
haftmann@55683:     val (prepared_serializer, (prepared_syms, prepared_program)) =
haftmann@55757:       prepare_serializer ctxt serializer
haftmann@59103:         (Code_Printer.the_reserved data) (Code_Printer.the_identifiers data)
haftmann@59103:         (Code_Printer.the_printings data)
haftmann@55147:         module_name args (modify program) syms
haftmann@34071:     val width = the_default default_width some_width;
haftmann@55683:   in (fn program => fn syms => prepared_serializer syms program width, (prepared_syms, prepared_program)) end;
haftmann@41344: 
haftmann@59099: fun invoke_serializer ctxt target_name some_width raw_module_name args program all_public syms =
haftmann@41344:   let
haftmann@55291:     val module_name = if raw_module_name = "" then ""
haftmann@55291:       else (check_name true raw_module_name; raw_module_name)
haftmann@55757:     val (mounted_serializer, (prepared_syms, prepared_program)) =
haftmann@59099:       mount_serializer ctxt target_name some_width module_name args program syms;
haftmann@55776:   in mounted_serializer prepared_program (if all_public then [] else prepared_syms) end;
haftmann@34021: 
haftmann@52138: fun assert_module_name "" = error "Empty module name not allowed here"
haftmann@38933:   | assert_module_name module_name = module_name;
haftmann@38933: 
haftmann@55757: fun using_master_directory ctxt =
wenzelm@56208:   Option.map (Path.append (File.pwd ()) o
wenzelm@56208:     Path.append (Resources.master_directory (Proof_Context.theory_of ctxt)));
haftmann@48371: 
haftmann@34021: in
haftmann@34021: 
haftmann@48568: val generatedN = "Generated_Code";
haftmann@48568: 
haftmann@59099: fun export_code_for ctxt some_path target_name some_width module_name args =
haftmann@55757:   export (using_master_directory ctxt some_path)
haftmann@59099:   ooo invoke_serializer ctxt target_name some_width module_name args;
haftmann@38918: 
haftmann@59099: fun produce_code_for ctxt target_name some_width module_name args =
haftmann@39102:   let
haftmann@59099:     val serializer = invoke_serializer ctxt target_name some_width (assert_module_name module_name) args;
haftmann@55683:   in fn program => fn all_public => fn syms =>
haftmann@55683:     produce (serializer program all_public syms) |> apsnd (fn deresolve => map deresolve syms)
haftmann@39484:   end;
haftmann@38929: 
haftmann@59099: fun present_code_for ctxt target_name some_width module_name args =
haftmann@39484:   let
haftmann@59099:     val serializer = invoke_serializer ctxt target_name some_width (assert_module_name module_name) args;
haftmann@55147:   in fn program => fn (syms, selects) =>
haftmann@55683:     present selects (serializer program false syms)
haftmann@39484:   end;
haftmann@38918: 
haftmann@59099: fun check_code_for ctxt target_name strict args program all_public syms =
haftmann@37824:   let
haftmann@37824:     val { env_var, make_destination, make_command } =
haftmann@59102:       (#check o the_language ctxt) target_name;
wenzelm@41939:     fun ext_check p =
wenzelm@43564:       let
haftmann@37824:         val destination = make_destination p;
haftmann@59099:         val _ = export (SOME destination) (invoke_serializer ctxt target_name (SOME 80)
haftmann@55683:           generatedN args program all_public syms);
haftmann@48568:         val cmd = make_command generatedN;
wenzelm@43850:       in
wenzelm@43850:         if Isabelle_System.bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
haftmann@59099:         then error ("Code check failed for " ^ target_name ^ ": " ^ cmd)
haftmann@37824:         else ()
haftmann@37824:       end;
wenzelm@43850:   in
wenzelm@43850:     if getenv env_var = ""
haftmann@37825:     then if strict
haftmann@59099:       then error (env_var ^ " not set; cannot check code for " ^ target_name)
haftmann@59099:       else warning (env_var ^ " not set; skipped checking code for " ^ target_name)
wenzelm@41939:     else Isabelle_System.with_tmp_dir "Code_Test" ext_check
haftmann@37824:   end;
haftmann@37824: 
haftmann@56920: fun subevaluator mounted_serializer prepared_program syms all_public ((vs, ty), t) =
haftmann@41344:   let
haftmann@41344:     val _ = if Code_Thingol.contains_dict_var t then
haftmann@41344:       error "Term to be evaluated contains free dictionaries" else ();
wenzelm@43324:     val v' = singleton (Name.variant_list (map fst vs)) "a";
haftmann@41344:     val vs' = (v', []) :: vs;
haftmann@55147:     val ty' = ITyVar v' `-> ty;
haftmann@41344:     val program = prepared_program
haftmann@55147:       |> Code_Symbol.Graph.new_node (Code_Symbol.value,
haftmann@57249:           Code_Thingol.Fun (((vs', ty'), [(([IVar (SOME "dummy")], t), (NONE, true))]), NONE))
haftmann@55147:       |> fold (curry (perhaps o try o
haftmann@55147:           Code_Symbol.Graph.add_edge) Code_Symbol.value) syms;
haftmann@55683:     val (program_code, deresolve) =
haftmann@55684:       produce (mounted_serializer program (if all_public then [] else [Code_Symbol.value]));
haftmann@55147:     val value_name = the (deresolve Code_Symbol.value);
haftmann@55147:   in (program_code, value_name) end;
haftmann@41344: 
haftmann@59099: fun evaluator ctxt target_name program syms =
haftmann@41344:   let
haftmann@55683:     val (mounted_serializer, (_, prepared_program)) =
haftmann@59099:       mount_serializer ctxt target_name NONE generatedN [] program syms;
haftmann@56920:   in subevaluator mounted_serializer prepared_program syms end;
haftmann@41344: 
haftmann@34021: end; (* local *)
haftmann@34021: 
haftmann@34021: 
haftmann@34021: (* code generation *)
haftmann@34021: 
haftmann@38918: fun prep_destination "" = NONE
haftmann@38918:   | prep_destination s = SOME (Path.explode s);
haftmann@38918: 
haftmann@55757: fun export_code ctxt all_public cs seris =
haftmann@34021:   let
haftmann@55757:     val thy = Proof_Context.theory_of ctxt;
haftmann@55188:     val program = Code_Thingol.consts_program thy cs;
haftmann@59099:     val _ = map (fn (((target_name, module_name), some_path), args) =>
haftmann@59099:       export_code_for ctxt some_path target_name NONE module_name args program all_public (map Constant cs)) seris;
haftmann@34021:   in () end;
haftmann@34021: 
haftmann@55757: fun export_code_cmd all_public raw_cs seris ctxt =
haftmann@55757:   export_code ctxt all_public
haftmann@55757:     (Code_Thingol.read_const_exprs ctxt raw_cs)
haftmann@55683:     ((map o apfst o apsnd) prep_destination seris);
haftmann@38918: 
haftmann@59099: fun produce_code ctxt all_public cs target_name some_width some_module_name args =
haftmann@38918:   let
haftmann@55757:     val thy = Proof_Context.theory_of ctxt;
haftmann@55188:     val program = Code_Thingol.consts_program thy cs;
haftmann@59099:   in produce_code_for ctxt target_name some_width some_module_name args program all_public (map Constant cs) end;
haftmann@38929: 
haftmann@59099: fun present_code ctxt cs syms target_name some_width some_module_name args =
haftmann@38929:   let
haftmann@55757:     val thy = Proof_Context.theory_of ctxt;
haftmann@55188:     val program = Code_Thingol.consts_program thy cs;
haftmann@59099:   in present_code_for ctxt target_name some_width some_module_name args program (map Constant cs, syms) end;
haftmann@34021: 
haftmann@55757: fun check_code ctxt all_public cs seris =
haftmann@37824:   let
haftmann@55757:     val thy = Proof_Context.theory_of ctxt;
haftmann@55188:     val program = Code_Thingol.consts_program thy cs;
haftmann@59099:     val _ = map (fn ((target_name, strict), args) =>
haftmann@59099:       check_code_for ctxt target_name strict args program all_public (map Constant cs)) seris;
haftmann@37824:   in () end;
haftmann@37824: 
haftmann@55757: fun check_code_cmd all_public raw_cs seris ctxt =
haftmann@55757:   check_code ctxt all_public
haftmann@55757:     (Code_Thingol.read_const_exprs ctxt raw_cs) seris;
haftmann@37824: 
haftmann@39480: local
haftmann@39480: 
haftmann@39480: val parse_const_terms = Scan.repeat1 Args.term
haftmann@55757:   >> (fn ts => fn ctxt => map (Code.check_const (Proof_Context.theory_of ctxt)) ts);
haftmann@39480: 
haftmann@55147: fun parse_names category parse internalize mark_symbol =
haftmann@39480:   Scan.lift (Args.parens (Args.$$$ category)) |-- Scan.repeat1 parse
haftmann@55757:   >> (fn xs => fn ctxt => map (mark_symbol o internalize ctxt) xs);
wenzelm@43564: 
haftmann@39480: val parse_consts = parse_names "consts" Args.term
haftmann@55757:   (Code.check_const o Proof_Context.theory_of) Constant;
haftmann@39480: 
haftmann@39480: val parse_types = parse_names "types" (Scan.lift Args.name)
haftmann@55757:   (Sign.intern_type o Proof_Context.theory_of) Type_Constructor;
haftmann@39480: 
haftmann@39480: val parse_classes = parse_names "classes" (Scan.lift Args.name)
haftmann@55757:   (Sign.intern_class o Proof_Context.theory_of) Type_Class;
haftmann@39480: 
haftmann@39480: val parse_instances = parse_names "instances" (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name))
haftmann@55757:   (fn ctxt => fn (raw_tyco, raw_class) =>
haftmann@55757:     let
haftmann@55757:       val thy = Proof_Context.theory_of ctxt;
haftmann@55757:     in (Sign.intern_class thy raw_tyco, Sign.intern_type thy raw_class) end) Class_Instance;
haftmann@39480: 
haftmann@39480: in
haftmann@39480: 
haftmann@59323: val _ = Theory.setup
haftmann@59323:   (Thy_Output.antiquotation @{binding code_stmts}
wenzelm@43564:     (parse_const_terms --
wenzelm@43564:       Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances)
wenzelm@43564:       -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
haftmann@59099:     (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target_name, some_width)) =>
haftmann@55757:         present_code ctxt (mk_cs ctxt)
haftmann@55757:           (maps (fn f => f ctxt) mk_stmtss)
haftmann@59323:           target_name some_width "Example" []));
haftmann@39480: 
haftmann@39480: end;
haftmann@39480: 
haftmann@34021: 
haftmann@28054: (** serializer configuration **)
haftmann@27000: 
haftmann@52138: (* reserved symbol names *)
haftmann@52138: 
haftmann@59099: fun add_reserved target_name sym thy =
haftmann@52138:   let
haftmann@59103:     val (_, (_, data)) = join_ancestry thy target_name;
haftmann@59103:     val _ = if member (op =) (Code_Printer.the_reserved data) sym
haftmann@52138:       then error ("Reserved symbol " ^ quote sym ^ " already declared")
haftmann@52138:       else ();
haftmann@52138:   in
haftmann@52138:     thy
haftmann@59099:     |> map_reserved target_name (insert (op =) sym)
haftmann@52138:   end;
haftmann@52138: 
haftmann@52138: 
haftmann@52377: (* checking of syntax *)
haftmann@52138: 
haftmann@59099: fun check_const_syntax ctxt target_name c syn =
haftmann@55757:   if Code_Printer.requires_args syn > Code.args_number (Proof_Context.theory_of ctxt) c
haftmann@52137:   then error ("Too many arguments in syntax for constant " ^ quote c)
haftmann@59099:   else Code_Printer.prep_const_syntax (Proof_Context.theory_of ctxt) (the_literals ctxt target_name) c syn;
haftmann@52137: 
haftmann@59099: fun check_tyco_syntax ctxt target_name tyco syn =
haftmann@55757:   if fst syn <> Sign.arity_number (Proof_Context.theory_of ctxt) tyco
haftmann@52137:   then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
haftmann@52137:   else syn;
haftmann@34071: 
haftmann@52138: 
haftmann@52138: (* custom symbol names *)
haftmann@52138: 
wenzelm@52218: fun arrange_name_decls x =
haftmann@52138:   let
haftmann@52138:     fun arrange is_module (sym, target_names) = map (fn (target, some_name) =>
haftmann@52138:       (target, (sym, Option.map (check_name is_module) some_name))) target_names;
haftmann@52138:   in
haftmann@52138:     Code_Symbol.maps_attr' (arrange false) (arrange false) (arrange false)
wenzelm@52218:       (arrange false) (arrange false) (arrange true) x
haftmann@52138:   end;
haftmann@52138: 
haftmann@55757: fun cert_name_decls ctxt = cert_syms ctxt #> arrange_name_decls;
haftmann@52138: 
haftmann@55757: fun read_name_decls ctxt = read_syms ctxt #> arrange_name_decls;
haftmann@52138: 
haftmann@59099: fun set_identifier (target_name, sym_name) = map_identifiers target_name (Code_Symbol.set_data sym_name);
haftmann@52138: 
haftmann@52138: fun gen_set_identifiers prep_name_decl raw_name_decls thy =
haftmann@55757:   fold set_identifier (prep_name_decl (Proof_Context.init_global thy) raw_name_decls) thy;
haftmann@52138: 
haftmann@52138: val set_identifiers = gen_set_identifiers cert_name_decls;
haftmann@52138: val set_identifiers_cmd = gen_set_identifiers read_name_decls;
haftmann@52138: 
haftmann@52138: 
haftmann@52138: (* custom printings *)
haftmann@52138: 
haftmann@55757: fun arrange_printings prep_const ctxt =
haftmann@52137:   let
haftmann@52137:     fun arrange check (sym, target_syns) =
haftmann@59099:       map (fn (target_name, some_syn) =>
haftmann@59099:         (target_name, (sym, Option.map (check ctxt target_name sym) some_syn))) target_syns;
haftmann@52137:   in
haftmann@52137:     Code_Symbol.maps_attr'
haftmann@52137:       (arrange check_const_syntax) (arrange check_tyco_syntax)
haftmann@55149:         (arrange ((K o K o K) I)) (arrange ((K o K o K) I)) (arrange ((K o K o K) I))
haftmann@55757:         (arrange (fn ctxt => fn _ => fn _ => fn (raw_content, raw_cs) =>
wenzelm@59430:           (Pretty.blk (0, Pretty.fbreaks (map Code_Printer.str (split_lines raw_content))),
wenzelm@59430:             map (prep_const ctxt) raw_cs)))
haftmann@52137:   end;
haftmann@52137: 
haftmann@55757: fun cert_printings ctxt = cert_syms ctxt #> arrange_printings cert_const ctxt;
haftmann@24219: 
haftmann@55757: fun read_printings ctxt = read_syms ctxt #> arrange_printings read_const ctxt;
haftmann@52137: 
haftmann@59099: fun set_printing (target_name, sym_syn) = map_printings target_name (Code_Symbol.set_data sym_syn);
haftmann@52137: 
haftmann@52137: fun gen_set_printings prep_print_decl raw_print_decls thy =
haftmann@55757:   fold set_printing (prep_print_decl (Proof_Context.init_global thy) raw_print_decls) thy;
haftmann@52137: 
haftmann@52137: val set_printings = gen_set_printings cert_printings;
haftmann@52137: val set_printings_cmd = gen_set_printings read_printings;
haftmann@52137: 
haftmann@52137: 
haftmann@27103: (* concrete syntax *)
haftmann@27000: 
haftmann@28054: fun parse_args f args =
wenzelm@36959:   case Scan.read Token.stopper f args
haftmann@28054:    of SOME x => x
haftmann@28054:     | NONE => error "Bad serializer arguments";
haftmann@28054: 
haftmann@28054: 
haftmann@27304: (** Isar setup **)
haftmann@27103: 
haftmann@52137: fun parse_single_symbol_pragma parse_keyword parse_isa parse_target =
haftmann@52434:   parse_keyword |-- Parse.!!! (parse_isa --| (@{keyword "\<rightharpoonup>"} || @{keyword "=>"})
haftmann@52434:     -- Parse.and_list1 (@{keyword "("} |-- (Parse.name --| @{keyword ")"} -- Scan.option parse_target)));
haftmann@52137: 
haftmann@52137: fun parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module =
wenzelm@52801:   parse_single_symbol_pragma @{keyword "constant"} Parse.term parse_const
haftmann@55150:     >> Constant
haftmann@52377:   || parse_single_symbol_pragma @{keyword "type_constructor"} Parse.type_const parse_tyco
haftmann@55150:     >> Type_Constructor
haftmann@52377:   || parse_single_symbol_pragma @{keyword "type_class"} Parse.class parse_class
haftmann@55150:     >> Type_Class
haftmann@52137:   || parse_single_symbol_pragma @{keyword "class_relation"} parse_classrel_ident parse_classrel
haftmann@55150:     >> Class_Relation
haftmann@52137:   || parse_single_symbol_pragma @{keyword "class_instance"} parse_inst_ident parse_inst
haftmann@55150:     >> Class_Instance
haftmann@52137:   || parse_single_symbol_pragma @{keyword "code_module"} Parse.name parse_module
haftmann@52137:     >> Code_Symbol.Module;
haftmann@52137: 
haftmann@52137: fun parse_symbol_pragmas parse_const parse_tyco parse_class parse_classrel parse_inst parse_module =
haftmann@52137:   Parse.enum1 "|" (Parse.group (fn () => "code symbol pragma")
haftmann@52137:     (parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module));
haftmann@52137: 
wenzelm@56201: val code_expr_argsP = Scan.optional (@{keyword "("} |-- Parse.args --| @{keyword ")"}) [];
haftmann@52138: 
haftmann@55683: fun code_expr_inP all_public raw_cs =
haftmann@52434:   Scan.repeat (@{keyword "in"} |-- Parse.!!! (Parse.name
haftmann@52434:     -- Scan.optional (@{keyword "module_name"} |-- Parse.name) ""
haftmann@52434:     -- Scan.optional (@{keyword "file"} |-- Parse.name) ""
haftmann@52434:     -- code_expr_argsP))
haftmann@55683:       >> (fn seri_args => export_code_cmd all_public raw_cs seri_args);
haftmann@52434: 
haftmann@55683: fun code_expr_checkingP all_public raw_cs =
haftmann@52434:   (@{keyword "checking"} |-- Parse.!!!
haftmann@52434:     (Scan.repeat (Parse.name -- ((@{keyword "?"} |-- Scan.succeed false) || Scan.succeed true)
haftmann@52434:     -- code_expr_argsP)))
haftmann@55683:       >> (fn seri_args => check_code_cmd all_public raw_cs seri_args);
haftmann@52434: 
haftmann@55683: val code_exprP = (Scan.optional (@{keyword "open"} |-- Scan.succeed true) false
haftmann@55683:   -- Scan.repeat1 Parse.term)
haftmann@55683:   :|-- (fn (all_public, raw_cs) => (code_expr_checkingP all_public raw_cs || code_expr_inP all_public raw_cs));
haftmann@52138: 
haftmann@52138: val _ =
wenzelm@59936:   Outer_Syntax.command @{command_keyword code_reserved}
haftmann@52138:     "declare words as reserved for target language"
haftmann@52138:     (Parse.name -- Scan.repeat1 Parse.name
haftmann@52138:       >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds));
haftmann@52138: 
haftmann@52138: val _ =
wenzelm@59936:   Outer_Syntax.command @{command_keyword code_identifier} "declare mandatory names for code symbols"
haftmann@52138:     (parse_symbol_pragmas Parse.name Parse.name Parse.name Parse.name Parse.name Parse.name
haftmann@52138:       >> (Toplevel.theory o fold set_identifiers_cmd));
haftmann@52138: 
haftmann@52138: val _ =
wenzelm@59936:   Outer_Syntax.command @{command_keyword code_printing} "declare dedicated printing for code symbols"
haftmann@52137:     (parse_symbol_pragmas (Code_Printer.parse_const_syntax) (Code_Printer.parse_tyco_syntax)
haftmann@52137:       Parse.string (Parse.minus >> K ()) (Parse.minus >> K ())
haftmann@52137:       (Parse.text -- Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [])
haftmann@52137:       >> (Toplevel.theory o fold set_printings_cmd));
haftmann@52137: 
haftmann@52137: val _ =
wenzelm@59936:   Outer_Syntax.command @{command_keyword export_code} "generate executable code for constants"
haftmann@55757:     (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.context_of)));
haftmann@30494: 
haftmann@24219: end; (*struct*)