# HG changeset patch # User haftmann # Date 1132936912 -3600 # Node ID b17724cae93533356f1a3b9f3a2c84138f664e9e # Parent 676d2e625d9872ab41e1dc4df5cd220b2fb3b35a code generator: case expressions, improved name resolving diff -r 676d2e625d98 -r b17724cae935 src/HOL/Tools/datatype_codegen.ML --- a/src/HOL/Tools/datatype_codegen.ML Fri Nov 25 14:51:39 2005 +0100 +++ b/src/HOL/Tools/datatype_codegen.ML Fri Nov 25 17:41:52 2005 +0100 @@ -10,6 +10,7 @@ val is_datatype: theory -> string -> bool val get_datatype: theory -> string -> (string list * string list) option val get_datacons: theory -> string * string -> typ list option + val get_case_const_data: theory -> string -> (string * int) list option; val setup: (theory -> theory) list end; @@ -264,17 +265,17 @@ fun datatype_codegen thy defs gr dep module brack t = (case strip_comb t of (c as Const (s, T), ts) => - (case find_first (fn (_, {index, descr, case_name, ...}) => + (case Library.find_first (fn (_, {index, descr, case_name, ...}) => s = case_name orelse AList.defined (op =) ((#3 o the o AList.lookup (op =) descr) index) s) (Symtab.dest (DatatypePackage.get_datatypes thy)) of NONE => NONE | SOME (tname, {index, descr, ...}) => - if isSome (get_assoc_code thy s T) then NONE else + if is_some (get_assoc_code thy s T) then NONE else let val SOME (_, _, constrs) = AList.lookup (op =) descr index in (case (AList.lookup (op =) constrs s, strip_type T) of (NONE, _) => SOME (pretty_case thy defs gr dep module brack - (#3 (valOf (AList.lookup (op =) descr index))) c ts) + ((#3 o the o AList.lookup (op =) descr) index) c ts) | (SOME args, (_, Type _)) => SOME (pretty_constr thy defs (fst (invoke_tycodegen thy defs dep module false (gr, snd (strip_type T)))) @@ -342,15 +343,26 @@ else NONE end; +fun get_case_const_data thy f = + case Library.find_first (fn (_, {index, descr, case_name, ...}) => + case_name = f + ) ((Symtab.dest o DatatypePackage.get_datatypes) thy) + of NONE => NONE + | SOME (_, {index, descr, ...}) => + (SOME o map (apsnd length) o #3 o the o AList.lookup (op =) descr) index; + + val setup = [ add_codegen "datatype" datatype_codegen, add_tycodegen "datatype" datatype_tycodegen, CodegenPackage.set_is_datatype is_datatype, - CodegenPackage.add_defgen + CodegenPackage.add_defgen ("datatype", CodegenPackage.defgen_datatype get_datatype), CodegenPackage.add_defgen - ("datacons", CodegenPackage.defgen_datacons get_datacons) + ("datacons", CodegenPackage.defgen_datacons get_datacons), + CodegenPackage.add_codegen_expr + ("case", CodegenPackage.codegen_case get_case_const_data) ]; end; diff -r 676d2e625d98 -r b17724cae935 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Fri Nov 25 14:51:39 2005 +0100 +++ b/src/Pure/Tools/codegen_package.ML Fri Nov 25 17:41:52 2005 +0100 @@ -59,6 +59,8 @@ -> codegen_expr; val codegen_number_of: (term -> IntInf.int) -> (term -> term) -> codegen_expr; + val codegen_case: (theory -> string -> (string * int) list option) + -> codegen_expr; val defgen_datatype: (theory -> string -> (string list * string list) option) -> defgen; val defgen_datacons: (theory -> string * string -> typ list option) @@ -66,7 +68,7 @@ val defgen_recfun: (theory -> string * typ -> (term list * term) list * typ) -> defgen; - val print_codegen_modl: theory -> unit; + val print_codegen_generated: theory -> unit; val mk_deftab: theory -> deftab; structure CodegenData: THEORY_DATA; structure Insttab: TABLE; @@ -117,7 +119,7 @@ val serializer_ml = let - val name_root = "module"; + val name_root = "Generated"; val nsp_conn_ml = [ [nsp_class, nsp_type, nsp_eq_class], [nsp_const, nsp_inst, nsp_mem, nsp_eq] ]; @@ -283,7 +285,7 @@ in CodegenData.put { modl = modl, gens = gens, lookups = lookups, serialize_data = serialize_data, logic_data = logic_data } thy end; -val print_codegen_modl = writeln o Pretty.output o pretty_module o #modl o CodegenData.get; +val print_codegen_generated = writeln o Pretty.output o pretty_module o #modl o CodegenData.get; fun add_codegen_sort (name, cg) = map_codegen_data @@ -527,39 +529,18 @@ |-> (fn ((eqs, ty), sortctxt) => pair (Fun (eqs, (sortctxt, ty)))) end; -fun mk_app thy defs f ty_use args trns = - let - val _ = debug 5 (fn _ => "making application of " ^ quote f) (); - val ty_def = Sign.the_const_constraint thy f; - val _ = debug 10 (fn _ => "making application (2)") (); - fun mk_lookup (ClassPackage.Instance (i, ls)) trns = - trns - |> ensure_def_class thy defs ((idf_of_name thy nsp_class o fst) i) - ||>> ensure_def_class thy defs (idf_of_inst thy defs i) - ||>> (fold_map o fold_map) mk_lookup ls - |-> (fn ((cls, i), ls) => pair (ClassPackage.Instance ((cls, i), ls))) - | mk_lookup (ClassPackage.Lookup (clss, (v, i))) trns = - trns - |> fold_map (ensure_def_class thy defs) (map (idf_of_name thy nsp_class) clss) - |-> (fn clss => pair (ClassPackage.Lookup (clss, (name_of_tvar (TFree (v, [])), i)))); - val _ = debug 10 (fn _ => "making application (3)") (); - fun mk_itapp e [] = e - | mk_itapp e lookup = IInst (e, lookup); - in +fun fix_nargs thy defs gen i (t, ts) trns = + if length ts < i + then trns - |> debug 10 (fn _ => "making application (4): " ^ f ^ "::" ^ Sign.string_of_typ thy ty_use) - |> ensure_def_const thy defs (idf_of_cname thy defs (f, ty_use)) - |> debug 10 (fn _ => "making application (5)") - ||>> fold_map (invoke_cg_expr thy defs) args - |> debug 10 (fn _ => "making application (6)") - ||>> (fold_map o fold_map) mk_lookup (ClassPackage.extract_sortlookup thy (ty_def, ty_use)) - |> debug 10 (fn _ => "making application (7)") - ||>> invoke_cg_type thy defs ty_use - |> debug 10 (fn _ => "making application (8)") - |-> (fn (((f, args), lookup), ty_use) => - pair (mk_apps (mk_itapp (IConst (f, ty_use)) lookup, args))) - end; - + |> debug 10 (fn _ => "eta-expanding") + |> gen (strip_comb (Codegen.eta_expand t ts i)) + else + trns + |> debug 10 (fn _ => "splitting arguments (" ^ string_of_int i ^ ", " ^ string_of_int (length ts) ^ ")") + |> gen (t, Library.take (i, ts)) + ||>> fold_map (invoke_cg_expr thy defs) (Library.drop (i, ts)) + |-> pair o mk_apps; local open CodegenThingolOp; @@ -568,6 +549,8 @@ infixr 6 `-->; infix 4 `$; infix 4 `$$; + infixr 5 `|->; + infixr 5 `|-->; in (* code generators *) @@ -597,38 +580,54 @@ ||>> fold_map (invoke_cg_type thy defs) tys |-> (fn (tyco, tys) => succeed (tyco `%% tys)) -fun codegen_expr_default thy defs t trns = - let - val (u, ts) = strip_comb t; - fun name_of_var (Free (v, _)) = v - | name_of_var (Var ((v, i), _)) = if i=0 then v else v ^ string_of_int i - fun cg_default (Var (_, ty)) = - trns - |> fold_map (invoke_cg_expr thy defs) ts - ||>> invoke_cg_type thy defs ty - |-> (fn (args, ty) => succeed (IVarE (name_of_var u, ty) `$$ args)) - | cg_default (Free (_, ty)) = - trns - |> fold_map (invoke_cg_expr thy defs) ts - ||>> invoke_cg_type thy defs ty - |-> (fn (args, ty) => succeed (IVarE (name_of_var u, ty) `$$ args)) - | cg_default (Const (f, ty)) = - trns - |> mk_app thy defs f ty ts - |-> (fn e => succeed e) - | cg_default (Abs _) = - let - val (bs, tys) = ListPair.unzip (strip_abs_vars u); - val t = strip_abs_body u; - val bs' = Codegen.new_names t bs; - val t' = subst_bounds (map Free (rev (bs' ~~ tys)), t) - in - trns - |> fold_map (invoke_cg_expr thy defs) ts - ||>> invoke_cg_expr thy defs t' - |-> (fn (es, e) => succeed (e `$$ es)) - end; - in cg_default u end; +fun codegen_expr_default thy defs (Const (f, ty)) trns = + let + val _ = debug 5 (fn _ => "making application of " ^ quote f) (); + val ty_def = Sign.the_const_constraint thy f; + val _ = debug 10 (fn _ => "making application (2)") (); + fun mk_lookup (ClassPackage.Instance (i, ls)) trns = + trns + |> ensure_def_class thy defs ((idf_of_name thy nsp_class o fst) i) + ||>> ensure_def_class thy defs (idf_of_inst thy defs i) + ||>> (fold_map o fold_map) mk_lookup ls + |-> (fn ((cls, i), ls) => pair (ClassPackage.Instance ((cls, i), ls))) + | mk_lookup (ClassPackage.Lookup (clss, (v, i))) trns = + trns + |> fold_map (ensure_def_class thy defs) (map (idf_of_name thy nsp_class) clss) + |-> (fn clss => pair (ClassPackage.Lookup (clss, (name_of_tvar (TFree (v, [])), i)))); + val _ = debug 10 (fn _ => "making application (3)") (); + fun mk_itapp e [] = e + | mk_itapp e lookup = IInst (e, lookup); + in + trns + |> debug 10 (fn _ => "making application (4): " ^ f ^ "::" ^ Sign.string_of_typ thy ty ^ " <~> " ^ Sign.string_of_typ thy ty_def) + |> ensure_def_const thy defs (idf_of_cname thy defs (f, ty)) + |> debug 10 (fn _ => "making application (5)") + ||>> (fold_map o fold_map) mk_lookup (ClassPackage.extract_sortlookup thy (ty_def, ty)) + |> debug 10 (fn _ => "making application (6)") + ||>> invoke_cg_type thy defs ty + |> debug 10 (fn _ => "making application (7)") + |-> (fn ((f, lookup), ty) => + succeed (mk_itapp (IConst (f, ty)) lookup)) + end + | codegen_expr_default thy defs (Free (v, ty)) trns = + trns + |> invoke_cg_type thy defs ty + |-> (fn ty => succeed (IVarE (v, ty))) + | codegen_expr_default thy defs (Var ((v, i), ty)) trns = + trns + |> invoke_cg_type thy defs ty + |-> (fn ty => succeed (IVarE (if i=0 then v else v ^ string_of_int i, ty))) + | codegen_expr_default thy defs (Abs (v, ty, t)) trns = + trns + |> invoke_cg_type thy defs ty + ||>> invoke_cg_expr thy defs (subst_bound (Free (v, ty), t)) + |-> (fn (ty, e) => succeed ((v, ty) `|-> e)) + | codegen_expr_default thy defs (t1 $ t2) trns = + trns + |> invoke_cg_expr thy defs t1 + ||>> invoke_cg_expr thy defs t2 + |-> (fn (e1, e2) => succeed (e1 `$ e2)); (*fun codegen_eq thy defs t trns = let @@ -810,6 +809,59 @@ trns |> fail ("not a number: " ^ Sign.string_of_term thy t); +fun codegen_case get_case_const_data thy defs t trns = + let + fun cg_case_d gen_names dty (((cname, i), ty), t) trns = + let + val vs = gen_names i; + val tys = Library.take (i, (fst o strip_type) ty); + val frees = map2 Free (vs, tys); + val t' = Envir.beta_norm (list_comb (t, frees)); + in + trns + |> invoke_cg_expr thy defs (list_comb (Const (cname, tys ---> dty), frees)) + ||>> invoke_cg_expr thy defs t' + |-> (fn (ep, e) => pair (ipat_of_iexpr ep, e)) + end; + fun cg_case dty cs (_, ts) trns = + let + val (ts', t) = split_last ts + val _ = debug 10 (fn _ => " in " ^ Sign.string_of_typ thy dty ^ ", pairing " + ^ (commas o map (fst o fst)) cs ^ " with " ^ (commas o map (Sign.string_of_term thy)) ts') (); + fun gen_names i = + variantlist (replicate i "x", foldr add_term_names + (map (fst o fst o dest_Var) (foldr add_term_vars [] ts)) ts) + in + trns + |> invoke_cg_expr thy defs t + ||>> fold_map (cg_case_d gen_names dty) (cs ~~ ts') + |-> (fn (t, ds) => pair (ICase (t, ds))) + end; + in case strip_comb t + of (t as Const (f, ty), ts) => + (case get_case_const_data thy f + of NONE => + trns + |> fail ("not a case constant: " ^ quote f) + | SOME cs => + let + val (tys, dty) = (split_last o fst o strip_type) ty; + in + trns + |> debug 9 (fn _ => "for case const " ^ f ^ "::" + ^ Sign.string_of_typ thy ty ^ ",\n with " ^ AList.string_of_alist I string_of_int cs + ^ ",\n given as args " ^ (commas o map (Sign.string_of_term thy)) ts + ^ ",\n with significant length " ^ string_of_int (length cs + 1)) + |> fix_nargs thy defs (cg_case dty (cs ~~ tys)) + (length cs + 1) (t, ts) + |-> succeed + end + ) + | _ => + trns + |> fail ("not a case constant expression: " ^ Sign.string_of_term thy t) + end; + fun defgen_datatype get_datatype thy defs tyco trns = case tname_of_idf thy tyco of SOME dtname => @@ -912,9 +964,8 @@ | mk_idf (nm, ty) = if is_number nm then nm - else idf_of_name thy nsp_const - (((perhaps o Symtab.lookup) ((fst o #alias o #logic_data o CodegenData.get) thy) nm) - ^ "_" ^ mangle_tyname (ty_decl, ty)) + else idf_of_name thy nsp_const nm + ^ "_" ^ mangle_tyname (ty_decl, ty) val overl_lookups = map (fn (ty, (_, (args, rhs))) => (ty, mk_idf (name, ty), args, rhs)) ds; in @@ -964,8 +1015,8 @@ classtab)) in ((Symtab.empty, Symtab.empty), Symtab.empty, (Insttab.empty, Symtab.empty, Symtab.empty)) + |> add_clsmems (ClassPackage.get_classtab thy) |> fold add_def (Codegen.mk_deftab thy |> Symtab.dest) - |> add_clsmems (ClassPackage.get_classtab thy) end; fun expand_module defs gen thy = @@ -1102,15 +1153,18 @@ (#serializer o (fn data => (the oo Symtab.lookup) data serial_name) o #serialize_data o CodegenData.get) thy; -fun mk_const thy f = +fun mk_const thy (f, s_ty) = let val f' = Sign.intern_const thy f; - in (f', Sign.the_const_constraint thy f') end; + val ty = case s_ty + of NONE => Sign.the_const_constraint thy f' + | SOME s => Sign.read_typ (thy, K NONE) s; + in (f', ty) end; -fun gen_generate_code consts thy = +fun generate_code consts thy = let val defs = mk_deftab thy; - val consts' = map (idf_of_cname thy defs) consts; + val consts' = map (idf_of_cname thy defs o mk_const thy) consts; fun generate thy defs = fold_map (ensure_def_const thy defs) consts' in thy @@ -1118,9 +1172,6 @@ |-> (fn _ => pair consts') end; -fun generate_code consts thy = - gen_generate_code (map (mk_const thy) consts) thy; - fun serialize_code serial_name filename consts thy = let fun mk_sfun tab name args f = @@ -1141,10 +1192,9 @@ if compile_it then use_text Context.ml_output false code else File.write (Path.unpack filename) (code ^ "\n"); - val consts' = Option.map (map (mk_const thy)) consts; in thy - |> (if is_some consts then gen_generate_code (the consts') else pair []) + |> (if is_some consts then generate_code (the consts) else pair []) |-> (fn [] => `(serializer' NONE o #modl o CodegenData.get) | consts => `(serializer' (SOME consts) o #modl o CodegenData.get)) |-> (fn code => ((use_code o Pretty.output) code; I)) @@ -1165,7 +1215,7 @@ val generateP = OuterSyntax.command generateK "generate executable code for constants" K.thy_decl ( - Scan.repeat1 P.name + Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) >> (fn consts => Toplevel.theory (generate_code consts #> snd)) ); @@ -1176,7 +1226,7 @@ -- P.name -- Scan.option ( P.$$$ extractingK - |-- Scan.repeat1 P.name + |-- Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) ) >> (fn ((serial_name, filename), consts) => Toplevel.theory (serialize_code serial_name filename consts)) @@ -1253,7 +1303,11 @@ add_alias ("op <>", "neq"), add_alias ("op >=", "ge"), add_alias ("op >", "gt"), + add_alias ("op <=", "le"), + add_alias ("op <", "lt"), + add_alias ("op +", "add"), add_alias ("op -", "minus"), + add_alias ("op *", "times"), add_alias ("op @", "append"), add_lookup_tyco ("bool", type_bool), add_lookup_tyco ("IntDef.int", type_integer), diff -r 676d2e625d98 -r b17724cae935 src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Fri Nov 25 14:51:39 2005 +0100 +++ b/src/Pure/Tools/codegen_serializer.ML Fri Nov 25 17:41:52 2005 +0100 @@ -282,10 +282,10 @@ ml_from_iexpr NOBR e ] in brackify (eval_br br BR) ( - Pretty.str "case " + Pretty.str "case" :: ml_from_iexpr NOBR e :: mk_clause "of " c - :: map (mk_clause "|") cs + :: map (mk_clause "| ") cs ) end | ml_from_iexpr br (IInst _) = error "cannot serialize poly instant to ML" @@ -391,13 +391,13 @@ | check_args (_, Fun ((pats, _)::_, _)) (SOME definer) = if mk_definer pats = definer then SOME definer - else error ("Mixing simultaneous vals and funs not implemented") + else error ("mixing simultaneous vals and funs not implemented") | check_args _ _ = - error ("Function definition block containing other definitions than functions") + error ("function definition block containing other definitions than functions") val definer = the (fold check_args ds NONE); - fun mk_eq definer f' ty (pats, expr) = + fun mk_eq definer f ty (pats, expr) = let - val lhs = [Pretty.str (definer ^ " " ^ f')] + val lhs = [Pretty.str (definer ^ " " ^ f)] @ (if null pats then [Pretty.str ":", ml_from_typ NOBR ty] else map (ml_from_pat BR) pats) @@ -407,15 +407,11 @@ end fun mk_fun definer (f, Fun (eqs as eq::eq_tl, (_, ty))) = let - val (pats_hd::pats_tl) = (fst o split_list) eqs - val _ = fold (fn x => fn y => (x ~~ y; y)) pats_tl pats_hd + val (pats_hd::pats_tl) = (fst o split_list) eqs; + val _ = fold (fn x => fn y => (x ~~ y; y)) pats_tl pats_hd; (*check for equal length of argument lists*) - in (Pretty.block o Pretty.fbreaks) ( - (*Pretty.block [ - Pretty.brk 1, - Pretty.str ": ", - ml_from_typ NOBR ty - ]*) + val shift = if null eq_tl then I else map (Pretty.block o single); + in (Pretty.block o Pretty.fbreaks o shift) ( mk_eq definer f ty eq :: map (mk_eq "|" f ty) eq_tl ) @@ -516,7 +512,7 @@ Pretty.str ("structure " ^ name ^ " = "), Pretty.str "struct", Pretty.str "" - ] @ ps @ [ + ] @ separate (Pretty.str "") ps @ [ Pretty.str "", Pretty.str ("end; (* struct " ^ name ^ " *)") ]); @@ -542,7 +538,7 @@ else 0 in module - |> debug 5 (Pretty.output o pretty_module) + |> debug 12 (Pretty.output o pretty_module) |> debug 3 (fn _ => "connecting datatypes and classdecls...") |> connect_datatypes_clsdecls |> debug 3 (fn _ => "selecting submodule...") @@ -551,7 +547,7 @@ |> eta_expand eta_expander |> debug 3 (fn _ => "eta-expanding polydefs...") |> eta_expand_poly - |> debug 5 (Pretty.output o pretty_module) + |> debug 12 (Pretty.output o pretty_module) |> debug 3 (fn _ => "tupelizing datatypes...") |> tupelize_cons |> debug 3 (fn _ => "eliminating classes...") diff -r 676d2e625d98 -r b17724cae935 src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Fri Nov 25 14:51:39 2005 +0100 +++ b/src/Pure/Tools/codegen_thingol.ML Fri Nov 25 17:41:52 2005 +0100 @@ -30,6 +30,7 @@ val eq_iexpr: iexpr * iexpr -> bool val mk_funs: itype list * itype -> itype; val mk_apps: iexpr * iexpr list -> iexpr; + val mk_abss: (vname * itype) list * iexpr -> iexpr; val pretty_itype: itype -> Pretty.T; val pretty_ipat: ipat -> Pretty.T; val pretty_iexpr: iexpr -> Pretty.T; @@ -129,6 +130,8 @@ val `--> : itype list * itype -> itype; val `$ : iexpr * iexpr -> iexpr; val `$$ : iexpr * iexpr list -> iexpr; + val `|-> : (vname * itype) * iexpr -> iexpr; + val `|--> : (vname * itype) list * iexpr -> iexpr; end; @@ -192,6 +195,8 @@ infixr 6 `-->; infix 4 `$; infix 4 `$$; +infixr 5 `|->; +infixr 5 `|-->; type vname = string; @@ -223,12 +228,15 @@ val mk_funs = Library.foldr IFun; val mk_apps = Library.foldl IApp; +val mk_abss = Library.foldr IAbs; -fun tyco `%% tys = IType (tyco, tys); +val op `%% = IType; val op `-> = IFun; -fun f `$ x = IApp (f, x); +val op `$ = IApp; +val op `|-> = IAbs; val op `--> = mk_funs; val op `$$ = mk_apps; +val op `|--> = mk_abss; val unfold_fun = unfoldr (fn IFun t => SOME t @@ -1171,10 +1179,12 @@ fun resolver modl name = if NameSpace.is_qualified name then let + val _ = debug 12 (fn name' => "resolving " ^ quote name ^ " in " ^ (quote o NameSpace.pack) modl) (); val modl' = if null modl then [] else (NameSpace.unpack o the o Symtab.lookup tab o NameSpace.pack) modl; val name' = (NameSpace.unpack o the o Symtab.lookup tab) name in (NameSpace.pack o #3 o get_prefix (op =)) (modl', name') + |> debug 12 (fn name' => "resolving " ^ quote name ^ " to " ^ quote name' ^ " in " ^ (quote o NameSpace.pack) modl) end else name in resolver end; @@ -1187,13 +1197,14 @@ val resolvtab = mk_resolvtab nspgrp validate module; val resolver = mk_resolv resolvtab; fun seri prfx ([(name, Module module)]) = - s_module (name, + s_module (resolver prfx (prfx @ [name] |> NameSpace.pack), (map (seri (prfx @ [name])) ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module))) | seri prfx ds = - s_def (resolver prfx) (map (fn (name, Def def) => (name, def)) ds) + s_def (resolver prfx) (map (fn (name, Def def) => (resolver prfx (prfx @ [name] |> NameSpace.pack), def)) ds) in - seri [] [(name_root, Module module)] + s_module (name_root, (map (seri []) + ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module))) end; end; (* struct *)