Stop vector_typ_args_of from failing when order is a variable

Now it just returns the actual arguments and a separate function
calculates the start index when required.

6 files changed, 43 insertions, 34 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 08532eb4..97ce3896 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -459,6 +459,9 @@ let id_loc = function
 let kid_loc = function
   | Kid_aux (_, l) -> l
 
+let typ_loc = function
+  | Typ_aux (_, l) -> l
+
 let pat_loc = function
   | P_aux (_, (l, _)) -> l
 
@@ -855,17 +858,19 @@ let typ_app_args_of = function
 
 let rec vector_typ_args_of typ = match typ_app_args_of typ with
   | ("vector", [Typ_arg_nexp len; Typ_arg_order ord; Typ_arg_typ etyp], l) ->
-     begin
-       match ord with
-       | Ord_aux (Ord_inc, _) -> (nint 0, nexp_simp len, ord, etyp)
-       | Ord_aux (Ord_dec, _) -> (nexp_simp (nminus len (nint 1)), nexp_simp len, ord, etyp) (* FIXME to return 3 arguments *)
-       | _ -> raise (Reporting_basic.err_typ l "Can't calculate start index without order")
-     end
+     (nexp_simp len, ord, etyp)
   | ("register", [Typ_arg_typ rtyp], _) -> vector_typ_args_of rtyp
   | (_, _, l) ->
      raise (Reporting_basic.err_typ l
        ("vector_typ_args_of called on non-vector type " ^ string_of_typ typ))
 
+let vector_start_index typ =
+  let (len, ord, etyp) = vector_typ_args_of typ in
+  match ord with
+  | Ord_aux (Ord_inc, _) -> nint 0
+  | Ord_aux (Ord_dec, _) -> nexp_simp (nminus len (nint 1))
+  | _ -> raise (Reporting_basic.err_typ (typ_loc typ) "Can't calculate start index without order")
+
 let is_order_inc = function
   | Ord_aux (Ord_inc, _) -> true
   | Ord_aux (Ord_dec, _) -> false
@@ -878,7 +883,7 @@ let is_bit_typ = function
 
 let is_bitvector_typ typ =
   if is_vector_typ typ then
-    let (_,_,_,etyp) = vector_typ_args_of typ in
+    let (_,_,etyp) = vector_typ_args_of typ in
     is_bit_typ etyp
   else false
 
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 951f5bed..4ceeea44 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -178,7 +178,7 @@ val map_letbind_annot : ('a annot -> 'b annot) -> 'a letbind -> 'b letbind
 (* Extract locations from identifiers *)
 val id_loc : id -> Parse_ast.l
 val kid_loc : kid -> Parse_ast.l
-
+val typ_loc : typ -> Parse_ast.l
 val pat_loc : 'a pat -> Parse_ast.l
 val exp_loc : 'a exp -> Parse_ast.l
 val def_loc : 'a def -> Parse_ast.l
@@ -285,7 +285,8 @@ val is_bit_typ : typ -> bool
 val is_bitvector_typ : typ -> bool
 
 val typ_app_args_of : typ -> string * typ_arg_aux list * Ast.l
-val vector_typ_args_of : typ -> nexp * nexp * order * typ
+val vector_typ_args_of : typ -> nexp * order * typ
+val vector_start_index : typ -> nexp
 val destruct_range : typ -> (nexp * nexp) option
 
 val is_order_inc : order -> bool
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index c7956c21..08feccbe 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -2710,7 +2710,7 @@ let deps_of_uvar l fn_id env arg_deps = function
   | U_typ typ -> InFun (deps_of_typ l env.kid_deps arg_deps typ)
 
 let mk_subrange_pattern vannot vstart vend =
