src/Tools/code/code_thingol.ML

   val empty_funs: code -> string list;
   val is_cons: code -> string -> bool;
   val contr_classparam_typs: code -> string -> itype option list;
 
   type transact;
-  val ensure_const: theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
-    -> CodeFuncgr.T -> string -> transact -> string * transact;
-  val ensure_value: theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
-    -> CodeFuncgr.T -> term
-      -> transact -> (code * ((typscheme * iterm) * string list)) * transact;
+  val ensure_const: theory -> (sort -> sort) * Sorts.algebra -> CodeFuncgr.T
+    -> string -> transact -> string * transact;
+  val ensure_value: theory -> (sort -> sort) * Sorts.algebra -> CodeFuncgr.T
+    -> term -> transact -> (code * ((typscheme * iterm) * string list)) * transact;
   val transact: theory -> CodeFuncgr.T
-    -> (theory -> ((sort -> sort) * Sorts.algebra) * Consts.T -> CodeFuncgr.T
+    -> (theory -> (sort -> sort) * Sorts.algebra -> CodeFuncgr.T
       -> transact -> 'a * transact) -> code -> 'a * code;
   val add_value_stmt: iterm * itype -> code -> code;
 end;
 
 structure CodeThingol: CODE_THINGOL =

     |> pair dep
     |> pair name
   end;
 
 fun transact thy funcgr f code =
-  let
-    val naming = NameSpace.qualified_names NameSpace.default_naming;
-    val consttab = Consts.empty
-      |> fold (fn c => Consts.declare true naming [] (c, CodeFuncgr.typ funcgr c))
-           (CodeFuncgr.all funcgr);
-    val algbr = (Code.operational_algebra thy, consttab);
-  in
-    (NONE, code)
-    |> f thy algbr funcgr
-    |-> (fn x => fn (_, code) => (x, code))
-  end;
+  (NONE, code)
+  |> f thy (Code.operational_algebra thy) funcgr
+  |-> (fn x => fn (_, code) => (x, code));
 
 
 (* translation kernel *)
 
-fun ensure_class thy (algbr as ((_, algebra), _)) funcgr class =
+fun not_wellsorted thy thm ty sort e =
+  let
+    val err_class = Sorts.class_error (Syntax.pp_global thy) e;
+    val err_thm = case thm
+     of SOME thm => "\n(in defining equation " ^ Display.string_of_thm thm ^ ")" | NONE => "";
+    val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
+      ^ Syntax.string_of_sort_global thy sort;
+  in error ("Wellsortedness error" ^ err_thm ^ ":\n" ^ err_typ ^ "\n" ^ err_class) end;
+
+fun ensure_class thy (algbr as (_, algebra)) funcgr class =
   let
     val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
     val cs = #params (AxClass.get_info thy class);
     val class' = CodeName.class thy class;
     val stmt_class =

           end;
         val tyco' = CodeName.tyco thy tyco;
       in
         ensure_stmt stmt_datatype tyco'
       end
-and exprgen_tyvar_sort thy (algbr as ((proj_sort, _), _)) funcgr (v, sort) =
+and exprgen_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
   fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
   #>> (fn sort => (unprefix "'" v, sort))
 and exprgen_typ thy algbr funcgr (TFree vs) =
       exprgen_tyvar_sort thy algbr funcgr vs
       #>> (fn (v, sort) => ITyVar v)
   | exprgen_typ thy algbr funcgr (Type (tyco, tys)) =
       ensure_tyco thy algbr funcgr tyco
       ##>> fold_map (exprgen_typ thy algbr funcgr) tys
       #>> (fn (tyco, tys) => tyco `%% tys)
-and exprgen_dicts thy (algbr as ((proj_sort, algebra), consts)) funcgr (ty_ctxt, sort_decl) =
+and exprgen_dicts thy (algbr as (proj_sort, algebra)) funcgr thm (ty, sort) =
   let
     val pp = Syntax.pp_global thy;
     datatype typarg =
         Global of (class * string) * typarg list list
       | Local of (class * class) list * (string * (int * sort));

       let
         val sort' = proj_sort sort;
       in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
     val typargs = Sorts.of_sort_derivation pp algebra
       {class_relation = class_relation, type_constructor = type_constructor,
-       type_variable = type_variable}
-      (ty_ctxt, proj_sort sort_decl);
+       type_variable = type_variable} (ty, proj_sort sort)
+      handle Sorts.CLASS_ERROR e => not_wellsorted thy thm ty sort e;
     fun mk_dict (Global (inst, yss)) =
           ensure_inst thy algbr funcgr inst
           ##>> (fold_map o fold_map) mk_dict yss
           #>> (fn (inst, dss) => DictConst (inst, dss))
       | mk_dict (Local (classrels, (v, (k, sort)))) =
           fold_map (ensure_classrel thy algbr funcgr) classrels
           #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
   in
     fold_map mk_dict typargs
   end
-and exprgen_dict_parms thy (algbr as (_, consts)) funcgr (c, ty_ctxt) =
-  let
-    val ty_decl = Consts.the_type consts c;
-    val (tys, tys_decl) = pairself (curry (Consts.typargs consts) c) (ty_ctxt, ty_decl);
-    val sorts = map (snd o dest_TVar) tys_decl;
-  in
-    fold_map (exprgen_dicts thy algbr funcgr) (tys ~~ sorts)
-  end
 and exprgen_eq thy algbr funcgr thm =
   let
     val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
       o Logic.unvarify o prop_of) thm;
   in
