diff options
Diffstat (limited to 'language/l2.ott')
| -rw-r--r-- | language/l2.ott | 243 |
1 files changed, 100 insertions, 143 deletions
diff --git a/language/l2.ott b/language/l2.ott index 02823237..69073421 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -26,7 +26,7 @@ metavar hex ::= {{ ocaml string }} {{ lem string }} {{ com Bit vector literal, specified by C-style hex number }} - + metavar bin ::= {{ phantom }} {{ lex numeric }} @@ -55,10 +55,16 @@ metavar real ::= {{ hol string }} {{ com Real number literal }} +metavar value ::= + {{ phantom }} + {{ ocaml value }} + {{ lem value }} + embed {{ ocaml open Big_int +open Value type text = string @@ -72,28 +78,15 @@ type loop = While | Until embed {{ lem -open import Pervasives -open import Pervasives_extra -open import Map -open import Maybe -open import Set_extra - -type l = - | Unknown - | Int of string * maybe l (*internal types, functions*) - | Range of string * nat * nat * nat * nat - | Generated of l (*location for a generated node, where l is the location of the closest original source*) - -type annot 'a = l * 'a -val duplicates : forall 'a. list 'a -> list 'a +type l = | Unknown -val set_from_list : forall 'a. list 'a -> set 'a - -val subst : forall 'a. list 'a -> list 'a -> bool +type value = | Val type loop = While | Until +type annot 'a = l * 'a + }} metavar x , y , z ::= @@ -113,8 +106,6 @@ metavar ix ::= {{ ocamlvar "[[ix]]" }} {{ lemvar "[[ix]]" }} - - grammar l :: '' ::= {{ phantom }} @@ -139,7 +130,7 @@ id :: '' ::= | x :: :: id | ( deinfix x ) :: D :: deIid {{ com remove infix status }} | bool :: M :: bool {{ com built in type identifiers }} {{ ichlo (Id "bool") }} - | bit :: M :: bit {{ ichlo (Id "bit") }} + | bit :: M :: bit {{ ichlo (Id "bit") }} | unit :: M :: unit {{ ichlo (Id "unit") }} | nat :: M :: nat {{ ichlo (Id "nat") }} | int :: M :: int {{ ichlo (Id "int") }} @@ -246,23 +237,12 @@ base_effect :: 'BE_' ::= effect :: 'Effect_' ::= {{ com effect set, of kind $[[Effect]]$ }} {{ aux _ l }} - | kid :: :: var | { base_effect1 , .. , base_effectn } :: :: set {{ com effect set }} | pure :: M :: pure {{ com sugar for empty effect set }} {{ lem (Effect_set []) }} {{icho [[{}]] }} | effect1 u+ .. u+ effectn :: M :: union {{ com union of sets of effects }} {{ icho [] }} {{ lem (List.foldr effect_union (Effect_aux (Effect_set []) Unknown) [[effect1..effectn]]) }} -embed -{{ lem -let effect_union e1 e2 = - match (e1,e2) with - | ((Effect_aux (Effect_set els) _),(Effect_aux (Effect_set els2) l)) -> Effect_aux (Effect_set (els++els2)) l - end -}} - -grammar - % TODO: are we going to need any effect polymorphism? Conceivably for built-in maps and folds. Yes. But we think we don't need any interesting effect-set expressions, eg effectset-variable union {rreg}. typ :: 'Typ_' ::= @@ -446,8 +426,11 @@ type_def_aux :: 'TD_' ::= | typedef id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } :: :: enum {{ com enumeration type definition}} {{ texlong }} - | typedef id = register bits [ nexp : nexp' ] { index_range1 : id1 ; ... ; index_rangen : idn } -:: :: register {{ com register mutable bitfield type definition }} {{ texlong }} + | bitfield id : typ = { id1 : index_range1 , ... , idn : index_rangen } :: :: bitfield + {{ com register mutable bitfield type definition }} {{ texlong }} + +% | typedef id = register bits [ nexp : nexp' ] { index_range1 : id1 ; ... ; index_rangen : idn } +% :: :: register {{ com register mutable bitfield type definition }} {{ texlong }} % the D(eprecated) forms here should be removed; they add complexity for no purpose. The nexp abbreviation form should have better syntax. @@ -575,7 +558,7 @@ pat :: 'P_' ::= % cf ntoes for this | pat1 : .... : patn :: :: vector_concat - {{ com concatenated vector pattern }} + {{ com concatenated vector pattern }} | ( pat1 , .... , patn ) :: :: tup {{ com tuple pattern }} @@ -596,114 +579,85 @@ parsing P_app <= P_app P_app <= P_as -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Machinery for typing rules % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -embed -{{ lem - -let rec remove_one i l = - match l with - | [] -> [] - | i2::l2 -> if i2 = i then l2 else i2::(remove_one i l2) -end - -let rec remove_from l l2 = - match l2 with - | [] -> l - | i::l2' -> remove_from (remove_one i l) l2' -end - -let disjoint s1 s2 = Set.null (s1 inter s2) - -let rec disjoint_all sets = - match sets with - | [] -> true - | s1::[] -> true - | s1::s2::sets -> (disjoint s1 s2) && (disjoint_all (s2::sets)) -end -}} - 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 +% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% % 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 % @@ -835,6 +789,7 @@ exp :: 'E_' ::= % this can be used to break out of for loops | exit exp :: :: exit {{ com halt all current execution }} + | ref id :: :: ref | throw exp :: :: throw | try exp catch pexp1 .. pexpn :: :: try %, potentially calling a system, trap, or interrupt handler with exp @@ -848,7 +803,7 @@ exp :: 'E_' ::= | annot , annot' :: I :: internal_exp_user {{ com This is like the above but the user has specified an implicit parameter for the current function }} | comment string :: I :: comment {{ com For generated unstructured comments }} | comment exp :: I :: comment_struc {{ com For generated structured comments }} - | 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 }} + | var lexp = exp in exp' :: I :: var {{ 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 }} @@ -874,6 +829,8 @@ exp :: 'E_' ::= lexp :: 'LEXP_' ::= {{ com lvalue expression }} {{ aux _ annot }} {{ auxparam 'a }} | id :: :: id +% | ref id :: :: ref + | deref exp :: :: deref {{ com identifier }} | id ( exp1 , .. , expn ) :: :: memory {{ com memory or register write via function call }} | id exp :: S :: mem_tup {{ ichlo [[id (exp)]] }} @@ -1040,7 +997,7 @@ val_spec {{ ocaml 'a val_spec }} {{ lem val_spec 'a }} :: 'VS_' ::= val_spec_aux :: 'VS_' ::= {{ com value type specification }} {{ ocaml VS_val_spec of typschm * id * (string -> string option) * bool }} - {{ lem VS_val_spec of typschm * id * maybe string * bool }} + {{ lem VS_val_spec of typschm * id * (string -> maybe string) * bool }} | val typschm id :: S :: val_spec {{ com specify the type of an upcoming definition }} {{ ocaml (VS_val_spec [[typschm]] [[id]] None false) }} {{ lem }} |