-  let (_,len,ord,typ) = vector_typ_args_of (Env.base_typ_of (env_of_annot vannot) (typ_of_annot vannot)) in
+  let (len,ord,typ) = vector_typ_args_of (Env.base_typ_of (env_of_annot vannot) (typ_of_annot vannot)) in
   match ord with
   | Ord_aux (Ord_var _,_) -> None
   | Ord_aux (ord',_) ->
@@ -3020,7 +3020,7 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
             typ
        in
        if is_bitvector_typ typ then
-         let _,size,_,_ = vector_typ_args_of typ in
+         let size,_,_ = vector_typ_args_of typ in
          let Nexp_aux (size,_) as size_nexp = simplify_size_nexp env tenv size in
          let is_tyvar_parameter v =
            List.exists (fun k -> Kid.compare k v == 0) env.top_kids
@@ -3488,8 +3488,8 @@ let rewrite_app env typ (id,args) =
         when is_append append && is_subrange subrange1 && is_subrange subrange2 &&
           is_constant_vec_typ env (typ_of e1) &&
           not (is_constant_range (start1, end1) || is_constant_range (start2, end2)) ->
-       let (start,size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
-       let (_,size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in
+       let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
+       let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in
        let midsize = nminus size size1 in
        let midtyp = vector_typ midsize order bittyp in
        E_app (append,
@@ -3507,8 +3507,8 @@ let rewrite_app env typ (id,args) =
         when is_append append && is_slice slice1 && is_slice slice2 &&
           is_constant_vec_typ env (typ_of e1) &&
           not (is_constant length1 || is_constant length2) ->
-       let (start,size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
-       let (_,size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in
+       let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
+       let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in
        let midsize = nminus size size1 in
        let midtyp = vector_typ midsize order bittyp in
        E_app (append,
@@ -3548,8 +3548,8 @@ let rewrite_app env typ (id,args) =
         when is_append append1 && is_slice slice1 && is_zeros zeros1 &&
           is_constant_vec_typ env (typ_of e1) &&
           not (is_constant length1 || is_constant length2) ->
-       let (start,size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
-       let (_,size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in
+       let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
+       let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in
        let midsize = nminus size size1 in
        let midtyp = vector_typ midsize order bittyp in
        E_cast (typ,
@@ -3919,7 +3919,7 @@ let rewrite_toplevel_nexps (Defs defs) =
          | Some nexp -> Some nexp
          | None ->
             if is_bitvector_typ typ' then
-              let (_,size,_,_) = vector_typ_args_of typ' in
+              let (size,_,_) = vector_typ_args_of typ' in
               Some size
             else None
        in match nexp_opt with
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 18fcbf69..025e876e 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -811,8 +811,8 @@ let doc_exp_lem, doc_let_lem =
        anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp ctxt recordtyp) fexps))
     | E_vector exps ->
        let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
-       let (start, len, order, etyp) =
-         if is_vector_typ t then vector_typ_args_of t
+       let start, (len, order, etyp) =
+         if is_vector_typ t then vector_start_index t, vector_typ_args_of t
          else raise (Reporting_basic.err_unreachable l
            "E_vector of non-vector type") in
        let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in
@@ -1012,7 +1012,7 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
         | _ -> ftyp in
       let (start, is_inc) =
         try
-          let (start, _, ord, _) = vector_typ_args_of base_ftyp in
+          let start, (_, ord, _) = vector_start_index base_ftyp, vector_typ_args_of base_ftyp in
           match nexp_simp start with
           | Nexp_aux (Nexp_constant i, _) -> (i, is_order_inc ord)
           | _ ->
@@ -1296,7 +1296,7 @@ let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) =
        let env = env_of_annot annot in
        let rt = Env.base_typ_of env typ in
        if is_vector_typ rt then
-         let (start, size, order, etyp) = vector_typ_args_of rt in
+         let start, (size, order, etyp) = vector_start_index rt, vector_typ_args_of rt in
          if is_bit_typ etyp && is_nexp_constant start && is_nexp_constant size then
            let o = if is_order_inc order then "true" else "false" in
            (doc_op equals)
diff --git a/src/rewrites.ml b/src/rewrites.ml
index b328307d..80c339e6 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -361,7 +361,7 @@ let rewrite_sizeof (Defs defs) =
                       (try
                          (match Env.get_val_spec id_length (env_of_annot annot) with
                           | _ ->
-                             let (_,len,_,_) = vector_typ_args_of typ_aux in
+                             let (len,_,_) = vector_typ_args_of typ_aux in
                              let exp = E_app (id_length, [E_aux (E_id id, annot)]) in
                              [len, exp])
                        with
@@ -738,7 +738,7 @@ let remove_vector_concat_pat pat =
 
       (* FIXME *)
       let subv = fix_eff_exp (E_aux (E_vector_subrange (root, index_i, index_j), cannot)) in
-      (* let (_, _, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of root) (typ_of root)) in
+      (* let (_, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of root) (typ_of root)) in
       let subrange_id = if is_order_inc ord then "bitvector_subrange_inc" else "bitvector_subrange_dec" in
       let subv = fix_eff_exp (E_aux (E_app (mk_id subrange_id, [root; index_i; index_j]), cannot)) in *)
 
@@ -757,8 +757,8 @@ let remove_vector_concat_pat pat =
     let p_aux = function
       | ((P_as (P_aux (P_vector_concat pats,rannot'),rootid),decls),rannot) ->
          let rtyp = Env.base_typ_of (env_of_annot rannot') (typ_of_annot rannot') in
-         let (start,last_idx) = (match vector_typ_args_of rtyp with
-          | (Nexp_aux (Nexp_constant start,_), Nexp_aux (Nexp_constant length,_), ord, _) ->
+         let (start,last_idx) = (match vector_start_index rtyp, vector_typ_args_of rtyp with
+          | Nexp_aux (Nexp_constant start,_), (Nexp_aux (Nexp_constant length,_), ord, _) ->
              (start, if is_order_inc ord
                      then Big_int.sub (Big_int.add start length) (Big_int.of_int 1)
                      else Big_int.add (Big_int.sub start length) (Big_int.of_int 1))
@@ -767,7 +767,7 @@ let remove_vector_concat_pat pat =
               ("unname_vector_concat_elements: vector of unspecified length in vector-concat pattern"))) in
          let rec aux typ_opt (pos,pat_acc,decl_acc) (P_aux (p,cannot),is_last) =
            let ctyp = Env.base_typ_of (env_of_annot cannot) (typ_of_annot cannot) in
-           let (_,length,ord,_) = vector_typ_args_of ctyp in
+           let (length,ord,_) = vector_typ_args_of ctyp in
            let (pos',index_j) = match length with
              | Nexp_aux (Nexp_constant i,_) ->
                 if is_order_inc ord
@@ -886,7 +886,7 @@ let remove_vector_concat_pat pat =
         if is_vector_typ typ then
           match p, vector_typ_args_of typ with
           | P_vector ps,_ -> acc @ ps
-          | _, (_,Nexp_aux (Nexp_constant length,_),_,_) ->
+          | _, (Nexp_aux (Nexp_constant length,_),_,_) ->
              acc @ (List.map wild (range Big_int.zero (Big_int.sub length (Big_int.of_int 1))))
           | _, _ ->
             (*if is_last then*) acc @ [wild Big_int.zero]
@@ -898,7 +898,7 @@ let remove_vector_concat_pat pat =
       let has_length (P_aux (p,annot)) =
         let typ = Env.base_typ_of (env_of_annot annot) (typ_of_annot annot) in
         match vector_typ_args_of typ with
-        | (_,Nexp_aux (Nexp_constant length,_),_,_) -> true
+        | (Nexp_aux (Nexp_constant length,_),_,_) -> true
         | _ -> false in
 
       let ps_tagged = tag_last ps in
@@ -1225,7 +1225,8 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
     Some (check_eq_exp (strip_exp elem) (strip_exp exp)) in
 
   let test_subvec_exp rootid l typ i j lits =
-    let (start, length, ord, _) = vector_typ_args_of typ in
+    let start = vector_start_index typ in
+    let (length, ord, _) = vector_typ_args_of typ in
     let subvec_exp =
       match start, length with
       | Nexp_aux (Nexp_constant s, _), Nexp_aux (Nexp_constant l, _)
@@ -1256,7 +1257,8 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
   (* Collect guards and let bindings *)
   let guard_bitvector_pat =
     let collect_guards_decls ps rootid t =
-      let (start,_,ord,_) = vector_typ_args_of t in
+      let start = vector_start_index t in
+      let (_,ord,_) = vector_typ_args_of t in
       let start_idx = match start with
       | Nexp_aux (Nexp_constant s, _) -> s
       | _ ->
@@ -2280,11 +2282,12 @@ let rewrite_tuple_vector_assignments defs =
        let typ = Env.base_typ_of env (typ_of exp) in
        if is_vector_typ typ then
          (* let _ = Pretty_print_common.print stderr (Pretty_print_sail.doc_exp (E_aux (e_aux, annot))) in *)
-         let (start, _, ord, etyp) = vector_typ_args_of typ in
+         let start = vector_start_index typ in
+         let (_, ord, etyp) = vector_typ_args_of typ in
          let len (LEXP_aux (le, lannot)) =
            let ltyp = Env.base_typ_of env (typ_of_annot lannot) in
            if is_vector_typ ltyp then
-             let (_, len, _, _) = vector_typ_args_of ltyp in
+             let (len, _, _) = vector_typ_args_of ltyp in
              match nexp_simp len with
              | Nexp_aux (Nexp_constant len, _) -> len
              | _ -> (Big_int.of_int 1)
diff --git a/src/state.ml b/src/state.ml
index 8e024179..40ec80ad 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -157,7 +157,7 @@ let add_regval_conv id typ defs =
 
 let rec regval_convs_lem mwords (Typ_aux (t, _) as typ) = match t with
   | Typ_app _ when is_vector_typ typ && not (mwords && is_bitvector_typ typ) ->
-     let _, size, ord, etyp = vector_typ_args_of typ in
+     let size, ord, etyp = vector_typ_args_of typ in
      let size = string_of_nexp (nexp_simp size) in
      let is_inc = if is_order_inc ord then "true" else "false" in
      let etyp_of, of_etyp = regval_convs_lem mwords etyp in