diff options
Diffstat (limited to 'src/state.ml')
| -rw-r--r-- | src/state.ml | 32 |
1 files changed, 16 insertions, 16 deletions
diff --git a/src/state.ml b/src/state.ml index 00f81bf4..4fc2e1e8 100644 --- a/src/state.ml +++ b/src/state.ml @@ -102,12 +102,12 @@ let generate_initial_regstate defs = if string_of_id id = "unit" then "()" else Bindings.find id vals [] | Typ_app (id, _) when string_of_id id = "list" -> "[||]" - | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp, _)]) when string_of_id id = "atom" -> + | Typ_app (id, [A_aux (A_nexp nexp, _)]) when string_of_id id = "atom" -> string_of_nexp nexp - | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp, _); _]) when string_of_id id = "range" -> + | Typ_app (id, [A_aux (A_nexp nexp, _); _]) when string_of_id id = "range" -> string_of_nexp nexp - | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_constant len, _)), _); _ ; - Typ_arg_aux (Typ_arg_typ etyp, _)]) + | Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_constant len, _)), _); _ ; + A_aux (A_typ etyp, _)]) when string_of_id id = "vector" -> (* Output a list of initial values of the vector elements, or a literal binary zero value if this is a bitvector and the @@ -146,7 +146,7 @@ let generate_initial_regstate defs = string_of_id id1 ^ " (" ^ lookup_init_val vals typ1 ^ ")" in Bindings.add id init_val vals - | TD_abbrev (id, tq, Typ_arg_aux (Typ_arg_typ typ, _)) -> + | TD_abbrev (id, tq, A_aux (A_typ typ, _)) -> let init_val args = lookup_init_val vals (typ_subst_typquant tq args typ) in Bindings.add id init_val vals | TD_record (id, _, tq, fields, _) -> @@ -174,12 +174,12 @@ let generate_initial_regstate defs = let rec regval_constr_id mwords (Typ_aux (t, l) as typ) = match t with | Typ_id id -> id | Typ_app (id, args) -> - let name_arg (Typ_arg_aux (targ, _)) = match targ with - | Typ_arg_typ targ -> string_of_id (regval_constr_id mwords targ) - | Typ_arg_nexp nexp when is_nexp_constant (nexp_simp nexp) -> + let name_arg (A_aux (targ, _)) = match targ with + | A_typ targ -> string_of_id (regval_constr_id mwords targ) + | A_nexp nexp when is_nexp_constant (nexp_simp nexp) -> string_of_nexp (nexp_simp nexp) - | Typ_arg_order (Ord_aux (Ord_inc, _)) -> "inc" - | Typ_arg_order (Ord_aux (Ord_dec, _)) -> "dec" + | A_order (Ord_aux (Ord_inc, _)) -> "inc" + | A_order (Ord_aux (Ord_dec, _)) -> "dec" | _ -> raise (Reporting.err_typ l "Unsupported register type") in @@ -194,9 +194,9 @@ let register_base_types mwords typs = match t with | Typ_app (id, args) when IdSet.mem id builtins && not (mwords && is_bitvector_typ typ) -> - let add_typ_arg base_typs (Typ_arg_aux (targ, _)) = + let add_typ_arg base_typs (A_aux (targ, _)) = match targ with - | Typ_arg_typ typ -> add_base_typs typs typ + | A_typ typ -> add_base_typs typs typ | _ -> typs in List.fold_left add_typ_arg typs args @@ -243,12 +243,12 @@ let rec regval_convs_lem mwords (Typ_aux (t, _) as typ) = match t with let etyp_of, of_etyp = regval_convs_lem mwords etyp in "(fun v -> vector_of_regval " ^ etyp_of ^ " v)", "(fun v -> regval_of_vector " ^ of_etyp ^ " " ^ size ^ " " ^ is_inc ^ " v)" - | Typ_app (id, [Typ_arg_aux (Typ_arg_typ etyp, _)]) + | Typ_app (id, [A_aux (A_typ etyp, _)]) when string_of_id id = "list" -> let etyp_of, of_etyp = regval_convs_lem mwords etyp in "(fun v -> list_of_regval " ^ etyp_of ^ " v)", "(fun v -> regval_of_list " ^ of_etyp ^ " v)" - | Typ_app (id, [Typ_arg_aux (Typ_arg_typ etyp, _)]) + | Typ_app (id, [A_aux (A_typ etyp, _)]) when string_of_id id = "option" -> let etyp_of, of_etyp = regval_convs_lem mwords etyp in "(fun v -> option_of_regval " ^ etyp_of ^ " v)", @@ -407,12 +407,12 @@ let rec regval_convs_coq (Typ_aux (t, _) as typ) = match t with let etyp_of, of_etyp = regval_convs_coq etyp in "(fun v => vector_of_regval " ^ size ^ " " ^ etyp_of ^ " v)", "(fun v => regval_of_vector " ^ of_etyp ^ " " ^ size ^ " " ^ is_inc ^ " v)" - | Typ_app (id, [Typ_arg_aux (Typ_arg_typ etyp, _)]) + | Typ_app (id, [A_aux (A_typ etyp, _)]) when string_of_id id = "list" -> let etyp_of, of_etyp = regval_convs_coq etyp in "(fun v => list_of_regval " ^ etyp_of ^ " v)", "(fun v => regval_of_list " ^ of_etyp ^ " v)" - | Typ_app (id, [Typ_arg_aux (Typ_arg_typ etyp, _)]) + | Typ_app (id, [A_aux (A_typ etyp, _)]) when string_of_id id = "option" -> let etyp_of, of_etyp = regval_convs_coq etyp in "(fun v => option_of_regval " ^ etyp_of ^ " v)", |