src/Tools/code/code_thingol.ML
author haftmann
Tue Jul 15 16:02:07 2008 +0200 (2008-07-15)
changeset 27609 b23c9ad0fe7d
parent 27422 73d25d422124
child 27711 5052736b8bcc
permissions -rw-r--r--
tuned code theorem bookkeeping
     1 (*  Title:      Tools/code/code_thingol.ML
     2     ID:         $Id$
     3     Author:     Florian Haftmann, TU Muenchen
     4 
     5 Intermediate language ("Thin-gol") representing executable code.
     6 Representation and translation.
     7 *)
     8 
     9 infix 8 `%%;
    10 infixr 6 `->;
    11 infixr 6 `-->;
    12 infix 4 `$;
    13 infix 4 `$$;
    14 infixr 3 `|->;
    15 infixr 3 `|-->;
    16 
    17 signature BASIC_CODE_THINGOL =
    18 sig
    19   type vname = string;
    20   datatype dict =
    21       DictConst of string * dict list list
    22     | DictVar of string list * (vname * (int * int));
    23   datatype itype =
    24       `%% of string * itype list
    25     | ITyVar of vname;
    26   type const = string * (dict list list * itype list (*types of arguments*))
    27   datatype iterm =
    28       IConst of const
    29     | IVar of vname
    30     | `$ of iterm * iterm
    31     | `|-> of (vname * itype) * iterm
    32     | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
    33         (*((term, type), [(selector pattern, body term )]), primitive term)*)
    34   val `-> : itype * itype -> itype;
    35   val `--> : itype list * itype -> itype;
    36   val `$$ : iterm * iterm list -> iterm;
    37   val `|--> : (vname * itype) list * iterm -> iterm;
    38   type typscheme = (vname * sort) list * itype;
    39 end;
    40 
    41 signature CODE_THINGOL =
    42 sig
    43   include BASIC_CODE_THINGOL;
    44   val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list;
    45   val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a;
    46   val unfold_fun: itype -> itype list * itype;
    47   val unfold_app: iterm -> iterm * iterm list;
    48   val split_abs: iterm -> (((vname * iterm option) * itype) * iterm) option;
    49   val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm;
    50   val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option;
    51   val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm;
    52   val unfold_const_app: iterm ->
    53     ((string * (dict list list * itype list)) * iterm list) option;
    54   val collapse_let: ((vname * itype) * iterm) * iterm
    55     -> (iterm * itype) * (iterm * iterm) list;
    56   val eta_expand: (string * (dict list list * itype list)) * iterm list -> int -> iterm;
    57   val contains_dictvar: iterm -> bool;
    58   val locally_monomorphic: iterm -> bool;
    59   val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
    60   val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
    61   val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
    62 
    63   datatype stmt =
    64       NoStmt
    65     | Fun of typscheme * ((iterm list * iterm) * thm) list
    66     | Datatype of (vname * sort) list * (string * itype list) list
    67     | Datatypecons of string
    68     | Class of vname * ((class * string) list * (string * itype) list)
    69     | Classrel of class * class
    70     | Classparam of class
    71     | Classinst of (class * (string * (vname * sort) list))
    72           * ((class * (string * (string * dict list list))) list
    73         * ((string * const) * thm) list);
    74   type program = stmt Graph.T;
    75   val empty_funs: program -> string list;
    76   val transitivly_non_empty_funs: program -> string list -> string list;
    77   val is_cons: program -> string -> bool;
    78   val contr_classparam_typs: program -> string -> itype option list;
    79 
    80   val consts_program: theory -> string list -> string list * program;
    81   val cached_program: theory -> program;
    82   val eval_conv: theory
    83     -> (term -> term * (program -> typscheme * iterm -> string list -> thm))
    84     -> cterm -> thm;
    85   val eval_term: theory
    86     -> (term -> term * (program -> typscheme * iterm -> string list -> 'a))
    87     -> term -> 'a;
    88 end;
    89 
    90 structure CodeThingol: CODE_THINGOL =
    91 struct
    92 
    93 (** auxiliary **)
    94 
    95 fun unfoldl dest x =
    96   case dest x
    97    of NONE => (x, [])
    98     | SOME (x1, x2) =>
    99         let val (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end;
   100 
   101 fun unfoldr dest x =
   102   case dest x
   103    of NONE => ([], x)
   104     | SOME (x1, x2) =>
   105         let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
   106 
   107 
   108 (** language core - types, pattern, expressions **)
   109 
   110 (* language representation *)
   111 
   112 type vname = string;
   113 
   114 datatype dict =
   115     DictConst of string * dict list list
   116   | DictVar of string list * (vname * (int * int));
   117 
   118 datatype itype =
   119     `%% of string * itype list
   120   | ITyVar of vname;
   121 
   122 type const = string * (dict list list * itype list (*types of arguments*))
   123 
   124 datatype iterm =
   125     IConst of const
   126   | IVar of vname
   127   | `$ of iterm * iterm
   128   | `|-> of (vname * itype) * iterm
   129   | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
   130     (*see also signature*)
   131 
   132 (*
   133   variable naming conventions
   134 
   135   bare names:
   136     variable names          v
   137     class names             class
   138     type constructor names  tyco
   139     datatype names          dtco
   140     const names (general)   c (const)
   141     constructor names       co
   142     class parameter names   classparam
   143     arbitrary name          s
   144 
   145     v, c, co, classparam also annotated with types etc.
   146 
   147   constructs:
   148     sort                    sort
   149     type parameters         vs
   150     type                    ty
   151     type schemes            tysm
   152     term                    t
   153     (term as pattern)       p
   154     instance (class, tyco)  inst
   155  *)
   156 
   157 fun ty1 `-> ty2 = "fun" `%% [ty1, ty2];
   158 val op `--> = Library.foldr (op `->);
   159 val op `$$ = Library.foldl (op `$);
   160 val op `|--> = Library.foldr (op `|->);
   161 
   162 val unfold_fun = unfoldr
   163   (fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2)
   164     | _ => NONE);
   165 
   166 val unfold_app = unfoldl
   167   (fn op `$ t => SOME t
   168     | _ => NONE);
   169 
   170 val split_abs =
   171   (fn (v, ty) `|-> (t as ICase (((IVar w, _), [(p, t')]), _)) =>
   172         if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t)
   173     | (v, ty) `|-> t => SOME (((v, NONE), ty), t)
   174     | _ => NONE);
   175 
   176 val unfold_abs = unfoldr split_abs;
   177 
   178 val split_let = 
   179   (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
   180     | _ => NONE);
   181 
   182 val unfold_let = unfoldr split_let;
   183 
   184 fun unfold_const_app t =
   185  case unfold_app t
   186   of (IConst c, ts) => SOME (c, ts)
   187    | _ => NONE;
   188 
   189 fun fold_aiterms f (t as IConst _) = f t
   190   | fold_aiterms f (t as IVar _) = f t
   191   | fold_aiterms f (t1 `$ t2) = fold_aiterms f t1 #> fold_aiterms f t2
   192   | fold_aiterms f (t as _ `|-> t') = f t #> fold_aiterms f t'
   193   | fold_aiterms f (ICase (_, t)) = fold_aiterms f t;
   194 
   195 fun fold_constnames f =
   196   let
   197     fun add (IConst (c, _)) = f c
   198       | add _ = I;
   199   in fold_aiterms add end;
   200 
   201 fun fold_varnames f =
   202   let
   203     fun add (IVar v) = f v
   204       | add ((v, _) `|-> _) = f v
   205       | add _ = I;
   206   in fold_aiterms add end;
   207 
   208 fun fold_unbound_varnames f =
   209   let
   210     fun add _ (IConst _) = I
   211       | add vs (IVar v) = if not (member (op =) vs v) then f v else I
   212       | add vs (t1 `$ t2) = add vs t1 #> add vs t2
   213       | add vs ((v, _) `|-> t) = add (insert (op =) v vs) t
   214       | add vs (ICase (_, t)) = add vs t;
   215   in add [] end;
   216 
   217 fun collapse_let (((v, ty), se), be as ICase (((IVar w, _), ds), _)) =
   218       let
   219         fun exists_v t = fold_unbound_varnames (fn w => fn b =>
   220           b orelse v = w) t false;
   221       in if v = w andalso forall (fn (t1, t2) =>
   222         exists_v t1 orelse not (exists_v t2)) ds
   223         then ((se, ty), ds)
   224         else ((se, ty), [(IVar v, be)])
   225       end
   226   | collapse_let (((v, ty), se), be) =
   227       ((se, ty), [(IVar v, be)])
   228 
   229 fun eta_expand (c as (_, (_, tys)), ts) k =
   230   let
   231     val j = length ts;
   232     val l = k - j;
   233     val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
   234     val vs_tys = Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys);
   235   in vs_tys `|--> IConst c `$$ ts @ map (fn (v, _) => IVar v) vs_tys end;
   236 
   237 fun contains_dictvar t =
   238   let
   239     fun contains (DictConst (_, dss)) = (fold o fold) contains dss
   240       | contains (DictVar _) = K true;
   241   in
   242     fold_aiterms
   243       (fn IConst (_, (dss, _)) => (fold o fold) contains dss | _ => I) t false
   244   end;
   245   
   246 fun locally_monomorphic (IConst _) = false
   247   | locally_monomorphic (IVar _) = true
   248   | locally_monomorphic (t `$ _) = locally_monomorphic t
   249   | locally_monomorphic (_ `|-> t) = locally_monomorphic t
   250   | locally_monomorphic (ICase ((_, ds), _)) = exists (locally_monomorphic o snd) ds;
   251 
   252 
   253 
   254 (** statements, abstract programs **)
   255 
   256 type typscheme = (vname * sort) list * itype;
   257 datatype stmt =
   258     NoStmt
   259   | Fun of typscheme * ((iterm list * iterm) * thm) list
   260   | Datatype of (vname * sort) list * (string * itype list) list
   261   | Datatypecons of string
   262   | Class of vname * ((class * string) list * (string * itype) list)
   263   | Classrel of class * class
   264   | Classparam of class
   265   | Classinst of (class * (string * (vname * sort) list))
   266         * ((class * (string * (string * dict list list))) list
   267       * ((string * const) * thm) list);
   268 
   269 type program = stmt Graph.T;
   270 
   271 fun empty_funs program =
   272   Graph.fold (fn (name, (Fun (_, []), _)) => cons name
   273                | _ => I) program [];
   274 
   275 fun transitivly_non_empty_funs program names_ignored =
   276   let
   277     val names_empty = empty_funs program;
   278     val names_delete = Graph.all_preds program (subtract (op =) names_ignored names_empty)
   279   in subtract (op =) names_delete (Graph.keys program) end;
   280 
   281 fun is_cons program name = case Graph.get_node program name
   282  of Datatypecons _ => true
   283   | _ => false;
   284 
   285 fun contr_classparam_typs program name = case Graph.get_node program name
   286  of Classparam class => let
   287         val Class (_, (_, params)) = Graph.get_node program class;
   288         val SOME ty = AList.lookup (op =) params name;
   289         val (tys, res_ty) = unfold_fun ty;
   290         fun no_tyvar (_ `%% tys) = forall no_tyvar tys
   291           | no_tyvar (ITyVar _) = false;
   292       in if no_tyvar res_ty
   293         then map (fn ty => if no_tyvar ty then NONE else SOME ty) tys
   294         else []
   295       end
   296   | _ => [];
   297 
   298 
   299 (** translation kernel **)
   300 
   301 fun ensure_stmt stmtgen name (dep, program) =
   302   let
   303     val add_dep = case dep of NONE => I | SOME dep => Graph.add_edge (dep, name);
   304     fun add_stmt false =
   305           Graph.default_node (name, NoStmt)
   306           #> add_dep
   307           #> curry stmtgen (SOME name)
   308           ##> snd
   309           #-> (fn stmt => Graph.map_node name (K stmt))
   310       | add_stmt true =
   311           add_dep;
   312   in
   313     program
   314     |> add_stmt (can (Graph.get_node program) name)
   315     |> pair dep
   316     |> pair name
   317   end;
   318 
   319 fun not_wellsorted thy thm ty sort e =
   320   let
   321     val err_class = Sorts.class_error (Syntax.pp_global thy) e;
   322     val err_thm = case thm
   323      of SOME thm => "\n(in defining equation " ^ Display.string_of_thm thm ^ ")" | NONE => "";
   324     val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
   325       ^ Syntax.string_of_sort_global thy sort;
   326   in error ("Wellsortedness error" ^ err_thm ^ ":\n" ^ err_typ ^ "\n" ^ err_class) end;
   327 
   328 fun ensure_class thy (algbr as (_, algebra)) funcgr class =
   329   let
   330     val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
   331     val cs = #params (AxClass.get_info thy class);
   332     val class' = CodeName.class thy class;
   333     val stmt_class =
   334       fold_map (fn superclass => ensure_class thy algbr funcgr superclass
   335         ##>> ensure_classrel thy algbr funcgr (class, superclass)) superclasses
   336       ##>> fold_map (fn (c, ty) => ensure_const thy algbr funcgr c
   337         ##>> exprgen_typ thy algbr funcgr ty) cs
   338       #>> (fn info => Class (unprefix "'" Name.aT, info))
   339   in ensure_stmt stmt_class class' end
   340 and ensure_classrel thy algbr funcgr (subclass, superclass) =
   341   let
   342     val classrel' = CodeName.classrel thy (subclass, superclass);
   343     val stmt_classrel =
   344       ensure_class thy algbr funcgr subclass
   345       ##>> ensure_class thy algbr funcgr superclass
   346       #>> Classrel;
   347   in ensure_stmt stmt_classrel classrel' end
   348 and ensure_tyco thy algbr funcgr "fun" =
   349       pair "fun"
   350   | ensure_tyco thy algbr funcgr tyco =
   351       let
   352         val stmt_datatype =
   353           let
   354             val (vs, cos) = Code.get_datatype thy tyco;
   355           in
   356             fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
   357             ##>> fold_map (fn (c, tys) =>
   358               ensure_const thy algbr funcgr c
   359               ##>> fold_map (exprgen_typ thy algbr funcgr) tys) cos
   360             #>> Datatype
   361           end;
   362         val tyco' = CodeName.tyco thy tyco;
   363       in ensure_stmt stmt_datatype tyco' end
   364 and exprgen_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
   365   fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
   366   #>> (fn sort => (unprefix "'" v, sort))
   367 and exprgen_typ thy algbr funcgr (TFree v_sort) =
   368       exprgen_tyvar_sort thy algbr funcgr v_sort
   369       #>> (fn (v, sort) => ITyVar v)
   370   | exprgen_typ thy algbr funcgr (Type (tyco, tys)) =
   371       ensure_tyco thy algbr funcgr tyco
   372       ##>> fold_map (exprgen_typ thy algbr funcgr) tys
   373       #>> (fn (tyco, tys) => tyco `%% tys)
   374 and exprgen_dicts thy (algbr as (proj_sort, algebra)) funcgr thm (ty, sort) =
   375   let
   376     val pp = Syntax.pp_global thy;
   377     datatype typarg =
   378         Global of (class * string) * typarg list list
   379       | Local of (class * class) list * (string * (int * sort));
   380     fun class_relation (Global ((_, tyco), yss), _) class =
   381           Global ((class, tyco), yss)
   382       | class_relation (Local (classrels, v), subclass) superclass =
   383           Local ((subclass, superclass) :: classrels, v);
   384     fun type_constructor tyco yss class =
   385       Global ((class, tyco), (map o map) fst yss);
   386     fun type_variable (TFree (v, sort)) =
   387       let
   388         val sort' = proj_sort sort;
   389       in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
   390     val typargs = Sorts.of_sort_derivation pp algebra
   391       {class_relation = class_relation, type_constructor = type_constructor,
   392        type_variable = type_variable} (ty, proj_sort sort)
   393       handle Sorts.CLASS_ERROR e => not_wellsorted thy thm ty sort e;
   394     fun mk_dict (Global (inst, yss)) =
   395           ensure_inst thy algbr funcgr inst
   396           ##>> (fold_map o fold_map) mk_dict yss
   397           #>> (fn (inst, dss) => DictConst (inst, dss))
   398       | mk_dict (Local (classrels, (v, (k, sort)))) =
   399           fold_map (ensure_classrel thy algbr funcgr) classrels
   400           #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
   401   in fold_map mk_dict typargs end
   402 and exprgen_eq thy algbr funcgr thm =
   403   let
   404     val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
   405       o Logic.unvarify o prop_of) thm;
   406   in
   407     fold_map (exprgen_term thy algbr funcgr (SOME thm)) args
   408     ##>> exprgen_term thy algbr funcgr (SOME thm) rhs
   409     #>> rpair thm
   410   end
   411 and ensure_inst thy (algbr as (_, algebra)) funcgr (class, tyco) =
   412   let
   413     val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
   414     val classparams = these (try (#params o AxClass.get_info thy) class);
   415     val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
   416     val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
   417     val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
   418       Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
   419     val arity_typ = Type (tyco, map TFree vs);
   420     val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
   421     fun exprgen_superarity superclass =
   422       ensure_class thy algbr funcgr superclass
   423       ##>> ensure_classrel thy algbr funcgr (class, superclass)
   424       ##>> exprgen_dicts thy algbr funcgr NONE (arity_typ, [superclass])
   425       #>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
   426             (superclass, (classrel, (inst, dss))));
   427     fun exprgen_classparam_inst (c, ty) =
   428       let
   429         val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
   430         val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy c_inst);
   431         val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd
   432           o Logic.dest_equals o Thm.prop_of) thm;
   433       in
   434         ensure_const thy algbr funcgr c
   435         ##>> exprgen_const thy algbr funcgr (SOME thm) c_ty
   436         #>> (fn (c, IConst c_inst) => ((c, c_inst), thm))
   437       end;
   438     val stmt_inst =
   439       ensure_class thy algbr funcgr class
   440       ##>> ensure_tyco thy algbr funcgr tyco
   441       ##>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
   442       ##>> fold_map exprgen_superarity superclasses
   443       ##>> fold_map exprgen_classparam_inst classparams
   444       #>> (fn ((((class, tyco), arity), superarities), classparams) =>
   445              Classinst ((class, (tyco, arity)), (superarities, classparams)));
   446     val inst = CodeName.instance thy (class, tyco);
   447   in ensure_stmt stmt_inst inst end
   448 and ensure_const thy algbr funcgr c =
   449   let
   450     val c' = CodeName.const thy c;
   451     fun stmt_datatypecons tyco =
   452       ensure_tyco thy algbr funcgr tyco
   453       #>> Datatypecons;
   454     fun stmt_classparam class =
   455       ensure_class thy algbr funcgr class
   456       #>> Classparam;
   457     fun stmt_fun trns =
   458       let
   459         val raw_thms = CodeFuncgr.funcs funcgr c;
   460         val (vs, raw_ty) = CodeFuncgr.typ funcgr c;
   461         val ty = Logic.unvarifyT raw_ty;
   462         val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
   463           then raw_thms
   464           else map (CodeUnit.expand_eta 1) raw_thms;
   465       in
   466         trns
   467         |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
   468         ||>> exprgen_typ thy algbr funcgr ty
   469         ||>> fold_map (exprgen_eq thy algbr funcgr) thms
   470         |>> (fn ((vs, ty), eqs) => Fun ((vs, ty), eqs))
   471       end;
   472     val stmtgen = case Code.get_datatype_of_constr thy c
   473      of SOME tyco => stmt_datatypecons tyco
   474       | NONE => (case AxClass.class_of_param thy c
   475          of SOME class => stmt_classparam class
   476           | NONE => stmt_fun)
   477   in ensure_stmt stmtgen c' end
   478 and exprgen_term thy algbr funcgr thm (Const (c, ty)) =
   479       exprgen_app thy algbr funcgr thm ((c, ty), [])
   480   | exprgen_term thy algbr funcgr thm (Free (v, _)) =
   481       pair (IVar v)
   482   | exprgen_term thy algbr funcgr thm (Abs (abs as (_, ty, _))) =
   483       let
   484         val (v, t) = Syntax.variant_abs abs;
   485       in
   486         exprgen_typ thy algbr funcgr ty
   487         ##>> exprgen_term thy algbr funcgr thm t
   488         #>> (fn (ty, t) => (v, ty) `|-> t)
   489       end
   490   | exprgen_term thy algbr funcgr thm (t as _ $ _) =
   491       case strip_comb t
   492        of (Const (c, ty), ts) =>
   493             exprgen_app thy algbr funcgr thm ((c, ty), ts)
   494         | (t', ts) =>
   495             exprgen_term thy algbr funcgr thm t'
   496             ##>> fold_map (exprgen_term thy algbr funcgr thm) ts
   497             #>> (fn (t, ts) => t `$$ ts)
   498 and exprgen_const thy algbr funcgr thm (c, ty) =
   499   let
   500     val tys = Sign.const_typargs thy (c, ty);
   501     val sorts = (map snd o fst o CodeFuncgr.typ funcgr) c;
   502     val tys_args = (fst o Term.strip_type) ty;
   503   in
   504     ensure_const thy algbr funcgr c
   505     ##>> fold_map (exprgen_dicts thy algbr funcgr thm) (tys ~~ sorts)
   506     ##>> fold_map (exprgen_typ thy algbr funcgr) tys_args
   507     #>> (fn ((c, iss), tys) => IConst (c, (iss, tys)))
   508   end
   509 and exprgen_app_default thy algbr funcgr thm (c_ty, ts) =
   510   exprgen_const thy algbr funcgr thm c_ty
   511   ##>> fold_map (exprgen_term thy algbr funcgr thm) ts
   512   #>> (fn (t, ts) => t `$$ ts)
   513 and exprgen_case thy algbr funcgr thm n cases (app as ((c, ty), ts)) =
   514   let
   515     val (tys, _) =
   516       (chop (1 + (if null cases then 1 else length cases)) o fst o strip_type) ty;
   517     val dt = nth ts n;
   518     val dty = nth tys n;
   519     fun is_undefined (Const (c, _)) = Code.is_undefined thy c
   520       | is_undefined _ = false;
   521     fun mk_case (co, n) t =
   522       let
   523         val (vs, body) = Term.strip_abs_eta n t;
   524         val selector = list_comb (Const (co, map snd vs ---> dty), map Free vs);
   525       in if is_undefined body then NONE else SOME (selector, body) end;
   526     fun mk_ds [] =
   527           let
   528             val ([v_ty], body) = Term.strip_abs_eta 1 (the_single (nth_drop n ts))
   529           in [(Free v_ty, body)] end
   530       | mk_ds cases = map_filter (uncurry mk_case)
   531           (AList.make (CodeUnit.no_args thy) cases ~~ nth_drop n ts);
   532   in
   533     exprgen_term thy algbr funcgr thm dt
   534     ##>> exprgen_typ thy algbr funcgr dty
   535     ##>> fold_map (fn (pat, body) => exprgen_term thy algbr funcgr thm pat
   536           ##>> exprgen_term thy algbr funcgr thm body) (mk_ds cases)
   537     ##>> exprgen_app_default thy algbr funcgr thm app
   538     #>> (fn (((dt, dty), ds), t0) => ICase (((dt, dty), ds), t0))
   539   end
   540 and exprgen_app thy algbr funcgr thm ((c, ty), ts) = case Code.get_case_data thy c
   541  of SOME (n, cases) => let val i = 1 + (if null cases then 1 else length cases) in
   542       if length ts < i then
   543         let
   544           val k = length ts;
   545           val tys = (curry Library.take (i - k) o curry Library.drop k o fst o strip_type) ty;
   546           val ctxt = (fold o fold_aterms)
   547             (fn Free (v, _) => Name.declare v | _ => I) ts Name.context;
   548           val vs = Name.names ctxt "a" tys;
   549         in
   550           fold_map (exprgen_typ thy algbr funcgr) tys
   551           ##>> exprgen_case thy algbr funcgr thm n cases ((c, ty), ts @ map Free vs)
   552           #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
   553         end
   554       else if length ts > i then
   555         exprgen_case thy algbr funcgr thm n cases ((c, ty), Library.take (i, ts))
   556         ##>> fold_map (exprgen_term thy algbr funcgr thm) (Library.drop (i, ts))
   557         #>> (fn (t, ts) => t `$$ ts)
   558       else
   559         exprgen_case thy algbr funcgr thm n cases ((c, ty), ts)
   560       end
   561   | NONE => exprgen_app_default thy algbr funcgr thm ((c, ty), ts);
   562 
   563 
   564 (** generated programs **)
   565 
   566 (* store *)
   567 
   568 structure Program = CodeDataFun
   569 (
   570   type T = program;
   571   val empty = Graph.empty;
   572   fun purge thy cs program =
   573     let
   574       val cs_exisiting =
   575         map_filter (CodeName.const_rev thy) (Graph.keys program);
   576       val dels = (Graph.all_preds program
   577           o map (CodeName.const thy)
   578           o filter (member (op =) cs_exisiting)
   579         ) cs;
   580     in Graph.del_nodes dels program end;
   581 );
   582 
   583 val cached_program = Program.get;
   584 
   585 fun transact f program =
   586   (NONE, program)
   587   |> f
   588   |-> (fn x => fn (_, program) => (x, program));
   589 
   590 fun generate thy funcgr f x =
   591   Program.change_yield thy (transact (f thy (Code.operational_algebra thy) funcgr x));
   592 
   593 
   594 (* program generation *)
   595 
   596 fun consts_program thy cs =
   597   let
   598     fun project_consts cs program =
   599       let
   600         val cs_all = Graph.all_succs program cs;
   601       in (cs, Graph.subgraph (member (op =) cs_all) program) end;
   602     fun generate_consts thy algebra funcgr =
   603       fold_map (ensure_const thy algebra funcgr);
   604   in
   605     generate thy (CodeFuncgr.make thy cs) generate_consts cs
   606     |-> project_consts
   607   end;
   608 
   609 
   610 (* value evaluation *)
   611 
   612 fun ensure_value thy algbr funcgr t = 
   613   let
   614     val ty = fastype_of t;
   615     val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
   616       o dest_TFree))) t [];
   617     val stmt_value =
   618       fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
   619       ##>> exprgen_typ thy algbr funcgr ty
   620       ##>> exprgen_term thy algbr funcgr NONE t
   621       #>> (fn ((vs, ty), t) => Fun ((vs, ty), [(([], t), Drule.dummy_thm)]));
   622     fun term_value (dep, program1) =
   623       let
   624         val Fun ((vs, ty), [(([], t), _)]) =
   625           Graph.get_node program1 CodeName.value_name;
   626         val deps = Graph.imm_succs program1 CodeName.value_name;
   627         val program2 = Graph.del_nodes [CodeName.value_name] program1;
   628         val deps_all = Graph.all_succs program2 deps;
   629         val program3 = Graph.subgraph (member (op =) deps_all) program2;
   630       in ((program3, (((vs, ty), t), deps)), (dep, program2)) end;
   631   in
   632     ensure_stmt stmt_value CodeName.value_name
   633     #> snd
   634     #> term_value
   635   end;
   636 
   637 fun eval eval_kind thy evaluator =
   638   let
   639     fun evaluator'' evaluator''' funcgr t =
   640       let
   641         val ((program, (vs_ty_t, deps)), _) = generate thy funcgr ensure_value t;
   642       in evaluator''' program vs_ty_t deps end;
   643     fun evaluator' t =
   644       let
   645         val (t', evaluator''') = evaluator t;
   646       in (t', evaluator'' evaluator''') end;
   647   in eval_kind thy evaluator' end
   648 
   649 fun eval_conv thy = eval CodeFuncgr.eval_conv thy;
   650 fun eval_term thy = eval CodeFuncgr.eval_term thy;
   651 
   652 end; (*struct*)
   653 
   654 
   655 structure BasicCodeThingol: BASIC_CODE_THINGOL = CodeThingol;