Added support for vector append and indexing

12 files changed, 187 insertions, 3 deletions

diff --git a/src/type_check_new.ml b/src/type_check_new.ml
index 495d52b7..65227d5e 100644
--- a/src/type_check_new.ml
+++ b/src/type_check_new.ml
@@ -229,6 +229,8 @@ end
 let unaux_nexp (Nexp_aux (nexp, _)) = nexp
 
 let unaux_order (Ord_aux (ord, _)) = ord
+
+let unaux_typ (Typ_aux (typ, _)) = typ
                                         
 let rec nexp_subst sv subst (Nexp_aux (nexp, l)) = Nexp_aux (nexp_subst_aux sv subst nexp, l)
 and nexp_subst_aux sv subst = function
@@ -266,6 +268,21 @@ and typ_subst_arg_nexp_aux sv subst = function
   | Typ_arg_order ord -> Typ_arg_order ord
   | Typ_arg_effect eff -> Typ_arg_effect eff
 
+let rec typ_subst_typ sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_typ_aux sv subst typ, l)
+and typ_subst_typ_aux sv subst = function
+  | Typ_wild -> Typ_wild
+  | Typ_id v -> Typ_id v
+  | Typ_var kid -> if Kid.compare kid sv = 0 then subst else Typ_var kid
+  | Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_typ sv subst typ1, typ_subst_typ sv subst typ2, effs)
+  | Typ_tup typs -> Typ_tup (List.map (typ_subst_typ sv subst) typs)
+  | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_nexp sv subst) args)
+and typ_subst_arg_nexp sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_nexp_aux sv subst arg, l)
+and typ_subst_arg_nexp_aux sv subst = function
+  | Typ_arg_nexp nexp -> Typ_arg_nexp nexp
+  | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_typ sv subst typ)
+  | Typ_arg_order ord -> Typ_arg_order ord
+  | Typ_arg_effect eff -> Typ_arg_effect eff
+                                         
 let order_subst_aux sv subst = function
   | Ord_var kid -> if Kid.compare kid sv = 0 then subst else Ord_var kid
   | Ord_inc -> Ord_inc
@@ -873,7 +890,7 @@ let unify l env typ1 typ2 =
     | Typ_id v1, Typ_id v2 ->
        if Id.compare v1 v2 = 0 then KBindings.empty
        else unify_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2)
-    | Typ_var _, Typ_var _ -> unify_error l "Raw identifiers during unification"
+    | Typ_var kid, _ -> KBindings.singleton kid (U_typ typ2)
     | Typ_tup typs1, Typ_tup typs2 ->
        begin
          try List.fold_left (KBindings.merge (merge_unifiers l)) KBindings.empty (List.map2 (unify_typ l) typs1 typs2) with
@@ -1009,6 +1026,10 @@ let is_nat_kid kid = function
 let is_order_kid kid = function
   | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_order, _)], _), kid'), _) -> Kid.compare kid kid' = 0
   | _ -> false
+
+let is_typ_kid kid = function
+  | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_type, _)], _), kid'), _) -> Kid.compare kid kid' = 0
+  | _ -> false
            
 let rec instantiate_quants quants kid uvar = match quants with
   | [] -> []
@@ -1023,14 +1044,18 @@ let rec instantiate_quants quants kid uvar = match quants with
           if is_order_kid kid kinded_id
           then instantiate_quants quants kid uvar
           else quant :: instantiate_quants quants kid uvar
+       | U_typ typ ->
+          if is_typ_kid kid kinded_id
+          then instantiate_quants quants kid uvar
+          else quant :: instantiate_quants quants kid uvar                         
        | _ -> typ_error Parse_ast.Unknown "Cannot instantiate quantifier"
      end
   | ((QI_aux (QI_const nc, l)) :: quants) ->
      begin
        match uvar with
        | U_nexp nexp ->
