diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.lem | 12 | ||||
| -rw-r--r-- | language/l2.ott | 2 | ||||
| -rw-r--r-- | language/l2_parse.ml | 2 | ||||
| -rw-r--r-- | language/l2_parse.ott | 2 | ||||
| -rw-r--r-- | language/l2_typ.ott | 10 |
5 files changed, 14 insertions, 14 deletions
diff --git a/language/l2.lem b/language/l2.lem index 82e2450f..9f500046 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -7,7 +7,7 @@ open import Set_extra type l = | Unknown - | Trans of string * maybe l + | Int of string * maybe l (*Internally generated*) | Range of string * nat * nat * nat * nat type annot 'a = l * 'a @@ -446,7 +446,7 @@ type k = (* Internal kinds *) type ne = (* internal numeric expressions *) - | Ne_var of kid + | Ne_var of x | Ne_const of integer | Ne_mult of ne * ne | Ne_add of list ne @@ -468,7 +468,7 @@ type nec = (* Numeric expression constraints *) | Nec_lteq of ne * ne | Nec_eq of ne * ne | Nec_gteq of ne * ne - | Nec_in of kid * list integer + | Nec_in of x * list integer type tag = (* Data indicating where the identifier arises and thus information necessary in compilation *) @@ -481,11 +481,11 @@ type tag = (* Data indicating where the identifier arises and thus information type t = (* Internal types *) - | T_id of id - | T_var of kid + | T_id of x + | T_var of x | T_fn of t * t * effect | T_tup of list t - | T_app of id * t_args + | T_app of x * t_args | T_abbrev of t * t and t_arg = (* Argument to type constructors *) diff --git a/language/l2.ott b/language/l2.ott index 3abad576..87fddc49 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -57,7 +57,7 @@ open import Set_extra type l = | Unknown - | Trans of string * maybe l + | Int of string * maybe l (*Internally generated*) | Range of string * nat * nat * nat * nat type annot 'a = l * 'a diff --git a/language/l2_parse.ml b/language/l2_parse.ml index 92d00530..741a8a94 100644 --- a/language/l2_parse.ml +++ b/language/l2_parse.ml @@ -5,7 +5,7 @@ type text = string type l = | Unknown - | Trans of string * l option + | Int of string * l option | Range of Lexing.position * Lexing.position type 'a annot = l * 'a diff --git a/language/l2_parse.ott b/language/l2_parse.ott index eb238b65..2e48c264 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -45,7 +45,7 @@ type text = string type l = | Unknown - | Trans of string * l option + | Int of string * l option | Range of Lexing.position * Lexing.position type 'a annot = l * 'a diff --git a/language/l2_typ.ott b/language/l2_typ.ott index 057ddfba..894ac328 100644 --- a/language/l2_typ.ott +++ b/language/l2_typ.ott @@ -42,11 +42,11 @@ k :: 'Ki_' ::= t , u :: 'T_' ::= {{ com Internal types }} - | id :: :: id - | kid :: :: var + | x :: :: id + | ' x :: :: var | t1 -> t2 effect :: :: fn | ( t1 * .... * tn ) :: :: tup - | id t_args :: :: app + | x t_args :: :: app | t |-> t1 :: :: abbrev | register t_args :: S :: reg_app {{ ichlo T_app "register" [[t_args]] }} | t [ t1 / id1 ... tn / idn ] :: M :: subst {{ ichlo "todo" }} @@ -69,7 +69,7 @@ tag :: 'Tag_' ::= ne :: 'Ne_' ::= {{ com internal numeric expressions }} - | kid :: :: var + | ' x :: :: var | num :: :: const | ne1 * ne2 :: :: mult | ne1 + ... + nen :: :: add @@ -110,7 +110,7 @@ ne :: 'Ne_' ::= | ne <= ne' :: :: lteq | ne = ne' :: :: eq | ne >= ne' :: :: gteq - | kid 'IN' { num1 , ... , numn } :: :: in + | ' x 'IN' { num1 , ... , numn } :: :: in S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }} {{ hol nec list }} |