src/Pure/Tools/codegen_thingol.ML

     | IVarT of vname * sort;
   datatype iexpr =
       IConst of (string * itype) * classlookup list list
     | IVarE of vname * itype
     | IApp of iexpr * iexpr
-    | IAbs of (vname * itype) * iexpr
+    | IAbs of iexpr * iexpr
     | ICase of iexpr * (iexpr * iexpr) list;
   val mk_funs: itype list * itype -> itype;
   val mk_apps: iexpr * iexpr list -> iexpr;
-  val mk_abss: (vname * itype) list * iexpr -> iexpr;
+  val mk_abss: iexpr list * iexpr -> iexpr;
   val pretty_itype: itype -> Pretty.T;
   val pretty_iexpr: iexpr -> Pretty.T;
   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: iexpr -> iexpr * iexpr list;
-  val unfold_abs: iexpr -> (vname * itype) list * iexpr;
+  val unfold_abs: iexpr -> iexpr list * iexpr;
   val unfold_let: iexpr -> (iexpr * iexpr) list * iexpr;
   val unfold_const_app: iexpr ->
     (((string * itype) * classlookup list list) * iexpr list) option;
   val ensure_pat: iexpr -> iexpr;
   val itype_of_iexpr: iexpr -> itype;

   val `%% : string * itype list -> itype;
   val `-> : itype * itype -> itype;
   val `--> : itype list * itype -> itype;
   val `$ : iexpr * iexpr -> iexpr;
   val `$$ : iexpr * iexpr list -> iexpr;
-  val `|-> : (vname * itype) * iexpr -> iexpr;
-  val `|--> : (vname * itype) list * iexpr -> iexpr;
+  val `|-> : iexpr * iexpr -> iexpr;
+  val `|--> : iexpr list * iexpr -> iexpr;
 
   type funn = (iexpr list * iexpr) list * (ClassPackage.sortcontext * itype);
   datatype prim =
       Pretty of Pretty.T
     | Name;
   datatype def =
       Undef
     | Prim of (string * prim list) list
     | Fun of funn
-    | Typesyn of (vname * string list) list * itype
-    | Datatype of ((vname * string list) list * (string * itype list) list)
-        * string list
+    | Typesyn of (vname * sort) list * itype
+    | Datatype of (vname * sort) list * (string * itype list) list
     | Datatypecons of string
-    | Class of (class list * (vname * (string * (ClassPackage.sortcontext * itype)) list))
-        * string list
+    | Class of class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)
     | Classmember of class
     | Classinst of ((class * (string * (vname * sort) list))
           * (class * classlookup list list) list)
         * (string * funn) list;
   type module;

   val debug_level: int ref;
   val debug: int -> ('a -> string) -> 'a -> 'a;
   val soft_exc: bool ref;
 
   val serialize:
-    ((string -> string) -> (string * def) list -> 'a option)
+    ((string -> string -> string) -> string -> (string * def) list -> 'a option)
     -> (string list -> (string * string) * 'a list -> 'a option)
     -> (string -> string option)
     -> (string * string -> string)
     -> string list list -> string -> module -> 'a option;
 end;

 
 datatype iexpr =
     IConst of (string * itype) * classlookup list list
   | IVarE of vname * itype
   | IApp of iexpr * iexpr
-  | IAbs of (vname * itype) * iexpr
+  | IAbs of iexpr * iexpr
   | ICase of iexpr * (iexpr * iexpr) list;
 
 (*
   variable naming conventions
 

       Pretty.block [Pretty.str (c ^ "::"), pretty_itype ty]
   | pretty_iexpr (IVarE (v, ty)) =
       Pretty.block [Pretty.str ("?" ^ v ^ "::"), pretty_itype ty]
   | pretty_iexpr (IApp (e1, e2)) =
       Pretty.enclose "(" ")" [pretty_iexpr e1, Pretty.brk 1, pretty_iexpr e2]
-  | pretty_iexpr (IAbs ((v, ty), e)) =
-      Pretty.enclose "(" ")" [Pretty.str ("?" ^ v ^ " |->"), Pretty.brk 1, pretty_iexpr e]
+  | pretty_iexpr (IAbs (e1, e2)) =
+      Pretty.enclose "(" ")" [pretty_iexpr e1, Pretty.brk 1, Pretty.str "|->", Pretty.brk 1, pretty_iexpr e2]
   | pretty_iexpr (ICase (e, cs)) =
       Pretty.enclose "(" ")" [
         Pretty.str "case ",
         pretty_iexpr e,
         Pretty.enclose "(" ")" (map (fn (p, e) =>

   let
     fun instant (IVarT x) = f x
       | instant y = map_itype instant y;
   in map_itype instant end;
 
-
-(* simple diagnosis *)
-
-fun pretty_itype (IType (tyco, tys)) =
-      Pretty.enum "" "(" ")" (Pretty.str tyco :: map pretty_itype tys)
-  | pretty_itype (IFun (ty1, ty2)) =
-      Pretty.enum "" "(" ")" [pretty_itype ty1, Pretty.str "->", pretty_itype ty2]
-  | pretty_itype (IVarT (v, sort)) =
-      Pretty.str (v ^ enclose "|" "|" (space_implode "|" sort));
-
-fun pretty_iexpr (IConst ((c, ty), _)) =
-      Pretty.block [Pretty.str (c ^ "::"), pretty_itype ty]
-  | pretty_iexpr (IVarE (v, ty)) =
-      Pretty.block [Pretty.str ("?" ^ v ^ "::"), pretty_itype ty]
-  | pretty_iexpr (IApp (e1, e2)) =
-      Pretty.enclose "(" ")" [pretty_iexpr e1, Pretty.brk 1, pretty_iexpr e2]
-  | pretty_iexpr (IAbs ((v, ty), e)) =
-      Pretty.enclose "(" ")" [Pretty.str ("?" ^ v ^ " |->"), Pretty.brk 1, pretty_iexpr e]
-  | pretty_iexpr (ICase (e, cs)) =
-      Pretty.enclose "(" ")" [
-        Pretty.str "case ",
-        pretty_iexpr e,
-        Pretty.enclose "(" ")" (map (fn (p, e) =>
-          Pretty.block [
-            pretty_iexpr p,
-            Pretty.str " => ",
-            pretty_iexpr e
-          ]
-        ) cs)
-      ];
-
-
-(* language auxiliary *)
-
 fun itype_of_iexpr (IConst ((_, ty), s)) = ty
   | itype_of_iexpr (IVarE (_, ty)) = ty
   | itype_of_iexpr (e as IApp (e1, e2)) = (case itype_of_iexpr e1
       of (IFun (ty2, ty')) =>
             if ty2 = itype_of_iexpr e2
             then ty'
             else error ("inconsistent application: in " ^ Pretty.output (pretty_iexpr e)
               ^ ", " ^ (Pretty.output o pretty_itype) ty2
               ^ " vs. " ^ (Pretty.output o pretty_itype o itype_of_iexpr) e2)
        | _ => error ("expression is not a function: " ^ Pretty.output (pretty_iexpr e1)))
-  | itype_of_iexpr (IAbs ((_, ty1), e2)) = ty1 `-> itype_of_iexpr e2
+  | itype_of_iexpr (IAbs (e1, e2)) = itype_of_iexpr e1 `-> itype_of_iexpr e2
   | itype_of_iexpr (ICase ((_, [(_, e)]))) = itype_of_iexpr e;
 
 fun ensure_pat (e as IConst (_, [])) = e
   | ensure_pat (e as IVarE _) = e
   | ensure_pat (e as IApp (e1, e2)) =

       error ("illegal expression for pattern: " ^ (Pretty.output o pretty_iexpr) e);
 
 fun type_vnames ty = 
   let
     fun extr (IVarT (v, _)) =
-      insert (op =) v
+          insert (op =) v
+      | extr _ = I;
   in fold_atype extr ty end;
 
 fun expr_names e =
   let
     fun extr (IConst ((c, _), _)) =

 
 datatype def =
     Undef
   | Prim of (string * prim list) list
   | Fun of funn
-  | Typesyn of (vname * string list) list * itype
-  | Datatype of ((vname * string list) list * (string * itype list) list)
-      * string list
+  | Typesyn of (vname * sort) list * itype
+  | Datatype of (vname * sort) list * (string * itype list) list
   | Datatypecons of string
-  | Class of (class list * (vname * (string * (ClassPackage.sortcontext * itype)) list))
-      * string list
+  | Class of class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)
   | Classmember of class
   | Classinst of ((class * (string * (vname * sort) list))
         * (class * classlookup list list) list)
       * (string * funn) list;
 

       Pretty.block [
         Pretty.list "(" ")" (map (pretty_itype o IVarT) vs),
         Pretty.str " |=> ",
         pretty_itype ty
       ]
-  | pretty_def (Datatype ((vs, cs), insts)) =
+  | pretty_def (Datatype (vs, cs)) =
       Pretty.block [
         Pretty.list "(" ")" (map (pretty_itype o IVarT) vs),
         Pretty.str " |=> ",
         Pretty.enum " |" "" ""
           (map (fn (c, tys) => (Pretty.block o Pretty.breaks)
-            (Pretty.str c :: map pretty_itype tys)) cs),
-        Pretty.str ", instances ",
-        Pretty.enum "," "[" "]" (map Pretty.str insts)
+            (Pretty.str c :: map pretty_itype tys)) cs)
       ]
   | pretty_def (Datatypecons dtname) =
       Pretty.str ("cons " ^ dtname)
-  | pretty_def (Class ((supcls, (v, mems)), insts)) =
+  | pretty_def (Class (supcls, (v, mems))) =
       Pretty.block [
         Pretty.str ("class var " ^ v ^ "extending "),
         Pretty.enum "," "[" "]" (map Pretty.str supcls),
         Pretty.str " with ",
         Pretty.enum "," "[" "]"
           (map (fn (m, (_, ty)) => Pretty.block
-            [Pretty.str (m ^ "::"), pretty_itype ty]) mems),
-        Pretty.str " instances ",
-        Pretty.enum "," "[" "]" (map Pretty.str insts)
+            [Pretty.str (m ^ "::"), pretty_itype ty]) mems)
       ]
   | pretty_def (Classmember clsname) =
       Pretty.block [
         Pretty.str "class member belonging to ",
         Pretty.str clsname

       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
+        else fn edge => (Graph.add_edge_acyclic edge
+          handle Graph.CYCLES _ => error ("adding dependency "
+            ^ quote name1 ^ " -> " ^ quote name2 ^ " would result in module dependency cycle"))
       fun add [] node =
             node
             |> add_edge (s1, s2)
         | add (m::ms) node =
             node

       d
   | check_prep_def modl (Fun (eqs, d)) =
       Fun (check_funeqs eqs, d)
   | check_prep_def modl (d as Typesyn _) =
       d
-  | check_prep_def modl (d as Datatype (_, insts)) =
-      if null insts
-      then d
-      else error "attempted to add datatype with bare instances"
+  | check_prep_def modl (d as Datatype _) =
+      d
   | check_prep_def modl (Datatypecons dtco) =
       error "attempted to add bare datatype constructor"
-  | check_prep_def modl (d as Class ((_, (v, membrs)), insts)) =
-      if null insts
-      then
-        if member (op =) (map fst (Library.flat (map (fst o snd) membrs))) v
-        then error "incorrectly abstracted class type variable"
-        else d
-      else error "attempted to add class with bare instances"
+  | check_prep_def modl (d as Class _) =
+      d
   | check_prep_def modl (Classmember _) =
       error "attempted to add bare class member"
   | check_prep_def modl (Classinst ((d as ((class, (tyco, arity)), _), memdefs))) =
       let
-        val Class ((_, (v, membrs)), _) = get_def modl class;
+        val Class (_, (v, membrs)) = get_def modl class;
         val _ = if length memdefs > length memdefs
           then error "too many member definitions given"
           else ();
         fun instant (w, ty) (var as (v, _)) =
           if v = w then ty else IVarT var;

                 if eq_itype (instant_itype (instant (v, tyco `%% map IVarT arity)) ty, ty')
                 then (m, (check_funeqs eqs, (ctxt', ty')))
                 else error ("inconsistent type for member definition " ^ quote m)
       in Classinst (d, map mk_memdef membrs) end;
 
