summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ast_util.ml8
-rw-r--r--src/initial_check.ml2
-rw-r--r--src/monomorphise.ml16
-rw-r--r--src/pretty_print_lem.ml2
-rw-r--r--src/pretty_print_lem_ast.ml2
-rw-r--r--src/pretty_print_sail.ml9
-rw-r--r--src/rewriter.ml6
-rw-r--r--src/rewriter.mli2
-rw-r--r--src/rewrites.ml2
-rw-r--r--src/type_check.ml12
10 files changed, 35 insertions, 26 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 891990b4..3f13e6ad 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -407,7 +407,7 @@ and map_pat_annot_aux f = function
| P_as (pat, id) -> P_as (map_pat_annot f pat, id)
| P_typ (typ, pat) -> P_typ (typ, map_pat_annot f pat)
| P_id id -> P_id id
- | P_var (pat, kid) -> P_var (map_pat_annot f pat, kid)
+ | P_var (pat, tpat) -> P_var (map_pat_annot f pat, tpat)
| P_app (id, pats) -> P_app (id, List.map (map_pat_annot f) pats)
| P_record (fpats, b) -> P_record (List.map (map_fpat_annot f) fpats, b)
| P_tup pats -> P_tup (List.map (map_pat_annot f) pats)
@@ -665,12 +665,16 @@ 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_tpat = function
+ | TP_wild -> "_"
+ | TP_var kid -> string_of_kid kid
+ | TP_app (f, tpats) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_tpat tpats ^ ")"
and string_of_pat (P_aux (pat, l)) =
match pat with
| P_lit lit -> string_of_lit lit
| P_wild -> "_"
| P_id v -> string_of_id v
- | P_var (pat, kid) -> string_of_pat pat ^ " as " ^ string_of_kid kid
+ | P_var (pat, tpat) -> string_of_pat pat ^ " as " ^ string_of_tpat tpat
| P_typ (typ, pat) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_pat pat
| P_tup pats -> "(" ^ string_of_list ", " string_of_pat pats ^ ")"
| P_app (f, pats) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_pat pats ^ ")"
diff --git a/src/initial_check.ml b/src/initial_check.ml
index f859affa..812bfaad 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -440,7 +440,7 @@ let rec to_ast_pat (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.P_aux(pa
| Parse_ast.P_as(pat,id) -> P_as(to_ast_pat k_env def_ord pat,to_ast_id id)
| Parse_ast.P_typ(typ,pat) -> P_typ(to_ast_typ k_env def_ord typ,to_ast_pat k_env def_ord pat)
| Parse_ast.P_id(id) -> P_id(to_ast_id id)
- | Parse_ast.P_var (pat, kid) -> P_var (to_ast_pat k_env def_ord pat, to_ast_var kid)
+ | Parse_ast.P_var (pat,kid) -> P_var (to_ast_pat k_env def_ord pat, TP_var (to_ast_var kid))
| Parse_ast.P_app(id,pats) ->
if pats = []
then P_id (to_ast_id id)
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 4a075a15..a4d404e1 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -499,7 +499,7 @@ let nexp_subst_fns substs =
let re p = P_aux (p,(l,s_tannot annot)) in
match p with
| P_lit _ | P_wild | P_id _ -> re p
- | P_var (p',kid) -> re (P_var (s_pat p',kid))
+ | P_var (p',tpat) -> re (P_var (s_pat p',tpat))
| P_as (p',id) -> re (P_as (s_pat p', id))
| P_typ (ty,p') -> re (P_typ (s_t ty,s_pat p'))
| P_app (id,ps) -> re (P_app (id, List.map s_pat ps))
@@ -1310,7 +1310,7 @@ let split_defs continue_anyway 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), kid),_) ->
+ | P_aux (P_var (P_aux (P_id id,p_id_annot), TP_var kid),_) ->
begin
match lit_e with
| L_num i ->
@@ -1335,7 +1335,7 @@ let split_defs continue_anyway 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), kid),_) ->
+ | P_aux (P_var (P_aux (P_id id,p_id_annot), 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. *)
@@ -1555,7 +1555,7 @@ let split_defs continue_anyway splits defs =
begin
let kid,kid_annot =
match args with
- | [P_aux (P_var (_,kid),ann)] -> kid,ann
+ | [P_aux (P_var (_, TP_var kid),ann)] -> kid,ann
| _ ->
raise (Reporting_basic.err_general l
"Pattern match not currently supported by monomorphisation")
@@ -1802,7 +1802,7 @@ 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),kid) -> KidSet.add kid s, P_var (pat,kid)) }
+ p_var = (fun ((s,pat), TP_var kid) -> KidSet.add kid s, P_var (pat, TP_var kid)) }
pat)
let tyvars_bound_in_lb (LB_aux (LB_val (pat,_),_)) = tyvars_bound_in_pat pat
@@ -2056,7 +2056,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',kid1), P_var (p2',kid2) -> Kid.compare kid1 kid2 == 0 && pat_eq p1' p2'
+ | P_var (p1', TP_var kid1), P_var (p2', TP_var kid2) -> Kid.compare kid1 kid2 == 0 && 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) ->
@@ -2246,7 +2246,7 @@ 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),kid) -> (KidSet.add kid s, P_var (p,kid))) }) pat)
+ with p_var = (fun ((s,p), TP_var kid) -> (KidSet.add kid s, P_var (p, TP_var kid))) }) pat)
(* Add bound variables from a pattern to the environment with the given dependency. *)
@@ -2730,7 +2730,7 @@ let initial_env fn_id (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,kid) ->
+ | P_var (pat, TP_var kid) ->
let s,v,k = aux pat in
s,v,KBindings.add kid (Have (ArgSplits.empty,CallerArgSet.singleton (fn_id,i),CallerKidSet.empty)) k
| P_app (_,pats) -> of_list pats
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 48825540..40d373b2 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -449,7 +449,7 @@ let rec doc_pat_lem ctxt apat_needed (P_aux (p,(l,annot)) as pa) = match p with
begin match id with
| Id_aux (Id "None",_) -> string "Nothing" (* workaround temporary issue *)
| _ -> doc_id_lem id end
- | P_var(p,kid) -> doc_pat_lem ctxt true p
+ | P_var(p,_) -> doc_pat_lem ctxt true p
| P_as(p,id) -> parens (separate space [doc_pat_lem ctxt true p; string "as"; doc_id_lem id])
| P_typ(Typ_aux (Typ_tup typs, _), P_aux (P_tup pats, _)) ->
(* Isabelle does not seem to like type-annotated tuple patterns;
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 21001f55..63661bb9 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -317,7 +317,7 @@ let rec pp_format_pat_lem (P_aux(p,(l,annot))) =
| P_lit(lit) -> "(P_lit " ^ pp_format_lit_lem lit ^ ")"
| P_wild -> "P_wild"
| P_id(id) -> "(P_id " ^ pp_format_id_lem id ^ ")"
- | P_var(pat,kid) -> "(P_var " ^ pp_format_pat_lem pat ^ " " ^ pp_format_var_lem kid ^ ")"
+ | P_var(pat,_) -> "(P_var " ^ pp_format_pat_lem pat ^ ")" (* FIXME *)
| P_as(pat,id) -> "(P_as " ^ pp_format_pat_lem pat ^ " " ^ pp_format_id_lem id ^ ")"
| P_typ(typ,pat) -> "(P_typ " ^ pp_format_typ_lem typ ^ " " ^ pp_format_pat_lem pat ^ ")"
| P_app(id,pats) -> "(P_app " ^ pp_format_id_lem id ^ " [" ^
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index b55448fa..8d9b12d1 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -70,6 +70,11 @@ let doc_ord (Ord_aux(o,_)) = match o with
| Ord_inc -> string "inc"
| Ord_dec -> string "dec"
+let rec doc_typ_pat = function
+ | 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)
+
let rec doc_nexp =
let rec atomic_nexp (Nexp_aux (n_aux, _) as nexp) =
match n_aux with
@@ -216,9 +221,9 @@ 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, _), kid) when Id.compare (id_of_kid kid) id == 0 ->
+ | P_var (P_aux (P_id id, _), TP_var kid) when Id.compare (id_of_kid kid) id == 0 ->
doc_kid kid
- | P_var (pat, kid) -> separate space [doc_pat pat; string "as"; 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)
| P_vector_concat pats -> separate_map (space ^^ string "@" ^^ space) doc_pat pats
| P_wild -> string "_"
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 9e9409ec..539ba0c8 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -408,7 +408,7 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
; p_as : 'pat * id -> 'pat_aux
; p_typ : Ast.typ * 'pat -> 'pat_aux
; p_id : id -> 'pat_aux
- ; p_var : 'pat * kid -> 'pat_aux
+ ; p_var : 'pat * typ_pat -> 'pat_aux
; p_app : id * 'pat list -> 'pat_aux
; p_record : 'fpat list * bool -> 'pat_aux
; p_vector : 'pat list -> 'pat_aux
@@ -426,7 +426,7 @@ let rec fold_pat_aux (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat
| P_lit lit -> alg.p_lit lit
| P_wild -> alg.p_wild
| P_id id -> alg.p_id id
- | P_var (p, kid) -> alg.p_var (fold_pat alg p, kid)
+ | P_var (p,tpat) -> alg.p_var (fold_pat alg p, tpat)
| P_as (p,id) -> alg.p_as (fold_pat alg p, id)
| P_typ (typ,p) -> alg.p_typ (typ,fold_pat alg p)
| P_app (id,ps) -> alg.p_app (id,List.map (fold_pat alg) ps)
@@ -454,7 +454,7 @@ let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg =
; p_as = (fun (pat,id) -> P_as (pat,id))
; p_typ = (fun (typ,pat) -> P_typ (typ,pat))
; p_id = (fun id -> P_id id)
- ; p_var = (fun (pat,kid) -> P_var (pat,kid))
+ ; p_var = (fun (pat,tpat) -> P_var (pat,tpat))
; p_app = (fun (id,ps) -> P_app (id,ps))
; p_record = (fun (ps,b) -> P_record (ps,b))
; p_vector = (fun ps -> P_vector ps)
diff --git a/src/rewriter.mli b/src/rewriter.mli
index c3c384bf..b830bdeb 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -87,7 +87,7 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
; p_as : 'pat * id -> 'pat_aux
; p_typ : Ast.typ * 'pat -> 'pat_aux
; p_id : id -> 'pat_aux
- ; p_var : 'pat * kid -> 'pat_aux
+ ; p_var : 'pat * typ_pat -> 'pat_aux
; p_app : id * 'pat list -> 'pat_aux
; p_record : 'fpat list * bool -> 'pat_aux
; p_vector : 'pat list -> 'pat_aux
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 074ad60f..e38169cc 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -2677,7 +2677,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)),
- lvar_kid)) el env lvar_typ) in
+ TP_var lvar_kid)) 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 248faceb..9b704a90 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2367,7 +2367,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
| Unification_error (l, m) -> typ_error l ("Unification error when pattern matching against union constructor: " ^ m)
end
end
- | P_var (pat, kid) ->
+ | P_var (pat, TP_var kid) ->
let typ = Env.expand_synonyms env typ in
begin
match destruct_exist env typ, typ with
@@ -2376,29 +2376,29 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
let ex_typ = typ_subst_nexp kid' (Nexp_var kid) ex_typ in
let env = Env.add_constraint (nc_subst_nexp kid' (Nexp_var kid) nc) env in
let typed_pat, env, guards = bind_pat env pat ex_typ in
- annot_pat (P_var (typed_pat, kid)) typ, env, guards
+ annot_pat (P_var (typed_pat, TP_var kid)) typ, env, guards
| Some _, _ -> typ_error l ("Cannot bind type variable pattern against multiple argument existential")
| None, Typ_aux (Typ_id id, _) when Id.compare id (mk_id "int") == 0 ->
let env = Env.add_typ_var kid BK_nat env in
let typed_pat, env, guards = bind_pat env pat (atom_typ (nvar kid)) in
- annot_pat (P_var (typed_pat, kid)) typ, env, guards
+ annot_pat (P_var (typed_pat, TP_var kid)) typ, env, guards
| None, Typ_aux (Typ_id id, _) when Id.compare id (mk_id "nat") == 0 ->
let env = Env.add_typ_var kid BK_nat env in
let env = Env.add_constraint (nc_gt (nvar kid) (nint 0)) env in
let typed_pat, env, guards = bind_pat env pat (atom_typ (nvar kid)) in
- annot_pat (P_var (typed_pat, kid)) typ, env, guards
+ annot_pat (P_var (typed_pat, TP_var kid)) typ, env, guards
| None, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp lo, _); Typ_arg_aux (Typ_arg_nexp hi, _)]), _)
when Id.compare id (mk_id "range") == 0 ->
let env = Env.add_typ_var kid BK_nat env in
let env = Env.add_constraint (nc_and (nc_lteq lo (nvar kid)) (nc_lteq (nvar kid) hi)) env in
let typed_pat, env, guards = bind_pat env pat (atom_typ (nvar kid)) in
- annot_pat (P_var (typed_pat, kid)) typ, env, guards
+ annot_pat (P_var (typed_pat, TP_var kid)) typ, env, guards
| None, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n, _)]), _)
when Id.compare id (mk_id "atom") == 0 ->
let env = Env.add_typ_var kid BK_nat env in
let env = Env.add_constraint (nc_eq (nvar kid) n) env in
let typed_pat, env, guards = bind_pat env pat (atom_typ (nvar kid)) in
- annot_pat (P_var (typed_pat, kid)) typ, env, guards
+ annot_pat (P_var (typed_pat, TP_var kid)) typ, env, guards
| None, _ -> typ_error l ("Cannot bind type variable against non existential or numeric type")
end
| P_wild -> annot_pat P_wild typ, env, []
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 22:37:29 +0000