wib

2 files changed, 75 insertions, 59 deletions

diff --git a/language/l2.ott b/language/l2.ott
index 0e0e3ce6..50c14c9c 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -170,6 +170,13 @@ id :: '' ::=
   {{ aux _ l }}
   | x                           :: :: id
   | ( x )                       :: :: deIid {{ com remove infix status }}
+% Note: we have just a single namespace. We don't want the same
+% identifier to be reused as a type name or variable, expression
+% variable, and field name.  We don't enforce any lexical convention
+% on type variables (or variables of other kinds)
+% We don't enforce a lexical convention on infix operators, as some of the 
+% targets use alphabetical infix operators. 
+
 
 %% 
 %% x_l {{ tex \ottnt{x}^{l} }} , y_l {{ tex \ottnt{y}^{l} }} , z_l {{ tex \ottnt{z}^{l} }} , name :: '' ::=
@@ -288,7 +295,7 @@ base_kind :: 'BK_' ::=
   {{ aux _ l }}
   | Type                                       :: :: type    {{ com kind of types  }} 
   | Nat                                        :: :: nat     {{ com kind of natural number size expressions  }} 
-  | Endian                                     :: :: endian  {{ com kind of endianness specifications  }} 
+  | Order                                     :: :: order  {{ com kind of vector order specifications  }} 
   | Effects                                    :: :: effects {{ com kind of effect sets  }} 
 
 kind :: 'K_' ::=  
@@ -299,7 +306,7 @@ kind :: 'K_' ::=
 
     
 nexp :: 'Nexp_' ::=  
-  {{ com expression of kind Nat, for vector sizes and origins }}
+  {{ com expression of kind $[[Nat]]$, for vector sizes and origins }}
   {{ aux _ l }}
   | id                                  :: :: id          {{ com identifier }}
   | num                                 :: :: constant     {{ com constant }}
@@ -309,13 +316,13 @@ nexp :: 'Nexp_' ::=
   | 2 ** nexp                            :: :: exp         {{ com exponential }}
   | ( nexp )                            :: S :: paren  {{ icho [[nexp]] }}
 
-endian :: 'End_' ::=  
-  {{ com endianness specifications}}
+order :: 'Ord_' ::=  
+  {{ com vector order specifications, of kind $[[Order]]$}}
   {{ aux _ l }}
   | id                                  :: :: id  {{ com identifier }}
   | inc                                 :: :: inc  {{ com increasing (little-endian) }}
   | dec                                 :: :: dec  {{ com decreasing (big-endian) }}
-  | ( endian )                             :: S :: paren {{ icho [[endian]] }}
+  | ( order )                             :: S :: paren {{ icho [[order]] }}
 
 effect :: 'Effect_' ::=
   {{ com effect }}
@@ -330,7 +337,7 @@ effect :: 'Effect_' ::=
 
 
 effects :: 'Effects_' ::=
-  {{ com effect set }}
+  {{ com effect set, of kind $[[Effects]]$ }}
   {{ aux _ l }}
  | id                                  :: :: var
  | { effect1 , .. , effectn }           :: :: set {{ com effect set }}
@@ -340,7 +347,7 @@ effects :: 'Effects_' ::=
 
 
 typ :: 'Typ_' ::=
-  {{ com Constructor of kind Type }}
+  {{ com Type expressions, of kind $[[Type]]$ }}
   | _                                           :: :: wild
     {{ com Unspecified type }}
   | id                                         :: :: var
@@ -360,7 +367,7 @@ typ_arg :: 'Typ_arg_' ::=
   {{ com Type constructor arguments of all kinds }}
   | nexp       :: :: nexp
   | typ        :: :: typ
-  | endian     :: :: endian
+  | order     :: :: order
   | effects    :: :: effects
 
 % plus more for l-value/r-value pairs, as introduced by the L3 'compound' declarations   ... ref typ
