--- a/src/Tools/code/code_package.ML Mon Oct 08 22:03:30 2007 +0200
+++ b/src/Tools/code/code_package.ML Mon Oct 08 22:03:31 2007 +0200
@@ -2,7 +2,7 @@
ID: $Id$
Author: Florian Haftmann, TU Muenchen
-Code generator translation kernel. Code generator Isar setup.
+Code generator interfaces and Isar setup.
*)
signature CODE_PACKAGE =
@@ -17,16 +17,12 @@
-> term -> 'a;
val satisfies_ref: (unit -> bool) option ref;
val satisfies: theory -> term -> string list -> bool;
- val eval_invoke: theory -> (string * (unit -> 'a) option ref) -> CodeThingol.code
- -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
val codegen_command: theory -> string -> unit;
end;
structure CodePackage : CODE_PACKAGE =
struct
-open BasicCodeThingol;
-
(** code theorems **)
fun code_depgr thy [] = CodeFuncgr.make thy []
@@ -57,7 +53,9 @@
in Present.display_graph prgr end;
-(** code translation **)
+(** code generation interfaces **)
+
+(* code data *)
structure Program = CodeDataFun
(
@@ -77,300 +75,15 @@
in Graph.del_nodes dels code end;
);
-
-(* translation kernel *)
-
-val value_name = "Isabelle_Eval.EVAL.EVAL";
-
-fun ensure_def thy = CodeThingol.ensure_def
- (fn s => if s = value_name then "<term>" else CodeName.labelled_name thy s);
-
-exception CONSTRAIN of (string * typ) * typ;
+(* generic generation combinators *)
-fun ensure_def_class thy (algbr as ((_, algebra), _)) funcgr class =
- let
- val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
- val (v, cs) = AxClass.params_of_class thy class;
- val class' = CodeName.class thy class;
- val defgen_class =
- fold_map (fn superclass => ensure_def_class thy algbr funcgr superclass
- ##>> ensure_def_classrel thy algbr funcgr (class, superclass)) superclasses
- ##>> fold_map (fn (c, ty) => ensure_def_const thy algbr funcgr c
- ##>> exprgen_typ thy algbr funcgr ty) cs
- #>> (fn info => CodeThingol.Class (unprefix "'" v, info))
- in
- ensure_def thy defgen_class class'
- #> pair class'
- end
-and ensure_def_classrel thy algbr funcgr (subclass, superclass) =
- let
- val classrel' = CodeName.classrel thy (subclass, superclass);
- val defgen_classrel =
- ensure_def_class thy algbr funcgr subclass
- ##>> ensure_def_class thy algbr funcgr superclass
- #>> CodeThingol.Classrel;
- in
- ensure_def thy defgen_classrel classrel'
- #> pair classrel'
- end
-and ensure_def_tyco thy algbr funcgr "fun" =
- pair "fun"
- | ensure_def_tyco thy algbr funcgr tyco =
- let
- val defgen_datatype =
- let
- val (vs, cos) = Code.get_datatype thy tyco;
- in
- fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
- ##>> fold_map (fn (c, tys) =>
- ensure_def_const thy algbr funcgr c
- ##>> fold_map (exprgen_typ thy algbr funcgr) tys) cos
- #>> CodeThingol.Datatype
- end;
- val tyco' = CodeName.tyco thy tyco;
- in
- ensure_def thy defgen_datatype tyco'
- #> pair tyco'
- end
-and exprgen_tyvar_sort thy (algbr as ((proj_sort, _), _)) funcgr (v, sort) =
- fold_map (ensure_def_class thy algbr funcgr) (proj_sort sort)
- #>> (fn sort => (unprefix "'" v, sort))
-and exprgen_typ thy algbr funcgr (TFree vs) =
- exprgen_tyvar_sort thy algbr funcgr vs
- #>> (fn (v, sort) => ITyVar v)
- | exprgen_typ thy algbr funcgr (Type (tyco, tys)) =
- ensure_def_tyco thy algbr funcgr tyco
- ##>> fold_map (exprgen_typ thy algbr funcgr) tys
- #>> (fn (tyco, tys) => tyco `%% tys)
-and exprgen_dicts thy (algbr as ((proj_sort, algebra), consts)) funcgr (ty_ctxt, sort_decl) =
- let
- val pp = Sign.pp thy;
- datatype typarg =
- Global of (class * string) * typarg list list
- | Local of (class * class) list * (string * (int * sort));
- fun class_relation (Global ((_, tyco), yss), _) class =
- Global ((class, tyco), yss)
- | class_relation (Local (classrels, v), subclass) superclass =
- Local ((subclass, superclass) :: classrels, v);
- fun type_constructor tyco yss class =
- Global ((class, tyco), (map o map) fst yss);
- fun type_variable (TFree (v, sort)) =
- let
- val sort' = proj_sort sort;
- in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
- val typargs = Sorts.of_sort_derivation pp algebra
- {class_relation = class_relation, type_constructor = type_constructor,
- type_variable = type_variable}
- (ty_ctxt, proj_sort sort_decl);
- fun mk_dict (Global (inst, yss)) =
- ensure_def_inst thy algbr funcgr inst
- ##>> (fold_map o fold_map) mk_dict yss
- #>> (fn (inst, dss) => DictConst (inst, dss))
- | mk_dict (Local (classrels, (v, (k, sort)))) =
- fold_map (ensure_def_classrel thy algbr funcgr) classrels
- #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
- in
- fold_map mk_dict typargs
- end
-and exprgen_dict_parms thy (algbr as (_, consts)) funcgr (c, ty_ctxt) =
- let
- 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)
- end
-and exprgen_eq thy algbr funcgr thm =
- let
- val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
- o Logic.unvarify o prop_of) thm;
- in
- fold_map (exprgen_term thy algbr funcgr) args
- ##>> exprgen_term thy algbr funcgr rhs
- #>> rpair thm
- end
-and ensure_def_inst thy (algbr as ((_, algebra), _)) funcgr (class, tyco) =
- let
- val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
- val (var, classparams) = try (AxClass.params_of_class thy) class |> the_default ("'a", [])
- val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
- val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
- val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
- Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
- val arity_typ = Type (tyco, map TFree vs);
- val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
- fun exprgen_superarity superclass =
- ensure_def_class thy algbr funcgr superclass
- ##>> ensure_def_classrel thy algbr funcgr (class, superclass)
- ##>> exprgen_dicts thy algbr funcgr (arity_typ, [superclass])
- #>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
- (superclass, (classrel, (inst, dss))));
- fun exprgen_classparam_inst (c, ty) =
- let
- val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
- val thm = Class.unoverload thy (Thm.cterm_of thy c_inst);
- val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd
- o Logic.dest_equals o Thm.prop_of) thm;
- in
- ensure_def_const thy algbr funcgr c
- ##>> exprgen_const thy algbr funcgr c_ty
- #>> (fn (c, IConst c_inst) => ((c, c_inst), thm))
- end;
- val defgen_inst =
- ensure_def_class thy algbr funcgr class
- ##>> ensure_def_tyco thy algbr funcgr tyco
- ##>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
- ##>> fold_map exprgen_superarity superclasses
- ##>> fold_map exprgen_classparam_inst classparams
- #>> (fn ((((class, tyco), arity), superarities), classparams) =>
- CodeThingol.Classinst ((class, (tyco, arity)), (superarities, classparams)));
- val inst = CodeName.instance thy (class, tyco);
- in
- ensure_def thy defgen_inst inst
- #> pair inst
- end
-and ensure_def_const thy (algbr as (_, consts)) funcgr c =
- let
- val c' = CodeName.const thy c;
- fun defgen_datatypecons tyco =
- ensure_def_tyco thy algbr funcgr tyco
- #>> K (CodeThingol.Datatypecons c');
- fun defgen_classparam class =
- ensure_def_class thy algbr funcgr class
- #>> K (CodeThingol.Classparam c');
- fun defgen_fun trns =
- let
- val raw_thms = CodeFuncgr.funcs funcgr c;
- val ty = (Logic.unvarifyT o CodeFuncgr.typ funcgr) c;
- val vs = (map dest_TFree o Consts.typargs consts) (c, ty);
- 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;
- in
- trns
- |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
- ||>> exprgen_typ thy algbr funcgr ty
- ||>> fold_map (exprgen_eq thy algbr funcgr) thms
- |>> (fn ((vs, ty), eqs) => CodeThingol.Fun ((vs, ty), eqs))
- end;
- val defgen = case Code.get_datatype_of_constr thy c
- of SOME tyco => defgen_datatypecons tyco
- | NONE => (case AxClass.class_of_param thy c
- of SOME class => defgen_classparam class
- | NONE => defgen_fun)
- in
- ensure_def thy defgen c'
- #> pair c'
- end
-and exprgen_term thy algbr funcgr (Const (c, ty)) =
- exprgen_app thy algbr funcgr ((c, ty), [])
- | exprgen_term thy algbr funcgr (Free (v, _)) =
- pair (IVar v)
- | exprgen_term thy algbr funcgr (Abs (abs as (_, ty, _))) =
- let
- val (v, t) = Syntax.variant_abs abs;
- in
- exprgen_typ thy algbr funcgr ty
- ##>> exprgen_term thy algbr funcgr t
- #>> (fn (ty, t) => (v, ty) `|-> t)
- end
- | exprgen_term thy algbr funcgr (t as _ $ _) =
- case strip_comb t
- of (Const (c, ty), ts) =>
- exprgen_app thy algbr funcgr ((c, ty), ts)
- | (t', ts) =>
- exprgen_term thy algbr funcgr t'
- ##>> fold_map (exprgen_term thy algbr funcgr) ts
- #>> (fn (t, ts) => t `$$ ts)
-and exprgen_const thy algbr funcgr (c, ty) =
- ensure_def_const thy algbr funcgr c
- ##>> exprgen_dict_parms thy algbr funcgr (c, ty)
- ##>> fold_map (exprgen_typ thy algbr funcgr) ((fst o Term.strip_type) ty)
- (*##>> exprgen_typ thy algbr funcgr ((snd o Term.strip_type) ty)*)
- #>> (fn ((c, iss), tys) => IConst (c, (iss, tys)))
-and exprgen_app_default thy algbr funcgr (c_ty, ts) =
- exprgen_const thy algbr funcgr c_ty
- ##>> fold_map (exprgen_term thy algbr funcgr) ts
- #>> (fn (t, ts) => t `$$ ts)
-and exprgen_case thy algbr funcgr n cases (app as ((c, ty), ts)) =
- let
- (*FIXME rework this code*)
- val (all_tys, _) = strip_type ty;
- val (tys, _) = chop (1 + (if null cases then 1 else length cases)) all_tys;
- val st = nth ts n;
- val sty = nth tys n;
- fun is_undefined (Const (c, _)) = Code.is_undefined thy c
- | is_undefined _ = false;
- fun mk_case (co, n) t =
- let
- val (vs, body) = Term.strip_abs_eta n t;
- val selector = list_comb (Const (co, map snd vs ---> sty), map Free vs);
- in if is_undefined body then NONE else SOME (selector, body) end;
- val ds = case cases
- of [] => let val ([v_ty], body) = Term.strip_abs_eta 1 (the_single (nth_drop n ts))
- in [(Free v_ty, body)] end
- | cases => map_filter (uncurry mk_case) (AList.make (CodeUnit.no_args thy) cases
- ~~ nth_drop n ts);
- in
- exprgen_term thy algbr funcgr st
- ##>> exprgen_typ thy algbr funcgr sty
- ##>> fold_map (fn (pat, body) => exprgen_term thy algbr funcgr pat
- ##>> exprgen_term thy algbr funcgr body) ds
- ##>> exprgen_app_default thy algbr funcgr app
- #>> (fn (((st, sty), ds), t0) => ICase (((st, sty), ds), t0))
- end
-and exprgen_app thy algbr funcgr ((c, ty), ts) = case Code.get_case_data thy c
- of SOME (n, cases) => let val i = 1 + (if null cases then 1 else length cases) in
- if length ts < i then
- let
- val k = length ts;
- val tys = (curry Library.take (i - k) o curry Library.drop k o fst o strip_type) ty;
- val ctxt = (fold o fold_aterms)
- (fn Free (v, _) => Name.declare v | _ => I) ts Name.context;
- val vs = Name.names ctxt "a" tys;
- in
- fold_map (exprgen_typ thy algbr funcgr) tys
- ##>> exprgen_case thy algbr funcgr n cases ((c, ty), ts @ map Free vs)
- #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
- end
- else if length ts > i then
- exprgen_case thy algbr funcgr n cases ((c, ty), Library.take (i, ts))
- ##>> fold_map (exprgen_term thy algbr funcgr) (Library.drop (i, ts))
- #>> (fn (t, ts) => t `$$ ts)
- else
- exprgen_case thy algbr funcgr n cases ((c, ty), ts)
- end
- | NONE => exprgen_app_default thy algbr funcgr ((c, ty), ts);
+val ensure_const = CodeThingol.ensure_const;
-
-(* entrance points into translation kernel *)
-
-fun ensure_def_const' thy algbr funcgr c trns =
- ensure_def_const thy algbr funcgr c trns
- handle CONSTRAIN ((c, ty), ty_decl) => error (
- "Constant " ^ c ^ " with most general type\n"
- ^ CodeUnit.string_of_typ thy ty
- ^ "\noccurs with type\n"
- ^ CodeUnit.string_of_typ thy ty_decl);
-
-fun perhaps_def_const thy algbr funcgr c trns =
- case try (ensure_def_const thy algbr funcgr c) trns
+fun perhaps_const thy algbr funcgr c trns =
+ case try (CodeThingol.ensure_const thy algbr funcgr c) trns
of SOME (c, trns) => (SOME c, trns)
| NONE => (NONE, trns);
-fun exprgen_term' thy algbr funcgr t trns =
- exprgen_term thy algbr funcgr t trns
- handle CONSTRAIN ((c, ty), ty_decl) => error ("In term " ^ (quote o Sign.string_of_term thy) t
- ^ ",\nconstant " ^ c ^ " with most general type\n"
- ^ CodeUnit.string_of_typ thy ty
- ^ "\noccurs with type\n"
- ^ CodeUnit.string_of_typ thy ty_decl);
-
-
-(** code generation interfaces **)
-
-(* generic generation combinators *)
-
fun generate thy funcgr gen it =
let
val naming = NameSpace.qualified_names NameSpace.default_naming;
@@ -380,66 +93,51 @@
val algbr = (Code.operational_algebra thy, consttab);
in
Program.change_yield thy
- (CodeThingol.start_transact (gen thy algbr funcgr it))
- |> fst
+ (CodeThingol.transact (gen thy algbr funcgr it))
end;
fun code thy permissive cs seris =
let
val code = Program.get thy;
val seris' = map (fn (((target, module), file), args) =>
- CodeTarget.get_serializer thy target permissive module file args
- CodeName.labelled_name cs) seris;
+ CodeTarget.get_serializer thy target permissive module file args cs) seris;
in (map (fn f => f code) seris' : unit list; ()) end;
fun raw_eval evaluate term_of thy g =
let
- val value_name = "Isabelle_Eval.EVAL.EVAL";
- fun ensure_eval thy algbr funcgr t =
+ fun result (_, code) =
let
- val ty = fastype_of t;
- val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
- o dest_TFree))) t [];
- val defgen_eval =
- fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
- ##>> exprgen_typ thy algbr funcgr ty
- ##>> exprgen_term' thy algbr funcgr t
- #>> (fn ((vs, ty), t) => CodeThingol.Fun ((vs, ty), [(([], t), Drule.dummy_thm)]));
- fun result (dep, code) =
- let
- val CodeThingol.Fun ((vs, ty), [(([], t), _)]) = Graph.get_node code value_name;
- val deps = Graph.imm_succs code value_name;
- val code' = Graph.del_nodes [value_name] code;
- val code'' = CodeThingol.project_code false [] (SOME deps) code';
- in ((code'', ((vs, ty), t), deps), (dep, code')) end;
- in
- ensure_def thy defgen_eval value_name
- #> result
- end;
+ val CodeThingol.Fun ((vs, ty), [(([], t), _)]) =
+ Graph.get_node code CodeName.value_name;
+ val deps = Graph.imm_succs code CodeName.value_name;
+ val code' = Graph.del_nodes [CodeName.value_name] code;
+ val code'' = CodeThingol.project_code false [] (SOME deps) code';
+ in ((code'', ((vs, ty), t), deps), code') end;
fun h funcgr ct =
let
- val (code, vs_ty_t, deps) = generate thy funcgr ensure_eval (term_of ct);
+ val ((code, vs_ty_t, deps), _) = term_of ct
+ |> generate thy funcgr CodeThingol.ensure_value
+ |> result
+ ||> `(fn code' => Program.change thy (K code'));
in g code vs_ty_t deps ct end;
in evaluate thy h end;
fun eval_conv thy = raw_eval CodeFuncgr.eval_conv Thm.term_of thy;
fun eval_term thy = raw_eval CodeFuncgr.eval_term I thy;
-fun eval_invoke thy = CodeTarget.eval_invoke thy CodeName.labelled_name;
-
val satisfies_ref : (unit -> bool) option ref = ref NONE;
fun satisfies thy t witnesses =
let
fun evl code ((vs, ty), t) deps ct =
- eval_invoke thy ("CodePackage.satisfies_ref", satisfies_ref)
+ CodeTarget.eval_invoke thy ("CodePackage.satisfies_ref", satisfies_ref)
code (t, ty) witnesses;
in eval_term thy evl t end;
fun filter_generatable thy consts =
let
val (consts', funcgr) = CodeFuncgr.make_consts thy consts;
- val consts'' = generate thy funcgr (fold_map ooo perhaps_def_const) consts';
+ val (consts'', _) = generate thy funcgr (fold_map ooo perhaps_const) consts';
val consts''' = map_filter (fn (const, SOME _) => SOME const | (_, NONE) => NONE)
(consts' ~~ consts'');
in consts''' end;
@@ -449,9 +147,9 @@
val (perm1, cs) = CodeUnit.read_const_exprs thy
(filter_generatable thy) raw_cs;
val (perm2, cs') = case generate thy (CodeFuncgr.make thy cs)
- (fold_map ooo ensure_def_const') cs
- of [] => (true, NONE)
- | cs => (false, SOME cs);
+ (fold_map ooo ensure_const) cs
+ of ([], _) => (true, NONE)
+ | (cs, _) => (false, SOME cs);
in (perm1 orelse perm2, cs') end;
@@ -515,8 +213,7 @@
end;
-
-(** toplevel interface and setup **)
+(** interfaces and Isar setup **)
local
@@ -542,8 +239,8 @@
val (c_thms, thy') = add_codeprops (map (the o CodeName.const_rev thy) (these all_cs))
(map (the o CodeName.const_rev thy) (these cs)) thy;
val prop_cs = (filter_generatable thy' o map fst) c_thms;
- val _ = if null seris then [] else generate thy' (CodeFuncgr.make thy' prop_cs)
- (fold_map ooo ensure_def_const') prop_cs;
+ val _ = if null seris then () else (generate thy' (CodeFuncgr.make thy' prop_cs)
+ (fold_map ooo ensure_const) prop_cs; ());
val _ = if null seris then () else code thy' permissive
(SOME (map (CodeName.const thy') prop_cs)) seris;
in thy' end;
--- a/src/Tools/code/code_target.ML Mon Oct 08 22:03:30 2007 +0200
+++ b/src/Tools/code/code_target.ML Mon Oct 08 22:03:31 2007 +0200
@@ -34,14 +34,12 @@
type serializer;
val add_serializer: string * serializer -> theory -> theory;
val get_serializer: theory -> string -> bool -> string option -> string option -> Args.T list
- -> (theory -> string -> string) -> string list option
- -> CodeThingol.code -> unit;
+ -> string list option -> CodeThingol.code -> unit;
val assert_serializer: theory -> string -> string;
val eval_verbose: bool ref;
- val eval_invoke: theory -> (theory -> string -> string)
- -> (string * (unit -> 'a) option ref) -> CodeThingol.code
- -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
+ val eval_invoke: theory -> (string * (unit -> 'a) option ref)
+ -> CodeThingol.code -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
val code_width: int ref;
val setup: theory -> theory;
@@ -1632,7 +1630,7 @@
val target_diag = "diag";
fun get_serializer thy target permissive module file args
- labelled_name = fn cs =>
+ = fn cs =>
let
val (seris, exc) = CodeTargetData.get thy;
val data = case Symtab.lookup seris target
@@ -1648,28 +1646,26 @@
fun check_empty_funs code = case (filter_out (member (op =) exc)
(CodeThingol.empty_funs code))
of [] => code
- | names => error ("No defining equations for " ^ commas (map (labelled_name thy) names));
+ | names => error ("No defining equations for " ^ commas (map (CodeName.labelled_name thy) names));
in
project
#> check_empty_funs
- #> seri module file args (labelled_name thy) reserved (Symtab.lookup alias) (Symtab.lookup prolog)
- (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
+ #> seri module file args (CodeName.labelled_name thy) reserved (Symtab.lookup alias)
+ (Symtab.lookup prolog) (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
end;
-fun eval_invoke thy labelled_name (ref_name, reff) code (t, ty) args =
+fun eval_invoke thy (ref_name, reff) code (t, ty) args =
let
val _ = if CodeThingol.contains_dictvar t then
error "Term to be evaluated constains free dictionaries" else ();
- val val_name = "Isabelle_Eval.EVAL.EVAL";
- val val_name' = "Isabelle_Eval.EVAL";
- val val_name'_args = space_implode " " (val_name' :: map (enclose "(" ")") args);
- val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE []
- labelled_name;
+ val val_args = space_implode " "
+ (NameSpace.qualifier CodeName.value_name :: map (enclose "(" ")") args);
+ val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE [];
fun eval code = (
reff := NONE;
- seri (SOME [val_name]) code;
+ seri (SOME [CodeName.value_name]) code;
use_text "generated code for evaluation" Output.ml_output (!eval_verbose)
- ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ val_name'_args ^ "))");
+ ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ val_args ^ "))");
case !reff
of NONE => error ("Could not retrieve value of ML reference " ^ quote ref_name
^ " (reference probably has been shadowed)")
@@ -1677,7 +1673,7 @@
);
in
code
- |> CodeThingol.add_eval_def (val_name, (t, ty))
+ |> CodeThingol.add_value_stmt (t, ty)
|> eval
end;
--- a/src/Tools/code/code_thingol.ML Mon Oct 08 22:03:30 2007 +0200
+++ b/src/Tools/code/code_thingol.ML Mon Oct 08 22:03:31 2007 +0200
@@ -3,6 +3,7 @@
Author: Florian Haftmann, TU Muenchen
Intermediate language ("Thin-gol") representing executable code.
+Representation and translation.
*)
infix 8 `%%;
@@ -58,7 +59,7 @@
val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
- datatype def =
+ datatype stmt =
Bot
| Fun of typscheme * ((iterm list * iterm) * thm) list
| Datatype of (vname * sort) list * (string * itype list) list
@@ -69,8 +70,7 @@
| Classinst of (class * (string * (vname * sort) list))
* ((class * (string * (string * dict list list))) list
* ((string * const) * thm) list);
- type code = def Graph.T;
- type transact;
+ type code = stmt Graph.T;
val empty_code: code;
val merge_code: code * code -> code;
val project_code: bool (*delete empty funs*)
@@ -78,11 +78,14 @@
-> code -> code;
val empty_funs: code -> string list;
val is_cons: code -> string -> bool;
- val add_eval_def: string (*bind name*) * (iterm * itype) -> code -> code;
- val ensure_def: (string -> string) -> (transact -> def * transact) -> string
- -> transact -> transact;
- val start_transact: (transact -> 'a * transact) -> code -> 'a * code;
+ type transact;
+ val ensure_const: theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
+ -> CodeFuncgr.T -> string -> transact -> string * transact;
+ val ensure_value: theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
+ -> CodeFuncgr.T -> term -> transact -> string * transact;
+ val add_value_stmt: iterm * itype -> code -> code;
+ val transact: (transact -> 'a * transact) -> code -> 'a * code;
end;
structure CodeThingol: CODE_THINGOL =
@@ -245,7 +248,7 @@
(** definitions, transactions **)
type typscheme = (vname * sort) list * itype;
-datatype def =
+datatype stmt =
Bot
| Fun of typscheme * ((iterm list * iterm) * thm) list
| Datatype of (vname * sort) list * (string * itype list) list
@@ -257,7 +260,7 @@
* ((class * (string * (string * dict list list))) list
* ((string * const) * thm) list);
-type code = def Graph.T;
+type code = stmt Graph.T;
(* abstract code *)
@@ -315,12 +318,12 @@
type transact = Graph.key option * code;
-fun ensure_def labelled_name defgen name (dep, code) =
+fun ensure_stmt stmtgen name (dep, code) =
let
fun add_def false =
ensure_bot name
#> add_dep (dep, name)
- #> curry defgen (SOME name)
+ #> curry stmtgen (SOME name)
##> snd
#-> (fn def => add_def_incr (name, def))
| add_def true =
@@ -329,17 +332,284 @@
code
|> add_def (can (Graph.get_node code) name)
|> pair dep
+ |> pair name
end;
-fun start_transact f code =
+fun transact f code =
(NONE, code)
|> f
|-> (fn x => fn (_, code) => (x, code));
-fun add_eval_def (name, (t, ty)) code =
+
+(* translation kernel *)
+
+fun ensure_class thy (algbr as ((_, algebra), _)) funcgr class =
+ let
+ val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
+ val (v, cs) = AxClass.params_of_class thy class;
+ val class' = CodeName.class thy class;
+ val stmt_class =
+ fold_map (fn superclass => ensure_class thy algbr funcgr superclass
+ ##>> ensure_classrel thy algbr funcgr (class, superclass)) superclasses
+ ##>> fold_map (fn (c, ty) => ensure_const thy algbr funcgr c
+ ##>> exprgen_typ thy algbr funcgr ty) cs
+ #>> (fn info => Class (unprefix "'" v, info))
+ in
+ ensure_stmt stmt_class class'
+ end
+and ensure_classrel thy algbr funcgr (subclass, superclass) =
+ let
+ val classrel' = CodeName.classrel thy (subclass, superclass);
+ val stmt_classrel =
+ ensure_class thy algbr funcgr subclass
+ ##>> ensure_class thy algbr funcgr superclass
+ #>> Classrel;
+ in
+ ensure_stmt stmt_classrel classrel'
+ end
+and ensure_tyco thy algbr funcgr "fun" =
+ pair "fun"
+ | ensure_tyco thy algbr funcgr tyco =
+ let
+ val stmt_datatype =
+ let
+ val (vs, cos) = Code.get_datatype thy tyco;
+ in
+ fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
+ ##>> fold_map (fn (c, tys) =>
+ ensure_const thy algbr funcgr c
+ ##>> fold_map (exprgen_typ thy algbr funcgr) tys) cos
+ #>> Datatype
+ end;
+ val tyco' = CodeName.tyco thy tyco;
+ in
+ ensure_stmt stmt_datatype tyco'
+ end
+and exprgen_tyvar_sort thy (algbr as ((proj_sort, _), _)) funcgr (v, sort) =
+ fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
+ #>> (fn sort => (unprefix "'" v, sort))
+and exprgen_typ thy algbr funcgr (TFree vs) =
+ exprgen_tyvar_sort thy algbr funcgr vs
+ #>> (fn (v, sort) => ITyVar v)
+ | exprgen_typ thy algbr funcgr (Type (tyco, tys)) =
+ ensure_tyco thy algbr funcgr tyco
+ ##>> fold_map (exprgen_typ thy algbr funcgr) tys
+ #>> (fn (tyco, tys) => tyco `%% tys)
+and exprgen_dicts thy (algbr as ((proj_sort, algebra), consts)) funcgr (ty_ctxt, sort_decl) =
+ let
+ val pp = Sign.pp thy;
+ datatype typarg =
+ Global of (class * string) * typarg list list
+ | Local of (class * class) list * (string * (int * sort));
+ fun class_relation (Global ((_, tyco), yss), _) class =
+ Global ((class, tyco), yss)
+ | class_relation (Local (classrels, v), subclass) superclass =
+ Local ((subclass, superclass) :: classrels, v);
+ fun type_constructor tyco yss class =
+ Global ((class, tyco), (map o map) fst yss);
+ fun type_variable (TFree (v, sort)) =
+ let
+ val sort' = proj_sort sort;
+ in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
+ val typargs = Sorts.of_sort_derivation pp algebra
+ {class_relation = class_relation, type_constructor = type_constructor,
+ type_variable = type_variable}
+ (ty_ctxt, proj_sort sort_decl);
+ fun mk_dict (Global (inst, yss)) =
+ ensure_inst thy algbr funcgr inst
+ ##>> (fold_map o fold_map) mk_dict yss
+ #>> (fn (inst, dss) => DictConst (inst, dss))
+ | mk_dict (Local (classrels, (v, (k, sort)))) =
+ fold_map (ensure_classrel thy algbr funcgr) classrels
+ #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
+ in
+ fold_map mk_dict typargs
+ end
+and exprgen_dict_parms thy (algbr as (_, consts)) funcgr (c, ty_ctxt) =
+ let
+ 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)
+ end
+and exprgen_eq thy algbr funcgr thm =
+ let
+ val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
+ o Logic.unvarify o prop_of) thm;
+ in
+ fold_map (exprgen_term thy algbr funcgr) args
+ ##>> exprgen_term thy algbr funcgr rhs
+ #>> rpair thm
+ end
+and ensure_inst thy (algbr as ((_, algebra), _)) funcgr (class, tyco) =
+ let
+ val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
+ val (var, classparams) = try (AxClass.params_of_class thy) class |> the_default ("'a", [])
+ val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
+ val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
+ val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
+ Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
+ val arity_typ = Type (tyco, map TFree vs);
+ val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
+ fun exprgen_superarity superclass =
+ ensure_class thy algbr funcgr superclass
+ ##>> ensure_classrel thy algbr funcgr (class, superclass)
+ ##>> exprgen_dicts thy algbr funcgr (arity_typ, [superclass])
+ #>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
+ (superclass, (classrel, (inst, dss))));
+ fun exprgen_classparam_inst (c, ty) =
+ let
+ val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
+ val thm = Class.unoverload thy (Thm.cterm_of thy c_inst);
+ val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd
+ o Logic.dest_equals o Thm.prop_of) thm;
+ in
+ ensure_const thy algbr funcgr c
+ ##>> exprgen_const thy algbr funcgr c_ty
+ #>> (fn (c, IConst c_inst) => ((c, c_inst), thm))
+ end;
+ val stmt_inst =
+ ensure_class thy algbr funcgr class
+ ##>> ensure_tyco thy algbr funcgr tyco
+ ##>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
+ ##>> fold_map exprgen_superarity superclasses
+ ##>> fold_map exprgen_classparam_inst classparams
+ #>> (fn ((((class, tyco), arity), superarities), classparams) =>
+ Classinst ((class, (tyco, arity)), (superarities, classparams)));
+ val inst = CodeName.instance thy (class, tyco);
+ in
+ ensure_stmt stmt_inst inst
+ end
+and ensure_const thy (algbr as (_, consts)) funcgr c =
+ let
+ val c' = CodeName.const thy c;
+ fun stmt_datatypecons tyco =
+ ensure_tyco thy algbr funcgr tyco
+ #>> K (Datatypecons c');
+ fun stmt_classparam class =
+ ensure_class thy algbr funcgr class
+ #>> K (Classparam c');
+ fun stmt_fun trns =
+ let
+ val raw_thms = CodeFuncgr.funcs funcgr c;
+ val ty = (Logic.unvarifyT o CodeFuncgr.typ funcgr) c;
+ val vs = (map dest_TFree o Consts.typargs consts) (c, ty);
+ 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;
+ in
+ trns
+ |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
+ ||>> exprgen_typ thy algbr funcgr ty
+ ||>> fold_map (exprgen_eq thy algbr funcgr) thms
+ |>> (fn ((vs, ty), eqs) => Fun ((vs, ty), eqs))
+ end;
+ val stmtgen = case Code.get_datatype_of_constr thy c
+ of SOME tyco => stmt_datatypecons tyco
+ | NONE => (case AxClass.class_of_param thy c
+ of SOME class => stmt_classparam class
+ | NONE => stmt_fun)
+ in
+ ensure_stmt stmtgen c'
+ end
+and exprgen_term thy algbr funcgr (Const (c, ty)) =
+ exprgen_app thy algbr funcgr ((c, ty), [])
+ | exprgen_term thy algbr funcgr (Free (v, _)) =
+ pair (IVar v)
+ | exprgen_term thy algbr funcgr (Abs (abs as (_, ty, _))) =
+ let
+ val (v, t) = Syntax.variant_abs abs;
+ in
+ exprgen_typ thy algbr funcgr ty
+ ##>> exprgen_term thy algbr funcgr t
+ #>> (fn (ty, t) => (v, ty) `|-> t)
+ end
+ | exprgen_term thy algbr funcgr (t as _ $ _) =
+ case strip_comb t
+ of (Const (c, ty), ts) =>
+ exprgen_app thy algbr funcgr ((c, ty), ts)
+ | (t', ts) =>
+ exprgen_term thy algbr funcgr t'
+ ##>> fold_map (exprgen_term thy algbr funcgr) ts
+ #>> (fn (t, ts) => t `$$ ts)
+and exprgen_const thy algbr funcgr (c, ty) =
+ ensure_const thy algbr funcgr c
+ ##>> exprgen_dict_parms thy algbr funcgr (c, ty)
+ ##>> fold_map (exprgen_typ thy algbr funcgr) ((fst o Term.strip_type) ty)
+ #>> (fn ((c, iss), tys) => IConst (c, (iss, tys)))
+and exprgen_app_default thy algbr funcgr (c_ty, ts) =
+ exprgen_const thy algbr funcgr c_ty
+ ##>> fold_map (exprgen_term thy algbr funcgr) ts
+ #>> (fn (t, ts) => t `$$ ts)
+and exprgen_case thy algbr funcgr n cases (app as ((c, ty), ts)) =
+ let
+ val (tys, _) =
+ (chop (1 + (if null cases then 1 else length cases)) o fst o strip_type) ty;
+ val dt = nth ts n;
+ val dty = nth tys n;
+ fun is_undefined (Const (c, _)) = Code.is_undefined thy c
+ | is_undefined _ = false;
+ fun mk_case (co, n) t =
+ let
+ val (vs, body) = Term.strip_abs_eta n t;
+ val selector = list_comb (Const (co, map snd vs ---> dty), map Free vs);
+ in if is_undefined body then NONE else SOME (selector, body) end;
+ fun mk_ds [] =
+ let
+ val ([v_ty], body) = Term.strip_abs_eta 1 (the_single (nth_drop n ts))
+ in [(Free v_ty, body)] end
+ | mk_ds cases = map_filter (uncurry mk_case)
+ (AList.make (CodeUnit.no_args thy) cases ~~ nth_drop n ts);
+ in
+ exprgen_term thy algbr funcgr dt
+ ##>> exprgen_typ thy algbr funcgr dty
+ ##>> fold_map (fn (pat, body) => exprgen_term thy algbr funcgr pat
+ ##>> exprgen_term thy algbr funcgr body) (mk_ds cases)
+ ##>> exprgen_app_default thy algbr funcgr app
+ #>> (fn (((dt, dty), ds), t0) => ICase (((dt, dty), ds), t0))
+ end
+and exprgen_app thy algbr funcgr ((c, ty), ts) = case Code.get_case_data thy c
+ of SOME (n, cases) => let val i = 1 + (if null cases then 1 else length cases) in
+ if length ts < i then
+ let
+ val k = length ts;
+ val tys = (curry Library.take (i - k) o curry Library.drop k o fst o strip_type) ty;
+ val ctxt = (fold o fold_aterms)
+ (fn Free (v, _) => Name.declare v | _ => I) ts Name.context;
+ val vs = Name.names ctxt "a" tys;
+ in
+ fold_map (exprgen_typ thy algbr funcgr) tys
+ ##>> exprgen_case thy algbr funcgr n cases ((c, ty), ts @ map Free vs)
+ #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
+ end
+ else if length ts > i then
+ exprgen_case thy algbr funcgr n cases ((c, ty), Library.take (i, ts))
+ ##>> fold_map (exprgen_term thy algbr funcgr) (Library.drop (i, ts))
+ #>> (fn (t, ts) => t `$$ ts)
+ else
+ exprgen_case thy algbr funcgr n cases ((c, ty), ts)
+ end
+ | NONE => exprgen_app_default thy algbr funcgr ((c, ty), ts);
+
+fun ensure_value thy algbr funcgr t =
+ let
+ val ty = fastype_of t;
+ val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
+ o dest_TFree))) t [];
+ val stmt_value =
+ fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
+ ##>> exprgen_typ thy algbr funcgr ty
+ ##>> exprgen_term thy algbr funcgr t
+ #>> (fn ((vs, ty), t) => Fun ((vs, ty), [(([], t), Drule.dummy_thm)]));
+ in
+ ensure_stmt stmt_value CodeName.value_name
+ end;
+
+fun add_value_stmt (t, ty) code =
code
- |> Graph.new_node (name, Fun (([], ty), [(([], t), Drule.dummy_thm)]))
- |> fold (curry Graph.add_edge name) (Graph.keys code);
+ |> Graph.new_node (CodeName.value_name, Fun (([], ty), [(([], t), Drule.dummy_thm)]))
+ |> fold (curry Graph.add_edge CodeName.value_name) (Graph.keys code);
end; (*struct*)