# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1272151882 -7200
# Node ID 48add8d4d7e5513e180b5837b7bcbdd7bb45b455
# Parent  d3b89f6c086a41b4378c802d526daa6d005d851e
slight tuning

diff -r d3b89f6c086a -r 48add8d4d7e5 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Sat Apr 24 10:00:33 2010 +0200
+++ b/Nominal/NewParser.thy	Sun Apr 25 01:31:22 2010 +0200
@@ -7,32 +7,6 @@
 
 section{* Interface for nominal_datatype *}
 
-text {*
-
-Nominal-Datatype-part:
-
-
-1nd Arg: (string list * binding * mixfix * (binding * typ list * mixfix) list) list
-         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-               type(s) to be defined             constructors list
-               (ty args, name, syn)              (name, typs, syn)
-
-Binder-Function-part:
-
-2rd Arg: (binding * typ option * mixfix) list 
-         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^    
-            binding function(s)           
-              to be defined               
-            (name, type, syn)             
-
-3th Arg:  term list 
-          ^^^^^^^^^
-          the equations of the binding functions
-          (Trueprop equations)
-*}
-
-text {*****************************************************}
-ML {* OuterParse.triple2 *}
 
 ML {* 
 (* nominal datatype parser *)
@@ -50,7 +24,7 @@
 val _ = OuterKeyword.keyword "bind_set"
 val _ = OuterKeyword.keyword "bind_res"
 
-val anno_typ = Scan.option (P.name --| P.$$$ "::") -- P.typ
+val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ
 
 val bind_mode = P.$$$ "bind" || P.$$$ "bind_set" || P.$$$ "bind_res"
 
@@ -58,16 +32,16 @@
   P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple1)
 
 val cnstr_parser =
-  P.binding -- Scan.repeat anno_typ
+  P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tswap
 
 (* datatype parser *)
 val dt_parser =
   (P.type_args -- P.binding -- P.opt_mixfix >> triple1) -- 
-    (P.$$$ "=" |-- P.enum1 "|" (cnstr_parser -- bind_clauses -- P.opt_mixfix >> tswap)) >> tuple
+    (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple
 
 (* binding function parser *)
 val bnfun_parser = 
-  Scan.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([],[])
+  S.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([],[])
 
 (* main parser *)
 val main_parser =
@@ -185,7 +159,6 @@
     | rawify_bclause (BLst (bnds, bdys)) = BLst (rawify_bnds bnds, bdys)
     | rawify_bclause (BSet (bnds, bdys)) = BSet (rawify_bnds bnds, bdys)
     | rawify_bclause (BRes (bnds, bdys)) = BRes (rawify_bnds bnds, bdys)
-
 in
   map (map (map rawify_bclause)) bclauses
 end
@@ -412,6 +385,11 @@
 end
 *}
 
+text {* 
+  adds an empty binding clause for every argument
+  that is not already part of a binding clause
+*}
+
 ML {*
 fun included i bcs = 
 let
@@ -464,7 +442,6 @@
 
 val _ = OuterSyntax.local_theory "nominal_datatype" "test" OuterKeyword.thy_decl
   (main_parser >> nominal_datatype2_cmd)
-
 *}