summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/gen_lib/sail_values.lem38
-rw-r--r--src/gen_lib/state.lem6
-rw-r--r--src/gen_lib/vector.lem12
-rw-r--r--src/pretty_print.ml521
4 files changed, 355 insertions, 222 deletions
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index c47e763f..a51a0091 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -13,15 +13,7 @@ let get_elements (Vector elements _) = elements
let get_start (Vector _ s) = s
let length (Vector bs _) = length bs
-let rec nth n xs = match (n,l) with
- | (0,x :: xs) -> x
- | (n + 1,x :: xs) -> nth n xs
-end
-
-let vector_access (Vector bs start) n =
- if is_inc then nth bs (n - start) else nth bs (start - n)
-
-
+(*
let write_two_registers r1 r2 vec =
let size = length_register r1 in
let start = get_start vec in
@@ -32,7 +24,7 @@ let write_two_registers r1 r2 vec =
vec (if is_inc then size - start else start - size)
(if is_inc then vsize - start else start - vsize) in
write_register r1 r1_v >> write_register r2 r2_v
-
+ *)
let rec replace bs ((n : nat),b') = match (n,bs) with
| (_, []) -> []
@@ -141,7 +133,7 @@ let rec add_one_bit bs co i =
(* | Vundef,_ -> assert false*)
end
-let to_vec len (n : integer) =
+let to_vec (len,(n : integer)) =
let bs = List.replicate len B0 in
let start = if is_inc then 0 else len-1 in
if n = 0 then Vector bs start
@@ -152,6 +144,8 @@ let to_vec len (n : integer) =
let (Vector bs start) = bitwise_not (Vector abs_bs start) in
Vector (add_one_bit bs false (len-1)) start
+let to_vec_inc = to_vec
+let to_vec_dec = to_vec
let to_vec_undef len =
Vector (replicate len BU) (if is_inc then 0 else len-1)
@@ -167,7 +161,7 @@ let power = uncurry integerPow
let arith_op_vec op sign size (l,r) =
let (l',r') = (to_num sign l, to_num sign r) in
let n = op l' r' in
- to_vec (size * (length l)) n
+ to_vec (size * (length l),n)
let add_vec = arith_op_vec integerAdd false 1
let add_vec_signed = arith_op_vec integerAdd true 1
@@ -176,7 +170,7 @@ let multiply_vec = arith_op_vec integerMult false 2
let multiply_vec_signed = arith_op_vec integerMult true 2
let arith_op_vec_range op sign size (l,r) =
- arith_op_vec op sign size (l, to_vec (length l) r)
+ arith_op_vec op sign size (l, to_vec (length l,r))
let add_vec_range = arith_op_vec_range integerAdd false 1
let add_vec_range_signed = arith_op_vec_range integerAdd true 1
@@ -185,7 +179,7 @@ let mult_vec_range = arith_op_vec_range integerMult false 2
let mult_vec_range_signed = arith_op_vec_range integerMult true 2
let arith_op_range_vec op sign size (l,r) =
- arith_op_vec op sign size (to_vec (length r) l, r)
+ arith_op_vec op sign size (to_vec (length r, l), r)
let add_range_vec = arith_op_range_vec integerAdd false 1
let add_range_vec_signed = arith_op_range_vec integerAdd true 1
@@ -215,7 +209,7 @@ let add_vec_vec_range_signed = arith_op_vec_vec_range integerAdd true
let arith_op_vec_bit op sign (size : nat) (l,r) =
let l' = to_num sign l in
let n = op l' match r with | B1 -> (1 : integer) | _ -> 0 end in
- to_vec (length l * size) n
+ to_vec (length l * size,n)
let add_vec_bit = arith_op_vec_bit integerAdd false 1
let add_vec_bit_signed = arith_op_vec_bit integerAdd true 1
@@ -228,8 +222,8 @@ let rec arith_op_overflow_vec (op : integer -> integer -> integer) sign size (l,
let (l_unsign,r_unsign) = (to_num false l,to_num false r) in
let n = op l_sign r_sign in
let n_unsign = op l_unsign r_unsign in
- let correct_size_num = to_vec act_size n in
- let one_more_size_u = to_vec (act_size + 1) n_unsign in
+ let correct_size_num = to_vec (act_size,n) in
+ let one_more_size_u = to_vec (act_size + 1,n_unsign) in
let overflow =
if n <= get_max_representable_in sign len &&
n >= get_min_representable_in sign len
@@ -253,8 +247,8 @@ let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (siz
| B0 -> (l',l_u,false)
end in
(* | _ -> assert false *)
- let correct_size_num = to_vec act_size n in
- let one_larger = to_vec (act_size + 1) nu in
+ let correct_size_num = to_vec (act_size,n) in
+ let one_larger = to_vec (act_size + 1,nu) in
let overflow =
if changed
then
@@ -308,7 +302,7 @@ let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size (((Vecto
| _ -> (false,0)
end in
if representable
- then to_vec act_size n'
+ then to_vec (act_size,n')
else Vector (List.replicate act_size BU) start
let mod_vec = arith_op_vec_no0 integerMod false 1
@@ -331,7 +325,7 @@ let arith_op_overflow_no0_vec op sign size (((Vector _ start) as l),r) =
end in
let (correct_size_num,one_more) =
if representable then
- (to_vec act_size n',to_vec (act_size + 1) n_u')
+ (to_vec (act_size,n'),to_vec (act_size + 1,n_u'))
else
(Vector (List.replicate act_size BU) start,
Vector (List.replicate (act_size + 1) BU) start) in
@@ -342,7 +336,7 @@ let quot_overflow_vec = arith_op_overflow_no0_vec integerDiv false 1
let quot_overflow_vec_signed = arith_op_overflow_no0_vec integerDiv true 1
let arith_op_vec_range_no0 op sign size (l,r) =
- arith_op_vec_no0 op sign size (l,to_vec (length l) r)
+ arith_op_vec_no0 op sign size (l,to_vec (length l,r))
let mod_vec_range = arith_op_vec_range_no0 integerMod false 1
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index ce3be419..f9404416 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -1,12 +1,12 @@
open import Pervasives
-type M 's 'a = <| runState : 's -> ('a * 's) |>
+type M 's 'a = 's -> ('a * 's)
val return : forall 's 'a. 'a -> M 's 'a
-let return a = <| runState = (fun s -> (a,s)) |>
+let return a = fun s -> (a,s)
val bind : forall 's 'a 'b. M 's 'a -> ('a -> M 's 'b) -> M 's 'b
-let bind m f = <| runState = (fun s -> let (a,s) = m.runState s in (f a).runState s) |>
+let bind m f s = let (a,s') = m s in f a s'
let (>>=) = bind
let (>>) m n = m >>= fun _ -> n
diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem
index 75628f45..d5f47492 100644
--- a/src/gen_lib/vector.lem
+++ b/src/gen_lib/vector.lem
@@ -1,8 +1,15 @@
open import Pervasives
type bit = B0 | B1 | BU
-type vector = Vector of list bit * nat
+type vector 'a = Vector of list 'a * nat
+let rec nth xs (n : nat) = match (n,xs) with
+ | (0,x :: xs) -> x
+ | (n + 1,x :: xs) -> nth xs n
+end
+
+let vector_access is_inc (Vector bs start) n =
+ if is_inc then nth bs (n - start) else nth bs (start - n)
let read_vector_subrange is_inc (Vector bs start) n m =
let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
@@ -16,4 +23,7 @@ let write_vector_subrange is_inc (Vector bs start) n m (Vector bs' _) =
let (_,suffix) = List.splitAt (offset + length) bs in
Vector (prefix ++ (List.take length bs') ++ suffix) start
+let write_vector_bit is_inc v n (Vector [b] 0) =
+ write_vector_subrange is_inc v n n b
+
let hd (x :: xs) = x
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 07f931de..5e42d2bb 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -1920,13 +1920,13 @@ let doc_pat_lem =
parens
(separate space [string "Vector";
(separate space [brackets (separate_map semi pat pats);
- underscore;underscore])]) in
+ underscore])]) in
(match annot with
| Base(([],t),_,_,_,_,_) ->
if is_bit_vector t
then parens (separate space [string "Vector";
(separate space [brackets (separate_map semi pat pats);
- underscore;underscore])])
+ underscore])])
else non_bit_print()
| _ -> non_bit_print ())
| P_tup pats -> parens (separate_map comma_sp pat pats)
@@ -1965,13 +1965,27 @@ let doc_exp_lem, doc_let_lem =
| E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) -> failwith "shouldn't happen"
| E_let(leb,e) -> (let_exp leb) ^^ space ^^ string "in" ^/^ (exp e)
| E_app(f,args) ->
- let call = match annot with
- | Base(_,External (Some n),_,_,_,_) -> string n
- | Base(_,Constructor _,_,_,_,_) -> doc_id_lem_ctor f
- | _ -> doc_id_lem f in
- parens (doc_unop call (parens (separate_map comma exp args)))
+ (match f with
+ (* temporary hack to make the loop body a function of the temporary variables *)
+ | Id_aux ((Id (("foreach_inc" | "foreach_dec") as loopf),_)) ->
+ let call = doc_id_lem in
+ let [indices;body;E_aux (E_tuple vars,_) as e5] = args in
+ let vars = List.map (fun (E_aux (E_id (Id_aux (Id name,_)),_)) -> string name) vars in
+ separate space [string loopf;exp indices;
+ parens((separate space)
+ [string "fun";parens (separate comma vars);arrow] ^/^
+ exp body
+ );
+ exp e5]
+ | _ ->
+ let call = match annot with
+ | Base(_,External (Some n),_,_,_,_) -> string n
+ | Base(_,Constructor _,_,_,_,_) -> doc_id_lem_ctor f
+ | _ -> doc_id_lem f in
+ parens (doc_unop call (parens (separate_map comma exp args)))
+ )
| E_vector_access(v,e) ->
- let call = (match annot with
+ let call = (match annot with
| Base((_,t),_,_,_,_,_) ->
(match t.t with
| Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> (string "bit_vector_access")
@@ -1987,8 +2001,8 @@ let doc_exp_lem, doc_let_lem =
let field_f = match annot with
| Base((_,{t = Tid "bit"}),_,_,_,_,_) |
Base((_,{t = Tabbrev(_,{t=Tid "bit"})}),_,_,_,_,_) ->
- string "get_register_field_bit"
- | _ -> string "get_register_field_vec" in
+ string "read_register_field_bit"
+ | _ -> string "read_register_field" in
parens (field_f ^^ space ^^ (exp fexp) ^^ space ^^ string_lit (doc_id id))
| _ -> exp fexp ^^ dot ^^ doc_id id)
| E_block [] -> string "()"
@@ -2007,12 +2021,19 @@ let doc_exp_lem, doc_let_lem =
| Base((_,t),Alias alias_info,_,_,_,_) ->
(match alias_info with
| Alias_field(reg,field) ->
- (match t.t with
- | Tid "bit"
- | Tabbrev(_,{t=Tid "bit"}) ->
- parens (string "hd" ^^ space ^^
- parens (separate space [string "read_register"; string reg]))
- | _ -> string "read_register" ^^ space ^^ string reg)
+ let field_f = match t.t with
+ | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> string "read_register_field_bit"
+ | _ -> string "read_register_field" in
+ parens (separate space [field_f; string reg; string_lit (string field)])
+ | Alias_extract(reg,start,stop) ->
+ if start = stop
+ then parens (separate space [string "vector_access";string reg;doc_int start])
+ else parens
+ (separate space [string "vector_subrange"; string reg; doc_int start; doc_int stop])
+ | Alias_pair(reg1,reg2) ->
+ parens (separate space [string "vector_concat";
+ string reg1;
+ string reg2])
| Alias_extract(reg,start,stop) ->
if start = stop
then
@@ -2034,7 +2055,7 @@ let doc_exp_lem, doc_let_lem =
| E_cast(typ,e) ->
(match annot with
| Base(_,External _,_,_,_,_) -> parens( string "read_register" ^^ space ^^ exp e)
- | _ -> (parens (doc_op colon (group (exp e)) (doc_typ_lem typ))))
+ | _ -> exp e) (*(parens (doc_op colon (group (exp e)) (doc_typ_lem typ)))) *)
| E_tuple exps ->
parens (separate_map comma exp exps)
| E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
@@ -2055,8 +2076,7 @@ let doc_exp_lem, doc_let_lem =
| N2n(_,Some i) -> string_of_big_int i
| _ -> if dir then "0" else string_of_int (List.length exps) in
parens (separate space [string "Vector"; brackets (separate_map semi exp exps);
- string start;
- string dir_out]))
+ string start]))
| E_vector_indexed (iexps, (Def_val_aux (default,_))) ->
(match annot with
| Base((_,t),_,_,_,_,_) ->
@@ -2187,45 +2207,45 @@ let doc_exp_lem, doc_let_lem =
| E_aux(_,(_,Base((_,t),_,_,_,_,_))) ->
(match t.t with
| Tapp("vector", [_;_;_;(TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})}))]) |
- Tabbrev(_,{t=Tapp("vector",[_;_;_;TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})})])}) |
- Tapp("reg",[TA_typ {t = Tapp("vector", [_;_;_;(TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})}))])}])
+ Tabbrev(_,{t=Tapp("vector",[_;_;_;TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})})])}) |
+ Tapp("reg", [TA_typ {t= Tapp("vector", [_;_;_;(TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})}))])}])
->
- (false,true)
+ (false,true)
| Tid "bit" | Tabbrev(_,{t=Tid "bit"}) | Tapp("reg",[TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})})])
-> (true,false)
| _ -> (false,false))
| _ -> (false,false) in
match lexp with
| LEXP_vector(v,e) ->
- doc_op (string "write_register")
- (group (parens (string "get_elements" ^^ space ^^ doc_lexp_lem false v)) ^^
- dot ^^ parens (exp e))
+ doc_op (string "<-")
+ (group (parens ((string "get_elements") ^^ space ^^ doc_lexp_lem false v)) ^^
+ dot ^^ parens (exp e))
(exp e_new_v)
| LEXP_vector_range(v,e1,e2) ->
- parens (string "write_register_subrange" ^^ space ^^
- doc_lexp_lem false v ^^ space ^^ exp e1 ^^ space ^^ exp e2 ^^ space ^^ exp e_new_v)
+ parens ((string "write_vector_subrange") ^^ space ^^
+ doc_lexp_lem false v ^^ space ^^ exp e1 ^^ space ^^ exp e2 ^^ space ^^ exp e_new_v)
| LEXP_field(v,id) ->
- parens (string "write_register" ^^ space ^^
- doc_lexp_lem false v ^^ space ^^ string_lit (doc_id id) ^^ space ^^ exp e_new_v)
+ parens ((string (if is_bit then "read_register_field_bit" else "read_register_field")) ^^ space ^^
+ doc_lexp_lem false v ^^ space ^^string_lit (doc_id id) ^^ space ^^ exp e_new_v)
| LEXP_id id | LEXP_cast (_,id) ->
(match annot with
| Base(_,Alias alias_info,_,_,_,_) ->
(match alias_info with
| Alias_field(reg,field) ->
- parens (string "write_register" ^^ space ^^
- string reg ^^ space ^^ string_lit (string field) ^^ space ^^ exp e_new_v)
+ parens ((if is_bit then string "write_register_field_bit" else string "write_register_field_v") ^^ space ^^
+ string (String.uncapitalize reg) ^^ space ^^string_lit (string field) ^^ space ^^ exp e_new_v)
| Alias_extract(reg,start,stop) ->
if start = stop
then
- doc_op (string "write_register")
- (group (parens (string "get_elements" ^^ space ^^ string reg)) ^^
+ doc_op (string "<-")
+ (group (parens ((string "get_elements") ^^ space ^^ string reg)) ^^
dot ^^ parens (doc_int start))
(exp e_new_v)
else
- parens (string "write_vector_subrange" ^^ space ^^
+ parens ((string "write_vector_subrange") ^^ space ^^
string reg ^^ space ^^ doc_int start ^^ space ^^ doc_int stop ^^ space ^^ exp e_new_v)
| Alias_pair(reg1,reg2) ->
- parens ((string "write_two_regs") ^^ space ^^ string reg1 ^^ space ^^ string reg2 ^^ space ^^ exp e_new_v))
+ parens ((string "write_two_regs") ^^ space ^^ string reg1 ^^ space ^^ string reg2 ^^ space ^^ exp e_new_v))
| _ ->
parens (separate space [string "write_register"; doc_id_lem id; exp e_new_v]))
@@ -2318,178 +2338,288 @@ let doc_def_lem def = match def with
| DEF_reg_dec dec -> empty (*group (doc_dec_lem dec) ^/^ hardline *)
| DEF_scattered sdef -> empty (*shoulnd't still be here*)
-
-
let reg_decls (Defs defs) =
+ let is_inc = match Spec_analysis.default_order (Defs defs) with
+ | {order = Oinc} -> true
+ | {order = Odec} -> false
+ | {order = _} -> failwith "Can't deal with variable order" in
+
let dirpp =
- let b = match Spec_analysis.default_order (Defs defs) with
- | {order = Oinc} -> "true"
- | {order = Odec} -> "false"
- | {order = _} -> failwith "Can't deal with variable order" in
- separate space [string "let";string "is_inc";equals;string "true"] in
+ let is_inc = if is_inc then "true" else "false" in
+ separate space [string "let";string "is_inc";equals;string is_inc] in
- let (regtyps,typedregs,simpleregs,defs) =
+ let (regtypes,defs) =
List.fold_left
- (fun (regtyps,typedregs,simpleregs,defs) def ->
- match def with
- | DEF_type (TD_aux(TD_register (Id_aux (Id name, _),n1,n2,rs),_)) ->
- (regtyps @ [(name,(n1,n2,rs))],typedregs,simpleregs,defs)
- | DEF_reg_dec (DEC_aux (DEC_reg(Typ_aux (Typ_id (Id_aux (Id typ,_)),_),Id_aux (Id name,_)),_)) ->
- (regtyps,typedregs @ [(name,typ)],simpleregs,defs)
- | DEF_reg_dec (DEC_aux (DEC_reg(_, Id_aux (Id name,_)),_)) ->
- (regtyps,typedregs,simpleregs @ [name],defs)
- | def -> (regtyps,typedregs,simpleregs,defs @ [def])
- ) ([],[],[],[]) defs in
+ (fun (regtypes,defs) def ->
+ match def with
+ | DEF_type (TD_aux(TD_register (Id_aux (Id name, _),n1,n2,rs),_)) ->
+ let (rsbits,rsranges) =
+ List.fold_left
+ (fun (rsbits,rsranges) field ->
+ match field with
+ | (BF_aux (BF_range (i,j), _), Id_aux (Id name,_)) ->
+ (rsbits,rsranges @ [(name,i,j)])
+ | (BF_aux (BF_single i, _), Id_aux (Id name, _)) ->
+ (rsbits @ [(name,i)],rsranges)
+ ) ([],[]) rs in
+ (regtypes @ [(name,(n1,n2,rsranges,rsbits))],defs)
+ | _ -> (regtypes,defs @ [def])
+ ) ([],[]) defs in
+
+ let ((simpleregs : string list),(typedregs : ((string * string) list)),defs) =
+ List.fold_left
+ (fun (simpleregs,typedregs,defs) def ->
+ match def with
+ | DEF_reg_dec (DEC_aux (DEC_reg(Typ_aux (Typ_id (Id_aux (Id typ,_)),_),Id_aux (Id name,_)),_)) ->
+ (simpleregs,typedregs @ [(name,typ)],defs)
+ | DEF_reg_dec (DEC_aux (DEC_reg(_, Id_aux (Id name,_)),_)) ->
+ (simpleregs @ [name],typedregs,defs)
+ | def -> (simpleregs,typedregs,defs @ [def])
+ ) ([],[],[]) defs in
- let default name = (name,
- Nexp_aux (Nexp_constant 0,Unknown),
- Nexp_aux (Nexp_constant 63,Unknown),
- name) in
-
- let reg_decls =
- (List.map default simpleregs) @
- List.fold_left
- (fun acc (id,typ) ->
- let (n1,n2,rs) = List.assoc typ regtyps in
- let rs_decls =
- List.map
- (function
- | (BF_aux (BF_range (i,j), _), Id_aux (Id name,_)) ->
- (name, Nexp_aux (Nexp_constant i,Unknown), Nexp_aux (Nexp_constant j, Unknown),id)
- | (BF_aux (BF_single i, _), Id_aux (Id name, _)) ->
- (name, Nexp_aux (Nexp_constant i,Unknown), Nexp_aux (Nexp_constant i, Unknown),id)
- ) rs in
- acc @ ((id,n1,n2,id) :: rs_decls)
- ) [] typedregs in
-
- let proper_regs = (List.map snd typedregs) @ simpleregs in
- let regs_and_fields = List.map (fun (x,_,_,_) -> x) reg_decls in
- let regspp =
- prefix 2 1
- (separate space [string "type"; string "register";equals])
- (separate_map space (fun reg -> pipe ^^ space ^^ string reg) regs_and_fields) in
+ let typedregs_per_type : (string * (string list)) list =
+ List.map (fun (typ,_) ->
+ let regs = List.filter (fun (_,regtyp) -> regtyp = typ) typedregs in
+ (typ,List.map fst regs)) regtypes in
+
+
+ let regs_per_type : (string option * string list) list =
+ (None,simpleregs) ::
+ (List.map (fun (name,regs) -> (Some name,regs)) typedregs_per_type) in
+
+ let _ = List.map (fun (name,regs) ->
+ let name = match name with Some name -> name | None -> "register" in
+ print_endline (name ^ " " ^ String.concat " " regs)) regs_per_type in
+
+ (* maybe we need a function that analyses the spec for this as well *)
+ let default =
+ (Nexp_aux (Nexp_constant (if is_inc then 0 else 63),Unknown),
+ Nexp_aux (Nexp_constant (if is_inc then 63 else 0),Unknown),
+ [],[]) in
+ let regspp =
+ separate_map
+ (break 1)
+ (fun (typ,names) ->
+ let typ = match typ with Some typ -> "register_" ^ typ | None -> "register" in
+ (prefix 2 1)
+ (separate space [string "type"; string typ; equals])
+ (separate_map space (fun reg -> pipe ^^ space ^^ string reg) names)
+ ) regs_per_type in
+
+ let regfieldspp =
+ separate_map
+ (break 1)
+ (fun (typ,(_,_,rsranges,rsbits)) ->
+ (if rsranges = [] then empty else
+ (prefix 2 1)
+ (separate space [string "type"; string ("register_field_" ^ typ); equals])
+ (separate_map space (fun (name,_,_) -> pipe ^^ space ^^ string name) rsranges)
+ ) ^/^
+ (if rsranges = [] then empty else
+ (prefix 2 1)
+ (separate space [string "type"; string ("register_field_bit_" ^ typ); equals])
+ (separate_map space (fun (name,_) -> pipe ^^ space ^^ string name) rsbits)
+ )
+ )
+ regtypes in
+
let statepp =
- prefix 2 1
- (separate space [string "type";string "state";equals])
- (anglebars
- (separate_map
- (semi ^^ break 1)
- (fun reg -> separate space [string (String.lowercase reg);colon;string "vector"])
- proper_regs
- )) in
-
- let lengthpp =
- prefix 2 1
- (separate space [string "let";string "length_register";colon;string "register";
- arrow;string "nat";equals;string "function"])
- ((separate_map
- (break 1)
- (fun (id,n1,n2,_) ->
- separate
- space
- [pipe;string id;arrow;
- string "natFromInteger" ^^
- parens (
- separate
- space [
- string "abs";
- parens (separate
- space
- [doc_nexp n2;
- minus;
- doc_nexp n1]);
- plus;string "1"]
- )
- ])
- reg_decls
- ) ^^
- hardline ^^
- string "end") in
+ (prefix 2 1)
+ (separate space [string "type";string "state";equals])
+ (anglebars
+ ((separate_map (semi ^^ break 1))
+ (fun reg -> separate space [string (String.lowercase reg);colon;string "vector bit"])
+ (simpleregs @ List.map fst typedregs)
+ )) in
+
+ let length_pp =
+ (separate_map (break 1))
+ (fun (typ,regs) ->
+ let ((n1,n2,_,_),typname) =
+ match typ with
+ | Some typname -> (List.assoc typname regtypes,"register_" ^ typname)
+ | None -> (default,"register") in
+ ((separate space)
+ [string "let";string ("length_" ^ typname);underscore;equals;
+ string "natFromInteger";
+ parens (
+ (separate space)
+ [string "abs";parens (separate space [doc_nexp n2;minus;doc_nexp n1]);
+ plus;string "1"]
+ )])
+ ) regs_per_type in
let read_register_pp =
- prefix
- 2 1
- (separate space [string "let";string "read_register";string "reg";equals])
- (enclose
- (langlebar ^^ space) (ranglebar)
- (prefix
- 2 1
- (separate space [string "runState";equals])
- (prefix 2 1
- ((separate space [string "fun"; string "s";arrow]) ^^ hardline ^^
- (separate space [string "let";string "v";equals;string "match reg with"]))
- ((separate_map
- (break 1)
- (fun (id,n1,n2,id2) ->
- separate
- space
- [pipe;
- string id;
- arrow;
- string "read_vector_subrange";
- string "is_inc";
- string "s." ^^ (string (String.lowercase id2));
- doc_nexp n1;
- doc_nexp n2])
- reg_decls
- ) ^^
- hardline ^^
- string "end in")
- ) ^^ hardline ^^
- string "(v,s)" ^^ hardline
- )
- )
+ separate_map
+ (break 1)
+ (fun (typ,regs) ->
+ let typ = match typ with Some typ -> "register_" ^ typ | None -> "register" in
+ (prefix 2 1)
+ (separate space [string "let";string ("read_" ^ typ);string "reg";string "s";equals])
+ ((prefix 2 1)
+ ((separate space) [string "let";string "v";equals])
+ (string "match reg with" ^/^
+ ((separate_map (break 1))
+ (fun name ->
+ separate space [pipe;string name;arrow;
+ string "s." ^^ (string (String.lowercase name))])
+ regs) ^/^
+ string "end in" )
+ ^^ hardline ^^ string "(v,s)" ^^ hardline)
+ ) regs_per_type
in
let write_register_pp =
- prefix
- 2 1
- (separate space [string "let";string "write_register";string "reg";string "v";equals])
- (enclose
- (langlebar ^^ space) (ranglebar)
- (prefix
- 2 1
- (separate space [string "runState";equals])
- (prefix 2 1
- ((separate space [string "fun"; string "s";arrow]) ^^ hardline ^^
- (separate space [string "let";string "s'";equals;string "match reg with"]))
- ((separate_map
- (break 1)
- (fun (id,n1,n2,id2) ->
- separate
- space
- [pipe;string id;arrow;
- (
- enclose
- (langlebar ^^ space) (space ^^ ranglebar)
- (separate
- space
- [string "s with";
- string (String.lowercase id2);
- equals;
- string "write_vector_subrange";
- string "is_inc";
- string "s." ^^ string (String.lowercase id2);
- doc_nexp n1;
- doc_nexp n2;
- string "v"])
- )
- ]
- )
- reg_decls
- ) ^^
- hardline ^^
- string "end in")
- ) ^^ hardline ^^
- string "((),s')" ^^ hardline
- )
- )
+ separate_map
+ (break 1)
+ (fun (typ,regs) ->
+ let typ = match typ with Some typ -> "register_" ^ typ | None -> "register" in
+ (prefix 2 1)
+ (separate space [string "let";string ("write_" ^ typ);string "reg";string "v";string "s";equals])
+ (string "match reg with" ^/^
+ ((separate_map (break 1))
+ (fun name ->
+ separate
+ space
+ [pipe;string name;arrow;
+ parens (string "()" ^^ comma ^^
+ anglebars (
+ (separate space) [string "s";string"with";string (String.lowercase name);
+ equals;string "v"]
+ ))
+ ])
+ regs) ^/^
+ string "end" ^^ hardline )
+ ) regs_per_type
in
- (separate (hardline ^^ hardline) [dirpp;regspp;statepp;lengthpp;read_register_pp;write_register_pp],defs)
+ let read_register_field_pp =
+ separate_map
+ (break 1)
+ (fun (typ,(n1,n2,rsranges,rsbits)) ->
+ (if rsranges = [] then empty else
+ ((prefix 2 1)
+ ((separate space) [string "let";string ("read_register_field_" ^ typ);
+ string "reg";string "rfield";equals])
+ (string "match rfield with" ^/^
+ ((separate_map (break 1))
+ (fun (name,i,j) ->
+ (separate space)
+ [pipe;string name;arrow;
+ string ("read_register_" ^ typ ^ " reg");
+ string ">>=";string "fun v";arrow;
+ string "return";
+ parens (
+ (separate space)
+ [string "read_vector_subrange";
+ string "is_inc";
+ string "v";
+ string (string_of_int i);
+ string (string_of_int j)]
+ )
+ ];
+ )
+ rsranges) ^/^
+ string "end"
+ ) ^^ hardline
+ ) ^/^
+ hardline
+ ) ^^
+ (if rsbits = [] then empty else
+ (prefix 2 1)
+ ((separate space) [string "let";string ("read_register_field_bit_" ^ typ);
+ string "reg";string "rfield";equals])
+ (string "match rfield with" ^/^
+ ((separate_map (break 1))
+ (fun (name,i) ->
+ (separate space)
+ [pipe;string name;arrow;
+ string ("read_register_" ^ typ ^ " reg");
+ string ">>=";string "fun v";arrow;
+ string "return";
+ parens (
+ (separate space)
+ [string "vector_access";
+ string "is_inc";
+ string "v";
+ string (string_of_int i)]
+ )
+ ];
+ )
+ rsbits) ^/^
+ string "end"
+ ) ^^ hardline
+ )
+ ) regtypes
+ in
+
+ let write_register_field_pp =
+ separate_map
+ (break 1)
+ (fun (typ,(n1,n2,rsranges,rsbits)) ->
+ (if rsranges = [] then empty else
+ (prefix 2 1)
+ (separate space [string "let";string ("write_register_field_" ^ typ);string "reg";
+ string "rfield";string "v";string "s";equals])
+ (string "match (reg,rfield) with" ^/^
+ (separate_map (break 1))
+ (fun regname ->
+ ((separate_map (break 1))
+ (fun (fieldname,i,j) ->
+ (prefix 2 1)
+ (separate space [pipe;parens (string regname ^^ comma ^^ string fieldname);arrow])
+ (parens
+ (string "()" ^^ comma ^^
+ anglebars (
+ (separate space)
+ [string "s";string"with";string (String.lowercase regname);equals;
+ string "write_vector_subrange";string "is_inc";
+ string "s." ^^ string (String.lowercase regname);
+ string (string_of_int i); string (string_of_int j);string "v"]
+ )
+ )
+ )
+ ) rsranges
+ )
+ ) (List.assoc typ typedregs_per_type) ^/^
+ string "end" ^^ hardline
+ ) ^/^ hardline) ^^
+ (if rsbits = [] then empty else
+ (prefix 2 1)
+ (separate space [string "let";string ("write_register_field_bit_" ^ typ);string "reg";
+ string "rfield";string "v";string "s";equals])
+ (string "match (reg,rfield) with" ^/^
+ (separate_map (break 1))
+ (fun regname ->
+ ((separate_map (break 1))
+ (fun (fieldname,i) ->
+ (prefix 2 1)
+ (separate space [pipe;parens (string regname ^^ comma ^^ string fieldname);arrow])
+ (parens
+ (string "()" ^^ comma ^^
+ anglebars (
+ (separate space)
+ [string "s";string"with";string (String.lowercase regname);equals;
+ string "write_vector_bit";string "is_inc";
+ string "s." ^^ string (String.lowercase regname);
+ string (string_of_int i);string "v"]
+ )
+ )
+ )
+ ) rsbits
+ )
+ ) (List.assoc typ typedregs_per_type) ^/^
+ string "end" ^^ hardline
+ ) ^^ hardline)
+ ) regtypes
+ in
+
+ (separate (hardline ^^ hardline)
+ [dirpp;regspp;regfieldspp;statepp;length_pp;read_register_pp;write_register_pp;
+ read_register_field_pp;write_register_field_pp],defs)
let doc_defs_lem (Defs defs) =
@@ -2501,12 +2631,11 @@ let pp_defs_lem f_arch f d top_line opens =
let (decls,defs) = doc_defs_lem d in
print f
(string "(*" ^^ (string top_line) ^^ string "*)" ^/^
- (separate_map
- hardline
+ ((separate_map hardline)
(fun lib -> separate space [string "open import";string lib])
("Vector" :: "State" :: "Arch" :: opens)) ^/^ defs);
print f_arch
(string "(*" ^^ (string top_line) ^^ string "*)" ^/^
- (separate_map
- hardline
- (fun lib -> separate space [string "open import";string lib]) ["Pervasives";"State";"Vector"]) ^/^ decls)
+ ((separate_map hardline)
+ (fun lib -> separate space [string "open import";string lib])
+ ["Pervasives";"State";"Vector"]) ^/^ decls)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 08:38:26 +0000