diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/parser.mly | 8 | ||||
| -rw-r--r-- | src/rewriter.ml | 4 | ||||
| -rw-r--r-- | src/type_check.ml | 5 |
3 files changed, 13 insertions, 4 deletions
diff --git a/src/parser.mly b/src/parser.mly index 10241137..5413ac0d 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -519,7 +519,7 @@ atomic_pat: { ploc (P_list([])) } | SquareBarBar pat BarBarSquare { ploc (P_list([$2])) } - | SquareBarBar comma_pats BarBarSquare + | SquareBarBar semi_pats BarBarSquare { ploc (P_list($2)) } | atomic_pat ColonColon pat { ploc (P_cons ($1, $3)) } @@ -552,6 +552,12 @@ comma_pats: | atomic_pat Comma comma_pats { $1::$3 } +semi_pats: + | atomic_pat Semi atomic_pat + { [$1;$3] } + | atomic_pat Semi semi_pats + { $1::$3 } + fpat: | id Eq pat { fploc (FP_Fpat($1,$3)) } diff --git a/src/rewriter.ml b/src/rewriter.ml index da1b5d23..d61939ee 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -1223,9 +1223,9 @@ let rewrite_sizeof (Defs defs) = let kid_annot kid = simple_annot l (kid_typ kid) in let kid_pat kid = P_aux (P_typ (kid_typ kid, - P_aux (P_id (Id_aux (Id (string_of_kid kid), l)), + P_aux (P_id (Id_aux (Id (string_of_id (id_of_kid kid) ^ "__tv"), l)), kid_annot kid)), kid_annot kid) in - let kid_eaux kid = E_id (Id_aux (Id (string_of_kid kid), l)) in + let kid_eaux kid = E_id (Id_aux (Id (string_of_id (id_of_kid kid) ^ "__tv"), l)) in let kid_typs = List.map kid_typ (KidSet.elements nvars) in let kid_pats = List.map kid_pat (KidSet.elements nvars) in let kid_nmap = List.map (fun kid -> (nvar kid, kid_eaux kid)) (KidSet.elements nvars) in diff --git a/src/type_check.ml b/src/type_check.ml index 9797ac25..9811b0d4 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2154,7 +2154,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) in let pats, env = process_pats env pats in annot_pat (P_list pats) typ, env - | _ -> typ_error l "Cannot match list pattern against non-list type" + | _ -> typ_error l ("Cannot match list pattern " ^ string_of_pat pat ^ " against non-list type " ^ string_of_typ typ) end | P_tup [] -> begin @@ -2207,6 +2207,9 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) end | P_app (f, _) when not (Env.is_union_constructor f env) -> typ_error l (string_of_id f ^ " is not a union constructor in pattern " ^ string_of_pat pat) + | P_as (pat, id) -> + let (typed_pat, env) = bind_pat env pat typ in + annot_pat (P_as (typed_pat, id)) (pat_typ_of typed_pat), Env.add_local id (Immutable, pat_typ_of typed_pat) env | _ -> let (inferred_pat, env) = infer_pat env pat in subtyp l env (pat_typ_of inferred_pat) typ; |