Added preprocessors.
authorberghofe
Tue Oct 26 16:32:09 2004 +0200 (2004-10-26)
changeset 15261ba3c9fdbace3
parent 15260 a12e999a0113
child 15262 49f70168f4c0
Added preprocessors.
src/Pure/codegen.ML
     1.1 --- a/src/Pure/codegen.ML	Tue Oct 26 16:31:09 2004 +0200
     1.2 +++ b/src/Pure/codegen.ML	Tue Oct 26 16:32:09 2004 +0200
     1.3 @@ -23,6 +23,8 @@
     1.4    val add_codegen: string -> term codegen -> theory -> theory
     1.5    val add_tycodegen: string -> typ codegen -> theory -> theory
     1.6    val add_attribute: string -> (Args.T list -> theory attribute * Args.T list) -> theory -> theory
     1.7 +  val add_preprocessor: (theory -> thm list -> thm list) -> theory -> theory
     1.8 +  val preprocess: theory -> thm list -> thm list
     1.9    val print_codegens: theory -> unit
    1.10    val generate_code: theory -> (string * string) list -> string
    1.11    val generate_code_i: theory -> (string * term) list -> string
    1.12 @@ -134,26 +136,28 @@
    1.13       consts : ((string * typ) * term mixfix list) list,
    1.14       types : (string * typ mixfix list) list,
    1.15       attrs: (string * (Args.T list -> theory attribute * Args.T list)) list,
    1.16 +     preprocs: (stamp * (theory -> thm list -> thm list)) list,
    1.17       test_params: test_params};
    1.18  
    1.19    val empty =
    1.20      {codegens = [], tycodegens = [], consts = [], types = [], attrs = [],
    1.21 -     test_params = default_test_params};
    1.22 +     preprocs = [], test_params = default_test_params};
    1.23    val copy = I;
    1.24    val prep_ext = I;
    1.25  
    1.26    fun merge
    1.27      ({codegens = codegens1, tycodegens = tycodegens1,
    1.28        consts = consts1, types = types1, attrs = attrs1,
    1.29 -      test_params = test_params1},
    1.30 +      preprocs = preprocs1, test_params = test_params1},
    1.31       {codegens = codegens2, tycodegens = tycodegens2,
    1.32        consts = consts2, types = types2, attrs = attrs2,
    1.33 -      test_params = test_params2}) =
    1.34 -    {codegens = rev (merge_alists (rev codegens1) (rev codegens2)),
    1.35 -     tycodegens = rev (merge_alists (rev tycodegens1) (rev tycodegens2)),
    1.36 +      preprocs = preprocs2, test_params = test_params2}) =
    1.37 +    {codegens = merge_alists' codegens1 codegens2,
    1.38 +     tycodegens = merge_alists' tycodegens1 tycodegens2,
    1.39       consts = merge_alists consts1 consts2,
    1.40       types = merge_alists types1 types2,
    1.41       attrs = merge_alists attrs1 attrs2,
    1.42 +     preprocs = merge_alists' preprocs1 preprocs2,
    1.43       test_params = merge_test_params test_params1 test_params2};
    1.44  
    1.45    fun print sg ({codegens, tycodegens, ...} : T) =
    1.46 @@ -171,10 +175,10 @@
    1.47  fun get_test_params thy = #test_params (CodegenData.get thy);
    1.48  
    1.49  fun map_test_params f thy =
    1.50 -  let val {codegens, tycodegens, consts, types, attrs, test_params} =
    1.51 +  let val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} =
    1.52      CodegenData.get thy;
    1.53    in CodegenData.put {codegens = codegens, tycodegens = tycodegens,
    1.54 -    consts = consts, types = types, attrs = attrs,
    1.55 +    consts = consts, types = types, attrs = attrs, preprocs = preprocs,
    1.56      test_params = f test_params} thy
    1.57    end;
    1.58  
    1.59 @@ -182,22 +186,22 @@
    1.60  (**** add new code generators to theory ****)
    1.61  
    1.62  fun add_codegen name f thy =
    1.63 -  let val {codegens, tycodegens, consts, types, attrs, test_params} =
    1.64 +  let val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} =
    1.65      CodegenData.get thy
    1.66    in (case assoc (codegens, name) of
    1.67        None => CodegenData.put {codegens = (name, f) :: codegens,
    1.68          tycodegens = tycodegens, consts = consts, types = types,
    1.69 -        attrs = attrs, test_params = test_params} thy
    1.70 +        attrs = attrs, preprocs = preprocs, test_params = test_params} thy
    1.71      | Some _ => error ("Code generator " ^ name ^ " already declared"))
    1.72    end;
    1.73  
    1.74  fun add_tycodegen name f thy =
    1.75 -  let val {codegens, tycodegens, consts, types, attrs, test_params} =
    1.76 +  let val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} =
    1.77      CodegenData.get thy
    1.78    in (case assoc (tycodegens, name) of
    1.79        None => CodegenData.put {tycodegens = (name, f) :: tycodegens,
    1.80          codegens = codegens, consts = consts, types = types,
    1.81 -        attrs = attrs, test_params = test_params} thy
    1.82 +        attrs = attrs, preprocs = preprocs, test_params = test_params} thy
    1.83      | Some _ => error ("Code generator " ^ name ^ " already declared"))
    1.84    end;
    1.85  
    1.86 @@ -205,12 +209,14 @@
    1.87  (**** code attribute ****)
    1.88  
    1.89  fun add_attribute name att thy =
    1.90 -  let val {codegens, tycodegens, consts, types, attrs, test_params} =
    1.91 +  let val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} =
    1.92      CodegenData.get thy
    1.93    in (case assoc (attrs, name) of
    1.94        None => CodegenData.put {tycodegens = tycodegens,
    1.95          codegens = codegens, consts = consts, types = types,
    1.96 -        attrs = (name, att) :: attrs, test_params = test_params} thy
    1.97 +        attrs = if name = "" then attrs @ [(name, att)] else (name, att) :: attrs,
    1.98 +        preprocs = preprocs,
    1.99 +        test_params = test_params} thy
   1.100      | Some _ => error ("Code attribute " ^ name ^ " already declared"))
   1.101    end;
   1.102  
   1.103 @@ -221,12 +227,41 @@
   1.104      (#attrs (CodegenData.get thy)), Scan.fail) >> pair thy));
   1.105  
   1.106  
   1.107 +(**** preprocessors ****)
   1.108 +
   1.109 +fun add_preprocessor p thy =
   1.110 +  let val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} =
   1.111 +    CodegenData.get thy
   1.112 +  in CodegenData.put {tycodegens = tycodegens,
   1.113 +    codegens = codegens, consts = consts, types = types,
   1.114 +    attrs = attrs, preprocs = (stamp (), p) :: preprocs,
   1.115 +    test_params = test_params} thy
   1.116 +  end;
   1.117 +
   1.118 +fun preprocess thy ths =
   1.119 +  let val {preprocs, ...} = CodegenData.get thy
   1.120 +  in foldl (fn (ths, (_, f)) => f thy ths) (ths, preprocs) end;
   1.121 +
   1.122 +fun unfold_attr (thy, eqn) =
   1.123 +  let
   1.124 +    val (name, _) = dest_Const (head_of
   1.125 +      (fst (Logic.dest_equals (prop_of eqn))));
   1.126 +    fun prep thy = map (fn th =>
   1.127 +      if name mem term_consts (prop_of th) then
   1.128 +        let val sg = sign_of_thm eqn
   1.129 +        in rewrite_rule [eqn] (if Sign.subsig (sign_of_thm th, sg) then
   1.130 +          Thm.transfer_sg sg th else th)
   1.131 +        end
   1.132 +      else th)
   1.133 +  in (add_preprocessor prep thy, eqn) end;
   1.134 +
   1.135 +
   1.136  (**** associate constants with target language code ****)
   1.137  
   1.138  fun gen_assoc_consts prep_type xs thy = foldl (fn (thy, (s, tyopt, syn)) =>
   1.139    let
   1.140      val sg = sign_of thy;
   1.141 -    val {codegens, tycodegens, consts, types, attrs, test_params} =
   1.142 +    val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} =
   1.143        CodegenData.get thy;
   1.144      val cname = Sign.intern_const sg s;
   1.145    in
   1.146 @@ -243,7 +278,8 @@
   1.147               None => CodegenData.put {codegens = codegens,
   1.148                 tycodegens = tycodegens,
   1.149                 consts = ((cname, T'), syn) :: consts,
   1.150 -               types = types, attrs = attrs, test_params = test_params} thy
   1.151 +               types = types, attrs = attrs, preprocs = preprocs,
   1.152 +               test_params = test_params} thy
   1.153             | Some _ => error ("Constant " ^ cname ^ " already associated with code"))
   1.154           end
   1.155       | _ => error ("Not a constant: " ^ s))
   1.156 @@ -256,7 +292,7 @@
   1.157  
   1.158  fun assoc_types xs thy = foldl (fn (thy, (s, syn)) =>
   1.159    let
   1.160 -    val {codegens, tycodegens, consts, types, attrs, test_params} =
   1.161 +    val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} =
   1.162        CodegenData.get thy;
   1.163      val tc = Sign.intern_tycon (sign_of thy) s
   1.164    in
   1.165 @@ -264,7 +300,7 @@
   1.166         None => CodegenData.put {codegens = codegens,
   1.167           tycodegens = tycodegens, consts = consts,
   1.168           types = (tc, syn) :: types, attrs = attrs,
   1.169 -         test_params = test_params} thy
   1.170 +         preprocs = preprocs, test_params = test_params} thy
   1.171       | Some _ => error ("Type " ^ tc ^ " already associated with code"))
   1.172    end) (thy, xs);
   1.173  
   1.174 @@ -343,17 +379,28 @@
   1.175    let
   1.176      val axms = flat (map (Symtab.dest o #axioms o Theory.rep_theory)
   1.177        (thy :: Theory.ancestors_of thy));
   1.178 -    val defs = mapfilter (fn (_, t) =>
   1.179 -      (let
   1.180 -         val (lhs, rhs) = Logic.dest_equals t;
   1.181 -         val (c, args) = strip_comb lhs;
   1.182 -         val (s', T') = dest_Const c
   1.183 -       in if s=s' then Some (T', split_last (rename_terms (args @ [rhs])))
   1.184 -         else None end) handle TERM _ => None) axms;
   1.185 -    val i = find_index (is_instance thy T o fst) defs
   1.186 +    fun prep_def def = (case preprocess thy [def] of
   1.187 +      [def'] => prop_of def' | _ => error "get_defn: bad preprocessor");
   1.188 +    fun dest t =
   1.189 +      let
   1.190 +        val (lhs, rhs) = Logic.dest_equals t;
   1.191 +        val (c, args) = strip_comb lhs;
   1.192 +        val (s', T') = dest_Const c
   1.193 +      in if s = s' then Some (T', (args, rhs)) else None
   1.194 +      end handle TERM _ => None;
   1.195 +    val defs = mapfilter (fn (name, t) => apsome (pair name) (dest t)) axms;
   1.196 +    val i = find_index (is_instance thy T o fst o snd) defs
   1.197    in
   1.198 -    if i>=0 then Some (snd (nth_elem (i, defs)),
   1.199 -      if length defs = 1 then None else Some i)
   1.200 +    if i >= 0 then
   1.201 +      let val (name, (T', (args, _))) = nth_elem (i, defs)
   1.202 +      in case dest (prep_def (Thm.get_axiom thy name)) of
   1.203 +          None => None
   1.204 +        | Some (T'', p as (args', rhs)) =>
   1.205 +            if T' = T'' andalso args = args' then
   1.206 +              Some (split_last (rename_terms (args @ [rhs])),
   1.207 +                if length defs = 1 then None else Some i)
   1.208 +            else None
   1.209 +      end
   1.210      else None
   1.211    end;
   1.212  
   1.213 @@ -724,7 +771,8 @@
   1.214     assoc_types [("fun", parse_mixfix (K dummyT) "(_ ->/ _)")],
   1.215     Attrib.add_attributes [("code",
   1.216       (code_attr, K Attrib.undef_local_attribute),
   1.217 -     "declare theorems for code generation")]];
   1.218 +     "declare theorems for code generation")],
   1.219 +   add_attribute "unfold" (Scan.succeed unfold_attr)];
   1.220  
   1.221  end;
   1.222