@@ -376,16 +383,16 @@ typ_lib :: 'Typ_lib_' ::=
   | nat :: :: nat {{ com natural numbers 0,1,2,... }}
   | string :: :: string {{ com UTF8 strings }}
 % finite subranges of nat
-  | enum nexp1 nexp2 endian :: :: enum  {{ com natural numbers [[nexp2]] .. [[nexp2]]+[[nexp1]]-1, ordered by [[endian]] }}
+  | enum nexp1 nexp2 order :: :: enum  {{ com natural numbers [[nexp2]] .. [[nexp2]]+[[nexp1]]-1, ordered by [[order]] }}
   | [ nexp ]             :: :: enum1 {{ com sugar for \texttt{enum nexp 0 inc} }}
   | [ 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
-  | vector nexp1 nexp2 endian typ :: :: vector {{ com vector of [[typ]], indexed by natural range }}
+  | vector nexp1 nexp2 order typ :: :: vector {{ com vector of [[typ]], indexed by natural range }}
 % probably some sugar for vector types, using [ ] similarly to enums:
 % (but with .. not : in the former, to avoid confusion...)
   | typ [ nexp ]  :: :: vector2 {{ com sugar for vector indexed by [ [[nexp]] ] }}
-  | typ [ nexp : nexp' ] :: :: vector3 {{ com sugar for vector indexed by [ [[nexp]]:[[nexp']] ] }}
+  | typ [ nexp : nexp' ] :: :: vector3 {{ com sugar for vector indexed by [ [[nexp]]..[[nexp']] ] }}
 % ...so bit [ nexp ] etc is just an instance of that
   | list typ :: :: list {{ com list of [[typ]] }}
   | set typ  :: :: set  {{ com finite set of [[typ]] }}
@@ -405,7 +412,7 @@ Typ_fn <= Typ_tup
 grammar
 
 nexp_constraint :: 'NC_' ::=
-  {{ com contraint over kind Nat }}
+  {{ com constraint over kind $[[Nat]]$ }}
   {{ aux _ l }}
   | nexp = nexp'                                :: :: fixed
   | nexp >= nexp'                               :: :: bounded_ge
@@ -422,16 +429,16 @@ kinded_id :: 'KOpt_' ::=
   | ( kinded_id ) 			      :: S :: paren {{ icho [[kinded_id]] }}
 
 typquant :: 'TypQ_' ::= 
-  {{ aux _ l }}
+  {{ aux _ l }} {{ com type quantifiers and constraints}}
   | forall kinded_id1 ... kinded_idn . nexp_constraint1 , ... , nexp_constrainti . :: :: tq {{ texlong }}
 
 % WHY ARE CONSTRAINTS HERE AND NOT IN THE KIND LANGUAGE
 
-  | forall kinded_id1 ... kinded_idn . ::  ::  no_constraint {{ com sugar }}
-  |                           ::  ::  no_forall     {{ com sugar }}
+  | forall kinded_id1 ... kinded_idn . ::  ::  no_constraint {{ com sugar, omitting constraints}}
+  |                           ::  ::  no_forall     {{ com sugar, omitting quantifier and constraints }}
 
 typschm :: 'TypSchm_' ::=
-    {{ com Type schemes  }}
+    {{ com type scheme  }}
   {{ aux _ l }}
   |  typquant typ                                                       :: :: ts
 
@@ -626,7 +633,8 @@ exp :: 'E_' ::=
   {{ com Expression }}
   {{ aux _ l }}  
 
-  | { exp1 ; ... ; expn }                               ::   :: block {{ com block (parsing conflict with structs?) }}
+  | { exp1 ; ... ; expn }                               :: :: block {{ com block (parsing conflict with structs?) }}
+% maybe we really should have indentation-sensitive syntax :-)  (given that some of the targets do)
 
   | id                                                  :: :: id
     {{ com identifier }}
@@ -634,22 +642,29 @@ exp :: 'E_' ::=
   | lit                                                 :: :: lit
     {{ com literal constant }}
 
