src/Tools/code/code_package.ML
changeset 24436 b694324cd2be
parent 24423 ae9cd0e92423
child 24585 c359896d0f48
     1.1 --- a/src/Tools/code/code_package.ML	Mon Aug 27 11:34:17 2007 +0200
     1.2 +++ b/src/Tools/code/code_package.ML	Mon Aug 27 11:34:18 2007 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature CODE_PACKAGE =
     1.6  sig
     1.7 -  (* interfaces *)
     1.8 +  (*interfaces*)
     1.9    val eval_conv: theory
    1.10      -> (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm
    1.11         -> string list -> cterm -> thm)
    1.12 @@ -20,7 +20,7 @@
    1.13    val satisfies: theory -> cterm -> string list -> bool;
    1.14    val codegen_command: theory -> string -> unit;
    1.15  
    1.16 -  (* axiomatic interfaces *)
    1.17 +  (*axiomatic interfaces*)
    1.18    type appgen;
    1.19    val add_appconst: string * appgen -> theory -> theory;
    1.20    val appgen_let: appgen;
    1.21 @@ -429,13 +429,22 @@
    1.22      |> fst
    1.23    end;
    1.24  
    1.25 +fun code thy permissive cs seris =
    1.26 +  let
    1.27 +    val code = Program.get thy;
    1.28 +    val seris' = map (fn (((target, module), file), args) =>
    1.29 +      CodeTarget.get_serializer thy target permissive module file args
    1.30 +        CodeName.labelled_name cs) seris;
    1.31 +  in (map (fn f => f code) seris' : unit list; ()) end;
    1.32 +
    1.33  fun raw_eval f thy g =
    1.34    let
    1.35      val value_name = "Isabelle_Eval.EVAL.EVAL";
    1.36      fun ensure_eval thy algbr funcgr t = 
    1.37        let
    1.38          val ty = fastype_of t;
    1.39 -        val vs = typ_tfrees ty;
    1.40 +        val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
    1.41 +          o dest_TFree))) t [];
    1.42          val defgen_eval =
    1.43            fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
    1.44            ##>> exprgen_typ thy algbr funcgr ty
    1.45 @@ -485,6 +494,77 @@
    1.46        (consts' ~~ consts'');
    1.47    in consts''' end;
    1.48  
    1.49 +fun generate_const_exprs thy raw_cs =
    1.50 +  let
    1.51 +    val (perm1, cs) = CodeUnit.read_const_exprs thy
    1.52 +      (filter_generatable thy) raw_cs;
    1.53 +    val (perm2, cs') = case generate thy (CodeFuncgr.make thy cs)
    1.54 +      (fold_map ooo ensure_def_const') cs
    1.55 +     of [] => (true, NONE)
    1.56 +      | cs => (false, SOME cs);
    1.57 +  in (perm1 orelse perm2, cs') end;
    1.58 +
    1.59 +
    1.60 +(** code properties **)
    1.61 +
    1.62 +fun mk_codeprops thy all_cs sel_cs =
    1.63 +  let
    1.64 +    fun select (thmref, thm) = case try (Drule.unvarify o Drule.zero_var_indexes) thm
    1.65 +     of NONE => NONE
    1.66 +      | SOME thm => let
    1.67 +          val t = (ObjectLogic.drop_judgment thy o Thm.prop_of) thm;
    1.68 +          val cs = fold_aterms (fn Const (c, ty) =>
    1.69 +            cons (Class.unoverload_const thy (c, ty)) | _ => I) t [];
    1.70 +        in if exists (member (op =) sel_cs) cs
    1.71 +          andalso forall (member (op =) all_cs) cs
    1.72 +          then SOME (thmref, thm) else NONE end;
    1.73 +    fun mk_codeprop (thmref, thm) =
    1.74 +      let
    1.75 +        val t = ObjectLogic.drop_judgment thy (Thm.prop_of thm);
    1.76 +        val ty_judg = fastype_of t;
    1.77 +        val tfrees1 = fold_aterms (fn Const (c, ty) =>
    1.78 +          Term.add_tfreesT ty | _ => I) t [];
    1.79 +        val vars = Term.add_frees t [];
    1.80 +        val tfrees2 = fold (Term.add_tfreesT o snd) vars [];
    1.81 +        val tfrees' = subtract (op =) tfrees2 tfrees1 |> map TFree;
    1.82 +        val ty = map Term.itselfT tfrees' @ map snd vars ---> ty_judg;
    1.83 +        val tfree_vars = map Logic.mk_type tfrees';
    1.84 +        val c = PureThy.string_of_thmref thmref
    1.85 +          |> NameSpace.explode
    1.86 +          |> (fn [x] => [x] | (x::xs) => xs)
    1.87 +          |> space_implode "_"
    1.88 +        val propdef = (((c, ty), tfree_vars @ map Free vars), t);
    1.89 +      in if c = "" then NONE else SOME (thmref, propdef) end;
    1.90 +  in
    1.91 +    PureThy.thms_containing thy ([], [])
    1.92 +    |> maps PureThy.selections
    1.93 +    |> map_filter select
    1.94 +    |> map_filter mk_codeprop
    1.95 +  end;
    1.96 +
    1.97 +fun add_codeprops all_cs sel_cs thy =
    1.98 +  let
    1.99 +    val codeprops = mk_codeprops thy all_cs sel_cs;
   1.100 +    fun lift_name_yield f x = (Name.context, x) |> f ||> snd;
   1.101 +    fun add (thmref, (((raw_c, ty), ts), t)) (names, thy) =
   1.102 +      let
   1.103 +        val _ = warning ("Adding theorem " ^ quote (PureThy.string_of_thmref thmref)
   1.104 +          ^ " as code property " ^ quote raw_c);
   1.105 +        val ([raw_c'], names') = Name.variants [raw_c] names;
   1.106 +      in
   1.107 +        thy
   1.108 +        |> PureThy.simple_def ("", []) (((raw_c', ty, Syntax.NoSyn), ts), t)
   1.109 +        ||> pair names'
   1.110 +      end;
   1.111 +  in
   1.112 +    thy
   1.113 +    |> Sign.sticky_prefix "codeprop"
   1.114 +    |> lift_name_yield (fold_map add codeprops)
   1.115 +    ||> Sign.restore_naming thy
   1.116 +    |-> (fn c_thms => fold (Code.add_func true o snd) c_thms #> pair c_thms)
   1.117 +  end;
   1.118 +
   1.119 +
   1.120  
   1.121  (** toplevel interface and setup **)
   1.122  
   1.123 @@ -493,20 +573,11 @@
   1.124  structure P = OuterParse
   1.125  and K = OuterKeyword
   1.126  
   1.127 -fun code raw_cs seris thy =
   1.128 +fun code_cmd raw_cs seris thy =
   1.129    let
   1.130 -    val (perm1, cs) = CodeUnit.read_const_exprs thy
   1.131 -      (filter_generatable thy) raw_cs;
   1.132 -    val (perm2, cs') = case generate thy (CodeFuncgr.make thy cs) (fold_map ooo ensure_def_const') cs
   1.133 -     of [] => (true, NONE)
   1.134 -      | cs => (false, SOME cs);
   1.135 -    val code = Program.get thy;
   1.136 -    val seris' = map (fn (((target, module), file), args) =>
   1.137 -      CodeTarget.get_serializer thy target (perm1 orelse perm2) module file args
   1.138 -        CodeName.labelled_name cs') seris;
   1.139 -  in
   1.140 -    (map (fn f => f code) seris' : unit list; ())
   1.141 -  end;
   1.142 +    val (permissive, cs) = generate_const_exprs thy raw_cs;
   1.143 +    val _ = code thy permissive cs seris;
   1.144 +  in () end;
   1.145  
   1.146  fun code_thms_cmd thy =
   1.147    code_thms thy o snd o CodeUnit.read_const_exprs thy (fst o CodeFuncgr.make_consts thy);
   1.148 @@ -514,28 +585,42 @@
   1.149  fun code_deps_cmd thy =
   1.150    code_deps thy o snd o CodeUnit.read_const_exprs thy (fst o CodeFuncgr.make_consts thy);
   1.151  
   1.152 +fun code_props_cmd raw_cs seris thy =
   1.153 +  let
   1.154 +    val (_, all_cs) = generate_const_exprs thy ["*"];
   1.155 +    val (permissive, cs) = generate_const_exprs thy raw_cs;
   1.156 +    val (c_thms, thy') = add_codeprops (map (the o CodeName.const_rev thy) (these all_cs))
   1.157 +      (map (the o CodeName.const_rev thy) (these cs)) thy;
   1.158 +    val prop_cs = (filter_generatable thy' o map fst) c_thms;
   1.159 +    val _ = if null seris then [] else generate thy' (CodeFuncgr.make thy' prop_cs)
   1.160 +      (fold_map ooo ensure_def_const') prop_cs;
   1.161 +    val _ = if null seris then () else code thy' permissive
   1.162 +      (SOME (map (CodeName.const thy') prop_cs)) seris;
   1.163 +  in thy' end;
   1.164 +
   1.165  val (inK, module_nameK, fileK) = ("in", "module_name", "file");
   1.166  
   1.167 -val code_exprP =
   1.168 +fun code_exprP cmd =
   1.169    (Scan.repeat P.term
   1.170    -- Scan.repeat (P.$$$ inK |-- P.name
   1.171       -- Scan.option (P.$$$ module_nameK |-- P.name)
   1.172       -- Scan.option (P.$$$ fileK |-- P.name)
   1.173       -- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") []
   1.174 -  ) >> (fn (raw_cs, seris) => code raw_cs seris));
   1.175 +  ) >> (fn (raw_cs, seris) => cmd raw_cs seris));
   1.176  
   1.177  val _ = OuterSyntax.add_keywords [inK, module_nameK, fileK];
   1.178  
   1.179 -val (codeK, code_thmsK, code_depsK) = ("export_code", "code_thms", "code_deps");
   1.180 +val (codeK, code_thmsK, code_depsK, code_propsK) =
   1.181 +  ("export_code", "code_thms", "code_deps", "code_props");
   1.182  
   1.183  in
   1.184  
   1.185  val codeP =
   1.186    OuterSyntax.improper_command codeK "generate executable code for constants"
   1.187 -    K.diag (P.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
   1.188 +    K.diag (P.!!! (code_exprP code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
   1.189  
   1.190  fun codegen_command thy cmd =
   1.191 -  case Scan.read OuterLex.stopper (P.!!! code_exprP) ((filter OuterLex.is_proper o OuterSyntax.scan) cmd)
   1.192 +  case Scan.read OuterLex.stopper (P.!!! (code_exprP code_cmd)) ((filter OuterLex.is_proper o OuterSyntax.scan) cmd)
   1.193     of SOME f => (writeln "Now generating code..."; f thy)
   1.194      | NONE => error ("Bad directive " ^ quote cmd);
   1.195  
   1.196 @@ -551,8 +636,12 @@
   1.197        >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
   1.198          o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
   1.199  
   1.200 -val _ = OuterSyntax.add_parsers [codeP, code_thmsP, code_depsP];
   1.201 +val code_propsP =
   1.202 +  OuterSyntax.command code_propsK "generate characteristic properties for executable constants"
   1.203 +    K.thy_decl (P.!!! (code_exprP code_props_cmd) >> Toplevel.theory);
   1.204  
   1.205 -end; (* local *)
   1.206 +val _ = OuterSyntax.add_parsers [codeP, code_thmsP, code_depsP, code_propsP];
   1.207  
   1.208 -end; (* struct *)
   1.209 +end; (*local*)
   1.210 +
   1.211 +end; (*struct*)