# HG changeset patch # User haftmann # Date 1225276420 -3600 # Node ID a1a436f09ec6c6e24a20bcccb3feec72f3357e39 # Parent 548703affff5796f038ce3f5336891b1f57307cd explicit check for pattern discipline before code translation diff -r 548703affff5 -r a1a436f09ec6 src/HOL/Library/Code_Index.thy --- 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: "(\n\index. PROP P n) \ (\n\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\index) = Numeral0" - by (simp add: number_of_index_def Pls_def) -lemma [code post]: "Numeral0 = (0\index)" - using zero_index_code .. - definition [simp, code del]: "(1\index) = index_of_nat 1" -lemma one_index_code [code inline, code]: - "(1\index) = Numeral1" - by (simp add: number_of_index_def Pls_def Bit1_def) -lemma [code post]: "Numeral1 = (1\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 \ m \ nat_of_index n \ nat_of_index m" definition [simp, code del]: "n < m \ 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\index) = Numeral0" + by (simp add: number_of_index_def Pls_def) +lemma [code post]: "Numeral0 = (0\index)" + using zero_index_code .. + +lemma one_index_code [code inline, code]: + "(1\index) = Numeral1" + by (simp add: number_of_index_def Pls_def Bit1_def) +lemma [code post]: "Numeral1 = (1\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 \ index \ 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 \ index_of_nat m \ n \ m" by simp -lemma less_index_code [code]: +lemma less_index_code [code nbe]: "index_of_nat n < index_of_nat m \ 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 \ index_of_nat 0 \ i \ 1" by (cases i) auto -definition - nat_of_index_aux :: "index \ nat \ nat" -where +definition nat_of_index_aux :: "index \ nat \ 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 - \ index \ index \ index"}, - @{term "op div \ index \ index \ index"} and @{term "op mod \ index \ index \ index"} - operations *} - -definition - minus_index_aux :: "index \ index \ index" -where - [code del]: "minus_index_aux = op -" - -lemma [code]: "op - = minus_index_aux" - using minus_index_aux_def .. - -definition - div_mod_index :: "index \ index \ index \ index" -where +definition div_mod_index :: "index \ index \ index \ 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 \ index \ index \ index" +code_const "subtract_index \ index \ index \ index" (SML "Int.max/ (_/ -/ _,/ 0 : int)") (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ") (Haskell "max/ (_/ -/ _)/ (0 :: Int)") diff -r 548703affff5 -r a1a436f09ec6 src/HOL/Library/Multiset.thy --- 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 (\a. 0)" +definition Mempty :: "'a multiset" ("{#}") where + [code del]: "{#} = Abs_multiset (\a. 0)" -definition - single :: "'a => 'a multiset" where - "single a = Abs_multiset (\b. if b = a then 1 else 0)" +definition single :: "'a => 'a multiset" where + [code del]: "single a = Abs_multiset (\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 (\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 (\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 (\a. Rep_multiset M a + Rep_multiset N a)" -definition - diff_def: "M - N = Abs_multiset (\a. Rep_multiset M a - Rep_multiset N a)" +definition diff_def [code del]: + "M - N = Abs_multiset (\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) = (\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 \ 'a) set => ('a multiset \ 'a multiset) set" where - [code del]:"mult1 r = - {(N, M). \a M0 K. M = M0 + {#a#} \ N = M0 + K \ +definition mult1 :: "('a \ 'a) set => ('a multiset \ 'a multiset) set" where + [code del]: "mult1 r = {(N, M). \a M0 K. M = M0 + {#a#} \ N = M0 + K \ (\b. b :# K --> (b, a) \ r)}" -definition - mult :: "('a \ 'a) set => ('a multiset \ 'a multiset) set" where +definition mult :: "('a \ 'a) set => ('a multiset \ 'a multiset) set" where "mult r = (mult1 r)\<^sup>+" lemma not_less_empty [iff]: "(M, {#}) \ mult1 r" @@ -715,11 +702,11 @@ instantiation multiset :: (order) order begin -definition - less_multiset_def [code del]: "M' < M \ (M', M) \ mult {(x', x). x' < x}" +definition less_multiset_def [code del]: + "M' < M \ (M', M) \ mult {(x', x). x' < x}" -definition - le_multiset_def [code del]: "M' <= M \ M' = M \ M' < (M::'a multiset)" +definition le_multiset_def [code del]: + "M' <= M \ M' = M \ 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 \ 'a multiset \ bool" (infix "\#" 50) where - [code del]: "(A \# B) = (\a. count A a \ count B a)" +definition mset_le :: "'a multiset \ 'a multiset \ bool" (infix "\#" 50) where + [code del]: "A \# B \ (\a. count A a \ count B a)" -definition - mset_less :: "'a multiset \ 'a multiset \ bool" (infix "<#" 50) where - [code del]: "(A <# B) = (A \# B \ A \ B)" +definition mset_less :: "'a multiset \ 'a multiset \ bool" (infix "<#" 50) where + [code del]: "A <# B \ A \# B \ A \ B" notation mset_le (infix "\#" 50) notation mset_less (infix "\#" 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 = {#} \ M = {#}" by (cases M) auto - syntax comprehension1_mset :: "'a \ 'b \ 'b multiset \ 'a multiset" ("({#_/. _ :# _#})") diff -r 548703affff5 -r a1a436f09ec6 src/HOL/List.thy --- 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 diff -r 548703affff5 -r a1a436f09ec6 src/HOL/Tools/numeral.ML --- 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 diff -r 548703affff5 -r a1a436f09ec6 src/Pure/Isar/code.ML --- 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; diff -r 548703affff5 -r a1a436f09ec6 src/Pure/Isar/code_unit.ML --- 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); diff -r 548703affff5 -r a1a436f09ec6 src/Tools/code/code_haskell.ML --- 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] diff -r 548703affff5 -r a1a436f09ec6 src/Tools/code/code_ml.ML --- 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 ( diff -r 548703affff5 -r a1a436f09ec6 src/Tools/code/code_printer.ML --- 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; diff -r 548703affff5 -r a1a436f09ec6 src/Tools/code/code_thingol.ML --- 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;