wneuper/isa: src/Tools/code/code_thingol.ML@cacc5744be75

     1 (*  Title:      Tools/code/code_thingol.ML

     2     ID:         $Id$

     3     Author:     Florian Haftmann, TU Muenchen

     5 Intermediate language ("Thin-gol") representing executable code.

     6 *)

     8 infix 8 `%%;

     9 infixr 6 `->;

    10 infixr 6 `-->;

    11 infix 4 `$;

    12 infix 4 `$$;

    13 infixr 3 `|->;

    14 infixr 3 `|-->;

    16 signature BASIC_CODE_THINGOL =

    17 sig

    18   type vname = string;

    19   datatype dict =

    20       DictConst of string * dict list list

    21     | DictVar of string list * (vname * (int * int));

    22   datatype itype =

    23       `%% of string * itype list

    24     | ITyVar of vname;

    25   type const = string * (dict list list * itype list (*types of arguments*))

    26   datatype iterm =

    27       IConst of const

    28     | IVar of vname

    29     | `$ of iterm * iterm

    30     | `|-> of (vname * itype) * iterm

    31     | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;

    32         (*((term, type), [(selector pattern, body term )]), primitive term)*)

    33   val `-> : itype * itype -> itype;

    34   val `--> : itype list * itype -> itype;

    35   val `$$ : iterm * iterm list -> iterm;

    36   val `|--> : (vname * itype) list * iterm -> iterm;

    37   type typscheme = (vname * sort) list * itype;

    38 end;

    40 signature CODE_THINGOL =

    41 sig

    42   include BASIC_CODE_THINGOL;

    43   val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list;

    44   val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a;

    45   val unfold_fun: itype -> itype list * itype;

    46   val unfold_app: iterm -> iterm * iterm list;

    47   val split_abs: iterm -> (((vname * iterm option) * itype) * iterm) option;

    48   val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm;

    49   val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option;

    50   val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm;

    51   val unfold_const_app: iterm ->

    52     ((string * (dict list list * itype list)) * iterm list) option;

    53   val collapse_let: ((vname * itype) * iterm) * iterm

    54     -> (iterm * itype) * (iterm * iterm) list;

    55   val eta_expand: (string * (dict list list * itype list)) * iterm list -> int -> iterm;

    56   val contains_dictvar: iterm -> bool;

    57   val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;

    58   val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;

    59   val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;

    61   datatype def =

    62       Bot

    63     | Fun of typscheme * ((iterm list * iterm) * thm) list

    64     | Datatype of (vname * sort) list * (string * itype list) list

    65     | Datatypecons of string

    66     | Class of vname * ((class * string) list * (string * itype) list)

    67     | Classrel of class * class

    68     | Classparam of class

    69     | Classinst of (class * (string * (vname * sort) list))

    70           * ((class * (string * (string * dict list list))) list

    71         * ((string * const) * thm) list);

    72   type code = def Graph.T;

    73   type transact;

    74   val empty_code: code;

    75   val merge_code: code * code -> code;

    76   val project_code: bool (*delete empty funs*)

    77     -> string list (*hidden*) -> string list option (*selected*)

    78     -> code -> code;

    79   val empty_funs: code -> string list;

    80   val is_cons: code -> string -> bool;

    81   val add_eval_def: string (*bind name*) * (iterm * itype) -> code -> code;

    83   val ensure_def: (string -> string) -> (transact -> def * transact) -> string

    84     -> transact -> transact;

    85   val start_transact: (transact -> 'a * transact) -> code -> 'a * code;

    86 end;

    88 structure CodeThingol: CODE_THINGOL =

    89 struct

    91 (** auxiliary **)

    93 fun unfoldl dest x =

    94   case dest x

    95    of NONE => (x, [])

    96     | SOME (x1, x2) =>

    97         let val (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end;

    99 fun unfoldr dest x =

   100   case dest x

   101    of NONE => ([], x)

   102     | SOME (x1, x2) =>

   103         let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;

   106 (** language core - types, pattern, expressions **)

   108 (* language representation *)

   110 type vname = string;

   112 datatype dict =

   113     DictConst of string * dict list list

   114   | DictVar of string list * (vname * (int * int));

   116 datatype itype =

   117     `%% of string * itype list

   118   | ITyVar of vname;

   120 type const = string * (dict list list * itype list (*types of arguments*))

   122 datatype iterm =

   123     IConst of const

   124   | IVar of vname

   125   | `$ of iterm * iterm

   126   | `|-> of (vname * itype) * iterm

   127   | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;

   128     (*see also signature*)

   130 (*

   131   variable naming conventions

   133   bare names:

   134     variable names          v

   135     class names             class

   136     type constructor names  tyco

   137     datatype names          dtco

   138     const names (general)   c (const)

   139     constructor names       co

   140     class parameter names   classparam

   141     arbitrary name          s

   143     v, c, co, classparam also annotated with types etc.

   145   constructs:

   146     sort                    sort

   147     type parameters         vs

   148     type                    ty

   149     type schemes            tysm

   150     term                    t

   151     (term as pattern)       p

   152     instance (class, tyco)  inst

   153  *)

   155 fun ty1 `-> ty2 = "fun" `%% [ty1, ty2];

   156 val op `--> = Library.foldr (op `->);

   157 val op `$$ = Library.foldl (op `$);

   158 val op `|--> = Library.foldr (op `|->);

   160 val unfold_fun = unfoldr

   161   (fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2)

   162     | _ => NONE);

   164 val unfold_app = unfoldl

   165   (fn op `$ t => SOME t

   166     | _ => NONE);

   168 val split_abs =

   169   (fn (v, ty) `|-> (t as ICase (((IVar w, _), [(p, t')]), _)) =>

   170         if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t)

   171     | (v, ty) `|-> t => SOME (((v, NONE), ty), t)

   172     | _ => NONE);

   174 val unfold_abs = unfoldr split_abs;

   176 val split_let =

   177   (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)

   178     | _ => NONE);

   180 val unfold_let = unfoldr split_let;

   182 fun unfold_const_app t =

   183  case unfold_app t

   184   of (IConst c, ts) => SOME (c, ts)

   185    | _ => NONE;

   187 fun fold_aiterms f (t as IConst _) = f t

   188   | fold_aiterms f (t as IVar _) = f t

   189   | fold_aiterms f (t1 `$ t2) = fold_aiterms f t1 #> fold_aiterms f t2

   190   | fold_aiterms f (t as _ `|-> t') = f t #> fold_aiterms f t'

   191   | fold_aiterms f (ICase (_, t)) = fold_aiterms f t;

   193 fun fold_constnames f =

   194   let

   195     fun add (IConst (c, _)) = f c

   196       | add _ = I;

   197   in fold_aiterms add end;

   199 fun fold_varnames f =

   200   let

   201     fun add (IVar v) = f v

   202       | add ((v, _) `|-> _) = f v

   203       | add _ = I;

   204   in fold_aiterms add end;

   206 fun fold_unbound_varnames f =

   207   let

   208     fun add _ (IConst _) = I

   209       | add vs (IVar v) = if not (member (op =) vs v) then f v else I

   210       | add vs (t1 `$ t2) = add vs t1 #> add vs t2

   211       | add vs ((v, _) `|-> t) = add (insert (op =) v vs) t

   212       | add vs (ICase (_, t)) = add vs t;

   213   in add [] end;

   215 fun collapse_let (((v, ty), se), be as ICase (((IVar w, _), ds), _)) =

   216       let

   217         fun exists_v t = fold_unbound_varnames (fn w => fn b =>

   218           b orelse v = w) t false;

   219       in if v = w andalso forall (fn (t1, t2) =>

   220         exists_v t1 orelse not (exists_v t2)) ds

   221         then ((se, ty), ds)

   222         else ((se, ty), [(IVar v, be)])

   223       end

   224   | collapse_let (((v, ty), se), be) =

   225       ((se, ty), [(IVar v, be)])

   227 fun eta_expand (c as (_, (_, tys)), ts) k =

   228   let

   229     val j = length ts;

   230     val l = k - j;

   231     val ctxt = (fold o fold_varnames) Name.declare ts Name.context;

   232     val vs_tys = Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys);

   233   in vs_tys `|--> IConst c `$$ ts @ map (fn (v, _) => IVar v) vs_tys end;

   235 fun contains_dictvar t =

   236   let

   237     fun contains (DictConst (_, dss)) = (fold o fold) contains dss

   238       | contains (DictVar _) = K true;

   239   in

   240     fold_aiterms

   241       (fn IConst (_, (dss, _)) => (fold o fold) contains dss | _ => I) t false

   242   end;

   245 (** definitions, transactions **)

   247 type typscheme = (vname * sort) list * itype;

   248 datatype def =

   249     Bot

   250   | Fun of typscheme * ((iterm list * iterm) * thm) list

   251   | Datatype of (vname * sort) list * (string * itype list) list

   252   | Datatypecons of string

   253   | Class of vname * ((class * string) list * (string * itype) list)

   254   | Classrel of class * class

   255   | Classparam of class

   256   | Classinst of (class * (string * (vname * sort) list))

   257         * ((class * (string * (string * dict list list))) list

   258       * ((string * const) * thm) list);

   260 type code = def Graph.T;

   263 (* abstract code *)

   265 val empty_code = Graph.empty : code; (*read: "depends on"*)

   267 fun ensure_bot name = Graph.default_node (name, Bot);

   269 fun add_def_incr (name, Bot) code =

   270       (case the_default Bot (try (Graph.get_node code) name)

   271        of Bot => error "Attempted to add Bot to code"

   272         | _ => code)

   273   | add_def_incr (name, def) code =

   274       (case try (Graph.get_node code) name

   275        of NONE => Graph.new_node (name, def) code

   276         | SOME Bot => Graph.map_node name (K def) code

   277         | SOME _ => error ("Tried to overwrite definition " ^ quote name));

   279 fun add_dep (NONE, _) = I

   280   | add_dep (SOME name1, name2) =

   281       if name1 = name2 then I else Graph.add_edge (name1, name2);

   283 val merge_code : code * code -> code = Graph.merge (K true);

   285 fun project_code delete_empty_funs hidden raw_selected code =

   286   let

   287     fun is_empty_fun name = case Graph.get_node code name

   288      of Fun (_, []) => true

   289       | _ => false;

   290     val names = subtract (op =) hidden (Graph.keys code);

   291     val deleted = Graph.all_preds code (filter is_empty_fun names);

   292     val selected = case raw_selected

   293      of NONE => names |> subtract (op =) deleted

   294       | SOME sel => sel

   295           |> delete_empty_funs ? subtract (op =) deleted

   296           |> subtract (op =) hidden

   297           |> Graph.all_succs code

   298           |> delete_empty_funs ? subtract (op =) deleted

   299           |> subtract (op =) hidden;

   300   in

   301     code

   302     |> Graph.subgraph (member (op =) selected)

   303   end;

   305 fun empty_funs code =

   306   Graph.fold (fn (name, (Fun (_, []), _)) => cons name

   307                | _ => I) code [];

   309 fun is_cons code name = case Graph.get_node code name

   310  of Datatypecons _ => true

   311   | _ => false;

   314 (* transaction protocol *)

   316 type transact = Graph.key option * code;

   318 fun ensure_def labelled_name defgen name (dep, code) =

   319   let

   320     fun add_def false =

   321           ensure_bot name

   322           #> add_dep (dep, name)

   323           #> curry defgen (SOME name)

   324           ##> snd

   325           #-> (fn def => add_def_incr (name, def))

   326       | add_def true =

   327           add_dep (dep, name);

   328   in

   329     code

   330     |> add_def (can (Graph.get_node code) name)

   331     |> pair dep

   332   end;

   334 fun start_transact f code =

   335   (NONE, code)

   336   |> f

   337   |-> (fn x => fn (_, code) => (x, code));

   339 fun add_eval_def (name, (t, ty)) code =

   340   code

   341   |> Graph.new_node (name, Fun (([], ty), [(([], t), Drule.dummy_thm)]))

   342   |> fold (curry Graph.add_edge name) (Graph.keys code);

   344 end; (*struct*)

   347 structure BasicCodeThingol: BASIC_CODE_THINGOL = CodeThingol;

author	haftmann
	Thu, 04 Oct 2007 19:41:51 +0200
changeset 24837	cacc5744be75
parent 24811	3bf788a0c49a
child 24918	22013215eece
permissions	-rw-r--r--