src/HOL/Tools/Datatype/datatype_case.ML
changeset 46003 c0fe5e8e4864
parent 45898 b619242b0439
child 46059 f805747f8571
equal deleted inserted replaced
46002:b319f1b0c634 46003:c0fe5e8e4864
    10   datatype config = Error | Warning | Quiet
    10   datatype config = Error | Warning | Quiet
    11   type info = Datatype_Aux.info
    11   type info = Datatype_Aux.info
    12   val make_case :  Proof.context -> config -> string list -> term -> (term * term) list -> term
    12   val make_case :  Proof.context -> config -> string list -> term -> (term * term) list -> term
    13   val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
    13   val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
    14   val case_tr: bool -> Proof.context -> term list -> term
    14   val case_tr: bool -> Proof.context -> term list -> term
       
    15   val show_cases: bool Config.T
    15   val case_tr': string -> Proof.context -> term list -> term
    16   val case_tr': string -> Proof.context -> term list -> term
    16   val add_case_tr' : string list -> theory -> theory
    17   val add_case_tr' : string list -> theory -> theory
    17   val setup: theory -> theory
    18   val setup: theory -> theory
    18 end;
    19 end;
    19 
    20 
   412 end;
   413 end;
   413 
   414 
   414 
   415 
   415 (* print translation *)
   416 (* print translation *)
   416 
   417 
       
   418 val show_cases = Attrib.setup_config_bool @{binding show_cases} (K true);
       
   419 
   417 fun case_tr' cname ctxt ts =
   420 fun case_tr' cname ctxt ts =
   418   let
   421   if Config.get ctxt show_cases then
   419     fun mk_clause (pat, rhs) =
   422     let
   420       let val xs = Term.add_frees pat [] in
   423       fun mk_clause (pat, rhs) =
   421         Syntax.const @{syntax_const "_case1"} $
   424         let val xs = Term.add_frees pat [] in
   422           map_aterms
   425           Syntax.const @{syntax_const "_case1"} $
   423             (fn Free p => Syntax_Trans.mark_boundT p
   426             map_aterms
   424               | Const (s, _) => Syntax.const (Lexicon.mark_const s)
   427               (fn Free p => Syntax_Trans.mark_boundT p
   425               | t => t) pat $
   428                 | Const (s, _) => Syntax.const (Lexicon.mark_const s)
   426           map_aterms
   429                 | t => t) pat $
   427             (fn x as Free (s, T) => if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x
   430             map_aterms
   428               | t => t) rhs
   431               (fn x as Free (s, T) => if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x
   429       end;
   432                 | t => t) rhs
   430   in
   433         end;
   431     (case strip_case' ctxt true (list_comb (Syntax.const cname, ts)) of
   434     in
   432       SOME (x, clauses) =>
   435       (case strip_case' ctxt true (list_comb (Syntax.const cname, ts)) of
   433         Syntax.const @{syntax_const "_case_syntax"} $ x $
   436         SOME (x, clauses) =>
   434           foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
   437           Syntax.const @{syntax_const "_case_syntax"} $ x $
   435             (map mk_clause clauses)
   438             foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
   436     | NONE => raise Match)
   439               (map mk_clause clauses)
   437   end;
   440       | NONE => raise Match)
       
   441     end
       
   442   else raise Match;
   438 
   443 
   439 fun add_case_tr' case_names thy =
   444 fun add_case_tr' case_names thy =
   440   Sign.add_advanced_trfuns ([], [],
   445   Sign.add_advanced_trfuns ([], [],
   441     map (fn case_name =>
   446     map (fn case_name =>
   442       let val case_name' = Lexicon.mark_const case_name
   447       let val case_name' = Lexicon.mark_const case_name