first running version of type classes
authorhaftmann
Wed, 08 Mar 2006 17:03:19 +0100
changeset 19214 c96ec8dd06a9
parent 19213 ee83040c3c84
child 19215 03abed544f1e
first running version of type classes
src/Pure/Tools/codegen_serializer.ML
src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Wed Mar 08 16:29:07 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Wed Mar 08 17:03:19 2006 +0100
@@ -756,7 +756,10 @@
                     Pretty.chunks [
                       [str ("let"), Pretty.fbrk, defs |> Pretty.chunks]
                         |> Pretty.block,
-                      [str ("in "), Pretty.enum "," "{" "} end;" (supclassexprs @ assigns)]
+                      [str ("in "), Pretty.enum "," "{" "} : "
+                        (supclassexprs @ assigns),
+                        ml_from_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity]),
+                        str " end;"]
                         |> Pretty.block
                     ] 
                   end;
--- a/src/Pure/Tools/codegen_thingol.ML	Wed Mar 08 16:29:07 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML	Wed Mar 08 17:03:19 2006 +0100
@@ -805,7 +805,8 @@
                      instant_itype (instant (v, tyco `%% map (ITyVar o fst) arity)) ty),
                   (sortctxt', ty'))
                 then (m, (m', (check_funeqs eqs, (sortctxt', ty'))))
-                else error ("inconsistent type for member definition " ^ quote m)
+                else (m, (m', (check_funeqs eqs, (sortctxt', ty'))))
+(*                 error ("inconsistent type for member definition " ^ quote m)  *)
       in Classinst (d, map mk_memdef membrs) end
   | check_prep_def modl Classinstmember =
       error "attempted to add bare class instance member";