src/Tools/code/code_thingol.ML

added explicit theorems

(*  Title:      Tools/code/code_thingol.ML
    ID:         $Id$
    Author:     Florian Haftmann, TU Muenchen

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

infix 8 `%%;
infixr 6 `->;
infixr 6 `-->;
infix 4 `$;
infix 4 `$$;
infixr 3 `|->;
infixr 3 `|-->;

signature BASIC_CODE_THINGOL =
sig
  type vname = string;
  datatype dict =
      DictConst of string * dict list list
    | DictVar of string list * (vname * (int * int));
  datatype itype =
      `%% of string * itype list
    | ITyVar of vname;
  type const = string * (dict list list * itype list (*types of arguments*))
  datatype iterm =
      IConst of const
    | IVar of vname
    | `$ of iterm * iterm
    | `|-> of (vname * itype) * iterm
    | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
        (*((term, type), [(selector pattern, body term )]), primitive term)*)
  val `-> : itype * itype -> itype;
  val `--> : itype list * itype -> itype;
  val `$$ : iterm * iterm list -> iterm;
  val `|--> : (vname * itype) list * iterm -> iterm;
  type typscheme = (vname * sort) list * itype;
end;

signature CODE_THINGOL =
sig
  include BASIC_CODE_THINGOL;
  val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list;
  val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a;
  val unfold_fun: itype -> itype list * itype;
  val unfold_app: iterm -> iterm * iterm list;
  val split_abs: iterm -> (((vname * iterm option) * itype) * iterm) option;
  val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm;
  val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option;
  val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm;
  val unfold_const_app: iterm ->
    ((string * (dict list list * itype list)) * iterm list) option;
  val collapse_let: ((vname * itype) * iterm) * iterm
    -> (iterm * itype) * (iterm * iterm) list;
  val eta_expand: (string * (dict list list * itype list)) * iterm list -> int -> iterm;
  val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
  val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
  val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;

  datatype def =
      Bot
    | Fun of typscheme * ((iterm list * iterm) * thm) list
    | Datatype of (vname * sort) list * (string * itype list) list
    | Datatypecons of string
    | Class of (class * string) list * (vname * (string * itype) list)
    | Classop of class
    | Classrel of class * class
    | 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;
  val empty_code: code;
  val merge_code: code * code -> code;
  val project_code: bool (*delete empty funs*)
    -> string list (*hidden*) -> string list option (*selected*)
    -> 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
    -> string -> transact -> transact;
  val start_transact: (transact -> 'a * transact) -> code -> 'a * code;
end;

structure CodeThingol: CODE_THINGOL =
struct

(** auxiliary **)

fun unfoldl dest x =
  case dest x
   of NONE => (x, [])
    | SOME (x1, x2) =>
        let val (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end;

fun unfoldr dest x =
  case dest x
   of NONE => ([], x)
    | SOME (x1, x2) =>
        let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;


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

(* language representation *)

type vname = string;

datatype dict =
    DictConst of string * dict list list
  | DictVar of string list * (vname * (int * int));

datatype itype =
    `%% of string * itype list
  | ITyVar of vname;

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

datatype iterm =
    IConst of const
  | IVar of vname
  | `$ of iterm * iterm
  | `|-> of (vname * itype) * iterm
  | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
    (*see also signature*)

(*
  variable naming conventions

  bare names:
    variable names          v
    class names             class
    type constructor names  tyco
    datatype names          dtco
    const names (general)   c
    constructor names       co
    class operation names   clsop (op)
    arbitrary name          s

    v, c, co, clsop also annotated with types etc.

  constructs:
    sort                    sort
    type parameters         vs
    type                    ty
    type schemes            tysm
    term                    t
    (term as pattern)       p
    instance (class, tyco)  inst
 *)

fun ty1 `-> ty2 = "fun" `%% [ty1, ty2];
val op `--> = Library.foldr (op `->);
val op `$$ = Library.foldl (op `$);
val op `|--> = Library.foldr (op `|->);

val unfold_fun = unfoldr
  (fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2)
    | _ => NONE);

val unfold_app = unfoldl
  (fn op `$ t => SOME t
    | _ => NONE);

val split_abs =
  (fn (v, ty) `|-> (t as ICase (((IVar w, _), [(p, t')]), _)) =>
        if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t)
    | (v, ty) `|-> t => SOME (((v, NONE), ty), t)
    | _ => NONE);

val unfold_abs = unfoldr split_abs;

val split_let = 
  (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
    | _ => NONE);

val unfold_let = unfoldr split_let;

fun unfold_const_app t =
 case unfold_app t
  of (IConst c, ts) => SOME (c, ts)
   | _ => NONE;

fun fold_aiterms f (t as IConst _) = f t
  | fold_aiterms f (t as IVar _) = f t
  | fold_aiterms f (t1 `$ t2) = fold_aiterms f t1 #> fold_aiterms f t2
  | fold_aiterms f (t as _ `|-> t') = f t #> fold_aiterms f t'
  | fold_aiterms f (ICase (_, t)) = fold_aiterms f t;

fun fold_constnames f =
  let
    fun add (IConst (c, _)) = f c
      | add _ = I;
  in fold_aiterms add end;

fun fold_varnames f =
  let
    fun add (IVar v) = f v
      | add ((v, _) `|-> _) = f v
      | add _ = I;
  in fold_aiterms add end;

fun fold_unbound_varnames f =
  let
    fun add _ (IConst _) = I
      | add vs (IVar v) = if not (member (op =) vs v) then f v else I
      | add vs (t1 `$ t2) = add vs t1 #> add vs t2
      | add vs ((v, _) `|-> t) = add (insert (op =) v vs) t
      | add vs (ICase (_, t)) = add vs t;
  in add [] end;

fun collapse_let (((v, ty), se), be as ICase (((IVar w, _), ds), _)) =
      let
        fun exists_v t = fold_unbound_varnames (fn w => fn b =>
          b orelse v = w) t false;
      in if v = w andalso forall (fn (t1, t2) =>
        exists_v t1 orelse not (exists_v t2)) ds
        then ((se, ty), ds)
        else ((se, ty), [(IVar v, be)])
      end
  | collapse_let (((v, ty), se), be) =
      ((se, ty), [(IVar v, be)])

fun eta_expand (c as (_, (_, tys)), ts) k =
  let
    val j = length ts;
    val l = k - j;
    val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
    val vs_tys = Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys);
  in vs_tys `|--> IConst c `$$ ts @ map (fn (v, _) => IVar v) vs_tys end;


(** definitions, transactions **)

type typscheme = (vname * sort) list * itype;
datatype def =
    Bot
  | Fun of typscheme * ((iterm list * iterm) * thm) list
  | Datatype of (vname * sort) list * (string * itype list) list
  | Datatypecons of string
  | Class of (class * string) list * (vname * (string * itype) list)
  | Classop of class
  | Classrel of class * class
  | Classinst of (class * (string * (vname * sort) list))
        * ((class * (string * (string * dict list list))) list
      * ((string * const) * thm) list);

type code = def Graph.T;


(* abstract code *)

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

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

fun add_def_incr (name, Bot) code =
      (case the_default Bot (try (Graph.get_node code) name)
       of Bot => error "Attempted to add Bot to code"
        | _ => code)
  | add_def_incr (name, def) code =
      (case try (Graph.get_node code) name
       of NONE => Graph.new_node (name, def) code
        | SOME Bot => Graph.map_node name (K def) code
        | SOME _ => error ("Tried to overwrite definition " ^ quote name));

fun add_dep (dep as (name1, name2)) =
  if name1 = name2 then I else Graph.add_edge dep;

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

fun project_code delete_empty_funs hidden raw_selected code =
  let
    fun is_empty_fun name = case Graph.get_node code name
     of Fun (_, []) => true
      | _ => false;
    val names = subtract (op =) hidden (Graph.keys code);
    val deleted = Graph.all_preds code (filter is_empty_fun names);
    val selected = case raw_selected
     of NONE => names |> subtract (op =) deleted 
      | SOME sel => sel
          |> delete_empty_funs ? subtract (op =) deleted
          |> subtract (op =) hidden
          |> Graph.all_succs code
          |> delete_empty_funs ? subtract (op =) deleted
          |> subtract (op =) hidden;
  in
    code
    |> Graph.subgraph (member (op =) selected)
  end;

fun empty_funs code =
  Graph.fold (fn (name, (Fun (_, []), _)) => cons name
               | _ => I) code [];

fun is_cons code name = case Graph.get_node code name
 of Datatypecons _ => true
  | _ => false;

fun check_samemodule names =
  fold (fn name =>
    let
      val module_name = (NameSpace.qualifier o NameSpace.qualifier) name
    in
     fn NONE => SOME module_name
      | SOME module_name' => if module_name = module_name' then SOME module_name
          else error ("Inconsistent name prefix for simultanous names: " ^ commas_quote names)
    end
  ) names NONE;

fun check_funeqs eqs =
  (fold (fn ((pats, _), _) =>
    let
      val l = length pats
    in
     fn NONE => SOME l
      | SOME l' => if l = l' then SOME l
          else error "Function definition with different number of arguments"
    end
  ) eqs NONE; eqs);

fun check_prep_def code Bot =
      Bot
  | check_prep_def code (Fun (d, eqs)) =
      Fun (d, check_funeqs eqs)
  | check_prep_def code (d as Datatype _) =
      d
  | check_prep_def code (Datatypecons dtco) =
      error "Attempted to add bare term constructor"
  | check_prep_def code (d as Class _) =
      d
  | check_prep_def code (Classop _) =
      error "Attempted to add bare class operation"
  | check_prep_def code (Classrel _) =
      error "Attempted to add bare class relation"
  | check_prep_def code (d as Classinst ((class, (tyco, arity)), (_, inst_classops))) =
      let
        val Class (_, (_, classops)) = Graph.get_node code class;
        val _ = if length inst_classops > length classops
          then error "Too many class operations given"
          else ();
        fun check_classop (f, _) =
          if AList.defined (op =) (map fst inst_classops) f
          then () else error ("Missing definition for class operation " ^ quote f);
        val _ = map check_classop classops;
      in d end;

fun postprocess_def (name, Datatype (_, constrs)) =
      tap (fn _ => check_samemodule (name :: map fst constrs))
      #> fold (fn (co, _) =>
        add_def_incr (co, Datatypecons name)
        #> add_dep (co, name)
        #> add_dep (name, co)
      ) constrs
  | postprocess_def (name, Class (classrels, (_, classops))) =
      tap (fn _ => check_samemodule (name :: map fst classops @ map snd classrels))
      #> fold (fn (f, _) =>
        add_def_incr (f, Classop name)
        #> add_dep (f, name)
        #> add_dep (name, f)
      ) classops
      #> fold (fn (superclass, classrel) =>
        add_def_incr (classrel, Classrel (name, superclass))
        #> add_dep (classrel, name)
        #> add_dep (name, classrel)
      ) classrels
  | postprocess_def _ =
      I;


(* transaction protocol *)

type transact = Graph.key option * code;

fun ensure_def labelled_name defgen msg name (dep, code) =
  let
    val msg' = (case dep
     of NONE => msg
      | SOME dep => msg ^ ", required for " ^ labelled_name dep);
    fun add_dp NONE = I
      | add_dp (SOME dep) = add_dep (dep, name);
    fun prep_def def code =
      (check_prep_def code def, code);
    fun add_def false =
          ensure_bot name
          #> add_dp dep
          #> curry defgen (SOME name)
          ##> snd
          #-> (fn def => prep_def def)
          #-> (fn def => add_def_incr (name, def)
          #> postprocess_def (name, def))
      | add_def true =
          add_dp dep;
  in
    code
    |> add_def (can (Graph.get_node code) name)
    |> pair dep
  end;

fun start_transact f code =
  (NONE, code)
  |> f
  |-> (fn x => fn (_, code) => (x, code));

fun add_eval_def (name, (t, ty)) code =
  code
  |> Graph.new_node (name, Fun (([], ty), [(([], t), Drule.dummy_thm)]))
  |> fold (curry Graph.add_edge name) (Graph.keys code);

end; (*struct*)


structure BasicCodeThingol: BASIC_CODE_THINGOL = CodeThingol;