summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ast_util.ml3
-rw-r--r--src/initial_check.ml6
-rw-r--r--src/monomorphise.ml24
-rw-r--r--src/pretty_print_sail.ml5
-rw-r--r--src/rewrites.ml2
-rw-r--r--src/type_check.ml14
6 files changed, 33 insertions, 21 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 2fb90b02..e58842d2 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -669,7 +669,8 @@ and string_of_pexp (Pat_aux (pexp, _)) =
match pexp with
| Pat_exp (pat, exp) -> string_of_pat pat ^ " -> " ^ string_of_exp exp
| Pat_when (pat, guard, exp) -> string_of_pat pat ^ " when " ^ string_of_exp guard ^ " -> " ^ string_of_exp exp
-and string_of_typ_pat = function
+and string_of_typ_pat (TP_aux (tpat_aux, _)) =
+ match tpat_aux with
| TP_wild -> "_"
| TP_var kid -> string_of_kid kid
| TP_app (f, tpats) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_typ_pat tpats ^ ")"
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 9516f53e..9da200d9 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -434,10 +434,10 @@ let to_ast_lit (Parse_ast.L_aux(lit,l)) : lit =
let rec to_ast_typ_pat (Parse_ast.ATyp_aux (typ_aux, l)) =
match typ_aux with
- | Parse_ast.ATyp_wild -> TP_wild
- | Parse_ast.ATyp_var kid -> TP_var (to_ast_var kid)
+ | Parse_ast.ATyp_wild -> TP_aux (TP_wild, l)
+ | Parse_ast.ATyp_var kid -> TP_aux (TP_var (to_ast_var kid), l)
| Parse_ast.ATyp_app (f, typs) ->
- TP_app (to_ast_id f, List.map to_ast_typ_pat typs)
+ TP_aux (TP_app (to_ast_id f, List.map to_ast_typ_pat typs), l)
| _ -> typ_error l "Unexpected type in type pattern" None None None
let rec to_ast_pat (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.P_aux(pat,l) : Parse_ast.pat) : unit pat =
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 3b8a5073..2b4821e0 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -1392,7 +1392,7 @@ let split_defs all_errors splits defs =
let checkpat = function
| P_aux (P_lit (L_aux (lit_p, _)),_) ->
if lit_match (lit_e,lit_p) then DoesMatch ([],[]) else DoesNotMatch
- | P_aux (P_var (P_aux (P_id id,p_id_annot), TP_var kid),_) ->
+ | P_aux (P_var (P_aux (P_id id,p_id_annot), TP_aux (TP_var kid, _)),_) ->
begin
match lit_e with
| L_num i ->
@@ -1417,7 +1417,7 @@ let split_defs all_errors splits defs =
| E_cast (undef_typ, (E_aux (E_lit (L_aux (L_undef, lit_l)),_) as e_undef)) ->
let checkpat = function
| P_aux (P_lit (L_aux (lit_p, _)),_) -> DoesNotMatch
- | P_aux (P_var (P_aux (P_id id,p_id_annot), TP_var kid),_) ->
+ | P_aux (P_var (P_aux (P_id id,p_id_annot), TP_aux (TP_var kid, _)),_) ->
(* For undefined we fix the type-level size (because there's no good
way to construct an undefined size), but leave the term as undefined
to make the meaning clear. *)
@@ -1651,7 +1651,7 @@ let split_defs all_errors splits defs =
begin
let kid,kid_annot =
match args with
- | [P_aux (P_var (_, TP_var kid),ann)] -> kid,ann
+ | [P_aux (P_var (_, TP_aux (TP_var kid, _)),ann)] -> kid,ann
| _ ->
raise (Reporting_basic.err_general l
"Pattern match not currently supported by monomorphisation")
@@ -1905,7 +1905,8 @@ let tyvars_bound_in_pat pat =
let open Rewriter in
fst (fold_pat
{ (compute_pat_alg KidSet.empty KidSet.union) with
- p_var = (fun ((s,pat), TP_var kid) -> KidSet.add kid s, P_var (pat, TP_var kid)) }
+ p_var = (fun ((s,pat), (TP_aux (TP_var kid, _) as tpat)) ->
+ KidSet.add kid s, P_var (pat, tpat)) }
pat)
let tyvars_bound_in_lb (LB_aux (LB_val (pat,_),_)) = tyvars_bound_in_pat pat
@@ -2159,6 +2160,14 @@ let lit_eq' (L_aux (l1,_)) (L_aux (l2,_)) =
let forall2 p x y =
try List.for_all2 p x y with Invalid_argument _ -> false
+let rec typ_pat_eq (TP_aux (tp1, _)) (TP_aux (tp2, _)) =
+ match tp1, tp2 with
+ | TP_wild, TP_wild -> true
+ | TP_var kid1, TP_var kid2 -> Kid.compare kid1 kid2 = 0
+ | TP_app (f1, args1), TP_app (f2, args2) when List.length args1 = List.length args2 ->
+ Id.compare f1 f2 = 0 && List.for_all2 typ_pat_eq args1 args2
+ | _, _ -> false
+
let rec pat_eq (P_aux (p1,_)) (P_aux (p2,_)) =
match p1, p2 with
| P_lit lit1, P_lit lit2 -> lit_eq' lit1 lit2
@@ -2166,7 +2175,7 @@ let rec pat_eq (P_aux (p1,_)) (P_aux (p2,_)) =
| P_as (p1',id1), P_as (p2',id2) -> Id.compare id1 id2 == 0 && pat_eq p1' p2'
| P_typ (_,p1'), P_typ (_,p2') -> pat_eq p1' p2'
| P_id id1, P_id id2 -> Id.compare id1 id2 == 0
- | P_var (p1', TP_var kid1), P_var (p2', TP_var kid2) -> Kid.compare kid1 kid2 == 0 && pat_eq p1' p2'
+ | P_var (p1', tpat1), P_var (p2', tpat2) -> typ_pat_eq tpat1 tpat2 && pat_eq p1' p2'
| P_app (id1,args1), P_app (id2,args2) ->
Id.compare id1 id2 == 0 && forall2 pat_eq args1 args2
| P_record (fpats1, flag1), P_record (fpats2, flag2) ->
@@ -2404,7 +2413,8 @@ let rec split3 = function
let kids_bound_by_pat pat =
let open Rewriter in
fst (fold_pat ({ (compute_pat_alg KidSet.empty KidSet.union)
- with p_var = (fun ((s,p), TP_var kid) -> (KidSet.add kid s, P_var (p, TP_var kid))) }) pat)
+ with p_var = (fun ((s,p), (TP_aux (TP_var kid, _) as tpat)) ->
+ (KidSet.add kid s, P_var (p, tpat))) }) pat)
(* Add bound variables from a pattern to the environment with the given dependency. *)
@@ -2904,7 +2914,7 @@ let initial_env fn_id fn_l (TypQ_aux (tq,_)) pat set_assertions =
Bindings.singleton id (Unknown (l, ("Unable to give location for " ^ string_of_id id))),
KBindings.empty
end
- | P_var (pat, TP_var kid) ->
+ | P_var (pat, TP_aux (TP_var kid, _)) ->
let s,v,k = aux pat in
s,v,KBindings.add kid (Have (s, ExtraSplits.empty)) k
| P_app (_,pats) -> of_list pats
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 8d9b12d1..7620ca50 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -70,7 +70,8 @@ let doc_ord (Ord_aux(o,_)) = match o with
| Ord_inc -> string "inc"
| Ord_dec -> string "dec"
-let rec doc_typ_pat = function
+let rec doc_typ_pat (TP_aux (tpat_aux, _)) =
+ match tpat_aux with
| TP_wild -> string "_"
| TP_var kid -> doc_kid kid
| TP_app (f, tpats) -> doc_id f ^^ parens (separate_map (comma ^^ space) doc_typ_pat tpats)
@@ -221,7 +222,7 @@ let rec doc_pat (P_aux (p_aux, _) as pat) =
| P_typ (typ, pat) -> separate space [doc_pat pat; colon; doc_typ typ]
| P_lit lit -> doc_lit lit
(* P_var short form sugar *)
- | P_var (P_aux (P_id id, _), TP_var kid) when Id.compare (id_of_kid kid) id == 0 ->
+ | P_var (P_aux (P_id id, _), TP_aux (TP_var kid, _)) when Id.compare (id_of_kid kid) id == 0 ->
doc_kid kid
| P_var (pat, tpat) -> separate space [doc_pat pat; string "as"; doc_typ_pat tpat]
| P_vector pats -> brackets (separate_map (comma ^^ space) doc_pat pats)
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 6146e73b..ec5d5f6d 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -2684,7 +2684,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
let lvar_typ = mk_typ (Typ_exist ([lvar_kid], lvar_nc, atom_typ (nvar lvar_kid))) in
let lvar_pat = P_typ (lvar_typ, annot_pat (P_var (
annot_pat (P_id id) el env (atom_typ (nvar lvar_kid)),
- TP_var lvar_kid)) el env lvar_typ) in
+ TP_aux (TP_var lvar_kid, gen_loc el))) el env lvar_typ) in
let lb = annot_letbind (lvar_pat, exp1) el env lvar_typ in
let body = annot_exp (E_let (lb, exp4)) el env (typ_of exp4) in
let v = annot_exp (E_app (mk_id "foreach", [exp1; exp2; exp3; ord_exp; tuple_exp vars; body])) el env (typ_of body) in
diff --git a/src/type_check.ml b/src/type_check.ml
index 4d599125..f455b5b0 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2414,7 +2414,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
env, atom_typ (nvar kid)
| None, _ -> typ_error l ("Cannot bind type variable against non existential or numeric type")
in
- let env = bind_typ_pat l env typ_pat ex_typ in
+ let env = bind_typ_pat env typ_pat ex_typ in
let typed_pat, env, guards = bind_pat env pat ex_typ in
annot_pat (P_var (typed_pat, typ_pat)) typ, env, guards
| P_wild -> annot_pat P_wild typ, env, []
@@ -2559,8 +2559,8 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) =
guards
| _ -> typ_error l ("Couldn't infer type of pattern " ^ string_of_pat pat)
-and bind_typ_pat l env typ_pat (Typ_aux (typ_aux, _) as typ) =
- match typ_pat, typ_aux with
+and bind_typ_pat env (TP_aux (typ_pat_aux, l) as typ_pat) (Typ_aux (typ_aux, _) as typ) =
+ match typ_pat_aux, typ_aux with
| TP_wild, _ -> env
| TP_var kid, _ ->
begin
@@ -2573,14 +2573,14 @@ and bind_typ_pat l env typ_pat (Typ_aux (typ_aux, _) as typ) =
typ_error l ("Type " ^ string_of_typ typ ^ " has multiple numeric expressions. Cannot bind " ^ string_of_kid kid)
end
| TP_app (f1, tpats), Typ_app (f2, typs) when Id.compare f1 f2 = 0->
- List.fold_left2 (bind_typ_pat_arg l) env tpats typs
+ List.fold_left2 bind_typ_pat_arg env tpats typs
| _, _ -> typ_error l ("Couldn't bind type " ^ string_of_typ typ ^ " with " ^ string_of_typ_pat typ_pat)
-and bind_typ_pat_arg l env typ_pat (Typ_arg_aux (typ_arg_aux, _) as typ_arg) =
- match typ_pat, typ_arg_aux with
+and bind_typ_pat_arg env (TP_aux (typ_pat_aux, l) as typ_pat) (Typ_arg_aux (typ_arg_aux, _) as typ_arg) =
+ match typ_pat_aux, typ_arg_aux with
| TP_wild, _ -> env
| TP_var kid, Typ_arg_nexp nexp ->
Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var kid BK_nat env)
- | _, Typ_arg_typ typ -> bind_typ_pat l env typ_pat typ
+ | _, Typ_arg_typ typ -> bind_typ_pat env typ_pat typ
| _, Typ_arg_order _ -> typ_error l "Cannot bind type pattern against order"
| _, _ -> typ_error l ("Couldn't bind type argument " ^ string_of_typ_arg typ_arg ^ " with " ^ string_of_typ_pat typ_pat)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 14:17:40 +0000