gkp

1 files changed, 95 insertions, 82 deletions

diff --git a/language/l2.ott b/language/l2.ott
index d1bf5793..031cfb5a 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -291,7 +291,7 @@ base_kind :: 'BK_' ::=
   | Endian                                     :: :: endian
   | Effects                                    :: :: effects
 
-kind :: '' ::=  
+kind :: 'K_' ::=  
   {{ com kinds}}
   {{ aux _ l }}
   | base_kind1 -> ... -> base_kindn            :: :: kind
@@ -305,7 +305,7 @@ nexp :: 'Nexp_' ::=
   | num                                 :: :: constant
   | nexp1 * nexp2                       :: :: times {{ com must be linear after normalisation... except for the type of *, ahem }}
   | nexp1 + nexp2                       :: :: sum
-  | 2 ^ nexp                            :: :: exp
+  | 2 ** nexp                            :: :: exp
   | ( nexp )                            :: S :: paren  {{ icho [[nexp]] }}
 
 endian :: 'End_' ::=  
@@ -380,11 +380,11 @@ typ_sugar :: 'Typ_sugar_' ::=
   | [ nexp '..' nexp' ]  :: :: enum2 {{ com sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} }}
 % use .. not - to avoid ambiguity with nexp -
 % total maps and vectors indexed by finite subranges of nat
-  | enummap nexp1 nexp2 endian typ :: :: enummap 
-% probably some sugar for enummap types, using [ ] similarly to enums:
+  | vector nexp1 nexp2 endian typ :: :: vector 
+% probably some sugar for vector types, using [ ] similarly to enums:
 % (but with .. not : in the former, to avoid confusion...)
-  | typ [ nexp ]  :: :: enummap2
-  | typ [ nexp : nexp' ] :: :: enummap3
+  | typ [ nexp ]  :: :: vector2
+  | typ [ nexp : nexp' ] :: :: vector3
 % ...so bit [ nexp ] etc is just an instance of that
   | list typ :: :: list
   | set typ  :: :: set
@@ -414,27 +414,25 @@ nexp_constraint :: 'NC_' ::=
 % Note only id on the left and constants on the right in a
 % finite-set-bound, as we don't think we need anything more
 
-opt_kind :: 'ki_ant_' ::=
+kinded_id :: 'KOpt_' ::=
   {{ com optionally kind-annotated identifier }}
   | id	 	    		   	      :: :: none
-  | id : kind				      :: :: kind
-  | ( opt_kind ) 			      :: S :: paren {{ icho [[opt_kind]] }}
+  | kind id				      :: :: kind
+  | ( kinded_id ) 			      :: S :: paren {{ icho [[kinded_id]] }}
 
-typquant :: 'TQ_' ::= 
+typquant :: 'TypQ_' ::= 
   {{ aux _ l }}
-  | forall opt_kind1 ... opt_kindn . nexp_constraint1 , ... , nexp_constrainti . :: :: Ts {{ texlong }}
-
-% TODO those ids have to have optional kind annotations
+  | forall kinded_id1 ... kinded_idn . nexp_constraint1 , ... , nexp_constrainti . :: :: tq {{ texlong }}
 
 % WHY ARE CONSTRAINTS HERE AND NOT IN THE KIND LANGUAGE
 
-  | forall opt_kind1 ... opt_kindn . ::  ::  Ts_no_constraint {{ com sugar }}
-  |                           ::  ::  Ts_no_forall     {{ com sugar }}
+  | forall kinded_id1 ... kinded_idn . ::  ::  no_constraint {{ com sugar }}
+  |                           ::  ::  no_forall     {{ com sugar }}
 
-typschm :: 'TS_' ::=
+typschm :: 'TypSchm_' ::=
     {{ com Type schemes  }}
   {{ aux _ l }}
-  |  typquant typ                                                       :: :: Ts
+  |  typquant typ                                                       :: :: ts
 
 
 
@@ -443,43 +441,43 @@ typschm :: 'TS_' ::=
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 grammar
-ctor_def :: '' ::=
+ctor_def :: 'CT_' ::=
   {{ com Datatype definition clauses }}
-  | id : typschm                                       :: :: Cte
+  | id : typschm                                       :: :: ct
 % but we could get away with disallowing constraints in typschm, we
 % think - if it's useful to do that
 
-enum_opt :: 'Enum_' ::=
+enum_opt :: 'EnumOpt_' ::=
   |      :: :: empty
   | enum :: :: enum
 
-tdefbody :: 'Te_' ::=
-  {{ com Type definition bodies }}
-  | typschm                                                     :: :: abbrev
-    {{ com Type abbreviations }}
-  | typquant <| id1 : typ1 ; ... ; idn : typn semi_opt |>     :: :: record
-    {{ com Record types }}
-  | enumeration_flag_opt '|' ctor_def1 '|' ... '|' ctor_defn            :: :: variant
-    {{ com Variant types }}
-
-naming_scheme_opt {{ tex \ottnt{name}^{?} }} :: 'Name_sect_' ::=
-  {{ com Optional variable-naming-scheme specification for variables of defined type }} 
-  |                                                   :: :: none
-  | [ name = regexp ]                                 :: :: some
-
-type_def :: '' ::=
-  {{ com Type definitions }}
-  | type id : kind naming_scheme_opt = tdefbody                                :: :: Td
-%  | enumeration id naming_scheme_opt = tdefbody                               ::   :: Td2
-% the enumeration is sugar for something that uses an enum flag, where the type system will restrict the tdefbody to be a simple enum...
-
+%% tdefbody :: 'TD_' ::=
+%%   {{ com Type definition bodies }}
+%%   | typschm                                                     :: :: abbrev
+%%     {{ com Type abbreviations }}
+%%   | typquant <| id1 : typ1 ; ... ; idn : typn semi_opt |>     :: :: record
+%%     {{ com Record types }}
+%%   | enumeration_flag_opt '|' ctor_def1 '|' ... '|' ctor_defn            :: :: variant
+%%     {{ com Variant types }}
+%% 
+%% naming_scheme_opt {{ tex \ottnt{name}^{?} }} :: 'Name_sect_' ::=
+%%   {{ com Optional variable-naming-scheme specification for variables of defined type }} 
+%%   |                                                   :: :: none
+%%   | [ name = regexp ]                                 :: :: some
+%% 
+%% type_def :: '' ::=
+%%   {{ com Type definitions }}
+%%   | type id : kind naming_scheme_opt = tdefbody                                :: :: Td
+%% %  | enumeration id naming_scheme_opt = tdefbody                               ::   :: Td2
+%% % the enumeration is sugar for something that uses an enum flag, where the type system will restrict the tdefbody to be a simple enum...
+%% 
 
 % TODO: do we need mutually recursive type definitions?  
 
 
 %%% OR, IN C STYLE
 
-c_tdefbody :: 'C_Te_' ::=
+tdef :: 'TD_' ::=
   {{ com Type definition bodies }}
   | typedef id naming_scheme_opt = typschm                                        :: :: abbrev
     {{ com Type abbreviations }}
@@ -570,8 +568,8 @@ pat :: 'P_' ::=
     {{ com Single variable and constructor patterns }}
 % OR?  do we invent something ghastly including a union keyword?  Perhaps not...
 
-  | <| fpat1 ; ... ; fpatn semi_opt |>                  :: :: record
-    {{ com Record patterns }}
+%  | <| fpat1 ; ... ; fpatn semi_opt |>                  :: :: record
+%    {{ com Record patterns }}
 % OR
   | struct { fpat1 ; ... ; fpatn semi_opt }                  :: :: c_record
     {{ com C-style struct patterns }}
@@ -579,10 +577,14 @@ pat :: 'P_' ::=
 %Patterns for vectors
 %Should these be the same since vector syntax has changed, and lists have also changed?
 
-  | [| pat1 ; .. ; patn semi_opt |]                     :: :: vector
+  | [ pat1 , .. , patn  ]                     :: :: vector
+   {{ com Vector patterns }}
+
+  | [ num1 = pat1 , .. , numn = patn  ]                     :: :: vector_indexed
    {{ com Vector patterns }}
 
-  | [| pat1 .. patn |]                                  :: :: vector_concat
+% cf ntoes for this
+  |  pat1 : .. : patn                                   :: :: vector_concat
   {{ com Concatenated vector patterns }} 
 
   | ( pat1 , .... , patn )                              :: :: tup
@@ -590,10 +592,10 @@ pat :: 'P_' ::=
   | [| pat1 , .. , patn |]	                        :: :: list
     {{ com List patterns }}
   | ( pat )                                             :: :: paren
-  | pat1 '::' pat2                                      :: :: cons
-    {{ com Cons patterns }}
-  | id '+' num                                         :: :: num_add
-    {{ com constant addition patterns }}
+%  | pat1 '::' pat2                                      :: :: cons
+%    {{ com Cons patterns }}
+%  | id '+' num                                         :: :: num_add
+%    {{ com constant addition patterns }}
   | lit                                                 :: :: lit
     {{ com Literal constant patterns }}
 
@@ -640,28 +642,30 @@ exp :: 'E_' ::=
 
 
 
-% enummaps
-  | [ exp1 , ... , expn ]                             :: :: enummap
+% vectors
+  | [ exp1 , ... , expn ]                             :: :: vector
+% endianness comes from global command-line option???
 
-  | [ num1 = exp1 , ... , numn = expn ]               :: :: enummap_e
+  | [ num1 = exp1 , ... , numn = expn ]               :: :: vector_indexed
+% num1 .. numn must be a consecutive list of naturals
 
-% we pick [ ] not { } for enummap literals for consistency with their
+% we pick [ ] not { } for vector literals for consistency with their
 % array-like access syntax, in contrast to the C which has funny
 % syntax for array literals.  We don't have to preserve [ ] for lists
 % as we don't expect to use lists very much. 
 
-  | exp [ exp' ]                                      :: :: enummap_access
-  {{ com enummap access }}
+  | exp [ exp' ]                                      :: :: vector_access
+  {{ com vector access }}
 
-  | exp [ exp1 '..' exp2 ]                            :: :: enummap_subrange
-  {{ com Subenummap extraction }}
+  | exp [ exp1 : exp2 ]                            :: :: vector_subrange
+  {{ com Subvector extraction }}
   % do we want to allow a comma-separated list of such thingies?  
 
-  | [ exp with exp1 = exp2 ]                          :: :: enummap_update 
-  {{ com enummap functional update }}
+  | [ exp with exp1 = exp2 ]                          :: :: vector_update 
+  {{ com vector functional update }}
 
-  | [ exp with exp1 .. exp2 = exp3 ]                          :: :: enummap_update_range
-  {{ com enummap functional subrange update (with another enummap)}}
+  | [ exp with exp1 : exp2 = exp3 ]                          :: :: vector_update_range
+  {{ com vector functional subrange update (with another vector)}}
   % do we want a functional update form with a comma-separated list of such?
 
 
@@ -702,7 +706,7 @@ exp :: 'E_' ::=
     {{ com Pattern matching expressions }}
 %  | ( typ ) exp                                      :: :: Typed
 %    {{ com Type-annotated expressions }}
-  | c_letbind in exp                                  :: :: let
+  | letbind in exp                                  :: :: let
     {{ com Let expressions }}
 
   | lexp := exp                                      :: :: assign
@@ -711,8 +715,8 @@ exp :: 'E_' ::=
 lexp :: 'LEXP_' ::=
     | id                                                  :: :: ident
     {{ com Identifiers }}
-    | lexp [ exp ]  :: ::                         enummap
-    | lexp [ exp1 '..' exp2 ]  :: ::              enummap_range
+    | lexp [ exp ]  :: ::                         vector
+    | lexp [ exp1 : exp2 ]  :: ::              vector_range
     % maybe comma-sep such lists too
     | lexp . id :: :: field  
 
@@ -804,43 +808,43 @@ grammar
 
 %%%%% C-ish style %%%%%%%%%%
 
-c_tannot_opt :: 'C_typ_annot_' ::=
+tannot_opt :: 'Typ_annot_opt_' ::=
   {{ com Optional type annotations }}
   |                                             :: :: none
   | typ_quant typ                               :: :: some 
 
-c_funcl :: 'C_FCL_' ::=
+funcl :: 'FCL_' ::=
   {{ com Function clauses }}
   {{ aux _ l }}
   | id pat = exp                   :: :: Funcl
 
-c_rec_opt :: '' ::=
+rec_opt :: 'Rec_' ::=
   {{ aux _ l }}
   |                                             :: :: nonrec
   | rec                                         :: :: rec
 
-c_effects_opt :: '' ::=
+effects_opt :: 'Effects_opt_' ::=
   {{ aux _ l }}
   |                                             :: :: pure {{ com sugar for pure }}
   | effects                                     :: :: nonpure
 
-c_fundef :: 'C_FD_' ::=
+fundef :: 'FD_' ::=
   {{ com Function definition}}
   {{ aux _ l }}
-  | function c_rec_opt c_tannot_opt c_effects_opt c_funcl1 and ... and c_funcln :: :: function {{ texlong }}  {{ com function definition }}
-% TODO note that the typ in the c_tannot_opt is the *result* type, not
+  | function rec_opt tannot_opt effects_opt funcl1 and ... and funcln :: :: function {{ texlong }}  {{ com function definition }}
+% TODO note that the typ in the tannot_opt is the *result* type, not
 %  the type of the whole function.  The argument type comes from the
-%  pattern in the c_funcl
+%  pattern in the funcl
 % TODO the above is ok for single functions, but not for mutually
-%  recursive functions - the c_tannot_opt scopes over all the c_funcli,
+%  recursive functions - the tannot_opt scopes over all the funcli,
 %  which is ok for the typ_quant part but not for the typ part
 
-c_letbind :: 'LB_' ::=
+letbind :: 'LB_' ::=
   {{ com Let bindings }}
   {{ aux _ l }}
-  | typschm id = exp                                :: :: val_exp
+  | typschm id = exp                                :: :: val_explicit
     {{ com Value binding }}
-  | let id = exp                                    :: :: val_imp
+  | let id = exp                                    :: :: val_implicit
     {{ com value binding with implicit type }}
 
 
@@ -868,24 +872,33 @@ default_typing_spec :: 'DT_' ::=
 def :: 'DEF_' ::=
   {{ com Top-level definitions }}
   {{ aux _ l }}
-  | type_def                                                    :: :: type_def
+  | type_def                                                    :: :: type
     {{ com Type definition }}
-  | c_fundef                                                   :: :: fun_def
+  | fundef                                                   :: :: fundef
     {{ com Function definition }}
-  | c_letbind                                                   :: :: val_def
+  | letbind                                                   :: :: val
     {{ com Value definition }}
-  | val_spec                                                    :: :: spec_def
+  | val_spec                                                    :: :: spec
     {{ com Top-level type constraint }}
-  | default_typing_spec                                         :: :: default_def
+  | default_typing_spec                                         :: :: default
     {{ com default kind and type assumptions }}
   | register typ id                                   :: :: reg_dec
     {{ com Register declaration }}
 
+  | split function rec_opt tannot_opt effects_opt id   :: :: split_function
+
+  | function clause funcl  :: :: split_funcl
+
+  | end id  :: :: split_end
+
+  | split typedef id naming_scheme_opt = const union typquant :: :: split_variant
+
+  | union member id =  typ id'  :: :: split_unioncl
 
 defs :: '' ::=
   {{ com Definition sequences }}
   {{ aux _ l }}
-  | def1  .. defn                  :: :: Defs
+  | def1  .. defn                 :: :: Defs