# HG changeset patch
# User haftmann
# Date 1131982000 -3600
# Node ID 73ce773f12de286a9a81644008906702e432c64d
# Parent  45def66f86cbadfaf9ebbde95b1684782dcef81f
added module system

diff -r 45def66f86cb -r 73ce773f12de src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Mon Nov 14 15:23:33 2005 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML	Mon Nov 14 16:26:40 2005 +0100
@@ -40,6 +40,41 @@
   val instant_itype: vname * itype -> itype -> itype;
   val invent_tvar_names: itype list -> int -> vname list -> vname -> vname list;
   val invent_evar_names: iexpr list -> int -> vname list -> vname -> vname list;
+
+  datatype def =
+      Nop
+    | Fun of (ipat list * iexpr) list * (ClassPackage.sortcontext * itype)
+    | Typsyn of (vname * string list) list * itype
+    | Datatyp of (vname * string list) list * string list * string list
+    | Datatypcons of string * itype list
+    | Class of string list * string list * string list
+    | Classmember of string * vname * itype
+    | Classinst of string * (string * string list list) * (string * string) list;
+  type module;
+  type transact;
+  type 'dst transact_fin;
+  type ('src, 'dst) gen_codegen = 'src -> transact -> 'dst transact_fin;
+  type gen_defgen = string -> transact -> (def * string list) transact_fin;
+  val eq_def: def * def -> bool;
+  val pretty_def: def -> Pretty.T;
+  val pretty_module: module -> Pretty.T;  
+  val empty_module: module;
+  val get_def: module -> string -> def;
+  val map_defs: (def -> def) -> module -> module;
+  val add_deps: (string * def -> (string * string) list) -> module -> module;
+  val fold_defs: (string * def -> 'a -> 'a) -> module -> 'a -> 'a;
+  val fold_map_defs: (string * def -> 'a -> def * 'a) -> module -> 'a -> module * 'a;
+  val merge_module: module * module -> module;
+  val partof: string list -> module -> module;
+  val succeed: 'a -> transact -> 'a transact_fin;
+  val fail: string -> transact -> 'a transact_fin;
+  val gen_invoke: (string * ('src, 'dst) gen_codegen) list -> string
+    -> 'src -> transact -> 'dst * transact;
+  val gen_ensure_def: (string * gen_defgen) list -> string
+    -> string -> transact -> transact;
+
+  val debug_level : int ref;
+  val debug : int -> ('a -> string) -> 'a -> 'a;
 end;
 
 signature CODEGEN_THINGOL_OP =
@@ -56,8 +91,10 @@
 structure CodegenThingolOp: CODEGEN_THINGOL_OP =
 struct
 
+(** auxiliary **)
 
-(* auxiliary *)
+val debug_level = ref 0;
+fun debug d f x = (if d <= !debug_level then Output.debug (f x) else (); x);
 
 fun foldl' f (l, []) = the l
   | foldl' f (_, (r::rs)) =
@@ -85,6 +122,16 @@
     | SOME (x1, x2) =>
         let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
 
+fun get_prefix eq ([], ys) = ([], [], ys)
+  | get_prefix eq (xs, []) = ([], xs, [])
+  | get_prefix eq (xs as x::xs', ys as y::ys') =
+      if eq (x, y) then
+        let val (ps', xs'', ys'') = get_prefix eq (xs', ys')
+        in (x::ps', xs'', ys'') end
+      else ([], xs, ys);
+
+
+(** language core - types, pattern, expressions **)
 
 (* language representation *)
 
@@ -244,18 +291,341 @@
           fold (fn (p, e) => append (vars_of_ipats [p]) #> invent e) cs
   in Term.invent_names (fold invent es used) a n end;
 
+
+(** language module system - definitions, modules, transactions **)
+
+
+
+(* type definitions *)
+
+datatype def =
+    Nop
+  | Fun of (ipat list * iexpr) list * (ClassPackage.sortcontext * itype)
+  | Typsyn of (vname * string list) list * itype
+  | Datatyp of (vname * string list) list * string list * string list
+  | Datatypcons of string * itype list
+  | Class of string list * string list * string list
+  | Classmember of string * string * itype
+  | Classinst of string * (string * string list list) * (string * string) list;
+
+datatype node = Def of def | Module of node Graph.T;
+type module = node Graph.T;
+type transact = Graph.key list * module;
+datatype 'dst transact_res = Succeed of 'dst | Fail of string;
+type 'dst transact_fin = 'dst transact_res * transact;
+type ('src, 'dst) gen_codegen = 'src -> transact -> 'dst transact_fin;
+type gen_defgen = string -> transact -> (def * string list) transact_fin;
+exception FAIL of string;
+
+val eq_def = (op =);
+
+(* simple diagnosis *)
+
+fun pretty_def Nop =
+      Pretty.str "<NOP>"
+  | pretty_def (Fun (eqs, (_, ty))) =
+      Pretty.gen_list " |" "" "" (
+        map (fn (ps, body) =>
+          Pretty.block [
+            Pretty.gen_list "," "[" "]" (map pretty_ipat ps),
+            Pretty.str " |->",
+            Pretty.brk 1,
+            pretty_iexpr body,
+            Pretty.str "::",
+            pretty_itype ty
+          ]) eqs
+        )
+  | pretty_def (Typsyn (vs, ty)) =
+      Pretty.block [
+        Pretty.list "(" ")" (map (pretty_itype o IVarT) vs),
+        Pretty.str " |=> ",
+        pretty_itype ty
+      ]
+  | pretty_def (Datatyp (vs, cs, clss)) =
+      Pretty.block [
+        Pretty.list "(" ")" (map (pretty_itype o IVarT) vs),
+        Pretty.str " |=> ",
+        Pretty.gen_list " |" "" "" (map Pretty.str cs),
+        Pretty.str ", instance of ",
+        Pretty.gen_list "," "[" "]" (map Pretty.str clss)
+      ]
+  | pretty_def (Datatypcons (dtname, tys)) =
+      Pretty.block [
+        Pretty.str "cons ",
+        Pretty.gen_list " ->" "" "" (map pretty_itype tys @ [Pretty.str dtname])
+      ]
+  | pretty_def (Class (supcls, mems, insts)) =
+      Pretty.str "Class ..."
+  | pretty_def (Classmember (cls, v, ty)) =
+      Pretty.str "Classmember ..."
+  | pretty_def (Classinst (cls, insts, mems)) =
+      Pretty.str "Classinst ..."
+
+fun pretty_module modl =
+  let
+    fun pretty (name, Module modl) =
+          Pretty.block (
+            Pretty.str ("module " ^ name ^ " {")
+            :: Pretty.brk 1
+            :: Pretty.chunks (map pretty (AList.make (Graph.get_node modl)
+                 (Graph.strong_conn modl |> List.concat |> rev)))
+            :: Pretty.str "}" :: nil
+          )
+      | pretty (name, Def def) =
+          Pretty.block [Pretty.str name, Pretty.str " :=", Pretty.brk 1, pretty_def def]
+  in pretty ("//", Module modl) end;
+
+
+(* name handling *)
+
+fun dest_name name =
+  let
+    val name' = NameSpace.unpack name
+    val (name'', name_base) = split_last name'
+    val (modl, shallow) = split_last name''
+  in (modl, NameSpace.pack [shallow, name_base]) end
+  handle Empty => error ("not a qualified name: " ^ quote name);
+
+fun dest_modl (Module m) = m;
+fun dest_def (Def d) = d;
+
+
+(* modules *)
+
+val empty_module = Graph.empty; (*read: "depends on"*)
+
+fun get_def modl name =
+  case dest_name name
+   of (modlname, base) =>
+        let
+          fun get (Module node) [] =
+                (dest_def o Graph.get_node node) base
+            | get (Module node) (m::ms) =
+                get (Graph.get_node node m) ms
+        in get (Module modl) modlname end;
+
+fun add_def (name, def) =
+  let
+    val (modl, base) = dest_name name;
+    fun add [] =
+          Graph.new_node (base, Def def)
+      | add (m::ms) =
+          Graph.default_node (m, Module empty_module)
+          #> Graph.map_node m (Module o add ms o dest_modl)
+  in add modl end;
+
+fun map_def name f =
+  let
+    val (modl, base) = dest_name name;
+    fun mapp [] =
+          Graph.map_node base (Def o f o dest_def)
+      | mapp (m::ms) =
+          Graph.map_node m (Module o mapp ms o dest_modl)
+  in mapp modl end;
+
+fun add_dep (name1, name2) modl =
+  if name1 = name2 then modl
+  else
+    let
+      val m1 = dest_name name1 |> apsnd single |> (op @);
+      val m2 = dest_name name2 |> apsnd single |> (op @);
+      val (ms, r1, r2) = get_prefix (op =) (m1, m2);
+      val (ms, s1::r1, s2::r2) = get_prefix (op =) (m1, m2);
+      val add_edge =
+        if null r1 andalso null r2
+        then Graph.add_edge
+        else Graph.add_edge_acyclic
+      fun add [] node =
+            node
+            |> add_edge (s1, s2)
+        | add (m::ms) node =
+            node
+            |> Graph.map_node m (Module o add ms o dest_modl);
+    in add ms modl end;
+
+fun map_defs f =
+  let
+    fun mapp (Def def) =
+          (Def o f) def
+      | mapp (Module modl) =
+          (Module o Graph.map_nodes mapp) modl
+  in dest_modl o mapp o Module end;
+
+fun fold_defs f =
+  let
+    fun fol prfix (name, Def def) =
+          f (NameSpace.pack (prfix @ [name]), def)
+      | fol prfix (name, Module modl) =
+          Graph.fold_nodes (fol (prfix @ [name])) modl
+  in Graph.fold_nodes (fol []) end;
+
+fun add_deps f modl =
+  modl
+  |> fold add_dep ([] |> fold_defs (append o f) modl);
+
+fun fold_map_defs f =
+  let
+    fun foldmap prfix (name, Def def) =
+          apfst Def o f (NameSpace.pack (prfix @ [name]), def)
+      | foldmap prfix (name, Module modl) =
+          apfst Module o Graph.fold_map_nodes (foldmap (prfix @ [name])) modl
+  in Graph.fold_map_nodes (foldmap []) end;
+
+fun merge_module modl12 =
+  let
+    fun join_module (Module m1, Module m2) =
+          (SOME o Module) (merge_module (m1, m2))
+      | join_module (Def d1, Def d2) =
+          if eq_def (d1, d2) then (SOME o Def) d1 else NONE
+      | join_module _ =
+          NONE
+  in Graph.join (K join_module) modl12 end;
+
+fun partof names modl =
+      let
+        datatype pathnode = PN of (string list * (string * pathnode) list);
+        fun mk_path ([], base) (PN (defs, modls)) =
+              PN (base :: defs, modls)
+          | mk_path (n::ns, base) (PN (defs, modls)) =
+              modls
+              |> AList.default (op =) (n, PN ([], []))
+              |> AList.map_entry (op =) n (mk_path (ns, base))
+              |> (pair defs #> PN);
+        fun select (PN (defs, modls)) (Module module) =
+          module
+          |> Graph.subgraph (Graph.all_succs module (defs @ map fst modls))
+          |> fold (fn (name, modls) => Graph.map_node name (select modls)) modls
+          |> Module;
+      in
+        Module modl
+        |> select (fold (mk_path o dest_name) (filter NameSpace.is_qualified names) (PN ([], [])))
+        |> dest_modl
+      end;
+
+fun add_check_transform (name, (Datatypcons (dtname, _))) =
+      ([([dtname],
+          fn [Datatyp (_, _, [])] => NONE | _ => "attempted to add constructor to already instantiating datatype" |> SOME)],
+       [(dtname,
+          fn Datatyp (vs, cs, clss) => Datatyp (vs, name::cs, clss)
+           | def => "attempted to add datatype constructor to non-datatype: "
+              ^ (Pretty.output o pretty_def) def |> error)])
+  | add_check_transform (name, Classmember (clsname, v, ty)) =
+      let
+        fun check_var (IType (tyco, tys)) s =
+              fold check_var tys s
+          | check_var (IFun (ty1, ty2)) s =
+              s
+              |> check_var ty1
+              |> check_var ty2
+          | check_var (IVarT (w, sort)) s =
+              if v = w
+              andalso member (op =) sort clsname
+              then "additional class appears at type variable" |> SOME
+              else NONE
+      in
+        ([([], fn [] => check_var ty NONE),
+          ([clsname],
+             fn [Class (_, _, [])] => NONE
+              | _ => "attempted to add class member to witnessed class" |> SOME)],
+         [(clsname,
+             fn Class (supcs, mems, insts) => Class (supcs, name::mems, insts)
+              | def => "attempted to add class member to non-class"
+                 ^ (Pretty.output o pretty_def) def |> error)])
+      end
+  | add_check_transform (name, Classinst (clsname, (tyco, arity), memdefs)) =
+      let
+        fun check [Classmember (_, v, mtyp_c), Fun (_, (_, mtyp_i))] =
+          let
+            val mtyp_i' = instant_itype (v, tyco `%%
+              map2 IVarT ((invent_tvar_names [mtyp_c] (length arity) [] "a"), arity)) mtyp_c;
+          in if eq_itype (mtyp_i', mtyp_i) (*! PERHAPS TOO STRICT !*)
+          then NONE
+          else "wrong type signature for class member: "
+            ^ (Pretty.output o pretty_itype) mtyp_i' ^ " expected,"
+            ^ (Pretty.output o pretty_itype) mtyp_i ^ " given" |> SOME end
+      in
+        (map (fn (memname, memprim) => ((writeln memname; writeln memprim; [memname, memprim]), check)) memdefs,
+          [(clsname,
+              fn Class (supcs, mems, insts) => Class (supcs, mems, name::insts)
+               | def => "attempted to add class instance to non-class"
+                  ^ (Pretty.output o pretty_def) def |> error),
+           (tyco,
+              fn Datatyp (vs, cs, clss) => Datatyp (vs, cs, clsname::clss)
+               | Nop => Nop
+               | def => "attempted to instantiate non-type to class instance"
+                  ^ (Pretty.output o pretty_def) def |> error)])
+      end
+  | add_check_transform _ = ([], []);
+
+fun succeed some = (pair o Succeed) some;
+fun fail msg = (pair o Fail) msg;
+
+fun check_fail msg' (Succeed dst, trns) = (dst, trns)
+  | check_fail msg' (Fail errmsg, _) = (tracing ("ROLLBACK CHECK: " ^ errmsg ^ "\n" ^ msg'); raise FAIL errmsg);
+
+fun handle_fail msg f modl =
+  f modl handle FAIL msg' => ([], modl) |> fail (msg ^ "\n" ^ msg');
+
+fun select_generator print_msg src [] trns =
+      fail ("no code generator available") trns
+  | select_generator print_msg src [(gname, cgen)] trns =
+      (print_msg gname; cgen src trns)
+  | select_generator print_msg src ((gname, cgen)::cgens) trns =
+      case cgen src trns
+       of result as (Succeed _, _) =>
+            (print_msg gname; result)
+        | _ => select_generator print_msg src cgens trns
+
+fun gen_invoke codegens msg src (deps, modl) =
+  ([], modl)
+  |> select_generator (fn gname => "choosing code generator " ^ gname ^ " for source " ^ quote msg)
+       src codegens
+  |> check_fail msg
+  ||> (fn (deps', modl') => (append deps' deps, modl'));
+
+fun gen_ensure_def defgens msg name (deps, modl) =
+  let
+    fun add (name, def) (deps, modl) =
+      let
+        val (checks, trans) = add_check_transform (name, def);
+        fun check (check_defs, checker) modl =
+          case checker (check_defs |> filter NameSpace.is_qualified |> map (get_def modl))
+           of NONE => modl
+            | SOME e => raise FAIL e;
+        fun transform (name, f) modl =
+          modl
+          |> K (NameSpace.is_qualified name) ? map_def name f;
+      in
+        modl
+        |> fold check checks
+        |> fold (curry add_dep name) deps
+        |> map_def name (fn _ => def)
+        |> fold transform trans
+      end;
+    fun ensure_node name modl =
+      if can (get_def modl) name
+      then ([name], modl)
+      else
+        ([], modl |> add_def (name, Nop))
+        |> select_generator (fn gname => "choosing code generator " ^ gname ^ " for definition of " ^ quote name)
+             name defgens
+        |> check_fail msg
+        |-> (fn (def, names') =>
+           add (name, def)
+           #> fold_map ensure_node names')
+        |-> (fn names' => pair (name :: Library.flat names'))
+  in
+    modl
+    |> ensure_node name
+    |-> (fn names => pair (names@deps))
+  end;
+
 end; (* struct *)
 
 
 structure CodegenThingol : CODEGEN_THINGOL =
 struct
 
-infix 8 `%%;
-infixr 6 `->;
-infixr 6 `-->;
-infix 4 `$;
-infix 4 `$$;
-
 open CodegenThingolOp;
 
 end; (* struct *)