src/Tools/Code/code_thingol.ML
changeset 37437 4202e11ae7dc
parent 37431 e9004a3e0d94
child 37440 a5d44161ba2a
     1.1 --- a/src/Tools/Code/code_thingol.ML	Tue Jun 15 07:42:48 2010 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Jun 15 08:32:32 2010 +0200
     1.3 @@ -66,7 +66,7 @@
     1.4  
     1.5    datatype stmt =
     1.6        NoStmt
     1.7 -    | Fun of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
     1.8 +    | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
     1.9      | Datatype of string * ((vname * sort) list * (string * itype list) list)
    1.10      | Datatypecons of string * string
    1.11      | Class of class * (vname * ((class * string) list * (string * itype) list))
    1.12 @@ -402,7 +402,7 @@
    1.13  type typscheme = (vname * sort) list * itype;
    1.14  datatype stmt =
    1.15      NoStmt
    1.16 -  | Fun of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
    1.17 +  | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
    1.18    | Datatype of string * ((vname * sort) list * (string * itype list) list)
    1.19    | Datatypecons of string * string
    1.20    | Class of class * (vname * ((class * string) list * (string * itype) list))
    1.21 @@ -416,7 +416,7 @@
    1.22  type program = stmt Graph.T;
    1.23  
    1.24  fun empty_funs program =
    1.25 -  Graph.fold (fn (name, (Fun (c, (_, [])), _)) => cons c
    1.26 +  Graph.fold (fn (name, (Fun (c, ((_, []), _)), _)) => cons c
    1.27                 | _ => I) program [];
    1.28  
    1.29  fun map_terms_bottom_up f (t as IConst _) = f t
    1.30 @@ -430,8 +430,8 @@
    1.31          (map_terms_bottom_up f) ps), map_terms_bottom_up f t0));
    1.32  
    1.33  fun map_terms_stmt f NoStmt = NoStmt
    1.34 -  | map_terms_stmt f (Fun (c, (tysm, eqs))) = Fun (c, (tysm, (map o apfst)
    1.35 -      (fn (ts, t) => (map f ts, f t)) eqs))
    1.36 +  | map_terms_stmt f (Fun (c, ((tysm, eqs), case_cong))) = Fun (c, ((tysm, (map o apfst)
    1.37 +      (fn (ts, t) => (map f ts, f t)) eqs), case_cong))
    1.38    | map_terms_stmt f (stmt as Datatype _) = stmt
    1.39    | map_terms_stmt f (stmt as Datatypecons _) = stmt
    1.40    | map_terms_stmt f (stmt as Class _) = stmt
    1.41 @@ -573,7 +573,7 @@
    1.42          ##>> translate_typ thy algbr eqngr permissive ty
    1.43          ##>> (fold_map (translate_equation thy algbr eqngr permissive) eqns
    1.44            #>> map_filter I)
    1.45 -        #>> (fn info => Fun (c, info))
    1.46 +        #>> (fn info => Fun (c, (info, NONE)))
    1.47        end;
    1.48      val stmt_const = case Code.get_type_of_constr_or_abstr thy c
    1.49       of SOME (tyco, _) => stmt_datatypecons tyco
    1.50 @@ -847,10 +847,10 @@
    1.51        ##>> translate_typ thy algbr eqngr false ty
    1.52        ##>> translate_term thy algbr eqngr false NONE (Code.subst_signatures thy t, NONE)
    1.53        #>> (fn ((vs, ty), t) => Fun
    1.54 -        (Term.dummy_patternN, ((vs, ty), [(([], t), (NONE, true))])));
    1.55 +        (Term.dummy_patternN, (((vs, ty), [(([], t), (NONE, true))]), NONE)));
    1.56      fun term_value (dep, (naming, program1)) =
    1.57        let
    1.58 -        val Fun (_, (vs_ty, [(([], t), _)])) =
    1.59 +        val Fun (_, ((vs_ty, [(([], t), _)]), _)) =
    1.60            Graph.get_node program1 Term.dummy_patternN;
    1.61          val deps = Graph.imm_succs program1 Term.dummy_patternN;
    1.62          val program2 = Graph.del_nodes [Term.dummy_patternN] program1;