# HG changeset patch # User berghofe # Date 1098801129 -7200 # Node ID ba3c9fdbace32a4911bee2b8519d01f10d8db977 # Parent a12e999a0113ee7cd2ca062c2177ada539a151b9 Added preprocessors. diff -r a12e999a0113 -r ba3c9fdbace3 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Tue Oct 26 16:31:09 2004 +0200 +++ b/src/Pure/codegen.ML Tue Oct 26 16:32:09 2004 +0200 @@ -23,6 +23,8 @@ val add_codegen: string -> term codegen -> theory -> theory val add_tycodegen: string -> typ codegen -> theory -> theory val add_attribute: string -> (Args.T list -> theory attribute * Args.T list) -> theory -> theory + val add_preprocessor: (theory -> thm list -> thm list) -> theory -> theory + val preprocess: theory -> thm list -> thm list val print_codegens: theory -> unit val generate_code: theory -> (string * string) list -> string val generate_code_i: theory -> (string * term) list -> string @@ -134,26 +136,28 @@ consts : ((string * typ) * term mixfix list) list, types : (string * typ mixfix list) list, attrs: (string * (Args.T list -> theory attribute * Args.T list)) list, + preprocs: (stamp * (theory -> thm list -> thm list)) list, test_params: test_params}; val empty = {codegens = [], tycodegens = [], consts = [], types = [], attrs = [], - test_params = default_test_params}; + preprocs = [], test_params = default_test_params}; val copy = I; val prep_ext = I; fun merge ({codegens = codegens1, tycodegens = tycodegens1, consts = consts1, types = types1, attrs = attrs1, - test_params = test_params1}, + preprocs = preprocs1, test_params = test_params1}, {codegens = codegens2, tycodegens = tycodegens2, consts = consts2, types = types2, attrs = attrs2, - test_params = test_params2}) = - {codegens = rev (merge_alists (rev codegens1) (rev codegens2)), - tycodegens = rev (merge_alists (rev tycodegens1) (rev tycodegens2)), + preprocs = preprocs2, test_params = test_params2}) = + {codegens = merge_alists' codegens1 codegens2, + tycodegens = merge_alists' tycodegens1 tycodegens2, consts = merge_alists consts1 consts2, types = merge_alists types1 types2, attrs = merge_alists attrs1 attrs2, + preprocs = merge_alists' preprocs1 preprocs2, test_params = merge_test_params test_params1 test_params2}; fun print sg ({codegens, tycodegens, ...} : T) = @@ -171,10 +175,10 @@ fun get_test_params thy = #test_params (CodegenData.get thy); fun map_test_params f thy = - let val {codegens, tycodegens, consts, types, attrs, test_params} = + let val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} = CodegenData.get thy; in CodegenData.put {codegens = codegens, tycodegens = tycodegens, - consts = consts, types = types, attrs = attrs, + consts = consts, types = types, attrs = attrs, preprocs = preprocs, test_params = f test_params} thy end; @@ -182,22 +186,22 @@ (**** add new code generators to theory ****) fun add_codegen name f thy = - let val {codegens, tycodegens, consts, types, attrs, test_params} = + let val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} = CodegenData.get thy in (case assoc (codegens, name) of None => CodegenData.put {codegens = (name, f) :: codegens, tycodegens = tycodegens, consts = consts, types = types, - attrs = attrs, test_params = test_params} thy + attrs = attrs, preprocs = preprocs, test_params = test_params} thy | Some _ => error ("Code generator " ^ name ^ " already declared")) end; fun add_tycodegen name f thy = - let val {codegens, tycodegens, consts, types, attrs, test_params} = + let val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} = CodegenData.get thy in (case assoc (tycodegens, name) of None => CodegenData.put {tycodegens = (name, f) :: tycodegens, codegens = codegens, consts = consts, types = types, - attrs = attrs, test_params = test_params} thy + attrs = attrs, preprocs = preprocs, test_params = test_params} thy | Some _ => error ("Code generator " ^ name ^ " already declared")) end; @@ -205,12 +209,14 @@ (**** code attribute ****) fun add_attribute name att thy = - let val {codegens, tycodegens, consts, types, attrs, test_params} = + let val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} = CodegenData.get thy in (case assoc (attrs, name) of None => CodegenData.put {tycodegens = tycodegens, codegens = codegens, consts = consts, types = types, - attrs = (name, att) :: attrs, test_params = test_params} thy + attrs = if name = "" then attrs @ [(name, att)] else (name, att) :: attrs, + preprocs = preprocs, + test_params = test_params} thy | Some _ => error ("Code attribute " ^ name ^ " already declared")) end; @@ -221,12 +227,41 @@ (#attrs (CodegenData.get thy)), Scan.fail) >> pair thy)); +(**** preprocessors ****) + +fun add_preprocessor p thy = + let val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} = + CodegenData.get thy + in CodegenData.put {tycodegens = tycodegens, + codegens = codegens, consts = consts, types = types, + attrs = attrs, preprocs = (stamp (), p) :: preprocs, + test_params = test_params} thy + end; + +fun preprocess thy ths = + let val {preprocs, ...} = CodegenData.get thy + in foldl (fn (ths, (_, f)) => f thy ths) (ths, preprocs) end; + +fun unfold_attr (thy, eqn) = + let + val (name, _) = dest_Const (head_of + (fst (Logic.dest_equals (prop_of eqn)))); + fun prep thy = map (fn th => + if name mem term_consts (prop_of th) then + let val sg = sign_of_thm eqn + in rewrite_rule [eqn] (if Sign.subsig (sign_of_thm th, sg) then + Thm.transfer_sg sg th else th) + end + else th) + in (add_preprocessor prep thy, eqn) end; + + (**** associate constants with target language code ****) fun gen_assoc_consts prep_type xs thy = foldl (fn (thy, (s, tyopt, syn)) => let val sg = sign_of thy; - val {codegens, tycodegens, consts, types, attrs, test_params} = + val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} = CodegenData.get thy; val cname = Sign.intern_const sg s; in @@ -243,7 +278,8 @@ None => CodegenData.put {codegens = codegens, tycodegens = tycodegens, consts = ((cname, T'), syn) :: consts, - types = types, attrs = attrs, test_params = test_params} thy + types = types, attrs = attrs, preprocs = preprocs, + test_params = test_params} thy | Some _ => error ("Constant " ^ cname ^ " already associated with code")) end | _ => error ("Not a constant: " ^ s)) @@ -256,7 +292,7 @@ fun assoc_types xs thy = foldl (fn (thy, (s, syn)) => let - val {codegens, tycodegens, consts, types, attrs, test_params} = + val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} = CodegenData.get thy; val tc = Sign.intern_tycon (sign_of thy) s in @@ -264,7 +300,7 @@ None => CodegenData.put {codegens = codegens, tycodegens = tycodegens, consts = consts, types = (tc, syn) :: types, attrs = attrs, - test_params = test_params} thy + preprocs = preprocs, test_params = test_params} thy | Some _ => error ("Type " ^ tc ^ " already associated with code")) end) (thy, xs); @@ -343,17 +379,28 @@ let val axms = flat (map (Symtab.dest o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy)); - val defs = mapfilter (fn (_, t) => - (let - val (lhs, rhs) = Logic.dest_equals t; - val (c, args) = strip_comb lhs; - val (s', T') = dest_Const c - in if s=s' then Some (T', split_last (rename_terms (args @ [rhs]))) - else None end) handle TERM _ => None) axms; - val i = find_index (is_instance thy T o fst) defs + fun prep_def def = (case preprocess thy [def] of + [def'] => prop_of def' | _ => error "get_defn: bad preprocessor"); + fun dest t = + let + val (lhs, rhs) = Logic.dest_equals t; + val (c, args) = strip_comb lhs; + val (s', T') = dest_Const c + in if s = s' then Some (T', (args, rhs)) else None + end handle TERM _ => None; + val defs = mapfilter (fn (name, t) => apsome (pair name) (dest t)) axms; + val i = find_index (is_instance thy T o fst o snd) defs in - if i>=0 then Some (snd (nth_elem (i, defs)), - if length defs = 1 then None else Some i) + if i >= 0 then + let val (name, (T', (args, _))) = nth_elem (i, defs) + in case dest (prep_def (Thm.get_axiom thy name)) of + None => None + | Some (T'', p as (args', rhs)) => + if T' = T'' andalso args = args' then + Some (split_last (rename_terms (args @ [rhs])), + if length defs = 1 then None else Some i) + else None + end else None end; @@ -724,7 +771,8 @@ assoc_types [("fun", parse_mixfix (K dummyT) "(_ ->/ _)")], Attrib.add_attributes [("code", (code_attr, K Attrib.undef_local_attribute), - "declare theorems for code generation")]]; + "declare theorems for code generation")], + add_attribute "unfold" (Scan.succeed unfold_attr)]; end;