changes to ocaml pp to allow mips->ocaml to compile

3 files changed, 66 insertions, 14 deletions

diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml
index 4713f9a7..0072d5b6 100644
--- a/src/gen_lib/sail_values.ml
+++ b/src/gen_lib/sail_values.ml
@@ -3,7 +3,7 @@ open Big_int_Z
 (* only expected to be 0, 1, 2; 2 represents undef *)
 type vbit = Vone | Vzero | Vundef
 type number = Big_int_Z.big_int
-
+type _bool = vbit
 type value =
   | Vvector of vbit array * int * bool
   | VvectorR of value array * int * bool
@@ -20,6 +20,10 @@ let is_one_big i =
   then Vone
   else Vzero
 
+
+let exit _ = failwith "called exit"
+
+
 let is_one i =
   if i = 1 then Vone else Vzero
 
@@ -40,11 +44,19 @@ let get_start = function
   | Vvector(_,s,o) | Vregister(_,s,o,_) | VvectorR(_,s,o) -> s
   | _ -> assert false  
   
+let set_start i = function
+  | Vvector(a,start,dir) -> Vvector(a,i,dir)
+  | Vregister(bits,start,dir,regfields) -> Vregister(bits,i,dir,regfields)
+  | VvectorR(a,start,dir) -> VvectorR(a,i,dir)
+  | _ -> assert false  
+
 let length = function
   | Vvector(array,_,_) -> Array.length array
   | Vregister(array,_,_,_) -> Array.length !array
   | VvectorR(array,_,_) -> Array.length array
   | _ -> assert false
+  
+let set_start_to_length v = set_start (length v) v
 
 let length_big v = big_int_of_int (length v)
 
@@ -779,8 +791,8 @@ let rec arith_op_no0 op (l,r) =
   then None
   else Some (op l r)
 
-let modulo = arith_op_no0 (mod)
-let quot = arith_op_no0 (/)
+let modulo = arith_op (mod)
+let quot = arith_op (/)
 
 let rec arith_op_vec_no0 op sign size (l,r) =
   let ord = get_ord l in
@@ -986,9 +998,35 @@ let gteq_range_vec_big = compare_op_range_vec_big ge_big_int true
 
 
 let eq (l,r) = if l == r then Vone else Vzero
+let eq_vec_vec (l,r) = eq (to_num true l, to_num true r)
+let eq_vec (l,r) = eq_vec_vec(l,r)
 let eq_vec_range (l,r) = eq (to_num false l,r)
 let eq_range_vec (l,r) = eq (l, to_num false r)
-let eq_vec_vec (l,r) = eq (to_num true l, to_num true r)
+let eq_range = eq
+let eq_bit = bitwise_binop_bit (=)
 
 let neq (l,r) = bitwise_not_bit (eq (l,r))
 let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec(l,r))
+let neq_bit (l,r) = bitwise_not_bit (eq_bit(l,r))
+
+let mask (n,v) = match v with
+  | Vvector (bits,start,dir) ->
+     let current_size = Array.length bits in 
+     let to_drop = (current_size - n) in
+     let bits' = Array.sub bits to_drop n in
+     Vvector (bits',(if dir then 0 else n-1), dir)
+  | VvectorR (bits,start,dir) ->
+     let current_size = Array.length bits in 
+     let to_drop = (current_size - n) in
+     let bits' = Array.sub bits to_drop n in
+     VvectorR (bits',(if dir then 0 else n-1), dir)
+  | Vregister _ -> failwith "mask not implemented for Vregister"
+  | Vbit _ -> failwith "mask called for bit"
+
+let slice_raw (v, i, j) = match v with
+  | Vvector (bs, start, is_inc) ->
+     let bits = Array.sub bs i j in
+     let len = Array.length bits in
+     Vvector (bits, (if is_inc then 0 else len - 1), is_inc)
+  | _ -> failwith "slice_raw only implemented for VVector"
+let _slice_raw = slice_raw
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index d526a6ed..83b0cabf 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -1535,7 +1535,7 @@ let doc_id_ocaml (Id_aux(i,_)) =
   | Id("bit") -> string "vbit"
   | Id i -> string (if i.[0] = '\'' || is_number(i.[0])
                     then "_" ^ i
-                    else  String.uncapitalize i)
+                    else  "_" ^ (String.uncapitalize i))
   | DeIid x ->
       (* add an extra space through empty to avoid a closing-comment
        * token in case of x ending with star. *)
@@ -1544,7 +1544,7 @@ let doc_id_ocaml (Id_aux(i,_)) =
 let doc_id_ocaml_type (Id_aux(i,_)) =
   match i with
   | Id("bit") -> string "vbit"
-  | Id i -> string (String.uncapitalize i)
+  | Id i -> string ("_" ^ (String.uncapitalize i))
   | DeIid x ->
       (* add an extra space through empty to avoid a closing-comment
        * token in case of x ending with star. *)
@@ -1637,9 +1637,9 @@ let doc_pat_ocaml =
   | P_typ(typ,p) -> doc_op colon (pat p) (doc_typ_ocaml typ)
   | P_app(id,[]) ->
     (match annot with
-     | Base(_,Constructor n,_,_,_,_) ->
+     | Base(_,(Constructor n | Enum n),_,_,_,_) ->
        doc_id_ocaml_ctor n id
-     | _ -> empty)
+     | _ -> failwith "encountered unexpected P_app pattern")
   | P_vector pats ->
     let non_bit_print () =
       parens
