diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 2 | ||||
| -rw-r--r-- | src/initial_check.ml | 1 | ||||
| -rw-r--r-- | src/parse_ast.ml | 1 | ||||
| -rw-r--r-- | src/parser.mly | 2 | ||||
| -rw-r--r-- | src/rewrites.ml | 7 | ||||
| -rw-r--r-- | src/sail_lib.ml | 10 | ||||
| -rw-r--r-- | src/type_check.ml | 13 |
7 files changed, 35 insertions, 1 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index fbbe274b..c57cd21f 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -472,6 +472,7 @@ and map_mpat_annot_aux f = function | MP_cons (mpat1, mpat2) -> MP_cons (map_mpat_annot f mpat1, map_mpat_annot f mpat2) | MP_string_append mpats -> MP_string_append (List.map (map_mpat_annot f) mpats) | MP_typ (mpat, typ) -> MP_typ (map_mpat_annot f mpat, typ) + | MP_as (mpat, id) -> MP_as (map_mpat_annot f mpat, id) and map_fpat_annot f (FP_aux (FP_Fpat (id, pat), annot)) = FP_aux (FP_Fpat (id, map_pat_annot f pat), f annot) and map_mfpat_annot f (MFP_aux (MFP_mpat (id, mpat), annot)) = MFP_aux (MFP_mpat (id, map_mpat_annot f mpat), f annot) @@ -765,6 +766,7 @@ and string_of_mpat (MP_aux (pat, l)) = | MP_vector pats -> "[" ^ string_of_list ", " string_of_mpat pats ^ "]" | MP_string_append pats -> string_of_list " ^^ " string_of_mpat pats | MP_typ (mpat, typ) -> "(" ^ string_of_mpat mpat ^ " : " ^ string_of_typ typ ^ ")" + | MP_as (mpat, id) -> "((" ^ string_of_mpat mpat ^ ") as " ^ string_of_id id ^ ")" | _ -> "MPAT" and string_of_lexp (LEXP_aux (lexp, _)) = diff --git a/src/initial_check.ml b/src/initial_check.ml index 63ff8f57..a774352d 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -787,6 +787,7 @@ let rec to_ast_mpat k_env def_ord (Parse_ast.MP_aux(mpat,l)) = (match mpat with | Parse_ast.MP_lit(lit) -> MP_lit(to_ast_lit lit) | Parse_ast.MP_id(id) -> MP_id(to_ast_id id) + | Parse_ast.MP_as (mpat, id) -> MP_as (to_ast_mpat k_env def_ord mpat, to_ast_id id) | Parse_ast.MP_app(id,mpats) -> if mpats = [] then MP_id (to_ast_id id) diff --git a/src/parse_ast.ml b/src/parse_ast.ml index c31d548c..2848edc0 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -440,6 +440,7 @@ type mpat_aux = (* Mapping pattern. Mostly the same as normal patterns but only | MP_cons of ( mpat) * ( mpat) | MP_string_append of mpat list | MP_typ of mpat * atyp + | MP_as of mpat * id and mpat = | MP_aux of ( mpat_aux) * l diff --git a/src/parser.mly b/src/parser.mly index 375eb7d1..60ccc81f 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -1229,6 +1229,8 @@ mpat_string_append: mpat: | atomic_mpat { $1 } + | atomic_mpat As id + { mk_mpat (MP_as ($1, $3)) $startpos $endpos } | atomic_mpat At mpat_concat { mk_mpat (MP_vector_concat ($1 :: $3)) $startpos $endpos } | atomic_mpat ColonColon mpat diff --git a/src/rewrites.ml b/src/rewrites.ml index b938d2d7..eab8db17 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -3720,6 +3720,10 @@ let rec exp_of_mpat (MP_aux (mpat, annot)) = | MP_cons (mpat1, mpat2) -> E_aux (E_cons (exp_of_mpat mpat1, exp_of_mpat mpat2), annot) | MP_string_append mpats -> List.fold_right (string_append annot) (List.map exp_of_mpat mpats) empty_string | MP_typ (mpat, typ) -> E_aux (E_cast (typ, exp_of_mpat mpat), annot) + | MP_as (mpat, id) -> E_aux (E_case (E_aux (E_id id, annot), [ + Pat_aux (Pat_exp (pat_of_mpat mpat, exp_of_mpat mpat), annot) + ]), annot) (* TODO FIXME ditto *) + and fexps_of_mfpats mfpats flag annot = let fexp_of_mfpat (MFP_aux (MFP_mpat (id, mpat), annot)) = @@ -3727,7 +3731,7 @@ and fexps_of_mfpats mfpats flag annot = in FES_aux (FES_Fexps (List.map fexp_of_mfpat mfpats, flag), annot) -let rec pat_of_mpat (MP_aux (mpat, annot)) = +and pat_of_mpat (MP_aux (mpat, annot)) = match mpat with | MP_lit lit -> P_aux (P_lit lit, annot) | MP_id id -> P_aux (P_id id, annot) @@ -3740,6 +3744,7 @@ let rec pat_of_mpat (MP_aux (mpat, annot)) = | MP_cons (mpat1, mpat2) -> P_aux ((P_cons (pat_of_mpat mpat1, pat_of_mpat mpat2), annot)) | MP_string_append (mpats) -> P_aux ((P_string_append (List.map pat_of_mpat mpats), annot)) | MP_typ (mpat, typ) -> P_aux (P_typ (typ, pat_of_mpat mpat), annot) + | MP_as (mpat, id) -> P_aux (P_as (pat_of_mpat mpat, id), annot) and fpats_of_mfpats mfpats = let fpat_of_mfpat (MFP_aux (MFP_mpat (id, mpat), annot)) = diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 89056347..8430ef86 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -721,6 +721,16 @@ let hex_bits_13_matches_prefix s = else ZNone () +let hex_bits_16_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + let n = Big_int.to_int n in + if 0 <= n && n < 65536 then + ZSome ((bits_of_int 32768 n, len)) + else + ZNone () + let hex_bits_20_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () diff --git a/src/type_check.ml b/src/type_check.ml index 66e5e656..be8f477f 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -3623,6 +3623,11 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) ( end | MP_app (f, _) when not (Env.is_union_constructor f env || Env.is_mapping f env) -> typ_error l (string_of_id f ^ " is not a union constructor or mapping in mapping-pattern " ^ string_of_mpat mpat) + | MP_as (mpat, id) -> + let (typed_mpat, env, guards) = bind_mpat allow_unknown other_env env mpat typ in + (annot_mpat (MP_as (typed_mpat, id)) (typ_of_mpat typed_mpat), + Env.add_local id (Immutable, typ_of_mpat typed_mpat) env, + guards) (* This is a special case for flow typing when we match a constant numeric literal. *) | MP_lit (L_aux (L_num n, _) as lit) when is_atom typ -> let nexp = match destruct_atom_nexp env typ with Some n -> n | None -> assert false in @@ -3723,6 +3728,11 @@ and infer_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) List.fold_left fold_pats ([], env, []) mpats in annot_mpat (MP_string_append typed_mpats) string_typ, env, guards + | MP_as (mpat, id) -> + let (typed_mpat, env, guards) = infer_mpat allow_unknown other_env env mpat in + (annot_mpat (MP_as (typed_mpat, id)) (typ_of_mpat typed_mpat), + Env.add_local id (Immutable, typ_of_mpat typed_mpat) env, + guards) | _ -> typ_error l ("Couldn't infer type of mapping-pattern " ^ string_of_mpat mpat) @@ -4028,6 +4038,9 @@ and propagate_mpat_effect_aux = function | MP_typ (mpat, typ) -> let p_mpat = propagate_mpat_effect mpat in MP_typ (p_mpat, typ), effect_of_mpat mpat + | MP_as (mpat, id) -> + let p_mpat = propagate_mpat_effect mpat in + MP_as (p_mpat, id), effect_of_mpat mpat | _ -> typ_error Parse_ast.Unknown "Unimplemented: Cannot propagate effect in mpat" |