-    fold_map (exprgen_term thy algbr funcgr) args
-    ##>> exprgen_term thy algbr funcgr rhs
+    fold_map (exprgen_term thy algbr funcgr (SOME thm)) args
+    ##>> exprgen_term thy algbr funcgr (SOME thm) rhs
     #>> rpair thm
   end
-and ensure_inst thy (algbr as ((_, algebra), _)) funcgr (class, tyco) =
+and ensure_inst thy (algbr as (_, algebra)) funcgr (class, tyco) =
   let
     val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
     val classparams = these (try (#params o AxClass.get_info thy) class);
     val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
     val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];

     val arity_typ = Type (tyco, map TFree vs);
     val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
     fun exprgen_superarity superclass =
       ensure_class thy algbr funcgr superclass
       ##>> ensure_classrel thy algbr funcgr (class, superclass)
-      ##>> exprgen_dicts thy algbr funcgr (arity_typ, [superclass])
+      ##>> exprgen_dicts thy algbr funcgr NONE (arity_typ, [superclass])
       #>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
             (superclass, (classrel, (inst, dss))));
     fun exprgen_classparam_inst (c, ty) =
       let
         val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
         val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy c_inst);
         val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd
           o Logic.dest_equals o Thm.prop_of) thm;
       in
         ensure_const thy algbr funcgr c
-        ##>> exprgen_const thy algbr funcgr c_ty
+        ##>> exprgen_const thy algbr funcgr (SOME thm) c_ty
         #>> (fn (c, IConst c_inst) => ((c, c_inst), thm))
       end;
     val stmt_inst =
       ensure_class thy algbr funcgr class
       ##>> ensure_tyco thy algbr funcgr tyco

              Classinst ((class, (tyco, arity)), (superarities, classparams)));
     val inst = CodeName.instance thy (class, tyco);
   in
     ensure_stmt stmt_inst inst
   end
-and ensure_const thy (algbr as (_, consts)) funcgr c =
+and ensure_const thy algbr funcgr c =
   let
     val c' = CodeName.const thy c;
     fun stmt_datatypecons tyco =
       ensure_tyco thy algbr funcgr tyco
       #>> Datatypecons;

       ensure_class thy algbr funcgr class
       #>> Classparam;
     fun stmt_fun trns =
       let
         val raw_thms = CodeFuncgr.funcs funcgr c;
-        val ty = (Logic.unvarifyT o CodeFuncgr.typ funcgr) c;
-        val vs = (map dest_TFree o Consts.typargs consts) (c, ty);
+        val (vs, raw_ty) = CodeFuncgr.typ funcgr c;
+        val ty = Logic.unvarifyT raw_ty;
         val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
           then raw_thms
           else map (CodeUnit.expand_eta 1) raw_thms;
       in
         trns

          of SOME class => stmt_classparam class
           | NONE => stmt_fun)
   in
     ensure_stmt stmtgen c'
   end
-and exprgen_term thy algbr funcgr (Const (c, ty)) =
-      exprgen_app thy algbr funcgr ((c, ty), [])
-  | exprgen_term thy algbr funcgr (Free (v, _)) =
+and exprgen_term thy algbr funcgr thm (Const (c, ty)) =
+      exprgen_app thy algbr funcgr thm ((c, ty), [])
+  | exprgen_term thy algbr funcgr thm (Free (v, _)) =
       pair (IVar v)
-  | exprgen_term thy algbr funcgr (Abs (abs as (_, ty, _))) =
+  | exprgen_term thy algbr funcgr thm (Abs (abs as (_, ty, _))) =
       let
         val (v, t) = Syntax.variant_abs abs;
       in
         exprgen_typ thy algbr funcgr ty
-        ##>> exprgen_term thy algbr funcgr t
+        ##>> exprgen_term thy algbr funcgr thm t
         #>> (fn (ty, t) => (v, ty) `|-> t)
       end
-  | exprgen_term thy algbr funcgr (t as _ $ _) =
+  | exprgen_term thy algbr funcgr thm (t as _ $ _) =
       case strip_comb t
        of (Const (c, ty), ts) =>