-fun postprocess_def (name, Datatype ((_, constrs), _)) =
+fun postprocess_def (name, Datatype (_, constrs)) =
       (check_samemodule (name :: map fst constrs);
       fold (fn (co, _) =>
         ensure_def (co, Datatypecons name)
         #> add_dep (co, name)
         #> add_dep (name, co)
       ) constrs
       )
-  | postprocess_def (name, Class ((_, (_, membrs)), _)) =
+  | postprocess_def (name, Class (_, (_, membrs))) =
       (check_samemodule (name :: map fst membrs);
       fold (fn (m, _) =>
         ensure_def (m, Classmember name)
         #> add_dep (m, name)
         #> add_dep (name, m)
       ) membrs
       )
-  | postprocess_def (name, Classinst (((class, (tyco, _)), _), _)) =
-      map_def class (fn Datatype (d, insts) => Datatype (d, name::insts)
-                      | d => d)
-      #> map_def class (fn Class (d, insts) => Class (d, name::insts))
   | postprocess_def _ =
       I;
 
 fun succeed some (_, modl) = (Succeed some, modl);
 fun fail msg (_, modl) = (Fail ([msg], NONE), modl);

             val tys =
               (fst o unfold_fun) ty
               |> curry Library.drop (length es)
               |> curry Library.take add_n
             val add_vars =