@@ -1798,7 +1798,19 @@ let doc_exp_ocaml, doc_let_ocaml =
         if read_registers
         then parens (string "read_register" ^^ space ^^ exp e)
         else exp e
-      | _ -> (parens (doc_op colon (group (exp e)) (doc_typ_ocaml typ))))
+      | _ -> 
+         let (Typ_aux (t,_)) = typ in
+             (match t with
+            | Typ_app (Id_aux (Id "vector",_), [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i,_)),_);_;_;_]) ->
+               parens ((concat [string "set_start";space;string (string_of_int i)]) ^//^
+                           exp e)
+            | Typ_var (Kid_aux (Var "length",_)) ->
+               parens ((string "set_start_to_length") ^//^ exp e)
+            | _ -> 
+               parens (doc_op colon (group (exp e)) (doc_typ_ocaml typ)))
+
+
+)
     | E_tuple exps ->
       parens (separate_map comma exp exps)
     | E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
@@ -2132,7 +2144,8 @@ let doc_dec_ocaml (DEC_aux (reg,(l,annot))) =
     (match annot with
      | Base((_,t),_,_,_,_,_) ->
        (match t.t with
-        | Tapp("register", [TA_typ {t= Tapp("vector", [TA_nexp start; TA_nexp size; TA_ord order; TA_typ itemt])}]) ->
+        | Tapp("register", [TA_typ {t= Tapp("vector", [TA_nexp start; TA_nexp size; TA_ord order; TA_typ itemt])}]) 
+        | Tapp("register", [TA_typ {t= Tabbrev(_,{t=Tapp("vector", [TA_nexp start; TA_nexp size; TA_ord order; TA_typ itemt])})}]) ->
           (match itemt.t,start.nexp,size.nexp with
            | Tid "bit", Nconst start, Nconst size ->
              let o = if order.order = Oinc then string "true" else string "false" in
@@ -2154,10 +2167,10 @@ let doc_dec_ocaml (DEC_aux (reg,(l,annot))) =
           separate space [string "let";
                           doc_id_ocaml id;
                           equals;
-                          string idt;
+                          doc_id_ocaml (Id_aux (Id idt, Unknown));
                           string "None"]
-        |_-> empty)
-     | _ ->  empty)
+        |_-> failwith "type was not handled in register declaration")
+     | _ -> failwith "annot was not Base")
     | DEC_alias(id,alspec) -> empty (*
         doc_op equals (string "register alias" ^^ space ^^ doc_id id) (doc_alias alspec) *)
     | DEC_typ_alias(typ,id,alspec) -> empty (*
diff --git a/src/rewriter.ml b/src/rewriter.ml
index dc96b952..bd0670f4 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -1347,7 +1347,8 @@ let rewrite_defs_separate_numbs defs = rewrite_defs_base
      rewrite_defs = rewrite_defs_base} defs
 
 let rewrite_defs_ocaml defs =
-  let defs_vec_concat_removed = rewrite_defs_remove_vector_concat defs in
+  let defs_sorted = top_sort_defs defs in
+  let defs_vec_concat_removed = rewrite_defs_remove_vector_concat defs_sorted in
   let defs_lifted_assign = rewrite_defs_exp_lift_assign defs_vec_concat_removed in
   let defs_separate_nums = rewrite_defs_separate_numbs defs_lifted_assign in
   defs_separate_nums