-            exprgen_app thy algbr funcgr ((c, ty), ts)
+            exprgen_app thy algbr funcgr thm ((c, ty), ts)
         | (t', ts) =>
-            exprgen_term thy algbr funcgr t'
-            ##>> fold_map (exprgen_term thy algbr funcgr) ts
+            exprgen_term thy algbr funcgr thm t'
+            ##>> fold_map (exprgen_term thy algbr funcgr thm) ts
             #>> (fn (t, ts) => t `$$ ts)
-and exprgen_const thy algbr funcgr (c, ty) =
-  ensure_const thy algbr funcgr c
-  ##>> exprgen_dict_parms thy algbr funcgr (c, ty)
-  ##>> fold_map (exprgen_typ thy algbr funcgr) ((fst o Term.strip_type) ty)
-  #>> (fn ((c, iss), tys) => IConst (c, (iss, tys)))
-and exprgen_app_default thy algbr funcgr (c_ty, ts) =
-  exprgen_const thy algbr funcgr c_ty
-  ##>> fold_map (exprgen_term thy algbr funcgr) ts
+and exprgen_const thy algbr funcgr thm (c, ty) =
+  let
+    val tys = Sign.const_typargs thy (c, ty);
+    val sorts = (map snd o fst o CodeFuncgr.typ funcgr) c;
+    val tys_args = (fst o Term.strip_type) ty;
+  in
+    ensure_const thy algbr funcgr c
+    ##>> fold_map (exprgen_dicts thy algbr funcgr thm) (tys ~~ sorts)
+    ##>> fold_map (exprgen_typ thy algbr funcgr) tys_args
+    #>> (fn ((c, iss), tys) => IConst (c, (iss, tys)))
+  end
+and exprgen_app_default thy algbr funcgr thm (c_ty, ts) =
+  exprgen_const thy algbr funcgr thm c_ty
+  ##>> fold_map (exprgen_term thy algbr funcgr thm) ts
   #>> (fn (t, ts) => t `$$ ts)
-and exprgen_case thy algbr funcgr n cases (app as ((c, ty), ts)) =
+and exprgen_case thy algbr funcgr thm n cases (app as ((c, ty), ts)) =
   let
     val (tys, _) =
       (chop (1 + (if null cases then 1 else length cases)) o fst o strip_type) ty;
     val dt = nth ts n;
     val dty = nth tys n;

             val ([v_ty], body) = Term.strip_abs_eta 1 (the_single (nth_drop n ts))
           in [(Free v_ty, body)] end
       | mk_ds cases = map_filter (uncurry mk_case)
           (AList.make (CodeUnit.no_args thy) cases ~~ nth_drop n ts);
   in
-    exprgen_term thy algbr funcgr dt
+    exprgen_term thy algbr funcgr thm dt
     ##>> exprgen_typ thy algbr funcgr dty
-    ##>> fold_map (fn (pat, body) => exprgen_term thy algbr funcgr pat
-          ##>> exprgen_term thy algbr funcgr body) (mk_ds cases)
-    ##>> exprgen_app_default thy algbr funcgr app
+    ##>> fold_map (fn (pat, body) => exprgen_term thy algbr funcgr thm pat
+          ##>> exprgen_term thy algbr funcgr thm body) (mk_ds cases)
+    ##>> exprgen_app_default thy algbr funcgr thm app
     #>> (fn (((dt, dty), ds), t0) => ICase (((dt, dty), ds), t0))
   end
-and exprgen_app thy algbr funcgr ((c, ty), ts) = case Code.get_case_data thy c
+and exprgen_app thy algbr funcgr thm ((c, ty), ts) = case Code.get_case_data thy c
  of SOME (n, cases) => let val i = 1 + (if null cases then 1 else length cases) in
       if length ts < i then
         let
           val k = length ts;
           val tys = (curry Library.take (i - k) o curry Library.drop k o fst o strip_type) ty;
           val ctxt = (fold o fold_aterms)
             (fn Free (v, _) => Name.declare v | _ => I) ts Name.context;
           val vs = Name.names ctxt "a" tys;
         in
           fold_map (exprgen_typ thy algbr funcgr) tys
-          ##>> exprgen_case thy algbr funcgr n cases ((c, ty), ts @ map Free vs)
+          ##>> exprgen_case thy algbr funcgr thm n cases ((c, ty), ts @ map Free vs)
           #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
         end
       else if length ts > i then
-        exprgen_case thy algbr funcgr n cases ((c, ty), Library.take (i, ts))
-        ##>> fold_map (exprgen_term thy algbr funcgr) (Library.drop (i, ts))
+        exprgen_case thy algbr funcgr thm n cases ((c, ty), Library.take (i, ts))
+        ##>> fold_map (exprgen_term thy algbr funcgr thm) (Library.drop (i, ts))
         #>> (fn (t, ts) => t `$$ ts)
       else
-        exprgen_case thy algbr funcgr n cases ((c, ty), ts)
+        exprgen_case thy algbr funcgr thm n cases ((c, ty), ts)
       end
-  | NONE => exprgen_app_default thy algbr funcgr ((c, ty), ts);
+  | NONE => exprgen_app_default thy algbr funcgr thm ((c, ty), ts);
 
 
 (** evaluation **)
 
 fun add_value_stmt (t, ty) code =

     val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
       o dest_TFree))) t [];
     val stmt_value =
       fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
       ##>> exprgen_typ thy algbr funcgr ty
-      ##>> exprgen_term thy algbr funcgr t
+      ##>> exprgen_term thy algbr funcgr NONE t
       #>> (fn ((vs, ty), t) => Fun ((vs, ty), [(([], t), Drule.dummy_thm)]));
     fun term_value (dep, code1) =
       let
         val Fun ((vs, ty), [(([], t), _)]) =
           Graph.get_node code1 CodeName.value_name;