diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.ott | 85 |
1 files changed, 81 insertions, 4 deletions
diff --git a/language/l2.ott b/language/l2.ott index 8145de7a..6963d8bd 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -16,6 +16,7 @@ metavar num,numZero,numOne ::= metavar nat ::= {{ phantom }} + {{ ocaml int }} {{ lex numeric }} {{ lem nat }} @@ -31,7 +32,7 @@ metavar bin ::= {{ lex numeric }} {{ ocaml string }} {{ lem string }} - {{ com Bit vector literal, specified by C-style binary number }} + {{ com Bit vector literal, specified by C-style binary number }} metavar string ::= {{ phantom }} @@ -622,9 +623,85 @@ let rec disjoint_all sets = end }} - -grammar +grammar + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Interpreter specific things % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +optx :: '' ::= {{ phantom }} {{ lem maybe string }} {{ ocaml string option }} + | x :: :: optx_x + {{ lem (Just [[x]]) }} {{ ocaml (Some [[x]]) }} + | :: :: optx_none + {{ lem Nothing }} {{ ocaml None }} + +tag :: 'Tag_' ::= +{{ com Data indicating where the identifier arises and thus information necessary in compilation }} + | None :: :: empty + | Intro :: :: intro {{ com Denotes an assignment and lexp that introduces a binding }} + | Set :: :: set {{ com Denotes an expression that mutates a local variable }} + | Tuple :: :: tuple_assign {{ com Denotes an assignment with a tuple lexp }} + | Global :: :: global {{ com Globally let-bound or enumeration based value/variable }} + | Ctor :: :: ctor {{ com Data constructor from a type union }} + | Extern optx :: :: extern {{ com External function, specied only with a val statement }} + | Default :: :: default {{ com Type has come from default declaration, identifier may not be bound locally }} + | Spec :: :: spec + | Enum num :: :: enum + | Alias :: :: alias + | Unknown_path optx :: :: unknown {{ com Tag to distinguish an unknown path from a non-analysis non deterministic path}} + +embed +{{ lem + +type tannot = maybe (typ * tag * list unit * effect * effect) +}} + +embed +{{ ocaml + +(* Interpreter specific things are just set to unit here *) +type tannot = unit + +type reg_form_set = unit + +}} + +grammar +tannot :: '' ::= + {{ phantom }} + {{ ocaml unit }} + {{ lem tannot }} + +i_direction :: 'I' ::= + | IInc :: :: Inc + | IDec :: :: Dec + +ctor_kind :: 'C_' ::= + | C_Enum nat :: :: Enum + | C_Union :: :: Union + +reg_form :: 'Form_' ::= + | Reg id tannot i_direction :: :: Reg + | SubReg id reg_form index_range :: :: SubReg + +reg_form_set :: '' ::= {{ phantom }} {{ lem set reg_form }} + +alias_spec_tannot :: '' ::= {{ phantom }} {{ lem alias_spec tannot }} {{ ocaml tannot alias_spec }} + +value :: 'V_' ::= {{ com interpreter evaluated value }} + | Boxref nat typ :: :: boxref + | Lit lit :: :: lit + | Tuple ( value1 , ... , valuen ) :: :: tuple + | List ( value1 , ... , valuen ) :: :: list + | Vector nat i_direction ( value1 , ... , valuen ) :: :: vector + | Vector_sparse nat' nat'' i_direction ( nat1 value1 , ... , natn valuen ) value' :: :: vector_sparse + | Record typ ( id1 value1 , ... , idn valuen ) :: :: record + | V_ctor id typ ctor_kind value1 :: :: ctor + | Unknown :: :: unknown + | Register reg_form :: :: register + | Register_alias alias_spec_tannot tannot :: :: register_alias + | Track value reg_form_set :: :: track %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Expressions % @@ -772,7 +849,7 @@ exp :: 'E_' ::= | let lexp = exp in exp' :: I :: internal_let {{ com This is an internal node for compilation that demonstrates the scope of a local mutable variable }} | let pat = exp in exp' :: I :: internal_plet {{ com This is an internal node, used to distinguised some introduced lets during processing from original ones }} | return_int ( exp ) :: :: internal_return {{ com For internal use to embed into monad definition }} -% | value :: I :: internal_value {{ com For internal use in interpreter to wrap pre-evaluated values when returning an action }} + | value :: I :: internal_value {{ com For internal use in interpreter to wrap pre-evaluated values when returning an action }} | constraint n_constraint :: :: constraint %i_direction :: 'I' ::= |