Allow global type variables

Wanted to know yesterday if possible to parameterise specification by 32/64 bits in context of RISCV - i.e. can we do something like

let size = 32
type xlen = bits(size)

This patch tweaks the typechecker slightly to allow type variables to be introduced by global let bindings in the same way they can be introduced by local let bindings (techically this was always allowed, but some bugs prevented it from really working), so

let 'size : atom(32) = 32

means we have a global type variable 'size, with a global constraint 'size  = 32

We can go further though...

let 'size : {|32, 64|} = 32

means we have a global type variable 'size with a constraint 'size = 32 | 'size = 64, in this case the specification will only typecheck if the specification is correct for BOTH 'size = 32 and 'size = 64. This also creates a global binding size (note no tick) with value 32 and type atom('size), one can also do

let _ as 'size : {|32, 64|} = 32

which won't create the binding, only the type variable.

These global type variables are bound to not be very well understood by certain parts of sail, so typical here be dragons warning etc.

1 files changed, 10 insertions, 1 deletions

diff --git a/src/type_check.ml b/src/type_check.ml
index 2b558421..248faceb 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -634,7 +634,10 @@ end = struct
 
   let freshen_kid env kid (typq, typ) =
     let fresh = fresh_kid ~kid:kid env in
-    (typquant_subst_kid kid fresh typq, typ_subst_kid kid fresh typ)
+    if KidSet.mem kid (KidSet.of_list (List.map kopt_kid (quant_kopts typq))) then
+      (typquant_subst_kid kid fresh typq, typ_subst_kid kid fresh typ)
+    else
+      (typq, typ)
 
   let freshen_bind env bind =
     List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars)
@@ -2390,6 +2393,12 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
           let env = Env.add_constraint (nc_and (nc_lteq lo (nvar kid)) (nc_lteq (nvar kid) hi)) env in
           let typed_pat, env, guards = bind_pat env pat (atom_typ (nvar kid)) in
           annot_pat (P_var (typed_pat, kid)) typ, env, guards
+       | None, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n, _)]), _)
+            when Id.compare id (mk_id "atom") == 0 ->
+          let env = Env.add_typ_var kid BK_nat env in
+          let env = Env.add_constraint (nc_eq (nvar kid) n) env in
+          let typed_pat, env, guards = bind_pat env pat (atom_typ (nvar kid)) in
+          annot_pat (P_var (typed_pat, kid)) typ, env, guards
        | None, _ -> typ_error l ("Cannot bind type variable against non existential or numeric type")
      end
   | P_wild -> annot_pat P_wild typ, env, []