More use of variants

spectec/src/al/al_util.ml

@@ -45,7 +45,7 @@ let mk_expr at note it = it $$ at % note
 let varE ?(at = no) ~note id = VarE id |> mk_expr at note
 let boolE ?(at = no) ~note b = BoolE b |> mk_expr at note
 let numE ?(at = no) ~note i = NumE i |> mk_expr at note
-let natE ?(at = no) ~note i = NumE (Num.Nat i) |> mk_expr at note
+let natE ?(at = no) ~note i = NumE (`Nat i) |> mk_expr at note
 let cvtE ?(at = no) ~note (e, nt1, nt2) = CvtE (e, nt1, nt2) |> mk_expr at note
 let unE ?(at = no) ~note (unop, e) = UnE (unop, e) |> mk_expr at note
 let binE ?(at = no) ~note (binop, e1, e2) = BinE (binop, e1, e2) |> mk_expr at note
@@ -85,8 +85,8 @@ let sliceP ?(at = no) (e1, e2) = SliceP (e1, e2) |> mk_path at
 let dotP ?(at = no) a = DotP a |> mk_path at
 
 let numV n = NumV n
-let natV i = assert (i >= Z.zero); NumV (Num.Nat i)
-let intV i = NumV (Num.Int i)
+let natV i = assert (i >= Z.zero); NumV (`Nat i)
+let intV i = NumV (`Int i)
 let natV_of_int i = Z.of_int i |> natV
 let boolV b = BoolV b
 let strV r = StrV r
@@ -178,10 +178,10 @@ let rec typ_to_var_name ty =
   (* TODO: guess this for "var" in el? *)
   | Il.Ast.VarT (id, _) -> id.it
   | Il.Ast.BoolT -> "b"
-  | Il.Ast.NumT NatT -> "n"
-  | Il.Ast.NumT IntT -> "i"
-  | Il.Ast.NumT RatT -> "q"
-  | Il.Ast.NumT RealT -> "r"
+  | Il.Ast.NumT `NatT -> "n"
+  | Il.Ast.NumT `IntT -> "i"
+  | Il.Ast.NumT `RatT -> "q"
+  | Il.Ast.NumT `RealT -> "r"
   | Il.Ast.TextT -> "s"
   | Il.Ast.TupT tys -> List.map typ_to_var_name (List.map snd tys) |> String.concat "_"
   | Il.Ast.IterT (t, _) -> typ_to_var_name t
@@ -223,12 +223,12 @@ let unwrap_numv: value -> Num.num = function
 
 let unwrap_natv v =
   match unwrap_numv v with
-  | Num.Nat n -> assert (n >= Z.zero); n
+  | `Nat n -> assert (n >= Z.zero); n
   | n -> fail_value "unwrap_natv" (NumV n)
 
 let unwrap_intv v =
   match unwrap_numv v with
-  | Num.Int i -> i
+  | `Int i -> i
   | n -> fail_value "unwrap_natv" (NumV n)
 
 let unwrap_natv_to_int (v: value): int = unwrap_natv v |> Z.to_int
@@ -302,7 +302,7 @@ let iterT ty iter = Il.Ast.IterT (ty, iter) $ no_region
 let listT ty = iterT ty Il.Ast.List
 let listnT ty n = Il.Ast.IterT (ty, Il.Ast.ListN (n, None)) $ no_region
 let boolT = Il.Ast.BoolT $ no_region
-let natT = Il.Ast.NumT Num.NatT $ no_region
+let natT = Il.Ast.NumT `NatT $ no_region
 let topT = varT "TOP" []
 let valT = varT "val" []
 let frameT = varT "frame" []

spectec/src/al/eval.ml

@@ -153,15 +153,15 @@ let rec reduce_exp s e : expr =
       let e1' = reduce_exp s e1 in
       let e2' = reduce_exp s e2 in
       (match e1'.it, e2'.it with
-      | ListE es, NumE (Num.Nat i) when i < Z.of_int (List.length es) -> List.nth es (Z.to_int i)
+      | ListE es, NumE (`Nat i) when i < Z.of_int (List.length es) -> List.nth es (Z.to_int i)
       | _ -> AccE (e1', IdxP e2' $ p.at) $> e
       )
     | SliceP (e2, e3) ->
       let e1' = reduce_exp s e1 in
       let e2' = reduce_exp s e2 in
       let e3' = reduce_exp s e3 in
       (match e1'.it, e2'.it, e3'.it with
-      | ListE es, NumE (Num.Nat i), NumE (Num.Nat n) when Z.(i + n) < Z.of_int (List.length es) ->
+      | ListE es, NumE (`Nat i), NumE (`Nat n) when Z.(i + n) < Z.of_int (List.length es) ->
         ListE (Lib.List.take (Z.to_int n) (Lib.List.drop (Z.to_int i) es))
       | _ -> AccE (e1', SliceP (e2', e3') $ p.at)
       ) $> e
@@ -219,7 +219,7 @@ let rec reduce_exp s e : expr =
   | LenE e1 ->
     let e1' = reduce_exp s e1 in
     (match e1'.it with
-    | ListE es -> NumE (Num.Nat (Z.of_int (List.length es)))
+    | ListE es -> NumE (`Nat (Z.of_int (List.length es)))
     | _ -> LenE e1'
     ) $> e
   | TupE es -> TupE (List.map (reduce_exp s) es) $> e
@@ -250,11 +250,11 @@ let rec reduce_exp s e : expr =
       | List | List1 ->
         let n = List.length (as_list_exp (List.hd es')) in
         if iter' = List || n >= 1 then
-          let en = NumE (Num.Nat (Z.of_int n)) $$ e.at % (Il.Ast.NumT Num.NatT $ e.at) in
+          let en = NumE (`Nat (Z.of_int n)) $$ e.at % (Il.Ast.NumT `NatT $ e.at) in
           reduce_exp s (IterE (e1', (ListN (en, None), xes')) $> e)
         else
           IterE (e1', iterexp') $> e
-      | ListN ({it = NumE (Num.Nat n'); _}, ido) ->
+      | ListN ({it = NumE (`Nat n'); _}, ido) ->
         let ess' = List.map as_list_exp es' in
         let ns = List.map List.length ess' in
         let n = Z.to_int n' in
@@ -264,7 +264,7 @@ let rec reduce_exp s e : expr =
             let s = List.fold_right2 Subst.add ids esI' Subst.empty in
             let s' =
               Option.fold ido ~none:s ~some:(fun id ->
-                let en = NumE (Num.Nat (Z.of_int i)) $$ no_region % (Il.Ast.NumT Num.NatT $ no_region) in
+                let en = NumE (`Nat (Z.of_int i)) $$ no_region % (Il.Ast.NumT `NatT $ no_region) in
                 Subst.add id en s
               )
             in Subst.subst_exp s' e1'
@@ -306,7 +306,7 @@ and reduce_path s e p f =
       let e1' = reduce_exp s e1 in
       let f' e' p1' =
         match e'.it, e1'.it with
-        | ListE es, NumE (Num.Nat i) when i < Z.of_int (List.length es) ->
+        | ListE es, NumE (`Nat i) when i < Z.of_int (List.length es) ->
           ListE (List.mapi (fun j eJ -> if Z.of_int j = i then f eJ p1' else eJ) es) $> e'
         | _ ->
           f e' (ps @ [IdxP (e1') $> p'])
@@ -317,7 +317,7 @@ and reduce_path s e p f =
       let e2' = reduce_exp s e2 in
       let f' e' p1' =
         match e'.it, e1'.it, e2'.it with
-        | ListE es, NumE (Num.Nat i), NumE (Num.Nat n) when Z.(i + n) < Z.of_int (List.length es) ->
+        | ListE es, NumE (`Nat i), NumE (`Nat n) when Z.(i + n) < Z.of_int (List.length es) ->
           let e1' = ListE Lib.List.(take (Z.to_int i) es) $> e' in
           let e2' = ListE Lib.List.(take (Z.to_int n) (drop (Z.to_int i) es)) $> e' in
           let e3' = ListE Lib.List.(drop Z.(to_int (i + n)) es) $> e' in

spectec/src/al/valid.ml

@@ -175,7 +175,7 @@ and ground_typ_of (typ: typ) : typ =
     let typ' = IlEnv.find_var !il_env id in
     if Il.Eq.eq_typ typ typ' then typ else ground_typ_of typ'
   (* NOTE: Consider `fN` as a `NumT` to prevent diverging ground type *)
-  | VarT (id, _) when id.it = "fN" -> NumT RealT $ typ.at
+  | VarT (id, _) when id.it = "fN" -> NumT `RealT $ typ.at
   | VarT (id, args) ->
     get_deftyps id args
     |> unify_deftyps_opt

spectec/src/backend-interpreter/construct.ml

@@ -5,7 +5,6 @@ open Value
 open Al.Ast
 open Al.Al_util
 open Al.Print
-open Xl
 open Source
 open Util
 
@@ -223,7 +222,7 @@ let al_to_tag_type: value -> tag_type = function
 
 (* Destruct operator *)
 
-let num i = Num.Nat (Z.of_int i)
+let num i = `Nat (Z.of_int i)
 let two = num 2
 let four = num 4
 let eight = num 8

spectec/src/backend-interpreter/interpreter.ml

@@ -371,7 +371,7 @@ and eval_expr env expr =
   (* TODO : This should be replaced with executing the validation algorithm *)
   | IsValidE e ->
     let valid_lim k = function
-      | TupV [ NumV (Num.Nat n); NumV (Num.Nat m) ] -> n <= m && m <= k
+      | TupV [ NumV (`Nat n); NumV (`Nat m) ] -> n <= m && m <= k
       | _ -> false
     in
     (match eval_expr env e with

spectec/src/backend-interpreter/manual.ml

@@ -1,6 +1,5 @@
 open Reference_interpreter
 open Al
-open Xl
 open Ast
 open Al_util
 open Ds
@@ -42,7 +41,7 @@ let ref_type =
   (* exception *)
   | [CaseV ("REF.EXN_ADDR", [ _ ])] -> CaseV ("REF", [ nonull; nullary "EXN"])
   (* array/func/struct addr *)
-  | [CaseV (name, [ NumV (Num.Nat i) ])]
+  | [CaseV (name, [ NumV (`Nat i) ])]
   when String.starts_with ~prefix:"REF." name && String.ends_with ~suffix:"_ADDR" name ->
     let field_name = String.sub name 4 (String.length name - 9) in
     let object_ = listv_nth (Ds.Store.access (field_name ^ "S")) (Z.to_int i) in
@@ -116,7 +115,7 @@ let module_ok = function
   | vs -> Numerics.error_values "$Module_ok" vs
 
 let externaddr_type = function
-  | [ CaseV (name, [ NumV (Num.Nat z) ]); t ] ->
+  | [ CaseV (name, [ NumV (`Nat z) ]); t ] ->
     (try
       let addr = Z.to_int z in
       let externaddr_type =