src/Tools/code/code_thingol.ML

--- a/src/Tools/code/code_thingol.ML	Tue Oct 02 07:59:54 2007 +0200
+++ b/src/Tools/code/code_thingol.ML	Tue Oct 02 07:59:55 2007 +0200
@@ -63,7 +63,7 @@
     | 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)
+    | Class of vname * ((class * string) list * (string * itype) list)
     | Classop of class
     | Classrel of class * class
     | Classinst of (class * (string * (vname * sort) list))
@@ -81,7 +81,7 @@
   val add_eval_def: string (*bind name*) * (iterm * itype) -> code -> code;
 
   val ensure_def: (string -> string) -> (transact -> def * transact) -> string
-    -> string -> transact -> transact;
+    -> transact -> transact;
   val start_transact: (transact -> 'a * transact) -> code -> 'a * code;
 end;
 
@@ -250,7 +250,7 @@
   | 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)
+  | Class of vname * ((class * string) list * (string * itype) list)
   | Classop of class
   | Classrel of class * class
   | Classinst of (class * (string * (vname * sort) list))
@@ -276,8 +276,9 @@
         | 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;
+fun add_dep (NONE, _) = I
+  | add_dep (SOME name1, name2) =
+      if name1 = name2 then I else Graph.add_edge (name1, name2);
 
 val merge_code : code * code -> code = Graph.merge (K true);
 
@@ -309,100 +310,21 @@
  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) =
+fun ensure_def labelled_name defgen 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
+          #> add_dep (dep, name)
           #> curry defgen (SOME name)
           ##> snd
-          #-> (fn def => prep_def def)
-          #-> (fn def => add_def_incr (name, def)
-          #> postprocess_def (name, def))
+          #-> (fn def => add_def_incr (name, def))
       | add_def true =
-          add_dp dep;
+          add_dep (dep, name);
   in
     code
     |> add_def (can (Graph.get_node code) name)