# HG changeset patch # User wenzelm # Date 1323968920 -3600 # Node ID d73605c829cc6a4d8a0a29c11b3151dd2bfba7b0 # Parent 5f70aaecae26af0ff9e7e0e9c9aec70f8f4438bf clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype; diff -r 5f70aaecae26 -r d73605c829cc src/HOL/Inductive.thy --- a/src/HOL/Inductive.thy Thu Dec 15 17:37:14 2011 +0100 +++ b/src/HOL/Inductive.thy Thu Dec 15 18:08:40 2011 +0100 @@ -11,9 +11,9 @@ "Tools/dseq.ML" "Tools/Datatype/datatype_aux.ML" "Tools/Datatype/datatype_prop.ML" - "Tools/Datatype/datatype_case.ML" ("Tools/Datatype/datatype_abs_proofs.ML") ("Tools/Datatype/datatype_data.ML") + ("Tools/Datatype/datatype_case.ML") ("Tools/Datatype/rep_datatype.ML") ("Tools/primrec.ML") ("Tools/Datatype/datatype_codegen.ML") @@ -277,9 +277,8 @@ text {* Package setup. *} use "Tools/Datatype/datatype_abs_proofs.ML" -use "Tools/Datatype/datatype_data.ML" -setup Datatype_Data.setup - +use "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup +use "Tools/Datatype/datatype_case.ML" setup Datatype_Case.setup use "Tools/Datatype/rep_datatype.ML" use "Tools/Datatype/datatype_codegen.ML" @@ -300,7 +299,7 @@ let (* FIXME proper name context!? *) val x = Free (singleton (Name.variant_list (Term.add_free_names cs [])) "x", dummyT); - val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr_permissive ctxt [x, cs]; + val ft = Datatype_Case.case_tr true ctxt [x, cs]; in lambda x ft end in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end *} diff -r 5f70aaecae26 -r d73605c829cc src/HOL/List.thy --- a/src/HOL/List.thy Thu Dec 15 17:37:14 2011 +0100 +++ b/src/HOL/List.thy Thu Dec 15 18:08:40 2011 +0100 @@ -391,7 +391,7 @@ Syntax.const @{syntax_const "_case1"} $ Syntax.const @{const_syntax dummy_pattern} $ NilC; val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2; - val ft = Datatype_Case.case_tr false Datatype.info_of_constr_permissive ctxt [x, cs]; + val ft = Datatype_Case.case_tr false ctxt [x, cs]; in lambda x ft end; fun abs_tr ctxt (p as Free (s, T)) e opti = diff -r 5f70aaecae26 -r d73605c829cc src/HOL/Tools/Datatype/datatype_case.ML --- a/src/HOL/Tools/Datatype/datatype_case.ML Thu Dec 15 17:37:14 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_case.ML Thu Dec 15 18:08:40 2011 +0100 @@ -9,17 +9,12 @@ sig datatype config = Error | Warning | Quiet type info = Datatype_Aux.info - val make_case: (string * typ -> info option) -> - Proof.context -> config -> string list -> term -> (term * term) list -> - term - val dest_case: (string -> info option) -> bool -> - string list -> term -> (term * (term * term) list) option - val strip_case: (string -> info option) -> bool -> - term -> (term * (term * term) list) option - val case_tr: bool -> (theory -> string * typ -> info option) -> - Proof.context -> term list -> term - val case_tr': (theory -> string -> info option) -> - string -> Proof.context -> term list -> term + val make_case : Proof.context -> config -> string list -> term -> (term * term) list -> term + val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option + val case_tr: bool -> Proof.context -> term list -> term + val case_tr': string -> Proof.context -> term list -> term + val add_case_tr' : string list -> theory -> theory + val setup: theory -> theory end; structure Datatype_Case : DATATYPE_CASE = @@ -147,8 +142,10 @@ (* Translation of pattern terms into nested case expressions. *) -fun mk_case tab ctxt ty_match ty_inst type_of used range_ty = +fun mk_case ctxt ty_match ty_inst type_of used range_ty = let + val tab = Datatype_Data.info_of_constr_permissive (Proof_Context.theory_of ctxt); + val name = singleton (Name.variant_list used) "a"; fun expand constructors used ty ((_, []), _) = raise CASE_ERROR ("mk_case: expand_var_row", ~1) | expand constructors used ty (row as ((prfx, p :: ps), (rhs, tag))) = @@ -215,7 +212,7 @@ else x :: xs) | _ => I) pat []; -fun gen_make_case ty_match ty_inst type_of tab ctxt config used x clauses = +fun gen_make_case ty_match ty_inst type_of ctxt config used x clauses = let fun string_of_clause (pat, rhs) = Syntax.string_of_term ctxt (Syntax.const @{syntax_const "_case1"} $ pat $ rhs); @@ -228,7 +225,7 @@ | _ => case_error "all cases must have the same result type"); val used' = fold add_row_used rows used; val (tags, case_tm) = - mk_case tab ctxt ty_match ty_inst type_of used' rangeT [x] rows + mk_case ctxt ty_match ty_inst type_of used' rangeT [x] rows handle CASE_ERROR (msg, i) => case_error (msg ^ (if i < 0 then "" else "\nIn clause\n" ^ string_of_clause (nth clauses i))); @@ -245,9 +242,9 @@ in -fun make_case tab ctxt = +fun make_case ctxt = gen_make_case (match_type (Proof_Context.theory_of ctxt)) - Envir.subst_term_types fastype_of tab ctxt; + Envir.subst_term_types fastype_of ctxt; val make_case_untyped = gen_make_case (K (K Vartab.empty)) (K (Term.map_types (K dummyT))) (K dummyT); @@ -257,7 +254,7 @@ (* parse translation *) -fun case_tr err tab_of ctxt [t, u] = +fun case_tr err ctxt [t, u] = let val thy = Proof_Context.theory_of ctxt; val intern_const_syntax = Consts.intern_syntax (Proof_Context.consts_of ctxt); @@ -291,12 +288,17 @@ | dest_case2 t = [t]; val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 u)); val case_tm = - make_case_untyped (tab_of thy) ctxt + make_case_untyped ctxt (if err then Error else Warning) [] (fold (fn tT => fn t => Syntax.const @{syntax_const "_constrain"} $ t $ tT) (flat cnstrts) t) cases; in case_tm end - | case_tr _ _ _ ts = case_error "case_tr"; + | case_tr _ _ ts = case_error "case_tr"; + +val trfun_setup = + Sign.add_advanced_trfuns ([], + [(@{syntax_const "_case_syntax"}, case_tr true)], + [], []); (* Pretty printing of nested case expressions *) @@ -306,7 +308,7 @@ local (* FIXME proper name context!? *) -fun gen_dest_case name_of type_of tab d used t = +fun gen_dest_case name_of type_of ctxt d used t = (case apfst name_of (strip_comb t) of (SOME cname, ts as _ :: _) => let @@ -328,6 +330,7 @@ | count_cases (c, (_, body), false) = AList.map_default op aconv (body, []) (cons c); val is_undefined = name_of #> equal (SOME @{const_name undefined}); fun mk_case (c, (xs, body), _) = (list_comb (c, xs), body); + val tab = Datatype_Data.info_of_case (Proof_Context.theory_of ctxt); in (case ty_info tab cname of SOME {constructors, case_name} => @@ -409,9 +412,10 @@ (* print translation *) -fun case_tr' tab_of cname ctxt ts = +fun case_tr' cname ctxt ts = let val thy = Proof_Context.theory_of ctxt; + fun mk_clause (pat, rhs) = let val xs = Term.add_frees pat [] in Syntax.const @{syntax_const "_case1"} $ @@ -424,7 +428,7 @@ | t => t) rhs end; in - (case strip_case' (tab_of thy) true (list_comb (Syntax.const cname, ts)) of + (case strip_case' ctxt true (list_comb (Syntax.const cname, ts)) of SOME (x, clauses) => Syntax.const @{syntax_const "_case_syntax"} $ x $ foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u) @@ -432,4 +436,15 @@ | NONE => raise Match) end; +fun add_case_tr' case_names thy = + Sign.add_advanced_trfuns ([], [], + map (fn case_name => + let val case_name' = Lexicon.mark_const case_name + in (case_name', case_tr' case_name') end) case_names, []) thy; + + +(* theory setup *) + +val setup = trfun_setup; + end; diff -r 5f70aaecae26 -r d73605c829cc src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Thu Dec 15 17:37:14 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Thu Dec 15 18:08:40 2011 +0100 @@ -24,10 +24,6 @@ val mk_case_names_exhausts: descr -> string list -> attribute list val interpretation : (config -> string list -> theory -> theory) -> theory -> theory val interpretation_data : config * string list -> theory -> theory - val make_case : Proof.context -> Datatype_Case.config -> string list -> term -> - (term * term) list -> term - val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option - val add_case_tr' : string list -> theory -> theory val setup: theory -> theory end; @@ -198,27 +194,6 @@ end; -(* translation rules for case *) - -fun make_case ctxt = - Datatype_Case.make_case (info_of_constr_permissive (Proof_Context.theory_of ctxt)) ctxt; - -fun strip_case ctxt = - Datatype_Case.strip_case (info_of_case (Proof_Context.theory_of ctxt)); - -fun add_case_tr' case_names thy = - Sign.add_advanced_trfuns ([], [], - map (fn case_name => - let val case_name' = Lexicon.mark_const case_name in - (case_name', Datatype_Case.case_tr' info_of_case case_name') - end) case_names, []) thy; - -val trfun_setup = - Sign.add_advanced_trfuns ([], - [(@{syntax_const "_case_syntax"}, Datatype_Case.case_tr true info_of_constr_permissive)], - [], []); - - (** document antiquotation **) @@ -262,7 +237,6 @@ (** setup theory **) val setup = - trfun_setup #> antiq_setup #> Datatype_Interpretation.init; diff -r 5f70aaecae26 -r d73605c829cc src/HOL/Tools/Datatype/rep_datatype.ML --- a/src/HOL/Tools/Datatype/rep_datatype.ML Thu Dec 15 17:37:14 2011 +0100 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML Thu Dec 15 18:08:40 2011 +0100 @@ -99,9 +99,9 @@ ((Binding.empty, flat (distinct @ inject)), [Induct.induct_simp_add])] @ named_rules @ unnamed_rules) |> snd - |> Datatype_Data.add_case_tr' case_names |> Datatype_Data.register dt_infos |> Datatype_Data.interpretation_data (config, dt_names) + |> Datatype_Case.add_case_tr' case_names |> pair dt_names end; diff -r 5f70aaecae26 -r d73605c829cc src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Dec 15 17:37:14 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Dec 15 18:08:40 2011 +0100 @@ -663,7 +663,7 @@ val v = Free (name, T); val v' = Free (name', T); in - lambda v (Datatype.make_case ctxt Datatype_Case.Quiet [] v + lambda v (Datatype_Case.make_case ctxt Datatype_Case.Quiet [] v [(HOLogic.mk_tuple out_ts, if null eqs'' then success_t else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $ @@ -949,7 +949,7 @@ in (pattern, compilation) end - val switch = Datatype.make_case ctxt Datatype_Case.Quiet [] inp_var + val switch = Datatype_Case.make_case ctxt Datatype_Case.Quiet [] inp_var ((map compile_single_case switched_clauses) @ [(xt, mk_empty compfuns (HOLogic.mk_tupleT outTs))]) in diff -r 5f70aaecae26 -r d73605c829cc src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Dec 15 17:37:14 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Dec 15 18:08:40 2011 +0100 @@ -412,7 +412,7 @@ end fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) = - Datatype.make_case ctxt Datatype_Case.Quiet [] (Free (x, T)) (map (fn (t, c) => + Datatype_Case.make_case ctxt Datatype_Case.Quiet [] (Free (x, T)) (map (fn (t, c) => (t, mk_case_term ctxt (p - 1) qs' c)) cs) | mk_case_term ctxt p ((@{const_name All}, (x, T)) :: qs') (Universal_Counterexample (t, c)) = if p = 0 then t else mk_case_term ctxt (p - 1) qs' c