# HG changeset patch # User blanchet # Date 1402427757 -7200 # Node ID d9be905d62833944df1ac5929bb6cfe4063198f3 # Parent c7b06cdf108a9a3a21ad78240118175ea3aacc13 changed syntax of map: and rel: arguments to BNF-based datatypes diff -r c7b06cdf108a -r d9be905d6283 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Tue Jun 10 19:51:00 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Tue Jun 10 21:15:57 2014 +0200 @@ -374,9 +374,12 @@ context early begin (*>*) - datatype_new (set: 'a) list (map: map rel: list_all2) = + datatype_new (set: 'a) list = null: Nil | Cons (hd: 'a) (tl: "'a list") + for + map: map + rel: list_all2 where "tl Nil = Nil" @@ -440,9 +443,12 @@ text {* \blankline *} - datatype_new (set: 'a) list (map: map rel: list_all2) = + datatype_new (set: 'a) list = null: Nil ("[]") | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65) + for + map: map + rel: list_all2 text {* \noindent @@ -472,10 +478,12 @@ @{rail \ @@{command datatype_new} target? @{syntax dt_options}? \ - (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') + @'and') \ - (@'where' (@{syntax prop} + '|'))? + (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') \ + @{syntax map_rel}? (@'where' (prop + '|'))? + @'and') ; @{syntax_def dt_options}: '(' (('discs_sels' | 'no_code') + ',') ')' + ; + @{syntax_def map_rel}: @'for' ((('map' | 'rel') ':' name) +) \} \medskip @@ -513,11 +521,9 @@ define, its type parameters, and additional information: @{rail \ - @{syntax_def dt_name}: @{syntax tyargs}? name @{syntax map_rel}? mixfix? + @{syntax_def dt_name}: @{syntax tyargs}? name mixfix? ; @{syntax_def tyargs}: typefree | '(' (('dead' | name ':')? typefree + ',') ')' - ; - @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')' \} \medskip @@ -620,7 +626,7 @@ \end{itemize} An alternative to @{command datatype_compat} is to use the old package's -\keyw{rep\_datatype} command. The associated proof obligations must then be +\keyw{rep\_\allowbreak datatype} command. The associated proof obligations must then be discharged manually. *} @@ -1555,9 +1561,12 @@ definition of lazy lists: *} - codatatype (lset: 'a) llist (map: lmap rel: llist_all2) = + codatatype (lset: 'a) llist = lnull: LNil | LCons (lhd: 'a) (ltl: "'a llist") + for + map: lmap + rel: llist_all2 where "ltl LNil = LNil" @@ -1568,8 +1577,11 @@ infinite streams: *} - codatatype (sset: 'a) stream (map: smap rel: stream_all2) = + codatatype (sset: 'a) stream = SCons (shd: 'a) (stl: "'a stream") + for + map: smap + rel: stream_all2 text {* \noindent @@ -2559,8 +2571,8 @@ \end{matharray} @{rail \ - @@{command bnf_axiomatization} target? @{syntax tyargs}? name @{syntax map_rel}? \ - @{syntax wit_types}? mixfix? + @@{command bnf_axiomatization} target? @{syntax tyargs}? name @{syntax wit_types}? \ + mixfix? @{syntax map_rel}? ; @{syntax_def wit_types}: '[' 'wits' ':' types ']' \} @@ -2648,7 +2660,7 @@ @{rail \ @@{command free_constructors} target? @{syntax dt_options} \ name 'for' (@{syntax fc_ctor} + '|') \ - (@'where' (@{syntax prop} + '|'))? + (@'where' (prop + '|'))? ; @{syntax_def fc_ctor}: (name ':')? term (name * ) \} diff -r c7b06cdf108a -r d9be905d6283 src/HOL/BNF_Examples/ListF.thy --- a/src/HOL/BNF_Examples/ListF.thy Tue Jun 10 19:51:00 2014 +0200 +++ b/src/HOL/BNF_Examples/ListF.thy Tue Jun 10 21:15:57 2014 +0200 @@ -12,9 +12,12 @@ imports Main begin -datatype_new 'a listF (map: mapF rel: relF) = +datatype_new 'a listF = NilF | Conss (hdF: 'a) (tlF: "'a listF") +for + map: mapF + rel: relF where "tlF NilF = NilF" diff -r c7b06cdf108a -r d9be905d6283 src/HOL/BNF_Examples/Stream.thy --- a/src/HOL/BNF_Examples/Stream.thy Tue Jun 10 19:51:00 2014 +0200 +++ b/src/HOL/BNF_Examples/Stream.thy Tue Jun 10 21:15:57 2014 +0200 @@ -12,8 +12,11 @@ imports "~~/src/HOL/Library/Nat_Bijection" begin -codatatype (sset: 'a) stream (map: smap rel: stream_all2) = +codatatype (sset: 'a) stream = SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65) +for + map: smap + rel: stream_all2 (*for code generation only*) definition smember :: "'a \ 'a stream \ bool" where diff -r c7b06cdf108a -r d9be905d6283 src/HOL/BNF_Examples/Stream_Processor.thy --- a/src/HOL/BNF_Examples/Stream_Processor.thy Tue Jun 10 19:51:00 2014 +0200 +++ b/src/HOL/BNF_Examples/Stream_Processor.thy Tue Jun 10 21:15:57 2014 +0200 @@ -150,7 +150,7 @@ section {* Generalization to an Arbitrary BNF as Codomain *} -bnf_axiomatization ('a, 'b) F (map: F) +bnf_axiomatization ('a, 'b) F for map: F notation BNF_Def.convol ("<_ , _>") diff -r c7b06cdf108a -r d9be905d6283 src/HOL/Library/bnf_axiomatization.ML --- a/src/HOL/Library/bnf_axiomatization.ML Tue Jun 10 19:51:00 2014 +0200 +++ b/src/HOL/Library/bnf_axiomatization.ML Tue Jun 10 21:15:57 2014 +0200 @@ -108,13 +108,13 @@ @{keyword "]"} || Scan.succeed []; val parse_bnf_axiomatization = - parse_type_args_named_constrained -- Parse.binding -- parse_map_rel_bindings -- - parse_witTs -- Parse.opt_mixfix; + parse_type_args_named_constrained -- Parse.binding -- parse_witTs -- Parse.opt_mixfix -- + parse_map_rel_bindings; val _ = Outer_Syntax.local_theory @{command_spec "bnf_axiomatization"} "bnf declaration" (parse_bnf_axiomatization >> - (fn ((((bsTs, b), (mapb, relb)), witTs), mx) => + (fn ((((bsTs, b), witTs), mx), (mapb, relb)) => bnf_axiomatization_cmd bsTs b mx mapb relb witTs #> snd)); end; diff -r c7b06cdf108a -r d9be905d6283 src/HOL/List.thy --- a/src/HOL/List.thy Tue Jun 10 19:51:00 2014 +0200 +++ b/src/HOL/List.thy Tue Jun 10 21:15:57 2014 +0200 @@ -8,9 +8,12 @@ imports Presburger Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product begin -datatype_new (set: 'a) list (map: map rel: list_all2) = +datatype_new (set: 'a) list = Nil ("[]") | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65) +for + map: map + rel: list_all2 where "tl [] = []" diff -r c7b06cdf108a -r d9be905d6283 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Jun 10 19:51:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Jun 10 21:15:57 2014 +0200 @@ -72,8 +72,9 @@ BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> BNF_FP_Util.fp_result * local_theory) -> (bool * bool) - * ((((((binding option * (typ * sort)) list * binding) * (binding * binding)) * mixfix) - * ((binding, binding * typ) Ctr_Sugar.ctr_spec * mixfix) list) * term list) list -> + * ((((((binding option * (typ * sort)) list * binding) * mixfix) + * ((binding, binding * typ) Ctr_Sugar.ctr_spec * mixfix) list) * (binding * binding)) + * term list) list -> local_theory -> local_theory val parse_co_datatype_cmd: BNF_Util.fp_kind -> (mixfix list -> binding list -> binding list -> binding list list -> binding list -> (string * sort) list -> typ list * typ list list -> @@ -245,16 +246,12 @@ reassoc_conjs (thm RS @{thm conj_assoc[THEN iffD1]}) handle THM _ => thm; -type co_datatype_spec = - (((((binding option * (typ * sort)) list * binding) * (binding * binding)) * mixfix) - * ((binding, binding * typ) ctr_spec * mixfix) list) * term list; - fun type_args_named_constrained_of_spec (((((ncAs, _), _), _), _), _) = ncAs; fun type_binding_of_spec (((((_, b), _), _), _), _) = b; -fun map_binding_of_spec ((((_, (b, _)), _), _), _) = b; -fun rel_binding_of_spec ((((_, (_, b)), _), _), _) = b; -fun mixfix_of_spec (((_, mx), _), _) = mx; -fun mixfixed_ctr_specs_of_spec ((_, mx_ctr_specs), _) = mx_ctr_specs; +fun mixfix_of_spec ((((_, mx), _), _), _) = mx; +fun mixfixed_ctr_specs_of_spec (((_, mx_ctr_specs), _), _) = mx_ctr_specs; +fun map_binding_of_spec ((_, (b, _)), _) = b; +fun rel_binding_of_spec ((_, (_, b)), _) = b; fun sel_default_eqs_of_spec (_, ts) = ts; fun add_nesty_bnf_names Us = @@ -1547,8 +1544,8 @@ Parse.enum1 "|" (parse_ctr_spec Parse.binding parse_ctr_arg -- Parse.opt_mixfix); val parse_spec = - parse_type_args_named_constrained -- Parse.binding -- parse_map_rel_bindings -- - Parse.opt_mixfix -- (@{keyword "="} |-- parse_ctr_specs) -- parse_sel_default_eqs; + parse_type_args_named_constrained -- Parse.binding -- Parse.opt_mixfix -- + (@{keyword "="} |-- parse_ctr_specs) -- parse_map_rel_bindings -- parse_sel_default_eqs; val parse_co_datatype = parse_ctr_options -- Parse.and_list1 parse_spec; diff -r c7b06cdf108a -r d9be905d6283 src/HOL/Tools/BNF/bnf_util.ML --- a/src/HOL/Tools/BNF/bnf_util.ML Tue Jun 10 19:51:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_util.ML Tue Jun 10 21:15:57 2014 +0200 @@ -308,9 +308,9 @@ | extract_map_rel (s, _) = error ("Unknown label " ^ quote s ^ " (expected \"map\" or \"rel\")"); val parse_map_rel_bindings = - @{keyword "("} |-- Scan.repeat parse_map_rel_binding --| @{keyword ")"} - >> (fn ps => fold extract_map_rel ps no_map_rel) || - Scan.succeed no_map_rel; + @{keyword "for"} |-- Scan.repeat parse_map_rel_binding + >> (fn ps => fold extract_map_rel ps no_map_rel) + || Scan.succeed no_map_rel; (*TODO: is this really different from Typedef.add_typedef_global?*)