diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.lem | 43 | ||||
| -rw-r--r-- | language/l2.ml | 63 | ||||
| -rw-r--r-- | language/l2.ott | 11 |
3 files changed, 69 insertions, 48 deletions
diff --git a/language/l2.lem b/language/l2.lem index ff3d3d80..8f6144cb 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -83,11 +83,6 @@ type base_effect = | BE_aux of base_effect_aux * l -type id_aux = (* Identifier *) - | Id of x - | DeIid of x (* remove infix status *) - - type effect_aux = (* effect set, of kind Effects *) | Effect_var of kid | Effect_set of list base_effect (* effect set *) @@ -99,8 +94,9 @@ type order_aux = (* vector order specifications, of kind Order *) | Ord_dec (* decreasing (big-endian) *) -type id = - | Id_aux of id_aux * l +type id_aux = (* Identifier *) + | Id of x + | DeIid of x (* remove infix status *) type effect = @@ -110,6 +106,10 @@ type effect = type order = | Ord_aux of order_aux * l + +type id = + | Id_aux of id_aux * l + 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 @@ -228,7 +228,16 @@ type reg_id_aux 'a = | RI_id of id -type fexps_aux 'a = (* Field-expression list *) +type lexp 'a = + | LEXP_aux of (lexp_aux 'a) * annot 'a + +and fexp_aux 'a = (* Field-expression *) + | FE_Fexp of id * (exp 'a) + +and fexp 'a = + | FE_aux of (fexp_aux 'a) * annot 'a + +and fexps_aux 'a = (* Field-expression list *) | FES_Fexps of list (fexp 'a) * bool and fexps 'a = @@ -285,6 +294,8 @@ and exp_aux 'a = (* Expression *) | E_internal_cast of annot 'a * (exp 'a) (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *) | E_internal_exp of annot 'a (* This is an internal use for passing nexp information to library functions, postponed for constraint solving *) | E_internal_exp_user of annot 'a * annot 'a (* This is like the above but the user has specified an implicit parameter for the current function *) + | E_comment of string (* For generated unstructured comments *) + | E_comment_struc of (exp 'a) (* For generated structured comments *) | E_internal_let of (lexp 'a) * (exp 'a) * (exp 'a) (* This is an internal node for compilation that demonstrates the scope of a local mutable variable *) | E_internal_plet of (pat 'a) * (exp 'a) * (exp 'a) (* This is an internal node, used to distinguised some introduced lets during processing from original ones *) | E_internal_return of (exp 'a) (* For internal use to embed into monad definition *) @@ -300,15 +311,6 @@ and lexp_aux 'a = (* lvalue expression *) | LEXP_vector_range of (lexp 'a) * (exp 'a) * (exp 'a) (* subvector *) | LEXP_field of (lexp 'a) * id (* struct field *) -and lexp 'a = - | LEXP_aux of (lexp_aux 'a) * annot 'a - -and fexp_aux 'a = (* Field-expression *) - | FE_Fexp of id * (exp 'a) - -and fexp 'a = - | FE_aux of (fexp_aux 'a) * annot 'a - type reg_id 'a = | RI_aux of (reg_id_aux 'a) * annot 'a @@ -449,7 +451,11 @@ type val_spec 'a = | VS_aux of (val_spec_aux 'a) * annot 'a -type def 'a = (* Top-level definition *) +type dec_comm 'a = (* Top-level generated comments *) + | DC_comm of string (* generated unstructured comment *) + | DC_comm_struct of (def 'a) (* generated structured comment *) + +and def 'a = (* Top-level definition *) | DEF_type of (type_def 'a) (* type definition *) | DEF_fundef of (fundef 'a) (* function definition *) | DEF_val of (letbind 'a) (* value definition *) @@ -457,6 +463,7 @@ type def 'a = (* Top-level definition *) | DEF_default of (default_spec 'a) (* default kind and type assumptions *) | DEF_scattered of (scattered_def 'a) (* scattered function and type definition *) | DEF_reg_dec of (dec_spec 'a) (* register declaration *) + | DEF_comm of (dec_comm 'a) (* generated comments *) type defs 'a = (* Definition sequence *) diff --git a/language/l2.ml b/language/l2.ml index 00345dc7..b8e31514 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -20,13 +20,18 @@ base_kind_aux = (* base kind *) type +base_kind = + BK_aux of base_kind_aux * l + + +type kid_aux = (* variables with kind, ticked to differntiate from program variables *) Var of x type -base_kind = - BK_aux of base_kind_aux * l +kind_aux = (* kinds *) + K_kind of (base_kind) list type @@ -35,8 +40,8 @@ kid = type -kind_aux = (* kinds *) - K_kind of (base_kind) list +kind = + K_aux of kind_aux * l type @@ -54,11 +59,6 @@ and nexp = type -kind = - K_aux of kind_aux * l - - -type base_effect_aux = (* effect *) BE_rreg (* read register *) | BE_wreg (* write register *) @@ -81,6 +81,13 @@ base_effect = type +order_aux = (* vector order specifications, of kind Order *) + Ord_var of kid (* variable *) + | Ord_inc (* increasing (little-endian) *) + | Ord_dec (* decreasing (big-endian) *) + + +type id_aux = (* Identifier *) Id of x | DeIid of x (* remove infix status *) @@ -93,10 +100,8 @@ effect_aux = (* effect set, of kind Effects *) type -order_aux = (* vector order specifications, of kind Order *) - Ord_var of kid (* variable *) - | Ord_inc (* increasing (little-endian) *) - | Ord_dec (* decreasing (big-endian) *) +order = + Ord_aux of order_aux * l type @@ -110,8 +115,9 @@ effect = type -order = - Ord_aux of order_aux * l +kinded_id_aux = (* optionally kind-annotated identifier *) + KOpt_none of kid (* identifier *) + | KOpt_kind of kind * kid (* kind-annotated variable *) type @@ -123,9 +129,8 @@ n_constraint_aux = (* constraint over kind $_$ *) type -kinded_id_aux = (* optionally kind-annotated identifier *) - KOpt_none of kid (* identifier *) - | KOpt_kind of kind * kid (* kind-annotated variable *) +kinded_id = + KOpt_aux of kinded_id_aux * l type @@ -134,11 +139,6 @@ n_constraint = type -kinded_id = - KOpt_aux of kinded_id_aux * l - - -type quant_item_aux = (* Either a kinded identifier or a nexp constraint for a typquant *) QI_id of kinded_id (* An optionally kinded identifier *) | QI_const of n_constraint (* A constraint for this type *) @@ -175,7 +175,10 @@ typquant = type -typ_aux = (* Type expressions, of kind $_$ *) +typ_arg = + Typ_arg_aux of typ_arg_aux * l + +and typ_aux = (* Type expressions, of kind $_$ *) Typ_wild (* Unspecified type *) | Typ_id of id (* Defined type *) | Typ_var of kid (* Type variable *) @@ -192,9 +195,6 @@ and typ_arg_aux = (* Type constructor arguments of all kinds *) | Typ_arg_order of order | Typ_arg_effect of effect -and typ_arg = - Typ_arg_aux of typ_arg_aux * l - type lit = @@ -273,6 +273,8 @@ type | E_internal_cast of 'a annot * 'a exp (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *) | E_internal_exp of 'a annot (* This is an internal use for passing nexp information to library functions, postponed for constraint solving *) | E_internal_exp_user of 'a annot * 'a annot (* This is like the above but the user has specified an implicit parameter for the current function *) + | E_comment of string (* For generated unstructured comments *) + | E_comment_struc of 'a exp (* For generated structured comments *) | E_internal_let of 'a lexp * 'a exp * 'a exp (* This is an internal node for compilation that demonstrates the scope of a local mutable variable *) | E_internal_plet of 'a pat * 'a exp * 'a exp (* This is an internal node, used to distinguised some introduced lets during processing from original ones *) | E_internal_return of 'a exp (* For internal use to embed into monad definition *) @@ -492,7 +494,11 @@ type type -'a def = (* Top-level definition *) +'a dec_comm = (* Top-level generated comments *) + DC_comm of string (* generated unstructured comment *) + | DC_comm_struct of 'a def (* generated structured comment *) + +and 'a def = (* Top-level definition *) DEF_type of 'a type_def (* type definition *) | DEF_fundef of 'a fundef (* function definition *) | DEF_val of 'a letbind (* value definition *) @@ -500,6 +506,7 @@ type | DEF_default of 'a default_spec (* default kind and type assumptions *) | DEF_scattered of 'a scattered_def (* scattered function and type definition *) | DEF_reg_dec of 'a dec_spec (* register declaration *) + | DEF_comm of 'a dec_comm (* generated comments *) type diff --git a/language/l2.ott b/language/l2.ott index 1eb447be..c6e1e470 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -649,7 +649,9 @@ exp :: 'E_' ::= | ( exp ) :: S :: paren {{ ichlo [[exp]] }} | ( annot ) exp :: :: internal_cast {{ com This is an internal cast, generated during type checking that will resolve into a syntactic cast after }} | annot :: :: internal_exp {{ com This is an internal use for passing nexp information to library functions, postponed for constraint solving }} - | annot , annot' :: :: internal_exp_user {{ com This is like the above but the user has specified an implicit parameter for the current function }} + | annot , annot' :: :: internal_exp_user {{ com This is like the above but the user has specified an implicit parameter for the current function }} + | comment string :: :: comment {{ com For generated unstructured comments }} + | comment exp :: :: comment_struc {{ com For generated structured comments }} | let lexp = exp in exp' :: :: internal_let {{ com This is an internal node for compilation that demonstrates the scope of a local mutable variable }} | let pat = exp in exp' :: :: internal_plet {{ com This is an internal node, used to distinguised some introduced lets during processing from original ones }} | return ( exp ) :: :: internal_return {{ com For internal use to embed into monad definition }} @@ -863,6 +865,10 @@ dec_spec :: 'DEC_' ::= | register alias id = alias_spec :: :: alias | register alias typ id = alias_spec :: :: typ_alias +dec_comm :: 'DC_' ::= {{ com Top-level generated comments }} {{auxparam 'a}} + | comment string :: :: comm {{ com generated unstructured comment }} + | comment def :: :: comm_struct {{ com generated structured comment }} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Top-level definitions % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -884,7 +890,8 @@ def :: 'DEF_' ::= {{ com scattered function and type definition }} | dec_spec :: :: reg_dec {{ com register declaration }} - + | dec_comm :: :: comm + {{ com generated comments }} defs :: '' ::= {{ com Definition sequence }} |