diff -r a125f38a559a -r 24bf0e403526 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Thu Jan 25 09:32:50 2007 +0100 +++ b/src/Pure/Tools/codegen_package.ML Thu Jan 25 09:32:51 2007 +0100 @@ -112,9 +112,9 @@ fun ensure_def thy = CodegenThingol.ensure_def (CodegenNames.labelled_name thy); -fun ensure_def_class thy (algbr as ((proj_sort, _), _)) funcgr strct class trns = +fun ensure_def_class thy (algbr as ((_, algebra), _)) funcgr strct class trns = let - val superclasses = (proj_sort o Sign.super_classes thy) class; + val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class; val (v, cs) = AxClass.params_of_class thy class; val class' = CodegenNames.class thy class; val classrels' = map (curry (CodegenNames.classrel thy) class) superclasses; @@ -135,7 +135,7 @@ and ensure_def_classrel thy algbr funcgr strct (subclass, superclass) trns = trns |> ensure_def_class thy algbr funcgr strct subclass - |-> (fn _ => pair (CodegenNames.classrel thy (subclass, superclass))) + |>> (fn _ => CodegenNames.classrel thy (subclass, superclass)) and ensure_def_tyco thy algbr funcgr strct tyco trns = let fun defgen_datatype trns = @@ -164,18 +164,18 @@ and exprgen_tyvar_sort thy (algbr as ((proj_sort, _), _)) funcgr strct (v, sort) trns = trns |> fold_map (ensure_def_class thy algbr funcgr strct) (proj_sort sort) - |-> (fn sort => pair (unprefix "'" v, sort)) + |>> (fn sort => (unprefix "'" v, sort)) and exprgen_type thy algbr funcgr strct (TVar _) trns = error "TVar encountered in typ during code generation" | exprgen_type thy algbr funcgr strct (TFree vs) trns = trns |> exprgen_tyvar_sort thy algbr funcgr strct vs - |-> (fn (v, sort) => pair (ITyVar v)) + |>> (fn (v, sort) => ITyVar v) | exprgen_type thy algbr funcgr strct (Type ("fun", [t1, t2])) trns = trns |> exprgen_type thy algbr funcgr strct t1 ||>> exprgen_type thy algbr funcgr strct t2 - |-> (fn (t1', t2') => pair (t1' `-> t2')) + |>> (fn (t1', t2') => t1' `-> t2') | exprgen_type thy algbr funcgr strct (Type (tyco, tys)) trns = case get_abstype thy (tyco, tys) of SOME ty => @@ -185,7 +185,7 @@ trns |> ensure_def_tyco thy algbr funcgr strct tyco ||>> fold_map (exprgen_type thy algbr funcgr strct) tys - |-> (fn (tyco, tys) => pair (tyco `%% tys)); + |>> (fn (tyco, tys) => tyco `%% tys); exception CONSTRAIN of (string * typ) * typ; val timing = ref false; @@ -213,11 +213,11 @@ trns |> ensure_def_inst thy algbr funcgr strct inst ||>> (fold_map o fold_map) mk_dict yss - |-> (fn (inst, dss) => pair (DictConst (inst, dss))) + |>> (fn (inst, dss) => DictConst (inst, dss)) | mk_dict (Local (classrels, (v, (k, sort)))) trns = trns |> fold_map (ensure_def_classrel thy algbr funcgr strct) classrels - |-> (fn classrels => pair (DictVar (classrels, (unprefix "'" v, (k, length sort))))) + |>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort)))) in trns |> fold_map mk_dict typargs @@ -235,40 +235,37 @@ trns |> fold_map (exprgen_dicts thy algbr funcgr strct) insts end -and ensure_def_inst thy (algbr as ((proj_sort, _), _)) funcgr strct (class, tyco) trns = +and ensure_def_inst thy (algbr as ((_, algebra), _)) funcgr strct (class, tyco) trns = let - val (vs, classop_defs) = ((apsnd o map) Const o CodegenConsts.instance_dict thy) - (class, tyco); - val classops = (map (CodegenConsts.norm_of_typ thy) o snd - o AxClass.params_of_class thy) class; - val arity_typ = Type (tyco, (map TFree vs)); - val superclasses = (proj_sort o Sign.super_classes thy) class + val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class; + val (var, classops) = try (AxClass.params_of_class thy) class |> the_default ("'a", []) + val vs = Name.names (Name.declare var Name.context) "'a" (Sorts.mg_domain algebra tyco [class]); + val arity_typ = Type (tyco, map TFree vs); fun gen_superarity superclass trns = trns |> ensure_def_class thy algbr funcgr strct superclass ||>> ensure_def_classrel thy algbr funcgr strct (class, superclass) ||>> exprgen_dicts thy algbr funcgr strct (arity_typ, [superclass]) - |-> (fn ((superclass, classrel), [DictConst (inst, dss)]) => - pair (superclass, (classrel, (inst, dss)))); - fun gen_classop_def (classop, t) trns = + |>> (fn ((superclass, classrel), [DictConst (inst, dss)]) => + (superclass, (classrel, (inst, dss)))); + fun gen_classop_def (classop as (c, ty)) trns = trns - |> ensure_def_const thy algbr funcgr strct classop - ||>> exprgen_term thy algbr funcgr strct t; + |> ensure_def_const thy algbr funcgr strct (CodegenConsts.norm_of_typ thy classop) + ||>> exprgen_term thy algbr funcgr strct (Const (c, map_type_tfree (K arity_typ) ty)); fun defgen_inst trns = trns |> ensure_def_class thy algbr funcgr strct class ||>> ensure_def_tyco thy algbr funcgr strct tyco ||>> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs ||>> fold_map gen_superarity superclasses - ||>> fold_map gen_classop_def (classops ~~ classop_defs) + ||>> fold_map gen_classop_def classops |-> (fn ((((class, tyco), arity), superarities), classops) => succeed (CodegenThingol.Classinst ((class, (tyco, arity)), (superarities, classops)))); val inst = CodegenNames.instance thy (class, tyco); in trns |> tracing (fn _ => "generating instance " ^ quote class ^ " / " ^ quote tyco) - |> ensure_def thy defgen_inst true - ("generating instance " ^ quote class ^ " / " ^ quote tyco) inst + |> ensure_def thy defgen_inst true ("generating instance " ^ quote class ^ " / " ^ quote tyco) inst |> pair inst end and ensure_def_const thy (algbr as (_, consts)) funcgr strct (c_tys as (c, tys)) trns = @@ -334,7 +331,7 @@ | exprgen_term thy algbr funcgr strct (Free (v, ty)) trns = trns |> exprgen_type thy algbr funcgr strct ty - |-> (fn _ => pair (IVar v)) + |>> (fn _ => IVar v) | exprgen_term thy algbr funcgr strct (Abs (raw_v, ty, raw_t)) trns = let val (v, t) = Syntax.variant_abs (raw_v, ty, raw_t); @@ -342,27 +339,25 @@ trns |> exprgen_type thy algbr funcgr strct ty ||>> exprgen_term thy algbr funcgr strct t - |-> (fn (ty, t) => pair ((v, ty) `|-> t)) + |>> (fn (ty, t) => (v, ty) `|-> t) end | exprgen_term thy algbr funcgr strct (t as _ $ _) trns = case strip_comb t of (Const (c, ty), ts) => trns |> select_appgen thy algbr funcgr strct ((c, ty), ts) - |-> (fn t => pair t) | (t', ts) => trns |> exprgen_term thy algbr funcgr strct t' ||>> fold_map (exprgen_term thy algbr funcgr strct) ts - |-> (fn (t, ts) => pair (t `$$ ts)) + |>> (fn (t, ts) => t `$$ ts) 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 ||>> exprgen_dict_parms thy algbr funcgr strct (c, ty) ||>> fold_map (exprgen_term thy algbr funcgr strct) ts - |-> (fn (((c, ty), iss), ts) => - pair (IConst (c, (iss, ty)) `$$ ts)) + |>> (fn (((c, ty), iss), ts) => IConst (c, (iss, ty)) `$$ ts) and select_appgen thy algbr funcgr strct ((c, ty), ts) trns = case Symtab.lookup (fst (CodegenPackageData.get thy)) c of SOME (i, (appgen, _)) => @@ -377,13 +372,13 @@ trns |> fold_map (exprgen_type thy algbr funcgr strct) tys ||>> appgen thy algbr funcgr strct ((c, ty), ts @ map Free vs) - |-> (fn (tys, t) => pair (map2 (fn (v, _) => pair v) vs tys `|--> t)) + |>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t) end else if length ts > i then trns |> appgen thy algbr funcgr strct ((c, ty), Library.take (i, ts)) ||>> fold_map (exprgen_term thy algbr funcgr strct) (Library.drop (i, ts)) - |-> (fn (t, ts) => pair (t `$$ ts)) + |>> (fn (t, ts) => t `$$ ts) else trns |> appgen thy algbr funcgr strct ((c, ty), ts) @@ -401,6 +396,12 @@ ^ Sign.string_of_typ thy ty ^ "\noccurs with type\n" ^ Sign.string_of_typ thy ty_decl); + +fun perhaps_def_const thy algbr funcgr strct c trns = + case try (ensure_def_const thy algbr funcgr strct c) trns + of SOME (c, trns) => (SOME c, trns) + | NONE => (NONE, trns); + fun exprgen_term' thy algbr funcgr strct t trns = exprgen_term thy algbr funcgr strct t trns handle CONSTRAIN ((c, ty), ty_decl) => error ("In term " ^ (quote o Sign.string_of_term thy) t @@ -427,7 +428,7 @@ of SOME i => trns |> exprgen_type thy algbr funcgr strct ty - |-> (fn _ => pair (IChar (chr i))) + |>> (fn _ => IChar (chr i)) | NONE => trns |> appgen_default thy algbr funcgr strct app; @@ -446,7 +447,7 @@ |> exprgen_term thy algbr funcgr strct st ||>> exprgen_type thy algbr funcgr strct sty ||>> fold_map clausegen ds - |-> (fn ((se, sty), ds) => pair (ICase ((se, sty), ds))) + |>> (fn ((se, sty), ds) => ICase ((se, sty), ds)) end; fun appgen_let thy algbr funcgr strct (app as (_, [st, ct])) trns = @@ -554,20 +555,7 @@ (* generic generation combinators *) -fun operational_algebra thy = - let - fun add_iff_operational class classes = - if (not o null o these o Option.map #params o try (AxClass.get_definition thy)) class - orelse (length o gen_inter (op =)) - ((Sign.certify_sort thy o Sign.super_classes thy) class, classes) >= 2 - then class :: classes - else classes; - val operational_classes = fold add_iff_operational (Sign.all_classes thy) []; - in - Sorts.subalgebra (Sign.pp thy) (member (op =) operational_classes) (Sign.classes_of thy) - end; - -fun generate thy funcgr targets init gen it = +fun generate thy funcgr targets gen it = let val cs = map_filter (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy)) (CodegenFuncgr.all funcgr); @@ -577,9 +565,9 @@ |> fold (fn c => Consts.declare qnaming ((CodegenNames.const thy c, CodegenFuncgr.typ funcgr' c), true)) (CodegenFuncgr.all funcgr'); - val algbr = (operational_algebra thy, consttab); + val algbr = (CodegenData.operational_algebra thy, consttab); in - Code.change_yield thy (CodegenThingol.start_transact init (gen thy algbr funcgr' + Code.change_yield thy (CodegenThingol.start_transact (gen thy algbr funcgr' (true, targets) it)) |> fst end; @@ -589,7 +577,7 @@ val ct = Thm.cterm_of thy t; val (ct', funcgr) = CodegenFuncgr.make_term thy (K K) ct; val t' = Thm.term_of ct'; - in generate thy funcgr (SOME []) NONE exprgen_term' t' end; + in generate thy funcgr (SOME []) exprgen_term' t' end; fun eval_term thy (ref_spec, t) = let @@ -617,18 +605,17 @@ | SOME thyname => filter (is_const thyname) consts end; -fun filter_generatable thy consts = +fun filter_generatable thy targets consts = let - fun generatable const = - case try (CodegenFuncgr.make thy) [const] - of SOME funcgr => can - (generate thy funcgr NONE NONE (fold_map oooo ensure_def_const')) [const] - | NONE => false; - in filter generatable consts end; + val (consts', funcgr) = CodegenFuncgr.make_consts thy consts; + val consts'' = generate thy funcgr targets (fold_map oooo perhaps_def_const) consts'; + val consts''' = map_filter (fn (const, SOME _) => SOME const | (_, NONE) => NONE) + (consts' ~~ consts''); + in consts''' end; -fun read_constspec thy "*" = filter_generatable thy (consts_of thy NONE) - | read_constspec thy s = if String.isSuffix ".*" s - then filter_generatable thy (consts_of thy (SOME (unsuffix ".*" s))) +fun read_constspec thy targets "*" = filter_generatable thy targets (consts_of thy NONE) + | read_constspec thy targets s = if String.isSuffix ".*" s + then filter_generatable thy targets (consts_of thy (SOME (unsuffix ".*" s))) else [CodegenConsts.read_const thy s]; @@ -641,16 +628,16 @@ fun code raw_cs seris thy = let - val cs = maps (read_constspec thy) raw_cs; - (*FIXME: assert serializer*) val seris' = map (fn (target, args as _ :: _) => (target, SOME (CodegenSerializer.get_serializer thy target args)) | (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; fun generate' thy = case cs of [] => [] | _ => - generate thy (CodegenFuncgr.make thy cs) (case map fst seris' of [] => NONE | xs => SOME xs) - NONE (fold_map oooo ensure_def_const') cs; + generate thy (CodegenFuncgr.make thy cs) targets + (fold_map oooo ensure_def_const') cs; fun serialize' [] code seri = seri NONE code | serialize' cs code seri =