# HG changeset patch # User haftmann # Date 1140019785 -3600 # Node ID 630b8dd0b31af958a27a1214eb340d5bfdd07f69 # Parent 1a8f08f9f8afbfe8efd6d89efdb60bb3760936ba exported some interfaces useful for other code generator approaches diff -r 1a8f08f9f8af -r 630b8dd0b31a src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Wed Feb 15 17:09:25 2006 +0100 +++ b/src/Pure/Tools/codegen_package.ML Wed Feb 15 17:09:45 2006 +0100 @@ -39,6 +39,11 @@ -> theory -> theory; val set_int_tyco: string -> theory -> theory; + val codegen_incr: term -> theory -> (string * CodegenThingol.def) list * theory; + val get_ml_fun_datatype: theory -> (string -> string) + -> ((string * CodegenThingol.funn) list -> Pretty.T) + * ((string * CodegenThingol.datatyp) list -> Pretty.T); + val appgen_default: appgen; val appgen_let: (int -> term -> term list * term) -> appgen; @@ -500,7 +505,7 @@ |> Symtab.update ( #ml CodegenSerializer.serializers |> apsnd (fn seri => seri - (nsp_dtcon, nsp_class, fn tyco' => tyco' = idf_of_name thy nsp_tyco tyco ) + (nsp_dtcon, nsp_class, fn tyco' => tyco' = idf_of_name thy nsp_tyco tyco) [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst]] ) ) @@ -591,7 +596,7 @@ trns |> debug 5 (fn _ => "trying defgen class declaration for " ^ quote cls) |> fold_map (ensure_def_class thy tabs) (ClassPackage.the_superclasses thy cls) - ||>> (codegen_type thy tabs o map snd) cs + ||>> (exprsgen_type thy tabs o map snd) cs ||>> (fold_map o fold_map) (exprgen_tyvar_sort thy tabs) sortctxts |-> (fn ((supcls, memtypes), sortctxts) => succeed (Class (supcls, ("a", idfs ~~ (sortctxts ~~ memtypes))))) @@ -620,7 +625,7 @@ trns |> debug 5 (fn _ => "trying defgen datatype for " ^ quote dtco) |> fold_map (exprgen_tyvar_sort thy tabs) vars - ||>> fold_map (fn (c, ty) => codegen_type thy tabs ty #-> (fn ty' => pair (c, ty'))) cos' + ||>> fold_map (fn (c, ty) => exprsgen_type thy tabs ty #-> (fn ty' => pair (c, ty'))) cos' |-> (fn (sorts, cos'') => succeed (Datatype (sorts, cos''))) end @@ -657,7 +662,7 @@ |> ensure_def_tyco thy tabs tyco ||>> fold_map (exprgen_type thy tabs) tys |-> (fn (tyco, tys) => pair (tyco `%% tys)) -and codegen_type thy tabs = +and exprsgen_type thy tabs = fold_map (exprgen_type thy tabs) o snd o devarify_typs; fun exprgen_classlookup thy tabs (ClassPackage.Instance (inst, ls)) trns = @@ -695,9 +700,9 @@ end; in trns - |> (codegen_eqs thy tabs o map dest_eqthm) eq_thms - ||>> (codegen_eqs thy tabs o the_list o Option.map mk_default) default - ||>> codegen_type thy tabs [ty] + |> (exprsgen_eqs thy tabs o map dest_eqthm) eq_thms + ||>> (exprsgen_eqs thy tabs o the_list o Option.map mk_default) default + ||>> exprsgen_type thy tabs [ty] ||>> fold_map (exprgen_tyvar_sort thy tabs) sortctxt |-> (fn (((eqs, eq_default), [ty]), sortctxt) => (pair o SOME) (eqs @ eq_default, (sortctxt, ty))) end @@ -825,18 +830,18 @@ ||>> fold_map (exprgen_term thy tabs) ts |-> (fn (e, es) => pair (e `$$ es)) end -and codegen_term thy tabs = +and exprsgen_term thy tabs = fold_map (exprgen_term thy tabs) o snd o devarify_term_typs -and codegen_eqs thy tabs = +and exprsgen_eqs thy tabs = apfst (map (fn (rhs::args) => (args, rhs))) - oo fold_burrow (codegen_term thy tabs) + oo fold_burrow (exprsgen_term thy tabs) o map (fn (args, rhs) => (rhs :: args)) and appgen_default thy tabs ((c, ty), ts) trns = trns |> ensure_def_const thy tabs (c, ty) ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs) (ClassPackage.extract_classlookup thy (c, ty)) - ||>> codegen_type thy tabs [ty] + ||>> exprsgen_type thy tabs [ty] ||>> fold_map (exprgen_term thy tabs) ts |-> (fn (((c, ls), [ty]), es) => pair (IConst ((c, ty), ls) `$$ es)) @@ -925,7 +930,7 @@ |> exprgen_type thy tabs ty' ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs) (ClassPackage.extract_classlookup thy (c, ty)) - ||>> codegen_type thy tabs [ty_def] + ||>> exprsgen_type thy tabs [ty_def] ||>> exprgen_term thy tabs tf ||>> exprgen_term thy tabs tx |-> (fn ((((_, ls), [ty]), tf), tx) => pair (IConst ((idf, ty), ls) `$ tf `$ tx)) @@ -988,6 +993,8 @@ fun mk_tabs thy = let + fun get_specifications thy c = + Defs.specifications_of (Theory.defs_of thy) c; fun extract_defs thy = let fun dest thm = @@ -1037,6 +1044,25 @@ |> fold (fn ty' => ConstNameMangler.declare (thy, deftab) (c, (ty, ty')) #> snd) tys) end; + (* über *alle*: (map fst o NameSpace.dest_table o Consts.space_of o Sign.consts_of) thy + * (c, ty) reicht dann zur zünftigen Deklaration + * somit fliegt ein Haufen Grusch raus, deftab bleibt allerdings wegen thyname + fun mk_overltabs thy = + (Symtab.empty, ConstNameMangler.empty) + |> Symtab.fold + (fn c => if (is_none o ClassPackage.lookup_const_class thy) c + then case get_specifications thy c + of [_] => NONE + | tys => fold + (fn (overltab1, overltab2) => ( + overltab1 + |> Symtab.update_new (c, (Sign.the_const_type thy c, tys)), + overltab2 + |> fold (fn (ty, (_, thyname)) => ConstNameMangler.declare (thy, deftab) + (c, (Sign.the_const_type thy c, ty)) #> snd) tys)) + else I + ) deftab + |> add_monoeq thy deftab;*) fun mk_overltabs thy deftab = (Symtab.empty, ConstNameMangler.empty) |> Symtab.fold @@ -1126,6 +1152,23 @@ fold ensure (get_datatype_case_consts thy) thy end; +fun codegen_incr t thy = + thy + |> `(#modl o CodegenData.get) + ||>> expand_module NONE (fn thy => fn tabs => exprsgen_term thy tabs [t]) + ||>> `(#modl o CodegenData.get) + |-> (fn ((modl_old, _), modl_new) => pair (CodegenThingol.diff_module (modl_new, modl_old))); + +fun get_ml_fun_datatype thy resolv = + let + val target_data = + ((fn data => (the o Symtab.lookup data) "ml") o #target_data o CodegenData.get) thy; + in + CodegenSerializer.ml_fun_datatype (nsp_dtcon, nsp_class, K false) + ((Option.map fst oo Symtab.lookup o #syntax_tyco) target_data, + (Option.map fst oo Symtab.lookup o #syntax_const) target_data) + resolv + end; (** target languages **) @@ -1200,11 +1243,15 @@ if Sign.declared_tyname thy tyco then tyco else error ("no such type constructor: " ^ quote tyco); - fun prep_tyco thy tyco = - tyco + fun prep_tyco thy raw_tyco = + raw_tyco |> Sign.intern_type thy |> check_tyco thy |> idf_of_name thy nsp_tyco; + fun no_args_tyco thy raw_tyco = + AList.lookup (op =) ((NameSpace.dest_table o #types o Type.rep_tsig o Sign.tsig_of) thy) + (Sign.intern_type thy raw_tyco) + |> (fn SOME ((Type.LogicalType i), _) => i); fun mk reader target thy = let val _ = get_serializer target; @@ -1225,7 +1272,8 @@ logic_data))) end; in - CodegenSerializer.parse_syntax (read_quote (fn thy => prep_tyco thy raw_tyco) read_typ codegen_type) + CodegenSerializer.parse_syntax (fn thy => no_args_tyco thy raw_tyco) + (read_quote (fn thy => prep_tyco thy raw_tyco) read_typ exprsgen_type) #-> (fn reader => pair (mk reader)) end; @@ -1246,6 +1294,8 @@ let fun prep_const thy raw_const = idf_of_const thy (mk_tabs thy) (read_const thy raw_const); + fun no_args_const thy raw_const = + (length o fst o strip_type o snd o read_const thy) raw_const; fun mk reader target thy = let val _ = get_serializer target; @@ -1257,7 +1307,8 @@ |-> (fn pretty => add_pretty_syntax_const c target pretty) end; in - CodegenSerializer.parse_syntax (read_quote (fn thy => prep_const thy raw_const) Sign.read_term codegen_term) + CodegenSerializer.parse_syntax (fn thy => no_args_const thy raw_const) + (read_quote (fn thy => prep_const thy raw_const) Sign.read_term exprsgen_term) #-> (fn reader => pair (mk reader)) end; diff -r 1a8f08f9f8af -r 630b8dd0b31a src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Wed Feb 15 17:09:25 2006 +0100 +++ b/src/Pure/Tools/codegen_serializer.ML Wed Feb 15 17:09:45 2006 +0100 @@ -18,14 +18,20 @@ -> string list option -> CodegenThingol.module -> unit) * OuterParse.token list; - val parse_syntax: (string -> 'b -> 'a * 'b) -> OuterParse.token list -> + val parse_syntax: ('b -> int) -> (string -> 'b -> 'a * 'b) -> OuterParse.token list -> ('b -> 'a pretty_syntax * 'b) * OuterParse.token list; val parse_targetdef: string -> CodegenThingol.prim list; val pretty_list: string -> string -> int * string -> CodegenThingol.iexpr pretty_syntax; val serializers: { ml: string * (string * string * (string -> bool) -> serializer), haskell: string * (string list -> serializer) - } + }; + val ml_fun_datatype: string * string * (string -> bool) + -> ((string -> CodegenThingol.itype pretty_syntax option) + * (string -> CodegenThingol.iexpr pretty_syntax option)) + -> (string -> string) + -> ((string * CodegenThingol.funn) list -> Pretty.T) + * ((string * CodegenThingol.datatyp) list -> Pretty.T); end; structure CodegenSerializer: CODEGEN_SERIALIZER = @@ -177,19 +183,20 @@ || pair (parse_nonatomic_mixfix reader, BR) ) -- OuterParse.string --| OuterParse.$$$ ")" >> (fn ((p, fxy), s) => (p s, fxy)); -fun parse_syntax reader = +fun parse_syntax no_args reader = let fun is_arg (Arg _) = true | is_arg Ignore = true | is_arg _ = false; - fun mk fixity mfx = + fun mk fixity mfx ctxt = let - val i = length (List.filter is_arg mfx) - in ((i, i), fillin_mixfix fixity mfx) end; + val i = (length o List.filter is_arg) mfx; + val _ = if i > no_args ctxt then error "too many arguments in codegen syntax" else (); + in (((i, i), fillin_mixfix fixity mfx), ctxt) end; in parse_syntax_proto reader - #-> (fn (mfx_reader, fixity) : ('Z -> 'Y mixfix list * 'Z) * fixity => - pair (mfx_reader #-> (fn mfx => pair (mk fixity mfx))) + #-> (fn (mfx_reader, fixity) => + pair (mfx_reader #-> (fn mfx => mk fixity mfx)) ) end; @@ -342,55 +349,39 @@ local -fun ml_from_defs (is_cons, needs_type) - (from_prim, (_, tyco_syntax, const_syntax)) resolver prefix defs = +fun ml_expr_seri (is_cons, needs_type) (tyco_syntax, const_syntax) resolv = let - val resolv = resolver prefix; - fun chunk_defs ps = - let - val (p_init, p_last) = split_last ps - in - Pretty.chunks (p_init @ [Pretty.block ([p_last, str ";"])]) - end; val ml_from_label = - resolv - #> NameSpace.base - #> translate_string (fn "_" => "__" | "." => "_" | c => c) - #> str; - fun ml_from_label' l = - Pretty.block [str "#", ml_from_label l]; - fun ml_from_lookup fxy [] p = - p - | ml_from_lookup fxy [l] p = - brackify fxy [ - ml_from_label' l, - p - ] - | ml_from_lookup fxy ls p = - brackify fxy [ - Pretty.enum " o" "(" ")" (map ml_from_label' ls), - p - ]; + str o translate_string (fn "_" => "__" | "." => "_" | c => c) + o NameSpace.base o resolv; fun ml_from_sortlookup fxy ls = let + fun from_label l = + Pretty.block [str "#", ml_from_label l]; + fun from_lookup fxy [] p = p + | from_lookup fxy [l] p = + brackify fxy [ + from_label l, + p + ] + | from_lookup fxy ls p = + brackify fxy [ + Pretty.enum " o" "(" ")" (map from_label ls), + p + ]; fun from_classlookup fxy (Instance (inst, lss)) = brackify fxy ( (str o resolv) inst :: map (ml_from_sortlookup BR) lss ) | from_classlookup fxy (Lookup (classes, (v, ~1))) = - ml_from_lookup BR classes (str v) + from_lookup BR classes (str v) | from_classlookup fxy (Lookup (classes, (v, i))) = - ml_from_lookup BR (string_of_int (i+1) :: classes) (str v) + from_lookup BR (string_of_int (i+1) :: classes) (str v) in case ls of [l] => from_classlookup fxy l | ls => (Pretty.list "(" ")" o map (from_classlookup NOBR)) ls end; - val ml_from_label = - resolv - #> NameSpace.base - #> translate_string (fn "_" => "__" | "." => "_" | c => c) - #> str; fun ml_from_tycoexpr fxy (tyco, tys) = let val tyco' = (str o resolv) tyco @@ -422,7 +413,7 @@ ml_from_type (INFX (1, R)) t2 ] end - | ml_from_type _ (IVarT (v, _)) = + | ml_from_type fxy (IVarT (v, _)) = str ("'" ^ v); fun ml_from_expr fxy (e as IApp (e1, e2)) = (case unfold_const_app e @@ -512,19 +503,29 @@ :: (lss @ map (ml_from_expr BR) es) ); + in (ml_from_label, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, ml_from_expr) end; + +fun ml_fun_datatyp (is_cons, needs_type) (tyco_syntax, const_syntax) resolv = + let + val (ml_from_label, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, ml_from_expr) = + ml_expr_seri (is_cons, needs_type) (tyco_syntax, const_syntax) resolv; + fun chunk_defs ps = + let + val (p_init, p_last) = split_last ps + in + Pretty.chunks (p_init @ [Pretty.block ([p_last, str ";"])]) + end; fun ml_from_funs (defs as def::defs_tl) = let fun mk_definer [] = "val" | mk_definer _ = "fun"; - fun check_args (_, Fun ((pats, _)::_, _)) NONE = + fun check_args (_, ((pats, _)::_, _)) NONE = SOME (mk_definer pats) - | check_args (_, Fun ((pats, _)::_, _)) (SOME definer) = + | check_args (_, ((pats, _)::_, _)) (SOME definer) = if mk_definer pats = definer then SOME definer else error ("mixing simultaneous vals and funs not implemented") - | check_args _ _ = - error ("function definition block containing other definitions than functions") - fun mk_fun definer (name, Fun (eqs as eq::eq_tl, (sortctxt, ty))) = + fun mk_fun definer (name, (eqs as eq::eq_tl, (sortctxt, ty))) = let val shift = if null eq_tl then I else map (Pretty.block o single); fun mk_eq definer (pats, expr) = @@ -545,16 +546,10 @@ chunk_defs ( mk_fun (the (fold check_args defs NONE)) def :: map (mk_fun "and") defs_tl - ) |> SOME + ) end; - fun ml_from_datatypes defs = + fun ml_from_datatypes (defs as (def::defs_tl)) = let - val defs' = List.mapPartial - (fn (name, Datatype info) => SOME (name, info) - | (name, Datatypecons _) => NONE - | (name, def) => error ("datatype block containing illegal def: " - ^ (Pretty.output o pretty_def) def) - ) defs fun mk_cons (co, []) = str (resolv co) | mk_cons (co, tys) = @@ -573,14 +568,27 @@ :: separate (str "|") (map mk_cons cs) ) in - case defs' - of (def::defs_tl) => - chunk_defs ( - mk_datatype "datatype" def - :: map (mk_datatype "and ") defs_tl - ) |> SOME - | _ => NONE - end + chunk_defs ( + mk_datatype "datatype" def + :: map (mk_datatype "and") defs_tl + ) + end; + in (ml_from_funs, ml_from_datatypes) end; + +fun ml_from_defs (is_cons, needs_type) + (from_prim, (_, tyco_syntax, const_syntax)) resolver prefix defs = + let + val resolv = resolver prefix; + val (ml_from_label, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, ml_from_expr) = + ml_expr_seri (is_cons, needs_type) (tyco_syntax, const_syntax) resolv; + val (ml_from_funs, ml_from_datatypes) = + ml_fun_datatyp (is_cons, needs_type) (tyco_syntax, const_syntax) resolv; + val filter_datatype = + List.mapPartial + (fn (name, Datatype info) => SOME (name, info) + | (name, Datatypecons _) => NONE + | (name, def) => error ("datatype block containing illegal def: " + ^ (Pretty.output o pretty_def) def)); fun ml_from_def (name, Undef) = error ("empty definition during serialization: " ^ quote name) | ml_from_def (name, Prim prim) = @@ -643,7 +651,7 @@ :: map (ml_from_sortlookup NOBR) lss ); fun from_memdef (m, def) = - ((the o ml_from_funs) [(m, Fun def)], Pretty.block [ + (ml_from_funs [(m, def)], Pretty.block [ ml_from_label m, Pretty.brk 1, str "=", @@ -679,12 +687,22 @@ ] |> SOME end; in case defs - of (_, Fun _)::_ => ml_from_funs defs - | (_, Datatypecons _)::_ => ml_from_datatypes defs - | (_, Datatype _)::_ => ml_from_datatypes defs + of (_, Fun _)::_ => (SOME o ml_from_funs o map (fn (name, Fun info) => (name, info))) defs + | (_, Datatypecons _)::_ => (SOME o ml_from_datatypes o filter_datatype) defs + | (_, Datatype _)::_ => (SOME o ml_from_datatypes o filter_datatype) defs | [def] => ml_from_def def end; +fun ml_annotators (nsp_dtcon, nsp_class, is_int_tyco) = + let + fun needs_type (IType (tyco, _)) = + has_nsp tyco nsp_class + orelse is_int_tyco tyco + | needs_type _ = + false; + fun is_cons c = has_nsp c nsp_dtcon; + in (is_cons, needs_type) end; + in fun ml_from_thingol target (nsp_dtcon, nsp_class, is_int_tyco) nspgrp = @@ -701,12 +719,7 @@ str "", str ("end; (* struct " ^ name ^ " *)") ]); - fun needs_type (IType (tyco, _)) = - has_nsp tyco nsp_class - orelse is_int_tyco tyco - | needs_type _ = - false; - fun is_cons c = has_nsp c nsp_dtcon; + val (is_cons, needs_type) = ml_annotators (nsp_dtcon, nsp_class, is_int_tyco); val serializer = abstract_serializer (target, nspgrp) "ROOT" (ml_from_defs (is_cons, needs_type), ml_from_module, abstract_validator reserved_ml, snd); @@ -744,6 +757,9 @@ (preprocess const_syntax) (class_syntax, tyco_syntax, const_syntax)) end; +fun ml_fun_datatype (nsp_dtcon, nsp_class, is_int_tyco) = + ml_fun_datatyp (ml_annotators (nsp_dtcon, nsp_class, is_int_tyco)); + end; (* local *) local diff -r 1a8f08f9f8af -r 630b8dd0b31a src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Wed Feb 15 17:09:25 2006 +0100 +++ b/src/Pure/Tools/codegen_thingol.ML Wed Feb 15 17:09:45 2006 +0100 @@ -45,6 +45,7 @@ val `|--> : iexpr list * iexpr -> iexpr; type funn = (iexpr list * iexpr) list * (ClassPackage.sortcontext * itype); + type datatyp = (vname * sort) list * (string * itype list) list; datatype prim = Pretty of Pretty.T | Name; @@ -53,7 +54,7 @@ | Prim of (string * prim list) list | Fun of funn | Typesyn of (vname * sort) list * itype - | Datatype of (vname * sort) list * (string * itype list) list + | Datatype of datatyp | Datatypecons of string | Class of class list * (vname * (string * (ClassPackage.sortcontext * itype)) list) | Classmember of class @@ -72,6 +73,7 @@ val ensure_prim: string -> string -> module -> module; val get_def: module -> string -> def; val merge_module: module * module -> module; + val diff_module: module * module -> (string * def) list; val partof: string list -> module -> module; val has_nsp: string -> string -> bool; val succeed: 'a -> transact -> 'a transact_fin; @@ -379,6 +381,7 @@ (* type definitions *) type funn = (iexpr list * iexpr) list * (ClassPackage.sortcontext * itype); +type datatyp = (vname * sort) list * (string * itype list) list; datatype prim = Pretty of Pretty.T @@ -389,7 +392,7 @@ | Prim of (string * prim list) list | Fun of funn | Typesyn of (vname * sort) list * itype - | Datatype of (vname * sort) list * (string * itype list) list + | Datatype of datatyp | Datatypecons of string | Class of class list * (vname * (string * (ClassPackage.sortcontext * itype)) list) | Classmember of class @@ -672,6 +675,23 @@ | join_module name _ = raise Graph.DUP name in Graph.join join_module modl12 end; +fun diff_module modl12 = + let + fun diff_entry prefix modl2 (name, Def def1) = + let + val e2 = try (Graph.get_node modl2) name + in if is_some e2 andalso eq_def (def1, (dest_def o the) e2) + then I + else cons (NameSpace.pack (prefix @ [name]), def1) + end + | diff_entry prefix modl2 (name, Module modl1) = + diff_modl (prefix @ [name]) (modl1, + (the_default empty_module o Option.map dest_modl o try (Graph.get_node modl2)) name) + and diff_modl prefix (modl1, modl2) = + fold (diff_entry prefix modl2) + ((AList.make (Graph.get_node modl1) o Library.flat o Graph.strong_conn) modl1) + in diff_modl [] modl12 [] end; + fun partof names modl = let datatype pathnode = PN of (string list * (string * pathnode) list);