diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 12 | ||||
| -rw-r--r-- | src/initial_check.ml | 4 | ||||
| -rw-r--r-- | src/parse_ast.ml | 4 | ||||
| -rw-r--r-- | src/parser.mly | 20 | ||||
| -rw-r--r-- | src/pattern_completeness.ml | 11 | ||||
| -rw-r--r-- | src/rewriter.ml | 10 | ||||
| -rw-r--r-- | src/rewriter.mli | 2 | ||||
| -rw-r--r-- | src/rewrites.ml | 37 | ||||
| -rw-r--r-- | src/sail_lib.ml | 2 | ||||
| -rw-r--r-- | src/type_check.ml | 83 |
10 files changed, 108 insertions, 77 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index a766b846..98fc6bde 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -441,7 +441,7 @@ and map_pat_annot_aux f = function | P_vector_concat pats -> P_vector_concat (List.map (map_pat_annot f) pats) | P_vector pats -> P_vector (List.map (map_pat_annot f) pats) | P_cons (pat1, pat2) -> P_cons (map_pat_annot f pat1, map_pat_annot f pat2) - | P_string_append (pat1, pat2) -> P_string_append (map_pat_annot f pat1, map_pat_annot f pat2) + | P_string_append pats -> P_string_append (List.map (map_pat_annot f) pats) and map_mpexp_annot f (MPat_aux (mpexp, annot)) = MPat_aux (map_mpexp_annot_aux f mpexp, f annot) and map_mpexp_annot_aux f = function @@ -462,7 +462,7 @@ and map_mpat_annot_aux f = function | MP_vector_concat mpats -> MP_vector_concat (List.map (map_mpat_annot f) mpats) | MP_vector mpats -> MP_vector (List.map (map_mpat_annot f) mpats) | MP_cons (mpat1, mpat2) -> MP_cons (map_mpat_annot f mpat1, map_mpat_annot f mpat2) - | MP_string_append (mpat1, mpat2) -> MP_string_append (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) and map_fpat_annot f (FP_aux (FP_Fpat (id, pat), annot)) = FP_aux (FP_Fpat (id, map_pat_annot f pat), f annot) @@ -740,7 +740,7 @@ and string_of_pat (P_aux (pat, l)) = | P_vector_concat pats -> string_of_list " : " string_of_pat pats | P_vector pats -> "[" ^ string_of_list ", " string_of_pat pats ^ "]" | P_as (pat, id) -> string_of_pat pat ^ " as " ^ string_of_id id - | P_string_append (pat1, pat2) -> string_of_pat pat1 ^ " ^^ " ^ string_of_pat pat2 + | P_string_append pats -> string_of_list " ^^ " string_of_pat pats | _ -> "PAT" and string_of_mpat (MP_aux (pat, l)) = @@ -753,7 +753,7 @@ and string_of_mpat (MP_aux (pat, l)) = | MP_list pats -> "[||" ^ string_of_list "," string_of_mpat pats ^ "||]" | MP_vector_concat pats -> string_of_list " : " string_of_mpat pats | MP_vector pats -> "[" ^ string_of_list ", " string_of_mpat pats ^ "]" - | MP_string_append (pat1, pat2) -> string_of_mpat pat1 ^ " ^^ " ^ string_of_mpat pat2 + | MP_string_append pats -> string_of_list " ^^ " string_of_mpat pats | MP_typ (mpat, typ) -> "(" ^ string_of_mpat mpat ^ " : " ^ string_of_typ typ ^ ")" | _ -> "MPAT" @@ -791,8 +791,8 @@ let rec pat_ids (P_aux (pat_aux, _)) = 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 (pat1, pat2) -> - IdSet.union (pat_ids pat1) (pat_ids pat2) + | 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 diff --git a/src/initial_check.ml b/src/initial_check.ml index 3f7a7052..5df6b825 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -470,7 +470,7 @@ let rec to_ast_pat (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.P_aux(pa | Parse_ast.P_tup(pats) -> P_tup(List.map (to_ast_pat k_env def_ord) pats) | Parse_ast.P_list(pats) -> P_list(List.map (to_ast_pat k_env def_ord) pats) | Parse_ast.P_cons(pat1, pat2) -> P_cons (to_ast_pat k_env def_ord pat1, to_ast_pat k_env def_ord pat2) - | Parse_ast.P_string_append (pat1, pat2) -> P_string_append (to_ast_pat k_env def_ord pat1, to_ast_pat k_env def_ord pat2) + | Parse_ast.P_string_append pats -> P_string_append (List.map (to_ast_pat k_env def_ord) pats) ), (l,())) @@ -781,7 +781,7 @@ let rec to_ast_mpat k_env def_ord (Parse_ast.MP_aux(mpat,l)) = | Parse_ast.MP_tup(mpats) -> MP_tup(List.map (to_ast_mpat k_env def_ord) mpats) | Parse_ast.MP_list(mpats) -> MP_list(List.map (to_ast_mpat k_env def_ord) mpats) | Parse_ast.MP_cons(pat1, pat2) -> MP_cons (to_ast_mpat k_env def_ord pat1, to_ast_mpat k_env def_ord pat2) - | Parse_ast.MP_string_append (pat1, pat2) -> MP_string_append (to_ast_mpat k_env def_ord pat1, to_ast_mpat k_env def_ord pat2) + | Parse_ast.MP_string_append pats -> MP_string_append (List.map (to_ast_mpat k_env def_ord) pats) | Parse_ast.MP_typ (mpat, typ) -> MP_typ (to_ast_mpat k_env def_ord mpat, to_ast_typ k_env def_ord typ) ), (l,())) diff --git a/src/parse_ast.ml b/src/parse_ast.ml index e59dd356..b34ba1d2 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -252,7 +252,7 @@ pat_aux = (* Pattern *) | P_tup of (pat) list (* tuple pattern *) | P_list of (pat) list (* list pattern *) | P_cons of pat * pat (* cons pattern *) - | P_string_append of pat * pat (* string append pattern, x ^^ y *) + | P_string_append of pat list (* string append pattern, x ^^ y *) and pat = P_aux of pat_aux * l @@ -430,7 +430,7 @@ type mpat_aux = (* Mapping pattern. Mostly the same as normal patterns but only | MP_tup of ( mpat) list | MP_list of ( mpat) list | MP_cons of ( mpat) * ( mpat) - | MP_string_append of ( mpat) * ( mpat) + | MP_string_append of mpat list | MP_typ of mpat * atyp and mpat = diff --git a/src/parser.mly b/src/parser.mly index d41964b7..e1c6bd12 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -653,6 +653,12 @@ typschm_eof: | typschm Eof { $1 } +pat_string_append: + | atomic_pat + { [$1] } + | atomic_pat CaretCaret pat_string_append + { $1 :: $3 } + pat1: | atomic_pat { $1 } @@ -660,8 +666,8 @@ pat1: { mk_pat (P_vector_concat ($1 :: $3)) $startpos $endpos } | atomic_pat ColonColon pat1 { mk_pat (P_cons ($1, $3)) $startpos $endpos } - | atomic_pat CaretCaret pat1 - { mk_pat (P_string_append ($1, $3)) $startpos $endpos } + | atomic_pat CaretCaret pat_string_append + { mk_pat (P_string_append ($1 :: $3)) $startpos $endpos } pat_concat: | atomic_pat @@ -1202,6 +1208,12 @@ fun_def_list: | fun_def fun_def_list { $1 :: $2 } +mpat_string_append: + | atomic_mpat + { [$1] } + | atomic_mpat CaretCaret mpat_string_append + { $1 :: $3 } + mpat: | atomic_mpat { $1 } @@ -1209,8 +1221,8 @@ mpat: { mk_mpat (MP_vector_concat ($1 :: $3)) $startpos $endpos } | atomic_mpat ColonColon mpat { mk_mpat (MP_cons ($1, $3)) $startpos $endpos } - | atomic_mpat CaretCaret mpat - { mk_mpat (MP_string_append ($1, $3)) $startpos $endpos } + | atomic_mpat CaretCaret mpat_string_append + { mk_mpat (MP_string_append ($1 :: $3)) $startpos $endpos } mpat_concat: | atomic_mpat diff --git a/src/pattern_completeness.ml b/src/pattern_completeness.ml index 3797354c..2372ea82 100644 --- a/src/pattern_completeness.ml +++ b/src/pattern_completeness.ml @@ -68,7 +68,7 @@ type gpat = | GP_cons of gpat * gpat | GP_app of (gpat Bindings.t) | GP_record of (gpat Bindings.t) - | GP_string_append of gpat * gpat + | GP_string_append of gpat list let rec string_of_gpat = function | GP_lit lit -> string_of_lit lit @@ -81,7 +81,7 @@ let rec string_of_gpat = function | 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 (gpat1, gpat2) -> string_of_gpat gpat1 ^ " ^^" ^ string_of_gpat gpat2 + | GP_string_append gpats -> Util.string_of_list " ^^ " string_of_gpat gpats let is_wild = function | GP_wild -> true @@ -119,10 +119,9 @@ let rec generalize ctx (P_aux (p_aux, _) as pat) = let ghd_pat = generalize ctx hd_pat in let gtl_pat = generalize ctx tl_pat in if is_wild ghd_pat && is_wild gtl_pat then GP_wild else GP_cons (ghd_pat, gtl_pat) - | P_string_append (pat1, pat2) -> - let gpat1 = generalize ctx pat1 in - let gpat2 = generalize ctx pat2 in - if is_wild gpat1 && is_wild gpat2 then GP_wild else GP_string_append (gpat1, gpat2) + | P_string_append pats -> + let gpats = List.map (generalize ctx) pats in + if List.for_all is_wild gpats then GP_wild else GP_string_append gpats | P_app (f, pats) -> let gpats = List.map (generalize ctx) pats in if List.for_all is_wild gpats then diff --git a/src/rewriter.ml b/src/rewriter.ml index 74d9f40d..08c90803 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -304,7 +304,7 @@ let rewrite_pat rewriters (P_aux (pat,(l,annot)) as orig_pat) = | P_tup pats -> rewrap (P_tup (List.map rewrite pats)) | P_list pats -> rewrap (P_list (List.map rewrite pats)) | P_cons (pat1, pat2) -> rewrap (P_cons (rewrite pat1, rewrite pat2)) - | P_string_append (pat1, pat2) -> rewrap (P_string_append (rewrite pat1, rewrite pat2)) + | P_string_append pats -> rewrap (P_string_append (List.map rewrite pats)) let rewrite_exp rewriters (E_aux (exp,(l,annot)) as orig_exp) = let rewrap e = E_aux (e,(l,annot)) in @@ -453,7 +453,7 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg = ; p_tup : 'pat list -> 'pat_aux ; p_list : 'pat list -> 'pat_aux ; p_cons : 'pat * 'pat -> 'pat_aux - ; p_string_append : '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 @@ -474,7 +474,7 @@ let rec fold_pat_aux (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat | P_tup ps -> alg.p_tup (List.map (fold_pat alg) ps) | P_list ps -> alg.p_list (List.map (fold_pat alg) ps) | P_cons (ph,pt) -> alg.p_cons (fold_pat alg ph, fold_pat alg pt) - | P_string_append (p1, p2) -> alg.p_string_append (fold_pat alg p1, fold_pat alg p2) + | 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 = function @@ -501,7 +501,7 @@ let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg = ; p_tup = (fun ps -> P_tup ps) ; p_list = (fun ps -> P_list ps) ; p_cons = (fun (ph,pt) -> P_cons (ph,pt)) - ; p_string_append = (fun (p1,p2) -> P_string_append (p1,p2)) + ; 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)) @@ -748,7 +748,7 @@ let compute_pat_alg bot join = ; p_tup = split_join (fun ps -> P_tup ps) ; p_list = split_join (fun ps -> P_list ps) ; p_cons = (fun ((vh,ph),(vt,pt)) -> (join vh vt, P_cons (ph,pt))) - ; p_string_append = (fun ((v1,p1),(v2,p2)) -> (join v1 v2, P_string_append (p1,p2))) + ; 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))) diff --git a/src/rewriter.mli b/src/rewriter.mli index 70c894c4..90c15b16 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -95,7 +95,7 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg = ; p_tup : 'pat list -> 'pat_aux ; p_list : 'pat list -> 'pat_aux ; p_cons : 'pat * 'pat -> 'pat_aux - ; p_string_append : '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 diff --git a/src/rewrites.ml b/src/rewrites.ml index ac36dffa..e9afd415 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -676,7 +676,7 @@ let remove_vector_concat_pat pat = ; p_tup = (fun ps -> P_tup (List.map (fun p -> p false) ps)) ; p_list = (fun ps -> P_list (List.map (fun p -> p false) ps)) ; p_cons = (fun (p,ps) -> P_cons (p false, ps false)) - ; p_string_append = (fun (p1,p2) -> P_string_append (p1 false, p2 false)) + ; p_string_append = (fun (ps) -> P_string_append (List.map (fun p -> p false) ps)) ; p_aux = (fun (pat,((l,_) as annot)) contained_in_p_as -> match pat with @@ -819,8 +819,9 @@ let remove_vector_concat_pat pat = (P_tup ps,List.flatten decls)) ; p_list = (fun ps -> let (ps,decls) = List.split ps in (P_list ps,List.flatten decls)) + ; p_string_append = (fun ps -> let (ps,decls) = List.split ps in + (P_string_append ps,List.flatten decls)) ; p_cons = (fun ((p,decls),(p',decls')) -> (P_cons (p,p'), decls @ decls')) - ; p_string_append = (fun ((p1,decls1),(p2,decls2)) -> (P_string_append (p1,p2), decls1 @ decls2)) ; 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)) @@ -1074,7 +1075,7 @@ let rec pat_to_exp (P_aux (pat,(l,annot))) = | P_tup pats -> rewrap (E_tuple (List.map pat_to_exp pats)) | P_list pats -> rewrap (E_list (List.map pat_to_exp pats)) | P_cons (p,ps) -> rewrap (E_cons (pat_to_exp p, pat_to_exp ps)) - | P_string_append (p,ps) -> raise (Reporting_basic.err_unreachable l + | P_string_append (ps) -> raise (Reporting_basic.err_unreachable l "pat_to_exp not implemented for P_string_append") and fpat_to_fexp (FP_aux (FP_Fpat (id,pat),(l,annot))) = FE_aux (FE_Fexp (id, pat_to_exp pat),(l,annot)) @@ -1164,7 +1165,7 @@ let rec contains_bitvector_pat (P_aux (pat,annot)) = match pat with | P_app (_,pats) | P_tup pats | P_list pats -> List.exists contains_bitvector_pat pats | P_cons (p,ps) -> contains_bitvector_pat p || contains_bitvector_pat ps -| P_string_append (p1,p2) -> contains_bitvector_pat p1 || contains_bitvector_pat p2 +| 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 @@ -1190,10 +1191,10 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) = ; 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)) ; p_tup = (fun ps -> P_tup (List.map (fun p -> p false) ps)) ; p_list = (fun ps -> P_list (List.map (fun p -> p false) ps)) ; p_cons = (fun (p,ps) -> P_cons (p false, ps false)) - ; p_string_append = (fun (p1,p2) -> P_string_append (p1 false, p2 false)) ; p_aux = (fun (pat,annot) contained_in_p_as -> let env = env_of_annot annot in @@ -1342,14 +1343,14 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) = (P_vector ps, flatten_guards_decls gdls)) ; p_vector_concat = (fun ps -> let (ps,gdls) = List.split ps in (P_vector_concat ps, flatten_guards_decls gdls)) + ; p_string_append = (fun ps -> let (ps,gdls) = List.split ps in + (P_string_append ps, flatten_guards_decls gdls)) ; p_tup = (fun ps -> let (ps,gdls) = List.split ps in (P_tup ps, flatten_guards_decls gdls)) ; p_list = (fun ps -> let (ps,gdls) = List.split ps in (P_list ps, flatten_guards_decls gdls)) ; p_cons = (fun ((p,gdls),(p',gdls')) -> (P_cons (p,p'), flatten_guards_decls [gdls;gdls'])) - ; p_string_append = (fun ((p1,gdls1),(p2,gdls2)) -> - (P_string_append (p1,p2), flatten_guards_decls [gdls1;gdls2])) ; p_aux = (fun ((pat,gdls),annot) -> let env = env_of_annot annot in let t = Env.base_typ_of env (typ_of_annot annot) in @@ -2841,10 +2842,6 @@ let rec rewrite_defs_pat_string_append = let rec rewrite_pat (pat, guards, expr) = match pat with - (* (pat1 ^^ pat2) ^^ pat3 => expr ---> pat1 ^^ (pat2 ^^ pat3) => expr and recurse *) - | P_aux (P_string_append (P_aux (P_string_append (pat1, pat2), _), pat3), _) -> - let new_pat = mk_pat (P_string_append (pat1, mk_pat (P_string_append (pat2, pat3)))) in - rewrite_pat (new_pat, guards, expr) (* "lit" ^^ pat2 => expr ---> s# if startswith(s#, "lit") && match str_drop(s#, strlen("lit")) { @@ -2854,7 +2851,7 @@ let rec rewrite_defs_pat_string_append = pat2 => expr } *) - | P_aux (P_string_append (P_aux (P_lit (L_aux (L_string s, _) as lit), _), pat2), _) -> + | P_aux (P_string_append (P_aux (P_lit (L_aux (L_string s, _) as lit), _) :: pats), psa_annot) -> let id = mk_id ("_stringappend_" ^ (string_of_int !stringappend_counter) ^ "#") in stringappend_counter := !stringappend_counter + 1; @@ -2864,7 +2861,7 @@ let rec rewrite_defs_pat_string_append = (* recurse into pat2 *) let new_pat2_pexp = - match rewrite_pat (pat2, guards, expr) with + match rewrite_pat (P_aux (P_string_append (pats), psa_annot), guards, expr) with | pat, [], expr -> mk_pexp (Pat_exp (pat, expr)) | pat, gs, expr -> mk_pexp (Pat_when (pat, fold_guards gs, expr)) in @@ -2894,7 +2891,7 @@ let rec rewrite_defs_pat_string_append = pat2 => expr } *) - | P_aux (P_string_append (P_aux (P_app (Id_aux (Id builtin_id, _), [P_aux (P_id (Id_aux (Id var_id, _)), _)] ) , _), pat2), _) + | P_aux (P_string_append (P_aux (P_app (Id_aux (Id builtin_id, _), [P_aux (P_id (Id_aux (Id var_id, _)), _)] ) , _) :: pats), psa_annot) when List.mem_assoc builtin_id builtins -> (* common things *) @@ -2914,7 +2911,7 @@ let rec rewrite_defs_pat_string_append = (* recurse into pat2 *) let new_pat2_pexp = - match rewrite_pat (pat2, guards, expr) with + match rewrite_pat (P_aux (P_string_append (pats), psa_annot), guards, expr) with | pat, [], expr -> mk_pexp (Pat_exp (pat, expr)) | pat, gs, expr -> mk_pexp (Pat_when (pat, fold_guards gs, expr)) in @@ -2943,6 +2940,8 @@ let rec rewrite_defs_pat_string_append = (* construct final result *) mk_pat (P_id s_id), new_guard :: guards, new_let + | P_aux (P_string_append [], _) -> + mk_pat (P_lit (mk_lit (L_string ""))), guards, expr | P_aux (P_string_append _, _) -> failwith ("encountered a variety of string append pattern that is not yet implemented: " ^ string_of_pat pat) @@ -3493,6 +3492,10 @@ let rec exp_of_mpat (MP_aux (mpat, annot)) = let concat_vectors annot vec1 vec2 = (* TODO FIXME, this should be OK for typing but doesn't attach location information properly *) E_aux (E_vector_append (vec1, vec2), annot) in + let empty_string = E_aux (E_lit (L_aux (L_string "", Parse_ast.Unknown)), annot) in + let string_append annot str1 str2 = + E_aux (E_app (mk_id "string_append", [str1; str2]), annot) + in match mpat with | MP_lit lit -> E_aux (E_lit lit, annot) | MP_id id -> E_aux (E_id id, annot) @@ -3503,7 +3506,7 @@ let rec exp_of_mpat (MP_aux (mpat, annot)) = | MP_tup mpats -> E_aux (E_tuple (List.map exp_of_mpat mpats), annot) | MP_list mpats -> E_aux (E_list (List.map exp_of_mpat mpats), annot) | MP_cons (mpat1, mpat2) -> E_aux (E_cons (exp_of_mpat mpat1, exp_of_mpat mpat2), annot) - | MP_string_append (mpat1, mpat2) -> E_aux (E_app (mk_id "string_append", [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) and fexps_of_mfpats mfpats flag annot = @@ -3523,7 +3526,7 @@ let rec pat_of_mpat (MP_aux (mpat, annot)) = | MP_tup mpats -> P_aux (P_tup (List.map pat_of_mpat mpats), annot) | MP_list mpats -> P_aux (P_list (List.map pat_of_mpat mpats), annot) | MP_cons (mpat1, mpat2) -> P_aux ((P_cons (pat_of_mpat mpat1, pat_of_mpat mpat2), annot)) - | MP_string_append (mpat1, mpat2) -> P_aux ((P_string_append (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) and fpats_of_mfpats mfpats = diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 2f5d1d15..134a3e77 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -3,7 +3,7 @@ module Big_int = Nat_big_num type 'a return = { return : 'b . 'a -> 'b } type 'za zoption = | ZNone of unit | ZSome of 'za;; -let zint_forwardsz3 _ = assert false +let zint_forwardsz3 i = string_of_int (Big_int.to_int i) let opt_trace = ref false diff --git a/src/type_check.ml b/src/type_check.ml index f683feee..07aa199a 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2645,14 +2645,19 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) annot_pat (P_cons (hd_pat, tl_pat)) typ, env, hd_guards @ tl_guards | _ -> typ_error l "Cannot match cons pattern against non-list type" end - | P_string_append (pat1, pat2) -> + | P_string_append pats -> begin - let matcher = Env.expand_synonyms env typ in - match matcher with + match Env.expand_synonyms env typ with | Typ_aux (Typ_id id, _) when Id.compare id (mk_id "string") = 0 -> - let pat1, env, guards1 = bind_pat env pat1 typ in - let pat2, env, guards2 = bind_pat env pat2 typ in - annot_pat (P_string_append (pat1, pat2)) typ, env, guards1 @ guards2 + let rec process_pats env = function + | [] -> [], env, [] + | pat :: pats -> + let pat', env, guards = bind_pat env pat typ in + let pats', env, guards' = process_pats env pats in + pat' :: pats', env, guards @ guards' + in + let pats, env, guards = process_pats env pats in + annot_pat (P_string_append pats) typ, env, guards | _ -> typ_error l "Cannot match string-append pattern against non-string type" end | P_list pats -> @@ -2835,12 +2840,16 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) = in let len = nexp_simp (List.fold_left fold_len len (List.tl inferred_pats)) in annot_pat (P_vector_concat inferred_pats) (dvector_typ env len vtyp), env, guards - | P_string_append (pat1, pat2) -> - let typed_pat1, env, guards1 = infer_pat env pat1 in - let typed_pat2, env, guards2 = infer_pat env pat2 in - typ_equality l env (pat_typ_of typed_pat1) (string_typ); - typ_equality l env (pat_typ_of typed_pat2) (string_typ); - annot_pat (P_string_append (typed_pat1, typed_pat2)) string_typ, env, guards1 @ guards2 + | P_string_append pats -> + let fold_pats (pats, env, guards) pat = + let inferred_pat, env, guards' = infer_pat env pat in + typ_equality l env (pat_typ_of inferred_pat) string_typ; + pats @ [inferred_pat], env, guards' @ guards + in + let typed_pats, env, guards = + List.fold_left fold_pats ([], env, []) pats + in + annot_pat (P_string_append typed_pats) string_typ, env, guards | P_as (pat, id) -> let (typed_pat, env, guards) = infer_pat env pat in annot_pat (P_as (typed_pat, id)) (pat_typ_of typed_pat), @@ -3495,15 +3504,20 @@ and bind_mpat env (MP_aux (mpat_aux, (l, ())) as mpat) (Typ_aux (typ_aux, _) as annot_mpat (MP_cons (hd_mpat, tl_mpat)) typ, env, hd_guards @ tl_guards | _ -> typ_error l "Cannot match cons mapping-pattern against non-list type" end - | MP_string_append (mpat1, mpat2) -> + | MP_string_append mpats -> begin - let matcher = Env.expand_synonyms env typ in - match matcher with + match Env.expand_synonyms env typ with | Typ_aux (Typ_id id, _) when Id.compare id (mk_id "string") = 0 -> - let mpat1, env, guards1 = bind_mpat env mpat1 typ in - let mpat2, env, guards2 = bind_mpat env mpat2 typ in - annot_mpat (MP_string_append (mpat1, mpat2)) typ, env, guards1 @ guards2 - | _ -> typ_error l "Cannot match string-append mapping-pattern against non-string type" + let rec process_mpats env = function + | [] -> [], env, [] + | pat :: pats -> + let pat', env, guards = bind_mpat env pat typ in + let pats', env, guards' = process_mpats env pats in + pat' :: pats', env, guards @ guards' + in + let pats, env, guards = process_mpats env mpats in + annot_mpat (MP_string_append pats) typ, env, guards + | _ -> typ_error l "Cannot match string-append pattern against non-string type" end | MP_list mpats -> begin @@ -3661,12 +3675,17 @@ and infer_mpat env (MP_aux (mpat_aux, (l, ())) as mpat) = in let len = nexp_simp (List.fold_left fold_len len (List.tl inferred_mpats)) in annot_mpat (MP_vector_concat inferred_mpats) (dvector_typ env len vtyp), env, guards - | MP_string_append (mpat1, mpat2) -> - let typed_mpat1, env, guards1 = infer_mpat env mpat1 in - let typed_mpat2, env, guards2 = infer_mpat env mpat2 in - typ_equality l env (typ_of_mpat typed_mpat1) (string_typ); - typ_equality l env (typ_of_mpat typed_mpat2) (string_typ); - annot_mpat (MP_string_append (typed_mpat1, typed_mpat2)) string_typ, env, guards1 @ guards2 + | MP_string_append mpats -> + let fold_pats (pats, env, guards) pat = + let inferred_pat, env, guards' = infer_mpat env pat in + typ_equality l env (typ_of_mpat inferred_pat) string_typ; + pats @ [inferred_pat], env, guards' @ guards + in + let typed_mpats, env, guards = + List.fold_left fold_pats ([], env, []) mpats + in + annot_mpat (MP_string_append typed_mpats) string_typ, env, guards + | _ -> typ_error l ("Couldn't infer type of mapping-pattern " ^ string_of_mpat mpat) (**************************************************************************) @@ -3909,10 +3928,9 @@ and propagate_pat_effect_aux = function let p_pat1 = propagate_pat_effect pat1 in let p_pat2 = propagate_pat_effect pat2 in P_cons (p_pat1, p_pat2), union_effects (effect_of_pat p_pat1) (effect_of_pat p_pat2) - | P_string_append (pat1, pat2) -> - let p_pat1 = propagate_pat_effect pat1 in - let p_pat2 = propagate_pat_effect pat2 in - P_string_append (p_pat1, p_pat2), union_effects (effect_of_pat p_pat1) (effect_of_pat p_pat2) + | P_string_append pats -> + let p_pats = List.map propagate_pat_effect pats in + P_string_append p_pats, collect_effects_pat p_pats | P_as (pat, id) -> let p_pat = propagate_pat_effect pat in P_as (p_pat, id), effect_of_pat p_pat @@ -3949,10 +3967,9 @@ and propagate_mpat_effect_aux = function let p_mpat1 = propagate_mpat_effect mpat1 in let p_mpat2 = propagate_mpat_effect mpat2 in MP_cons (p_mpat1, p_mpat2), union_effects (effect_of_mpat p_mpat1) (effect_of_mpat p_mpat2) - | MP_string_append (mpat1, mpat2) -> - let p_mpat1 = propagate_mpat_effect mpat1 in - let p_mpat2 = propagate_mpat_effect mpat2 in - MP_string_append (p_mpat1, p_mpat2), union_effects (effect_of_mpat p_mpat1) (effect_of_mpat p_mpat2) + | MP_string_append mpats -> + let p_mpats = List.map propagate_mpat_effect mpats in + MP_string_append p_mpats, collect_effects_mpat p_mpats | MP_id id -> MP_id id, no_effect | MP_app (id, mpats) -> let p_mpats = List.map propagate_mpat_effect mpats in |