--- a/src/Tools/Code/code_eval.ML Tue Jun 15 07:42:48 2010 +0200
+++ b/src/Tools/Code/code_eval.ML Tue Jun 15 08:32:32 2010 +0200
@@ -55,7 +55,7 @@
val value_name = "Value.VALUE.value"
val program' = program
|> Graph.new_node (value_name,
- Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (NONE, true))])))
+ Code_Thingol.Fun (Term.dummy_patternN, ((([], ty), [(([], t), (NONE, true))]), NONE)))
|> fold (curry Graph.add_edge value_name) deps;
val (value_code, [SOME value_name']) = Code_ML.evaluation_code_of thy
(the_default target some_target) "" naming program' [value_name];
--- a/src/Tools/Code/code_haskell.ML Tue Jun 15 07:42:48 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Tue Jun 15 08:32:32 2010 +0200
@@ -115,7 +115,7 @@
end
| print_case tyvars some_thm vars fxy ((_, []), _) =
(brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
- fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) =
+ fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
let
val tyvars = intro_vars (map fst vs) reserved;
fun print_err n =
--- a/src/Tools/Code/code_ml.ML Tue Jun 15 07:42:48 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Tue Jun 15 08:32:32 2010 +0200
@@ -758,7 +758,7 @@
val base' = if upper then first_upper base else base;
val ([base''], nsp') = Name.variants [base'] nsp;
in (base'', nsp') end;
- fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, (tysm as (vs, ty), raw_eqs))) =
+ fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, ((tysm as (vs, ty), raw_eqs), _))) =
let
val eqs = filter (snd o snd) raw_eqs;
val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs
--- a/src/Tools/Code/code_scala.ML Tue Jun 15 07:42:48 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Tue Jun 15 08:32:32 2010 +0200
@@ -129,7 +129,7 @@
(map2 (fn param => fn ty => print_typed tyvars
((str o lookup_var vars) param) ty)
params tys)) implicits) ty, str " ="]
- fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) = (case filter (snd o snd) raw_eqs
+ fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) = (case filter (snd o snd) raw_eqs
of [] =>
let
val (tys, ty') = Code_Thingol.unfold_fun ty;
@@ -351,8 +351,8 @@
module_name reserved raw_module_alias program;
val reserved = make_vars reserved;
fun args_num c = case Graph.get_node program c
- of Code_Thingol.Fun (_, ((_, ty), [])) => (length o fst o Code_Thingol.unfold_fun) ty
- | Code_Thingol.Fun (_, (_, ((ts, _), _) :: _)) => length ts
+ of Code_Thingol.Fun (_, (((_, ty), []), _)) => (length o fst o Code_Thingol.unfold_fun) ty
+ | Code_Thingol.Fun (_, ((_, ((ts, _), _) :: _), _)) => length ts
| Code_Thingol.Datatypecons (_, tyco) =>
let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
in (length o the o AList.lookup (op =) constrs) c end
--- a/src/Tools/Code/code_thingol.ML Tue Jun 15 07:42:48 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML Tue Jun 15 08:32:32 2010 +0200
@@ -66,7 +66,7 @@
datatype stmt =
NoStmt
- | Fun of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
+ | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
| Datatype of string * ((vname * sort) list * (string * itype list) list)
| Datatypecons of string * string
| Class of class * (vname * ((class * string) list * (string * itype) list))
@@ -402,7 +402,7 @@
type typscheme = (vname * sort) list * itype;
datatype stmt =
NoStmt
- | Fun of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
+ | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
| Datatype of string * ((vname * sort) list * (string * itype list) list)
| Datatypecons of string * string
| Class of class * (vname * ((class * string) list * (string * itype) list))
@@ -416,7 +416,7 @@
type program = stmt Graph.T;
fun empty_funs program =
- Graph.fold (fn (name, (Fun (c, (_, [])), _)) => cons c
+ Graph.fold (fn (name, (Fun (c, ((_, []), _)), _)) => cons c
| _ => I) program [];
fun map_terms_bottom_up f (t as IConst _) = f t
@@ -430,8 +430,8 @@
(map_terms_bottom_up f) ps), map_terms_bottom_up f t0));
fun map_terms_stmt f NoStmt = NoStmt
- | map_terms_stmt f (Fun (c, (tysm, eqs))) = Fun (c, (tysm, (map o apfst)
- (fn (ts, t) => (map f ts, f t)) eqs))
+ | map_terms_stmt f (Fun (c, ((tysm, eqs), case_cong))) = Fun (c, ((tysm, (map o apfst)
+ (fn (ts, t) => (map f ts, f t)) eqs), case_cong))
| map_terms_stmt f (stmt as Datatype _) = stmt
| map_terms_stmt f (stmt as Datatypecons _) = stmt
| map_terms_stmt f (stmt as Class _) = stmt
@@ -573,7 +573,7 @@
##>> translate_typ thy algbr eqngr permissive ty
##>> (fold_map (translate_equation thy algbr eqngr permissive) eqns
#>> map_filter I)
- #>> (fn info => Fun (c, info))
+ #>> (fn info => Fun (c, (info, NONE)))
end;
val stmt_const = case Code.get_type_of_constr_or_abstr thy c
of SOME (tyco, _) => stmt_datatypecons tyco
@@ -847,10 +847,10 @@
##>> translate_typ thy algbr eqngr false ty
##>> translate_term thy algbr eqngr false NONE (Code.subst_signatures thy t, NONE)
#>> (fn ((vs, ty), t) => Fun
- (Term.dummy_patternN, ((vs, ty), [(([], t), (NONE, true))])));
+ (Term.dummy_patternN, (((vs, ty), [(([], t), (NONE, true))]), NONE)));
fun term_value (dep, (naming, program1)) =
let
- val Fun (_, (vs_ty, [(([], t), _)])) =
+ val Fun (_, ((vs_ty, [(([], t), _)]), _)) =
Graph.get_node program1 Term.dummy_patternN;
val deps = Graph.imm_succs program1 Term.dummy_patternN;
val program2 = Graph.del_nodes [Term.dummy_patternN] program1;
--- a/src/Tools/nbe.ML Tue Jun 15 07:42:48 2010 +0200
+++ b/src/Tools/nbe.ML Tue Jun 15 08:32:32 2010 +0200
@@ -396,9 +396,9 @@
(* preparing function equations *)
-fun eqns_of_stmt (_, Code_Thingol.Fun (_, (_, []))) =
+fun eqns_of_stmt (_, Code_Thingol.Fun (_, ((_, []), _))) =
[]
- | eqns_of_stmt (const, Code_Thingol.Fun (_, ((vs, _), eqns))) =
+ | eqns_of_stmt (const, Code_Thingol.Fun (_, (((vs, _), eqns), _))) =
[(const, (vs, map fst eqns))]
| eqns_of_stmt (_, Code_Thingol.Datatypecons _) =
[]