changed syntax of datatype declarations (curried types for constructor
authorclasohm
Tue Mar 28 12:25:20 1995 +0200 (1995-03-28 ago)
changeset 9775d57287e5e1e
parent 976 14b55f7fbf15
child 978 f7011b47ac38
changed syntax of datatype declarations (curried types for constructor
parameters)
src/HOL/IMP/Com.thy
src/HOL/List.thy
src/HOL/ex/PropLog.thy
src/HOL/ex/String.thy
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/IMP/Com.thy	Tue Mar 28 12:21:10 1995 +0200
     1.2 +++ b/src/HOL/IMP/Com.thy	Tue Mar 28 12:25:20 1995 +0200
     1.3 @@ -19,10 +19,10 @@
     1.4  arities loc :: term
     1.5  
     1.6  datatype
     1.7 -  aexp = N (nat)
     1.8 -       | X (loc)
     1.9 -       | Op1 (n2n, aexp)
    1.10 -       | Op2 (n2n2n, aexp, aexp)
    1.11 +  aexp = N nat
    1.12 +       | X loc
    1.13 +       | Op1 n2n aexp
    1.14 +       | Op2 n2n2n aexp aexp
    1.15  
    1.16  (** Evaluation of arithmetic expressions **)
    1.17  consts  evala    :: "(aexp*state*nat)set"
    1.18 @@ -44,10 +44,10 @@
    1.19  datatype
    1.20    bexp = true
    1.21         | false
    1.22 -       | ROp  (n2n2b, aexp, aexp)
    1.23 -       | noti (bexp)
    1.24 -       | andi (bexp,bexp)	(infixl 60)
    1.25 -       | ori  (bexp,bexp)	(infixl 60)
    1.26 +       | ROp  n2n2b aexp aexp
    1.27 +       | noti bexp
    1.28 +       | andi bexp bexp 	(infixl 60)
    1.29 +       | ori  bexp bexp 	(infixl 60)
    1.30  
    1.31  (** Evaluation of boolean expressions **)
    1.32  consts evalb	:: "(bexp*state*bool)set"	
    1.33 @@ -72,10 +72,10 @@
    1.34  
    1.35  datatype
    1.36    com = skip
    1.37 -      | ":="   (loc,aexp)	 (infixl  60)
    1.38 -      | semic  (com,com)	 ("_; _"  [60, 60] 10)
    1.39 -      | whileC (bexp,com)	 ("while _ do _"  60)
    1.40 -      | ifC    (bexp, com, com)	 ("ifc _ then _ else _"  60)
    1.41 +      | ":="   loc aexp	         (infixl  60)
    1.42 +      | semic  com com	         ("_; _"  [60, 60] 10)
    1.43 +      | whileC bexp com	         ("while _ do _"  60)
    1.44 +      | ifC    bexp com com	 ("ifc _ then _ else _"  60)
    1.45  
    1.46  (** Execution of commands **)
    1.47  consts  evalc    :: "(com*state*state)set"
     2.1 --- a/src/HOL/List.thy	Tue Mar 28 12:21:10 1995 +0200
     2.2 +++ b/src/HOL/List.thy	Tue Mar 28 12:25:20 1995 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  
     2.5  List = Arith +
     2.6  
     2.7 -datatype 'a list = "[]" ("[]") | "#"('a,'a list) (infixr 65)
     2.8 +datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65)
     2.9  
    2.10  consts
    2.11  
     3.1 --- a/src/HOL/ex/PropLog.thy	Tue Mar 28 12:21:10 1995 +0200
     3.2 +++ b/src/HOL/ex/PropLog.thy	Tue Mar 28 12:25:20 1995 +0200
     3.3 @@ -8,7 +8,7 @@
     3.4  
     3.5  PropLog = Finite +
     3.6  datatype
     3.7 -    'a pl = false | var ('a) ("#_" [1000]) | "->" ('a pl,'a pl) (infixr 90)
     3.8 +    'a pl = false | var 'a ("#_" [1000]) | "->" ('a pl) ('a pl) (infixr 90)
     3.9  consts
    3.10    thms :: "'a pl set => 'a pl set"
    3.11    "|-" 	:: "['a pl set, 'a pl] => bool"	(infixl 50)
     4.1 --- a/src/HOL/ex/String.thy	Tue Mar 28 12:21:10 1995 +0200
     4.2 +++ b/src/HOL/ex/String.thy	Tue Mar 28 12:25:20 1995 +0200
     4.3 @@ -11,7 +11,7 @@
     4.4           | H08 | H09 | H0A | H0B | H0C | H0D | H0E | H0F
     4.5  
     4.6  datatype
     4.7 -  char = Char (nibble, nibble)
     4.8 +  char = Char nibble nibble
     4.9  
    4.10  types
    4.11    string = "char list"
     5.1 --- a/src/HOL/thy_syntax.ML	Tue Mar 28 12:21:10 1995 +0200
     5.2 +++ b/src/HOL/thy_syntax.ML	Tue Mar 28 12:25:20 1995 +0200
     5.3 @@ -138,10 +138,12 @@
     5.4  
     5.5    (*parsers*)
     5.6    val tvars = type_args >> map (cat "dtVar");
     5.7 -  val typ =
     5.8 +  val complex_typ =
     5.9      tvars -- (ident>>quote) >> (cat "dtTyp" o mk_pair o apfst mk_list) ||
    5.10      type_var >> cat "dtVar";
    5.11 -  val opt_typs = optional ("(" $$-- list1 typ --$$ ")") [];
    5.12 +  val simple_typ = ident>>(cat "dtTyp" o curry mk_pair "[]" o quote) ||
    5.13 +    type_var >> cat "dtVar";
    5.14 +  val opt_typs = repeat (simple_typ || ("(" $$-- complex_typ --$$ ")"));
    5.15    val constructor = name -- opt_typs -- opt_mixfix;
    5.16  in
    5.17    val datatype_decl =