From e9badcc77afe07e95a1ace1598d50875e5331893 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Tue, 15 Aug 2017 14:25:28 +0100 Subject: Improve and simplify handling of mutable local variables --- src/gen_lib/state.lem | 2 +- src/pretty_print_lem.ml | 3 +- src/rewriter.ml | 186 ++++++++++++++++++------------------------------ 3 files changed, 72 insertions(+), 119 deletions(-) (limited to 'src') diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index 2e11e8a9..140258d8 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -52,7 +52,7 @@ let exit _ s = [(Right (), s)] val early_return : forall 'r. 'r -> MR unit 'r let early_return r s = [(Right (Just r), s)] -val catch_early_return : forall 'a 'r. MR 'a 'a -> M 'a +val catch_early_return : forall 'a. MR 'a 'a -> M 'a let catch_early_return m s = List.map (function diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 586773ca..1b6c67c5 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -670,7 +670,8 @@ let doc_exp_lem, doc_let_lem = (doc_fexp regtypes early_ret recordtyp) fexps)) ^^ space) in if aexp_needed then parens epp else epp | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) -> - let recordtyp = match annot with + let (E_aux (_, (_, eannot))) = e in + let recordtyp = match eannot with | Some (env, Typ_aux (Typ_id tid,_), _) when Env.is_record tid env -> tid | _ -> raise (report l "cannot get record type") in diff --git a/src/rewriter.ml b/src/rewriter.ml index 8da8aacf..9e170d0a 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -2057,6 +2057,42 @@ let rewrite_exp_guarded_pats rewriters (E_aux (exp,(l,annot)) as full_exp) = let rewrite_defs_guarded_pats = rewrite_defs_base { rewriters_base with rewrite_exp = rewrite_exp_guarded_pats } + +let id_is_local_var id env = match Env.lookup_id id env with + | Local _ | Unbound -> true + | _ -> false + +let rec lexp_is_local (LEXP_aux (lexp, _)) env = match lexp with + | LEXP_memory _ -> false + | LEXP_id id + | LEXP_cast (_, id) -> id_is_local_var id env + | LEXP_tup lexps -> List.for_all (fun lexp -> lexp_is_local lexp env) lexps + | LEXP_vector (lexp,_) + | LEXP_vector_range (lexp,_,_) + | LEXP_field (lexp,_) -> lexp_is_local lexp env + +let lexp_is_effectful (LEXP_aux (_, (_, annot))) = match annot with + | Some (_, _, eff) -> effectful_effs eff + | _ -> false + +let rec rewrite_local_lexp ((LEXP_aux(lexp,((l,_) as annot))) as le) = match lexp with + | LEXP_id id | LEXP_cast (_, id) -> + (le, E_aux (E_id id, annot), (fun exp -> exp)) + | LEXP_vector (lexp, e) -> + let (lexp, access, rexp) = rewrite_local_lexp lexp in + (lexp, E_aux (E_vector_access (access, e), annot), + (fun exp -> rexp (E_aux (E_vector_update (access, e, exp), annot)))) + | LEXP_vector_range (lexp, e1, e2) -> + let (lexp, access, rexp) = rewrite_local_lexp lexp in + (lexp, E_aux (E_vector_subrange (access, e1, e2), annot), + (fun exp -> rexp (E_aux (E_vector_update_subrange (access, e1, e2, exp), annot)))) + | LEXP_field (lexp, id) -> + let (lexp, access, rexp) = rewrite_local_lexp lexp in + let field_update exp = FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), annot)], false), annot) in + (lexp, E_aux (E_field (access, id), annot), + (fun exp -> rexp (E_aux (E_record_update (access, field_update exp), annot)))) + | _ -> raise (Reporting_basic.err_unreachable l "unsupported lexp") + (*Expects to be called after rewrite_defs; thus the following should not appear: internal_exp of any form lit vectors in patterns or expressions @@ -2071,17 +2107,14 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f | E_block exps -> let rec walker exps = match exps with | [] -> [] - | (E_aux(E_assign((LEXP_aux ((LEXP_id id | LEXP_cast (_,id)),_)) as le,e), - ((l, Some (env,typ,eff)) as annot)) as exp)::exps -> - (match Env.lookup_id id env with - | Unbound | Local _ -> - let le' = rewriters.rewrite_lexp rewriters le in - let e' = rewrite_base e in - let exps' = walker exps in - let effects = union_eff_exps exps' in - let block = E_aux (E_block exps', (l, Some (env, unit_typ, effects))) in - [fix_eff_exp (E_aux (E_internal_let(le', e', block), annot))] - | _ -> (rewrite_rec exp)::(walker exps)) + | (E_aux(E_assign(le,e), ((l, Some (env,typ,eff)) as annot)) as exp)::exps + when lexp_is_local le env && not (lexp_is_effectful le)-> + let (le', _, re') = rewrite_local_lexp le in + let e' = re' (rewrite_base e) in + let exps' = walker exps in + let effects = union_eff_exps exps' in + let block = E_aux (E_block exps', (l, Some (env, unit_typ, effects))) in + [fix_eff_exp (E_aux (E_internal_let(le', e', block), annot))] (*| ((E_aux(E_if(c,t,e),(l,annot))) as exp)::exps -> let vars_t = introduced_variables t in let vars_e = introduced_variables e in @@ -2127,20 +2160,12 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f | e::exps -> (rewrite_rec e)::(walker exps) in rewrap (E_block (walker exps)) - | E_assign(((LEXP_aux ((LEXP_id id | LEXP_cast (_,id)),lannot)) as le),e) -> - let le' = rewriters.rewrite_lexp rewriters le in - let e' = rewrite_base e in - let effects = effect_of e' in - (match Env.lookup_id id (env_of_annot annot) with - | Unbound -> - rewrap_effects - (E_internal_let(le', e', E_aux(E_block [], simple_annot l unit_typ))) - effects - | Local _ -> - let effects' = union_effects effects (effect_of_annot (snd lannot)) in - let annot' = Some (env_of_annot annot, unit_typ, effects') in - E_aux((E_assign(le', e')),(l, annot')) - | _ -> rewrite_base full_exp) + | E_assign(le,e) + when lexp_is_local le (env_of full_exp) && not (lexp_is_effectful le) -> + let (le', _, re') = rewrite_local_lexp le in + let e' = re' (rewrite_base e) in + let block = E_aux (E_block [], simple_annot l unit_typ) in + fix_eff_exp (E_aux (E_internal_let(le', e', block), annot)) | _ -> rewrite_base full_exp let rewrite_lexp_lift_assign_intro rewriters ((LEXP_aux(lexp,annot)) as le) = @@ -2607,13 +2632,15 @@ let rewrite_defs_effectful_let_expressions = else E_let (lb,body) in let e_internal_let = fun (lexp,exp1,exp2) -> - if effectful exp1 then - match lexp with - | LEXP_aux (LEXP_id id,annot) - | LEXP_aux (LEXP_cast (_,id),annot) -> + match lexp with + | LEXP_aux (LEXP_id id,annot) + | LEXP_aux (LEXP_cast (_,id),annot) -> + if effectful exp1 then E_internal_plet (P_aux (P_id id,annot),exp1,exp2) - | _ -> failwith "E_internal_plet with unexpected lexp" - else E_internal_let (lexp,exp1,exp2) in + else + let lb = LB_aux (LB_val_implicit (P_aux (P_id id,annot), exp1), annot) in + E_let (lb, exp2) + | _ -> failwith "E_internal_let with unexpected lexp" in let alg = { id_exp_alg with e_let = e_let; e_internal_let = e_internal_let } in rewrite_defs_base @@ -2639,92 +2666,17 @@ let eqidtyp (id1,_) (id2,_) = let name2 = match id2 with Id_aux ((Id name | DeIid name),_) -> name in name1 = name2 -let find_updated_vars (E_aux (_,(l,_)) as exp) = - let ( @@ ) (a,b) (a',b') = (a @ a',b @ b') in - let lapp2 (l : (('a list * 'b list) list)) : ('a list * 'b list) = - List.fold_left - (fun ((intros_acc : 'a list),(updates_acc : 'b list)) (intros,updates) -> - (intros_acc @ intros, updates_acc @ updates)) ([],[]) l in - - let (intros,updates) = - fold_exp - { e_aux = (fun (e,_) -> e) - ; e_id = (fun _ -> ([],[])) - ; e_lit = (fun _ -> ([],[])) - ; e_cast = (fun (_,e) -> e) - ; e_block = (fun es -> lapp2 es) - ; e_nondet = (fun es -> lapp2 es) - ; e_app = (fun (_,es) -> lapp2 es) - ; e_app_infix = (fun (e1,_,e2) -> e1 @@ e2) - ; e_tuple = (fun es -> lapp2 es) - ; e_if = (fun (e1,e2,e3) -> e1 @@ e2 @@ e3) - ; e_for = (fun (_,e1,e2,e3,_,e4) -> e1 @@ e2 @@ e3 @@ e4) - ; e_vector = (fun es -> lapp2 es) - ; e_vector_indexed = (fun (es,opt) -> opt @@ lapp2 (List.map snd es)) - ; e_vector_access = (fun (e1,e2) -> e1 @@ e2) - ; e_vector_subrange = (fun (e1,e2,e3) -> e1 @@ e2 @@ e3) - ; e_vector_update = (fun (e1,e2,e3) -> e1 @@ e2 @@ e3) - ; e_vector_update_subrange = (fun (e1,e2,e3,e4) -> e1 @@ e2 @@ e3 @@ e4) - ; e_vector_append = (fun (e1,e2) -> e1 @@ e2) - ; e_list = (fun es -> lapp2 es) - ; e_cons = (fun (e1,e2) -> e1 @@ e2) - ; e_record = (fun fexps -> fexps) - ; e_record_update = (fun (e1,fexp) -> e1 @@ fexp) - ; e_field = (fun (e1,id) -> e1) - ; e_case = (fun (e1,pexps) -> e1 @@ lapp2 pexps) - ; e_let = (fun (lb,e2) -> lb @@ e2) - ; e_assign = (fun ((ids,acc),e2) -> ([],ids) @@ acc @@ e2) - ; e_sizeof = (fun nexp -> ([],[])) - ; e_exit = (fun e1 -> ([],[])) - ; e_return = (fun e1 -> e1) - ; e_assert = (fun (e1,e2) -> ([],[])) - ; e_internal_cast = (fun (_,e1) -> e1) - ; e_internal_exp = (fun _ -> ([],[])) - ; e_internal_exp_user = (fun _ -> ([],[])) - ; e_comment = (fun _ -> ([],[])) - ; e_comment_struc = (fun _ -> ([],[])) - ; e_internal_let = - (fun ((ids,acc),e2,e3) -> - let id = match ids with - | [] -> raise (Reporting_basic.err_unreachable l "E_internal_let found not introducing a variable") - | [id] -> id - | _ -> raise (Reporting_basic.err_unreachable l "E_internal_let found introducing more than one variable") in - let (xs,ys) = ([id],[]) @@ acc @@ e2 @@ e3 in - let ys = List.filter (fun id2 -> not (eqidtyp id id2)) ys in - (xs,ys)) - ; e_internal_plet = (fun (_, e1, e2) -> e1 @@ e2) - ; e_internal_return = (fun e -> e) - ; lEXP_id = (fun id -> (Some id,[],([],[]))) - ; lEXP_memory = (fun (_,es) -> (None,[],lapp2 es)) - ; lEXP_cast = (fun (_,id) -> (Some id,[],([],[]))) - ; lEXP_tup = (fun tups -> failwith "FORCHRISTOPHER:: this needs implementing, not sure what you want to do") - ; lEXP_vector = (fun ((ids,acc),e1) -> (None,ids,acc @@ e1)) - ; lEXP_vector_range = (fun ((ids,acc),e1,e2) -> (None,ids,acc @@ e1 @@ e2)) - ; lEXP_field = (fun ((ids,acc),_) -> (None,ids,acc)) - ; lEXP_aux = - (function - | ((Some id,ids,acc),(annot)) -> - (match Env.lookup_id id (env_of_annot annot) with - | Unbound | Local _ -> ((id,annot) :: ids,acc) - | _ -> (ids,acc)) - | ((_,ids,acc),_) -> (ids,acc) - ) - ; fE_Fexp = (fun (_,e) -> e) - ; fE_aux = (fun (fexp,_) -> fexp) - ; fES_Fexps = (fun (fexps,_) -> lapp2 fexps) - ; fES_aux = (fun (fexp,_) -> fexp) - ; def_val_empty = ([],[]) - ; def_val_dec = (fun e -> e) - ; def_val_aux = (fun (defval,_) -> defval) - ; pat_exp = (fun (_,e) -> e) - ; pat_when = (fun (_,_,e) -> e) - ; pat_aux = (fun (pexp,_) -> pexp) - ; lB_val_explicit = (fun (_,_,e) -> e) - ; lB_val_implicit = (fun (_,e) -> e) - ; lB_aux = (fun (lb,_) -> lb) - ; pat_alg = id_pat_alg - } exp in - dedup eqidtyp updates +let find_updated_vars exp = + let lEXP_aux ((ids,lexp),annot) = + let ids = match lexp, annot with + | LEXP_id id, (_, Some (env, _, _)) -> + (match Env.lookup_id id env with + | Local (Mutable, _) -> (id, annot) :: ids + | _ -> ids) + | _ -> ids in + (ids, LEXP_aux (lexp, annot)) in + dedup eqidtyp (fst (fold_exp + { (compute_exp_alg [] (@)) with lEXP_aux = lEXP_aux } exp)) let swaptyp typ (l,tannot) = match tannot with | Some (env, typ', eff) -> (l, Some (env, typ, eff)) -- cgit v1.2.3 From d074a4eaad0f7164b44c3351660c5ee48381550d Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Thu, 17 Aug 2017 15:52:23 +0100 Subject: Add support for register types other than bitvector to state monad Make state monad parametric in register state, and generate a record with registers from the Sail spec --- src/gen_lib/sail_values.lem | 8 ++ src/gen_lib/state.lem | 129 +++++++++++++++------------- src/pretty_print.mli | 2 +- src/pretty_print_lem.ml | 203 ++++++++++++++++++++++++++++++++++++-------- src/process_file.ml | 63 ++++++-------- 5 files changed, 270 insertions(+), 135 deletions(-) (limited to 'src') diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index b4a15432..b5019df6 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -884,6 +884,14 @@ type register = | UndefinedRegister of integer (* length *) | RegisterPair of register * register +type register_ref 'regstate 'a = + <| read_from : 'regstate -> 'a; + write_to : 'regstate -> 'a -> 'regstate |> + +type field_ref 'regtype 'a = + <| get_field : 'regtype -> 'a; + set_field : 'regtype -> 'a -> 'regtype |> + let name_of_reg = function | Register name _ _ _ _ -> name | UndefinedRegister _ -> failwith "name_of_reg UndefinedRegister" diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index 140258d8..3cbcd4c8 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -6,53 +6,54 @@ open import Sail_values type memstate = map integer memory_byte type tagstate = map integer bitU -type regstate = map string (vector bitU) +(* type regstate = map string (vector bitU) *) -type sequential_state = <| regstate : regstate; - memstate : memstate; - tagstate : tagstate; - write_ea : maybe (write_kind * integer * integer); - last_exclusive_operation_was_load : bool|> +type sequential_state 'regs = + <| regstate : 'regs; + memstate : memstate; + tagstate : tagstate; + write_ea : maybe (write_kind * integer * integer); + last_exclusive_operation_was_load : bool|> (* State, nondeterminism and exception monad with result type 'a and exception type 'e. *) -type ME 'a 'e = sequential_state -> list ((either 'a 'e) * sequential_state) +type ME 'regs 'a 'e = sequential_state 'regs -> list ((either 'a 'e) * sequential_state 'regs) (* Most of the time, we don't distinguish between different types of exceptions *) -type M 'a = ME 'a unit +type M 'regs 'a = ME 'regs 'a unit (* For early return, we abuse exceptions by throwing and catching the return value. The exception type is "maybe 'r", where "Nothing" represents a proper exception and "Just r" an early return of value "r". *) -type MR 'a 'r = ME 'a (maybe 'r) +type MR 'regs 'a 'r = ME 'regs 'a (maybe 'r) -val liftR : forall 'a 'r. M 'a -> MR 'a 'r +val liftR : forall 'a 'r 'regs. M 'regs 'a -> MR 'regs 'a 'r let liftR m s = List.map (function | (Left a, s') -> (Left a, s') | (Right (), s') -> (Right Nothing, s') end) (m s) -val return : forall 'a 'e. 'a -> ME 'a 'e +val return : forall 'regs 'a 'e. 'a -> ME 'regs 'a 'e let return a s = [(Left a,s)] -val bind : forall 'a 'b 'e. ME 'a 'e -> ('a -> ME 'b 'e) -> ME 'b 'e -let bind m f (s : sequential_state) = +val bind : forall 'regs 'a 'b 'e. ME 'regs 'a 'e -> ('a -> ME 'regs 'b 'e) -> ME 'regs 'b 'e +let bind m f (s : sequential_state 'regs) = List.concatMap (function | (Left a, s') -> f a s' | (Right e, s') -> [(Right e, s')] end) (m s) let inline (>>=) = bind -val (>>): forall 'b 'e. ME unit 'e -> ME 'b 'e -> ME 'b 'e +val (>>): forall 'regs 'b 'e. ME 'regs unit 'e -> ME 'regs 'b 'e -> ME 'regs 'b 'e let inline (>>) m n = m >>= fun _ -> n -val exit : forall 'e 'a. 'e -> M 'a +val exit : forall 'regs 'e 'a. 'e -> M 'regs 'a let exit _ s = [(Right (), s)] -val early_return : forall 'r. 'r -> MR unit 'r +val early_return : forall 'regs 'r. 'r -> MR 'regs unit 'r let early_return r s = [(Right (Just r), s)] -val catch_early_return : forall 'a. MR 'a 'a -> M 'a +val catch_early_return : forall 'regs 'a 'r. MR 'regs 'a 'a -> M 'regs 'a let catch_early_return m s = List.map (function @@ -66,15 +67,15 @@ let rec range i j = if i = j then [i] else i :: range (i+1) j -val get_reg : sequential_state -> string -> vector bitU -let get_reg state reg = Map_extra.find reg state.regstate +val get_reg : forall 'regs 'a. sequential_state 'regs -> register_ref 'regs 'a -> 'a +let get_reg state reg = reg.read_from state.regstate -val set_reg : sequential_state -> string -> vector bitU -> sequential_state -let set_reg state reg bitv = - <| state with regstate = Map.insert reg bitv state.regstate |> +val set_reg : forall 'regs 'a. sequential_state 'regs -> register_ref 'regs 'a -> 'a -> sequential_state 'regs +let set_reg state reg v = + <| state with regstate = reg.write_to state.regstate v |> -val read_mem : forall 'a 'b. Size 'b => bool -> read_kind -> bitvector 'a -> integer -> M (bitvector 'b) +val read_mem : forall 'regs 'a 'b. Size 'b => bool -> read_kind -> bitvector 'a -> integer -> M 'regs (bitvector 'b) let read_mem dir read_kind addr sz state = let addr = unsigned addr in let addrs = range addr (addr+sz-1) in @@ -96,7 +97,7 @@ let read_mem dir read_kind addr sz state = (* caps are aligned at 32 bytes *) let cap_alignment = (32 : integer) -val read_tag : forall 'a. bool -> read_kind -> bitvector 'a -> M bitU +val read_tag : forall 'regs 'a. bool -> read_kind -> bitvector 'a -> M 'regs bitU let read_tag dir read_kind addr state = let addr = (unsigned addr) / cap_alignment in let tag = match (Map.lookup addr state.tagstate) with @@ -117,18 +118,18 @@ let read_tag dir read_kind addr state = then [(Left tag, <| state with last_exclusive_operation_was_load = true |>)] else [(Left tag, state)] -val excl_result : unit -> M bool +val excl_result : forall 'regs. unit -> M 'regs bool let excl_result () state = let success = (Left true, <| state with last_exclusive_operation_was_load = false |>) in (Left false, state) :: if state.last_exclusive_operation_was_load then [success] else [] -val write_mem_ea : forall 'a. write_kind -> bitvector 'a -> integer -> M unit +val write_mem_ea : forall 'regs 'a. write_kind -> bitvector 'a -> integer -> M 'regs unit let write_mem_ea write_kind addr sz state = let addr = unsigned addr in [(Left (), <| state with write_ea = Just (write_kind,addr,sz) |>)] -val write_mem_val : forall 'b. bitvector 'b -> M bool +val write_mem_val : forall 'regs 'b. bitvector 'b -> M 'regs bool let write_mem_val v state = let (write_kind,addr,sz) = match state.write_ea with | Nothing -> failwith "write ea has not been announced yet" @@ -140,7 +141,7 @@ let write_mem_val v state = state.memstate addresses_with_value in [(Left true, <| state with memstate = memstate |>)] -val write_tag : bitU -> M bool +val write_tag : forall 'regs. bitU -> M 'regs bool let write_tag t state = let (write_kind,addr,sz) = match state.write_ea with | Nothing -> failwith "write ea has not been announced yet" @@ -149,10 +150,10 @@ let write_tag t state = let tagstate = Map.insert taddr t state.tagstate in [(Left true, <| state with tagstate = tagstate |>)] -val read_reg : forall 'a. Size 'a => register -> M (bitvector 'a) +val read_reg : forall 'regs 'a. register_ref 'regs 'a -> M 'regs 'a let read_reg reg state = - let v = get_reg state (name_of_reg reg) in - [(Left (vec_to_bvec v),state)] + let v = reg.read_from state.regstate in + [(Left v,state)] (*let read_reg_range reg i j state = let v = slice (get_reg state (name_of_reg reg)) i j in [(Left (vec_to_bvec v),state)] @@ -168,41 +169,47 @@ let read_reg_bitfield reg regfield = let reg_deref = read_reg -val write_reg : forall 'a. Size 'a => register -> bitvector 'a -> M unit +val write_reg : forall 'regs 'a. register_ref 'regs 'a -> 'a -> M 'regs unit let write_reg reg v state = - [(Left (), set_reg state (name_of_reg reg) (bvec_to_vec v))] + [(Left (), <| state with regstate = reg.write_to state.regstate v |>)] +val update_reg : forall 'regs 'a 'b. register_ref 'regs 'a -> ('a -> 'b -> 'a) -> 'b -> M 'regs unit +let update_reg reg f v state = + let current_value = get_reg state reg in + let new_value = f current_value v in + [(Left (), set_reg state reg new_value)] let write_reg_range reg i j v state = - let current_value = get_reg state (name_of_reg reg) in - let new_value = update current_value i j (bvec_to_vec v) in - [(Left (), set_reg state (name_of_reg reg) new_value)] + let current_value = get_reg state reg in + let new_value = bvupdate current_value i j v in + [(Left (), set_reg state reg new_value)] let write_reg_bit reg i bit state = - let current_value = get_reg state (name_of_reg reg) in - let new_value = update_pos current_value i bit in - [(Left (), set_reg state (name_of_reg reg) new_value)] + let current_value = get_reg state reg in + let new_value = bvupdate_pos current_value i bit in + [(Left (), set_reg state reg new_value)] let write_reg_field reg regfield = - let (i,j) = register_field_indices reg regfield in - write_reg_range reg i j -let write_reg_bitfield reg regfield = - let (i,_) = register_field_indices reg regfield in - write_reg_bit reg i -let write_reg_field_range reg regfield i j v state = - let (i0,j0) = register_field_indices reg regfield in - let current_value = get_reg state (name_of_reg reg) in - let current_field_value = slice current_value i0 j0 in - let new_field_value = update current_field_value i j (bvec_to_vec v) in - let new_value = update current_value i j new_field_value in - [(Left (), set_reg state (name_of_reg reg) new_value)] - - -val barrier : barrier_kind -> M unit + update_reg reg regfield.set_field +let write_reg_field_range reg regfield i j = + let upd regval v = + let current_field_value = regfield.get_field regval in + let new_field_value = bvupdate current_field_value i j v in + regfield.set_field regval new_field_value in + update_reg reg upd +let write_reg_field_bit reg regfield i = + let upd regval v = + let current_field_value = regfield.get_field regval in + let new_field_value = bvupdate_pos current_field_value i v in + regfield.set_field regval new_field_value in + update_reg reg upd + + +val barrier : forall 'regs. barrier_kind -> M 'regs unit let barrier _ = return () -val footprint : M unit +val footprint : forall 'regs. M 'regs unit let footprint = return () -val foreachM_inc : forall 'vars 'e. (integer * integer * integer) -> 'vars -> - (integer -> 'vars -> ME 'vars 'e) -> ME 'vars 'e +val foreachM_inc : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e let rec foreachM_inc (i,stop,by) vars body = if i <= stop then @@ -211,8 +218,8 @@ let rec foreachM_inc (i,stop,by) vars body = else return vars -val foreachM_dec : forall 'vars 'e. (integer * integer * integer) -> 'vars -> - (integer -> 'vars -> ME 'vars 'e) -> ME 'vars 'e +val foreachM_dec : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e let rec foreachM_dec (i,stop,by) vars body = if i >= stop then @@ -220,7 +227,7 @@ let rec foreachM_dec (i,stop,by) vars body = foreachM_dec (i - by,stop,by) vars body else return vars -let write_two_regs r1 r2 bvec state = +(*let write_two_regs r1 r2 bvec state = let vec = bvec_to_vec bvec in let is_inc = let is_inc_r1 = is_inc_of_reg r1 in @@ -242,4 +249,4 @@ let write_two_regs r1 r2 bvec state = else slice vec (start_vec - size_r1) (start_vec - size_vec) in let state1 = set_reg state (name_of_reg r1) r1_v in let state2 = set_reg state1 (name_of_reg r2) r2_v in - [(Left (), state2)] + [(Left (), state2)]*) diff --git a/src/pretty_print.mli b/src/pretty_print.mli index 24816206..37de5241 100644 --- a/src/pretty_print.mli +++ b/src/pretty_print.mli @@ -52,4 +52,4 @@ val pat_to_string : 'a pat -> string val pp_lem_defs : Format.formatter -> tannot defs -> unit val pp_defs_ocaml : out_channel -> tannot defs -> string -> string list -> unit -val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit +val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 1b6c67c5..30d30f4a 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -140,6 +140,12 @@ let is_regtyp (Typ_aux (typ, _)) env = match typ with | Typ_id(id) when Env.is_regtyp id env -> true | _ -> false +let doc_nexp_lem (Nexp_aux (nexp, l) as full_nexp) = match nexp with + | Nexp_constant i -> string ("ty" ^ string_of_int i) + | Nexp_var v -> string (string_of_kid v) + | _ -> raise (Reporting_basic.err_unreachable l + ("cannot pretty-print non-atomic nexp \"" ^ string_of_nexp full_nexp ^ "\"")) + let doc_typ_lem, doc_atomic_typ_lem = (* following the structure of parser for precedence *) let rec typ regtypes ty = fn_typ regtypes true ty @@ -168,17 +174,19 @@ let doc_typ_lem, doc_atomic_typ_lem = Typ_arg_aux (Typ_arg_typ elem_typ, _)]) -> let tpp = match elem_typ with | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) -> - (match simplify_nexp m with + string "bitvector " ^^ doc_nexp_lem (simplify_nexp m) + (* (match simplify_nexp m with | (Nexp_aux(Nexp_constant i,_)) -> string "bitvector ty" ^^ doc_int i | (Nexp_aux(Nexp_var _, _)) -> separate space [string "bitvector"; doc_nexp m] | _ -> raise (Reporting_basic.err_unreachable l - "cannot pretty-print bitvector type with non-constant length")) + "cannot pretty-print bitvector type with non-constant length")) *) | _ -> string "vector" ^^ space ^^ typ regtypes elem_typ in if atyp_needed then parens tpp else tpp | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) -> (* TODO: Better distinguish register names and contents? *) (* fn_typ regtypes atyp_needed etyp *) - (string "register") + let tpp = (string "register_ref regstate " ^^ typ regtypes etyp) in + if atyp_needed then parens tpp else tpp | Typ_app(Id_aux (Id "range", _),_) -> (string "integer") | Typ_app(Id_aux (Id "implicit", _),_) -> @@ -206,7 +214,7 @@ let doc_typ_lem, doc_atomic_typ_lem = if atyp_needed then parens tpp else tpp and doc_typ_arg_lem regtypes (Typ_arg_aux(t,_)) = match t with | Typ_arg_typ t -> app_typ regtypes true t - | Typ_arg_nexp n -> empty + | Typ_arg_nexp n -> doc_nexp_lem (simplify_nexp n) | Typ_arg_order o -> empty | Typ_arg_effect e -> empty in typ', atomic_typ @@ -234,10 +242,10 @@ and contains_t_arg_pp_var (Typ_arg_aux (targ, _)) = match targ with | _ -> false let doc_tannot_lem regtypes eff typ = - if contains_t_pp_var typ then empty - else + (* if contains_t_pp_var typ then empty + else *) let ta = doc_typ_lem regtypes typ in - if eff then string " : M " ^^ parens ta + if eff then string " : _M " ^^ parens ta else string " : " ^^ ta (* doc_lit_lem gets as an additional parameter the type information from the @@ -346,6 +354,13 @@ let contains_early_return exp = { (Rewriter.compute_exp_alg false (||)) with e_return = (fun (_, r) -> (true, E_return r)) } exp) +let typ_id_of (Typ_aux (typ, l)) = match typ with + | Typ_id id -> id + | Typ_app (register, [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) + when string_of_id register = "register" -> id + | Typ_app (id, _) -> id + | _ -> raise (Reporting_basic.err_unreachable l "failed to get type id") + let prefix_recordtype = true let report = Reporting_basic.err_unreachable let doc_exp_lem, doc_let_lem = @@ -365,14 +380,18 @@ let doc_exp_lem, doc_let_lem = (match le_act (*, t, tag*) with | LEXP_vector_range (le,e2,e3) -> (match le with - | LEXP_aux (LEXP_field (le,id), lannot) -> - if is_bit_typ (typ_of_annot lannot) then + | LEXP_aux (LEXP_field ((LEXP_aux (_, lannot) as le),id), fannot) -> + if is_bit_typ (typ_of_annot fannot) then raise (report l "indexing a register's (single bit) bitfield not supported") else + let field_ref = + doc_id_lem (typ_id_of (typ_of_annot lannot)) ^^ + underscore ^^ + doc_id_lem id in liftR ((prefix 2 1) (string "write_reg_field_range") (align (doc_lexp_deref_lem regtypes early_ret le ^^ space^^ - string_lit (doc_id_lem id) ^/^ expY e2 ^/^ expY e3 ^/^ expY e))) + field_ref ^/^ expY e2 ^/^ expY e3 ^/^ expY e))) | _ -> liftR ((prefix 2 1) (string "write_reg_range") @@ -380,27 +399,35 @@ let doc_exp_lem, doc_let_lem = ) | LEXP_vector (le,e2) when is_bit_typ t -> (match le with - | LEXP_aux (LEXP_field (le,id), lannot) -> - if is_bit_typ (typ_of_annot lannot) then + | LEXP_aux (LEXP_field ((LEXP_aux (_, lannot) as le),id), fannot) -> + if is_bit_typ (typ_of_annot fannot) then raise (report l "indexing a register's (single bit) bitfield not supported") else + let field_ref = + doc_id_lem (typ_id_of (typ_of_annot lannot)) ^^ + underscore ^^ + doc_id_lem id in liftR ((prefix 2 1) (string "write_reg_field_bit") - (align (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ doc_id_lem id ^/^ expY e2 ^/^ expY e))) + (align (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ field_ref ^/^ expY e2 ^/^ expY e))) | _ -> liftR ((prefix 2 1) (string "write_reg_bit") (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ expY e2 ^/^ expY e)) ) - | LEXP_field (le,id) when is_bit_typ t -> + (* | LEXP_field (le,id) when is_bit_typ t -> liftR ((prefix 2 1) (string "write_reg_bitfield") - (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ string_lit(doc_id_lem id) ^/^ expY e)) - | LEXP_field (le,id) -> + (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ string_lit(doc_id_lem id) ^/^ expY e)) *) + | LEXP_field ((LEXP_aux (_, lannot) as le),id) -> + let field_ref = + doc_id_lem (typ_id_of (typ_of_annot lannot)) ^^ + underscore ^^ + doc_id_lem id in liftR ((prefix 2 1) (string "write_reg_field") (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ - string_lit(doc_id_lem id) ^/^ expY e)) + field_ref ^/^ expY e)) (* | (LEXP_id id | LEXP_cast (_,id)), t, Alias alias_info -> (match alias_info with | Alias_field(reg,field) -> @@ -562,8 +589,7 @@ let doc_exp_lem, doc_let_lem = when Env.is_regtyp tid env -> let t = (* Env.base_typ_of (env_of full_exp) *) (typ_of full_exp) in let eff = effect_of full_exp in - let field_f = string "get" ^^ underscore ^^ - doc_id_lem tid ^^ underscore ^^ doc_id_lem id in + let field_f = doc_id_lem tid ^^ underscore ^^ doc_id_lem id ^^ dot ^^ string "get_field" in let (ta,aexp_needed) = if contains_bitvector_typ t && not (contains_t_pp_var t) then (doc_tannot_lem regtypes (effectful eff) t, true) @@ -986,15 +1012,41 @@ let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with doc_op equals (concat [string "type"; space; doc_id_lem_type id]) (doc_typschm_lem regtypes false typschm) | TD_record(id,nm,typq,fs,_) -> - let f_pp (typ,fid) = - let fname = if prefix_recordtype - then concat [doc_id_lem id;string "_";doc_id_lem_type fid;] - else doc_id_lem_type fid in - concat [fname;space;colon;space;doc_typ_lem regtypes typ; semi] in - let fs_doc = group (separate_map (break 1) f_pp fs) in + let fname fid = if prefix_recordtype + then concat [doc_id_lem id;string "_";doc_id_lem_type fid;] + else doc_id_lem_type fid in + let f_pp (typ,fid) = + concat [fname fid;space;colon;space;doc_typ_lem regtypes typ; semi] in + let rectyp = match typq with + | TypQ_aux (TypQ_tq qs, _) -> + let quant_item = function + | QI_aux (QI_id (KOpt_aux (KOpt_none kid, _)), l) + | QI_aux (QI_id (KOpt_aux (KOpt_kind (_, kid), _)), l) -> + [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid, l)), l)] + | _ -> [] in + let targs = List.concat (List.map quant_item qs) in + mk_typ (Typ_app (id, targs)) + | TypQ_aux (TypQ_no_forall, _) -> mk_id_typ id in + let fs_doc = group (separate_map (break 1) f_pp fs) in + let doc_field (ftyp, fid) = + let reftyp = + mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown), + [mk_typ_arg (Typ_arg_typ rectyp); + mk_typ_arg (Typ_arg_typ ftyp)])) in + let rfannot = doc_tannot_lem regtypes false reftyp in + let get, set = + string "rec_val" ^^ dot ^^ fname fid, + anglebars (space ^^ string "rec_val with " ^^ + (doc_op equals (fname fid) (string "v")) ^^ space) in doc_op equals - (concat [string "type"; space; doc_id_lem_type id;]) - ((*doc_typquant_lem typq*) (anglebars (space ^^ align fs_doc ^^ space))) + (concat [string "let "; parens (concat [doc_id_lem id; underscore; doc_id_lem fid; rfannot])]) + (anglebars (concat [space; + doc_op equals (string "get_field") (parens (doc_op arrow (string "fun rec_val") get)); semi_sp; + doc_op equals (string "set_field") (parens (doc_op arrow (string "fun rec_val v") set)); space])) in + doc_op equals + (separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem typq]) + ((*doc_typquant_lem typq*) (anglebars (space ^^ align fs_doc ^^ space))) ^^ hardline ^^ + separate_map hardline doc_field fs | TD_variant(id,nm,typq,ar,_) -> (match id with | Id_aux ((Id "read_kind"),_) -> empty @@ -1198,27 +1250,38 @@ let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with | BF_aux (BF_single i, _) -> (i, i) | BF_aux (BF_range (i, j), _) -> (i, j) | _ -> raise (Reporting_basic.err_unreachable l "unsupported field type") in + let fsize = if dir_b then j-i+1 else i-j+1 in + let ftyp = vector_typ (nconstant i) (nconstant fsize) ord bit_typ in + let reftyp = + mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown), + [mk_typ_arg (Typ_arg_typ (mk_id_typ id)); + mk_typ_arg (Typ_arg_typ ftyp)])) in + let rfannot = doc_tannot_lem regtypes false reftyp in let get, set = "bitvector_subrange" ^ dir_suffix ^ " (reg, " ^ string_of_int i ^ ", " ^ string_of_int j ^ ")", "bitvector_update" ^ dir_suffix ^ " (reg, " ^ string_of_int i ^ ", " ^ string_of_int j ^ ", v)" in doc_op equals - (concat [string "let get_"; doc_id_lem id; underscore; doc_id_lem fid; - space; parens (string "reg" ^^ tannot)]) (string get) ^^ - hardline ^^ - doc_op equals + (concat [string "let "; parens (concat [doc_id_lem id; underscore; doc_id_lem fid; rfannot])]) + (concat [ + space; langlebar; string (" get_field = (fun reg -> " ^ get ^ ");"); hardline; + space; space; space; string (" set_field = (fun reg v -> " ^ set ^ ") "); ranglebar]) + (* string " = <|" (*; parens (string "reg" ^^ tannot) *)]) ^^ hardline ^^ + string (" get_field = (fun reg -> " ^ get ^ ");") ^^ hardline ^^ + string (" set_field = (fun reg v -> " ^ set ^") |>") *) + (* doc_op equals (concat [string "let set_"; doc_id_lem id; underscore; doc_id_lem fid; - space; parens (separate comma_sp [parens (string "reg" ^^ tannot); string "v"])]) (string set) + space; parens (separate comma_sp [parens (string "reg" ^^ tannot); string "v"])]) (string set) *) in doc_op equals (concat [string "type";space;doc_id_lem id]) (doc_typ_lem regtypes vtyp) ^^ hardline ^^ - doc_op equals + (* doc_op equals (concat [string "let";space;string "build_";doc_id_lem id;space;string "regname"]) (string "Register" ^^ space ^^ align (separate space [string "regname"; doc_int size; doc_int i1; dir; break 0 ^^ brackets (align doc_rids)])) - ^^ hardline ^^ + ^^ hardline ^^ *) doc_op equals (concat [string "let";space;string "cast_";doc_id_lem id;space;string "reg"]) (string "reg") @@ -1333,7 +1396,8 @@ let rec doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),fannot)) let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) = match reg with | DEC_reg(typ,id) -> - let env = env_of_annot annot in + empty + (* let env = env_of_annot annot in (match typ with | Typ_aux (Typ_id idt, _) when Env.is_regtyp idt env -> separate space [string "let";doc_id_lem id;equals; @@ -1356,7 +1420,7 @@ let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) = else raise (Reporting_basic.err_unreachable l ("can't deal with register type " ^ string_of_typ typ)) else raise (Reporting_basic.err_unreachable l - ("can't deal with register type " ^ string_of_typ typ))) + ("can't deal with register type " ^ string_of_typ typ))) *) | DEC_alias(id,alspec) -> empty | DEC_typ_alias(typ,id,alspec) -> empty @@ -1399,9 +1463,50 @@ let find_regtypes (Defs defs) = | _ -> acc ) [] defs -let pp_defs_lem (types_file,types_modules) (prompt_file,prompt_modules) (state_file,state_modules) d top_line = +let find_registers (Defs defs) = + List.fold_left + (fun acc def -> + match def with + | DEF_reg_dec (DEC_aux(DEC_reg (typ, id),_)) -> (typ, id) :: acc + | _ -> acc + ) [] defs + +let doc_regstate_lem regtypes registers = + let l = Parse_ast.Unknown in + let annot = (l, None) in + let regstate = match registers with + | [] -> + TD_abbrev ( + Id_aux (Id "regstate", l), + Name_sect_aux (Name_sect_none, l), + TypSchm_aux (TypSchm_ts (TypQ_aux (TypQ_tq [], l), unit_typ), l)) + | _ -> + TD_record ( + Id_aux (Id "regstate", l), + Name_sect_aux (Name_sect_none, l), + TypQ_aux (TypQ_tq [], l), + registers, + false) in + concat [ + doc_typdef_lem regtypes (TD_aux (regstate, annot)); hardline; + hardline; + string "type _M 'a = M regstate 'a" + ] + +let doc_register_refs_lem regtypes registers = + let doc_register_ref (typ, id) = + let idd = doc_id_lem id in + let field = if prefix_recordtype then string "regstate_" ^^ idd else idd in + concat [string "let "; idd; string " = <|"; hardline; + string " read_from = (fun s -> s."; field; string ");"; hardline; + string " write_to = (fun s v -> (<| s with "; field; string " = v |>)) |>"] in + separate_map hardline doc_register_ref registers + +let pp_defs_lem (types_file,types_modules) (types_seq_file,types_seq_modules) (prompt_file,prompt_modules) (state_file,state_modules) d top_line = let regtypes = find_regtypes d in let (typdefs,valdefs) = doc_defs_lem regtypes d in + let regstate_def = doc_regstate_lem regtypes (find_registers d) in + let register_refs = doc_register_refs_lem regtypes (find_registers d) in (print types_file) (concat [string "(*" ^^ (string top_line) ^^ string "*)";hardline; @@ -1420,6 +1525,30 @@ let pp_defs_lem (types_file,types_modules) (prompt_file,prompt_modules) (state_f hardline] else empty; typdefs]); + (print types_seq_file) + (concat + [string "(*" ^^ (string top_line) ^^ string "*)";hardline; + (separate_map hardline) + (fun lib -> separate space [string "open import";string lib]) types_seq_modules;hardline; + if !print_to_from_interp_value + then + concat + [(separate_map hardline) + (fun lib -> separate space [string " import";string lib]) ["Interp";"Interp_ast"]; + string "open import Deep_shallow_convert"; + hardline; + hardline; + string "module SI = Interp"; hardline; + string "module SIA = Interp_ast"; hardline; + hardline] + else empty; + typdefs; + hardline; + hardline; + regstate_def; + hardline; + hardline; + register_refs]); (print prompt_file) (concat [string "(*" ^^ (string top_line) ^^ string "*)";hardline; diff --git a/src/process_file.ml b/src/process_file.ml index 95562969..b63f7ba0 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -129,6 +129,31 @@ let close_output_with_check (o, temp_file_name, file_name) = let generated_line f = Printf.sprintf "Generated by Sail from %s." f +let output_lem filename libs libs_seq defs = + let generated_line = generated_line filename in + let types_module = (filename ^ "_embed_types") in + let types_module_sequential = (filename ^ "_embed_types_sequential") in + let ((ot,_, _) as ext_ot) = + open_output_with_check_unformatted (filename ^ "_embed_types.lem") in + let ((ots,_, _) as ext_ots) = + open_output_with_check_unformatted (filename ^ "_embed_types_sequential.lem") in + let ((o,_, _) as ext_o) = + open_output_with_check_unformatted (filename ^ "_embed.lem") in + let ((os,_, _) as ext_os) = + open_output_with_check_unformatted (filename ^ "_embed_sequential.lem") in + (Pretty_print.pp_defs_lem + (ot,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Prompt"]) + (ots,["Pervasives_extra";"Sail_impl_base";"Sail_values";"State"]) + (o,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Prompt"; + String.capitalize types_module] @ libs) + (os,["Pervasives_extra";"Sail_impl_base";"Sail_values";"State"; + String.capitalize types_module_sequential] @ libs_seq) + defs generated_line); + close_output_with_check ext_ot; + close_output_with_check ext_ots; + close_output_with_check ext_o; + close_output_with_check ext_os + let output1 libpath out_arg filename defs = let f' = Filename.basename (Filename.chop_extension filename) in match out_arg with @@ -175,43 +200,9 @@ let output1 libpath out_arg filename defs = close_output_with_check ext_o end | Lem_out None -> - let generated_line = generated_line filename in - let types_module = (f' ^ "_embed_types") in - let ((o,_, _) as ext_o) = - open_output_with_check_unformatted (f' ^ "_embed_types.lem") in - let ((o',_, _) as ext_o') = - open_output_with_check_unformatted (f' ^ "_embed.lem") in - let ((o'',_, _) as ext_o'') = - open_output_with_check_unformatted (f' ^ "_embed_sequential.lem") in - (Pretty_print.pp_defs_lem - (o,["Pervasives_extra";"Sail_impl_base";"Sail_values"]) - (o',["Pervasives_extra";"Sail_impl_base";"Prompt";"Sail_values"; - String.capitalize types_module]) - (o'',["Pervasives_extra";"Sail_impl_base";"State";"Sail_values"; - String.capitalize types_module]) - defs generated_line); - close_output_with_check ext_o; - close_output_with_check ext_o'; - close_output_with_check ext_o''; + output_lem f' [] [] defs | Lem_out (Some lib) -> - let generated_line = generated_line filename in - let types_module = (f' ^ "_embed_types") in - let ((o,_, _) as ext_o) = - open_output_with_check_unformatted (f' ^ "_embed_types.lem") in - let ((o',_, _) as ext_o') = - open_output_with_check_unformatted (f' ^ "_embed.lem") in - let ((o'',_, _) as ext_o'') = - open_output_with_check_unformatted (f' ^ "_embed_sequential.lem") in - (Pretty_print.pp_defs_lem - (o,["Pervasives_extra";"Sail_impl_base";"Sail_values"]) - (o',["Pervasives_extra";"Sail_impl_base";"Prompt"; - "Sail_values";String.capitalize types_module;lib]) - (o'',["Pervasives_extra";"Sail_impl_base";"State"; - "Sail_values";String.capitalize types_module;lib ^ "_sequential"]) - defs generated_line); - close_output_with_check ext_o; - close_output_with_check ext_o'; - close_output_with_check ext_o'' + output_lem f' [lib] [lib ^ "_sequential"] defs | Ocaml_out None -> let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in begin Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Big_int_Z";"Sail_values"]; -- cgit v1.2.3