# HG changeset patch # User haftmann # Date 1171095985 -3600 # Node ID 0e56750a092b13f1c4babfb234cadcac9ec0abe6 # Parent ba3d6b76a627eddace01abc2d7aefe74a338d205 changed representation of constants diff -r ba3d6b76a627 -r 0e56750a092b src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Sat Feb 10 09:26:24 2007 +0100 +++ b/src/Pure/Tools/codegen_package.ML Sat Feb 10 09:26:25 2007 +0100 @@ -349,10 +349,11 @@ and appgen_default thy algbr funcgr strct ((c, ty), ts) trns = trns |> ensure_def_const thy algbr funcgr strct (CodegenConsts.norm_of_typ thy (c, ty)) - ||>> exprgen_type thy algbr funcgr strct ty + ||>> fold_map (exprgen_type thy algbr funcgr strct) ((fst o Term.strip_type) ty) + ||>> exprgen_type thy algbr funcgr strct ((snd o Term.strip_type) ty) ||>> exprgen_dict_parms thy algbr funcgr strct (c, ty) ||>> fold_map (exprgen_term thy algbr funcgr strct) ts - |>> (fn (((c, ty), iss), ts) => IConst (c, (iss, ty)) `$$ ts) + |>> (fn ((((c, tys), ty), iss), ts) => IConst (c, (iss, tys)) `$$ ts) and select_appgen thy algbr funcgr strct ((c, ty), ts) trns = case Symtab.lookup (fst (CodegenPackageData.get thy)) c of SOME (i, (appgen, _)) => @@ -579,7 +580,7 @@ error ("Term" ^ Sign.string_of_term thy t ^ "is polymorhpic")) t; val t' = codegen_term thy t; - in CodegenSerializer.eval_term thy (Code.get thy) (ref_spec, t') end; + in CodegenSerializer.eval_term thy CodegenNames.labelled_name (Code.get thy) (ref_spec, t') end; (* constant specifications with wildcards *) @@ -623,7 +624,7 @@ fun code raw_cs seris thy = let val seris' = map (fn (target, args as _ :: _) => - (target, SOME (CodegenSerializer.get_serializer thy target args)) + (target, SOME (CodegenSerializer.get_serializer thy target args CodegenNames.labelled_name)) | (target, []) => (CodegenSerializer.assert_serializer thy target, NONE)) seris; val targets = case map fst seris' of [] => NONE | xs => SOME xs; val cs = maps (read_constspec thy targets) raw_cs; @@ -654,8 +655,8 @@ >> (fn (raw_cs, seris) => code raw_cs seris) ); -val (print_codethmsK, codeK, code_abstypeK, code_axiomsK) = - ("print_codethms", "code_gen", "code_abstype", "code_axioms"); +val (codeK, code_abstypeK, code_axiomsK, code_thmsK) = + ("code_gen", "code_abstype", "code_axioms", "code_thms"); in @@ -681,15 +682,13 @@ >> (Toplevel.theory o constsubst_e) ); -val print_codethmsP = - OuterSyntax.improper_command print_codethmsK "print code theorems of this theory" OuterKeyword.diag - (Scan.option (P.$$$ "(" |-- Scan.repeat P.term --| P.$$$ ")") - >> (fn NONE => CodegenData.print_thms - | SOME cs => fn thy => print_codethms_e thy cs) - >> (fn f => Toplevel.no_timing o Toplevel.unknown_theory - o Toplevel.keep (f o Toplevel.theory_of))); +val code_thmsP = + OuterSyntax.improper_command code_thmsK "print cached defining equations" OuterKeyword.diag + (Scan.repeat P.term + >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory + o Toplevel.keep ((fn thy => print_codethms_e thy cs) o Toplevel.theory_of))); -val _ = OuterSyntax.add_parsers [codeP, code_abstypeP, code_axiomsP, print_codethmsP]; +val _ = OuterSyntax.add_parsers [codeP, code_abstypeP, code_axiomsP, code_thmsP]; end; (* local *) diff -r ba3d6b76a627 -r 0e56750a092b src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Sat Feb 10 09:26:24 2007 +0100 +++ b/src/Pure/Tools/codegen_thingol.ML Sat Feb 10 09:26:25 2007 +0100 @@ -23,7 +23,7 @@ `%% of string * itype list | ITyVar of vname; datatype iterm = - IConst of string * (dict list list * itype) + IConst of string * (dict list list * itype list (*types of arguments*)) | IVar of vname | `$ of iterm * iterm | `|-> of (vname * itype) * iterm @@ -51,8 +51,8 @@ val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option; val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm; val unfold_const_app: iterm -> - ((string * (dict list list * itype)) * iterm list) option; - val eta_expand: (string * (dict list list * itype)) * iterm list -> int -> iterm; + ((string * (dict list list * itype list)) * iterm list) option; + val eta_expand: (string * (dict list list * itype list)) * iterm list -> int -> iterm; val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a; val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a; val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a; @@ -124,7 +124,7 @@ | ITyVar of vname; datatype iterm = - IConst of string * (dict list list * itype) + IConst of string * (dict list list * itype list) | IVar of vname | `$ of iterm * iterm | `|-> of (vname * itype) * iterm @@ -236,13 +236,12 @@ add vs td #> fold (fn (p, t) => add vs p #> add vs t) bs; in add [] end; -fun eta_expand (c as (_, (_, ty)), ts) k = +fun eta_expand (c as (_, (_, tys)), ts) k = let val j = length ts; val l = k - j; - val tys = (curry Library.take l o curry Library.drop j o fst o unfold_fun) ty; val ctxt = (fold o fold_varnames) Name.declare ts Name.context; - val vs_tys = Name.names ctxt "a" tys; + val vs_tys = Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys); in vs_tys `|--> IConst c `$$ ts @ map (fn (v, _) => IVar v) vs_tys end; @@ -410,22 +409,15 @@ code |> (if can (get_def code) name then - tracing (fn _ => "asserting definition " ^ labelled_name name) - #> add_dp dep + add_dp dep else - tracing (fn _ => "allocating definition " ^ labelled_name name - ^ (if strict then " (strict)" else " (non-strict)")) - #> ensure_bot name + ensure_bot name #> add_dp dep - #> tracing (fn _ => "creating definition " ^ labelled_name name) #> invoke_generator name defgen #-> (fn def => prep_def def) #-> (fn def => - tracing (fn _ => "adding") - #> add_def_incr strict (name, def) - #> tracing (fn _ => "postprocessing") + add_def_incr strict (name, def) #> postprocess_def (name, def) - #> tracing (fn _ => "adding done") )) |> pair dep end;