-  | exp1 exp2                                           :: :: app
+  | ( typ ) exp                                         :: :: cast
+    {{ com cast }}
+
+  | exp exp1 ... expn                                   :: :: app
     {{ com function application }}
-  | exp1 id exp2                                        :: :: infix
+% Note: fully applied function application only
+% We might restrict exp to be an identifier
+% We might require expn to have outermost parentheses (but not two sets if it's a tuple)
+
+  | exp1 id exp2                                        :: :: app_infix
     {{ com infix function application }}
  
-  | ( exp1 , .... , expn )                              :: :: tup
+  | ( exp1 , .... , expn )                              :: :: tuple
     {{ com tuple }}
 
   | if exp1 then exp2 else exp3                         :: :: if
     {{ com conditional }}
 
-
-
 % vectors
   | [ exp1 , ... , expn ]                             :: :: vector {{ com vector (indexed from 0) }}
-% endianness comes from global command-line option???
+% order comes from global command-line option???
+% here the expi are of type 'a and the result is a vector of 'a, whereas in exp1 : ... : expn 
+% the expi and the result are both of type vector of 'a 
 
   | [ num1 = exp1 , ... , numn = expn ]               :: :: vector_indexed {{ com vector (indexed consecutively) }}
 % num1 .. numn must be a consecutive list of naturals
@@ -662,22 +677,22 @@ exp :: 'E_' ::=
   | exp [ exp' ]                                      :: :: vector_access
   {{ com vector access }}
 
-  | exp [ exp1 : exp2 ]                            :: :: vector_subrange
+  | exp [ exp1 : exp2 ]                               :: :: vector_subrange
   {{ com subvector extraction }}
   % do we want to allow a comma-separated list of such thingies?  
 
   | [ exp with exp1 = exp2 ]                          :: :: vector_update 
   {{ com vector functional update }}
 
-  | [ exp with exp1 : exp2 = exp3 ]                          :: :: vector_update_range
+  | [ exp with exp1 : exp2 = exp3 ]                   :: :: vector_update_subrange
   {{ com vector subrange update (with vector)}}
   % do we want a functional update form with a comma-separated list of such?
 
 
 % lists 
-  | [| exp1 , ..  , expn |]                    :: :: list
+  | [| exp1 , ..  , expn |]                           :: :: list
   {{ com list }}
-  | exp1 '::' exp2                                      :: :: cons
+  | exp1 '::' exp2                                    :: :: cons
     {{ com cons }}
 
 
@@ -689,9 +704,9 @@ exp :: 'E_' ::=
 
   | { fexps }                                         :: :: record
     {{ com struct }}
-  | { exp with fexps }                                :: :: recup
+  | { exp with fexps }                                :: :: record_update
     {{ com functional update of struct }}
-  | exp . id                                            :: :: field
+  | exp . id                                          :: :: field
     {{ com field projection from struct  }}
 
 %Expressions for creating and accessing vectors
@@ -852,10 +867,10 @@ fundef :: 'FD_' ::=
 letbind :: 'LB_' ::=
   {{ com Let binding }}
   {{ aux _ l }}
-  | typschm id = exp                                :: :: val_explicit
-    {{ com value binding with explicit type }}
-  | let id = exp                                    :: :: val_implicit
-    {{ com value binding with implicit type }}
+  | typschm pat = exp                                :: :: val_explicit
+    {{ com value binding, explicit type ([[pat]] must be total)}}
+  | let pat = exp                                    :: :: val_implicit
+    {{ com value binding, implicit type ([[pat]] must be total)}}
 
 
 val_spec :: 'VS_' ::=
diff --git a/src/ast.ml b/src/ast.ml
index f1294016..f7454253 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -58,7 +58,7 @@ type
 base_kind_aux =  (* base kind *)
    BK_type of terminal (* kind of types *)
  | BK_nat of terminal (* kind of natural number size expressions *)
- | BK_endian of terminal (* kind of endianness specifications *)
+ | BK_order of terminal (* kind of vector order specifications *)
  | BK_effects of terminal (* kind of effect sets *)
 
 
@@ -84,7 +84,7 @@ effect_aux =  (* effect *)
 
 
 type 
-nexp_aux =  (* expression of kind Nat, for vector sizes and origins *)
+nexp_aux =  (* expression of kind $_$, for vector sizes and origins *)
    Nexp_id of id (* identifier *)
  | Nexp_constant of terminal * int (* constant *)
  | Nexp_times of nexp * terminal * nexp (* product *)
@@ -106,7 +106,7 @@ effect =
 
 
 type 
-nexp_constraint_aux =  (* contraint over kind Nat *)
+nexp_constraint_aux =  (* constraint over kind $_$ *)
    NC_fixed of nexp * terminal * nexp
  | NC_bounded_ge of nexp * terminal * nexp
  | NC_bounded_le of nexp * terminal * nexp
@@ -119,16 +119,16 @@ kind =
 
 
 type 
-effects_aux =  (* effect set *)
+effects_aux =  (* effect set, of kind $_$ *)
    Effects_var of id
  | Effects_set of terminal * (effect * terminal) list * terminal (* effect set *)
 
 
 type 
-endian_aux =  (* endianness specifications *)
-   End_id of id (* identifier *)
- | End_inc of terminal (* increasing (little-endian) *)
- | End_dec of terminal (* decreasing (big-endian) *)
+order_aux =  (* vector order specifications, of kind $_$ *)
+   Ord_id of id (* identifier *)
+ | Ord_inc of terminal (* increasing (little-endian) *)
+ | Ord_dec of terminal (* decreasing (big-endian) *)
 
 
 type 
@@ -148,19 +148,19 @@ effects =
 
 
 type 
-endian = 
-   End_aux of endian_aux * l
+order = 
+   Ord_aux of order_aux * l
 
 
 type 
-typquant_aux = 
+typquant_aux =  (* type quantifiers and constraints *)
    TypQ_tq of terminal * (kinded_id) list * terminal * (nexp_constraint * terminal) list * terminal
- | TypQ_no_constraint of terminal * (kinded_id) list * terminal (* sugar *)
- | TypQ_no_forall (* sugar *)
+ | TypQ_no_constraint of terminal * (kinded_id) list * terminal (* sugar, omitting constraints *)
+ | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
 
 
 type 
-typ =  (* Constructor of kind Type *)
+typ =  (* Type expressions, of kind $_$ *)
    Typ_wild of terminal (* Unspecified type *)
  | Typ_var of id (* Type variable *)
  | Typ_fn of typ * terminal * typ * effects (* Function type (first-order only in user code) *)
@@ -170,7 +170,7 @@ typ =  (* Constructor of kind Type *)
 and typ_arg =  (* Type constructor arguments of all kinds *)
    Typ_arg_nexp of nexp
  | Typ_arg_typ of typ
- | Typ_arg_endian of endian
+ | Typ_arg_order of order
  | Typ_arg_effects of effects
 
 
@@ -180,7 +180,7 @@ typquant =
 
 
 type 
-typschm_aux =  (* Type schemes *)
+typschm_aux =  (* type scheme *)
    TypSchm_ts of typquant * typ
 
 
@@ -232,20 +232,21 @@ exp_aux =  (* Expression *)
    E_block of terminal * (exp * terminal) list * terminal (* block (parsing conflict with structs?) *)
  | E_id of id (* identifier *)
  | E_lit of lit (* literal constant *)
- | E_app of exp * exp (* function application *)
- | E_infix of exp * id * exp (* infix function application *)
- | E_tup of terminal * (exp * terminal) list * terminal (* tuple *)
+ | E_cast of terminal * typ * terminal * exp (* cast *)
+ | E_app of exp * (exp) list (* function application *)
+ | E_app_infix of exp * id * exp (* infix function application *)
+ | E_tuple of terminal * (exp * terminal) list * terminal (* tuple *)
  | E_if of terminal * exp * terminal * exp * terminal * exp (* conditional *)
  | E_vector of terminal * (exp * terminal) list * terminal (* vector (indexed from 0) *)
  | E_vector_indexed of terminal * ((terminal * int * terminal * exp) * terminal) list * terminal (* vector (indexed consecutively) *)
  | E_vector_access of exp * terminal * exp * terminal (* vector access *)
  | E_vector_subrange of exp * terminal * exp * terminal * exp * terminal (* subvector extraction *)
  | E_vector_update of terminal * exp * terminal * exp * terminal * exp * terminal (* vector functional update *)
- | E_vector_update_range of terminal * exp * terminal * exp * terminal * exp * terminal * exp * terminal (* vector subrange update (with vector) *)
+ | E_vector_update_subrange of terminal * exp * terminal * exp * terminal * exp * terminal * exp * terminal (* vector subrange update (with vector) *)
  | E_list of terminal * (exp * terminal) list * terminal (* list *)
  | E_cons of exp * terminal * exp (* cons *)
  | E_record of terminal * fexps * terminal (* struct *)
- | E_recup of terminal * exp * terminal * fexps * terminal (* functional update of struct *)
+ | E_record_update of terminal * exp * terminal * fexps * terminal (* functional update of struct *)
  | E_field of exp * terminal * id (* field projection from struct *)
  | E_case of terminal * exp * terminal * ((terminal * pexp)) list * terminal (* pattern matching *)
  | E_let of letbind * terminal * exp (* let expression *)
@@ -279,8 +280,8 @@ and pexp =
    Pat_aux of pexp_aux * l
 
 and letbind_aux =  (* Let binding *)
-   LB_val_explicit of typschm * id * terminal * exp (* value binding with explicit type *)
- | LB_val_implicit of terminal * id * terminal * exp (* value binding with implicit type *)
+   LB_val_explicit of typschm * pat * terminal * exp (* value binding, explicit type (pat must be total) *)
+ | LB_val_implicit of terminal * pat * terminal * exp (* value binding, implicit type (pat must be total) *)
 
 and letbind = 
    LB_aux of letbind_aux * l
@@ -382,12 +383,12 @@ typ_lib_aux =  (* library types and syntactic sugar for them *)
  | Typ_lib_bit of terminal (* pure bit values (not mutable bits) *)
  | Typ_lib_nat of terminal (* natural numbers 0,1,2,... *)
  | Typ_lib_string of terminal * Ulib.UTF8.t (* UTF8 strings *)
- | Typ_lib_enum of terminal * nexp * nexp * endian (* natural numbers nexp .. nexp+nexp-1, ordered by endian *)
+ | Typ_lib_enum of terminal * nexp * nexp * order (* natural numbers nexp .. nexp+nexp-1, ordered by order *)
  | Typ_lib_enum1 of terminal * nexp * terminal (* sugar for \texttt{enum nexp 0 inc} *)
  | Typ_lib_enum2 of terminal * nexp * terminal * nexp * terminal (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *)
- | Typ_lib_vector of terminal * nexp * nexp * endian * typ (* vector of typ, indexed by natural range *)
+ | Typ_lib_vector of terminal * nexp * nexp * order * typ (* vector of typ, indexed by natural range *)
  | Typ_lib_vector2 of typ * terminal * nexp * terminal (* sugar for vector indexed by [ nexp ] *)
- | Typ_lib_vector3 of typ * terminal * nexp * terminal * nexp * terminal (* sugar for vector indexed by [ nexp:nexp ] *)
+ | Typ_lib_vector3 of typ * terminal * nexp * terminal * nexp * terminal (* sugar for vector indexed by [ nexp..nexp ] *)
  | Typ_lib_list of terminal * typ (* list of typ *)
  | Typ_lib_set of terminal * typ (* finite set of typ *)
  | Typ_lib_reg of terminal * typ (* mutable register components holding typ *)