haftmann@24219: (* Title: Tools/code/code_thingol.ML haftmann@24219: ID: $Id$ haftmann@24219: Author: Florian Haftmann, TU Muenchen haftmann@24219: haftmann@24219: Intermediate language ("Thin-gol") representing executable code. haftmann@24918: Representation and translation. haftmann@24219: *) haftmann@24219: haftmann@24219: infix 8 `%%; haftmann@24219: infixr 6 `->; haftmann@24219: infixr 6 `-->; haftmann@24219: infix 4 `$; haftmann@24219: infix 4 `$$; haftmann@24219: infixr 3 `|->; haftmann@24219: infixr 3 `|-->; haftmann@24219: haftmann@24219: signature BASIC_CODE_THINGOL = haftmann@24219: sig haftmann@24219: type vname = string; haftmann@24219: datatype dict = haftmann@24219: DictConst of string * dict list list haftmann@24219: | DictVar of string list * (vname * (int * int)); haftmann@24219: datatype itype = haftmann@24219: `%% of string * itype list haftmann@24219: | ITyVar of vname; haftmann@24591: type const = string * (dict list list * itype list (*types of arguments*)) haftmann@24219: datatype iterm = haftmann@24591: IConst of const haftmann@24219: | IVar of vname haftmann@24219: | `$ of iterm * iterm haftmann@24219: | `|-> of (vname * itype) * iterm haftmann@24219: | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm; haftmann@24219: (*((term, type), [(selector pattern, body term )]), primitive term)*) haftmann@24219: val `-> : itype * itype -> itype; haftmann@24219: val `--> : itype list * itype -> itype; haftmann@24219: val `$$ : iterm * iterm list -> iterm; haftmann@24219: val `|--> : (vname * itype) list * iterm -> iterm; haftmann@24219: type typscheme = (vname * sort) list * itype; haftmann@24219: end; haftmann@24219: haftmann@24219: signature CODE_THINGOL = haftmann@24219: sig haftmann@24219: include BASIC_CODE_THINGOL; haftmann@24219: val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list; haftmann@24219: val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a; haftmann@24219: val unfold_fun: itype -> itype list * itype; haftmann@24219: val unfold_app: iterm -> iterm * iterm list; haftmann@24219: val split_abs: iterm -> (((vname * iterm option) * itype) * iterm) option; haftmann@24219: val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm; haftmann@24219: val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option; haftmann@24219: val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm; haftmann@24219: val unfold_const_app: iterm -> haftmann@24219: ((string * (dict list list * itype list)) * iterm list) option; haftmann@24219: val collapse_let: ((vname * itype) * iterm) * iterm haftmann@24219: -> (iterm * itype) * (iterm * iterm) list; haftmann@24219: val eta_expand: (string * (dict list list * itype list)) * iterm list -> int -> iterm; haftmann@24662: val contains_dictvar: iterm -> bool; haftmann@25621: val locally_monomorphic: iterm -> bool; haftmann@24219: val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a; haftmann@24219: val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a; haftmann@24219: val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a; haftmann@24219: haftmann@24918: datatype stmt = haftmann@27024: NoStmt haftmann@24591: | Fun of typscheme * ((iterm list * iterm) * thm) list haftmann@24219: | Datatype of (vname * sort) list * (string * itype list) list haftmann@24219: | Datatypecons of string haftmann@24811: | Class of vname * ((class * string) list * (string * itype) list) haftmann@24219: | Classrel of class * class haftmann@24837: | Classparam of class haftmann@24219: | Classinst of (class * (string * (vname * sort) list)) haftmann@24219: * ((class * (string * (string * dict list list))) list haftmann@24591: * ((string * const) * thm) list); haftmann@27103: type program = stmt Graph.T; haftmann@27103: val empty_funs: program -> string list; haftmann@27103: val transitivly_non_empty_funs: program -> string list -> string list; haftmann@27103: val is_cons: program -> string -> bool; haftmann@27103: val contr_classparam_typs: program -> string -> itype option list; haftmann@24219: haftmann@27103: val consts_program: theory -> string list -> string list * program; haftmann@27103: val cached_program: theory -> program; haftmann@27103: val eval_conv: theory haftmann@27103: -> (term -> term * (program -> typscheme * iterm -> string list -> thm)) haftmann@27103: -> cterm -> thm; haftmann@27103: val eval_term: theory haftmann@27103: -> (term -> term * (program -> typscheme * iterm -> string list -> 'a)) haftmann@27103: -> term -> 'a; haftmann@24219: end; haftmann@24219: haftmann@24219: structure CodeThingol: CODE_THINGOL = haftmann@24219: struct haftmann@24219: haftmann@24219: (** auxiliary **) haftmann@24219: haftmann@24219: fun unfoldl dest x = haftmann@24219: case dest x haftmann@24219: of NONE => (x, []) haftmann@24219: | SOME (x1, x2) => haftmann@24219: let val (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end; haftmann@24219: haftmann@24219: fun unfoldr dest x = haftmann@24219: case dest x haftmann@24219: of NONE => ([], x) haftmann@24219: | SOME (x1, x2) => haftmann@24219: let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end; haftmann@24219: haftmann@24219: haftmann@24219: (** language core - types, pattern, expressions **) haftmann@24219: haftmann@24219: (* language representation *) haftmann@24219: haftmann@24219: type vname = string; haftmann@24219: haftmann@24219: datatype dict = haftmann@24219: DictConst of string * dict list list haftmann@24219: | DictVar of string list * (vname * (int * int)); haftmann@24219: haftmann@24219: datatype itype = haftmann@24219: `%% of string * itype list haftmann@24219: | ITyVar of vname; haftmann@24219: haftmann@24591: type const = string * (dict list list * itype list (*types of arguments*)) haftmann@24591: haftmann@24219: datatype iterm = haftmann@24591: IConst of const haftmann@24219: | IVar of vname haftmann@24219: | `$ of iterm * iterm haftmann@24219: | `|-> of (vname * itype) * iterm haftmann@24219: | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm; haftmann@24219: (*see also signature*) haftmann@24219: haftmann@24219: (* haftmann@24219: variable naming conventions haftmann@24219: haftmann@24219: bare names: haftmann@24219: variable names v haftmann@24219: class names class haftmann@24219: type constructor names tyco haftmann@24219: datatype names dtco haftmann@24837: const names (general) c (const) haftmann@24219: constructor names co haftmann@24837: class parameter names classparam haftmann@24219: arbitrary name s haftmann@24219: haftmann@24837: v, c, co, classparam also annotated with types etc. haftmann@24219: haftmann@24219: constructs: haftmann@24219: sort sort haftmann@24219: type parameters vs haftmann@24219: type ty haftmann@24219: type schemes tysm haftmann@24219: term t haftmann@24219: (term as pattern) p haftmann@24219: instance (class, tyco) inst haftmann@24219: *) haftmann@24219: haftmann@24219: fun ty1 `-> ty2 = "fun" `%% [ty1, ty2]; haftmann@24219: val op `--> = Library.foldr (op `->); haftmann@24219: val op `$$ = Library.foldl (op `$); haftmann@24219: val op `|--> = Library.foldr (op `|->); haftmann@24219: haftmann@24219: val unfold_fun = unfoldr haftmann@24219: (fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2) haftmann@24219: | _ => NONE); haftmann@24219: haftmann@24219: val unfold_app = unfoldl haftmann@24219: (fn op `$ t => SOME t haftmann@24219: | _ => NONE); haftmann@24219: haftmann@24219: val split_abs = haftmann@24219: (fn (v, ty) `|-> (t as ICase (((IVar w, _), [(p, t')]), _)) => haftmann@24219: if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t) haftmann@24219: | (v, ty) `|-> t => SOME (((v, NONE), ty), t) haftmann@24219: | _ => NONE); haftmann@24219: haftmann@24219: val unfold_abs = unfoldr split_abs; haftmann@24219: haftmann@24219: val split_let = haftmann@24219: (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t) haftmann@24219: | _ => NONE); haftmann@24219: haftmann@24219: val unfold_let = unfoldr split_let; haftmann@24219: haftmann@24219: fun unfold_const_app t = haftmann@24219: case unfold_app t haftmann@24219: of (IConst c, ts) => SOME (c, ts) haftmann@24219: | _ => NONE; haftmann@24219: haftmann@24219: fun fold_aiterms f (t as IConst _) = f t haftmann@24219: | fold_aiterms f (t as IVar _) = f t haftmann@24219: | fold_aiterms f (t1 `$ t2) = fold_aiterms f t1 #> fold_aiterms f t2 haftmann@24219: | fold_aiterms f (t as _ `|-> t') = f t #> fold_aiterms f t' haftmann@24219: | fold_aiterms f (ICase (_, t)) = fold_aiterms f t; haftmann@24219: haftmann@24219: fun fold_constnames f = haftmann@24219: let haftmann@24219: fun add (IConst (c, _)) = f c haftmann@24219: | add _ = I; haftmann@24219: in fold_aiterms add end; haftmann@24219: haftmann@24219: fun fold_varnames f = haftmann@24219: let haftmann@24219: fun add (IVar v) = f v haftmann@24219: | add ((v, _) `|-> _) = f v haftmann@24219: | add _ = I; haftmann@24219: in fold_aiterms add end; haftmann@24219: haftmann@24219: fun fold_unbound_varnames f = haftmann@24219: let haftmann@24219: fun add _ (IConst _) = I haftmann@24219: | add vs (IVar v) = if not (member (op =) vs v) then f v else I haftmann@24219: | add vs (t1 `$ t2) = add vs t1 #> add vs t2 haftmann@24219: | add vs ((v, _) `|-> t) = add (insert (op =) v vs) t haftmann@24219: | add vs (ICase (_, t)) = add vs t; haftmann@24219: in add [] end; haftmann@24219: haftmann@24219: fun collapse_let (((v, ty), se), be as ICase (((IVar w, _), ds), _)) = haftmann@24219: let haftmann@24219: fun exists_v t = fold_unbound_varnames (fn w => fn b => haftmann@24219: b orelse v = w) t false; haftmann@24219: in if v = w andalso forall (fn (t1, t2) => haftmann@24219: exists_v t1 orelse not (exists_v t2)) ds haftmann@24219: then ((se, ty), ds) haftmann@24219: else ((se, ty), [(IVar v, be)]) haftmann@24219: end haftmann@24219: | collapse_let (((v, ty), se), be) = haftmann@24219: ((se, ty), [(IVar v, be)]) haftmann@24219: haftmann@24219: fun eta_expand (c as (_, (_, tys)), ts) k = haftmann@24219: let haftmann@24219: val j = length ts; haftmann@24219: val l = k - j; haftmann@24219: val ctxt = (fold o fold_varnames) Name.declare ts Name.context; haftmann@24219: val vs_tys = Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys); haftmann@24219: in vs_tys `|--> IConst c `$$ ts @ map (fn (v, _) => IVar v) vs_tys end; haftmann@24219: haftmann@24662: fun contains_dictvar t = haftmann@24662: let haftmann@24662: fun contains (DictConst (_, dss)) = (fold o fold) contains dss haftmann@24662: | contains (DictVar _) = K true; haftmann@24662: in haftmann@24662: fold_aiterms haftmann@24662: (fn IConst (_, (dss, _)) => (fold o fold) contains dss | _ => I) t false haftmann@24662: end; haftmann@24662: haftmann@25621: fun locally_monomorphic (IConst _) = false haftmann@25621: | locally_monomorphic (IVar _) = true haftmann@25621: | locally_monomorphic (t `$ _) = locally_monomorphic t haftmann@25621: | locally_monomorphic (_ `|-> t) = locally_monomorphic t haftmann@25621: | locally_monomorphic (ICase ((_, ds), _)) = exists (locally_monomorphic o snd) ds; haftmann@25621: haftmann@25621: haftmann@24219: haftmann@27103: (** statements, abstract programs **) haftmann@24219: haftmann@24219: type typscheme = (vname * sort) list * itype; haftmann@24918: datatype stmt = haftmann@27024: NoStmt haftmann@24591: | Fun of typscheme * ((iterm list * iterm) * thm) list haftmann@24219: | Datatype of (vname * sort) list * (string * itype list) list haftmann@24219: | Datatypecons of string haftmann@24811: | Class of vname * ((class * string) list * (string * itype) list) haftmann@24219: | Classrel of class * class haftmann@24837: | Classparam of class haftmann@24219: | Classinst of (class * (string * (vname * sort) list)) haftmann@24219: * ((class * (string * (string * dict list list))) list haftmann@24591: * ((string * const) * thm) list); haftmann@24219: haftmann@27103: type program = stmt Graph.T; haftmann@24219: haftmann@27103: fun empty_funs program = haftmann@27103: Graph.fold (fn (name, (Fun (_, []), _)) => cons name haftmann@27103: | _ => I) program []; haftmann@24219: haftmann@27103: fun transitivly_non_empty_funs program names_ignored = haftmann@24219: let haftmann@27103: val names_empty = empty_funs program; haftmann@27103: val names_delete = Graph.all_preds program (subtract (op =) names_ignored names_empty) haftmann@27103: in subtract (op =) names_delete (Graph.keys program) end; haftmann@24219: haftmann@27103: fun is_cons program name = case Graph.get_node program name haftmann@24219: of Datatypecons _ => true haftmann@24219: | _ => false; haftmann@24219: haftmann@27103: fun contr_classparam_typs program name = case Graph.get_node program name haftmann@25621: of Classparam class => let haftmann@27103: val Class (_, (_, params)) = Graph.get_node program class; haftmann@25621: val SOME ty = AList.lookup (op =) params name; haftmann@25621: val (tys, res_ty) = unfold_fun ty; haftmann@25621: fun no_tyvar (_ `%% tys) = forall no_tyvar tys haftmann@25621: | no_tyvar (ITyVar _) = false; haftmann@25621: in if no_tyvar res_ty haftmann@25621: then map (fn ty => if no_tyvar ty then NONE else SOME ty) tys haftmann@25621: else [] haftmann@25621: end haftmann@25621: | _ => []; haftmann@25621: haftmann@24219: haftmann@27103: (** translation kernel **) haftmann@24219: haftmann@27103: fun ensure_stmt stmtgen name (dep, program) = haftmann@24219: let haftmann@27103: val add_dep = case dep of NONE => I | SOME dep => Graph.add_edge (dep, name); haftmann@27103: fun add_stmt false = haftmann@27103: Graph.default_node (name, NoStmt) haftmann@27103: #> add_dep haftmann@24918: #> curry stmtgen (SOME name) haftmann@24252: ##> snd haftmann@27103: #-> (fn stmt => Graph.map_node name (K stmt)) haftmann@27103: | add_stmt true = haftmann@27103: add_dep; haftmann@24219: in haftmann@27103: program haftmann@27103: |> add_stmt (can (Graph.get_node program) name) haftmann@24219: |> pair dep haftmann@24918: |> pair name haftmann@24219: end; haftmann@24219: haftmann@26972: fun not_wellsorted thy thm ty sort e = haftmann@26972: let haftmann@26972: val err_class = Sorts.class_error (Syntax.pp_global thy) e; haftmann@26972: val err_thm = case thm haftmann@26972: of SOME thm => "\n(in defining equation " ^ Display.string_of_thm thm ^ ")" | NONE => ""; haftmann@26972: val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort " haftmann@26972: ^ Syntax.string_of_sort_global thy sort; haftmann@26972: in error ("Wellsortedness error" ^ err_thm ^ ":\n" ^ err_typ ^ "\n" ^ err_class) end; haftmann@26972: haftmann@26972: fun ensure_class thy (algbr as (_, algebra)) funcgr class = haftmann@24918: let haftmann@24918: val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class; wenzelm@24969: val cs = #params (AxClass.get_info thy class); haftmann@24918: val class' = CodeName.class thy class; haftmann@24918: val stmt_class = haftmann@24918: fold_map (fn superclass => ensure_class thy algbr funcgr superclass haftmann@24918: ##>> ensure_classrel thy algbr funcgr (class, superclass)) superclasses haftmann@24918: ##>> fold_map (fn (c, ty) => ensure_const thy algbr funcgr c haftmann@24918: ##>> exprgen_typ thy algbr funcgr ty) cs wenzelm@24969: #>> (fn info => Class (unprefix "'" Name.aT, info)) haftmann@27422: in ensure_stmt stmt_class class' end haftmann@24918: and ensure_classrel thy algbr funcgr (subclass, superclass) = haftmann@24918: let haftmann@24918: val classrel' = CodeName.classrel thy (subclass, superclass); haftmann@24918: val stmt_classrel = haftmann@24918: ensure_class thy algbr funcgr subclass haftmann@24918: ##>> ensure_class thy algbr funcgr superclass haftmann@24918: #>> Classrel; haftmann@27422: in ensure_stmt stmt_classrel classrel' end haftmann@24918: and ensure_tyco thy algbr funcgr "fun" = haftmann@24918: pair "fun" haftmann@24918: | ensure_tyco thy algbr funcgr tyco = haftmann@24918: let haftmann@24918: val stmt_datatype = haftmann@24918: let haftmann@24918: val (vs, cos) = Code.get_datatype thy tyco; haftmann@24918: in haftmann@24918: fold_map (exprgen_tyvar_sort thy algbr funcgr) vs haftmann@24918: ##>> fold_map (fn (c, tys) => haftmann@24918: ensure_const thy algbr funcgr c haftmann@24918: ##>> fold_map (exprgen_typ thy algbr funcgr) tys) cos haftmann@24918: #>> Datatype haftmann@24918: end; haftmann@24918: val tyco' = CodeName.tyco thy tyco; haftmann@27422: in ensure_stmt stmt_datatype tyco' end haftmann@26972: and exprgen_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) = haftmann@24918: fold_map (ensure_class thy algbr funcgr) (proj_sort sort) haftmann@24918: #>> (fn sort => (unprefix "'" v, sort)) haftmann@27422: and exprgen_typ thy algbr funcgr (TFree v_sort) = haftmann@27422: exprgen_tyvar_sort thy algbr funcgr v_sort haftmann@24918: #>> (fn (v, sort) => ITyVar v) haftmann@24918: | exprgen_typ thy algbr funcgr (Type (tyco, tys)) = haftmann@24918: ensure_tyco thy algbr funcgr tyco haftmann@24918: ##>> fold_map (exprgen_typ thy algbr funcgr) tys haftmann@24918: #>> (fn (tyco, tys) => tyco `%% tys) haftmann@26972: and exprgen_dicts thy (algbr as (proj_sort, algebra)) funcgr thm (ty, sort) = haftmann@24918: let wenzelm@26939: val pp = Syntax.pp_global thy; haftmann@24918: datatype typarg = haftmann@24918: Global of (class * string) * typarg list list haftmann@24918: | Local of (class * class) list * (string * (int * sort)); haftmann@24918: fun class_relation (Global ((_, tyco), yss), _) class = haftmann@24918: Global ((class, tyco), yss) haftmann@24918: | class_relation (Local (classrels, v), subclass) superclass = haftmann@24918: Local ((subclass, superclass) :: classrels, v); haftmann@24918: fun type_constructor tyco yss class = haftmann@24918: Global ((class, tyco), (map o map) fst yss); haftmann@24918: fun type_variable (TFree (v, sort)) = haftmann@24918: let haftmann@24918: val sort' = proj_sort sort; haftmann@24918: in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end; haftmann@24918: val typargs = Sorts.of_sort_derivation pp algebra haftmann@24918: {class_relation = class_relation, type_constructor = type_constructor, haftmann@26972: type_variable = type_variable} (ty, proj_sort sort) haftmann@26972: handle Sorts.CLASS_ERROR e => not_wellsorted thy thm ty sort e; haftmann@24918: fun mk_dict (Global (inst, yss)) = haftmann@24918: ensure_inst thy algbr funcgr inst haftmann@24918: ##>> (fold_map o fold_map) mk_dict yss haftmann@24918: #>> (fn (inst, dss) => DictConst (inst, dss)) haftmann@24918: | mk_dict (Local (classrels, (v, (k, sort)))) = haftmann@24918: fold_map (ensure_classrel thy algbr funcgr) classrels haftmann@24918: #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort)))) haftmann@27422: in fold_map mk_dict typargs end haftmann@24918: and exprgen_eq thy algbr funcgr thm = haftmann@24918: let haftmann@24918: val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals haftmann@24918: o Logic.unvarify o prop_of) thm; haftmann@24918: in haftmann@26972: fold_map (exprgen_term thy algbr funcgr (SOME thm)) args haftmann@26972: ##>> exprgen_term thy algbr funcgr (SOME thm) rhs haftmann@24918: #>> rpair thm haftmann@24918: end haftmann@26972: and ensure_inst thy (algbr as (_, algebra)) funcgr (class, tyco) = haftmann@24918: let haftmann@24918: val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class; wenzelm@24969: val classparams = these (try (#params o AxClass.get_info thy) class); haftmann@24918: val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]); haftmann@24918: val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class]; haftmann@24918: val vs' = map2 (fn (v, sort1) => fn sort2 => (v, haftmann@24918: Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts'; haftmann@24918: val arity_typ = Type (tyco, map TFree vs); haftmann@24918: val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs'); haftmann@24918: fun exprgen_superarity superclass = haftmann@24918: ensure_class thy algbr funcgr superclass haftmann@24918: ##>> ensure_classrel thy algbr funcgr (class, superclass) haftmann@26972: ##>> exprgen_dicts thy algbr funcgr NONE (arity_typ, [superclass]) haftmann@24918: #>> (fn ((superclass, classrel), [DictConst (inst, dss)]) => haftmann@24918: (superclass, (classrel, (inst, dss)))); haftmann@24918: fun exprgen_classparam_inst (c, ty) = haftmann@24918: let haftmann@24918: val c_inst = Const (c, map_type_tfree (K arity_typ') ty); haftmann@25597: val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy c_inst); haftmann@24918: val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd haftmann@24918: o Logic.dest_equals o Thm.prop_of) thm; haftmann@24918: in haftmann@24918: ensure_const thy algbr funcgr c haftmann@26972: ##>> exprgen_const thy algbr funcgr (SOME thm) c_ty haftmann@24918: #>> (fn (c, IConst c_inst) => ((c, c_inst), thm)) haftmann@24918: end; haftmann@24918: val stmt_inst = haftmann@24918: ensure_class thy algbr funcgr class haftmann@24918: ##>> ensure_tyco thy algbr funcgr tyco haftmann@24918: ##>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs haftmann@24918: ##>> fold_map exprgen_superarity superclasses haftmann@24918: ##>> fold_map exprgen_classparam_inst classparams haftmann@24918: #>> (fn ((((class, tyco), arity), superarities), classparams) => haftmann@24918: Classinst ((class, (tyco, arity)), (superarities, classparams))); haftmann@24918: val inst = CodeName.instance thy (class, tyco); haftmann@27422: in ensure_stmt stmt_inst inst end haftmann@26972: and ensure_const thy algbr funcgr c = haftmann@24918: let haftmann@24918: val c' = CodeName.const thy c; haftmann@24918: fun stmt_datatypecons tyco = haftmann@24918: ensure_tyco thy algbr funcgr tyco haftmann@25621: #>> Datatypecons; haftmann@24918: fun stmt_classparam class = haftmann@24918: ensure_class thy algbr funcgr class haftmann@25621: #>> Classparam; haftmann@24918: fun stmt_fun trns = haftmann@24918: let haftmann@24918: val raw_thms = CodeFuncgr.funcs funcgr c; haftmann@26972: val (vs, raw_ty) = CodeFuncgr.typ funcgr c; haftmann@26972: val ty = Logic.unvarifyT raw_ty; haftmann@24918: val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty haftmann@24918: then raw_thms haftmann@24918: else map (CodeUnit.expand_eta 1) raw_thms; haftmann@24918: in haftmann@24918: trns haftmann@24918: |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs haftmann@24918: ||>> exprgen_typ thy algbr funcgr ty haftmann@24918: ||>> fold_map (exprgen_eq thy algbr funcgr) thms haftmann@24918: |>> (fn ((vs, ty), eqs) => Fun ((vs, ty), eqs)) haftmann@24918: end; haftmann@24918: val stmtgen = case Code.get_datatype_of_constr thy c haftmann@24918: of SOME tyco => stmt_datatypecons tyco haftmann@24918: | NONE => (case AxClass.class_of_param thy c haftmann@24918: of SOME class => stmt_classparam class haftmann@24918: | NONE => stmt_fun) haftmann@27422: in ensure_stmt stmtgen c' end haftmann@26972: and exprgen_term thy algbr funcgr thm (Const (c, ty)) = haftmann@26972: exprgen_app thy algbr funcgr thm ((c, ty), []) haftmann@26972: | exprgen_term thy algbr funcgr thm (Free (v, _)) = haftmann@24918: pair (IVar v) haftmann@26972: | exprgen_term thy algbr funcgr thm (Abs (abs as (_, ty, _))) = haftmann@24918: let haftmann@24918: val (v, t) = Syntax.variant_abs abs; haftmann@24918: in haftmann@24918: exprgen_typ thy algbr funcgr ty haftmann@26972: ##>> exprgen_term thy algbr funcgr thm t haftmann@24918: #>> (fn (ty, t) => (v, ty) `|-> t) haftmann@24918: end haftmann@26972: | exprgen_term thy algbr funcgr thm (t as _ $ _) = haftmann@24918: case strip_comb t haftmann@24918: of (Const (c, ty), ts) => haftmann@26972: exprgen_app thy algbr funcgr thm ((c, ty), ts) haftmann@24918: | (t', ts) => haftmann@26972: exprgen_term thy algbr funcgr thm t' haftmann@26972: ##>> fold_map (exprgen_term thy algbr funcgr thm) ts haftmann@24918: #>> (fn (t, ts) => t `$$ ts) haftmann@26972: and exprgen_const thy algbr funcgr thm (c, ty) = haftmann@26972: let haftmann@26972: val tys = Sign.const_typargs thy (c, ty); haftmann@26972: val sorts = (map snd o fst o CodeFuncgr.typ funcgr) c; haftmann@26972: val tys_args = (fst o Term.strip_type) ty; haftmann@26972: in haftmann@26972: ensure_const thy algbr funcgr c haftmann@26972: ##>> fold_map (exprgen_dicts thy algbr funcgr thm) (tys ~~ sorts) haftmann@26972: ##>> fold_map (exprgen_typ thy algbr funcgr) tys_args haftmann@26972: #>> (fn ((c, iss), tys) => IConst (c, (iss, tys))) haftmann@26972: end haftmann@26972: and exprgen_app_default thy algbr funcgr thm (c_ty, ts) = haftmann@26972: exprgen_const thy algbr funcgr thm c_ty haftmann@26972: ##>> fold_map (exprgen_term thy algbr funcgr thm) ts haftmann@24918: #>> (fn (t, ts) => t `$$ ts) haftmann@26972: and exprgen_case thy algbr funcgr thm n cases (app as ((c, ty), ts)) = haftmann@24918: let haftmann@24918: val (tys, _) = haftmann@24918: (chop (1 + (if null cases then 1 else length cases)) o fst o strip_type) ty; haftmann@24918: val dt = nth ts n; haftmann@24918: val dty = nth tys n; haftmann@24918: fun is_undefined (Const (c, _)) = Code.is_undefined thy c haftmann@24918: | is_undefined _ = false; haftmann@24918: fun mk_case (co, n) t = haftmann@24918: let haftmann@24918: val (vs, body) = Term.strip_abs_eta n t; haftmann@24918: val selector = list_comb (Const (co, map snd vs ---> dty), map Free vs); haftmann@24918: in if is_undefined body then NONE else SOME (selector, body) end; haftmann@24918: fun mk_ds [] = haftmann@24918: let haftmann@24918: val ([v_ty], body) = Term.strip_abs_eta 1 (the_single (nth_drop n ts)) haftmann@24918: in [(Free v_ty, body)] end haftmann@24918: | mk_ds cases = map_filter (uncurry mk_case) haftmann@24918: (AList.make (CodeUnit.no_args thy) cases ~~ nth_drop n ts); haftmann@24918: in haftmann@26972: exprgen_term thy algbr funcgr thm dt haftmann@24918: ##>> exprgen_typ thy algbr funcgr dty haftmann@26972: ##>> fold_map (fn (pat, body) => exprgen_term thy algbr funcgr thm pat haftmann@26972: ##>> exprgen_term thy algbr funcgr thm body) (mk_ds cases) haftmann@26972: ##>> exprgen_app_default thy algbr funcgr thm app haftmann@24918: #>> (fn (((dt, dty), ds), t0) => ICase (((dt, dty), ds), t0)) haftmann@24918: end haftmann@26972: and exprgen_app thy algbr funcgr thm ((c, ty), ts) = case Code.get_case_data thy c haftmann@24918: of SOME (n, cases) => let val i = 1 + (if null cases then 1 else length cases) in haftmann@24918: if length ts < i then haftmann@24918: let haftmann@24918: val k = length ts; haftmann@24918: val tys = (curry Library.take (i - k) o curry Library.drop k o fst o strip_type) ty; haftmann@24918: val ctxt = (fold o fold_aterms) haftmann@24918: (fn Free (v, _) => Name.declare v | _ => I) ts Name.context; haftmann@24918: val vs = Name.names ctxt "a" tys; haftmann@24918: in haftmann@24918: fold_map (exprgen_typ thy algbr funcgr) tys haftmann@26972: ##>> exprgen_case thy algbr funcgr thm n cases ((c, ty), ts @ map Free vs) haftmann@24918: #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t) haftmann@24918: end haftmann@24918: else if length ts > i then haftmann@26972: exprgen_case thy algbr funcgr thm n cases ((c, ty), Library.take (i, ts)) haftmann@26972: ##>> fold_map (exprgen_term thy algbr funcgr thm) (Library.drop (i, ts)) haftmann@24918: #>> (fn (t, ts) => t `$$ ts) haftmann@24918: else haftmann@26972: exprgen_case thy algbr funcgr thm n cases ((c, ty), ts) haftmann@24918: end haftmann@26972: | NONE => exprgen_app_default thy algbr funcgr thm ((c, ty), ts); haftmann@24918: haftmann@25969: haftmann@27103: (** generated programs **) haftmann@27103: haftmann@27103: (* store *) haftmann@27103: haftmann@27103: structure Program = CodeDataFun haftmann@27103: ( haftmann@27103: type T = program; haftmann@27103: val empty = Graph.empty; haftmann@27609: fun purge thy cs program = haftmann@27609: let haftmann@27609: val cs_exisiting = haftmann@27609: map_filter (CodeName.const_rev thy) (Graph.keys program); haftmann@27609: val dels = (Graph.all_preds program haftmann@27609: o map (CodeName.const thy) haftmann@27609: o filter (member (op =) cs_exisiting) haftmann@27609: ) cs; haftmann@27609: in Graph.del_nodes dels program end; haftmann@27103: ); haftmann@27103: haftmann@27103: val cached_program = Program.get; haftmann@25969: haftmann@27103: fun transact f program = haftmann@27103: (NONE, program) haftmann@27103: |> f haftmann@27103: |-> (fn x => fn (_, program) => (x, program)); haftmann@27103: haftmann@27103: fun generate thy funcgr f x = haftmann@27103: Program.change_yield thy (transact (f thy (Code.operational_algebra thy) funcgr x)); haftmann@27103: haftmann@27103: haftmann@27103: (* program generation *) haftmann@27103: haftmann@27103: fun consts_program thy cs = haftmann@27103: let haftmann@27103: fun project_consts cs program = haftmann@27103: let haftmann@27103: val cs_all = Graph.all_succs program cs; haftmann@27103: in (cs, Graph.subgraph (member (op =) cs_all) program) end; haftmann@27103: fun generate_consts thy algebra funcgr = haftmann@27103: fold_map (ensure_const thy algebra funcgr); haftmann@27103: in haftmann@27103: generate thy (CodeFuncgr.make thy cs) generate_consts cs haftmann@27103: |-> project_consts haftmann@27103: end; haftmann@27103: haftmann@27103: haftmann@27103: (* value evaluation *) haftmann@25969: haftmann@24918: fun ensure_value thy algbr funcgr t = haftmann@24918: let haftmann@24918: val ty = fastype_of t; haftmann@24918: val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =) haftmann@24918: o dest_TFree))) t []; haftmann@24918: val stmt_value = haftmann@24918: fold_map (exprgen_tyvar_sort thy algbr funcgr) vs haftmann@24918: ##>> exprgen_typ thy algbr funcgr ty haftmann@26972: ##>> exprgen_term thy algbr funcgr NONE t haftmann@24918: #>> (fn ((vs, ty), t) => Fun ((vs, ty), [(([], t), Drule.dummy_thm)])); haftmann@27103: fun term_value (dep, program1) = haftmann@25969: let haftmann@25969: val Fun ((vs, ty), [(([], t), _)]) = haftmann@27103: Graph.get_node program1 CodeName.value_name; haftmann@27103: val deps = Graph.imm_succs program1 CodeName.value_name; haftmann@27103: val program2 = Graph.del_nodes [CodeName.value_name] program1; haftmann@27103: val deps_all = Graph.all_succs program2 deps; haftmann@27103: val program3 = Graph.subgraph (member (op =) deps_all) program2; haftmann@27103: in ((program3, (((vs, ty), t), deps)), (dep, program2)) end; haftmann@26011: in haftmann@26011: ensure_stmt stmt_value CodeName.value_name haftmann@26011: #> snd haftmann@26011: #> term_value haftmann@26011: end; haftmann@24219: haftmann@27103: fun eval eval_kind thy evaluator = haftmann@27103: let haftmann@27103: fun evaluator'' evaluator''' funcgr t = haftmann@27103: let haftmann@27103: val ((program, (vs_ty_t, deps)), _) = generate thy funcgr ensure_value t; haftmann@27103: in evaluator''' program vs_ty_t deps end; haftmann@27103: fun evaluator' t = haftmann@27103: let haftmann@27103: val (t', evaluator''') = evaluator t; haftmann@27103: in (t', evaluator'' evaluator''') end; haftmann@27103: in eval_kind thy evaluator' end haftmann@27103: haftmann@27103: fun eval_conv thy = eval CodeFuncgr.eval_conv thy; haftmann@27103: fun eval_term thy = eval CodeFuncgr.eval_term thy; haftmann@27103: haftmann@24219: end; (*struct*) haftmann@24219: haftmann@24219: haftmann@24219: structure BasicCodeThingol: BASIC_CODE_THINGOL = CodeThingol;