diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/monomorphise.ml | 30 | ||||
| -rw-r--r-- | src/parse_ast.ml | 2 | ||||
| -rw-r--r-- | src/parser.mly | 4 | ||||
| -rw-r--r-- | src/pattern_completeness.ml | 12 | ||||
| -rw-r--r-- | src/pretty_print_sail.ml | 4 | ||||
| -rw-r--r-- | src/rewriter.ml | 2 | ||||
| -rw-r--r-- | src/type_check.ml | 25 |
7 files changed, 43 insertions, 36 deletions
diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 569f497d..9acb6052 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -549,8 +549,8 @@ 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_or(p1, p2) -> re (P_or(s_pat p1, s_pat p2)) - | P_not(p) -> re (P_not(s_pat p)) + | P_or (p1, p2) -> re (P_or (s_pat p1, s_pat p2)) + | P_not (p) -> re (P_not (s_pat p)) | 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')) @@ -645,8 +645,8 @@ let bindings_from_pat p = | P_lit _ | P_wild -> [] - | P_or(p1, p2) -> aux_pat p1 @ aux_pat p2 - | P_not(p) -> aux_pat p + | P_or (p1, p2) -> aux_pat p1 @ aux_pat p2 + | P_not (p) -> aux_pat p | P_as (p,id) -> id::(aux_pat p) | P_typ (_,p) -> aux_pat p | P_id id -> @@ -987,13 +987,13 @@ let rec freshen_pat_bindings p = match p with | P_lit _ | P_wild -> pat, [] - | P_or(p1, p2) -> + | P_or (p1, p2) -> let (r1, vs1) = aux p1 in let (r2, vs2) = aux p2 in - (mkp (P_or(r1, r2)), vs1 @ vs2) - | P_not(p) -> + (mkp (P_or (r1, r2)), vs1 @ vs2) + | P_not p -> let (r, vs) = aux p in - (mkp (P_not(r)), vs) + (mkp (P_not r), vs) | P_as (p,_) -> aux p | P_typ (typ,p) -> let p',vs = aux p in mkp (P_typ (typ,p')),vs | P_id id -> let id' = freshen_id id in mkp (P_id id'),[id,E_aux (E_id id',(Generated Unknown,None))] @@ -1772,12 +1772,12 @@ let split_defs all_errors splits defs = | P_lit _ | P_wild -> None - | P_or(p1, p2) -> + | P_or (p1, p2) -> (* 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 spl (fun [p1'; p2'] -> P_or(p1', p2')) [p1; p2] - | P_not(p) -> + relist spl (fun [p1'; p2'] -> P_or (p1', p2')) [p1; p2] + | P_not p -> (* todo: not sure that I can't split - but can't figure out how at * the moment *) raise (Reporting_basic.err_general l @@ -2471,12 +2471,12 @@ let rec typ_pat_eq (TP_aux (tp1, _)) (TP_aux (tp2, _)) = | 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 | P_wild, P_wild -> true - | P_or(p1, q1), P_or(p2, q2) -> + | P_or (p1, q1), P_or (p2, q2) -> (* ToDo: A case could be made for flattening trees of P_or nodes and * comparing the lists so that we treat P_or as associative *) @@ -3287,11 +3287,11 @@ let initial_env fn_id fn_l (TypQ_aux (tq,_)) pat body set_assertions = | P_lit _ | P_wild -> ArgSplits.empty,Bindings.empty,KBindings.empty - | P_or(p1, p2) -> + | P_or (p1, p2) -> let (s1, v1, k1) = aux p1 in let (s2, v2, k2) = aux p2 in (ArgSplits.merge merge_detail s1 s2, dep_bindings_merge v1 v2, dep_kbindings_merge k1 k2) - | P_not(p) -> aux p + | P_not p -> aux p | P_as (pat,id) -> begin let s,v,k = aux pat in diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 49878217..b5875ea7 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -242,7 +242,7 @@ type pat_aux = (* Pattern *) P_lit of lit (* literal constant pattern *) | P_wild (* wildcard - always matches *) - | P_or of ( pat * pat) (* choice pattern - P|Q matches if P matches or Q matches *) + | P_or of pat * pat (* choice pattern - P|Q matches if P matches or Q matches *) | P_typ of atyp * pat (* typed pattern *) | P_id of id (* identifier *) | P_var of pat * atyp (* bind pat to type variable *) diff --git a/src/parser.mly b/src/parser.mly index 2a05c013..694a4669 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -676,6 +676,8 @@ 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 @@ -710,8 +712,6 @@ atomic_pat: { mk_pat (P_lit $1) $startpos $endpos } | id { mk_pat (P_id $1) $startpos $endpos } - | pat Bar pat - { mk_pat (P_or ($1, $3)) $startpos $endpos } | kid { mk_pat (P_var (mk_pat (P_id (id_of_kid $1)) $startpos $endpos, mk_typ (ATyp_var $1) $startpos $endpos)) $startpos $endpos } diff --git a/src/pattern_completeness.ml b/src/pattern_completeness.ml index 83264453..c6fb5308 100644 --- a/src/pattern_completeness.ml +++ b/src/pattern_completeness.ml @@ -66,6 +66,7 @@ type gpat = | GP_tup of gpat list | GP_list of gpat list | 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 @@ -78,6 +79,7 @@ let rec string_of_gpat = function | GP_tup gpats -> "(" ^ Util.string_of_list ", " string_of_gpat gpats ^ ")" | GP_list gpats -> "[|" ^ Util.string_of_list ", " string_of_gpat gpats ^ "|]" | GP_cons (gpat1, gpat2) -> string_of_gpat gpat1 ^ " :: " ^ string_of_gpat gpat2 + | 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" @@ -88,14 +90,11 @@ let is_wild = function | _ -> false let rec generalize ctx (P_aux (p_aux, _) as pat) = - match p_aux with | P_lit lit -> GP_lit lit | P_wild -> GP_wild - (* todo: define GP_or/GP_not? or desugar at this stage? - | P_or(pat1, pat2) -> P_or(generalize ctx pat1, generalize ctx pat2) - | P_not(pat) -> P_not(generalize ctx pat) - *) + | P_or (pat1, pat2) -> GP_or (generalize ctx pat1, generalize ctx pat2) + | P_not(pat) -> GP_wild (* TODO: How to generalize negated patterns? *) | P_as (pat, _) -> generalize ctx pat | P_typ (_, pat) -> generalize ctx pat (* This will possibly overapproximate how general P_typ is *) | P_id id -> @@ -256,6 +255,9 @@ let rec join ctx gpat1 gpat2 = else GP_app ctors + | GP_or (gpat1, gpat2), gpat3 -> join ctx (join ctx gpat1 gpat2) gpat3 + | gpat1, GP_or (gpat2, gpat3) -> join ctx gpat1 (join ctx gpat2 gpat3) + | _, _ -> GP_wild let combine ctx gpat (l, pat) = diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 4df6fe75..9d9b4b4e 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -224,8 +224,8 @@ let doc_lit (L_aux(l,_)) = let rec doc_pat (P_aux (p_aux, _) as pat) = match p_aux with | P_id id -> doc_id id - | P_or(pat1, pat2) -> parens (doc_pat pat1 ^^ string " | " ^^ doc_pat pat2) - | P_not(pat) -> parens (doc_pat pat) + | P_or (pat1, pat2) -> parens (doc_pat pat1 ^^ string " | " ^^ doc_pat pat2) + | P_not pat -> string "~" ^^ parens (doc_pat pat) | P_tup pats -> lparen ^^ separate_map (comma ^^ space) doc_pat pats ^^ rparen | P_typ (typ, pat) -> separate space [doc_pat pat; colon; doc_typ typ] | P_lit lit -> doc_lit lit diff --git a/src/rewriter.ml b/src/rewriter.ml index 1fa3bc67..f072f91f 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -292,7 +292,7 @@ let rewrite_pat rewriters (P_aux (pat,(l,annot)) as orig_pat) = rewrap (P_vector ps) | P_lit _ | P_wild | P_id _ | P_var _ -> rewrap pat | P_or(pat1, pat2) -> rewrap (P_or(rewrite pat1, rewrite pat2)) - | P_not(pat) -> rewrap (P_not(rewrite pat)) + | P_not(pat) -> rewrap (P_not(rewrite 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)) diff --git a/src/type_check.ml b/src/type_check.ml index 4aaf73bf..28e0f930 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -406,6 +406,9 @@ module Env : sig val have_smt_op : id -> t -> bool val allow_unknowns : t -> bool val set_allow_unknowns : bool -> t -> t + + val no_bindings : t -> t + (* Well formedness-checks *) val wf_typ : ?exs:KidSet.t -> t -> typ -> unit val wf_nexp : ?exs:KidSet.t -> t -> nexp -> unit @@ -443,6 +446,7 @@ end = struct smt_ops : string Bindings.t; casts : id list; allow_casts : bool; + allow_bindings : bool; constraints : n_constraint list; default_order : order option; ret_typ : typ option; @@ -470,6 +474,7 @@ end = struct externs = Bindings.empty; smt_ops = Bindings.empty; casts = []; + allow_bindings = true; allow_casts = true; constraints = []; default_order = None; @@ -971,6 +976,7 @@ end = struct let add_local id mtyp env = begin + if not env.allow_bindings then typ_error (id_loc id) "Bindings are not allowed in this context" else (); wf_typ env (snd mtyp); if Bindings.mem id env.top_val_specs then typ_error (id_loc id) ("Local variable " ^ string_of_id id ^ " is already bound as a function name") @@ -1099,6 +1105,8 @@ end = struct let no_casts env = { env with allow_casts = false } let enable_casts env = { env with allow_casts = true } + let no_bindings env = { env with allow_bindings = false } + let add_cast cast env = typ_print (lazy ("Adding cast " ^ string_of_id cast)); { env with casts = cast :: env.casts } @@ -2618,16 +2626,13 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) let typed_pat, env, guards = bind_pat env pat typ in annot_pat (P_var (typed_pat, typ_pat)) typ, env, guards | P_wild -> annot_pat P_wild typ, env, [] - | P_or(pat1, pat2) -> - let tpat1, env1, guards1 = bind_pat env pat1 typ in - let tpat2, env2, guards2 = bind_pat env pat2 typ in - (* todo: report error if env != env1 or env != env2 *) - (* todo: not sure I am doing the right thing with guards1 @ guards2 *) - (annot_pat (P_or(tpat1, tpat2)) typ, env, guards1 @ guards2) - | P_not(pat) -> - let tpat, env', guards = bind_pat env pat typ in - (* todo: report error if env != env' *) - (annot_pat (P_not(tpat)) typ, env, guards) + | P_or (pat1, pat2) -> + let tpat1, env1, guards1 = bind_pat (Env.no_bindings env) pat1 typ in + let tpat2, env2, guards2 = bind_pat (Env.no_bindings env) pat2 typ in + annot_pat (P_or (tpat1, tpat2)) typ, env, guards1 @ guards2 + | P_not pat -> + let tpat, env', guards = bind_pat (Env.no_bindings env) pat typ in + annot_pat (P_not(tpat)) typ, env, guards | P_cons (hd_pat, tl_pat) -> begin match Env.expand_synonyms env typ with |