diff options
| author | Jon French | 2019-02-13 12:27:48 +0000 |
|---|---|---|
| committer | Jon French | 2019-02-13 12:27:48 +0000 |
| commit | ea39b3c674570ce5eea34067c36d5196ca201f83 (patch) | |
| tree | 516e7491bc32797a4d0ac397ea47387f2b16cf1b /src/state.ml | |
| parent | ab3f3671d4dd682b2aee922d5a05e9455afd5849 (diff) | |
| parent | 24fc989891ad266eae642815646294279e2485ca (diff) | |
Merge branch 'sail2' into rmem_interpreter
Diffstat (limited to 'src/state.ml')
| -rw-r--r-- | src/state.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/state.ml b/src/state.ml index fe1cebe7..86fd8395 100644 --- a/src/state.ml +++ b/src/state.ml @@ -58,7 +58,7 @@ open PPrint open Pretty_print_common open Pretty_print_sail -let defs_of_string = ast_of_def_string Ast_util.inc_ord +let defs_of_string = ast_of_def_string let is_defined defs name = IdSet.mem (mk_id name) (ids_of_defs (Defs defs)) @@ -69,7 +69,7 @@ let find_registers defs = List.fold_left (fun acc def -> match def with - | DEF_reg_dec (DEC_aux(DEC_reg (typ, id), (_, tannot))) -> + | DEF_reg_dec (DEC_aux(DEC_reg (_, _, typ, id), (_, tannot))) -> let env = match destruct_tannot tannot with | Some (env, _, _) -> env | _ -> Env.empty @@ -136,10 +136,10 @@ let generate_initial_regstate defs = List.fold_left2 typ_subst_quant_item typ (quant_items tq) args in let add_typ_init_val (defs', vals) = function - | TD_enum (id, _, id1 :: _, _) -> + | TD_enum (id, id1 :: _, _) -> (* Choose the first value of an enumeration type as default *) (defs', Bindings.add id (fun _ -> string_of_id id1) vals) - | TD_variant (id, _, tq, (Tu_aux (Tu_ty_id (typ1, id1), _)) :: _, _) -> + | TD_variant (id, tq, (Tu_aux (Tu_ty_id (typ1, id1), _)) :: _, _) -> (* Choose the first variant of a union type as default *) let init_val args = let typ1 = typ_subst_typquant tq args typ1 in @@ -149,7 +149,7 @@ let generate_initial_regstate defs = | TD_abbrev (id, tq, A_aux (A_typ typ, _)) -> let init_val args = lookup_init_val vals (typ_subst_typquant tq args typ) in (defs', Bindings.add id init_val vals) - | TD_record (id, _, tq, fields, _) -> + | TD_record (id, tq, fields, _) -> let init_val args = let init_field (typ, id) = let typ = typ_subst_typquant tq args typ in |