summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--language/sail.ott68
-rw-r--r--src/ast_util.ml14
-rw-r--r--src/ast_util.mli1
-rw-r--r--src/initial_check.ml10
-rw-r--r--src/interpreter.ml1
-rw-r--r--src/monomorphise.ml22
-rw-r--r--src/parse_ast.ml8
-rw-r--r--src/parser.mly2
-rw-r--r--src/pattern_completeness.ml11
-rw-r--r--src/pretty_print_coq.ml2
-rw-r--r--src/pretty_print_lem.ml1
-rw-r--r--src/pretty_print_sail.ml1
-rw-r--r--src/rewriter.ml37
-rw-r--r--src/rewriter.mli35
-rw-r--r--src/rewrites.ml50
-rw-r--r--src/slice.ml1
-rw-r--r--src/spec_analysis.ml9
-rw-r--r--src/type_check.ml5
18 files changed, 46 insertions, 232 deletions
diff --git a/language/sail.ott b/language/sail.ott
index eb77e4aa..c0c8da49 100644
--- a/language/sail.ott
+++ b/language/sail.ott
@@ -388,51 +388,21 @@ pat :: 'P_' ::=
{{ com bind pattern to type variable }}
| id ( pat1 , .. , patn ) :: :: app
{{ com union constructor pattern }}
-
-% OR? do we invent something ghastly including a union keyword? Perhaps not...
-
-% | <| fpat1 ; ... ; fpatn semi_opt |> :: :: record
-% {{ com Record patterns }}
-% OR
- | { fpat1 ; ... ; fpatn semi_opt } :: :: record
- {{ com struct pattern }}
-
-%Patterns for vectors
-%Should these be the same since vector syntax has changed, and lists have also changed?
-
- | [ pat1 , .. , patn ] :: :: vector
- {{ com vector pattern }}
-
-% | [ num1 = pat1 , .. , numn = patn ] :: :: vector_indexed
-% {{ com vector pattern (with explicit indices) }}
-
-% cf ntoes for this
- | pat1 : .... : patn :: :: vector_concat
- {{ com concatenated vector pattern }}
-
- | ( pat1 , .... , patn ) :: :: tup
+ | [ pat1 , ... , patn ] :: :: vector
+ {{ com vector pattern }}
+ | pat1 @ ... @ patn :: :: vector_concat
+ {{ com concatenated vector pattern }}
+ | ( pat1 , .... , patn ) :: :: tup
{{ com tuple pattern }}
- | [|| pat1 , .. , patn ||] :: :: list
+ | [|| pat1 , .. , patn ||] :: :: list
{{ com list pattern }}
- | ( pat ) :: S :: paren
+ | ( pat ) :: S :: paren
{{ ichlo [[pat]] }}
- | pat1 '::' pat2 :: :: cons
+ | pat1 '::' pat2 :: :: cons
{{ com Cons patterns }}
-
- | pat1 ^^ ... ^^ patn :: :: string_append
+ | pat1 ^^ ... ^^ patn :: :: string_append
{{ com string append pattern, x ^^ y }}
-% XXX Is this still useful?
-fpat :: 'FP_' ::=
- {{ com field pattern }}
- {{ aux _ annot }} {{ auxparam 'a }}
- | id = pat :: :: Fpat
-
-mfpat :: 'MFP_' ::=
- {{ com Mapping field pattern, why does this have to exist }}
- {{ aux _ annot }} {{ auxparam 'a }}
- | id = mpat :: :: mpat
-
parsing
P_app <= P_app
P_app <= P_as
@@ -551,11 +521,8 @@ exp :: 'E_' ::=
{{ com tuple }}
| if exp1 then exp2 else exp3 :: :: if
{{ com conditional }}
- | if exp1 then exp2 :: S :: ifnoelse {{ ichlo [[ if exp1 then exp2 else ( ) ]] }}
| loop internal_loop_measure exp1 exp2 :: :: loop
- | while internal_loop_measure exp1 do exp2 :: S :: while {{ ichlo [[ loop internal_loop_measure while exp1 exp2 ]] }}
- | repeat internal_loop_measure exp1 until exp2 :: S :: until {{ ichlo [[ loop internal_loop_measure until exp2 exp1 ]] }}
- | foreach ( id from exp1 to exp2 by exp3 in order ) exp4 :: :: for {{ com loop }}
+ | foreach ( id from exp1 to exp2 by exp3 in order ) exp4 :: :: for {{ com for loop }}
% vectors
| [ exp1 , ... , expn ] :: :: vector {{ com vector (indexed from 0) }}
@@ -703,10 +670,10 @@ grammar
tannot_opt :: 'Typ_annot_opt_' ::=
{{ com optional type annotation for functions}}
- {{ aux _ l }}
+ {{ aux _ l }}
| :: :: none
% Currently not optional; one issue, do the type parameters apply over the argument types, or should this be the type of the function and not just the return
- | typquant typ :: :: some
+ | typquant typ :: :: some
rec_opt :: 'Rec_' ::=
{{ com optional recursive annotation for functions }}
@@ -741,13 +708,9 @@ fundef :: 'FD_' ::=
{{ com function definition}}
{{ aux _ annot }} {{ auxparam 'a }}
| function rec_opt tannot_opt effect_opt funcl1 and ... and funcln :: :: function {{ texlong }}
-% {{ com function definition }}
-% TODO note that the typ in the tannot_opt is the *result* type, not
-% the type of the whole function. The argument type comes from the
-% pattern in the funcl
-% TODO the above is ok for single functions, but not for mutually
-% recursive functions - the tannot_opt scopes over all the funcli,
-% which is ok for the typ_quant part but not for the typ part
+% Note that the typ in the tannot_opt is
+% the *result* type, not the type of the whole function. The argument
+% type comes from the pattern in the funcl
mpat :: 'MP_' ::=
{{ com Mapping pattern. Mostly the same as normal patterns but only constructible parts }}
@@ -755,7 +718,6 @@ mpat :: 'MP_' ::=
| lit :: :: lit
| id :: :: id
| id ( mpat1 , ... , mpatn ) :: :: app
- | { mfpat1 ; ... ; mfpatn semi_opt } :: :: record
| [ mpat1 , ... , mpatn ] :: :: vector
| mpat1 @ ... @ mpatn :: :: vector_concat
| ( mpat1 , ... , mpatn ) :: :: tup
diff --git a/src/ast_util.ml b/src/ast_util.ml
index ac3c6d2b..4c6a583b 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -593,7 +593,6 @@ and map_pat_annot_aux f = function
| P_id id -> P_id id
| 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)
| P_list pats -> P_list (List.map (map_pat_annot f) pats)
| P_vector_concat pats -> P_vector_concat (List.map (map_pat_annot f) pats)
@@ -619,7 +618,6 @@ and map_mpat_annot_aux f = function
| MP_lit lit -> MP_lit lit
| MP_id id -> MP_id id
| MP_app (id, mpats) -> MP_app (id, List.map (map_mpat_annot f) mpats)
- | MP_record (fmpats, b) -> MP_record (List.map (map_mfpat_annot f) fmpats, b)
| MP_tup mpats -> MP_tup (List.map (map_mpat_annot f) mpats)
| MP_list mpats -> MP_list (List.map (map_mpat_annot f) mpats)
| MP_vector_concat mpats -> MP_vector_concat (List.map (map_mpat_annot f) mpats)
@@ -629,8 +627,6 @@ and map_mpat_annot_aux f = function
| 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)
and map_letbind_annot f (LB_aux (lb, annot)) = LB_aux (map_letbind_annot_aux f lb, f annot)
and map_letbind_annot_aux f = function
| LB_val (pat, exp) -> LB_val (map_pat_annot f pat, map_exp_annot f exp)
@@ -998,7 +994,6 @@ and string_of_pat (P_aux (pat, l)) =
| P_as (pat, id) -> "(" ^ string_of_pat pat ^ " as " ^ string_of_id id ^ ")"
| P_string_append [] -> "\"\""
| P_string_append pats -> string_of_list " ^ " string_of_pat pats
- | P_record _ -> "PAT"
and string_of_mpat (MP_aux (pat, l)) =
match pat with
@@ -1013,7 +1008,6 @@ and string_of_mpat (MP_aux (pat, l)) =
| 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, _)) =
match lexp with
@@ -1051,13 +1045,9 @@ let rec pat_ids (P_aux (pat_aux, _)) =
List.fold_right IdSet.union (List.map pat_ids pats) IdSet.empty
| P_cons (pat1, pat2) ->
IdSet.union (pat_ids pat1) (pat_ids pat2)
- | P_record (fpats, _) ->
- List.fold_right IdSet.union (List.map fpat_ids fpats) IdSet.empty
| P_string_append pats ->
List.fold_right IdSet.union (List.map pat_ids pats) IdSet.empty
-and fpat_ids (FP_aux (FP_Fpat (_, pat), _)) = pat_ids pat
-
let id_of_fundef (FD_aux (FD_function (_, _, _, funcls), (l, _))) =
match (List.fold_right
(fun (FCL_aux (FCL_Funcl (id, _), _)) id' ->
@@ -1770,7 +1760,6 @@ let rec locate_pat : 'a. (l -> l) -> 'a pat -> 'a pat = fun f (P_aux (p_aux, (l,
| P_id id -> P_id (locate_id f id)
| P_var (pat, typ_pat) -> P_var (locate_pat f pat, locate_typ_pat f typ_pat)
| P_app (id, pats) -> P_app (locate_id f id, List.map (locate_pat f) pats)
- | P_record (fpats, semi) -> P_record (List.map (locate_fpat f) fpats, semi)
| P_vector pats -> P_vector (List.map (locate_pat f) pats)
| P_vector_concat pats -> P_vector_concat (List.map (locate_pat f) pats)
| P_tup pats -> P_tup (List.map (locate_pat f) pats)
@@ -1780,9 +1769,6 @@ let rec locate_pat : 'a. (l -> l) -> 'a pat -> 'a pat = fun f (P_aux (p_aux, (l,
in
P_aux (p_aux, (f l, annot))
-and locate_fpat : 'a. (l -> l) -> 'a fpat -> 'a fpat = fun f (FP_aux (FP_Fpat (id, pat), (l, annot))) ->
- FP_aux (FP_Fpat (locate_id f id, locate_pat f pat), (f l, annot))
-
let rec locate : 'a. (l -> l) -> 'a exp -> 'a exp = fun f (E_aux (e_aux, (l, annot))) ->
let e_aux = match e_aux with
| E_block exps -> E_block (List.map (locate f) exps)
diff --git a/src/ast_util.mli b/src/ast_util.mli
index ee8fdf13..f6bf1fcc 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -343,7 +343,6 @@ val map_pexp_annot : ('a annot -> 'b annot) -> 'a pexp -> 'b pexp
val map_lexp_annot : ('a annot -> 'b annot) -> 'a lexp -> 'b lexp
val map_letbind_annot : ('a annot -> 'b annot) -> 'a letbind -> 'b letbind
val map_mpat_annot : ('a annot -> 'b annot) -> 'a mpat -> 'b mpat
-val map_mfpat_annot : ('a annot -> 'b annot) -> 'a mfpat -> 'b mfpat
val map_mpexp_annot : ('a annot -> 'b annot) -> 'a mpexp -> 'b mpexp
val map_mapcl_annot : ('a annot -> 'b annot) -> 'a mapcl -> 'b mapcl
diff --git a/src/initial_check.ml b/src/initial_check.ml
index ec3e1f24..1aebdbc2 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -338,11 +338,6 @@ let rec to_ast_pat ctx (P.P_aux (pat, l)) =
if List.length pats == 1 && string_of_parse_id id = "~"
then P_not (to_ast_pat ctx (List.hd pats))
else P_app (to_ast_id id, List.map (to_ast_pat ctx) pats)
- | P.P_record(fpats,_) ->
- P_record(List.map
- (fun (P.FP_aux(P.FP_Fpat(id,fp),l)) ->
- FP_aux(FP_Fpat(to_ast_id id, to_ast_pat ctx fp),(l,())))
- fpats, false)
| P.P_vector(pats) -> P_vector(List.map (to_ast_pat ctx) pats)
| P.P_vector_concat(pats) -> P_vector_concat(List.map (to_ast_pat ctx) pats)
| P.P_tup(pats) -> P_tup(List.map (to_ast_pat ctx) pats)
@@ -691,11 +686,6 @@ let rec to_ast_mpat ctx (P.MP_aux(mpat,l)) =
if mpats = []
then MP_id (to_ast_id id)
else MP_app(to_ast_id id, List.map (to_ast_mpat ctx) mpats)
- | P.MP_record(mfpats,_) ->
- MP_record(List.map
- (fun (P.MFP_aux(P.MFP_mpat(id,mfp),l)) ->
- MFP_aux(MFP_mpat(to_ast_id id, to_ast_mpat ctx mfp),(l,())))
- mfpats, false)
| P.MP_vector(mpats) -> MP_vector(List.map (to_ast_mpat ctx) mpats)
| P.MP_vector_concat(mpats) -> MP_vector_concat(List.map (to_ast_mpat ctx) mpats)
| P.MP_tup(mpats) -> MP_tup(List.map (to_ast_mpat ctx) mpats)
diff --git a/src/interpreter.ml b/src/interpreter.ml
index a2cc17bf..6707bc0b 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -714,7 +714,6 @@ and pattern_match env (P_aux (p_aux, (l, _)) as pat) value =
List.for_all fst matches, List.fold_left (Bindings.merge combine) Bindings.empty (List.map snd matches)
else
false, Bindings.empty
- | P_record _ -> assert false (* TODO *)
| P_vector pats ->
let matches = List.map2 (pattern_match env) pats (coerce_gv value) in
List.for_all fst matches, List.fold_left (Bindings.merge combine) Bindings.empty (List.map snd matches)
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 993cc4f5..bd36c262 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -475,9 +475,6 @@ let rec freshen_pat_bindings p =
| P_app (id,args) ->
let args',vs = List.split (List.map aux args) in
mkp (P_app (id,args')),List.concat vs
- | P_record (fpats,flag) ->
- let fpats,vs = List.split (List.map auxr fpats) in
- mkp (P_record (fpats,flag)),List.concat vs
| P_vector ps ->
let ps,vs = List.split (List.map aux ps) in
mkp (P_vector ps),List.concat vs
@@ -497,9 +494,6 @@ let rec freshen_pat_bindings p =
let p1,vs1 = aux p1 in
let p2,vs2 = aux p2 in
mkp (P_cons (p1, p2)), vs1@vs2
- and auxr (FP_aux (FP_Fpat (id,p),(l,annot))) =
- let p,vs = aux p in
- FP_aux (FP_Fpat (id, p),(Generated l,annot)), vs
in aux p
(* This cuts off function bodies at false assertions that we may have produced
@@ -795,11 +789,7 @@ let split_defs target all_errors splits env defs =
(* Todo: I am not proud of this abuse of relist - but creating a special
* version of re just for two entries did not seem worth it
*)
- relist f (fun [p1'; p2'] -> ctx p1' p2') [p1; p2]
- in
- let fpat (FP_aux ((FP_Fpat (id,p),annot))) =
- optmap (spl p)
- (fun ps -> List.map (fun (p,sub,pchoices,ksub) -> FP_aux (FP_Fpat (id,p), annot), sub, pchoices, ksub) ps)
+ relist f (function [p1'; p2'] -> ctx p1' p2' | _ -> assert false) [p1; p2]
in
match p with
| P_lit _
@@ -876,8 +866,6 @@ let split_defs target all_errors splits env defs =
)
| P_app (id,ps) ->
relist spl (fun ps -> P_app (id,ps)) ps
- | P_record (fps,flag) ->
- relist fpat (fun fps -> P_record (fps,flag)) fps
| P_vector ps ->
relist spl (fun ps -> P_vector ps) ps
| P_vector_concat ps ->
@@ -1528,17 +1516,12 @@ let rec pat_eq (P_aux (p1,_)) (P_aux (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) ->
- flag1 == flag2 && forall2 fpat_eq fpats1 fpats2
| P_vector ps1, P_vector ps2
| P_vector_concat ps1, P_vector_concat ps2
| P_tup ps1, P_tup ps2
| P_list ps1, P_list ps2 -> List.for_all2 pat_eq ps1 ps2
| P_cons (p1',p1''), P_cons (p2',p2'') -> pat_eq p1' p2' && pat_eq p1'' p2''
| _,_ -> false
-and fpat_eq (FP_aux (FP_Fpat (id1,p1),_)) (FP_aux (FP_Fpat (id2,p2),_)) =
- Id.compare id1 id2 == 0 && pat_eq p1 p2
-
module Analysis =
@@ -2023,6 +2006,8 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
let env = add_arg_only_kids env typ_env typ new_deps in
let t_deps, t_r, t_env = aux env (t,typs) in
new_deps::t_deps, merge new_r t_r, t_env
+ | _ :: _, [] ->
+ Reporting.unreachable l __POS__ "Argument and type list in non_det_args had different lengths"
in
let deps, r, env = aux env (es,typs) in
(deps, assigns, r, env)
@@ -2412,7 +2397,6 @@ let initial_env fn_id fn_l (TypQ_aux (tq,_)) pat body set_assertions globals =
kids kids in
s,v,KidSet.fold (fun kid k -> KBindings.add kid (Have (s, ExtraSplits.empty)) k) kids k
| P_app (_,pats) -> of_list pats
- | P_record (fpats,_) -> of_list (List.map (fun (FP_aux (FP_Fpat (_,p),_)) -> p) fpats)
| P_vector pats
| P_vector_concat pats
| P_string_append pats
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 1d2c3534..3147b7f4 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -218,7 +218,6 @@ pat_aux = (* Pattern *)
| P_id of id (* identifier *)
| P_var of pat * atyp (* bind pat to type variable *)
| P_app of id * (pat) list (* union constructor pattern *)
- | P_record of (fpat) list * bool (* struct pattern *)
| P_vector of (pat) list (* vector pattern *)
| P_vector_concat of (pat) list (* concatenated vector pattern *)
| P_tup of (pat) list (* tuple pattern *)
@@ -392,7 +391,6 @@ type mpat_aux = (* Mapping pattern. Mostly the same as normal patterns but only
| MP_lit of lit
| MP_id of id
| MP_app of id * ( mpat) list
- | MP_record of ( mfpat) list * bool
| MP_vector of ( mpat) list
| MP_vector_concat of ( mpat) list
| MP_tup of ( mpat) list
@@ -405,12 +403,6 @@ type mpat_aux = (* Mapping pattern. Mostly the same as normal patterns but only
and mpat =
| MP_aux of ( mpat_aux) * l
-and mfpat_aux = (* Mapping field pattern, why does this have to exist *)
- | MFP_mpat of id * mpat
-
-and mfpat =
- | MFP_aux of mfpat_aux * l
-
type mpexp_aux =
| MPat_pat of ( mpat)
| MPat_when of ( mpat) * ( exp)
diff --git a/src/parser.mly b/src/parser.mly
index 4bc2e5c5..0b09468c 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -674,8 +674,6 @@ pat_string_append:
pat1:
| atomic_pat
{ $1 }
- (* | atomic_pat Bar pat1
- { mk_pat (P_or ($1, $3)) $startpos $endpos } *)
| atomic_pat At pat_concat
{ mk_pat (P_vector_concat ($1 :: $3)) $startpos $endpos }
| atomic_pat ColonColon pat1
diff --git a/src/pattern_completeness.ml b/src/pattern_completeness.ml
index 3de0058f..afda3e1a 100644
--- a/src/pattern_completeness.ml
+++ b/src/pattern_completeness.ml
@@ -68,7 +68,6 @@ type gpat =
| GP_cons of gpat * gpat
| GP_or of gpat * gpat
| GP_app of (gpat Bindings.t)
- | GP_record of (gpat Bindings.t)
| GP_string_append of gpat list
let rec string_of_gpat = function
@@ -82,7 +81,6 @@ let rec string_of_gpat = function
| GP_or (gpat1, gpat2) -> string_of_gpat gpat1 ^ " | " ^ string_of_gpat gpat2
| GP_app app ->
Util.string_of_list "|" (fun (id, gpat) -> string_of_id id ^ string_of_gpat gpat) (Bindings.bindings app)
- | GP_record _ -> "GP RECORD"
| GP_string_append gpats -> Util.string_of_list " ^^ " string_of_gpat gpats
let is_wild = function
@@ -135,15 +133,6 @@ let rec generalize ctx (P_aux (p_aux, (l, _)) as pat) =
GP_app (Bindings.singleton f GP_wild)
else
GP_app (Bindings.singleton f (GP_tup gpats))
- | P_record (fpats, flag) ->
- let gfpats = List.concat (List.map (generalize_fpat ctx) fpats) in
- GP_record (List.fold_left (fun m (fid, gpat) -> Bindings.add fid gpat m) Bindings.empty gfpats)
-
-and generalize_fpat ctx (FP_aux (FP_Fpat (field_id, pat), annot)) =
- let gpat = generalize ctx pat in
- if is_wild gpat then []
- else
- [(field_id, gpat)]
let vector_pat bits =
let bit_pat = function
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 5e8c7145..3d50d48c 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1150,7 +1150,6 @@ let rec doc_pat ctxt apat_needed exists_as_pairs (P_aux (p,(l,annot)) as pat, ty
"string append pattern found in Coq backend, should have been rewritten"
| P_not _ -> unreachable l __POS__ "Coq backend doesn't support not patterns"
| P_or _ -> unreachable l __POS__ "Coq backend doesn't support or patterns yet"
- | P_record (_,_) -> empty (* TODO *)
let contains_early_return exp =
let e_app (f, args) =
@@ -1329,7 +1328,6 @@ let merge_new_tyvars ctxt old_env pat new_env =
| P_list ps
| P_string_append ps
-> List.fold_left merge_pat m ps
- | P_record (fps,_) -> unreachable l __POS__ "Coq backend doesn't support record patterns properly yet"
| P_cons (p1,p2) -> merge_pat (merge_pat m p1) p2
in
let m,r = IdSet.fold remove_binding (pat_ids pat) (ctxt.kid_id_renames, ctxt.kid_id_renames_rev) in
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 1367d9eb..d399ec29 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -549,6 +549,7 @@ let rec doc_pat_lem ctxt apat_needed (P_aux (p,(l,annot)) as pa) = match p with
| P_cons (p,p') -> doc_op (string "::") (doc_pat_lem ctxt true p) (doc_pat_lem ctxt true p')
| P_string_append _ -> unreachable l __POS__ "Lem doesn't support string append patterns"
| P_not _ -> unreachable l __POS__ "Lem doesn't support not patterns"
+ | P_or _ -> unreachable l __POS__ "Lem doesn't support or patterns"
let rec typ_needs_printed (Typ_aux (t,_) as typ) = match t with
| Typ_tup ts -> List.exists typ_needs_printed ts
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 5dbb6cd5..b3675263 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -345,7 +345,6 @@ let rec doc_pat (P_aux (p_aux, (l, _)) as pat) =
| P_string_append [] -> string "\"\""
| P_string_append pats ->
parens (separate_map (string " ^ ") doc_pat pats)
- | P_record _ -> raise (Reporting.err_unreachable l __POS__ "P_record passed to doc_pat")
(* if_block_x is true if x should be printed like a block, i.e. with
newlines. Blocks are automatically printed as blocks, so this
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 24261861..62870083 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -63,7 +63,6 @@ type 'a rewriters = {
rewrite_defs : 'a rewriters -> 'a defs -> 'a defs;
}
-let effect_of_fpat (FP_aux (_,(_,a))) = effect_of_annot a
let effect_of_lexp (LEXP_aux (_,(_,a))) = effect_of_annot a
let effect_of_fexp (FE_aux (_,(_,a))) = effect_of_annot a
let effect_of_fexps fexps =
@@ -255,9 +254,6 @@ let rewrite_pat rewriters (P_aux (pat,(l,annot)) as orig_pat) =
| P_as(pat,id) -> rewrap (P_as(rewrite pat, id))
| P_typ(typ,pat) -> rewrap (P_typ(typ, rewrite pat))
| P_app(id ,pats) -> rewrap (P_app(id, List.map rewrite pats))
- | P_record(fpats,_) ->
- rewrap (P_record(List.map (fun (FP_aux(FP_Fpat(id,pat),pannot)) -> FP_aux(FP_Fpat(id, rewrite pat), pannot)) fpats,
- false))
| P_vector pats -> rewrap (P_vector(List.map rewrite pats))
| P_vector_concat pats -> rewrap (P_vector_concat (List.map rewrite pats))
| P_tup pats -> rewrap (P_tup (List.map rewrite pats))
@@ -442,7 +438,7 @@ let rewrite_defs_base_parallel j rewriters (Defs defs) =
exit 1
done;
Defs (List.concat !rewritten)
-
+
let rewriters_base =
{rewrite_exp = rewrite_exp;
rewrite_pat = rewrite_pat;
@@ -454,7 +450,7 @@ let rewriters_base =
let rewrite_defs (Defs defs) = rewrite_defs_base rewriters_base (Defs defs)
-type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
+type ('a,'pat,'pat_aux) pat_alg =
{ p_lit : lit -> 'pat_aux
; p_wild : 'pat_aux
; p_or : 'pat * 'pat -> 'pat_aux
@@ -464,7 +460,6 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
; p_id : id -> '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
; p_vector_concat : 'pat list -> 'pat_aux
; p_tup : 'pat list -> 'pat_aux
@@ -472,11 +467,9 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
; p_cons : 'pat * 'pat -> 'pat_aux
; p_string_append : 'pat list -> 'pat_aux
; p_aux : 'pat_aux * 'a annot -> 'pat
- ; fP_aux : 'fpat_aux * 'a annot -> 'fpat
- ; fP_Fpat : id * 'pat -> 'fpat_aux
}
-let rec fold_pat_aux (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat_aux -> 'pat_aux =
+let rec fold_pat_aux (alg : ('a,'pat,'pat_aux) pat_alg) : 'a pat_aux -> 'pat_aux =
function
| P_lit lit -> alg.p_lit lit
| P_wild -> alg.p_wild
@@ -487,7 +480,6 @@ let rec fold_pat_aux (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat
| 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)
- | P_record (ps,b) -> alg.p_record (List.map (fold_fpat alg) ps, b)
| P_vector ps -> alg.p_vector (List.map (fold_pat alg) ps)
| P_vector_concat ps -> alg.p_vector_concat (List.map (fold_pat alg) ps)
| P_tup ps -> alg.p_tup (List.map (fold_pat alg) ps)
@@ -495,18 +487,12 @@ let rec fold_pat_aux (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat
| P_cons (ph,pt) -> alg.p_cons (fold_pat alg ph, fold_pat alg pt)
| P_string_append ps -> alg.p_string_append (List.map (fold_pat alg) ps)
-and fold_pat (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat -> 'pat =
+and fold_pat (alg : ('a,'pat,'pat_aux) pat_alg) : 'a pat -> 'pat =
function
| P_aux (pat,annot) -> alg.p_aux (fold_pat_aux alg pat,annot)
-and fold_fpat_aux (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a fpat_aux -> 'fpat_aux =
- function
- | FP_Fpat (id,pat) -> alg.fP_Fpat (id,fold_pat alg pat)
-and fold_fpat (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a fpat -> 'fpat =
- function
- | FP_aux (fpat,annot) -> alg.fP_aux (fold_fpat_aux alg fpat,annot)
(* identity fold from term alg to term alg *)
-let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg =
+let id_pat_alg : ('a,'a pat, 'a pat_aux) pat_alg =
{ p_lit = (fun lit -> P_lit lit)
; p_wild = P_wild
; p_or = (fun (pat1, pat2) -> P_or(pat1, pat2))
@@ -516,7 +502,6 @@ let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg =
; p_id = (fun id -> P_id id)
; 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)
; p_vector_concat = (fun ps -> P_vector_concat ps)
; p_tup = (fun ps -> P_tup ps)
@@ -524,13 +509,11 @@ let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg =
; p_cons = (fun (ph,pt) -> P_cons (ph,pt))
; p_string_append = (fun (ps) -> P_string_append (ps))
; p_aux = (fun (pat,annot) -> P_aux (pat,annot))
- ; fP_aux = (fun (fpat,annot) -> FP_aux (fpat,annot))
- ; fP_Fpat = (fun (id,pat) -> FP_Fpat (id,pat))
}
type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
- 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg =
+ 'pat,'pat_aux) exp_alg =
{ e_block : 'exp list -> 'exp_aux
; e_id : id -> 'exp_aux
; e_ref : id -> 'exp_aux
@@ -588,7 +571,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
; pat_aux : 'pexp_aux * 'a annot -> 'pexp
; lB_val : 'pat * 'exp -> 'letbind_aux
; lB_aux : 'letbind_aux * 'a annot -> 'letbind
- ; pat_alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg
+ ; pat_alg : ('a,'pat,'pat_aux) pat_alg
}
let rec fold_exp_aux alg = function
@@ -755,7 +738,6 @@ let compute_pat_alg bot join =
; p_id = (fun id -> (bot, P_id id))
; p_var = (fun ((v,pat),kid) -> (v, P_var (pat,kid)))
; p_app = (fun (id,ps) -> split_join (fun ps -> P_app (id,ps)) ps)
- ; p_record = (fun (ps,b) -> split_join (fun ps -> P_record (ps,b)) ps)
; p_vector = split_join (fun ps -> P_vector ps)
; p_vector_concat = split_join (fun ps -> P_vector_concat ps)
; p_tup = split_join (fun ps -> P_tup ps)
@@ -763,8 +745,6 @@ let compute_pat_alg bot join =
; p_cons = (fun ((vh,ph),(vt,pt)) -> (join vh vt, P_cons (ph,pt)))
; p_string_append = split_join (fun ps -> P_string_append ps)
; p_aux = (fun ((v,pat),annot) -> (v, P_aux (pat,annot)))
- ; fP_aux = (fun ((v,fpat),annot) -> (v, FP_aux (fpat,annot)))
- ; fP_Fpat = (fun (id,(v,pat)) -> (v, FP_Fpat (id,pat)))
}
let compute_exp_alg bot join =
@@ -862,7 +842,6 @@ let pure_pat_alg bot join =
; p_id = (fun id -> bot)
; p_var = (fun (v,kid) -> v)
; p_app = (fun (id,ps) -> join_list ps)
- ; p_record = (fun (ps,b) -> join_list ps)
; p_vector = join_list
; p_vector_concat = join_list
; p_tup = join_list
@@ -870,8 +849,6 @@ let pure_pat_alg bot join =
; p_string_append = join_list
; p_cons = (fun (vh,vt) -> join vh vt)
; p_aux = (fun (v,annot) -> v)
- ; fP_aux = (fun (v,annot) -> v)
- ; fP_Fpat = (fun (id,v) -> v)
}
let pure_exp_alg bot join =
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 77974f86..85f00453 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -90,7 +90,7 @@ val rewrite_def : tannot rewriters -> tannot def -> tannot def
val rewrite_fun : tannot rewriters -> tannot fundef -> tannot fundef
(* the type of interpretations of pattern-matching expressions *)
-type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
+type ('a,'pat,'pat_aux) pat_alg =
{ p_lit : lit -> 'pat_aux
; p_wild : 'pat_aux
; p_or : 'pat * 'pat -> 'pat_aux
@@ -100,7 +100,6 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
; p_id : id -> '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
; p_vector_concat : 'pat list -> 'pat_aux
; p_tup : 'pat list -> 'pat_aux
@@ -108,15 +107,13 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
; p_cons : 'pat * 'pat -> 'pat_aux
; p_string_append : 'pat list -> 'pat_aux
; p_aux : 'pat_aux * 'a annot -> 'pat
- ; fP_aux : 'fpat_aux * 'a annot -> 'fpat
- ; fP_Fpat : id * 'pat -> 'fpat_aux
}
(* fold over pat_aux expressions *)
(* the type of interpretations of expressions *)
type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
- 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg =
+ 'pat,'pat_aux) exp_alg =
{ e_block : 'exp list -> 'exp_aux
; e_id : id -> 'exp_aux
; e_ref : id -> 'exp_aux
@@ -174,63 +171,63 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
; pat_aux : 'pexp_aux * 'a annot -> 'pexp
; lB_val : 'pat * 'exp -> 'letbind_aux
; lB_aux : 'letbind_aux * 'a annot -> 'letbind
- ; pat_alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg
+ ; pat_alg : ('a,'pat,'pat_aux) pat_alg
}
(* fold over patterns *)
-val fold_pat : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg -> 'a pat -> 'pat
+val fold_pat : ('a,'pat,'pat_aux) pat_alg -> 'a pat -> 'pat
(* fold over expressions *)
val fold_exp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
- 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a exp -> 'exp
+ 'pat,'pat_aux) exp_alg -> 'a exp -> 'exp
val fold_letbind : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
- 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a letbind -> 'letbind
+ 'pat,'pat_aux) exp_alg -> 'a letbind -> 'letbind
val fold_pexp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
- 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a pexp -> 'pexp
+ 'pat,'pat_aux) exp_alg -> 'a pexp -> 'pexp
val fold_pexp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
- 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a pexp -> 'pexp
+ 'pat,'pat_aux) exp_alg -> 'a pexp -> 'pexp
val fold_funcl : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
'opt_default_aux,'opt_default,'a pexp,'pexp_aux,'letbind_aux,'letbind,
- 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a funcl -> 'a funcl
+ 'pat,'pat_aux) exp_alg -> 'a funcl -> 'a funcl
val fold_function : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
'opt_default_aux,'opt_default, 'a pexp,'pexp_aux,'letbind_aux,'letbind,
- 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a fundef -> 'a fundef
+ 'pat,'pat_aux) exp_alg -> 'a fundef -> 'a fundef
-val id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg
+val id_pat_alg : ('a,'a pat, 'a pat_aux) pat_alg
val id_exp_alg :
('a,'a exp,'a exp_aux,'a lexp,'a lexp_aux,'a fexp,
'a fexp_aux,
'a opt_default_aux,'a opt_default,'a pexp,'a pexp_aux,
'a letbind_aux,'a letbind,
- 'a pat,'a pat_aux,'a fpat,'a fpat_aux) exp_alg
+ 'a pat,'a pat_aux) exp_alg
val compute_pat_alg : 'b -> ('b -> 'b -> 'b) ->
- ('a,('b * 'a pat),('b * 'a pat_aux),('b * 'a fpat),('b * 'a fpat_aux)) pat_alg
+ ('a,('b * 'a pat),('b * 'a pat_aux)) pat_alg
val compute_exp_alg : 'b -> ('b -> 'b -> 'b) ->
('a,('b * 'a exp),('b * 'a exp_aux),('b * 'a lexp),('b * 'a lexp_aux),('b * 'a fexp),
('b * 'a fexp_aux),
('b * 'a opt_default_aux),('b * 'a opt_default),('b * 'a pexp),('b * 'a pexp_aux),
('b * 'a letbind_aux),('b * 'a letbind),
- ('b * 'a pat),('b * 'a pat_aux),('b * 'a fpat),('b * 'a fpat_aux)) exp_alg
+ ('b * 'a pat),('b * 'a pat_aux)) exp_alg
-val pure_pat_alg : 'b -> ('b -> 'b -> 'b) -> ('a,'b,'b,'b,'b) pat_alg
+val pure_pat_alg : 'b -> ('b -> 'b -> 'b) -> ('a,'b,'b) pat_alg
val pure_exp_alg : 'b -> ('b -> 'b -> 'b) ->
('a,'b,'b,'b,'b,'b,
'b,'b,'b,
'b,'b,
'b,'b,
- 'b,'b,'b,'b) exp_alg
+ 'b,'b) exp_alg
val simple_annot : Parse_ast.l -> typ -> Parse_ast.l * tannot
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 87891b6d..89b49043 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -370,7 +370,6 @@ let remove_vector_concat_pat pat =
; p_id = (fun id -> P_id id)
; p_var = (fun (pat,kid) -> P_var (pat true,kid))
; p_app = (fun (id,ps) -> P_app (id, List.map (fun p -> p false) ps))
- ; p_record = (fun (fpats,b) -> P_record (fpats, b))
; p_vector = (fun ps -> P_vector (List.map (fun p -> p false) ps))
; p_vector_concat = (fun ps -> P_vector_concat (List.map (fun p -> p false) ps))
; p_tup = (fun ps -> P_tup (List.map (fun p -> p false) ps))
@@ -386,8 +385,6 @@ let remove_vector_concat_pat pat =
else P_aux (P_as (P_aux (pat,annot),fresh_id_v l),annot))
| _ -> P_aux (pat,annot)
)
- ; fP_aux = (fun (fpat,annot) -> FP_aux (fpat,annot))
- ; fP_Fpat = (fun (id,p) -> FP_Fpat (id,p false))
} in
let pat = (fold_pat name_vector_concat_roots pat) false in
@@ -504,8 +501,6 @@ let remove_vector_concat_pat pat =
; p_var = (fun ((pat,decls),kid) -> (P_var (pat,kid),decls))
; p_app = (fun (id,ps) -> let (ps,decls) = List.split ps in
(P_app (id,ps),List.flatten decls))
- ; p_record = (fun (ps,b) -> let (ps,decls) = List.split ps in
- (P_record (ps,b),List.flatten decls))
; p_vector = (fun ps -> let (ps,decls) = List.split ps in
(P_vector ps,List.flatten decls))
; p_vector_concat = (fun ps -> let (ps,decls) = List.split ps in
@@ -518,8 +513,6 @@ let remove_vector_concat_pat pat =
(P_string_append ps,List.flatten decls))
; p_cons = (fun ((p,decls),(p',decls')) -> (P_cons (p,p'), decls @ decls'))
; p_aux = (fun ((pat,decls),annot) -> p_aux ((pat,decls),annot))
- ; fP_aux = (fun ((fpat,decls),annot) -> (FP_aux (fpat,annot),decls))
- ; fP_Fpat = (fun (id,(pat,decls)) -> (FP_Fpat (id,pat),decls))
} in
let (pat,decls) = fold_pat unname_vector_concat_elements pat in
@@ -697,8 +690,6 @@ let rec is_irrefutable_pattern (P_aux (p,ann)) =
| P_app (f,args) ->
Env.is_singleton_union_constructor f (env_of_annot ann) &&
List.for_all is_irrefutable_pattern args
- | P_record (fps,_) ->
- List.for_all (fun (FP_aux (FP_Fpat (_,p),_)) -> is_irrefutable_pattern p) fps
| P_vector ps
| P_vector_concat ps
| P_tup ps
@@ -749,8 +740,6 @@ let rec subsumes_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) =
| P_wild, _ -> Some []
| P_app (Id_aux (id1,l1),args1), P_app (Id_aux (id2,_),args2) ->
if id1 = id2 then subsumes_list subsumes_pat args1 args2 else None
- | P_record (fps1,b1), P_record (fps2,b2) ->
- if b1 = b2 then subsumes_list subsumes_fpat fps1 fps2 else None
| P_vector pats1, P_vector pats2
| P_vector_concat pats1, P_vector_concat pats2
| P_tup pats1, P_tup pats2
@@ -766,8 +755,6 @@ let rec subsumes_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) =
| _ -> None)
| _, P_wild -> if is_irrefutable_pattern pat1 then Some [] else None
| _ -> None
-and subsumes_fpat (FP_aux (FP_Fpat (id1,pat1),_)) (FP_aux (FP_Fpat (id2,pat2),_)) =
- if id1 = id2 then subsumes_pat pat1 pat2 else None
(* A simple check for pattern disjointness; used for optimisation in the
guarded pattern rewrite step *)
@@ -817,8 +804,6 @@ let rec pat_to_exp ((P_aux (pat,(l,annot))) as p_aux) =
| P_typ (_,pat) -> pat_to_exp pat
| P_id id -> rewrap (E_id id)
| P_app (id,pats) -> rewrap (E_app (id, List.map pat_to_exp pats))
- | P_record (fpats,b) ->
- rewrap (E_record (List.map fpat_to_fexp fpats))
| P_vector pats -> rewrap (E_vector (List.map pat_to_exp pats))
| P_vector_concat pats -> begin
let empty_vec = E_aux (E_vector [], (l,())) in
@@ -838,9 +823,6 @@ let rec pat_to_exp ((P_aux (pat,(l,annot))) as p_aux) =
(List.fold_right string_append (List.map pat_to_exp pats) empty_string)
end
-and fpat_to_fexp (FP_aux (FP_Fpat (id,pat),(l,annot))) =
- FE_aux (FE_Fexp (id, pat_to_exp pat),(l,annot))
-
let case_exp e t cs =
let l = get_loc_exp e in
let env = env_of e in
@@ -974,8 +956,6 @@ let rec contains_bitvector_pat (P_aux (pat,annot)) = match pat with
List.exists contains_bitvector_pat pats
| P_cons (p,ps) -> contains_bitvector_pat p || contains_bitvector_pat ps
| P_string_append (ps) -> List.exists contains_bitvector_pat ps
-| P_record (fpats,_) ->
- List.exists (fun (FP_aux (FP_Fpat (_,pat),_)) -> contains_bitvector_pat pat) fpats
let contains_bitvector_pexp = function
| Pat_aux (Pat_exp (pat,_),_) | Pat_aux (Pat_when (pat,_,_),_) ->
@@ -1001,7 +981,6 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
; p_id = (fun id -> P_id id)
; p_var = (fun (pat,kid) -> P_var (pat true,kid))
; p_app = (fun (id,ps) -> P_app (id, List.map (fun p -> p false) ps))
- ; p_record = (fun (fpats,b) -> P_record (fpats, b))
; p_vector = (fun ps -> P_vector (List.map (fun p -> p false) ps))
; p_vector_concat = (fun ps -> P_vector_concat (List.map (fun p -> p false) ps))
; p_string_append = (fun ps -> P_string_append (List.map (fun p -> p false) ps))
@@ -1018,8 +997,6 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
P_aux (P_as (P_aux (pat,annot),fresh_id "b__" l), annot)
| _ -> P_aux (pat,annot)
)
- ; fP_aux = (fun (fpat,annot) -> FP_aux (fpat,annot))
- ; fP_Fpat = (fun (id,p) -> FP_Fpat (id,p false))
} in
let pat, env = bind_pat_no_guard env
(strip_pat ((fold_pat name_bitvector_roots pat) false))
@@ -1153,8 +1130,6 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
; p_var = (fun ((pat,gdls),kid) -> (P_var (pat,kid), gdls))
; p_app = (fun (id,ps) -> let (ps,gdls) = List.split ps in
(P_app (id,ps), flatten_guards_decls gdls))
- ; p_record = (fun (ps,b) -> let (ps,gdls) = List.split ps in
- (P_record (ps,b), flatten_guards_decls gdls))
; p_vector = (fun ps -> let (ps,gdls) = List.split ps in
(P_vector ps, flatten_guards_decls gdls))
; p_vector_concat = (fun ps -> let (ps,gdls) = List.split ps in
@@ -1174,8 +1149,6 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
| P_as (P_aux (P_vector ps, _), id), true ->
(P_aux (P_id id, annot), collect_guards_decls ps id t)
| _, _ -> (P_aux (pat,annot), gdls)))
- ; fP_aux = (fun ((fpat,gdls),annot) -> (FP_aux (fpat,annot), gdls))
- ; fP_Fpat = (fun (id,(pat,gdls)) -> (FP_Fpat (id,pat), gdls))
} in
fold_pat guard_bitvector_pat pat
@@ -2657,7 +2630,6 @@ let rec bindings_of_pat (P_aux (p_aux, p_annot) as pat) =
match p_aux with
| P_lit _ | P_wild -> []
| P_id id -> [pat]
- | P_record _ -> failwith "record patterns not yet implemented"
(* we assume the type-checker has already checked the two sides have the same bindings *)
| P_or (left, right) -> bindings_of_pat left
| P_as (p, id) -> [annot_pat (P_id id) unk (env_of_pat p) (typ_of_pat p)]
@@ -2677,7 +2649,6 @@ let rec binding_typs_of_pat (P_aux (p_aux, p_annot) as pat) =
match p_aux with
| P_lit _ | P_wild -> []
| P_id id -> [typ_of_pat pat]
- | P_record _ -> failwith "record patterns not yet implemented"
(* we assume the type-checker has already checked the two sides have the same bindings *)
| P_or (left, right) -> binding_typs_of_pat left
| P_as (p, id) -> [typ_of_pat p]
@@ -3093,8 +3064,6 @@ let rec rewrite_defs_pat_string_append env =
| P_aux (P_var (inner_pat, typ_pat), p_annot) ->
let inner_pat, guards, expr = rewrite_pat env (inner_pat, guards, expr) in
P_aux (P_var (inner_pat, typ_pat), p_annot), guards, expr
- | P_aux (P_record _, p_annot) ->
- failwith "record patterns not yet implemented"
| P_aux (P_vector pats, p_annot) ->
let pats = List.map folder pats in
P_aux (P_vector pats, p_annot), !guards_ref, !expr_ref
@@ -3235,8 +3204,6 @@ let rewrite_defs_mapping_patterns env =
| P_aux (P_var (inner_pat, typ_pat), p_annot) ->
let inner_pat, guards, expr = rewrite_pat env (inner_pat, guards, expr) in
P_aux (P_var (inner_pat, typ_pat), p_annot), guards, expr
- | P_aux (P_record _, p_annot) ->
- failwith "record patterns not yet implemented"
| P_aux (P_vector pats, p_annot) ->
let pats = List.map folder pats in
P_aux (P_vector pats, p_annot), !guards_ref, !expr_ref
@@ -3860,7 +3827,6 @@ let rec exp_of_mpat ((MP_aux (mpat, (l,annot))) as mp_aux) =
| MP_lit lit -> E_aux (E_lit lit, (l,annot))
| MP_id id -> E_aux (E_id id, (l,annot))
| MP_app (id, args) -> E_aux (E_app (id, (List.map exp_of_mpat args)), (l,annot))
- | MP_record (mfpats, flag) -> E_aux (E_record (fexps_of_mfpats mfpats flag (l,annot)), (l,annot))
| MP_vector mpats -> E_aux (E_vector (List.map exp_of_mpat mpats), (l,annot))
| MP_vector_concat mpats -> List.fold_right concat_vectors (List.map (fun m -> strip_exp (exp_of_mpat m)) mpats) empty_vec
| MP_tup mpats -> E_aux (E_tuple (List.map exp_of_mpat mpats), (l,annot))
@@ -3872,19 +3838,11 @@ let rec exp_of_mpat ((MP_aux (mpat, (l,annot))) as mp_aux) =
Pat_aux (Pat_exp (pat_of_mpat mpat, exp_of_mpat mpat), (l,annot))
]), (l,annot)) (* TODO FIXME location information? *)
-
-and fexps_of_mfpats mfpats flag annot =
- let fexp_of_mfpat (MFP_aux (MFP_mpat (id, mpat), annot)) =
- FE_aux (FE_Fexp (id, exp_of_mpat mpat), annot)
- in
- List.map fexp_of_mfpat mfpats
-
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)
| MP_app (id, args) -> P_aux (P_app (id, (List.map pat_of_mpat args)), annot)
- | MP_record (mfpats, flag) -> P_aux (P_record ((fpats_of_mfpats mfpats), flag), annot)
| MP_vector mpats -> P_aux (P_vector (List.map pat_of_mpat mpats), annot)
| MP_vector_concat mpats -> P_aux (P_vector_concat (List.map pat_of_mpat mpats), annot)
| MP_tup mpats -> P_aux (P_tup (List.map pat_of_mpat mpats), annot)
@@ -3894,12 +3852,6 @@ and pat_of_mpat (MP_aux (mpat, 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)) =
- FP_aux (FP_Fpat (id, pat_of_mpat mpat), annot)
- in
- List.map fpat_of_mfpat mfpats
-
let rewrite_defs_realise_mappings _ (Defs defs) =
let realise_mpexps forwards mpexp1 mpexp2 =
let mpexp_pat, mpexp_exp =
@@ -4311,8 +4263,6 @@ let rec remove_clause_from_pattern ctx (P_aux (rm_pat,ann)) res_pat =
let res_pats = subpats [p1;p2] rps in
rp' @ List.map (function [rp1;rp2] -> RP_cons (rp1,rp2) | _ -> assert false) res_pats
end
- | P_record _ ->
- raise (Reporting.err_unreachable (fst ann) __POS__ "Record pattern not supported")
| P_or _ ->
raise (Reporting.err_unreachable (fst ann) __POS__ "Or pattern not supported")
| P_not _ ->
diff --git a/src/slice.ml b/src/slice.ml
index 1bbbca1e..427d5913 100644
--- a/src/slice.ml
+++ b/src/slice.ml
@@ -219,6 +219,7 @@ let add_def_to_graph graph def =
| QI_id _ -> ()
| QI_constraint nc ->
IdSet.iter (fun id -> graph := G.add_edge self (Type id) !graph) (constraint_ids nc)
+ | QI_constant _ -> ()
in
let scan_typquant self (TypQ_aux (aux, _)) =
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 57e415a8..40855eec 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -175,9 +175,6 @@ let rec pat_bindings consider_var bound used (P_aux(p,(_,tannot))) =
| P_app(id,pats) ->
let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
list_fv bound (Nameset.add (string_of_id id) used) pats
- | P_record(fpats,_) ->
- List.fold_right (fun (Ast.FP_aux(Ast.FP_Fpat(_,p),_)) (b,n) ->
- pat_bindings consider_var bound used p) fpats (bound,used)
| P_vector pats | Ast.P_vector_concat pats | Ast.P_tup pats | Ast.P_list pats -> list_fv bound used pats
| _ -> bound,used
@@ -738,12 +735,9 @@ let bindings_from_pat p =
| P_tup ps
| P_list ps
-> List.concat (List.map aux_pat ps)
- | P_record (fps,_) -> List.concat (List.map aux_fpat fps)
| P_cons (p1,p2) -> aux_pat p1 @ aux_pat p2
- and aux_fpat (FP_aux (FP_Fpat (_,p), _)) = aux_pat p
in aux_pat p
-
(* TODO: replace the below with solutions that don't depend so much on the
structure of the environment. *)
@@ -794,15 +788,12 @@ let nexp_subst_fns substs =
| 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))
- | P_record (fps,flag) -> re (P_record (List.map s_fpat fps, flag))
| P_vector ps -> re (P_vector (List.map s_pat ps))
| P_vector_concat ps -> re (P_vector_concat (List.map s_pat ps))
| P_string_append ps -> re (P_string_append (List.map s_pat ps))
| P_tup ps -> re (P_tup (List.map s_pat ps))
| P_list ps -> re (P_list (List.map s_pat ps))
| P_cons (p1,p2) -> re (P_cons (s_pat p1, s_pat p2))
- and s_fpat (FP_aux (FP_Fpat (id, p), (l,annot))) =
- FP_aux (FP_Fpat (id, s_pat p), (l,s_tannot annot))
in
let rec s_exp (E_aux (e,(l,annot))) =
let re e = E_aux (e,(l,s_tannot annot)) in
diff --git a/src/type_check.ml b/src/type_check.ml
index fb98ee1b..819143de 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -4672,7 +4672,9 @@ and propagate_pat_effect_aux = function
| P_vector pats ->
let p_pats = List.map propagate_pat_effect pats in
P_vector p_pats, collect_effects_pat p_pats
+ (*
| _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented: Cannot propagate effect in pat")
+ *)
and propagate_mpat_effect (MP_aux (mpat, annot)) =
let p_mpat, eff = propagate_mpat_effect_aux mpat in
@@ -4708,7 +4710,6 @@ and propagate_mpat_effect_aux = function
| MP_as (mpat, id) ->
let p_mpat = propagate_mpat_effect mpat in
MP_as (p_mpat, id), effect_of_mpat mpat
- | _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented: Cannot propagate effect in mpat")
and propagate_letbind_effect (LB_aux (lb, (l, annot))) =
let p_lb, eff = propagate_letbind_effect_aux lb in
@@ -5019,7 +5020,7 @@ let rec warn_if_unsafe_cast l env = function
| typ when is_bit_typ typ -> ()
| typ ->
Reporting.warn ("Potentially unsafe cast involving " ^ string_of_typ typ) l ""
-
+
(* Checking a val spec simply adds the type as a binding in the
context. We have to destructure the various kinds of val specs, but
the difference is irrelevant for the typechecker. *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 07:58:00 +0000