added code_reflect command
authorhaftmann
Wed Apr 28 15:17:09 2010 +0200 (2010-04-28)
changeset 36470ed9be131a4ec
parent 36469 ade0dee3a58e
child 36471 5aae37575885
added code_reflect command
src/Tools/Code/code_eval.ML
     1.1 --- a/src/Tools/Code/code_eval.ML	Wed Apr 28 14:54:17 2010 +0200
     1.2 +++ b/src/Tools/Code/code_eval.ML	Wed Apr 28 15:17:09 2010 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4    val target: string
     1.5    val eval: string option -> string * (unit -> 'a) option Unsynchronized.ref
     1.6      -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
     1.7 -  val evaluation_code: theory -> string list -> string list
     1.8 +  val evaluation_code: theory -> string -> string list -> string list
     1.9      -> string * ((string * string) list * (string * string) list)
    1.10    val setup: theory -> theory
    1.11  end;
    1.12 @@ -23,12 +23,14 @@
    1.13  
    1.14  val eval_struct_name = "Code";
    1.15  
    1.16 -fun evaluation_code thy tycos consts =
    1.17 +fun evaluation_code thy struct_name_hint tycos consts =
    1.18    let
    1.19      val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
    1.20      val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
    1.21 +    val struct_name = if struct_name_hint = "" then eval_struct_name
    1.22 +      else struct_name_hint;
    1.23      val (ml_code, target_names) = Code_ML.evaluation_code_of thy target
    1.24 -      eval_struct_name naming program (consts' @ tycos');
    1.25 +      struct_name naming program (consts' @ tycos');
    1.26      val (consts'', tycos'') = chop (length consts') target_names;
    1.27      val consts_map = map2 (fn const => fn NONE =>
    1.28          error ("Constant " ^ (quote o Code.string_of_const thy) const
    1.29 @@ -84,7 +86,8 @@
    1.30      val (struct_name', ctxt') = if struct_name = ""
    1.31        then ML_Antiquote.variant eval_struct_name ctxt
    1.32        else (struct_name, ctxt);
    1.33 -    val acc_code = Lazy.lazy (fn () => evaluation_code (ProofContext.theory_of ctxt) tycos' consts');
    1.34 +    val acc_code = Lazy.lazy
    1.35 +      (fn () => evaluation_code (ProofContext.theory_of ctxt) eval_struct_name tycos' consts');
    1.36    in CodeAntiqData.put ((tycos', consts'), (false, (struct_name', acc_code))) ctxt' end;
    1.37  
    1.38  fun register_const const = register_code [] [const];
    1.39 @@ -140,6 +143,71 @@
    1.40  end; (*local*)
    1.41  
    1.42  
    1.43 +(** reflection support **)
    1.44 +
    1.45 +fun check_datatype thy tyco consts =
    1.46 +  let
    1.47 +    val constrs = (map fst o snd o Code.get_type thy) tyco;
    1.48 +    val missing_constrs = subtract (op =) consts constrs;
    1.49 +    val _ = if null missing_constrs then []
    1.50 +      else error ("Missing constructor(s) " ^ commas (map quote missing_constrs)
    1.51 +        ^ " for datatype " ^ quote tyco);
    1.52 +    val false_constrs = subtract (op =) constrs consts;
    1.53 +    val _ = if null false_constrs then []
    1.54 +      else error ("Non-constructor(s) " ^ commas (map quote false_constrs)
    1.55 +        ^ " for datatype " ^ quote tyco);
    1.56 +  in () end;
    1.57 +
    1.58 +fun add_eval_tyco (tyco, tyco') thy =
    1.59 +  let
    1.60 +    val k = Sign.arity_number thy tyco;
    1.61 +    fun pr pr' fxy [] = tyco'
    1.62 +      | pr pr' fxy [ty] =
    1.63 +          Code_Printer.concat [pr' Code_Printer.BR ty, tyco']
    1.64 +      | pr pr' fxy tys =
    1.65 +          Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
    1.66 +  in
    1.67 +    thy
    1.68 +    |> Code_Target.add_syntax_tyco target tyco (SOME (k, pr))
    1.69 +  end;
    1.70 +
    1.71 +fun add_eval_const (const, const') = Code_Target.add_syntax_const target
    1.72 +  const (SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')));
    1.73 +
    1.74 +fun process (code_body, (tyco_map, const_map)) module_name NONE thy =
    1.75 +      let
    1.76 +        val pr = Code_Printer.str o Long_Name.append module_name;
    1.77 +      in
    1.78 +        thy
    1.79 +        |> Code_Target.add_reserved target module_name
    1.80 +        |> Context.theory_map (ML_Context.exec (fn () => ML_Context.eval true Position.none code_body))
    1.81 +        |> fold (add_eval_tyco o apsnd pr) tyco_map
    1.82 +        |> fold (add_eval_const o apsnd pr) const_map
    1.83 +      end
    1.84 +  | process (code_body, _) _ (SOME file_name) thy =
    1.85 +      let
    1.86 +        val preamble = "(* Generated from " ^ Path.implode (ThyLoad.thy_path (Context.theory_name thy))
    1.87 +          ^ "; DO NOT EDIT! *)";
    1.88 +        val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code_body);
    1.89 +      in
    1.90 +        thy
    1.91 +      end;
    1.92 +
    1.93 +fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name some_file thy  =
    1.94 +  let
    1.95 +    val datatypes = map (fn (raw_tyco, raw_cos) =>
    1.96 +      (prep_type thy raw_tyco, map (prep_const thy) raw_cos)) raw_datatypes;
    1.97 +    val functions = map (prep_const thy) raw_functions;
    1.98 +    val _ = map (uncurry (check_datatype thy)) datatypes;
    1.99 +  in
   1.100 +    thy
   1.101 +    |> process (evaluation_code thy module_name (map fst datatypes) (maps snd datatypes @ functions)) module_name some_file
   1.102 +  end;
   1.103 +
   1.104 +val code_reflect = gen_code_reflect Code_Target.cert_tyco Code.check_const;
   1.105 +val code_reflect_cmd = gen_code_reflect Code_Target.read_tyco Code.read_const;
   1.106 +
   1.107 +
   1.108  (** Isar setup **)
   1.109  
   1.110  val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
   1.111 @@ -148,6 +216,35 @@
   1.112      -- (Args.term ::: Scan.repeat (Scan.lift (Args.$$$ "|") |-- Args.term)))
   1.113        >> ml_code_datatype_antiq);
   1.114  
   1.115 +local
   1.116 +
   1.117 +structure P = OuterParse
   1.118 +and K = OuterKeyword
   1.119 +
   1.120 +val datatypesK = "datatypes";
   1.121 +val functionsK = "functions";
   1.122 +val module_nameK = "module_name";
   1.123 +val fileK = "file";
   1.124 +val andK = "and"
   1.125 +
   1.126 +val _ = List.app K.keyword [datatypesK, functionsK];
   1.127 +
   1.128 +val parse_datatype = (P.name --| P.$$$ "=" -- (P.term ::: (Scan.repeat (P.$$$ "|" |-- P.term))));
   1.129 +
   1.130 +in
   1.131 +
   1.132 +val _ =
   1.133 +  OuterSyntax.command "code_reflect" "enrich runtime environment with generated code"
   1.134 +    K.thy_decl (Scan.optional (P.$$$ datatypesK |-- (parse_datatype
   1.135 +      ::: Scan.repeat (P.$$$ andK |-- parse_datatype))) []
   1.136 +    -- Scan.optional (P.$$$ functionsK |-- Scan.repeat1 P.name) []
   1.137 +    --| P.$$$ module_nameK -- P.name
   1.138 +    -- Scan.option (P.$$$ fileK |-- P.name)
   1.139 +  >> (fn (((raw_datatypes, raw_functions), module_name), some_file) => Toplevel.theory
   1.140 +    (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
   1.141 +
   1.142 +end; (*local*)
   1.143 +
   1.144  val setup = Code_Target.extend_target (target, (Code_ML.target_SML, K I));
   1.145  
   1.146  end; (*struct*)