Fix all warnings (except for two lem warnings)

Remove P_record as it's never been implemented in
parser/typechecker/rewriter, and is not likely to be. This also means
we can get rid of some ugliness with the fpat and mfpat types. Stubs
for P_or and P_not are left as they still may get added to ASL and we
might want to support them, although there are good reasons to keep
our patterns simple.

The lem warning for while -> while0 for ocaml doesn't matter because
it's only used in lem, and the 32-bit number warning is just noise.

1 files changed, 15 insertions, 53 deletions

diff --git a/language/sail.ott b/language/sail.ott
index eb77e4aa..c0c8da49 100644
--- a/language/sail.ott
+++ b/language/sail.ott
@@ -388,51 +388,21 @@ pat :: 'P_' ::=
     {{ com bind pattern to type variable }}
   | id ( pat1 , .. , patn )                 :: :: app
     {{ com union constructor pattern }}
-
-% OR?  do we invent something ghastly including a union keyword?  Perhaps not...
-
-%  | <| fpat1 ; ... ; fpatn semi_opt |>                  :: :: record
-%    {{ com Record patterns }}
-% OR
-  | { fpat1 ; ... ; fpatn semi_opt }                  :: :: record
-    {{ com struct pattern }}
-
-%Patterns for vectors
-%Should these be the same since vector syntax has changed, and lists have also changed?
-
-  | [ pat1 , .. , patn  ]                     :: :: vector
-   {{ com vector pattern }}
-
-%  | [ num1 = pat1 , .. , numn = patn ]                     :: :: vector_indexed
-%   {{ com vector pattern (with explicit indices) }}
-
-% cf ntoes for this
-  |  pat1 : .... : patn                                   :: :: vector_concat
-  {{ com concatenated vector pattern }}
-
-  | ( pat1 , .... , patn )                              :: :: tup
+  | [ pat1 , ... , patn  ]                  :: :: vector
+    {{ com vector pattern }}
+  |  pat1 @ ... @ patn                      :: :: vector_concat
+    {{ com concatenated vector pattern }}
+  | ( pat1 , .... , patn )                  :: :: tup
     {{ com tuple pattern }}
-  | [|| pat1 , .. , patn ||]                            :: :: list
+  | [|| pat1 , .. , patn ||]                :: :: list
     {{ com list pattern }}
-  | ( pat )                                             :: S :: paren
+  | ( pat )                                 :: S :: paren
     {{ ichlo [[pat]] }}
-  | pat1 '::' pat2                                      :: :: cons
+  | pat1 '::' pat2                          :: :: cons
     {{ com Cons patterns }}
-
-  | pat1 ^^ ... ^^ patn                                 :: :: string_append
+  | pat1 ^^ ... ^^ patn                     :: :: string_append
     {{ com string append pattern, x ^^ y }}
 
-% XXX Is this still useful?
-fpat :: 'FP_' ::=
-  {{ com field pattern }}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | id = pat                                            :: :: Fpat
-
-mfpat  :: 'MFP_' ::=
-  {{ com Mapping field pattern, why does this have to exist }}
-  {{ aux _ annot }} {{ auxparam 'a }}
-  | id = mpat                                           :: :: mpat
-
 parsing
 P_app <= P_app
 P_app <= P_as
@@ -551,11 +521,8 @@ exp :: 'E_' ::=
     {{ com tuple }}
   | if exp1 then exp2 else exp3                         :: :: if
     {{ com conditional }}
-  | if exp1 then exp2                                   :: S :: ifnoelse {{ ichlo [[ if exp1 then exp2 else ( ) ]] }}
   | loop internal_loop_measure exp1 exp2                    :: :: loop
-  | while internal_loop_measure exp1 do exp2                :: S :: while {{ ichlo [[ loop internal_loop_measure while exp1 exp2 ]] }}
-  | repeat internal_loop_measure exp1 until exp2            :: S :: until {{ ichlo [[ loop internal_loop_measure until exp2 exp1 ]] }}
-  | foreach ( id from exp1 to exp2 by exp3 in order ) exp4  ::   :: for   {{ com loop }}
+  | foreach ( id from exp1 to exp2 by exp3 in order ) exp4  :: :: for   {{ com for loop }}
 
   % vectors
   | [ exp1 , ... , expn ]                             :: :: vector {{ com vector (indexed from 0) }}
@@ -703,10 +670,10 @@ grammar
 
 tannot_opt :: 'Typ_annot_opt_' ::=
   {{ com optional type annotation for functions}}
-  {{ aux _ l }} 
+  {{ aux _ l }}
   |                                             :: :: none
 % Currently not optional; one issue, do the type parameters apply over the argument types, or should this be the type of the function and not just the return
-  | typquant typ                                :: :: some 
+  | typquant typ                                :: :: some
 
 rec_opt :: 'Rec_' ::=
   {{ com optional recursive annotation for functions }}
@@ -741,13 +708,9 @@ fundef :: 'FD_' ::=
   {{ com function definition}}
   {{ aux _ annot }} {{ auxparam 'a }}
   | function rec_opt tannot_opt effect_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 funcl
-% TODO the above is ok for single functions, but not for mutually
-%  recursive functions - the tannot_opt scopes over all the funcli,
-%  which is ok for the typ_quant part but not for the typ part
+% 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 funcl
 
 mpat :: 'MP_' ::=
   {{ com Mapping pattern. Mostly the same as normal patterns but only constructible parts }}
@@ -755,7 +718,6 @@ mpat :: 'MP_' ::=
   | lit                                ::   :: lit
   | id                                 ::   :: id
   | id ( mpat1 , ... , mpatn )         ::   :: app
-  | { mfpat1 ; ... ; mfpatn semi_opt } ::   :: record
   | [ mpat1 , ... , mpatn ]            ::   :: vector
   | mpat1 @ ... @ mpatn                ::   :: vector_concat
   | ( mpat1 , ... , mpatn )            ::   :: tup