Port L2 to new Lem

Tests compile and run properly. There is a lot of hackery going
on to workaround the rough edges of new Lem. Use at your own
risk (you need the "library-format" branch of lem).

1 files changed, 12 insertions, 23 deletions

diff --git a/language/l2.lem b/language/l2.lem
index 8e5dd4ed..926706a0 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -1,24 +1,13 @@
 (* generated by Ott 0.22 from: l2.ott *)
 
-open Pmap
-open Pervasives
+open import Map
+open import Maybe
+open import Pervasives
 
 type l =
   | Unknown
-  | Trans of string * option l
-  | Range of num * num
-
-val disjoint : forall 'a . set 'a -> set 'a -> bool
-let disjoint s1 s2 = 
-  let diff = s1 inter s2 in
-  diff = Pervasives.empty
-
-val disjoint_all : forall 'a. list (set 'a) -> bool
-let rec disjoint_all ls = match ls with
-  | [] -> true
-  | [a] -> true
-  | a::b::rs -> (disjoint a b) && (disjoint_all (b::rs))
-end
+  | Trans of string * maybe l
+  | Range of nat * nat
 
 val duplicates : forall 'a. list 'a -> list 'a
 
@@ -50,7 +39,7 @@ type kind =  (* kinds *)
 
 type nexp =  (* expression of kind $Nat$, for vector sizes and origins *)
  | Nexp_id of id (* identifier *)
- | Nexp_constant of num (* constant *)
+ | Nexp_constant of nat (* constant *)
  | Nexp_times of nexp * nexp (* product *)
  | Nexp_sum of nexp * nexp (* sum *)
  | Nexp_exp of nexp (* exponential *)
@@ -75,7 +64,7 @@ type nexp_constraint =  (* constraint over kind $Nat$ *)
  | NC_fixed of nexp * nexp
  | NC_bounded_ge of nexp * nexp
  | NC_bounded_le of nexp * nexp
- | NC_nat_set_bounded of id * list num
+ | NC_nat_set_bounded of id * list nat
 
 
 type effects =  (* effect set, of kind $Effects$ *)
@@ -114,7 +103,7 @@ type lit =  (* Literal constant *)
  | L_one (* $bitone : bit$ *)
  | L_true (* $true : bool$ *)
  | L_false (* $false : bool$ *)
- | L_num of num (* natural number constant *)
+ | L_num of nat (* natural number constant *)
  | L_hex of string (* bit vector constant, C-style *)
  | L_bin of string (* bit vector constant, C-style *)
  | L_undef (* constant representing undefined values *)
@@ -135,7 +124,7 @@ type pat =  (* Pattern *)
  | P_app of id * list pat (* union constructor pattern *)
  | P_record of list fpat * bool (* struct pattern *)
  | P_vector of list pat (* vector pattern *)
- | P_vector_indexed of list (num * pat) (* vector pattern (with explicit indices) *)
+ | P_vector_indexed of list (nat * pat) (* vector pattern (with explicit indices) *)
  | P_vector_concat of list pat (* concatenated vector pattern *)
  | P_tup of list pat (* tuple pattern *)
  | P_list of list pat (* list pattern *)
@@ -159,7 +148,7 @@ type exp =  (* Expression *)
  | E_if of exp * exp * exp (* conditional *)
  | E_for of id * exp * exp * exp * exp (* loop *)
  | E_vector of list exp (* vector (indexed from 0) *)
- | E_vector_indexed of list (num * exp) (* vector (indexed consecutively) *)
+ | E_vector_indexed of list (nat * exp) (* vector (indexed consecutively) *)
  | E_vector_access of exp * exp (* vector access *)
  | E_vector_subrange of exp * exp * exp (* subvector extraction *)
  | E_vector_update of exp * exp * exp (* vector functional update *)
@@ -218,8 +207,8 @@ type naming_scheme_opt =  (* Optional variable-naming-scheme specification for v
 
 
 type index_range =  (* index specification, for bitfields in register types *)
- | BF_single of num (* single index *)
- | BF_range of num * num (* index range *)
+ | BF_single of nat (* single index *)
+ | BF_range of nat * nat (* index range *)
  | BF_concat of index_range * index_range (* concatenation of index ranges *)