-          QI_aux (QI_const (nc_subst_nexp kid (unaux_nexp nexp) nc), l) :: quants
-       | _ -> (QI_aux (QI_const nc, l)) :: quants
+          QI_aux (QI_const (nc_subst_nexp kid (unaux_nexp nexp) nc), l) :: instantiate_quants quants kid uvar
+       | _ -> (QI_aux (QI_const nc, l)) :: instantiate_quants quants kid uvar
      end
 
 let subst_unifiers unifiers typ =
@@ -1038,6 +1063,7 @@ let subst_unifiers unifiers typ =
     match uvar with
     | U_nexp nexp -> typ_subst_nexp kid (unaux_nexp nexp) typ
     | U_order ord -> typ_subst_order kid (unaux_order ord) typ
+    | U_typ subst -> typ_subst_typ kid (unaux_typ subst) typ
     | _ -> typ_error Parse_ast.Unknown "Cannot subst unifier"
   in
   List.fold_left subst_unifier typ (KBindings.bindings unifiers)
@@ -1125,6 +1151,8 @@ and infer_exp env (E_aux (exp_aux, (l, _)) as exp : 'a exp) : tannot exp =
      let checked_exp = check_exp env exp typ in
      annot_exp (E_cast (typ, checked_exp)) typ
   | E_app (f, xs) -> infer_funapp l env f xs None
+  | E_vector_access (v, n) -> infer_funapp l env (mk_id "vector_access") [v; n] None
+  | E_vector_append (v1, v2) -> infer_funapp l env (mk_id "vector_append") [v1; v2] None
   | _ -> typ_error l "Unimplemented"
                    
 and infer_funapp l env f xs ret_ctx_typ =
diff --git a/test/typecheck/fail/vector_access1.sail b/test/typecheck/fail/vector_access1.sail
new file mode 100644
index 00000000..1eef5250
--- /dev/null
+++ b/test/typecheck/fail/vector_access1.sail
@@ -0,0 +1,12 @@
+
+val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access
+
+default Order inc
+
+val bit[4] -> unit effect pure test
+    
+function unit test v =
+{
+  z := vector_access(v,0);
+  z := v[4]
+}
\ No newline at end of file
diff --git a/test/typecheck/fail/vector_access2.sail b/test/typecheck/fail/vector_access2.sail
new file mode 100644
index 00000000..0b4ba7c2
--- /dev/null
+++ b/test/typecheck/fail/vector_access2.sail
@@ -0,0 +1,12 @@
+
+val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access
+
+default Order inc
+
+val bit[4] -> unit effect pure test
+    
+function unit test v =
+{
+  z := vector_access(v,-1);
+  z := v[3]
+}
\ No newline at end of file
diff --git a/test/typecheck/fail/vector_access3.sail b/test/typecheck/fail/vector_access3.sail
new file mode 100644
index 00000000..dd43cfea
--- /dev/null
+++ b/test/typecheck/fail/vector_access3.sail
@@ -0,0 +1,12 @@
+
+val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access
+
+default Order inc
+
+val bit[0] -> unit effect pure test
+    
+function unit test v =
+{
+  z := vector_access(v,0);
+  z := v[0]
+}
\ No newline at end of file
diff --git a/test/typecheck/fail/vector_access4.sail b/test/typecheck/fail/vector_access4.sail
new file mode 100644
index 00000000..31d34eae
--- /dev/null
+++ b/test/typecheck/fail/vector_access4.sail
@@ -0,0 +1,12 @@
+
+val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access
+
+default Order inc
+
+val bit[-5] -> unit effect pure test
+    
+function unit test v =
+{
+  z := vector_access(v,([|0:-5|]) -1);
+  z := v[-1]
+}
\ No newline at end of file
diff --git a/test/typecheck/fail/vector_append1.sail b/test/typecheck/fail/vector_append1.sail
new file mode 100644
index 00000000..e2429380
--- /dev/null
+++ b/test/typecheck/fail/vector_append1.sail
@@ -0,0 +1,18 @@
+
+val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access
+
+val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0.
+  (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append
+
+default Order inc
+
+val (bit[4], bit[4]) -> bit[7] effect pure test
+    
+function bit[7] test (v1, v2) =
+{
+  z := vector_access(v1, 3);
+  z := v1[0];
+  zv := vector_append(v1, v2);
+  zv := v1 : v2;
+  zv
+}
\ No newline at end of file
diff --git a/test/typecheck/fail/vector_append2.sail b/test/typecheck/fail/vector_append2.sail
new file mode 100644
index 00000000..acaeb0b0
--- /dev/null
+++ b/test/typecheck/fail/vector_append2.sail
@@ -0,0 +1,18 @@
+
+val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access
+
+val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0.
+  (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append
+
+default Order inc
+
+val (bit[4], bit[4]) -> bit[9] effect pure test
+    
+function bit[9] test (v1, v2) =
+{
+  z := vector_access(v1, 3);
+  z := v1[0];
+  zv := vector_append(v1, v2);
+  zv := v1 : v2;
+  zv
+}
\ No newline at end of file
diff --git a/test/typecheck/fail/vector_append_gen1.sail b/test/typecheck/fail/vector_append_gen1.sail
new file mode 100644
index 00000000..727d5c14
--- /dev/null
+++ b/test/typecheck/fail/vector_append_gen1.sail
@@ -0,0 +1,14 @@
+
+val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access
+
+val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0.
+  (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append
+
+default Order inc
+
+val forall 'n, 'm. (bit['n], bit['m]) -> bit['n + 'm] effect pure test
+    
+function forall 'n, 'm. bit['n + 'm] test (v1, v2) =
+{
+  v1 : v2;
+}
\ No newline at end of file
diff --git a/test/typecheck/fail/vector_append_gen2.sail b/test/typecheck/fail/vector_append_gen2.sail
new file mode 100644
index 00000000..8e534253
--- /dev/null
+++ b/test/typecheck/fail/vector_append_gen2.sail
@@ -0,0 +1,14 @@
+
+val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access
+
+val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0.
+  (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append
+
+default Order inc
+
+val forall 'n, 'm. (bit['n], bit['m]) -> bit['n + 'm] effect pure test
+    
+function forall 'n, 'm. bit['n + 'm] test (v1, v2) =
+{
+  vector_append(v1, v2);
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/vector_access.sail b/test/typecheck/pass/vector_access.sail
new file mode 100644
index 00000000..9346f5fe
--- /dev/null
+++ b/test/typecheck/pass/vector_access.sail
@@ -0,0 +1,12 @@
+
+val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access
+
+default Order inc
+
+val bit[4] -> unit effect pure test
+    
+function unit test v =
+{
+  z := vector_access(v,3);
+  z := v[3]
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/vector_append.sail b/test/typecheck/pass/vector_append.sail
new file mode 100644
index 00000000..d2f1ca47
--- /dev/null
+++ b/test/typecheck/pass/vector_append.sail
@@ -0,0 +1,18 @@
+
+val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access
+
+val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0.
+  (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append
+
+default Order inc
+
+val (bit[4], bit[4]) -> bit[8] effect pure test
+    
+function bit[8] test (v1, v2) =
+{
+  z := vector_access(v1, 3);
+  z := v1[0];
+  zv := vector_append(v1, v2);
+  zv := v1 : v2;
+  zv
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/vector_append_gen.sail b/test/typecheck/pass/vector_append_gen.sail
new file mode 100644
index 00000000..ddb027ee
--- /dev/null
+++ b/test/typecheck/pass/vector_append_gen.sail
@@ -0,0 +1,14 @@
+
+val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access
+
+val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0.
+  (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append
+
+default Order inc
+
+val forall 'n, 'm, 'n >= 0, 'm >= 0. (bit['n], bit['m]) -> bit['n + 'm] effect pure test
+    
+function forall 'n, 'm. bit['n + 'm] test (v1, v2) =
+{
+  vector_append(v1, v2);
+}
\ No newline at end of file