--- a/src/Tools/code/code_package.ML Fri Aug 24 14:14:18 2007 +0200
+++ b/src/Tools/code/code_package.ML Fri Aug 24 14:14:20 2007 +0200
@@ -45,35 +45,25 @@
-> CodeFuncgr.T
-> (string * typ) * term list -> CodeThingol.transact -> iterm * CodeThingol.transact;
-type appgens = (int * (appgen * stamp)) Symtab.table;
-val merge_appgens : appgens * appgens -> appgens =
- Symtab.merge (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) =>
- bounds1 = bounds2 andalso stamp1 = stamp2);
-
-structure Consttab = CodeUnit.Consttab;
-type abstypes = typ Symtab.table * CodeUnit.const Consttab.table;
-fun merge_abstypes ((typs1, consts1) : abstypes, (typs2, consts2) : abstypes) =
- (Symtab.merge (Type.eq_type Vartab.empty) (typs1, typs2),
- Consttab.merge CodeUnit.eq_const (consts1, consts2));
-
-structure Translation = TheoryDataFun
+structure Appgens = TheoryDataFun
(
- type T = appgens * abstypes;
- val empty = (Symtab.empty, (Symtab.empty, Consttab.empty));
+ type T = (int * (appgen * stamp)) Symtab.table;
+ val empty = Symtab.empty;
val copy = I;
val extend = I;
- fun merge _ ((appgens1, abstypes1), (appgens2, abstypes2)) =
- (merge_appgens (appgens1, appgens2), merge_abstypes (abstypes1, abstypes2));
+ fun merge _ = Symtab.merge (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) =>
+ bounds1 = bounds2 andalso stamp1 = stamp2);
);
fun code_depgr thy [] = CodeFuncgr.make thy []
| code_depgr thy consts =
let
val gr = CodeFuncgr.make thy consts;
- val select = CodeFuncgr.Constgraph.all_succs gr consts;
+ val select = Graph.all_succs gr consts;
in
- CodeFuncgr.Constgraph.subgraph
- (member CodeUnit.eq_const select) gr
+ gr
+ |> Graph.subgraph (member (op =) select)
+ |> Graph.map_nodes ((apsnd o map) (Conv.fconv_rule (Class.overload thy)))
end;
fun code_thms thy =
@@ -89,7 +79,7 @@
in { name = name, ID = name, dir = "", unfold = true,
path = "", parents = nameparents }
end;
- val prgr = CodeFuncgr.Constgraph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr [];
+ val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr [];
in Present.display_graph prgr end;
structure Program = CodeDataFun
@@ -105,7 +95,7 @@
map_filter (CodeName.const_rev thy) (Graph.keys code);
val dels = (Graph.all_preds code
o map (CodeName.const thy)
- o filter (member CodeUnit.eq_const cs_exisiting)
+ o filter (member (op =) cs_exisiting)
) cs;
in Graph.del_nodes dels code end;
);
@@ -113,10 +103,6 @@
(* translation kernel *)
-fun get_abstype thy (tyco, tys) = case Symtab.lookup ((fst o snd o Translation.get) thy) tyco
- of SOME ty => SOME ((map_atyps (fn TFree (n, _) => nth tys (the (Int.fromString n)))) ty)
- | NONE => NONE;
-
val value_name = "Isabelle_Eval.EVAL.EVAL";
fun ensure_def thy = CodeThingol.ensure_def
@@ -128,7 +114,7 @@
val (v, cs) = AxClass.params_of_class thy class;
val class' = CodeName.class thy class;
val classrels' = map (curry (CodeName.classrel thy) class) superclasses;
- val classops' = map (CodeName.const thy o CodeUnit.const_of_cexpr thy) cs;
+ val classops' = map (CodeName.const thy o fst) cs;
val defgen_class =
fold_map (ensure_def_class thy algbr funcgr) superclasses
##>> (fold_map (exprgen_typ thy algbr funcgr) o map snd) cs
@@ -152,9 +138,7 @@
fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
##>> fold_map (fn (c, tys) =>
fold_map (exprgen_typ thy algbr funcgr) tys
- #>> (fn tys' =>
- ((CodeName.const thy o CodeUnit.const_of_cexpr thy)
- (c, tys ---> Type (tyco, map TFree vs)), tys'))) cos
+ #>> (fn tys' => (CodeName.const thy c, tys'))) cos
#>> (fn (vs, cos) => CodeThingol.Datatype (vs, cos))
end;
val tyco' = CodeName.tyco thy tyco;
@@ -171,15 +155,10 @@
|> exprgen_tyvar_sort thy algbr funcgr vs
|>> (fn (v, sort) => ITyVar v)
| exprgen_typ thy algbr funcgr (Type (tyco, tys)) trns =
- case get_abstype thy (tyco, tys)
- of SOME ty =>
- trns
- |> exprgen_typ thy algbr funcgr ty
- | NONE =>
- trns
- |> ensure_def_tyco thy algbr funcgr tyco
- ||>> fold_map (exprgen_typ thy algbr funcgr) tys
- |>> (fn (tyco, tys) => tyco `%% tys);
+ trns
+ |> ensure_def_tyco thy algbr funcgr tyco
+ ||>> fold_map (exprgen_typ thy algbr funcgr) tys
+ |>> (fn (tyco, tys) => tyco `%% tys);
exception CONSTRAIN of (string * typ) * typ;
val timing = ref false;
@@ -216,10 +195,8 @@
end
and exprgen_dict_parms thy (algbr as (_, consts)) funcgr (c, ty_ctxt) =
let
- val c' = CodeUnit.const_of_cexpr thy (c, ty_ctxt)
- val idf = CodeName.const thy c';
- val ty_decl = Consts.the_declaration consts idf;
- val (tys, tys_decl) = pairself (curry (Consts.typargs consts) idf) (ty_ctxt, ty_decl);
+ val ty_decl = Consts.the_declaration consts c;
+ val (tys, tys_decl) = pairself (curry (Consts.typargs consts) c) (ty_ctxt, ty_decl);
val sorts = map (snd o dest_TVar) tys_decl;
in
fold_map (exprgen_dicts thy algbr funcgr) (tys ~~ sorts)
@@ -237,10 +214,11 @@
||>> exprgen_dicts thy algbr funcgr (arity_typ, [superclass])
|>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
(superclass, (classrel, (inst, dss))));
- fun gen_classop_def (classop as (c, ty)) trns =
+ fun gen_classop_def (c, ty) trns =
trns
- |> ensure_def_const thy algbr funcgr (CodeUnit.const_of_cexpr thy classop)
- ||>> exprgen_term thy algbr funcgr (Const (c, map_type_tfree (K arity_typ) ty));
+ |> ensure_def_const thy algbr funcgr c
+ ||>> exprgen_term thy algbr funcgr
+ (Const (Class.inst_const thy (c, tyco), map_type_tfree (K arity_typ) ty));
fun defgen_inst trns =
trns
|> ensure_def_class thy algbr funcgr class
@@ -256,13 +234,13 @@
|> ensure_def thy defgen_inst ("generating instance " ^ quote class ^ " / " ^ quote tyco) inst
|> pair inst
end
-and ensure_def_const thy (algbr as (_, consts)) funcgr (const as (c, opt_tyco)) =
+and ensure_def_const thy (algbr as (_, consts)) funcgr c =
let
- val c' = CodeName.const thy const;
+ val c' = CodeName.const thy c;
fun defgen_datatypecons trns =
trns
|> ensure_def_tyco thy algbr funcgr
- ((the o Code.get_datatype_of_constr thy) const)
+ ((the o Code.get_datatype_of_constr thy) c)
|>> (fn _ => CodeThingol.Bot);
fun defgen_classop trns =
trns
@@ -271,15 +249,14 @@
|>> (fn _ => CodeThingol.Bot);
fun defgen_fun trns =
let
- val const' = perhaps (Consttab.lookup ((snd o snd o Translation.get) thy)) const;
- val raw_thms = CodeFuncgr.funcs funcgr const';
- val ty = (Logic.unvarifyT o CodeFuncgr.typ funcgr) const';
+ val raw_thms = CodeFuncgr.funcs funcgr c;
+ val ty = (Logic.unvarifyT o CodeFuncgr.typ funcgr) c;
val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
then raw_thms
else map (CodeUnit.expand_eta 1) raw_thms;
- val timeap = if !timing then Output.timeap_msg ("time for " ^ c')
+ val timeap = if !timing then Output.timeap_msg ("time for " ^ c)
else I;
- val vs = (map dest_TFree o Consts.typargs consts) (c', ty);
+ val vs = (map dest_TFree o Consts.typargs consts) (c, ty);
val dest_eqthm =
apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify o prop_of;
fun exprgen_eq (args, rhs) =
@@ -292,14 +269,13 @@
||>> timeap (fold_map (exprgen_eq o dest_eqthm) thms)
|>> (fn ((vs, ty), eqs) => CodeThingol.Fun ((vs, ty), eqs))
end;
- val defgen = if (is_some o Code.get_datatype_of_constr thy) const
+ val defgen = if (is_some o Code.get_datatype_of_constr thy) c
then defgen_datatypecons
- else if is_some opt_tyco
- orelse (not o is_some o AxClass.class_of_param thy) c
- then defgen_fun
- else defgen_classop
+ else if (is_some o AxClass.class_of_param thy) c
+ then defgen_classop
+ else defgen_fun
in
- ensure_def thy defgen ("generating constant " ^ CodeUnit.string_of_const thy const) c'
+ ensure_def thy defgen ("generating constant " ^ CodeUnit.string_of_const thy c) c'
#> pair c'
end
and exprgen_term thy algbr funcgr (Const (c, ty)) trns =
@@ -330,14 +306,14 @@
|>> (fn (t, ts) => t `$$ ts)
and appgen_default thy algbr funcgr ((c, ty), ts) trns =
trns
- |> ensure_def_const thy algbr funcgr (CodeUnit.const_of_cexpr thy (c, ty))
+ |> ensure_def_const thy algbr funcgr c
||>> fold_map (exprgen_typ thy algbr funcgr) ((fst o Term.strip_type) ty)
||>> exprgen_typ thy algbr funcgr ((snd o Term.strip_type) ty)
||>> exprgen_dict_parms thy algbr funcgr (c, ty)
||>> fold_map (exprgen_term thy algbr funcgr) ts
|>> (fn ((((c, tys), ty), iss), ts) => IConst (c, (iss, tys)) `$$ ts)
and select_appgen thy algbr funcgr ((c, ty), ts) trns =
- case Symtab.lookup (fst (Translation.get thy)) c
+ case Symtab.lookup (Appgens.get thy) c
of SOME (i, (appgen, _)) =>
if length ts < i then
let
@@ -396,7 +372,9 @@
let
val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts));
fun clause_gen (dt, bt) =
- exprgen_term thy algbr funcgr dt
+ exprgen_term thy algbr funcgr
+ (map_aterms (fn Const (c_ty as (c, ty)) => Const
+ (Class.unoverload_const thy c_ty, ty) | t => t) dt)
##>> exprgen_term thy algbr funcgr bt;
in
exprgen_term thy algbr funcgr st
@@ -429,107 +407,25 @@
val i = (length o fst o strip_type o Sign.the_const_type thy) c;
val _ = Program.change thy (K CodeThingol.empty_code);
in
- (Translation.map o apfst)
- (Symtab.update (c, (i, (appgen, stamp ())))) thy
+ Appgens.map (Symtab.update (c, (i, (appgen, stamp ())))) thy
end;
-
-(** abstype and constsubst interface **)
-
-local
-
-fun add_consts thy f (c1, c2 as (c, opt_tyco)) =
- let
- val _ = if
- is_some (AxClass.class_of_param thy c) andalso is_none opt_tyco
- orelse is_some (Code.get_datatype_of_constr thy c2)
- then error ("Not a function: " ^ CodeUnit.string_of_const thy c2)
- else ();
- val funcgr = CodeFuncgr.make thy [c1, c2];
- val ty1 = (f o CodeFuncgr.typ funcgr) c1;
- val ty2 = CodeFuncgr.typ funcgr c2;
- val _ = if Sign.typ_equiv thy (ty1, ty2) then () else
- error ("Incompatiable type signatures of " ^ CodeUnit.string_of_const thy c1
- ^ " and " ^ CodeUnit.string_of_const thy c2 ^ ":\n"
- ^ CodeUnit.string_of_typ thy ty1 ^ "\n" ^ CodeUnit.string_of_typ thy ty2);
- in Consttab.update (c1, c2) end;
-
-fun gen_abstyp prep_const prep_typ (raw_abstyp, raw_substtyp) raw_absconsts thy =
- let
- val abstyp = Type.no_tvars (prep_typ thy raw_abstyp);
- val substtyp = Type.no_tvars (prep_typ thy raw_substtyp);
- val absconsts = (map o pairself) (prep_const thy) raw_absconsts;
- val Type (abstyco, tys) = abstyp handle BIND => error ("Bad type: " ^ Sign.string_of_typ thy abstyp);
- val typarms = map (fst o dest_TFree) tys handle MATCH => error ("Bad type: " ^ Sign.string_of_typ thy abstyp);
- fun mk_index v =
- let
- val k = find_index (fn w => v = w) typarms;
- in if k = ~1
- then error ("Free type variable: " ^ quote v)
- else TFree (string_of_int k, [])
- end;
- val typpat = map_atyps (fn TFree (v, _) => mk_index v) substtyp;
- fun apply_typpat (Type (tyco, tys)) =
- let
- val tys' = map apply_typpat tys;
- in if tyco = abstyco then
- (map_atyps (fn TFree (n, _) => nth tys' (the (Int.fromString n)))) typpat
- else
- Type (tyco, tys')
- end
- | apply_typpat ty = ty;
- val _ = Program.change thy (K CodeThingol.empty_code);
- in
- thy
- |> (Translation.map o apsnd) (fn (abstypes, abscs) =>
- (abstypes
- |> Symtab.update (abstyco, typpat),
- abscs
- |> fold (add_consts thy apply_typpat) absconsts)
- )
- end;
-
-fun gen_constsubst prep_const raw_constsubsts thy =
- let
- val constsubsts = (map o pairself) (prep_const thy) raw_constsubsts;
- val _ = Program.change thy (K CodeThingol.empty_code);
- in
- thy
- |> (Translation.map o apsnd o apsnd) (fold (add_consts thy I) constsubsts)
- end;
-
-in
-
-val abstyp = gen_abstyp (K I) Sign.certify_typ;
-val abstyp_e = gen_abstyp CodeUnit.read_const Sign.read_typ;
-
-val constsubst = gen_constsubst (K I);
-val constsubst_e = gen_constsubst CodeUnit.read_const;
-
-end; (*local*)
-
-
(** code generation interfaces **)
(* generic generation combinators *)
fun generate thy funcgr gen it =
let
- (*FIXME*)
- val _ = CodeFuncgr.intervene thy funcgr;
- val cs = map_filter (Consttab.lookup ((snd o snd o Translation.get) thy))
- (CodeFuncgr.all funcgr);
- val CodeFuncgr' = CodeFuncgr.make thy cs;
val naming = NameSpace.qualified_names NameSpace.default_naming;
val consttab = Consts.empty
|> fold (fn c => Consts.declare naming
- ((CodeName.const thy c, CodeFuncgr.typ CodeFuncgr' c), true))
- (CodeFuncgr.all CodeFuncgr');
+ ((c, CodeFuncgr.typ funcgr c), true))
+ (CodeFuncgr.all funcgr);
val algbr = (Code.operational_algebra thy, consttab);
in
Program.change_yield thy
- (CodeThingol.start_transact (gen thy algbr CodeFuncgr' it))
+ (CodeThingol.start_transact (gen thy algbr funcgr it))
|> fst
end;
@@ -630,8 +526,7 @@
val _ = OuterSyntax.add_keywords [inK, module_nameK, fileK];
-val (codeK, code_abstypeK, code_axiomsK, code_thmsK, code_depsK) =
- ("export_code", "code_abstype", "code_axioms", "code_thms", "code_deps");
+val (codeK, code_thmsK, code_depsK) = ("export_code", "code_thms", "code_deps");
in
@@ -644,19 +539,6 @@
of SOME f => (writeln "Now generating code..."; f thy)
| NONE => error ("Bad directive " ^ quote cmd);
-val code_abstypeP =
- OuterSyntax.command code_abstypeK "axiomatic abstypes for code generation" K.thy_decl (
- (P.typ -- P.typ -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
- (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.term)) [])
- >> (Toplevel.theory o uncurry abstyp_e)
- );
-
-val code_axiomsP =
- OuterSyntax.command code_axiomsK "axiomatic constant equalities for code generation" K.thy_decl (
- Scan.repeat1 (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.term)
- >> (Toplevel.theory o constsubst_e)
- );
-
val code_thmsP =
OuterSyntax.improper_command code_thmsK "print system of defining equations for code" OuterKeyword.diag
(Scan.repeat P.term
@@ -669,7 +551,7 @@
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
-val _ = OuterSyntax.add_parsers [codeP, code_abstypeP, code_axiomsP, code_thmsP, code_depsP];
+val _ = OuterSyntax.add_parsers [codeP, code_thmsP, code_depsP];
end; (* local *)