# HG changeset patch # User haftmann # Date 1133535931 -3600 # Node ID 99baddf6b0d01428b68f2693c5d3fe69dfe32129 # Parent a41ce9c10b738bbcbdeed006a347c138823f8467 various improvements diff -r a41ce9c10b73 -r 99baddf6b0d0 src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Fri Dec 02 16:05:12 2005 +0100 +++ b/src/Pure/Tools/class_package.ML Fri Dec 02 16:05:31 2005 +0100 @@ -7,10 +7,7 @@ signature CLASS_PACKAGE = sig - val add_consts: class * xstring list -> theory -> theory - val add_consts_i: class * string list -> theory -> theory - val add_tycos: class * xstring list -> theory -> theory - val add_tycos_i: class * (string * string) list -> theory -> theory + val add_classentry: class -> string list -> string list -> theory -> theory val the_consts: theory -> class -> string list val the_tycos: theory -> class -> (string * string) list @@ -165,7 +162,7 @@ fun get_const_sign thy tvar const = let val class = (the o lookup_const_class thy) const; - val ty = (Type.unvarifyT o Sign.the_const_constraint thy) const; + val (ty, thaw) = (Type.freeze_thaw_type o Sign.the_const_constraint thy) const; val tvars_used = Term.add_tfreesT ty []; val tvar_rename = hd (Term.invent_names (map fst tvars_used) tvar 1); in @@ -174,8 +171,9 @@ if Sorts.sort_eq (Sign.classes_of thy) ([class], sort) then TFree (tvar, []) else if tvar' = tvar - then TFree (tvar_rename, sort) + then TVar ((tvar_rename, 0), sort) else TFree (tvar', sort)) + |> thaw end; fun get_inst_consts_sign thy (tyco, class) = @@ -188,7 +186,7 @@ val vars_new = Term.invent_names vars_used "'a" (length arities); val typ_arity = Type (tyco, map2 (curry TFree) vars_new arities); val instmem_signs = - map (typ_subst_atomic [(TFree ("'a", []), typ_arity)]) const_signs; + map (typ_subst_TVars [(("'a", 0), typ_arity)]) const_signs; in consts ~~ instmem_signs end; fun get_classtab thy = @@ -202,8 +200,8 @@ type sortcontext = (string * sort) list; -fun extract_sortctxt thy typ = - (typ_tfrees o Type.unvarifyT) typ +fun extract_sortctxt thy ty = + (typ_tfrees o Type.no_tvars) ty |> map (apsnd (filter_class thy)) |> filter (not o null o snd); @@ -235,7 +233,7 @@ in Lookup (deriv, (vname, classindex)) end; in map mk_look sort_def end; in - extract_sortctxt thy raw_typ_def + extract_sortctxt thy ((fst o Type.freeze_thaw_type) raw_typ_def) |> map (tab_lookup o fst) |> map (apfst (filter_class thy)) |> filter (not o null o fst) @@ -243,18 +241,9 @@ end; -(* outer syntax *) - -local +(* intermediate auxiliary *) -structure P = OuterParse -and K = OuterKeyword; - -in - -val classcgK = "codegen_class"; - -fun classcg raw_class raw_consts raw_tycos thy = +fun add_classentry raw_class raw_consts raw_tycos thy = let val class = Sign.intern_class thy raw_class; in @@ -267,22 +256,8 @@ } |> add_consts (class, raw_consts) |> add_tycos (class, raw_tycos) - end - -val classcgP = - OuterSyntax.command classcgK "codegen data for classes" K.thy_decl ( - P.xname - -- ((P.$$$ "\\" || P.$$$ "=>") |-- (P.list1 P.name)) - -- (Scan.optional ((P.$$$ "\\" || P.$$$ "=>") |-- (P.list1 P.name)) []) - >> (fn ((name, tycos), consts) => (Toplevel.theory (classcg name consts tycos))) - ) - -val _ = OuterSyntax.add_parsers [classcgP]; - -val _ = OuterSyntax.add_keywords ["\\", "=>"]; - -end; (* local *) - + end; + (* setup *) diff -r a41ce9c10b73 -r 99baddf6b0d0 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Fri Dec 02 16:05:12 2005 +0100 +++ b/src/Pure/Tools/codegen_package.ML Fri Dec 02 16:05:31 2005 +0100 @@ -12,11 +12,10 @@ signature CODEGEN_PACKAGE = sig type deftab; - type exprgen_type; type exprgen_term; + type appgen; type defgen; - val add_codegen_type: string * exprgen_type -> theory -> theory; - val add_codegen_expr: string * exprgen_term -> theory -> theory; + val add_appgen: string * appgen -> theory -> theory; val add_defgen: string * defgen -> theory -> theory; val add_lookup_tyco: string * string -> theory -> theory; val add_lookup_const: (string * typ) * CodegenThingol.iexpr -> theory -> theory; @@ -53,18 +52,23 @@ val ensure_def_const: theory -> deftab -> string -> CodegenThingol.transact -> string * CodegenThingol.transact; - val codegen_let: (int -> term -> term list * term) - -> exprgen_term; - val codegen_split: (int -> term -> term list * term) - -> exprgen_term; - val codegen_number_of: (term -> IntInf.int) -> (term -> term) - -> exprgen_term; - val codegen_case: (theory -> string -> (string * int) list option) - -> exprgen_term; + val appgen_let: (int -> term -> term list * term) + -> appgen; + val appgen_split: (int -> term -> term list * term) + -> appgen; + val appgen_number_of: (term -> IntInf.int) -> (term -> term) + -> appgen; + val appgen_case: (theory -> string -> (string * int) list option) + -> appgen; val defgen_datatype: (theory -> string -> (string list * string list) option) + -> (theory -> string * string -> typ list option) -> defgen; val defgen_datacons: (theory -> string * string -> typ list option) -> defgen; + val defgen_datatype_eq: (theory -> string -> (string list * string list) option) + -> defgen; + val defgen_datatype_eqinst: (theory -> string -> (string list * string list) option) + -> defgen; val defgen_recfun: (theory -> string * typ -> (term list * term) list * typ) -> defgen; @@ -81,7 +85,8 @@ (* auxiliary *) -fun perhaps f x = f x |> the_default x; +fun devarify_term t = (fst o Type.freeze_thaw) t; +fun devarify_type ty = (fst o Type.freeze_thaw_type) ty; (* code generator instantiation, part 1 *) @@ -101,6 +106,7 @@ type exprgen_sort = theory -> deftab -> (sort, sort) gen_exprgen; type exprgen_type = theory -> deftab -> (typ, itype) gen_exprgen; type exprgen_term = theory -> deftab -> (term, iexpr) gen_exprgen; +type appgen = theory -> deftab -> ((string * typ) * term list, iexpr) gen_exprgen; type defgen = theory -> deftab -> gen_defgen; @@ -140,29 +146,31 @@ exprgens_sort: (string * (exprgen_sort * stamp)) list, exprgens_type: (string * (exprgen_type * stamp)) list, exprgens_term: (string * (exprgen_term * stamp)) list, + appgens: (string * (appgen * stamp)) list, defgens: (string * (defgen * stamp)) list }; val empty_gens = { exprgens_sort = Symtab.empty, exprgens_type = Symtab.empty, - exprgens_term = Symtab.empty, defgens = Symtab.empty + exprgens_term = Symtab.empty, defgens = Symtab.empty, appgens = Symtab.empty }; -fun map_gens f { exprgens_sort, exprgens_type, exprgens_term, defgens } = +fun map_gens f { exprgens_sort, exprgens_type, exprgens_term, appgens, defgens } = let - val (exprgens_sort, exprgens_type, exprgens_term, defgens) = - f (exprgens_sort, exprgens_type, exprgens_term, defgens) + val (exprgens_sort, exprgens_type, exprgens_term, appgens, defgens) = + f (exprgens_sort, exprgens_type, exprgens_term, appgens, defgens) in { exprgens_sort = exprgens_sort, exprgens_type = exprgens_type, - exprgens_term = exprgens_term, defgens = defgens } end; + exprgens_term = exprgens_term, appgens = appgens, defgens = defgens } end; fun merge_gens ({ exprgens_sort = exprgens_sort1, exprgens_type = exprgens_type1, - exprgens_term = exprgens_term1, defgens = defgens1 }, + exprgens_term = exprgens_term1, appgens = appgens1, defgens = defgens1 }, { exprgens_sort = exprgens_sort2, exprgens_type = exprgens_type2, - exprgens_term = exprgens_term2, defgens = defgens2 }) = + exprgens_term = exprgens_term2, appgens = appgens2, defgens = defgens2 }) = { exprgens_sort = AList.merge (op =) (eq_snd (op =)) (exprgens_sort1, exprgens_sort2), exprgens_type = AList.merge (op =) (eq_snd (op =)) (exprgens_type1, exprgens_type2), exprgens_term = AList.merge (op =) (eq_snd (op =)) (exprgens_term1, exprgens_term2), + appgens = AList.merge (op =) (eq_snd (op =)) (appgens1, appgens2), defgens = AList.merge (op =) (eq_snd (op =)) (defgens1, defgens2) } : gens; type lookups = { @@ -247,7 +255,7 @@ }; val empty = { modl = empty_module, - gens = { exprgens_sort = [], exprgens_type = [], exprgens_term = [], defgens = [] } : gens, + gens = { exprgens_sort = [], exprgens_type = [], exprgens_term = [], appgens = [], defgens = [] } : gens, lookups = { lookups_tyco = Symtab.empty, lookups_const = Symtab.empty } : lookups, logic_data = { is_datatype = NONE, alias = (Symtab.empty, Symtab.empty) } : logic_data, serialize_data = @@ -261,7 +269,10 @@ |> CodegenSerializer.add_prim ("wfrec", ("fun wfrec f x = f (wfrec f) x;", [])), syntax_tyco = Symtab.empty, syntax_const = Symtab.empty }) |> Symtab.update ("haskell", - { serializer = serializer_hs : CodegenSerializer.serializer, primitives = CodegenSerializer.empty_prims, + { serializer = serializer_hs : CodegenSerializer.serializer, + primitives = + CodegenSerializer.empty_prims + |> CodegenSerializer.add_prim ("wfrec", ("wfrec f x = f (wfrec f) x", [])), syntax_tyco = Symtab.empty, syntax_const = Symtab.empty }) } : T; val copy = I; @@ -297,43 +308,54 @@ (fn (modl, gens, lookups, serialize_data, logic_data) => (modl, gens |> map_gens - (fn (exprgens_sort, exprgens_type, exprgens_term, defgens) => + (fn (exprgens_sort, exprgens_type, exprgens_term, appgens, defgens) => (exprgens_sort |> Output.update_warn (op =) ("overwriting existing class code generator " ^ name) (name, (cg, stamp ())), - exprgens_type, exprgens_term, defgens)), lookups, serialize_data, logic_data)); + exprgens_type, exprgens_term, appgens, defgens)), lookups, serialize_data, logic_data)); fun add_codegen_type (name, cg) = map_codegen_data (fn (modl, gens, lookups, serialize_data, logic_data) => (modl, gens |> map_gens - (fn (exprgens_sort, exprgens_type, exprgens_term, defgens) => + (fn (exprgens_sort, exprgens_type, exprgens_term, appgens, defgens) => (exprgens_sort, exprgens_type |> Output.update_warn (op =) ("overwriting existing type code generator " ^ name) (name, (cg, stamp ())), - exprgens_term, defgens)), lookups, serialize_data, logic_data)); + exprgens_term, appgens, defgens)), lookups, serialize_data, logic_data)); fun add_codegen_expr (name, cg) = map_codegen_data (fn (modl, gens, lookups, serialize_data, logic_data) => (modl, gens |> map_gens - (fn (exprgens_sort, exprgens_type, exprgens_term, defgens) => + (fn (exprgens_sort, exprgens_type, exprgens_term, appgens, defgens) => (exprgens_sort, exprgens_type, exprgens_term |> Output.update_warn (op =) ("overwriting existing expression code generator " ^ name) (name, (cg, stamp ())), - defgens)), + appgens, defgens)), lookups, serialize_data, logic_data)); +fun add_appgen (name, ag) = + map_codegen_data + (fn (modl, gens, lookups, serialize_data, logic_data) => + (modl, + gens |> map_gens + (fn (exprgens_sort, exprgens_type, exprgens_term, appgens, defgens) => + (exprgens_sort, exprgens_type, exprgens_term, + appgens + |> Output.update_warn (op =) ("overwriting existing definition application generator " ^ name) (name, (ag, stamp ())), + defgens)), lookups, serialize_data, logic_data)); + fun add_defgen (name, dg) = map_codegen_data (fn (modl, gens, lookups, serialize_data, logic_data) => (modl, gens |> map_gens - (fn (exprgens_sort, exprgens_type, exprgens_term, defgens) => + (fn (exprgens_sort, exprgens_type, exprgens_term, appgens, defgens) => (exprgens_sort, exprgens_type, exprgens_term, - defgens - |> Output.update_warn (op =) ("overwriting existing definition code generator " ^ name) (name, (dg, stamp ())))), + appgens, defgens + |> Output.update_warn (op =) ("overwriting existing definition definition generator " ^ name) (name, (dg, stamp ())))), lookups, serialize_data, logic_data)); val get_lookups_tyco = #lookups_tyco o #lookups o CodegenData.get; @@ -450,17 +472,6 @@ | s => s; -(* auxiliary *) - -fun find_lookup_expr thy (f, ty) = - Symtab.lookup_multi ((#lookups_const o #lookups o CodegenData.get) thy) f - |> (fn tab => AList.lookup (Sign.typ_instance thy) tab ty) - -fun name_of_tvar (TFree (v, _)) = v |> unprefix "'" - | name_of_tvar (TVar ((v, i), _)) = - (if i=0 then v else v ^ string_of_int i) |> unprefix "'" - - (* code generator instantiation, part 2 *) fun invoke_cg_sort thy defs sort trns = @@ -478,14 +489,30 @@ ((map (apsnd (fn (cg, _) => cg thy defs)) o #exprgens_term o #gens o CodegenData.get) thy) ("generating expression " ^ (quote o Sign.string_of_term thy) t) t trns; +fun invoke_appgen thy defs (app as ((f, ty), ts)) trns = + gen_invoke + ((map (apsnd (fn (ag, _) => ag thy defs)) o #appgens o #gens o CodegenData.get) thy) + ("generating application " ^ f ^ "::" ^ (Sign.string_of_typ thy) ty + ^ " " ^ enclose "(" ")" (commas (map (Sign.string_of_term thy) ts))) app trns; + +fun find_lookup_expr thy (f, ty) = + Symtab.lookup_multi ((#lookups_const o #lookups o CodegenData.get) thy) f + |> (fn tab => AList.lookup (Sign.typ_instance thy) tab ty); + fun get_defgens thy defs = (map (apsnd (fn (dg, _) => dg thy defs)) o #defgens o #gens o CodegenData.get) thy; -fun ensure_def_class thy defs cls_or_inst trns = +fun ensure_def_class thy defs cls trns = trns - |> debug 4 (fn _ => "generating class or instance " ^ quote cls_or_inst) - |> gen_ensure_def (get_defgens thy defs) ("generating class/instance " ^ quote cls_or_inst) cls_or_inst - |> pair cls_or_inst; + |> debug 4 (fn _ => "generating class " ^ quote cls) + |> gen_ensure_def (get_defgens thy defs) ("generating class " ^ quote cls) cls + |> pair cls; + +fun ensure_def_instance thy defs inst trns = + trns + |> debug 4 (fn _ => "generating instance " ^ quote inst) + |> gen_ensure_def (get_defgens thy defs) ("generating instance " ^ quote inst) inst + |> pair inst; fun ensure_def_tyco thy defs tyco trns = if NameSpace.is_qualified tyco @@ -506,9 +533,9 @@ of NONE => trns |> debug 4 (fn _ => "generating constant " ^ quote f) - |> invoke_cg_type thy defs (cname_of_idf thy defs f |> the |> snd) + |> invoke_cg_type thy defs (cname_of_idf thy defs f |> the |> snd |> devarify_type) ||> gen_ensure_def (get_defgens thy defs) ("generating constant " ^ quote f) f - |-> (fn ty' => pair f) + |-> (fn _ => pair f) | SOME (IConst (f, ty)) => trns |> pair f @@ -523,29 +550,34 @@ |-> (fn sort => pair (unprefix "'" v, sort)) fun mk_eq (args, rhs) trns = trns - |> fold_map (invoke_cg_expr thy defs) args - ||>> invoke_cg_expr thy defs rhs + |> fold_map (invoke_cg_expr thy defs o devarify_term) args + ||>> (invoke_cg_expr thy defs o devarify_term) rhs |-> (fn (args, rhs) => pair (map ipat_of_iexpr args, rhs)) in trns |> fold_map mk_eq eqs - ||>> invoke_cg_type thy defs ty + ||>> invoke_cg_type thy defs (devarify_type ty) ||>> fold_map mk_sortvar sortctxt |-> (fn ((eqs, ty), sortctxt) => pair (Fun (eqs, (sortctxt, ty)))) end; -fun fix_nargs thy defs gen i (t, ts) trns = - if length ts < i - then +fun fix_nargs thy defs gen (imin, imax) (t, ts) trns = + if length ts < imin then trns |> debug 10 (fn _ => "eta-expanding") - |> gen (strip_comb (Codegen.eta_expand t ts i)) + |> gen (strip_comb (Codegen.eta_expand t ts imin)) + |-> succeed + else if length ts > imax then + trns + |> debug 10 (fn _ => "splitting arguments (" ^ string_of_int imax ^ ", " ^ string_of_int (length ts) ^ ")") + |> gen (t, Library.take (imax, ts)) + ||>> fold_map (invoke_cg_expr thy defs) (Library.drop (imax, ts)) + |-> succeed o mk_apps 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; + |> debug 10 (fn _ => "keeping arguments") + |> gen (t, ts) + |-> succeed; local open CodegenThingolOp; @@ -566,14 +598,12 @@ (sort |> filter (ClassPackage.is_class thy) |> map (idf_of_name thy nsp_class)) |-> (fn sort => succeed sort) -fun exprgen_type_default thy defs(v as TVar (_, sort)) trns = +fun exprgen_type_default thy defs (TVar _) trns = + error "TVar encountered during code generation" + | exprgen_type_default thy defs (TFree (v, sort)) trns = trns |> invoke_cg_sort thy defs sort - |-> (fn sort => succeed (IVarT (name_of_tvar v, sort))) - | exprgen_type_default thy defs (v as TFree (_, sort)) trns = - trns - |> invoke_cg_sort thy defs sort - |-> (fn sort => succeed (IVarT (name_of_tvar v, sort))) + |-> (fn sort => succeed (IVarT (v |> unprefix "'", sort))) | exprgen_type_default thy defs (Type ("fun", [t1, t2])) trns = trns |> invoke_cg_type thy defs t1 @@ -586,53 +616,85 @@ |-> (fn (tyco, tys) => succeed (tyco `%% tys)) fun exprgen_term_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 + trns + |> invoke_appgen thy defs ((f, ty), []) + |-> (fn e => succeed e) + | exprgen_term_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))) | exprgen_term_default thy defs (Free (v, ty)) trns = trns |> invoke_cg_type thy defs ty |-> (fn ty => succeed (IVarE (v, ty))) - | exprgen_term_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))) | exprgen_term_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)) - | exprgen_term_default thy defs (t1 $ t2) trns = + | exprgen_term_default thy defs (t as t1 $ t2) trns = + let + val (t', ts) = strip_comb t + in case t' + of Const (f, ty) => + trns + |> invoke_appgen thy defs ((f, ty), ts) + |-> (fn e => succeed e) + | _ => + trns + |> invoke_cg_expr thy defs t' + ||>> fold_map (invoke_cg_expr thy defs) ts + |-> (fn (e, es) => succeed (e `$$ es)) + end; + +fun appgen_default thy defs ((f, ty), ts) 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_instance 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, (v |> unprefix "'", 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)") + ||>> fold_map (invoke_cg_expr thy defs) ts + ||> debug 10 (fn _ => "making application (8)") + |-> (fn (((f, lookup), ty), es) => + succeed (mk_itapp (IConst (f, ty)) lookup `$$ es)) + end + +fun appgen_neg thy defs (f as ("neg", Type ("fun", [ty, _])), ts) trns = + let + fun gen_neg _ trns = + trns + |> invoke_cg_expr thy defs (Const ("op >", ty --> ty --> Type ("bool", [])) $ Const ("0", ty)) + in + trns + |> fix_nargs thy defs gen_neg (0, 0) (Const f, ts) + end + | appgen_neg thy defs ((f, _), _) trns = trns - |> invoke_cg_expr thy defs t1 - ||>> invoke_cg_expr thy defs t2 - |-> (fn (e1, e2) => succeed (e1 `$ e2)); + |> fail ("not a negation: " ^ quote f); + +fun exprgen_term_eq thy defs (Const ("op =", Type ("fun", [ty, _]))) trns = + trns (*fun codegen_eq thy defs t trns = let @@ -650,18 +712,6 @@ |> fail ("no equality: " ^ Sign.string_of_term thy t) in cg_eq (strip_comb t) end;*) -fun codegen_neg thy defs t trns = - let - val (u, ts) = strip_comb t; - fun cg_neg (Const ("neg", _)) = - trns - |> invoke_cg_expr thy defs (hd ts) - |-> (fn e => succeed (Fun_lt `$ e `$ IConst ("0", Type_integer))) - | cg_neg _ = - trns - |> fail ("no negation: " ^ Sign.string_of_term thy t) - in cg_neg u end; - (* definition generators *) @@ -692,7 +742,7 @@ of SOME (args, rhs, ty) => trns |> debug 5 (fn _ => "trying defgen def for " ^ quote f) - |> mk_fun thy defs [(args, rhs)] ty + |> mk_fun thy defs [(args, rhs)] (devarify_type ty) |-> (fn def => succeed (def, [])) | _ => trns |> fail ("no definition found for " ^ quote f); @@ -721,7 +771,7 @@ in trns |> debug 5 (fn _ => "trying defgen class member for " ^ quote f) - |> invoke_cg_type thy defs ty + |> (invoke_cg_type thy defs o devarify_type) ty |-> (fn ty => succeed (Classmember (cls, "a", ty), [])) end | _ => @@ -731,16 +781,22 @@ case inst_of_idf thy defs clsinst of SOME (cls, tyco) => let + val _ = debug 10 (fn _ => "(1) CLSINST " ^ cls ^ " - " ^ tyco) () val arity = (map o map) (idf_of_name thy nsp_class) (ClassPackage.get_arities thy [cls] tyco); + val _ = debug 10 (fn _ => "(2) CLSINST " ^ cls ^ " - " ^ tyco) () val clsmems = map (idf_of_name thy nsp_mem) (ClassPackage.the_consts thy cls); + val _ = debug 10 (fn _ => "(3) CLSINST " ^ cls ^ " - " ^ tyco) () + val _ = debug 10 (fn _ => AList.string_of_alist I (Sign.string_of_typ thy) (ClassPackage.get_inst_consts_sign thy (tyco, cls))) () val instmem_idfs = map (idf_of_cname thy defs) (ClassPackage.get_inst_consts_sign thy (tyco, cls)); - fun add_vars arity clsmems (trns as (_, univ)) = + val _ = debug 10 (fn _ => "(4) CLSINST " ^ cls ^ " - " ^ tyco) () + fun add_vars arity clsmems (trns as (_, modl)) = ((Term.invent_names - (map ((fn Classmember (_, _, ty) => ty) o get_def univ) + (map ((fn Classmember (_, _, ty) => ty) o get_def modl) clsmems |> tvars_of_itypes) "a" (length arity) ~~ arity, clsmems), trns) + val _ = debug 10 (fn _ => "(5) CLSINST " ^ cls ^ " - " ^ tyco) () in trns |> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls ^ ", " ^ quote tyco ^ ")") @@ -759,69 +815,82 @@ (* parametrized generators, for instantiation in HOL *) -fun codegen_let strip_abs thy defs t trns = - let - fun dest_let (l as Const ("Let", _) $ t $ u) = - (case strip_abs 1 u - of ([p], u') => apfst (cons (p, t)) (dest_let u') - | _ => ([], l)) - | dest_let t = ([], t); - fun mk_let (l, r) trns = - trns - |> invoke_cg_expr thy defs l - ||>> invoke_cg_expr thy defs r - |-> (fn (l, r) => pair (r, ipat_of_iexpr l)); - fun cg_let' ([], _) _ = +fun appgen_let strip_abs thy defs (f as ("Let", _), ts) trns = + let + fun dest_let (l as Const ("Let", _) $ t $ u) = + (case strip_abs 1 u + of ([p], u') => apfst (cons (p, t)) (dest_let u') + | _ => ([], l)) + | dest_let t = ([], t); + fun mk_let (l, r) trns = trns - |> fail ("no let expression: " ^ Sign.string_of_term thy t) - | cg_let' (lets, body) args = - trns - |> fold_map mk_let lets - ||>> invoke_cg_expr thy defs body - ||>> fold_map (invoke_cg_expr thy defs) args - |-> (fn ((lets, body), args) => - succeed (Library.foldr (fn ((e, p), body) => ICase (e, [(p, body)])) (lets, body) `$$ args)) - fun cg_let (t1 as Const ("Let", _), t2 :: t3 :: ts) = - cg_let' (dest_let (t1 $ t2 $ t3)) ts - | cg_let _ = - trns - |> fail ("no let expression: " ^ Sign.string_of_term thy t); - in cg_let (strip_comb t) end; + |> invoke_cg_expr thy defs l + ||>> invoke_cg_expr thy defs r + |-> (fn (l, r) => pair (r, ipat_of_iexpr l)); + fun gen_let (t1, [t2, t3]) trns = + let + val (lets, body) = dest_let (t1 $ t2 $ t3) + in + trns + |> fold_map mk_let lets + ||>> invoke_cg_expr thy defs body + |-> (fn (lets, body) => + pair (Library.foldr (fn ((e, p), body) => ICase (e, [(p, body)])) (lets, body))) + end; + in + trns + |> fix_nargs thy defs gen_let (2, 2) (Const f, ts) + end + | appgen_let strip_abs thy defs ((f, _), _) trns = + trns + |> fail ("not a let: " ^ quote f); -fun codegen_split strip_abs thy defs t trns = - let - fun cg_split' ([p], body) args = - trns - |> invoke_cg_expr thy defs p - ||>> invoke_cg_expr thy defs body - ||>> fold_map (invoke_cg_expr thy defs) args - |-> (fn (((IVarE v), body), args) => succeed (IAbs (v, body) `$$ args)) - | cg_split' _ _ = - trns - |> fail ("no split expression: " ^ Sign.string_of_term thy t); - fun cg_split (t1 as Const ("split", _), t2 :: ts) = - cg_split' (strip_abs 1 (t1 $ t2)) ts - | cg_split _ = +fun appgen_split strip_abs thy defs (f as ("split", _), ts) trns = + let + fun gen_split (t1, [t2]) trns = + let + val ([p], body) = strip_abs 1 (t1 $ t2) + in + trns + |> invoke_cg_expr thy defs p + ||>> invoke_cg_expr thy defs body + |-> (fn (IVarE v, body) => pair (IAbs (v, body))) + end + in + trns + |> fix_nargs thy defs gen_split (1, 1) (Const f, ts) + end + | appgen_split strip_abs thy defs ((f, _), _) trns = + trns + |> fail ("not a split: " ^ quote f); + +fun appgen_number_of dest_binum mk_int_to_nat thy defs (f as ("Numeral.number_of", + Type ("fun", [_, Type ("IntDef.int", [])])), ts) trns = + let + fun gen_num (_, [bin]) trns = trns - |> fail ("no split expression: " ^ Sign.string_of_term thy t); - in cg_split (strip_comb t) end; - -fun codegen_number_of dest_binum mk_int_to_nat thy defs (Const ("Numeral.number_of", - Type ("fun", [_, Type ("IntDef.int", [])])) $ bin) trns = + |> (pair (IConst ((IntInf.toString o dest_binum) bin, Type_integer)) + handle TERM _ + => error ("not a number: " ^ Sign.string_of_term thy bin)) + in + trns + |> fix_nargs thy defs gen_num (1, 1) (Const f, ts) + end + | appgen_number_of dest_binum mk_int_to_nat thy defs (f as ("Numeral.number_of", + Type ("fun", [_, Type ("nat", [])])), ts) trns = + let + fun gen_num (_, [bin]) trns = + trns + |> invoke_cg_expr thy defs (mk_int_to_nat bin) + in + trns + |> fix_nargs thy defs gen_num (1, 1) (Const f, ts) + end + | appgen_number_of dest_binum mk_int_to_nat thy defs ((f, _), _) trns = trns - |> (succeed (IConst ((IntInf.toString o dest_binum) bin, Type_integer)) - handle TERM _ - => fail ("not a number: " ^ Sign.string_of_term thy bin)) - | codegen_number_of dest_binum mk_int_to_nat thy defs (Const ("Numeral.number_of", - Type ("fun", [_, Type ("nat", [])])) $ bin) trns = - trns - |> invoke_cg_expr thy defs (mk_int_to_nat bin) - |-> (fn expr => succeed expr) - | codegen_number_of dest_binum mk_int_to_nat thy defs t trns = - trns - |> fail ("not a number: " ^ Sign.string_of_term thy t); + |> fail ("not a number_of: " ^ quote f); -fun codegen_case get_case_const_data thy defs t trns = +fun appgen_case get_case_const_data thy defs ((f, ty), ts) trns = let fun cg_case_d gen_names dty (((cname, i), ty), t) trns = let @@ -849,42 +918,47 @@ ||>> 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 caseconstant expression: " ^ Sign.string_of_term thy t) + in + 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, length cs + 1) (Const (f, ty), ts) + end end; -fun defgen_datatype get_datatype thy defs tyco trns = +local + +fun add_eqinst get_datacons thy modl dtname cnames = + if forall (is_eqtype modl) + (Library.flat (map (fn cname => get_datacons thy (cname, dtname)) cnames)) + then append [idf_of_name thy nsp_eq_class dtname] + else I + +in + +fun defgen_datatype get_datatype get_datacons thy defs tyco trns = case tname_of_idf thy tyco of SOME dtname => - (case get_datatype thy tyco + (case get_datatype thy dtname of SOME (vs, cnames) => trns |> debug 5 (fn _ => "trying defgen datatype for " ^ quote dtname) |> succeed (Datatype (map (rpair [] o unprefix "'") vs, [], []), cnames |> map (idf_of_name thy nsp_const) - |> map (fn "0" => "const.Zero" | c => c)) + |> map (fn "0" => "const.Zero" | c => c) + (* |> add_eqinst get_datacons thy (snd trns) dtname cnames *)) (*! VARIABLEN, EQTYPE !*) | NONE => trns @@ -894,6 +968,8 @@ |> fail ("not a type constructor: " ^ quote tyco) end; +end; (* local *) + fun defgen_datacons get_datacons thy defs f trns = let fun the_type "0" = SOME "nat" @@ -911,7 +987,7 @@ trns |> debug 5 (fn _ => "trying defgen datatype constructor for " ^ quote c) |> ensure_def_tyco thy defs (idf_of_tname thy dtname) - ||>> fold_map (invoke_cg_type thy defs) tyargs + ||>> fold_map (invoke_cg_type thy defs o devarify_type) tyargs |-> (fn (dtname, tys) => succeed (Datatypecons (dtname, tys), [])) | NONE => trns @@ -924,6 +1000,42 @@ |> fail ("not a constant: " ^ quote f) end; +fun defgen_datatype_eq get_datatype thy defs f trns = + case name_of_idf thy nsp_eq f + of SOME dtname => + (case get_datatype thy dtname + of SOME (_, cnames) => + trns + |> debug 5 (fn _ => "trying defgen datatype_eq for " ^ quote dtname) + |> ensure_def_tyco thy defs (idf_of_tname thy dtname) + ||>> fold_map (ensure_def_const thy defs) (cnames + |> map (idf_of_name thy nsp_const) + |> map (fn "0" => "const.Zero" | c => c)) + ||>> `(fn (_, modl) => build_eqpred modl dtname) + |-> (fn (_, eqpred) => succeed (eqpred, [])) + | NONE => + trns + |> fail ("no datatype found for " ^ quote dtname)) + | NONE => + trns + |> fail ("not an equality predicate: " ^ quote f) + +fun defgen_datatype_eqinst get_datatype thy defs f trns = + case name_of_idf thy nsp_eq_class f + of SOME dtname => + (case get_datatype thy dtname + of SOME (vs, _) => + trns + |> debug 5 (fn _ => "trying defgen datatype_eqinst for " ^ quote dtname) + |> ensure_def_const thy defs (idf_of_name thy nsp_eq dtname) + |-> (fn pred_eq => succeed (Classinst (class_eq, (dtname, vs ~~ replicate (length vs) [class_eq]), [(fun_eq, pred_eq)]), [])) + | NONE => + trns + |> fail ("no datatype found for " ^ quote dtname)) + | NONE => + trns + |> fail ("not an equality instance: " ^ quote f) + fun defgen_recfun get_equations thy defs f trns = case cname_of_idf thy defs f of SOME (f, ty) => @@ -934,7 +1046,7 @@ of (_::_) => trns |> debug 5 (fn _ => "trying defgen recfun for " ^ quote f) - |> mk_fun thy defs eqs ty + |> mk_fun thy defs eqs (devarify_type ty) |-> (fn def => succeed (def, [])) | _ => trns @@ -1033,6 +1145,11 @@ |> fold add_def (Codegen.mk_deftab thy |> Symtab.dest) end; +fun check_for_serializer serial_name serialize_data = + if Symtab.defined serialize_data serial_name + then serialize_data + else error ("unknown code serializer: " ^ quote serial_name); + fun expand_module defs gen thy = let fun put_module modl = @@ -1063,7 +1180,7 @@ |-> (fn mfx => map_codegen_data (fn (modl, gens, lookups, serialize_data, logic_data) => (modl, gens, lookups, - serialize_data |> Symtab.map_entry serial_name + serialize_data |> check_for_serializer serial_name |> Symtab.map_entry serial_name (map_serialize_data (fn (primitives, syntax_tyco, syntax_const) => (primitives |> add_primdef primdef, @@ -1088,7 +1205,7 @@ let val proto_mfx = Codegen.parse_mixfix (typ_of o read_ctyp thy) mfx; - fun generate thy defs = fold_map (invoke_cg_type thy defs) + fun generate thy defs = fold_map (invoke_cg_type thy defs o devarify_type) (Codegen.quotes_of proto_mfx); in thy @@ -1115,7 +1232,7 @@ |-> (fn mfx => map_codegen_data (fn (modl, gens, lookups, serialize_data, logic_data) => (modl, gens, lookups, - serialize_data |> Symtab.map_entry serial_name + serialize_data |> check_for_serializer serial_name |> Symtab.map_entry serial_name (map_serialize_data (fn (primitives, syntax_tyco, syntax_const) => (primitives |> add_primdef primdef, @@ -1149,7 +1266,7 @@ let val proto_mfx = Codegen.parse_mixfix (term_of o read_cterm thy o rpair TypeInfer.logicT) mfx; - fun generate thy defs = fold_map (invoke_cg_expr thy defs) + fun generate thy defs = fold_map (invoke_cg_expr thy defs o devarify_term) (Codegen.quotes_of proto_mfx); in thy @@ -1198,6 +1315,7 @@ thy |> CodegenData.get |> #serialize_data + |> check_for_serializer serial_name |> (fn data => (the oo Symtab.lookup) data serial_name) val serializer' = (get_serializer thy serial_name) ((mk_sfun o #syntax_tyco) serialize_data) @@ -1227,8 +1345,18 @@ in -val (generateK, serializeK, extractingK, aliasK, definedK, dependingK, syntax_tycoK, syntax_constK) = - ("code_generate", "code_serialize", "extracting", "defined_by", "depending_on", "code_alias", "code_syntax_tyco", "code_syntax_const"); +val (classK, generateK, serializeK, syntax_tycoK, syntax_constK, aliasK) = + ("code_class", "code_generate", "code_serialize", "code_syntax_tyco", "code_syntax_const", "code_alias"); +val (extractingK, definedK, dependingK) = + ("extracting", "defined_by", "depending_on"); + +val classP = + OuterSyntax.command classK "codegen data for classes" K.thy_decl ( + P.xname + -- ((P.$$$ "\\" || P.$$$ "=>") |-- (P.list1 P.name)) + -- (Scan.optional ((P.$$$ "\\" || P.$$$ "=>") |-- (P.list1 P.name)) []) + >> (fn ((name, tycos), consts) => (Toplevel.theory (ClassPackage.add_classentry name consts tycos))) + ) val generateP = OuterSyntax.command generateK "generate executable code for constants" K.thy_decl ( @@ -1258,13 +1386,13 @@ val syntax_tycoP = OuterSyntax.command syntax_tycoK "define code syntax for type constructor" K.thy_decl ( - P.string + P.name -- Scan.repeat1 ( P.xname -- (P.$$$ "(" |-- P.string --| P.$$$ ")") -- Scan.option ( P.$$$ definedK |-- Scan.option (P.$$$ "(" |-- P.string --| P.$$$ ")") - -- (P.string -- Scan.optional (P.$$$ dependingK |-- P.list1 P.string) []) + -- (P.text -- Scan.optional (P.$$$ dependingK |-- P.list1 P.string) []) ) ) >> (fn (serial_name, xs) => @@ -1275,13 +1403,13 @@ val syntax_constP = OuterSyntax.command syntax_constK "define code syntax for constant" K.thy_decl ( - P.string + P.name -- Scan.repeat1 ( (P.xname -- Scan.option (P.$$$ "::" |-- P.typ)) -- (P.$$$ "(" |-- P.string --| P.$$$ ")") -- Scan.option ( P.$$$ definedK |-- Scan.option (P.$$$ "(" |-- P.string --| P.$$$ ")") - -- (P.string -- Scan.optional (P.$$$ dependingK |-- P.list1 P.string) []) + -- (P.text -- Scan.optional (P.$$$ dependingK |-- P.list1 P.string) []) ) ) >> (fn (serial_name, xs) => @@ -1290,8 +1418,8 @@ add_syntax_const serial_name ((f, raw_mfx), raw_def)) xs) ); -val _ = OuterSyntax.add_parsers [generateP, serializeP, aliasP, syntax_tycoP, syntax_constP]; -val _ = OuterSyntax.add_keywords [extractingK, definedK, dependingK]; +val _ = OuterSyntax.add_parsers [classP, generateP, serializeP, aliasP, syntax_tycoP, syntax_constP]; +val _ = OuterSyntax.add_keywords ["\\", "=>", extractingK, definedK, dependingK]; (* setup *) @@ -1309,8 +1437,9 @@ add_codegen_sort ("default", exprgen_sort_default), add_codegen_type ("default", exprgen_type_default), add_codegen_expr ("default", exprgen_term_default), + add_appgen ("default", appgen_default), (* add_codegen_expr ("eq", codegen_eq), *) - add_codegen_expr ("neg", codegen_neg), + add_appgen ("neg", appgen_neg), add_defgen ("clsdecl", defgen_clsdecl), add_defgen ("tyco_fallback", defgen_tyco_fallback), add_defgen ("const_fallback", defgen_const_fallback), diff -r a41ce9c10b73 -r 99baddf6b0d0 src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Fri Dec 02 16:05:12 2005 +0100 +++ b/src/Pure/Tools/codegen_serializer.ML Fri Dec 02 16:05:31 2005 +0100 @@ -13,7 +13,6 @@ val add_prim: string * (string * string list) -> primitives -> primitives; val merge_prims: primitives * primitives -> primitives; val has_prim: primitives -> string -> bool; - val mk_prims: primitives -> string; type 'a pretty_syntax = string -> (int * (Pretty.T list -> ('a -> Pretty.T) -> Pretty.T)) option; @@ -127,12 +126,16 @@ | postify (ps as _::_) f = [Pretty.list "(" ")" ps, Pretty.brk 1, f]; fun upper_first s = - let val (c :: cs) = String.explode s - in String.implode (Char.toUpper c :: cs) end; + let + val (pr, b) = split_last (NameSpace.unpack s); + val (c::cs) = String.explode b; + in NameSpace.pack (pr @ [String.implode (Char.toUpper c :: cs)]) end; fun lower_first s = - let val (c :: cs) = String.explode s - in String.implode (Char.toLower c :: cs) end; + let + val (pr, b) = split_last (NameSpace.unpack s); + val (c::cs) = String.explode b; + in NameSpace.pack (pr @ [String.implode (Char.toLower c :: cs)]) end; (** grouping functions **) @@ -289,10 +292,18 @@ |> brackify (eval_br br (INFX (5, R))) end | ml_from_pat br (ICons ((f, ps), ty)) = - ps - |> map (ml_from_pat BR) - |> cons ((Pretty.str o resolv) f) - |> brackify (eval_br br BR) + (case const_syntax f + of NONE => + ps + |> map (ml_from_pat BR) + |> cons ((Pretty.str o resolv) f) + |> brackify (eval_br br BR) + | SOME (i, pr) => + if i = length ps + then + pr (map (ml_from_pat BR) ps) (ml_from_expr BR) + else + error "number of argument mismatch in customary serialization") | ml_from_pat br (IVarP (v, IType ("Integer", []))) = brackify (eval_br br BR) [ Pretty.str v, @@ -300,8 +311,8 @@ Pretty.str "IntInf.int" ] | ml_from_pat br (IVarP (v, _)) = - Pretty.str v; - fun ml_from_expr br (e as (IApp (IConst ("Cons", _), _))) = + Pretty.str v + and ml_from_expr br (e as (IApp (IConst ("Cons", _), _))) = let fun dest_cons (IApp (IConst ("Cons", _), IApp (IApp (IConst ("Pair", _), e1), e2))) = SOME (e1, e2) @@ -396,7 +407,9 @@ brackify (eval_br br (INFX (4, L))) [ ml_from_expr (INFX (4, L)) e1, Pretty.str "=", - ml_from_expr (INFX (4, X)) e2 + ml_from_expr (INFX (4, X)) e2, + Pretty.str ":", + ml_from_type NOBR (itype_of_iexpr e2) ] | ml_from_app br ("Pair", [e1, e2]) = Pretty.list "(" ")" [ @@ -452,14 +465,15 @@ mk_app_p br (Pretty.str "~") es | ml_from_app br ("wfrec", es) = mk_app_p br (Pretty.str "wfrec") es - | ml_from_app br (f, []) = - Pretty.str (resolv f) | ml_from_app br (f, es) = case const_syntax f of NONE => - let - val (es', e) = split_last es; - in mk_app_p br (ml_from_app NOBR (f, es')) [e] end + (case es + of [] => Pretty.str (resolv f) + | es => + let + val (es', e) = split_last es; + in mk_app_p br (ml_from_app NOBR (f, es')) [e] end) | SOME (i, pr) => let val (es1, es2) = splitAt (i, es); @@ -552,7 +566,7 @@ error ("can't serialize class declaration " ^ quote name ^ " to ML") | ml_from_def (name, Classinst _) = error ("can't serialize instance declaration " ^ quote name ^ " to ML") - in (writeln "******************"; (*map (writeln o Pretty.o)*) + in (debug 10 (fn _ => "******************") (); (*map (writeln o Pretty.o)*) case (snd o hd) ds of Fun _ => ml_from_funs ds | Datatypecons _ => ml_from_datatypes ds @@ -630,6 +644,7 @@ |> eliminate_classes |> debug 3 (fn _ => "generating...") |> serialize (ml_from_defs tyco_syntax const_syntax) ml_from_module ml_validator nspgrp name_root + |> (fn p => Pretty.chunks [(Pretty.str o mk_prims) prims, p]) end; fun ml_from_thingol' nspgrp name_root = @@ -660,9 +675,13 @@ NameSpace.pack (map upper_first prfix @ [base]) end; fun resolv_const f = - if is_cons f - then (upper_first o resolv) f - else (lower_first o resolv) f + if NameSpace.is_qualified f + then + if is_cons f + then (upper_first o resolv) f + else (lower_first o resolv) f + else + f; fun haskell_from_sctxt vs = let fun from_sctxt [] = Pretty.str "" @@ -755,13 +774,21 @@ |> brackify (eval_br br (INFX (5, R))) end | haskell_from_pat br (ICons ((f, ps), _)) = - ps - |> map (haskell_from_pat BR) - |> cons ((Pretty.str o upper_first o resolv) f) - |> brackify (eval_br br BR) + (case const_syntax f + of NONE => + ps + |> map (haskell_from_pat BR) + |> cons ((Pretty.str o resolv_const) f) + |> brackify (eval_br br BR) + | SOME (i, pr) => + if i = length ps + then + pr (map (haskell_from_pat BR) ps) (haskell_from_expr BR) + else + error "number of argument mismatch in customary serialization") | haskell_from_pat br (IVarP (v, _)) = - (Pretty.str o lower_first) v; - fun haskell_from_expr br (e as (IApp (IApp (IConst ("Cons", _), _), _))) = + (Pretty.str o lower_first) v + and haskell_from_expr br (e as (IApp (IApp (IConst ("Cons", _), _), _))) = let fun dest_cons (IApp (IApp (IConst ("Cons", _), e1), e2)) = SOME (e1, e2) | dest_cons p = NONE @@ -846,23 +873,17 @@ Pretty.str "==", haskell_from_expr (INFX (4, X)) e2 ] + | haskell_from_app br ("eq", [e1, e2]) = + brackify (eval_br br (INFX (4, L))) [ + haskell_from_expr (INFX (4, L)) e1, + Pretty.str "==", + haskell_from_expr (INFX (4, X)) e2 + ] | haskell_from_app br ("Pair", [e1, e2]) = Pretty.list "(" ")" [ haskell_from_expr NOBR e1, haskell_from_expr NOBR e2 ] - | haskell_from_app br ("and", [e1, e2]) = - brackify (eval_br br (INFX (3, R))) [ - haskell_from_expr (INFX (3, X)) e1, - Pretty.str "&&", - haskell_from_expr (INFX (3, R)) e2 - ] - | haskell_from_app br ("or", [e1, e2]) = - brackify (eval_br br (INFX (2, L))) [ - haskell_from_expr (INFX (2, L)) e1, - Pretty.str "||", - haskell_from_expr (INFX (2, X)) e2 - ] | haskell_from_app br ("if", [b, e1, e2]) = brackify (eval_br br BR) [ Pretty.str "if", @@ -872,46 +893,49 @@ Pretty.str "else", haskell_from_expr NOBR e2 ] - | haskell_from_app br ("add", [e1, e2]) = - brackify (eval_br br (INFX (6, L))) [ - haskell_from_expr (INFX (6, L)) e1, - Pretty.str "+", - haskell_from_expr (INFX (6, X)) e2 - ] - | haskell_from_app br ("mult", [e1, e2]) = - brackify (eval_br br (INFX (7, L))) [ - haskell_from_expr (INFX (7, L)) e1, - Pretty.str "*", - haskell_from_expr (INFX (7, X)) e2 - ] - | haskell_from_app br ("lt", [e1, e2]) = - brackify (eval_br br (INFX (4, L))) [ - haskell_from_expr (INFX (4, L)) e1, - Pretty.str "<", - haskell_from_expr (INFX (4, X)) e2 - ] - | haskell_from_app br ("le", [e1, e2]) = - brackify (eval_br br (INFX (7, L))) [ - haskell_from_expr (INFX (4, L)) e1, - Pretty.str "<=", - haskell_from_expr (INFX (4, X)) e2 - ] + | haskell_from_app br ("and", es) = + haskell_from_binop br 3 R "&&" es + | haskell_from_app br ("or", es) = + haskell_from_binop br 2 R "||" es + | haskell_from_app br ("add", es) = + haskell_from_binop br 6 L "+" es + | haskell_from_app br ("mult", es) = + haskell_from_binop br 7 L "*" es + | haskell_from_app br ("lt", es) = + haskell_from_binop br 4 L "<" es + | haskell_from_app br ("le", es) = + haskell_from_binop br 4 L "<=" es | haskell_from_app br ("minus", es) = mk_app_p br (Pretty.str "negate") es | haskell_from_app br ("wfrec", es) = mk_app_p br (Pretty.str "wfrec") es - | haskell_from_app br (f, []) = - Pretty.str (resolv_const f) | haskell_from_app br (f, es) = case const_syntax f of NONE => - let - val (es', e) = split_last es; - in mk_app_p br (haskell_from_app NOBR (f, es')) [e] end + (case es + of [] => Pretty.str (resolv_const f) + | es => + let + val (es', e) = split_last es; + in mk_app_p br (haskell_from_app NOBR (f, es')) [e] end) | SOME (i, pr) => let val (es1, es2) = splitAt (i, es); - in mk_app_p br (pr (map (haskell_from_expr BR) es1) (haskell_from_expr BR)) es2 end; + in mk_app_p br (pr (map (haskell_from_expr BR) es1) (haskell_from_expr BR)) es2 end + and haskell_from_binop br pr L f [e1, e2] = + brackify (eval_br br (INFX (pr, L))) [ + haskell_from_expr (INFX (pr, L)) e1, + Pretty.str f, + haskell_from_expr (INFX (pr, X)) e2 + ] + | haskell_from_binop br pr R f [e1, e2] = + brackify (eval_br br (INFX (pr, R))) [ + haskell_from_expr (INFX (pr, X)) e1, + Pretty.str f, + haskell_from_expr (INFX (pr, R)) e2 + ] + | haskell_from_binop br pr ass f args = + mk_app_p br (Pretty.str ("(" ^ f ^ ")")) args fun haskell_from_datatypes defs = let fun mk_cons (co, typs) = @@ -1050,6 +1074,7 @@ |> eta_expand eta_expander |> debug 3 (fn _ => "generating...") |> serialize (haskell_from_defs tyco_syntax const_syntax is_cons) haskell_from_module haskell_validator nspgrp name_root + |> (fn p => Pretty.chunks [(Pretty.str o mk_prims) prims, p]) end; end; (* local *) diff -r a41ce9c10b73 -r 99baddf6b0d0 src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Fri Dec 02 16:05:12 2005 +0100 +++ b/src/Pure/Tools/codegen_thingol.ML Fri Dec 02 16:05:31 2005 +0100 @@ -1,4 +1,4 @@ -(* Title: Pure/Tools/codegen_thingol.ML + (* Title: Pure/Tools/codegen_thingol.ML ID: $Id$ Author: Florian Haftmann, TU Muenchen @@ -48,7 +48,7 @@ Nop | Fun of (ipat list * iexpr) list * (ClassPackage.sortcontext * itype) | Typesyn of (vname * string list) list * itype - | Datatype of (vname * string list) list * string list * class list + | Datatype of (vname * string list) list * string list * string list | Datatypecons of string * itype list | Class of class list * vname * string list * string list | Classmember of class * vname * itype @@ -78,6 +78,7 @@ val type_list: string; val type_integer: string; val cons_pair: string; + val fun_eq: string; val fun_fst: string; val fun_snd: string; val Type_integer: itype; @@ -103,7 +104,9 @@ val Fun_wfrec: iexpr; val prims: string list; + val get_eqpred: module -> string -> string option; val is_eqtype: module -> itype -> bool; + val build_eqpred: module -> string -> def; val extract_defs: iexpr -> string list; val eta_expand: (string -> int) -> module -> module; val eta_expand_poly: module -> module; @@ -484,13 +487,13 @@ Pretty.str " |=> ", pretty_itype ty ] - | pretty_def (Datatype (vs, cs, clss)) = + | pretty_def (Datatype (vs, cs, insts)) = Pretty.block [ Pretty.list "(" ")" (map (pretty_itype o IVarT) vs), Pretty.str " |=> ", Pretty.gen_list " |" "" "" (map Pretty.str cs), - Pretty.str ", instance of ", - Pretty.gen_list "," "[" "]" (map Pretty.str clss) + Pretty.str ", instances ", + Pretty.gen_list "," "[" "]" (map Pretty.str insts) ] | pretty_def (Datatypecons (dtname, tys)) = Pretty.block [ @@ -655,25 +658,25 @@ in Graph.join (K join_module) modl12 end; fun partof names modl = - let - datatype pathnode = PN of (string list * (string * pathnode) list); - fun mk_ipath ([], base) (PN (defs, modls)) = - PN (base :: defs, modls) - | mk_ipath (n::ns, base) (PN (defs, modls)) = - modls - |> AList.default (op =) (n, PN ([], [])) - |> AList.map_entry (op =) n (mk_ipath (ns, base)) - |> (pair defs #> PN); - fun select (PN (defs, modls)) (Module module) = - module - |> Graph.subgraph (Graph.all_succs module (defs @ map fst modls)) - |> fold (fn (name, modls) => Graph.map_node name (select modls)) modls - |> Module; - in - Module modl - |> select (fold (mk_ipath o dest_name) (filter NameSpace.is_qualified names) (PN ([], []))) - |> dest_modl - end; + let + datatype pathnode = PN of (string list * (string * pathnode) list); + fun mk_ipath ([], base) (PN (defs, modls)) = + PN (base :: defs, modls) + | mk_ipath (n::ns, base) (PN (defs, modls)) = + modls + |> AList.default (op =) (n, PN ([], [])) + |> AList.map_entry (op =) n (mk_ipath (ns, base)) + |> (pair defs #> PN); + fun select (PN (defs, modls)) (Module module) = + module + |> Graph.subgraph (Graph.all_succs module (defs @ map fst modls)) + |> fold (fn (name, modls) => Graph.map_node name (select modls)) modls + |> Module; + in + Module modl + |> select (fold (mk_ipath o dest_name) (filter NameSpace.is_qualified names) (PN ([], []))) + |> dest_modl + end; fun add_check_transform (name, (Datatypecons (dtname, _))) = (debug 7 (fn _ => "transformation for datatype constructor " ^ quote name @@ -682,7 +685,7 @@ fn [Datatype (_, _, [])] => NONE | _ => "attempted to add constructor to already instantiating datatype" |> SOME)], [(dtname, - fn Datatype (vs, cs, clss) => Datatype (vs, name::cs, clss) + fn Datatype (vs, cs, insts) => Datatype (vs, name::cs, insts) | def => "attempted to add datatype constructor to non-datatype: " ^ (Pretty.output o pretty_def) def |> error)]) ) @@ -734,7 +737,7 @@ | def => "attempted to add class instance to non-class" ^ (Pretty.output o pretty_def) def |> error), (tyco, - fn Datatype (vs, cs, clss) => Datatype (vs, cs, clsname::clss) + fn Datatype (vs, cs, insts) => Datatype (vs, cs, name::insts) | Nop => Nop | def => "attempted to instantiate non-type to class instance" ^ (Pretty.output o pretty_def) def |> error)]) @@ -945,32 +948,68 @@ cons_true, cons_false, cons_pair, cons_nil, cons_cons, fun_primeq, fun_eq, fun_not, fun_and, fun_or, fun_if, fun_fst, fun_snd, fun_add, fun_mult, fun_minus, fun_lt, fun_le, fun_wfrec]; -fun is_superclass_of modl class_sub class_sup = - if class_sub = class_sup - then true - else - if NameSpace.is_qualified class_sub - then - case get_def modl class_sub - of Class (supclsnames, _, _, _) - => exists (fn class => is_superclass_of modl class class_sup) supclsnames - else - false; + +(** equality handling **) + +fun get_eqpred modl tyco = + if NameSpace.is_qualified tyco + then + case get_def modl tyco + of Datatype (_, _, insts) => + get_first (fn inst => + case get_def modl inst + of Classinst (cls, _, memdefs) => + if cls = class_eq + then (SOME o snd o hd) memdefs + else NONE) insts + else SOME fun_primeq; fun is_eqtype modl (IType (tyco, tys)) = forall (is_eqtype modl) tys - andalso - if NameSpace.is_qualified tyco - then + andalso ( + NameSpace.is_qualified tyco + orelse case get_def modl tyco of Typesyn (vs, ty) => is_eqtype modl ty - | Datatype (_, _, classes) => exists (is_superclass_of modl class_eq) classes - else - true + | Datatype (_, _, insts) => + exists (fn inst => case get_def modl inst of Classinst (cls, _, _) => cls = class_eq) insts + ) | is_eqtype modl (IFun _) = false | is_eqtype modl (IVarT (_, sort)) = - exists (is_superclass_of modl class_eq) sort + member (op =) sort class_eq; + +fun build_eqpred modl dtname = + let + val cons = + map ((fn Datatypecons c => c) o get_def modl) + (case get_def modl dtname of Datatype (_, cs, _) => cs); + val sortctxt = + map (rpair [class_eq]) + (case get_def modl dtname of Datatype (_, vs, _) => vs); + val ty = IType (dtname, map IVarT sortctxt); + fun mk_eq (c, []) = + ([ICons ((c, []), ty), ICons ((c, []), ty)], Cons_true) + | mk_eq (c, tys) = + let + val vars1 = Term.invent_names [] "a" (length tys); + val vars2 = Term.invent_names vars1 "b" (length tys); + fun mk_eq_cons ty' (v1, v2) = + IConst (fun_eq, ty' `-> ty' `-> Type_bool) `$ IVarE (v1, ty) `$ IVarE (v2, ty) + fun mk_conj (e1, e2) = + Fun_and `$ e1 `$ e2; + in + ([ICons ((c, map2 (curry IVarP) vars1 tys), ty), + ICons ((c, map2 (curry IVarP) vars2 tys), ty)], + foldr1 mk_conj (map2 mk_eq_cons tys (vars1 ~~ vars2))) + end; + val eqs = map mk_eq cons @ [([IVarP ("_", ty), IVarP ("_", ty)], Cons_false)]; + in + Fun (eqs, (sortctxt, ty `-> ty `-> Type_bool)) + end; + + +(** generic transformation **) fun extract_defs e = let @@ -988,10 +1027,6 @@ fold_iexpr extr_itype extr_ipat extr_iexpr e in extr_iexpr e [] end; - - -(** generic transformation **) - fun eta_expand query = let fun eta_app ((f, ty), es) =