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).

4 files changed, 38 insertions, 71 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 *)
 
 
diff --git a/language/l2.ott b/language/l2.ott
index 68131d52..1e39aaff 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -7,7 +7,7 @@ metavar num , zero ::=
   {{ lex numeric }}
   {{ ocaml int }}
   {{ hol num }}
-  {{ lem num }}
+  {{ lem nat }}
   {{ com Numeric literals }}
 
 metavar hex ::=
@@ -51,25 +51,14 @@ type 'a annot = l * 'a
 
 embed
 {{ lem
-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
 
diff --git a/language/l2_parse.ott b/language/l2_parse.ott
index 56152bd1..c2cbe50d 100644
--- a/language/l2_parse.ott
+++ b/language/l2_parse.ott
@@ -7,7 +7,7 @@ metavar num ::=
   {{ lex numeric }}
   {{ ocaml int }}
   {{ hol num }}
-  {{ lem num }}
+  {{ lem nat }}
   {{ com Numeric literals }}
 
 metavar hex ::=
@@ -56,25 +56,14 @@ exception Parse_error_locn of l * string
 
 embed
 {{ lem
-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
 
diff --git a/language/l2_rules.ott b/language/l2_rules.ott
index 26bd899b..15083a16 100644
--- a/language/l2_rules.ott
+++ b/language/l2_rules.ott
@@ -142,7 +142,7 @@ S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }}
       {{ lem [[nec1 .. necn]] }}
    | S_N1 u+ .. u+ S_Nn                                                    :: M :: SN_union
      {{ hol (FOLDR FUNION FEMPTY [[S_N1..S_Nn]]) }}
-     {{ lem (List.fold_right union_map [[S_N1..S_Nn]] Pmap.empty) }}
+     {{ lem (List.fold_right union_map [[S_N1..S_Nn]] Map.empty) }}
      {{ ocaml (assert false) }}
    | consistent_increase ne1 ne'1 ... nen ne'n                    :: M :: SN_increasing
      {{ com Generates constraints from  pairs of constraints, where the first of each pair is always larger than the sum of the previous pair }}
@@ -184,11 +184,11 @@ S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }}
    {{ com Kind environments }}
    | { id1 |-> kinf1 , .. , idn |-> kinfn }    :: :: concrete
      {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[id1 kinf1 .. idn kinfn]]) }}
-     {{ lem (List.fold_right (fun (x,v) m -> Pmap.add x v m) [[id1 kinf1 .. idn kinfn]] Pmap.empty) }} 
+     {{ lem (List.fold_right (fun (x,v) m -> Map.insert x v m) [[id1 kinf1 .. idn kinfn]] Map.empty) }} 
    | E_k1 u+ .. u+ E_kn                                          :: M :: union
      {{ com In a unioning kinf, {k default} u {k} results in {k} (i.e. the default is locally forgotten) }} 
      {{ hol (FOLDR FUNION FEMPTY [[E_k1..E_kn]]) }}
-     {{ lem (List.fold_right union_map [[E_k1..E_kn]] Pmap.empty) }}
+     {{ lem (List.fold_right union_map [[E_k1..E_kn]] Map.empty) }}
      {{ ocaml (assert false) }}
    | E_k u- E_k1 .. E_kn                                            :: M :: multi_set_minus
      {{ hol arb }} {{ lem arb }} {{ ocaml assert false }}
@@ -205,10 +205,10 @@ S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }}
    {{ com Type environments }}
    | { id1 |-> tinf1 , .. , idn |-> tinfn }                    :: :: base
      {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[id1 tinf1 .. idn tinfn]]) }}
-     {{ lem (List.fold_right (fun (x,f) m -> Pmap.add x f m) [[id1 tinf1 .. idn tinfn]] Pmap.empty) }} 
+     {{ lem (List.fold_right (fun (x,f) m -> Map.insert x f m) [[id1 tinf1 .. idn tinfn]] Map.empty) }} 
    | ( E_t1 u+ .... u+ E_tn )                                         :: M :: union
      {{ hol (FOLDR FUNION FEMPTY [[E_t1....E_tn]]) }}
-     {{ lem (List.fold_right union_map [[E_t1....E_tn]] Pmap.empty) }}
+     {{ lem (List.fold_right union_map [[E_t1....E_tn]] Map.empty) }}
      {{ ocaml (assert false) }}
    | u+ E_t1 .. E_tn                                            :: M :: multi_union
      {{ hol arb }}
