diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.lem | 18 | ||||
| -rw-r--r-- | language/l2.ml | 24 | ||||
| -rw-r--r-- | language/l2.ott | 6 | ||||
| -rw-r--r-- | language/l2_parse.ml | 6 | ||||
| -rw-r--r-- | language/l2_parse.ott | 6 |
5 files changed, 26 insertions, 34 deletions
diff --git a/language/l2.lem b/language/l2.lem index 40b23099..f9d0a087 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -34,7 +34,7 @@ type base_kind = | BK_aux of base_kind_aux * l -type kid_aux = (* kinded IDs: Type, Nat, Order, and Effect variables *) +type kid_aux = (* kinded IDs: $Type$, $Nat$, $Order$, and $Effect$ variables *) | Var of x @@ -59,7 +59,7 @@ type kind = | K_aux of kind_aux * l -type nexp_aux = (* numeric expression, of kind Nat *) +type nexp_aux = (* numeric expression, of kind $Nat$ *) | Nexp_id of id (* abbreviation identifier *) | Nexp_var of kid (* variable *) | Nexp_constant of integer (* constant *) @@ -84,8 +84,8 @@ type base_effect_aux = (* effect *) | BE_depend (* dynamic footprint *) | BE_undef (* undefined-instruction exception *) | BE_unspec (* unspecified values *) - | BE_nondet (* nondeterminism, from nondet *) - | BE_escape (* potential call of exit *) + | BE_nondet (* nondeterminism, from $nondet$ *) + | BE_escape (* potential call of $exit$ *) | BE_lset (* local mutation; not user-writable *) | BE_lret (* local return; not user-writable *) @@ -94,13 +94,13 @@ type base_effect = | BE_aux of base_effect_aux * l -type order_aux = (* vector order specifications, of kind Order *) +type order_aux = (* vector order specifications, of kind $Order$ *) | Ord_var of kid (* variable *) | Ord_inc (* increasing *) | Ord_dec (* decreasing *) -type effect_aux = (* effect set, of kind Effect *) +type effect_aux = (* effect set, of kind $Effect$ *) | Effect_var of kid | Effect_set of list base_effect (* effect set *) @@ -138,9 +138,9 @@ type n_constraint = | NC_aux of n_constraint_aux * l -type quant_item_aux = (* kinded identifier or Nat constraint *) +type quant_item_aux = (* kinded identifier or $Nat$ constraint *) | QI_id of kinded_id (* optionally kinded identifier *) - | QI_const of n_constraint (* Nat constraint *) + | QI_const of n_constraint (* $Nat$ constraint *) type quant_item = @@ -415,7 +415,7 @@ type val_spec_aux 'a = (* value type specification *) type kind_def_aux 'a = (* Definition body for elements of kind *) - | KD_nabbrev of kind * id * name_scm_opt * nexp (* Nat-expression abbreviation *) + | KD_nabbrev of kind * id * name_scm_opt * nexp (* $Nat$-expression abbreviation *) | KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *) | KD_record of kind * id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) | KD_variant of kind * id * name_scm_opt * typquant * list type_union * bool (* union type definition *) diff --git a/language/l2.ml b/language/l2.ml index 538cd234..5b924498 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -1,15 +1,13 @@ (* generated by Ott 0.25 from: l2.ott *) -type text = string - type l = Parse_ast.l type 'a annot = l * 'a -type x = text (* identifier *) -type ix = text (* infix identifier *) +type x = string (* identifier *) +type ix = string (* infix identifier *) type base_kind_aux = (* base kind *) @@ -31,7 +29,7 @@ id_aux = (* identifier *) type -kid_aux = (* kinded IDs: _, _, _, and _ variables *) +kid_aux = (* kinded IDs: $_$, $_$, $_$, and $_$ variables *) Var of x @@ -56,7 +54,7 @@ kind = type -nexp_aux = (* numeric expression, of kind _ *) +nexp_aux = (* numeric expression, of kind $_$ *) Nexp_id of id (* abbreviation identifier *) | Nexp_var of kid (* variable *) | Nexp_constant of int (* constant *) @@ -82,8 +80,8 @@ base_effect_aux = (* effect *) | BE_depend (* dynamic footprint *) | BE_undef (* undefined-instruction exception *) | BE_unspec (* unspecified values *) - | BE_nondet (* nondeterminism, from _ *) - | BE_escape (* potential call of _ *) + | BE_nondet (* nondeterminism, from $_$ *) + | BE_escape (* potential call of $_$ *) | BE_lset (* local mutation; not user-writable *) | BE_lret (* local return; not user-writable *) @@ -94,14 +92,14 @@ base_effect = type -order_aux = (* vector order specifications, of kind _ *) +order_aux = (* vector order specifications, of kind $_$ *) Ord_var of kid (* variable *) | Ord_inc (* increasing *) | Ord_dec (* decreasing *) type -effect_aux = (* effect set, of kind _ *) +effect_aux = (* effect set, of kind $_$ *) Effect_var of kid | Effect_set of (base_effect) list (* effect set *) @@ -141,9 +139,9 @@ n_constraint = type -quant_item_aux = (* kinded identifier or _ constraint *) +quant_item_aux = (* kinded identifier or $_$ constraint *) QI_id of kinded_id (* optionally kinded identifier *) - | QI_const of n_constraint (* _ constraint *) + | QI_const of n_constraint (* $_$ constraint *) type @@ -449,7 +447,7 @@ type type 'a kind_def_aux = (* Definition body for elements of kind *) - KD_nabbrev of kind * id * name_scm_opt * nexp (* _-expression abbreviation *) + KD_nabbrev of kind * id * name_scm_opt * nexp (* $_$-expression abbreviation *) | KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *) | KD_record of kind * id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *) | KD_variant of kind * id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *) diff --git a/language/l2.ott b/language/l2.ott index 599e89bf..905c330a 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -41,8 +41,6 @@ metavar regexp ::= embed {{ ocaml -type text = string - type l = Parse_ast.l type 'a annot = l * 'a @@ -72,7 +70,7 @@ val subst : forall 'a. list 'a -> list 'a -> bool }} metavar x , y , z ::= - {{ ocaml text }} + {{ ocaml string }} {{ lem string }} {{ hol string }} {{ com identifier }} @@ -81,7 +79,7 @@ metavar x , y , z ::= metavar ix ::= {{ lex alphanum }} - {{ ocaml text }} + {{ ocaml string }} {{ lem string }} {{ hol string }} {{ com infix identifier }} diff --git a/language/l2_parse.ml b/language/l2_parse.ml index 8393207c..42ef8d44 100644 --- a/language/l2_parse.ml +++ b/language/l2_parse.ml @@ -1,8 +1,6 @@ (* generated by Ott 0.25 from: l2_parse.ott *) -type text = string - type l = | Unknown | Int of string * l option @@ -14,8 +12,8 @@ type 'a annot = l * 'a exception Parse_error_locn of l * string -type x = text (* identifier *) -type ix = text (* infix identifier *) +type x = string (* identifier *) +type ix = string (* infix identifier *) type base_kind_aux = (* base kind *) diff --git a/language/l2_parse.ott b/language/l2_parse.ott index 28803cb6..49df4908 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -41,8 +41,6 @@ metavar regexp ::= embed {{ ocaml -type text = string - type l = | Unknown | Int of string * l option @@ -77,7 +75,7 @@ val subst : forall 'a. list 'a -> list 'a -> bool }} metavar x , y , z ::= - {{ ocaml text }} + {{ ocaml string }} {{ lem string }} {{ hol string }} {{ com identifier }} @@ -86,7 +84,7 @@ metavar x , y , z ::= metavar ix ::= {{ lex alphanum }} - {{ ocaml text }} + {{ ocaml string }} {{ lem string }} {{ hol string }} {{ com infix identifier }} |