--- a/src/HOL/Library/Code_Index.thy Tue Oct 28 17:53:46 2008 +0100
+++ b/src/HOL/Library/Code_Index.thy Wed Oct 29 11:33:40 2008 +0100
@@ -27,6 +27,9 @@
by (rule index_of_nat_inverse)
(unfold index_def, rule UNIV_I)
+lemma [measure_function]:
+ "is_measure nat_of_index" by (rule is_measure_trivial)
+
lemma index:
"(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (index_of_nat n))"
proof
@@ -143,70 +146,73 @@
instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}"
begin
-lemma zero_index_code [code inline, code]:
- "(0\<Colon>index) = Numeral0"
- by (simp add: number_of_index_def Pls_def)
-lemma [code post]: "Numeral0 = (0\<Colon>index)"
- using zero_index_code ..
-
definition [simp, code del]:
"(1\<Colon>index) = index_of_nat 1"
-lemma one_index_code [code inline, code]:
- "(1\<Colon>index) = Numeral1"
- by (simp add: number_of_index_def Pls_def Bit1_def)
-lemma [code post]: "Numeral1 = (1\<Colon>index)"
- using one_index_code ..
-
definition [simp, code del]:
"n + m = index_of_nat (nat_of_index n + nat_of_index m)"
-lemma plus_index_code [code]:
- "index_of_nat n + index_of_nat m = index_of_nat (n + m)"
- by simp
-
definition [simp, code del]:
"n - m = index_of_nat (nat_of_index n - nat_of_index m)"
definition [simp, code del]:
"n * m = index_of_nat (nat_of_index n * nat_of_index m)"
-lemma times_index_code [code]:
- "index_of_nat n * index_of_nat m = index_of_nat (n * m)"
- by simp
-
definition [simp, code del]:
"n div m = index_of_nat (nat_of_index n div nat_of_index m)"
definition [simp, code del]:
"n mod m = index_of_nat (nat_of_index n mod nat_of_index m)"
-lemma div_index_code [code]:
- "index_of_nat n div index_of_nat m = index_of_nat (n div m)"
- by simp
-
-lemma mod_index_code [code]:
- "index_of_nat n mod index_of_nat m = index_of_nat (n mod m)"
- by simp
-
definition [simp, code del]:
"n \<le> m \<longleftrightarrow> nat_of_index n \<le> nat_of_index m"
definition [simp, code del]:
"n < m \<longleftrightarrow> nat_of_index n < nat_of_index m"
-lemma less_eq_index_code [code]:
+instance by default (auto simp add: left_distrib index)
+
+end
+
+lemma zero_index_code [code inline, code]:
+ "(0\<Colon>index) = Numeral0"
+ by (simp add: number_of_index_def Pls_def)
+lemma [code post]: "Numeral0 = (0\<Colon>index)"
+ using zero_index_code ..
+
+lemma one_index_code [code inline, code]:
+ "(1\<Colon>index) = Numeral1"
+ by (simp add: number_of_index_def Pls_def Bit1_def)
+lemma [code post]: "Numeral1 = (1\<Colon>index)"
+ using one_index_code ..
+
+lemma plus_index_code [code nbe]:
+ "index_of_nat n + index_of_nat m = index_of_nat (n + m)"
+ by simp
+
+definition subtract_index :: "index \<Rightarrow> index \<Rightarrow> index" where
+ [simp, code del]: "subtract_index = op -"
+
+lemma subtract_index_code [code nbe]:
+ "subtract_index (index_of_nat n) (index_of_nat m) = index_of_nat (n - m)"
+ by simp
+
+lemma minus_index_code [code]:
+ "n - m = subtract_index n m"
+ by simp
+
+lemma times_index_code [code nbe]:
+ "index_of_nat n * index_of_nat m = index_of_nat (n * m)"
+ by simp
+
+lemma less_eq_index_code [code nbe]:
"index_of_nat n \<le> index_of_nat m \<longleftrightarrow> n \<le> m"
by simp
-lemma less_index_code [code]:
+lemma less_index_code [code nbe]:
"index_of_nat n < index_of_nat m \<longleftrightarrow> n < m"
by simp
-instance by default (auto simp add: left_distrib index)
-
-end
-
lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp
lemma index_of_nat_code [code]:
@@ -222,9 +228,7 @@
lemma index_not_eq_zero: "i \<noteq> index_of_nat 0 \<longleftrightarrow> i \<ge> 1"
by (cases i) auto
-definition
- nat_of_index_aux :: "index \<Rightarrow> nat \<Rightarrow> nat"
-where
+definition nat_of_index_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where
"nat_of_index_aux i n = nat_of_index i + n"
lemma nat_of_index_aux_code [code]:
@@ -235,39 +239,7 @@
"nat_of_index i = nat_of_index_aux i 0"
by (simp add: nat_of_index_aux_def)
-
-text {* Measure function (for termination proofs) *}
-
-lemma [measure_function]:
- "is_measure nat_of_index" by (rule is_measure_trivial)
-
-subsection {* ML interface *}
-
-ML {*
-structure Index =
-struct
-
-fun mk k = HOLogic.mk_number @{typ index} k;
-
-end;
-*}
-
-
-subsection {* Specialized @{term "op - \<Colon> index \<Rightarrow> index \<Rightarrow> index"},
- @{term "op div \<Colon> index \<Rightarrow> index \<Rightarrow> index"} and @{term "op mod \<Colon> index \<Rightarrow> index \<Rightarrow> index"}
- operations *}
-
-definition
- minus_index_aux :: "index \<Rightarrow> index \<Rightarrow> index"
-where
- [code del]: "minus_index_aux = op -"
-
-lemma [code]: "op - = minus_index_aux"
- using minus_index_aux_def ..
-
-definition
- div_mod_index :: "index \<Rightarrow> index \<Rightarrow> index \<times> index"
-where
+definition div_mod_index :: "index \<Rightarrow> index \<Rightarrow> index \<times> index" where
[code del]: "div_mod_index n m = (n div m, n mod m)"
lemma [code]:
@@ -283,6 +255,18 @@
unfolding div_mod_index_def by simp
+subsection {* ML interface *}
+
+ML {*
+structure Index =
+struct
+
+fun mk k = HOLogic.mk_number @{typ index} k;
+
+end;
+*}
+
+
subsection {* Code generator setup *}
text {* Implementation of indices by bounded integers *}
@@ -308,7 +292,7 @@
(OCaml "Pervasives.( + )")
(Haskell infixl 6 "+")
-code_const "minus_index_aux \<Colon> index \<Rightarrow> index \<Rightarrow> index"
+code_const "subtract_index \<Colon> index \<Rightarrow> index \<Rightarrow> index"
(SML "Int.max/ (_/ -/ _,/ 0 : int)")
(OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
(Haskell "max/ (_/ -/ _)/ (0 :: Int)")
--- a/src/HOL/Library/Multiset.thy Tue Oct 28 17:53:46 2008 +0100
+++ b/src/HOL/Library/Multiset.thy Wed Oct 29 11:33:40 2008 +0100
@@ -20,27 +20,19 @@
Abs_multiset_inverse Rep_multiset_inverse Rep_multiset
and [simp] = Rep_multiset_inject [symmetric]
-definition
- Mempty :: "'a multiset" ("{#}") where
- "{#} = Abs_multiset (\<lambda>a. 0)"
+definition Mempty :: "'a multiset" ("{#}") where
+ [code del]: "{#} = Abs_multiset (\<lambda>a. 0)"
-definition
- single :: "'a => 'a multiset" where
- "single a = Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
+definition single :: "'a => 'a multiset" where
+ [code del]: "single a = Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
-declare
- Mempty_def[code del] single_def[code del]
-
-definition
- count :: "'a multiset => 'a => nat" where
+definition count :: "'a multiset => 'a => nat" where
"count = Rep_multiset"
-definition
- MCollect :: "'a multiset => ('a => bool) => 'a multiset" where
+definition MCollect :: "'a multiset => ('a => bool) => 'a multiset" where
"MCollect M P = Abs_multiset (\<lambda>x. if P x then Rep_multiset M x else 0)"
-abbreviation
- Melem :: "'a => 'a multiset => bool" ("(_/ :# _)" [50, 51] 50) where
+abbreviation Melem :: "'a => 'a multiset => bool" ("(_/ :# _)" [50, 51] 50) where
"a :# M == 0 < count M a"
notation (xsymbols)
@@ -51,25 +43,23 @@
translations
"{#x :# M. P#}" == "CONST MCollect M (\<lambda>x. P)"
-definition
- set_of :: "'a multiset => 'a set" where
+definition set_of :: "'a multiset => 'a set" where
"set_of M = {x. x :# M}"
instantiation multiset :: (type) "{plus, minus, zero, size}"
begin
-definition
- union_def[code del]:
+definition union_def [code del]:
"M + N = Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
-definition
- diff_def: "M - N = Abs_multiset (\<lambda>a. Rep_multiset M a - Rep_multiset N a)"
+definition diff_def [code del]:
+ "M - N = Abs_multiset (\<lambda>a. Rep_multiset M a - Rep_multiset N a)"
-definition
- Zero_multiset_def [simp]: "0 = {#}"
+definition Zero_multiset_def [simp]:
+ "0 = {#}"
-definition
- size_def[code del]: "size M = setsum (count M) (set_of M)"
+definition size_def:
+ "size M = setsum (count M) (set_of M)"
instance ..
@@ -207,10 +197,10 @@
subsubsection {* Size *}
-lemma size_empty [simp,code]: "size {#} = 0"
+lemma size_empty [simp]: "size {#} = 0"
by (simp add: size_def)
-lemma size_single [simp,code]: "size {#b#} = 1"
+lemma size_single [simp]: "size {#b#} = 1"
by (simp add: size_def)
lemma finite_set_of [iff]: "finite (set_of M)"
@@ -223,7 +213,7 @@
apply (simp add: Int_insert_left set_of_def)
done
-lemma size_union[simp,code]: "size (M + N::'a multiset) = size M + size N"
+lemma size_union [simp]: "size (M + N::'a multiset) = size M + size N"
apply (unfold size_def)
apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)")
prefer 2
@@ -376,16 +366,16 @@
subsubsection {* Comprehension (filter) *}
-lemma MCollect_empty[simp, code]: "MCollect {#} P = {#}"
+lemma MCollect_empty [simp]: "MCollect {#} P = {#}"
by (simp add: MCollect_def Mempty_def Abs_multiset_inject
in_multiset expand_fun_eq)
-lemma MCollect_single[simp, code]:
+lemma MCollect_single [simp]:
"MCollect {#x#} P = (if P x then {#x#} else {#})"
by (simp add: MCollect_def Mempty_def single_def Abs_multiset_inject
in_multiset expand_fun_eq)
-lemma MCollect_union[simp, code]:
+lemma MCollect_union [simp]:
"MCollect (M+N) f = MCollect M f + MCollect N f"
by (simp add: MCollect_def union_def Abs_multiset_inject
in_multiset expand_fun_eq)
@@ -498,14 +488,11 @@
subsubsection {* Well-foundedness *}
-definition
- mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
- [code del]:"mult1 r =
- {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
+definition mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
+ [code del]: "mult1 r = {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
(\<forall>b. b :# K --> (b, a) \<in> r)}"
-definition
- mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
+definition mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
"mult r = (mult1 r)\<^sup>+"
lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
@@ -715,11 +702,11 @@
instantiation multiset :: (order) order
begin
-definition
- less_multiset_def [code del]: "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
+definition less_multiset_def [code del]:
+ "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
-definition
- le_multiset_def [code del]: "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
+definition le_multiset_def [code del]:
+ "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}"
unfolding trans_def by (blast intro: order_less_trans)
@@ -981,13 +968,11 @@
subsection {* Pointwise ordering induced by count *}
-definition
- mset_le :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<le>#" 50) where
- [code del]: "(A \<le># B) = (\<forall>a. count A a \<le> count B a)"
+definition mset_le :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<le>#" 50) where
+ [code del]: "A \<le># B \<longleftrightarrow> (\<forall>a. count A a \<le> count B a)"
-definition
- mset_less :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where
- [code del]: "(A <# B) = (A \<le># B \<and> A \<noteq> B)"
+definition mset_less :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where
+ [code del]: "A <# B \<longleftrightarrow> A \<le># B \<and> A \<noteq> B"
notation mset_le (infix "\<subseteq>#" 50)
notation mset_less (infix "\<subset>#" 50)
@@ -1448,22 +1433,23 @@
subsection {* Image *}
-definition [code del]: "image_mset f == fold_mset (op + o single o f) {#}"
+definition [code del]:
+ "image_mset f = fold_mset (op + o single o f) {#}"
interpretation image_left_comm: left_commutative ["op + o single o f"]
by (unfold_locales) (simp add:union_ac)
-lemma image_mset_empty [simp, code]: "image_mset f {#} = {#}"
+lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
by (simp add: image_mset_def)
-lemma image_mset_single [simp, code]: "image_mset f {#x#} = {#f x#}"
+lemma image_mset_single [simp]: "image_mset f {#x#} = {#f x#}"
by (simp add: image_mset_def)
lemma image_mset_insert:
"image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
by (simp add: image_mset_def add_ac)
-lemma image_mset_union[simp, code]:
+lemma image_mset_union [simp]:
"image_mset f (M+N) = image_mset f M + image_mset f N"
apply (induct N)
apply simp
@@ -1476,7 +1462,6 @@
lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \<longleftrightarrow> M = {#}"
by (cases M) auto
-
syntax
comprehension1_mset :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
("({#_/. _ :# _#})")
--- a/src/HOL/List.thy Tue Oct 28 17:53:46 2008 +0100
+++ b/src/HOL/List.thy Wed Oct 29 11:33:40 2008 +0100
@@ -3578,7 +3578,7 @@
fun pretty_list literals =
let
val mk_list = Code_Printer.literal_list literals;
- fun pretty pr naming thm pat vars fxy [(t1, _), (t2, _)] =
+ fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] =
case Option.map (cons t1) (implode_list (list_names naming) t2)
of SOME ts => mk_list (map (pr vars Code_Printer.NOBR) ts)
| NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
@@ -3589,7 +3589,7 @@
val mk_list = Code_Printer.literal_list literals;
val mk_char = Code_Printer.literal_char literals;
val mk_string = Code_Printer.literal_string literals;
- fun pretty pr naming thm pat vars fxy [(t1, _), (t2, _)] =
+ fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] =
case Option.map (cons t1) (implode_list (list_names naming) t2)
of SOME ts => (case implode_string (char_name naming, nibble_names naming) mk_char mk_string ts
of SOME p => p
@@ -3600,7 +3600,7 @@
fun pretty_char literals =
let
val mk_char = Code_Printer.literal_char literals;
- fun pretty _ naming thm _ _ _ [(t1, _), (t2, _)] =
+ fun pretty _ naming thm _ _ [(t1, _), (t2, _)] =
case decode_char (nibble_names naming) (t1, t2)
of SOME c => (Code_Printer.str o mk_char) c
| NONE => Code_Printer.nerror thm "Illegal character expression";
@@ -3610,7 +3610,7 @@
let
val mk_char = Code_Printer.literal_char literals;
val mk_string = Code_Printer.literal_string literals;
- fun pretty _ naming thm _ _ _ [(t, _)] =
+ fun pretty _ naming thm _ _ [(t, _)] =
case implode_list (list_names naming) t
of SOME ts => (case implode_string (char_name naming, nibble_names naming) mk_char mk_string ts
of SOME p => p
--- a/src/HOL/Tools/numeral.ML Tue Oct 28 17:53:46 2008 +0100
+++ b/src/HOL/Tools/numeral.ML Wed Oct 29 11:33:40 2008 +0100
@@ -79,7 +79,7 @@
in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
| dest_num _ = Code_Printer.nerror thm "Illegal numeral expression: illegal term";
in dest_num end;
- fun pretty _ naming thm _ _ _ [(t, _)] =
+ fun pretty _ naming thm _ _ [(t, _)] =
(Code_Printer.str o pr_numeral unbounded o the_default 0 o dest_numeral naming thm) t;
in
thy
--- a/src/Pure/Isar/code.ML Tue Oct 28 17:53:46 2008 +0100
+++ b/src/Pure/Isar/code.ML Wed Oct 29 11:33:40 2008 +0100
@@ -462,13 +462,6 @@
cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
in map (Thm.instantiate (instT, [])) thms' end;
-fun certify_const thy c eqns =
- let
- fun cert (eqn as (thm, _)) = if c = Code_Unit.const_eqn thm
- then eqn else error ("Wrong head of defining equation,\nexpected constant "
- ^ Code_Unit.string_of_const thy c ^ "\n" ^ Display.string_of_thm thm)
- in map cert eqns end;
-
fun check_linear (eqn as (thm, linear)) =
if linear then eqn else Code_Unit.bad_thm
("Duplicate variables on left hand side of defining equation:\n"
@@ -542,6 +535,16 @@
in SOME (Logic.varifyT ty) end
| NONE => NONE;
+fun recheck_eqn thy = Code_Unit.error_thm
+ (Code_Unit.assert_linear (is_some o get_datatype_of_constr thy) o apfst (Code_Unit.assert_eqn thy));
+
+fun recheck_eqns_const thy c eqns =
+ let
+ fun cert (eqn as (thm, _)) = if c = Code_Unit.const_eqn thm
+ then eqn else error ("Wrong head of defining equation,\nexpected constant "
+ ^ Code_Unit.string_of_const thy c ^ "\n" ^ Display.string_of_thm thm)
+ in map (cert o recheck_eqn thy) eqns end;
+
fun change_eqns delete c f = (map_exec_purge (SOME [c]) o map_eqns
o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, Lazy.value [])), [])))
o apfst) (fn (_, eqns) => (true, f eqns));
@@ -568,8 +571,7 @@
fun add_eqnl (c, lthms) thy =
let
- val lthms' = certificate thy
- (fn thy => map (Code_Unit.assert_linear) o certify_const thy c) lthms;
+ val lthms' = certificate thy (fn thy => recheck_eqns_const thy c) lthms;
in change_eqns false c (add_lthms lthms') thy end;
val add_default_eqn_attribute = Thm.declaration_attribute
@@ -660,8 +662,7 @@
| apply_functrans thy c functrans eqns = eqns
|> perhaps (perhaps_loop (perhaps_apply functrans))
|> (map o apfst) (AxClass.unoverload thy)
- |> (map o Code_Unit.error_thm) (Code_Unit.assert_linear o apfst (Code_Unit.assert_eqn thy))
- |> certify_const thy c
+ |> recheck_eqns_const thy c
|> (map o apfst) (AxClass.overload thy);
fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
@@ -682,7 +683,7 @@
|> apply_functrans thy c functrans
|> (map o apfst) (Code_Unit.rewrite_eqn pre)
|> (map o apfst) (AxClass.unoverload thy)
- |> map (Code_Unit.assert_linear o apfst (Code_Unit.assert_eqn thy))
+ |> map (recheck_eqn thy)
|> burrow_fst (common_typ_eqns thy)
end;
--- a/src/Pure/Isar/code_unit.ML Tue Oct 28 17:53:46 2008 +0100
+++ b/src/Pure/Isar/code_unit.ML Wed Oct 29 11:33:40 2008 +0100
@@ -38,7 +38,7 @@
(*defining equations*)
val assert_eqn: theory -> thm -> thm
val mk_eqn: theory -> thm -> thm * bool
- val assert_linear: thm * bool -> thm * bool
+ val assert_linear: (string -> bool) -> thm * bool -> thm * bool
val const_eqn: thm -> string
val const_typ_eqn: thm -> string * typ
val head_eqn: theory -> thm -> string * ((string * sort) list * typ)
@@ -377,8 +377,17 @@
((fold o fold_aterms) (fn Var (v, _) => cons v | _ => I) args []))
in (thm, linear) end;
-fun assert_linear (thm, false) = (thm, false)
- | assert_linear (thm, true) = if snd (add_linear thm) then (thm, true)
+fun assert_pat is_cons thm =
+ let
+ val args = (snd o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
+ val _ = (map o map_aterms) (fn t as Const (c, _) => if is_cons c then t
+ else bad_thm ("Not a constructor on left hand side of equation: "
+ ^ quote c ^ ",\n in equation\n" ^ Display.string_of_thm thm)
+ | t => t) args;
+ in thm end;
+
+fun assert_linear is_cons (thm, false) = (thm, false)
+ | assert_linear is_cons (thm, true) = if snd (add_linear (assert_pat is_cons thm)) then (thm, true)
else bad_thm
("Duplicate variables on left hand side of defining equation:\n"
^ Display.string_of_thm thm);
--- a/src/Tools/code/code_haskell.ML Tue Oct 28 17:53:46 2008 +0100
+++ b/src/Tools/code/code_haskell.ML Wed Oct 29 11:33:40 2008 +0100
@@ -59,45 +59,45 @@
Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr);
fun pr_typscheme tyvars (vs, ty) =
Pretty.block (pr_typforall tyvars vs @ pr_typcontext tyvars vs @| pr_typ tyvars NOBR ty);
- fun pr_term tyvars thm pat vars fxy (IConst c) =
- pr_app tyvars thm pat vars fxy (c, [])
- | pr_term tyvars thm pat vars fxy (t as (t1 `$ t2)) =
+ fun pr_term tyvars thm vars fxy (IConst c) =
+ pr_app tyvars thm vars fxy (c, [])
+ | pr_term tyvars thm vars fxy (t as (t1 `$ t2)) =
(case Code_Thingol.unfold_const_app t
- of SOME app => pr_app tyvars thm pat vars fxy app
+ of SOME app => pr_app tyvars thm vars fxy app
| _ =>
brackify fxy [
- pr_term tyvars thm pat vars NOBR t1,
- pr_term tyvars thm pat vars BR t2
+ pr_term tyvars thm vars NOBR t1,
+ pr_term tyvars thm vars BR t2
])
- | pr_term tyvars thm pat vars fxy (IVar v) =
+ | pr_term tyvars thm vars fxy (IVar v) =
(str o Code_Name.lookup_var vars) v
- | pr_term tyvars thm pat vars fxy (t as _ `|-> _) =
+ | pr_term tyvars thm vars fxy (t as _ `|-> _) =
let
val (binds, t') = Code_Thingol.unfold_abs t;
fun pr ((v, pat), ty) = pr_bind tyvars thm BR ((SOME v, pat), ty);
val (ps, vars') = fold_map pr binds vars;
- in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm pat vars' NOBR t') end
- | pr_term tyvars thm pat vars fxy (ICase (cases as (_, t0))) =
+ in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm vars' NOBR t') end
+ | pr_term tyvars thm vars fxy (ICase (cases as (_, t0))) =
(case Code_Thingol.unfold_const_app t0
of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
then pr_case tyvars thm vars fxy cases
- else pr_app tyvars thm pat vars fxy c_ts
+ else pr_app tyvars thm vars fxy c_ts
| NONE => pr_case tyvars thm vars fxy cases)
- and pr_app' tyvars thm pat vars ((c, (_, tys)), ts) = case contr_classparam_typs c
- of [] => (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts
+ and pr_app' tyvars thm vars ((c, (_, tys)), ts) = case contr_classparam_typs c
+ of [] => (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts
| fingerprint => let
val ts_fingerprint = ts ~~ curry Library.take (length ts) fingerprint;
val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
(not o Code_Thingol.locally_monomorphic) t) ts_fingerprint;
- fun pr_term_anno (t, NONE) _ = pr_term tyvars thm pat vars BR t
+ fun pr_term_anno (t, NONE) _ = pr_term tyvars thm vars BR t
| pr_term_anno (t, SOME _) ty =
- brackets [pr_term tyvars thm pat vars NOBR t, str "::", pr_typ tyvars NOBR ty];
+ brackets [pr_term tyvars thm vars NOBR t, str "::", pr_typ tyvars NOBR ty];
in
if needs_annotation then
(str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
- else (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts
+ else (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts
end
- and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const is_cons naming
+ and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const naming
and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
let
@@ -105,12 +105,12 @@
fun pr ((pat, ty), t) vars =
vars
|> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
- |>> (fn p => semicolon [p, str "=", pr_term tyvars thm false vars NOBR t])
+ |>> (fn p => semicolon [p, str "=", pr_term tyvars thm vars NOBR t])
val (ps, vars') = fold_map pr binds vars;
in
Pretty.block_enclose (
str "let {",
- concat [str "}", str "in", pr_term tyvars thm false vars' NOBR t]
+ concat [str "}", str "in", pr_term tyvars thm vars' NOBR t]
) ps
end
| pr_case tyvars thm vars fxy (((td, ty), bs as _ :: _), _) =
@@ -118,10 +118,10 @@
fun pr (pat, t) =
let
val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
- in semicolon [p, str "->", pr_term tyvars thm false vars' NOBR t] end;
+ in semicolon [p, str "->", pr_term tyvars thm vars' NOBR t] end;
in
Pretty.block_enclose (
- concat [str "(case", pr_term tyvars thm false vars NOBR td, str "of", str "{"],
+ concat [str "(case", pr_term tyvars thm vars NOBR td, str "of", str "{"],
str "})"
) (map pr bs)
end
@@ -165,9 +165,9 @@
in
semicolon (
(str o deresolve_base) name
- :: map (pr_term tyvars thm true vars BR) ts
+ :: map (pr_term tyvars thm vars BR) ts
@ str "="
- @@ pr_term tyvars thm false vars NOBR t
+ @@ pr_term tyvars thm vars NOBR t
)
end;
in
@@ -250,7 +250,7 @@
of NONE => semicolon [
(str o deresolve_base) classparam,
str "=",
- pr_app tyvars thm false init_syms NOBR (c_inst, [])
+ pr_app tyvars thm init_syms NOBR (c_inst, [])
]
| SOME (k, pr) =>
let
@@ -266,9 +266,9 @@
(*dictionaries are not relevant at this late stage*)
in
semicolon [
- pr_term tyvars thm false vars NOBR lhs,
+ pr_term tyvars thm vars NOBR lhs,
str "=",
- pr_term tyvars thm false vars NOBR rhs
+ pr_term tyvars thm vars NOBR rhs
]
end;
in
@@ -463,10 +463,10 @@
| pr_monad pr_bind pr (SOME (bind, false), t) vars = vars
|> pr_bind NOBR bind
|>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
- fun pretty pr naming thm pat vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
+ fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
of SOME (bind, t') => let
val (binds, t'') = implode_monad ((the o Code_Thingol.lookup_const naming) c_bind) t'
- val (ps, vars') = fold_map (pr_monad (pr_haskell_bind (K (K pr)) thm) pr) (bind :: binds) vars;
+ val (ps, vars') = fold_map (pr_monad (pr_haskell_bind (K pr) thm) pr) (bind :: binds) vars;
in (brackify fxy o single o Pretty.enclose "do {" "}" o Pretty.breaks) (ps @| pr vars' NOBR t'') end
| NONE => brackify_infix (1, L) fxy
[pr vars (INFX (1, L)) t1, str ">>=", pr vars (INFX (1, X)) t2]
--- a/src/Tools/code/code_ml.ML Tue Oct 28 17:53:46 2008 +0100
+++ b/src/Tools/code/code_ml.ML Wed Oct 29 11:33:40 2008 +0100
@@ -83,40 +83,40 @@
of NONE => pr_tycoexpr fxy (tyco, tys)
| SOME (i, pr) => pr pr_typ fxy tys)
| pr_typ fxy (ITyVar v) = str ("'" ^ v);
- fun pr_term thm pat vars fxy (IConst c) =
- pr_app thm pat vars fxy (c, [])
- | pr_term thm pat vars fxy (IVar v) =
+ fun pr_term thm vars fxy (IConst c) =
+ pr_app thm vars fxy (c, [])
+ | pr_term thm vars fxy (IVar v) =
str (Code_Name.lookup_var vars v)
- | pr_term thm pat vars fxy (t as t1 `$ t2) =
+ | pr_term thm vars fxy (t as t1 `$ t2) =
(case Code_Thingol.unfold_const_app t
- of SOME c_ts => pr_app thm pat vars fxy c_ts
+ of SOME c_ts => pr_app thm vars fxy c_ts
| NONE =>
- brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])
- | pr_term thm pat vars fxy (t as _ `|-> _) =
+ brackify fxy [pr_term thm vars NOBR t1, pr_term thm vars BR t2])
+ | pr_term thm vars fxy (t as _ `|-> _) =
let
val (binds, t') = Code_Thingol.unfold_abs t;
fun pr ((v, pat), ty) =
pr_bind thm NOBR ((SOME v, pat), ty)
#>> (fn p => concat [str "fn", p, str "=>"]);
val (ps, vars') = fold_map pr binds vars;
- in brackets (ps @ [pr_term thm pat vars' NOBR t']) end
- | pr_term thm pat vars fxy (ICase (cases as (_, t0))) =
+ in brackets (ps @ [pr_term thm vars' NOBR t']) end
+ | pr_term thm vars fxy (ICase (cases as (_, t0))) =
(case Code_Thingol.unfold_const_app t0
of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
then pr_case thm vars fxy cases
- else pr_app thm pat vars fxy c_ts
+ else pr_app thm vars fxy c_ts
| NONE => pr_case thm vars fxy cases)
- and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =
+ and pr_app' thm vars (app as ((c, (iss, tys)), ts)) =
if is_cons c then let
val k = length tys
in if k < 2 then
- (str o deresolve) c :: map (pr_term thm pat vars BR) ts
+ (str o deresolve) c :: map (pr_term thm vars BR) ts
else if k = length ts then
- [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term thm pat vars NOBR) ts)]
- else [pr_term thm pat vars BR (Code_Thingol.eta_expand k app)] end else
+ [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term thm vars NOBR) ts)]
+ else [pr_term thm vars BR (Code_Thingol.eta_expand k app)] end else
(str o deresolve) c
- :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts
- and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons naming thm pat vars
+ :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm vars BR) ts
+ and pr_app thm vars = gen_pr_app pr_app' pr_term syntax_const naming thm vars
and pr_bind' ((NONE, NONE), _) = str "_"
| pr_bind' ((SOME v, NONE), _) = str v
| pr_bind' ((NONE, SOME p), _) = p
@@ -128,12 +128,12 @@
fun pr ((pat, ty), t) vars =
vars
|> pr_bind thm NOBR ((NONE, SOME pat), ty)
- |>> (fn p => semicolon [str "val", p, str "=", pr_term thm false vars NOBR t])
+ |>> (fn p => semicolon [str "val", p, str "=", pr_term thm vars NOBR t])
val (ps, vars') = fold_map pr binds vars;
in
Pretty.chunks [
[str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,
- [str ("in"), Pretty.fbrk, pr_term thm false vars' NOBR t'] |> Pretty.block,
+ [str ("in"), Pretty.fbrk, pr_term thm vars' NOBR t'] |> Pretty.block,
str ("end")
]
end
@@ -143,12 +143,12 @@
let
val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
in
- concat [str delim, p, str "=>", pr_term thm false vars' NOBR t]
+ concat [str delim, p, str "=>", pr_term thm vars' NOBR t]
end;
in
(Pretty.enclose "(" ")" o single o brackify fxy) (
str "case"
- :: pr_term thm false vars NOBR td
+ :: pr_term thm vars NOBR td
:: pr "of" b
:: map (pr "|") bs
)
@@ -209,8 +209,8 @@
then [str ":", pr_typ NOBR ty]
else
pr_tyvar_dicts vs_dict
- @ map (pr_term thm true vars BR) ts)
- @ [str "=", pr_term thm false vars NOBR t]
+ @ map (pr_term thm vars BR) ts)
+ @ [str "=", pr_term thm vars NOBR t]
)
end
in
@@ -303,7 +303,7 @@
concat [
(str o pr_label_classparam) classparam,
str "=",
- pr_app thm false reserved_names NOBR (c_inst, [])
+ pr_app thm reserved_names NOBR (c_inst, [])
];
in
semicolon ([
@@ -376,38 +376,38 @@
of NONE => pr_tycoexpr fxy (tyco, tys)
| SOME (i, pr) => pr pr_typ fxy tys)
| pr_typ fxy (ITyVar v) = str ("'" ^ v);
- fun pr_term thm pat vars fxy (IConst c) =
- pr_app thm pat vars fxy (c, [])
- | pr_term thm pat vars fxy (IVar v) =
+ fun pr_term thm vars fxy (IConst c) =
+ pr_app thm vars fxy (c, [])
+ | pr_term thm vars fxy (IVar v) =
str (Code_Name.lookup_var vars v)
- | pr_term thm pat vars fxy (t as t1 `$ t2) =
+ | pr_term thm vars fxy (t as t1 `$ t2) =
(case Code_Thingol.unfold_const_app t
- of SOME c_ts => pr_app thm pat vars fxy c_ts
+ of SOME c_ts => pr_app thm vars fxy c_ts
| NONE =>
- brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])
- | pr_term thm pat vars fxy (t as _ `|-> _) =
+ brackify fxy [pr_term thm vars NOBR t1, pr_term thm vars BR t2])
+ | pr_term thm vars fxy (t as _ `|-> _) =
let
val (binds, t') = Code_Thingol.unfold_abs t;
fun pr ((v, pat), ty) = pr_bind thm BR ((SOME v, pat), ty);
val (ps, vars') = fold_map pr binds vars;
- in brackets (str "fun" :: ps @ str "->" @@ pr_term thm pat vars' NOBR t') end
- | pr_term thm pat vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0
+ in brackets (str "fun" :: ps @ str "->" @@ pr_term thm vars' NOBR t') end
+ | pr_term thm vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0
of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
then pr_case thm vars fxy cases
- else pr_app thm pat vars fxy c_ts
+ else pr_app thm vars fxy c_ts
| NONE => pr_case thm vars fxy cases)
- and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =
+ and pr_app' thm vars (app as ((c, (iss, tys)), ts)) =
if is_cons c then
if length tys = length ts
then case ts
of [] => [(str o deresolve) c]
- | [t] => [(str o deresolve) c, pr_term thm pat vars BR t]
+ | [t] => [(str o deresolve) c, pr_term thm vars BR t]
| _ => [(str o deresolve) c, Pretty.enum "," "(" ")"
- (map (pr_term thm pat vars NOBR) ts)]
- else [pr_term thm pat vars BR (Code_Thingol.eta_expand (length tys) app)]
+ (map (pr_term thm vars NOBR) ts)]
+ else [pr_term thm vars BR (Code_Thingol.eta_expand (length tys) app)]
else (str o deresolve) c
- :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts)
- and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons naming thm pat vars
+ :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm vars BR) ts)
+ and pr_app thm vars = gen_pr_app pr_app' pr_term syntax_const naming thm vars
and pr_bind' ((NONE, NONE), _) = str "_"
| pr_bind' ((SOME v, NONE), _) = str v
| pr_bind' ((NONE, SOME p), _) = p
@@ -420,19 +420,19 @@
vars
|> pr_bind thm NOBR ((NONE, SOME pat), ty)
|>> (fn p => concat
- [str "let", p, str "=", pr_term thm false vars NOBR t, str "in"])
+ [str "let", p, str "=", pr_term thm vars NOBR t, str "in"])
val (ps, vars') = fold_map pr binds vars;
- in Pretty.chunks (ps @| pr_term thm false vars' NOBR t') end
+ in Pretty.chunks (ps @| pr_term thm vars' NOBR t') end
| pr_case thm vars fxy (((td, ty), b::bs), _) =
let
fun pr delim (pat, t) =
let
val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
- in concat [str delim, p, str "->", pr_term thm false vars' NOBR t] end;
+ in concat [str delim, p, str "->", pr_term thm vars' NOBR t] end;
in
(Pretty.enclose "(" ")" o single o brackify fxy) (
str "match"
- :: pr_term thm false vars NOBR td
+ :: pr_term thm vars NOBR td
:: pr "with" b
:: map (pr "|") bs
)
@@ -464,9 +464,9 @@
|> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
(insert (op =)) ts []);
in concat [
- (Pretty.block o Pretty.commas) (map (pr_term thm true vars NOBR) ts),
+ (Pretty.block o Pretty.commas) (map (pr_term thm vars NOBR) ts),
str "->",
- pr_term thm false vars NOBR t
+ pr_term thm vars NOBR t
] end;
fun pr_eqs name ty [] =
let
@@ -493,9 +493,9 @@
(insert (op =)) ts []);
in
concat (
- map (pr_term thm true vars BR) ts
+ map (pr_term thm vars BR) ts
@ str "="
- @@ pr_term thm false vars NOBR t
+ @@ pr_term thm vars NOBR t
)
end
| pr_eqs _ _ (eqs as (eq as (([_], _), _)) :: eqs') =
@@ -615,7 +615,7 @@
concat [
(str o deresolve) classparam,
str "=",
- pr_app thm false reserved_names NOBR (c_inst, [])
+ pr_app thm reserved_names NOBR (c_inst, [])
];
in
concat (
--- a/src/Tools/code/code_printer.ML Tue Oct 28 17:53:46 2008 +0100
+++ b/src/Tools/code/code_printer.ML Wed Oct 29 11:33:40 2008 +0100
@@ -43,12 +43,12 @@
-> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list
val simple_const_syntax: (int * ((fixity -> iterm -> Pretty.T)
-> fixity -> (iterm * itype) list -> Pretty.T)) option -> const_syntax option
- val gen_pr_app: (thm -> bool -> Code_Name.var_ctxt -> const * iterm list -> Pretty.T list)
- -> (thm -> bool -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
- -> (string -> const_syntax option) -> (string -> bool) -> Code_Thingol.naming
- -> thm -> bool -> Code_Name.var_ctxt -> fixity -> const * iterm list -> Pretty.T
+ val gen_pr_app: (thm -> Code_Name.var_ctxt -> const * iterm list -> Pretty.T list)
+ -> (thm -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
+ -> (string -> const_syntax option) -> Code_Thingol.naming
+ -> thm -> Code_Name.var_ctxt -> fixity -> const * iterm list -> Pretty.T
val gen_pr_bind: ((string option * Pretty.T option) * itype -> Pretty.T)
- -> (thm -> bool -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
+ -> (thm -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
-> thm -> fixity
-> (string option * iterm option) * itype -> Code_Name.var_ctxt -> Pretty.T * Code_Name.var_ctxt
@@ -127,26 +127,23 @@
type tyco_syntax = int * ((fixity -> itype -> Pretty.T)
-> fixity -> itype list -> Pretty.T);
type const_syntax = int * ((Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
- -> Code_Thingol.naming -> thm -> bool -> Code_Name.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
+ -> Code_Thingol.naming -> thm -> Code_Name.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
fun simple_const_syntax x = (Option.map o apsnd)
- (fn pretty => fn pr => fn naming => fn thm => fn pat => fn vars => pretty (pr vars)) x;
+ (fn pretty => fn pr => fn naming => fn thm => fn vars => pretty (pr vars)) x;
-fun gen_pr_app pr_app pr_term syntax_const is_cons naming thm pat
- vars fxy (app as ((c, (_, tys)), ts)) =
+fun gen_pr_app pr_app pr_term syntax_const naming thm vars fxy (app as ((c, (_, tys)), ts)) =
case syntax_const c
- of NONE => if pat andalso not (is_cons c) then
- nerror thm "Non-constructor in pattern"
- else brackify fxy (pr_app thm pat vars app)
+ of NONE => brackify fxy (pr_app thm vars app)
| SOME (k, pr) =>
let
- fun pr' fxy ts = pr (pr_term thm pat) naming thm pat vars fxy (ts ~~ curry Library.take k tys);
+ fun pr' fxy ts = pr (pr_term thm) naming thm vars fxy (ts ~~ curry Library.take k tys);
in if k = length ts
then pr' fxy ts
else if k < length ts
then case chop k ts of (ts1, ts2) =>
- brackify fxy (pr' APP ts1 :: map (pr_term thm pat vars BR) ts2)
- else pr_term thm pat vars fxy (Code_Thingol.eta_expand k app)
+ brackify fxy (pr' APP ts1 :: map (pr_term thm vars BR) ts2)
+ else pr_term thm vars fxy (Code_Thingol.eta_expand k app)
end;
fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) ((v, pat), ty : itype) vars =
@@ -157,7 +154,7 @@
val vars' = Code_Name.intro_vars (the_list v) vars;
val vars'' = Code_Name.intro_vars vs vars';
val v' = Option.map (Code_Name.lookup_var vars') v;
- val pat' = Option.map (pr_term thm true vars'' fxy) pat;
+ val pat' = Option.map (pr_term thm vars'' fxy) pat;
in (pr_bind ((v', pat'), ty), vars'') end;
--- a/src/Tools/code/code_thingol.ML Tue Oct 28 17:53:46 2008 +0100
+++ b/src/Tools/code/code_thingol.ML Wed Oct 29 11:33:40 2008 +0100
@@ -667,6 +667,11 @@
| is_undefined _ = false;
fun mk_case (co, n) t =
let
+ val _ = if (is_some o Code.get_datatype_of_constr thy) co then ()
+ else error ("Non-constructor " ^ quote co
+ ^ " encountered in case pattern"
+ ^ (case thm of NONE => ""
+ | SOME thm => ", in equation\n" ^ Display.string_of_thm thm))
val (vs, body) = Term.strip_abs_eta n t;
val selector = list_comb (Const (co, map snd vs ---> dty), map Free vs);
in if is_undefined body then NONE else SOME (selector, body) end;