src/Tools/Code/code_thingol.ML
changeset 37447 ad3e04f289b6
parent 37446 fc55011cfdfd
child 37448 3bd4b3809bee
     1.1 --- a/src/Tools/Code/code_thingol.ML	Thu Jun 17 10:57:00 2010 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Jun 17 11:33:04 2010 +0200
     1.3 @@ -69,13 +69,10 @@
     1.4      | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
     1.5      | Datatype of string * ((vname * sort) list * (string * itype list) list)
     1.6      | Datatypecons of string * string
     1.7 -    | Class of class * (vname
     1.8 -        * (((class * string) list (*direct superclasses*)
     1.9 -          * (class * string) list) (*indirect superclasses*)
    1.10 -            * (string * itype) list (*class operations*)))
    1.11 +    | Class of class * (vname * ((class * string) list * (string * itype) list))
    1.12      | Classrel of class * class
    1.13      | Classparam of string * class
    1.14 -    | Classinst of (class * (string * (vname * sort) list) (*class and arity*))
    1.15 +    | Classinst of (class * (string * (vname * sort) list) (*class and arity*) )
    1.16            * ((class * (string * (string * dict list list))) list (*super instances*)
    1.17          * ((string * const) * (thm * bool)) list (*class parameter instances*))
    1.18    type program = stmt Graph.T
    1.19 @@ -403,17 +400,17 @@
    1.20  (** statements, abstract programs **)
    1.21  
    1.22  type typscheme = (vname * sort) list * itype;
    1.23 -datatype stmt = (*see also signature*)
    1.24 +datatype stmt =
    1.25      NoStmt
    1.26    | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
    1.27    | Datatype of string * ((vname * sort) list * (string * itype list) list)
    1.28    | Datatypecons of string * string
    1.29 -  | Class of class * (vname * (((class * string) list * (class * string) list) * (string * itype) list))
    1.30 +  | Class of class * (vname * ((class * string) list * (string * itype) list))
    1.31    | Classrel of class * class
    1.32    | Classparam of string * class
    1.33    | Classinst of (class * (string * (vname * sort) list))
    1.34          * ((class * (string * (string * dict list list))) list
    1.35 -      * ((string * const) * (thm * bool)) list);
    1.36 +      * ((string * const) * (thm * bool)) list) (*see also signature*);
    1.37  
    1.38  type program = stmt Graph.T;
    1.39  
    1.40 @@ -596,7 +593,6 @@
    1.41      val stmt_class =
    1.42        fold_map (fn super_class => ensure_class thy algbr eqngr permissive super_class
    1.43          ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)) super_classes
    1.44 -      ##>> pair [] (*FIXME*)
    1.45        ##>> fold_map (fn (c, ty) => ensure_const thy algbr eqngr permissive c
    1.46          ##>> translate_typ thy algbr eqngr permissive ty) cs
    1.47        #>> (fn info => Class (class, (unprefix "'" Name.aT, info)))