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@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@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@24219: datatype def = haftmann@24219: Bot 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@24219: | Class of (class * string) list * (vname * (string * itype) list) haftmann@24219: | Classop of class haftmann@24219: | Classrel of class * 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: type code = def Graph.T; haftmann@24219: type transact; haftmann@24219: val empty_code: code; haftmann@24219: val merge_code: code * code -> code; haftmann@24219: val project_code: bool (*delete empty funs*) haftmann@24219: -> string list (*hidden*) -> string list option (*selected*) haftmann@24219: -> code -> code; haftmann@24219: val empty_funs: code -> string list; haftmann@24219: val is_cons: code -> string -> bool; haftmann@24283: val add_eval_def: string (*bind name*) * (iterm * itype) -> code -> code; haftmann@24219: haftmann@24252: val ensure_def: (string -> string) -> (transact -> def * transact) -> string haftmann@24219: -> string -> transact -> transact; haftmann@24219: val start_transact: (transact -> 'a * transact) -> code -> 'a * code; 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@24219: const names (general) c haftmann@24219: constructor names co haftmann@24219: class operation names clsop (op) haftmann@24219: arbitrary name s haftmann@24219: haftmann@24219: v, c, co, clsop 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@24219: haftmann@24219: (** definitions, transactions **) haftmann@24219: haftmann@24219: type typscheme = (vname * sort) list * itype; haftmann@24219: datatype def = haftmann@24219: Bot 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@24219: | Class of (class * string) list * (vname * (string * itype) list) haftmann@24219: | Classop of class haftmann@24219: | Classrel of class * 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@24219: type code = def Graph.T; haftmann@24219: haftmann@24219: haftmann@24219: (* abstract code *) haftmann@24219: haftmann@24219: val empty_code = Graph.empty : code; (*read: "depends on"*) haftmann@24219: haftmann@24219: fun ensure_bot name = Graph.default_node (name, Bot); haftmann@24219: haftmann@24219: fun add_def_incr (name, Bot) code = haftmann@24219: (case the_default Bot (try (Graph.get_node code) name) haftmann@24219: of Bot => error "Attempted to add Bot to code" haftmann@24219: | _ => code) haftmann@24219: | add_def_incr (name, def) code = haftmann@24219: (case try (Graph.get_node code) name haftmann@24219: of NONE => Graph.new_node (name, def) code haftmann@24219: | SOME Bot => Graph.map_node name (K def) code haftmann@24219: | SOME _ => error ("Tried to overwrite definition " ^ quote name)); haftmann@24219: haftmann@24219: fun add_dep (dep as (name1, name2)) = haftmann@24219: if name1 = name2 then I else Graph.add_edge dep; haftmann@24219: haftmann@24219: val merge_code : code * code -> code = Graph.merge (K true); haftmann@24219: haftmann@24219: fun project_code delete_empty_funs hidden raw_selected code = haftmann@24219: let haftmann@24219: fun is_empty_fun name = case Graph.get_node code name haftmann@24381: of Fun (_, []) => true haftmann@24219: | _ => false; haftmann@24219: val names = subtract (op =) hidden (Graph.keys code); haftmann@24219: val deleted = Graph.all_preds code (filter is_empty_fun names); haftmann@24219: val selected = case raw_selected haftmann@24219: of NONE => names |> subtract (op =) deleted haftmann@24219: | SOME sel => sel haftmann@24219: |> delete_empty_funs ? subtract (op =) deleted haftmann@24219: |> subtract (op =) hidden haftmann@24219: |> Graph.all_succs code haftmann@24219: |> delete_empty_funs ? subtract (op =) deleted haftmann@24219: |> subtract (op =) hidden; haftmann@24219: in haftmann@24219: code haftmann@24219: |> Graph.subgraph (member (op =) selected) haftmann@24219: end; haftmann@24219: haftmann@24219: fun empty_funs code = haftmann@24381: Graph.fold (fn (name, (Fun (_, []), _)) => cons name haftmann@24219: | _ => I) code []; haftmann@24219: haftmann@24219: fun is_cons code name = case Graph.get_node code name haftmann@24219: of Datatypecons _ => true haftmann@24219: | _ => false; haftmann@24219: haftmann@24219: fun check_samemodule names = haftmann@24219: fold (fn name => haftmann@24219: let haftmann@24219: val module_name = (NameSpace.qualifier o NameSpace.qualifier) name haftmann@24219: in haftmann@24219: fn NONE => SOME module_name haftmann@24219: | SOME module_name' => if module_name = module_name' then SOME module_name haftmann@24219: else error ("Inconsistent name prefix for simultanous names: " ^ commas_quote names) haftmann@24219: end haftmann@24219: ) names NONE; haftmann@24219: haftmann@24219: fun check_funeqs eqs = haftmann@24591: (fold (fn ((pats, _), _) => haftmann@24219: let haftmann@24219: val l = length pats haftmann@24219: in haftmann@24219: fn NONE => SOME l haftmann@24219: | SOME l' => if l = l' then SOME l haftmann@24219: else error "Function definition with different number of arguments" haftmann@24219: end haftmann@24219: ) eqs NONE; eqs); haftmann@24219: haftmann@24219: fun check_prep_def code Bot = haftmann@24219: Bot haftmann@24381: | check_prep_def code (Fun (d, eqs)) = haftmann@24381: Fun (d, check_funeqs eqs) haftmann@24219: | check_prep_def code (d as Datatype _) = haftmann@24219: d haftmann@24219: | check_prep_def code (Datatypecons dtco) = haftmann@24219: error "Attempted to add bare term constructor" haftmann@24219: | check_prep_def code (d as Class _) = haftmann@24219: d haftmann@24219: | check_prep_def code (Classop _) = haftmann@24219: error "Attempted to add bare class operation" haftmann@24219: | check_prep_def code (Classrel _) = haftmann@24219: error "Attempted to add bare class relation" haftmann@24219: | check_prep_def code (d as Classinst ((class, (tyco, arity)), (_, inst_classops))) = haftmann@24219: let haftmann@24219: val Class (_, (_, classops)) = Graph.get_node code class; haftmann@24219: val _ = if length inst_classops > length classops haftmann@24219: then error "Too many class operations given" haftmann@24219: else (); haftmann@24219: fun check_classop (f, _) = haftmann@24591: if AList.defined (op =) (map fst inst_classops) f haftmann@24219: then () else error ("Missing definition for class operation " ^ quote f); haftmann@24219: val _ = map check_classop classops; haftmann@24219: in d end; haftmann@24219: haftmann@24219: fun postprocess_def (name, Datatype (_, constrs)) = haftmann@24219: tap (fn _ => check_samemodule (name :: map fst constrs)) haftmann@24219: #> fold (fn (co, _) => haftmann@24219: add_def_incr (co, Datatypecons name) haftmann@24219: #> add_dep (co, name) haftmann@24219: #> add_dep (name, co) haftmann@24219: ) constrs haftmann@24219: | postprocess_def (name, Class (classrels, (_, classops))) = haftmann@24219: tap (fn _ => check_samemodule (name :: map fst classops @ map snd classrels)) haftmann@24219: #> fold (fn (f, _) => haftmann@24219: add_def_incr (f, Classop name) haftmann@24219: #> add_dep (f, name) haftmann@24219: #> add_dep (name, f) haftmann@24219: ) classops haftmann@24219: #> fold (fn (superclass, classrel) => haftmann@24219: add_def_incr (classrel, Classrel (name, superclass)) haftmann@24219: #> add_dep (classrel, name) haftmann@24219: #> add_dep (name, classrel) haftmann@24219: ) classrels haftmann@24219: | postprocess_def _ = haftmann@24219: I; haftmann@24219: haftmann@24219: haftmann@24219: (* transaction protocol *) haftmann@24219: haftmann@24283: type transact = Graph.key option * code; haftmann@24283: haftmann@24219: fun ensure_def labelled_name defgen msg name (dep, code) = haftmann@24219: let haftmann@24219: val msg' = (case dep haftmann@24219: of NONE => msg haftmann@24219: | SOME dep => msg ^ ", required for " ^ labelled_name dep); haftmann@24219: fun add_dp NONE = I haftmann@24219: | add_dp (SOME dep) = add_dep (dep, name); haftmann@24219: fun prep_def def code = haftmann@24219: (check_prep_def code def, code); haftmann@24219: fun add_def false = haftmann@24219: ensure_bot name haftmann@24219: #> add_dp dep haftmann@24252: #> curry defgen (SOME name) haftmann@24252: ##> snd haftmann@24219: #-> (fn def => prep_def def) haftmann@24219: #-> (fn def => add_def_incr (name, def) haftmann@24219: #> postprocess_def (name, def)) haftmann@24219: | add_def true = haftmann@24219: add_dp dep; haftmann@24219: in haftmann@24219: code haftmann@24219: |> add_def (can (Graph.get_node code) name) haftmann@24219: |> pair dep haftmann@24219: end; haftmann@24219: haftmann@24219: fun start_transact f code = haftmann@24252: (NONE, code) haftmann@24252: |> f haftmann@24252: |-> (fn x => fn (_, code) => (x, code)); haftmann@24219: haftmann@24283: fun add_eval_def (name, (t, ty)) code = haftmann@24219: code haftmann@24591: |> Graph.new_node (name, Fun (([], ty), [(([], t), Drule.dummy_thm)])) haftmann@24219: |> fold (curry Graph.add_edge name) (Graph.keys code); haftmann@24219: haftmann@24219: end; (*struct*) haftmann@24219: haftmann@24219: haftmann@24219: structure BasicCodeThingol: BASIC_CODE_THINGOL = CodeThingol;