@@ -236,10 +236,10 @@ S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }}
    {{ com Record environments }}
    | { { field_typs1 } |-> tinf1 , .. , { field_typsn } |-> tinfn }                    :: :: concrete
      {{ hol (FOLDR (\x E. E |+ x) FEMPTY) }}
-     {{ lem (List.fold_right (fun (x,f) m -> Pmap.add x f m)  Pmap.empty) }} 
+     {{ lem (List.fold_right (fun (x,f) m -> Map.insert x f m)  Map.empty) }} 
    | E_r1 u+ .. u+ E_rn                                          :: M :: union
      {{ hol (FOLDR FUNION FEMPTY [[E_r1..E_rn]]) }}
-     {{ lem (List.fold_right union_map [[E_r1..E_rn]] Pmap.empty) }}
+     {{ lem (List.fold_right union_map [[E_r1..E_rn]] Map.empty) }}
      {{ ocaml (assert false) }}
 
 ts :: ts_ ::=                                     {{ phantom }}
@@ -253,12 +253,12 @@ formula :: formula_ ::=
    | E_k ( id ) gives kinf                                      :: :: lookup_k
      {{ com Kind lookup }}
      {{ hol (FLOOKUP [[E_k]] [[id]] = SOME [[k]]) }}
-     {{ lem Pmap.find [[id]] [[E_k]] = [[k]] }} 
+     {{ lem Map.lookup [[id]] [[E_k]] = Just [[k]] }} 
 
    | E_t ( id ) gives tinf                                      :: :: lookup_t
      {{ com Type lookup }}
      {{ hol (FLOOKUP [[E_t]] [[id]] = SOME [[t]]) }}
-     {{ lem Pmap.find [[id]] [[E_t]] = [[t]] }} 
+     {{ lem Map.lookup [[id]] [[E_t]] = Just [[t]] }} 
 
   | E_k ( id ) <-| k						:: :: update_k
      {{ com Update the kind associated with id to k }}        
@@ -271,25 +271,25 @@ formula :: formula_ ::=
 
    | dom ( E_t1 ) inter dom ( E_t2 ) = emptyset                  :: :: E_t_disjoint
      {{ hol (DISJOINT (FDOM [[E_t1]]) (FDOM [[E_t2]])) }}
-     {{ lem disjoint (Pmap.domain [[E_t1]]) (Pmap.domain [[E_t2]])  }} 
+     {{ lem disjoint (Map.domain [[E_t1]]) (Map.domain [[E_t2]])  }} 
    
    | dom ( E_k1 ) inter dom ( E_k2 ) = emptyset                  :: :: E_k_disjoint
      {{ hol (DISJOINT (FDOM [[E_f1]]) (FDOM [[E_f2]])) }}
-     {{ lem disjoint (Pmap.domain [[E_f1]]) (Pmap.domain [[E_f2]]) }} 
+     {{ lem disjoint (Map.domain [[E_f1]]) (Map.domain [[E_f2]]) }} 
 
    | disjoint doms ( E_t1 , .... , E_tn )                        :: :: E_x_disjoint_many
     {{ hol (FOLDR (\E b. case b of NONE => NONE | SOME s => if DISJOINT (FDOM
        E) s then SOME (FDOM E UNION s) else NONE) (SOME {}) [[E_t1....E_tn]] <> NONE) }}
-     {{ lem disjoint_all (List.map Pmap.domain [[E_t1 .... E_tn]]) }}
+     {{ lem disjoint_all (List.map Map.domain [[E_t1 .... E_tn]]) }}
      {{ com Pairwise disjoint domains }}
 
    | id NOTIN dom ( E_k )                                         :: :: notin_dom_k
      {{ hol ([[id]] NOTIN FDOM [[E_k]]) }}
-     {{ lem Pervasives.not (Pmap.mem [[id]] [[E_k]]) }} 
+     {{ lem Pervasives.not (Map.member [[id]] [[E_k]]) }} 
 
    | id NOTIN dom ( E_t )                                         :: :: notin_dom_t
      {{ hol ([[id]] NOTIN FDOM [[E_t]]) }}
-     {{ lem Pervasives.not (Pmap.mem [[id]] [[E_t]]) }} 
+     {{ lem Pervasives.not (Map.member [[id]] [[E_t]]) }} 
 
    | id0 : t0 .. idn : tn SUBSET id'0 : t'0 .. id'i : t'i       :: :: subsetFields