-              Term.invent_names (fold expr_names es []) "x" add_n ~~ tys;
+              map2 (curry IVarE) (Term.invent_names (fold expr_names es []) "x" add_n) tys;
           in
-            add_vars `|--> IConst ((f, ty), ls) `$$ es `$$ map IVarE add_vars
+            add_vars `|--> IConst ((f, ty), ls) `$$ es `$$ add_vars
           end
        | NONE => map_iexpr eta e;
   in (map_defs o map_def_fun o map_def_fun_expr) eta end;
 
 val eta_expand_poly =

     fun eta (funn as ([([], e)], cty as (sortctxt, (ty as IFun (ty1, ty2))))) =
           if (not o null) sortctxt
             orelse null (type_vnames ty [])
           then funn
           else
-            let
-              val add_var = (hd (Term.invent_names (expr_names e []) "x" 1), ty1)
-            in (([([IVarE add_var], add_var `|-> e)], cty)) end
+            (case unfold_abs e
+             of ([], e) =>
+                  let
+                    val add_var = IVarE (hd (Term.invent_names (expr_names e []) "x" 1), ty1)
+                  in (([([add_var], add_var `|-> e)], cty)) end
+              | eq => 
+                  (([eq], cty)))
       | eta funn = funn;
   in (map_defs o map_def_fun) eta end;
 
 val unclash_vars_tvars = 
   let

 (* serialization *)
 
 fun serialize seri_defs seri_module validate postprocess nsp_conn name_root module =
   let
     val resolver = mk_deresolver module nsp_conn postprocess validate;
+    fun sresolver s = (resolver o NameSpace.unpack) s
     fun mk_name prfx name =
       let
         val name_qual = NameSpace.pack (prfx @ [name])
       in (name_qual, resolver prfx name_qual) end;
     fun mk_contents prfx module =

         ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)
     and seri prfx ([(name, Module modl)]) =
           seri_module (map (resolver []) (imports_of module (prfx @ [name])))
             (mk_name prfx name, mk_contents (prfx @ [name]) modl)
       | seri prfx ds =
-          seri_defs (resolver prfx)
+          seri_defs sresolver (NameSpace.pack prfx)
             (map (fn (name, Def def) => (fst (mk_name prfx name), def)) ds)
   in
     seri_module (map (resolver []) (Graph.strong_conn module |> List.concat |> rev))
       (("", name_root), (mk_contents [] module))
   end;