diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/sail.ott | 68 |
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 |