Parser,Dterm,Dexpr: accept typecasts in patterns

src/core/dterm.ml

@@ -156,6 +156,7 @@ and dpattern_node =
   | DPapp of lsymbol * dpattern list
   | DPor of dpattern * dpattern
   | DPas of dpattern * preid
+  | DPcast of dpattern * ty
 
 type dbinop =
   | DTand | DTand_asym | DTor | DTor_asym | DTimplies | DTiff
@@ -282,8 +283,12 @@ let dpattern ?loc node =
             "Variable %s has type %a,@ but is expected to have type %a"
             n print_dty dty1 print_dty dty2 in
         dp1.dp_dty, Mstr.union join dp1.dp_vars dp2.dp_vars
-    | DPas (dp, {pre_name = n}) ->
-        dp.dp_dty, Mstr.add_new (DuplicateVar n) n dp.dp_dty dp.dp_vars in
+    | DPas (dp,{pre_name = n}) ->
+        dp.dp_dty, Mstr.add_new (DuplicateVar n) n dp.dp_dty dp.dp_vars
+    | DPcast (dp,ty) ->
+        let dty = dty_of_ty ty in
+        dpat_expected_type dp dty;
+        dty, dp.dp_vars in
   let dty, vars = Loc.try1 ?loc get_dty node in
   { dp_node = node; dp_dty = dty; dp_vars = vars; dp_loc = loc }
 
@@ -403,7 +408,9 @@ let pattern ~strict env dp =
         pat_or (get dp1) (get dp2)
     | DPas (dp,id) ->
         let pat = get dp in
-        pat_as pat (find_var id pat.pat_ty) in
+        pat_as pat (find_var id pat.pat_ty)
+    | DPcast (dp,_) ->
+        get dp in
   let pat = get dp in
   Mstr.set_union !acc env, pat
 

src/core/dterm.mli

@@ -37,6 +37,7 @@ and dpattern_node =
   | DPapp of lsymbol * dpattern list
   | DPor of dpattern * dpattern
   | DPas of dpattern * preid
+  | DPcast of dpattern * ty
 
 type dbinop =
   | DTand | DTand_asym | DTor | DTor_asym | DTimplies | DTiff

src/parser/parser.mly

@@ -850,6 +850,7 @@ pat_uni_:
 | pat_arg_                              { $1 }
 | uqualid pat_arg+                      { Papp ($1,$2) }
 | mk_pat(pat_uni_) AS labels(lident)    { Pas ($1,$3) }
+| mk_pat(pat_uni_) cast                 { Pcast($1,$2) }
 
 pat_arg_:
 | UNDERSCORE                            { Pwild }

src/parser/ptree.ml

@@ -69,6 +69,7 @@ and pat_desc =
   | Ptuple of pattern list
   | Por of pattern * pattern
   | Pas of pattern * ident
+  | Pcast of pattern * pty
 
 type term = {
   term_desc : term_desc;

src/parser/typing.ml

@@ -170,7 +170,8 @@ let rec dpattern uc { pat_desc = desc; pat_loc = loc } =
         let cs,fl = parse_record ~loc uc get_val fl in
         DPapp (cs,fl)
     | Ptree.Pas (p, x) -> DPas (dpattern uc p, create_user_id x)
-    | Ptree.Por (p, q) -> DPor (dpattern uc p, dpattern uc q))
+    | Ptree.Por (p, q) -> DPor (dpattern uc p, dpattern uc q)
+    | Ptree.Pcast (p, ty) -> DPcast (dpattern uc p, ty_of_pty uc ty))
 
 let quant_var uc (loc, id, gh, ty) =
   assert (not gh);

src/whyml/mlw_dexpr.ml

@@ -341,6 +341,7 @@ type dpattern_node =
   | DPpapp of plsymbol * dpattern list
   | DPor   of dpattern * dpattern
   | DPas   of dpattern * preid
+  | DPcast of dpattern * ity
 
 (** Specifications *)
 
@@ -549,6 +550,11 @@ let dpat_expected_type {dp_dity = dp_dity; dp_loc = loc} dity =
     "This pattern has type %a,@ but is expected to have type %a"
     print_dity dp_dity print_dity dity
 
+let dpat_expected_type_weak {dp_dity = dp_dity; dp_loc = loc} dity =
+  try dity_unify_weak dp_dity dity with Exit -> Loc.errorm ?loc
+    "This pattern has type %a,@ but is expected to have type %a"
+    print_dity dp_dity print_dity dity
+
 let dexpr_expected_type {de_dvty = (al,res); de_loc = loc} dity =
   if al <> [] then Loc.errorm ?loc "This expression is not a first-order value";
   try dity_unify res dity with Exit -> Loc.errorm ?loc
@@ -635,6 +641,9 @@ let dpattern ?loc node =
         let { dp_pat = pat; dp_dity = dity; dp_vars = vars } = dp in
         let vars = Mstr.add_new (Dterm.DuplicateVar n) n dity vars in
         mk_dpat (PPas (pat, id)) dity vars
+    | DPcast (dp, ity) ->
+        dpat_expected_type_weak dp (dity_of_ity ity);
+        dp
   in
   Loc.try1 ?loc dpat node
 

src/whyml/mlw_dexpr.mli

@@ -47,6 +47,7 @@ type dpattern_node =
   | DPpapp of plsymbol * dpattern list
   | DPor   of dpattern * dpattern
   | DPas   of dpattern * preid
+  | DPcast of dpattern * ity
 
 (** Binders *)
 

src/whyml/mlw_typing.ml

@@ -189,6 +189,7 @@ let rec dpattern uc { pat_desc = desc; pat_loc = loc } =
     | Ptree.Ptuple pl ->
         let pl = List.map (fun p -> dpattern uc p) pl in
         DPlapp (fs_tuple (List.length pl), pl)
+    | Ptree.Pcast (p, pty) -> DPcast (dpattern uc p, ity_of_pty uc pty)
     | Ptree.Pas (p, x) -> DPas (dpattern uc p, create_user_id x)
     | Ptree.Por (p, q) -> DPor (dpattern uc p, dpattern uc q))