- removed test_params from CodegenData (now in Pure/Tools/quickcheck.ML)
authorberghofe
Sun Oct 19 21:19:27 2008 +0200 (2008-10-19)
changeset 28640188e9557c572
parent 28639 9788fb18a142
child 28641 f6e1b2beb766
- removed test_params from CodegenData (now in Pure/Tools/quickcheck.ML)
- improved code unfold preprocessor: now uses one single simpset
containing all unfolding rules
- got rid of some legacy functions
src/Pure/codegen.ML
     1.1 --- a/src/Pure/codegen.ML	Sun Oct 19 21:14:53 2008 +0200
     1.2 +++ b/src/Pure/codegen.ML	Sun Oct 19 21:19:27 2008 +0200
     1.3 @@ -182,33 +182,6 @@
     1.4    codegr ->    (* code dependency graph *)
     1.5    (Pretty.T * codegr) option;
     1.6  
     1.7 -(* parameters for random testing *)
     1.8 -
     1.9 -type test_params =
    1.10 -  {size: int, iterations: int, default_type: typ option};
    1.11 -
    1.12 -fun merge_test_params
    1.13 -  {size = size1, iterations = iterations1, default_type = default_type1}
    1.14 -  {size = size2, iterations = iterations2, default_type = default_type2} =
    1.15 -  {size = Int.max (size1, size2),
    1.16 -   iterations = Int.max (iterations1, iterations2),
    1.17 -   default_type = case default_type1 of
    1.18 -       NONE => default_type2
    1.19 -     | _ => default_type1};
    1.20 -
    1.21 -val default_test_params : test_params =
    1.22 -  {size = 10, iterations = 100, default_type = NONE};
    1.23 -
    1.24 -fun set_size size ({iterations, default_type, ...} : test_params) =
    1.25 -  {size = size, iterations = iterations, default_type = default_type};
    1.26 -
    1.27 -fun set_iterations iterations ({size, default_type, ...} : test_params) =
    1.28 -  {size = size, iterations = iterations, default_type = default_type};
    1.29 -
    1.30 -fun set_default_type s thy ({size, iterations, ...} : test_params) =
    1.31 -  {size = size, iterations = iterations,
    1.32 -   default_type = SOME (Syntax.read_typ_global thy s)};
    1.33 -
    1.34  
    1.35  (* theory data *)
    1.36  
    1.37 @@ -220,29 +193,27 @@
    1.38       consts : ((string * typ) * (term mixfix list * (string * string) list)) list,
    1.39       types : (string * (typ mixfix list * (string * string) list)) list,
    1.40       preprocs: (stamp * (theory -> thm list -> thm list)) list,
    1.41 -     modules: codegr Symtab.table,
    1.42 -     test_params: test_params};
    1.43 +     modules: codegr Symtab.table};
    1.44  
    1.45    val empty =
    1.46      {codegens = [], tycodegens = [], consts = [], types = [],
    1.47 -     preprocs = [], modules = Symtab.empty, test_params = default_test_params};
    1.48 +     preprocs = [], modules = Symtab.empty};
    1.49    val copy = I;
    1.50    val extend = I;
    1.51  
    1.52    fun merge _
    1.53      ({codegens = codegens1, tycodegens = tycodegens1,
    1.54        consts = consts1, types = types1,
    1.55 -      preprocs = preprocs1, modules = modules1, test_params = test_params1} : T,
    1.56 +      preprocs = preprocs1, modules = modules1} : T,
    1.57       {codegens = codegens2, tycodegens = tycodegens2,
    1.58        consts = consts2, types = types2,
    1.59 -      preprocs = preprocs2, modules = modules2, test_params = test_params2}) =
    1.60 +      preprocs = preprocs2, modules = modules2}) =
    1.61      {codegens = AList.merge (op =) (K true) (codegens1, codegens2),
    1.62       tycodegens = AList.merge (op =) (K true) (tycodegens1, tycodegens2),
    1.63       consts = AList.merge (op =) (K true) (consts1, consts2),
    1.64       types = AList.merge (op =) (K true) (types1, types2),
    1.65       preprocs = AList.merge (op =) (K true) (preprocs1, preprocs2),
    1.66 -     modules = Symtab.merge (K true) (modules1, modules2),
    1.67 -     test_params = merge_test_params test_params1 test_params2};
    1.68 +     modules = Symtab.merge (K true) (modules1, modules2)};
    1.69  );
    1.70  
    1.71  fun print_codegens thy =
    1.72 @@ -254,53 +225,38 @@
    1.73  
    1.74  
    1.75  
    1.76 -(**** access parameters for random testing ****)
    1.77 -
    1.78 -fun get_test_params thy = #test_params (CodegenData.get thy);
    1.79 -
    1.80 -fun map_test_params f thy =
    1.81 -  let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} =
    1.82 -    CodegenData.get thy;
    1.83 -  in CodegenData.put {codegens = codegens, tycodegens = tycodegens,
    1.84 -    consts = consts, types = types, preprocs = preprocs,
    1.85 -    modules = modules, test_params = f test_params} thy
    1.86 -  end;
    1.87 -
    1.88 -
    1.89  (**** access modules ****)
    1.90  
    1.91  fun get_modules thy = #modules (CodegenData.get thy);
    1.92  
    1.93  fun map_modules f thy =
    1.94 -  let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} =
    1.95 +  let val {codegens, tycodegens, consts, types, preprocs, modules} =
    1.96      CodegenData.get thy;
    1.97    in CodegenData.put {codegens = codegens, tycodegens = tycodegens,
    1.98      consts = consts, types = types, preprocs = preprocs,
    1.99 -    modules = f modules, test_params = test_params} thy
   1.100 +    modules = f modules} thy
   1.101    end;
   1.102  
   1.103  
   1.104  (**** add new code generators to theory ****)
   1.105  
   1.106  fun add_codegen name f thy =
   1.107 -  let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} =
   1.108 +  let val {codegens, tycodegens, consts, types, preprocs, modules} =
   1.109      CodegenData.get thy
   1.110    in (case AList.lookup (op =) codegens name of
   1.111        NONE => CodegenData.put {codegens = (name, f) :: codegens,
   1.112          tycodegens = tycodegens, consts = consts, types = types,
   1.113 -        preprocs = preprocs, modules = modules,
   1.114 -        test_params = test_params} thy
   1.115 +        preprocs = preprocs, modules = modules} thy
   1.116      | SOME _ => error ("Code generator " ^ name ^ " already declared"))
   1.117    end;
   1.118  
   1.119  fun add_tycodegen name f thy =
   1.120 -  let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} =
   1.121 +  let val {codegens, tycodegens, consts, types, preprocs, modules} =
   1.122      CodegenData.get thy
   1.123    in (case AList.lookup (op =) tycodegens name of
   1.124        NONE => CodegenData.put {tycodegens = (name, f) :: tycodegens,
   1.125          codegens = codegens, consts = consts, types = types,
   1.126 -        preprocs = preprocs, modules = modules,
   1.127 -        test_params = test_params} thy
   1.128 +        preprocs = preprocs, modules = modules} thy
   1.129      | SOME _ => error ("Code generator " ^ name ^ " already declared"))
   1.130    end;
   1.131  
   1.132 @@ -308,12 +264,12 @@
   1.133  (**** preprocessors ****)
   1.134  
   1.135  fun add_preprocessor p thy =
   1.136 -  let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} =
   1.137 +  let val {codegens, tycodegens, consts, types, preprocs, modules} =
   1.138      CodegenData.get thy
   1.139    in CodegenData.put {tycodegens = tycodegens,
   1.140      codegens = codegens, consts = consts, types = types,
   1.141      preprocs = (stamp (), p) :: preprocs,
   1.142 -    modules = modules, test_params = test_params} thy
   1.143 +    modules = modules} thy
   1.144    end;
   1.145  
   1.146  fun preprocess thy =
   1.147 @@ -332,27 +288,33 @@
   1.148      | _ => err ()
   1.149    end;
   1.150  
   1.151 +structure UnfoldData = TheoryDataFun
   1.152 +(
   1.153 +  type T = simpset;
   1.154 +  val empty = empty_ss;
   1.155 +  val copy = I;
   1.156 +  val extend = I;
   1.157 +  fun merge _ = merge_ss;
   1.158 +);
   1.159 +
   1.160  fun add_unfold eqn =
   1.161    let
   1.162 -    val thy = Thm.theory_of_thm eqn;
   1.163 -    val ctxt = ProofContext.init thy;
   1.164 +    val ctxt = ProofContext.init (Thm.theory_of_thm eqn);
   1.165      val eqn' = LocalDefs.meta_rewrite_rule ctxt eqn;
   1.166 -    val names = term_consts (fst (Logic.dest_equals (prop_of eqn')));
   1.167 -    fun prep thy = map (fn th =>
   1.168 -      let val prop = prop_of th
   1.169 -      in
   1.170 -        if forall (fn name => exists_Const (fn (c, _) => c = name) prop) names
   1.171 -        then rewrite_rule [eqn'] (Thm.transfer thy th)
   1.172 -        else th
   1.173 -      end)
   1.174 -  in add_preprocessor prep end;
   1.175 +  in
   1.176 +    UnfoldData.map (fn ss => ss addsimps [eqn'])
   1.177 +  end;
   1.178 +
   1.179 +fun unfold_preprocessor thy =
   1.180 +  let val ss = Simplifier.theory_context thy (UnfoldData.get thy)
   1.181 +  in map (Thm.transfer thy #> Simplifier.full_simplify ss) end;
   1.182  
   1.183  
   1.184  (**** associate constants with target language code ****)
   1.185  
   1.186  fun gen_assoc_const prep_const (raw_const, syn) thy =
   1.187    let
   1.188 -    val {codegens, tycodegens, consts, types, preprocs, modules, test_params} =
   1.189 +    val {codegens, tycodegens, consts, types, preprocs, modules} =
   1.190        CodegenData.get thy;
   1.191      val (cname, T) = prep_const thy raw_const;
   1.192    in
   1.193 @@ -363,7 +325,7 @@
   1.194          tycodegens = tycodegens,
   1.195          consts = ((cname, T), syn) :: consts,
   1.196          types = types, preprocs = preprocs,
   1.197 -        modules = modules, test_params = test_params} thy
   1.198 +        modules = modules} thy
   1.199      | SOME _ => error ("Constant " ^ cname ^ " already associated with code")
   1.200    end;
   1.201  
   1.202 @@ -375,7 +337,7 @@
   1.203  
   1.204  fun assoc_type (s, syn) thy =
   1.205    let
   1.206 -    val {codegens, tycodegens, consts, types, preprocs, modules, test_params} =
   1.207 +    val {codegens, tycodegens, consts, types, preprocs, modules} =
   1.208        CodegenData.get thy;
   1.209      val tc = Sign.intern_type thy s;
   1.210    in
   1.211 @@ -387,7 +349,7 @@
   1.212            NONE => CodegenData.put {codegens = codegens,
   1.213              tycodegens = tycodegens, consts = consts,
   1.214              types = (tc, syn) :: types,
   1.215 -            preprocs = preprocs, modules = modules, test_params = test_params} thy
   1.216 +            preprocs = preprocs, modules = modules} thy
   1.217          | SOME _ => error ("Type " ^ tc ^ " already associated with code"))
   1.218      | _ => error ("Not a type constructor: " ^ s)
   1.219    end;
   1.220 @@ -523,7 +485,7 @@
   1.221  (**** retrieve definition of constant ****)
   1.222  
   1.223  fun is_instance T1 T2 =
   1.224 -  Type.raw_instance (T1, Logic.legacy_varifyT T2);
   1.225 +  Type.raw_instance (T1, if null (typ_tfrees T2) then T2 else Logic.varifyT T2);
   1.226  
   1.227  fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) =>
   1.228    s = s' andalso is_instance T T') (#consts (CodegenData.get thy)));
   1.229 @@ -1032,7 +994,7 @@
   1.230          P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
   1.231       (fn xs => Toplevel.theory (fn thy => fold (assoc_const o
   1.232         (fn ((const, mfx), aux) =>
   1.233 -         (const, (parse_mixfix (OldGoals.read_term thy) mfx, aux)))) xs thy)));
   1.234 +         (const, (parse_mixfix (Syntax.read_term_global thy) mfx, aux)))) xs thy)));
   1.235  
   1.236  fun parse_code lib =
   1.237    Scan.optional (P.$$$ "(" |-- P.enum "," P.xname --| P.$$$ ")") (!mode) --
   1.238 @@ -1066,7 +1028,8 @@
   1.239    #> Value.add_evaluator ("SML", eval_term o ProofContext.theory_of)
   1.240    #> Quickcheck.add_generator ("SML", test_term)
   1.241    #> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute
   1.242 -       (fn thm => Context.mapping (add_unfold thm #> Code.add_inline thm) I)));
   1.243 +       (fn thm => Context.mapping (add_unfold thm #> Code.add_inline thm) I)))
   1.244 +  #> add_preprocessor unfold_preprocessor;
   1.245  
   1.246  val _ =
   1.247    OuterSyntax.command "code_library"