src/Tools/code/code_wellsorted.ML

 type var = const * int;
 
 structure Vargraph =
   GraphFun(type key = var val ord = prod_ord const_ord int_ord);
 
-datatype styp = Tyco of string * styp list | Var of var;
-
-val empty_vardeps : ((string * styp list) list * class list) Vargraph.T
-    * (const list * ((string * sort) list * (thm * bool) list) Symtab.table) =
-  (Vargraph.empty, ([], Symtab.empty));
-  (*FIXME: user table with proto equations as assertor for functions,
-    add dummy to styp which allows to process consts of terms directly*)
-
-(* computing instantiations *)
+datatype styp = Tyco of string * styp list | Var of var | Free;
+
+fun styp_of c_lhs (Type (tyco, tys)) = Tyco (tyco, map (styp_of c_lhs) tys)
+  | styp_of c_lhs (TFree (v, _)) = case c_lhs
+     of SOME (c, lhs) => Var (Fun c, find_index (fn (v', _) => v = v') lhs)
+      | NONE => Free;
+
+type vardeps_data = ((string * styp list) list * class list) Vargraph.T
+  * (((string * sort) list * (thm * bool) list) Symtab.table
+    * (class * string) list);
+
+val empty_vardeps_data : vardeps_data =
+  (Vargraph.empty, (Symtab.empty, []));
+
+(* retrieving equations and instances from the background context *)
 
 fun obtain_eqns thy eqngr c =
   case try (Graph.get_node eqngr) c
    of SOME ((lhs, _), eqns) => ((lhs, []), eqns)
     | NONE => let

         val classess = map (complete_proper_sort thy)
           (Sign.arity_sorts thy tyco [class]);
         val inst_params = inst_params thy tyco all_classes;
       in (classess, (superclasses, inst_params)) end;
 
+
+(* computing instantiations *)
+
 fun add_classes thy arities eqngr c_k new_classes vardeps_data =
   let
     val (styps, old_classes) = Vargraph.get_node (fst vardeps_data) c_k;
     val diff_classes = new_classes |> subtract (op =) old_classes;
   in if null diff_classes then vardeps_data
   else let
     val c_ks = Vargraph.imm_succs (fst vardeps_data) c_k |> insert (op =) c_k;
   in
     vardeps_data
     |> (apfst o Vargraph.map_node c_k o apsnd) (append diff_classes)
-    |> fold (fn styp => fold (add_typmatch_inst thy arities eqngr styp) new_classes) styps
+    |> fold (fn styp => fold (assert_typmatch_inst thy arities eqngr styp) new_classes) styps
     |> fold (fn c_k => add_classes thy arities eqngr c_k diff_classes) c_ks
   end end
 and add_styp thy arities eqngr c_k tyco_styps vardeps_data =
   let
     val (old_styps, classes) = Vargraph.get_node (fst vardeps_data) c_k;
   in if member (op =) old_styps tyco_styps then vardeps_data
   else
     vardeps_data
     |> (apfst o Vargraph.map_node c_k o apfst) (cons tyco_styps)
-    |> fold (add_typmatch_inst thy arities eqngr tyco_styps) classes
+    |> fold (assert_typmatch_inst thy arities eqngr tyco_styps) classes
   end
 and add_dep thy arities eqngr c_k c_k' vardeps_data =
   let
     val (_, classes) = Vargraph.get_node (fst vardeps_data) c_k;
   in
     vardeps_data
     |> add_classes thy arities eqngr c_k' classes
     |> apfst (Vargraph.add_edge (c_k, c_k'))
   end
-and add_typmatch_inst thy arities eqngr (tyco, styps) class vardeps_data =
+and assert_typmatch_inst thy arities eqngr (tyco, styps) class vardeps_data =
   if can (Sign.arity_sorts thy tyco) [class]
   then vardeps_data
-    |> assert thy arities eqngr (Inst (class, tyco))
+    |> assert_inst thy arities eqngr (class, tyco)
     |> fold_index (fn (k, styp) =>
-         add_typmatch thy arities eqngr styp (Inst (class, tyco), k)) styps
+         assert_typmatch thy arities eqngr styp (Inst (class, tyco), k)) styps
   else vardeps_data (*permissive!*)
-and add_typmatch thy arities eqngr (Var c_k') c_k vardeps_data =
-      vardeps_data
-      |> add_dep thy arities eqngr c_k c_k'
-  | add_typmatch thy arities eqngr (Tyco tyco_styps) c_k vardeps_data =
-      vardeps_data
-      |> add_styp thy arities eqngr c_k tyco_styps
-and add_inst thy arities eqngr (inst as (class, tyco)) vardeps_data =
-  let
+and assert_inst thy arities eqngr (inst as (class, tyco)) (vardeps_data as (_, (_, insts))) =
+  if member (op =) insts inst then vardeps_data
+  else let
     val (classess, (superclasses, inst_params)) =
       obtain_instance thy arities inst;
   in
     vardeps_data
-    |> fold (fn superclass => assert thy arities eqngr (Inst (superclass, tyco))) superclasses
-    |> fold (assert thy arities eqngr o Fun) inst_params
+    |> (apsnd o apsnd) (insert (op =) inst)
+    |> fold (fn superclass => assert_inst thy arities eqngr (superclass, tyco)) superclasses
+    |> fold (assert_fun thy arities eqngr) inst_params
     |> fold_index (fn (k, classes) =>
          apfst (Vargraph.new_node ((Inst (class, tyco), k), ([] ,[])))
          #> add_classes thy arities eqngr (Inst (class, tyco), k) classes
          #> fold (fn superclass =>
              add_dep thy arities eqngr (Inst (superclass, tyco), k)

              add_dep thy arities eqngr (Fun inst_param, k)
              (Inst (class, tyco), k)
              ) inst_params
          ) classess
   end
-and add_const thy arities eqngr c vardeps_data =
-  let
+and assert_typmatch thy arities eqngr (Tyco tyco_styps) c_k vardeps_data =
+      vardeps_data
+      |> add_styp thy arities eqngr c_k tyco_styps
+  | assert_typmatch thy arities eqngr (Var c_k') c_k vardeps_data =
+      vardeps_data
+      |> add_dep thy arities eqngr c_k c_k'
+  | assert_typmatch thy arities eqngr Free c_k vardeps_data =
+      vardeps_data
+and assert_rhs thy arities eqngr (c', styps) vardeps_data =
+  vardeps_data
+  |> assert_fun thy arities eqngr c'
+  |> fold_index (fn (k, styp) =>
+       assert_typmatch thy arities eqngr styp (Fun c', k)) styps
+and assert_fun thy arities eqngr c (vardeps_data as (_, (eqntab, _))) =
+  if Symtab.defined eqntab c then vardeps_data
+  else let
     val ((lhs, rhss), eqns) = obtain_eqns thy eqngr c;
-    fun styp_of (Type (tyco, tys)) = Tyco (tyco, map styp_of tys)
-      | styp_of (TFree (v, _)) = Var (Fun c, find_index (fn (v', _) => v = v') lhs);
-    val rhss' = (map o apsnd o map) styp_of rhss;
+    val rhss' = (map o apsnd o map) (styp_of (SOME (c, lhs))) rhss;
   in
     vardeps_data
-    |> (apsnd o apsnd) (Symtab.update_new (c, (lhs, eqns)))
+    |> (apsnd o apfst) (Symtab.update_new (c, (lhs, eqns)))
     |> fold_index (fn (k, (_, sort)) =>
          apfst (Vargraph.new_node ((Fun c, k), ([] ,[])))
          #> add_classes thy arities eqngr (Fun c, k) (complete_proper_sort thy sort)) lhs
-    |> fold (assert thy arities eqngr o Fun o fst) rhss'
-    |> fold (fn (c', styps) => fold_index (fn (k', styp) =>
-         add_typmatch thy arities eqngr styp (Fun c', k')) styps) rhss'
-  end
-and assert thy arities eqngr c vardeps_data =
-  if member (op =) ((fst o snd) vardeps_data) c then vardeps_data
-  else case c
-   of Fun const => vardeps_data |> (apsnd o apfst) (cons c) |> add_const thy arities eqngr const
-    | Inst inst => vardeps_data |> (apsnd o apfst) (cons c) |> add_inst thy arities eqngr inst;
+    |> fold (assert_rhs thy arities eqngr) rhss'
+  end;
 
 
 (* applying instantiations *)
 
 fun build_algebra thy arities =

     val is_proper = can (AxClass.get_info thy);
     val classrels = Sorts.classrels_of thy_algebra
       |> filter (is_proper o fst)
       |> (map o apsnd) (filter is_proper);
     val instances = Sorts.instances_of thy_algebra
-      |> filter (is_proper o snd);
+      |> filter (is_proper o snd)
+      |> map swap (*FIXME*)
     fun add_class (class, superclasses) algebra =
       Sorts.add_class pp (class, Sorts.minimize_sort algebra superclasses) algebra;
-    fun add_arity (tyco, class) algebra =
-      case AList.lookup (op =) arities (tyco, class)
-       of SOME sorts => Sorts.add_arities pp
-            (tyco, [(class, map (Sorts.minimize_sort algebra) sorts)]) algebra
-        | NONE => if Sign.arity_number thy tyco = 0
-            then Sorts.add_arities pp (tyco, [(class, [])]) algebra
-            else algebra;
+    fun add_arity (class, tyco) algebra = Sorts.add_arities pp
+      (tyco, [(class, ((map (Sorts.minimize_sort algebra) o the
+        o AList.lookup (op =) arities) (class, tyco)))]) algebra;
   in
     Sorts.empty_algebra
     |> fold add_class classrels
     |> fold add_arity instances
   end;
 
 fun dicts_of thy (proj_sort, algebra) (T, sort) =
   let
     fun class_relation (x, _) _ = x;
     fun type_constructor tyco xs class =
-      inst_params thy tyco (Sorts.complete_sort algebra [class]) @ (maps o maps) fst xs;
+      inst_params thy tyco (Sorts.complete_sort algebra [class])
+        @ (maps o maps) fst xs;
     fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort);
   in
     flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra
       { class_relation = class_relation, type_constructor = type_constructor,
         type_variable = type_variable } (T, proj_sort sort)
        handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
   end;
 
-fun add_arities thy vardeps = Vargraph.fold (fn ((Fun _, _), _) => I
-  | ((Inst (class, tyco), k), ((_, classes), _)) =>
-      AList.map_default (op =)
-        ((tyco, class), replicate (Sign.arity_number thy tyco) [])
-          (nth_map k (K classes))) vardeps;
-
-fun add_eqs thy (proj_sort, algebra) eqntab vardeps c gr =
-  let
-    val (proto_lhs, proto_eqns) = (the o Symtab.lookup eqntab) c;
+fun add_arity thy vardeps (class, tyco) =
+  AList.update (op =)
+    ((class, tyco), map (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k))
+      (0 upto Sign.arity_number thy tyco - 1));
+
+fun add_eqs thy (proj_sort, algebra) vardeps
+    (c, (proto_lhs, proto_eqns)) (rhss, eqngr) =
+  let
     val lhs = map_index (fn (k, (v, _)) =>
       (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs;
     val inst_tab = Vartab.empty |> fold (fn (v, sort) =>
       Vartab.update ((v, 0), sort)) lhs;
     val eqns = proto_eqns
       |> (map o apfst) (Code_Unit.inst_thm thy inst_tab);
-    val (tyscm, rhss) = tyscm_rhss_of thy c eqns;
-  in
-    gr
-    |> Graph.new_node (c, (tyscm, eqns))
-    |> fold (fn (c', Ts) => ensure_eqs_dep thy (proj_sort, algebra) eqntab vardeps c c'
-        #-> (fn (vs, _) =>
-          fold2 (ensure_match thy (proj_sort, algebra) eqntab vardeps c) Ts (map snd vs))) rhss
-    |> pair tyscm
-  end
-and ensure_match thy (proj_sort, algebra) eqntab vardeps c T sort gr =
-  gr
-  |> fold (fn c' => ensure_eqs_dep thy (proj_sort, algebra) eqntab vardeps c c' #> snd)
-       (dicts_of thy (proj_sort, algebra) (T, proj_sort sort))
-and ensure_eqs_dep thy (proj_sort, algebra) eqntab vardeps c c' gr =
-  gr
-  |> ensure_eqs thy (proj_sort, algebra) eqntab vardeps c'
-  ||> Graph.add_edge (c, c')
-and ensure_eqs thy (proj_sort, algebra) eqntab vardeps c gr =
-  case try (Graph.get_node gr) c
-   of SOME (tyscm, _) => (tyscm, gr)
-    | NONE => add_eqs thy (proj_sort, algebra) eqntab vardeps c gr;
-
-fun extend_arities_eqngr thy cs insts (arities, eqngr) =
-  let
-    val (vardeps, (_, eqntab)) = empty_vardeps
-      |> fold (assert thy arities eqngr o Fun) cs
-      |> fold (assert thy arities eqngr o Inst) insts;
-    val arities' = add_arities thy vardeps arities;
+    val (tyscm, rhss') = tyscm_rhss_of thy c eqns;
+    val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr;
+  in (map (pair c) rhss' @ rhss, eqngr') end;
+
+fun extend_arities_eqngr thy cs cs_rhss (arities, eqngr) =
+  let
+    val cs_rhss' = (map o apsnd o map) (styp_of NONE) cs_rhss;
+    val (vardeps, (eqntab, insts)) = empty_vardeps_data
+      |> fold (assert_fun thy arities eqngr) cs
+      |> fold (assert_rhs thy arities eqngr) cs_rhss';
+    val arities' = fold (add_arity thy vardeps) insts arities;
     val algebra = build_algebra thy arities';
     val proj_sort = complete_proper_sort thy #> Sorts.minimize_sort algebra;
-    fun complete_inst_params (class, tyco) =
-      inst_params thy tyco (Sorts.complete_sort algebra [class]);
-    val cs' = maps complete_inst_params insts @ cs; (*FIXME*)
-    val (_, eqngr') =
-      fold_map (ensure_eqs thy (proj_sort, algebra) eqntab vardeps) cs' eqngr;
-  in ((proj_sort, algebra), (arities', eqngr')) end;
+    val (rhss, eqngr') = Symtab.fold
+      (add_eqs thy (proj_sort, algebra) vardeps) eqntab ([], eqngr);
+    fun deps_of (c, rhs) = c ::
+      maps (dicts_of thy (proj_sort, algebra))
+        (rhs ~~ (map snd o fst o fst o Graph.get_node eqngr') c);
+    val eqngr'' = fold (fn (c, rhs) => fold
+      (curry Graph.add_edge c) (deps_of rhs)) rhss eqngr';
+  in ((proj_sort, algebra), (arities', eqngr'')) end;
 
 
 (** retrieval interfaces **)
-
-fun instance_dicts_of thy (proj_sort, algebra) (T, sort) = (*FIXME vs. consts_dicts_of *)
-  let
-    fun class_relation (x, _) _ = x;
-    fun type_constructor tyco xs class =
-      (class, tyco) :: (maps o maps) fst xs;
-    fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort);
-  in
-    flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra
-      { class_relation = class_relation, type_constructor = type_constructor,
-        type_variable = type_variable } (T, proj_sort sort)
-       handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
-  end;
 
 fun proto_eval thy cterm_of evaluator_lift evaluator proto_ct arities_eqngr =
   let
     val ct = cterm_of proto_ct;
     val _ = Sign.no_vars (Syntax.pp_global thy) (Thm.term_of ct);

     fun consts_of t =
       fold_aterms (fn Const c_ty => cons c_ty | _ => I) t [];
     val thm = Code.preprocess_conv thy ct;
     val ct' = Thm.rhs_of thm;
     val t' = Thm.term_of ct';
+    val (t'', evaluator_eqngr) = evaluator t';
     val consts = map fst (consts_of t');
-    val (algebra', arities_eqngr') = extend_arities_eqngr thy consts [] arities_eqngr;
-    val (t'', evaluator_eqngr) = evaluator t';
     val consts' = consts_of t'';
-    val const_matches = fold (fn (c, ty) =>
-      insert (op =) (Sign.const_typargs thy (c, Logic.unvarifyT ty), c)) consts' [];
-    val typ_matches = maps (fn (tys, c) =>
-      tys ~~ map snd (fst (fst (Graph.get_node (snd arities_eqngr') c))))
-      const_matches;
-    val insts = maps (instance_dicts_of thy algebra') typ_matches;
-    val (algebra'', arities_eqngr'') = extend_arities_eqngr thy [] insts arities_eqngr';
-  in (evaluator_lift (evaluator_eqngr algebra'') thm (snd arities_eqngr''), arities_eqngr'') end;
+    val const_matches' = fold (fn (c, ty) =>
+      insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty))) consts' [];
+    val (algebra', arities_eqngr') =
+      extend_arities_eqngr thy consts const_matches' arities_eqngr;
+  in
+    (evaluator_lift (evaluator_eqngr algebra') thm (snd arities_eqngr'),
+      arities_eqngr')
+  end;
 
 fun proto_eval_conv thy =
   let
     fun evaluator_lift evaluator thm1 eqngr =
       let