mappings: Support for unidirectional mapping clauses

8 files changed, 146 insertions, 51 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index db60005d..a4d6b37c 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -457,8 +457,13 @@ and map_mpexp_annot_aux f = function
   | MPat_pat mpat -> MPat_pat (map_mpat_annot f mpat)
   | MPat_when (mpat, guard) -> MPat_when (map_mpat_annot f mpat, map_exp_annot f guard)
 
-and map_mapcl_annot f (MCL_aux (MCL_mapcl (mpexp1, mpexp2), annot)) =
-  MCL_aux (MCL_mapcl (map_mpexp_annot f mpexp1, map_mpexp_annot f mpexp2), f annot)
+and map_mapcl_annot f = function
+  | (MCL_aux (MCL_bidir (mpexp1, mpexp2), annot)) ->
+     MCL_aux (MCL_bidir (map_mpexp_annot f mpexp1, map_mpexp_annot f mpexp2), f annot)
+  | (MCL_aux (MCL_forwards (mpexp, exp), annot)) ->
+     MCL_aux (MCL_forwards (map_mpexp_annot f mpexp, map_exp_annot f exp), f annot)
+  | (MCL_aux (MCL_backwards (mpexp, exp), annot)) ->
+     MCL_aux (MCL_backwards (map_mpexp_annot f mpexp, map_exp_annot f exp), f annot)
 
 and map_mpat_annot f (MP_aux (mpat, annot)) = MP_aux (map_mpat_annot_aux f mpat, f annot)
 and map_mpat_annot_aux f = function
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 4dcac1b8..dcb7a925 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -810,7 +810,9 @@ let to_ast_mpexp (names,k_env,def_ord) (Parse_ast.MPat_aux(mpexp, l)) =
 
 let to_ast_mapcl (names,k_env,def_ord) (Parse_ast.MCL_aux(mapcl, l)) =
   match mapcl with
-  | Parse_ast.MCL_mapcl (mpexp1, mpexp2) -> MCL_aux (MCL_mapcl (to_ast_mpexp (names,k_env,def_ord) mpexp1, to_ast_mpexp (names,k_env,def_ord) mpexp2), (l, ()))
+  | Parse_ast.MCL_bidir (mpexp1, mpexp2) -> MCL_aux (MCL_bidir (to_ast_mpexp (names,k_env,def_ord) mpexp1, to_ast_mpexp (names,k_env,def_ord) mpexp2), (l, ()))
+  | Parse_ast.MCL_forwards (mpexp, exp) -> MCL_aux (MCL_forwards (to_ast_mpexp (names,k_env,def_ord) mpexp, to_ast_exp k_env def_ord exp), (l, ()))
+  | Parse_ast.MCL_backwards (mpexp, exp) -> MCL_aux (MCL_backwards (to_ast_mpexp (names,k_env,def_ord) mpexp, to_ast_exp k_env def_ord exp), (l, ()))
 
 let to_ast_mapdef (names,k_env,def_ord) (Parse_ast.MD_aux(md,l):Parse_ast.mapdef) : (unit mapdef) envs_out =
   match md with
diff --git a/src/lexer.mll b/src/lexer.mll
index 16574ef1..cc49073c 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -250,6 +250,7 @@ rule token = parse
   | ">="				{ (GtEq(r">=")) }
   | "->"                                { MinusGt }
   | "<->"                               { Bidir }
+  | "<-"                                { LtMinus }
   | "=>"                                { EqGt(r "=>") }
   | "<="				{ (LtEq(r"<=")) }
   | "/*!"       { Doc (doc_comment (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) 0 lexbuf) }
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index d9ffb184..a4052d82 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -458,7 +458,9 @@ type mpexp =
   | MPat_aux of ( mpexp_aux) * l
 
 type mapcl_aux =  (* mapping clause (bidirectional pattern-match) *)
- | MCL_mapcl of ( mpexp) * ( mpexp)
+  | MCL_bidir of ( mpexp) * ( mpexp)
+  | MCL_forwards of mpexp * exp
+  | MCL_backwards of mpexp * exp
 
 type mapcl =
  | MCL_aux of ( mapcl_aux) * l
diff --git a/src/parser.mly b/src/parser.mly
index 4ebfe16e..b9aae275 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -117,7 +117,9 @@ let mk_default d n m = DT_aux (d, loc n m)
 
 let mk_mpexp mpexp n m = MPat_aux (mpexp, loc n m)
 let mk_mpat mpat n m = MP_aux (mpat, loc n m)
-let mk_mapcl mpexp1 mpexp2 n m = MCL_aux (MCL_mapcl (mpexp1, mpexp2), loc n m)
+let mk_bidir_mapcl mpexp1 mpexp2 n m = MCL_aux (MCL_bidir (mpexp1, mpexp2), loc n m)
+let mk_forwards_mapcl mpexp exp n m = MCL_aux (MCL_forwards (mpexp, exp), loc n m)
+let mk_backwards_mapcl mpexp exp n m = MCL_aux (MCL_backwards (mpexp, exp), loc n m)
 let mk_map id tannot mapcls n m = MD_aux (MD_mapping (id, tannot, mapcls), loc n m)
 
 let doc_vs doc (VS_aux (v, l)) = VS_aux (v, Documented (doc, l))
@@ -185,7 +187,7 @@ let rec desugar_rchain chain s e =
 
 %token Bar Comma Dot Eof Minus Semi Under DotDot
 %token Lcurly Rcurly Lparen Rparen Lsquare Rsquare LcurlyBar RcurlyBar LsquareBar RsquareBar
-%token MinusGt Bidir
+%token MinusGt Bidir LtMinus
 
 /*Terminals with content*/
 
@@ -1275,15 +1277,24 @@ atomic_mpat:
 
 
 
-mpexp:
+%inline mpexp:
   | mpat
     { mk_mpexp (MPat_pat $1) $startpos $endpos }
   | mpat If_ exp
     { mk_mpexp (MPat_when ($1, $3)) $startpos $endpos }
 
+
 mapcl:
   | mpexp Bidir mpexp
-    { mk_mapcl $1 $3 $startpos $endpos }
+    { mk_bidir_mapcl $1 $3 $startpos $endpos }
+  | mpexp EqGt exp
+      { mk_forwards_mapcl $1 $3 $startpos $endpos }
+  | mpexp LtMinus exp
+      { mk_backwards_mapcl $1 $3 $startpos $endpos }
+  (* | exp LtMinus pat
+   *   { mk_backwards_mapcl (mk_pexp (Pat_exp ($3, $1)) $startpos $endpos) $startpos $endpos }
+   * | exp LtMinus pat If_ exp
+   *   { mk_backwards_mapcl (mk_pexp (Pat_when ($3, $5, $1)) $startpos $endpos) $startpos $endpos } *)
 
 mapcl_list:
   | mapcl
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index b84bc3be..7b843ebe 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -471,10 +471,21 @@ let doc_mpexp (MPat_aux (mpexp, _)) =
   | MPat_pat mpat -> doc_mpat mpat
   | MPat_when (mpat, guard) -> doc_mpat mpat ^^ space ^^ string "if" ^^ space ^^ doc_exp guard
 
-let doc_mapcl (MCL_aux (MCL_mapcl (mpexp1, mpexp2), _)) =
-  let left = doc_mpexp mpexp1 in
-  let right = doc_mpexp mpexp2 in
-  left ^^ space ^^ string "<->" ^^ space ^^ right
+let doc_mapcl (MCL_aux (cl, _)) =
+  match cl with
+  | MCL_bidir (mpexp1, mpexp2) ->
+     let left = doc_mpexp mpexp1 in
+     let right = doc_mpexp mpexp2 in
+     separate space [left; string "<->"; right]
+  | MCL_forwards (mpexp, exp) ->
+     let left = doc_mpexp mpexp in
+     let right = doc_exp exp in
+     separate space [left; string "=>"; right]
+  | MCL_backwards (mpexp, exp) ->
+     let left = doc_mpexp mpexp in
+     let right = doc_exp exp in
+     separate space [left; string "<-"; right]
+
 
 let doc_mapdef (MD_aux (MD_mapping (id, typa, mapcls), _)) =
   match mapcls with
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 8a6b43a0..ec9ee393 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -3996,12 +3996,43 @@ let rewrite_defs_realise_mappings (Defs defs) =
     | MPat_aux (MPat_pat mpat, annot) -> Pat_aux (Pat_exp (pat_of_mpat mpat, exp), annot)
     | MPat_aux (MPat_when (mpat, guard), annot) -> Pat_aux (Pat_when (pat_of_mpat mpat, guard, exp), annot)
   in
-  let realise_mapcl forwards id (MCL_aux (MCL_mapcl (mpexp1, mpexp2), (l, ()))) =
-    realise_mpexps forwards mpexp1 mpexp2
+  let realise_single_mpexp mpexp exp =
+    match mpexp with
+    | MPat_aux (MPat_pat mpat, annot) ->
+       Pat_aux (Pat_exp (pat_of_mpat mpat, exp), annot)
+    | MPat_aux (MPat_when (mpat, guard), annot) ->
+       Pat_aux (Pat_when (pat_of_mpat mpat, guard, exp), annot)
   in
-  let realise_bool_mapcl forwards id (MCL_aux (MCL_mapcl (mpexp1, mpexp2), (l, ()))) =
-    let mpexp = if forwards then mpexp1 else mpexp2 in
-    realise_mpexps true mpexp (mk_mpexp (MPat_pat (mk_mpat (MP_lit (mk_lit L_true)))))
+  let realise_mapcl forwards id mapcl =
+    match mapcl with
+    | (MCL_aux (MCL_bidir (mpexp1, mpexp2), (l, ()))) ->
+       [realise_mpexps forwards mpexp1 mpexp2]
+    | (MCL_aux (MCL_forwards (mpexp, exp), (l, ()))) ->
+       if forwards then
+         [realise_single_mpexp mpexp exp]
+       else
+         []
+    | (MCL_aux (MCL_backwards (mpexp, exp), (l, ()))) ->
+       if forwards then
+         []
+       else
+         [realise_single_mpexp mpexp exp]
+  in
+  let realise_bool_mapcl forwards id mapcl =
+    match mapcl with
+    | (MCL_aux (MCL_bidir (mpexp1, mpexp2), (l, ()))) ->
+       let mpexp = if forwards then mpexp1 else mpexp2 in
+       [realise_mpexps true mpexp (mk_mpexp (MPat_pat (mk_mpat (MP_lit (mk_lit L_true)))))]
+    | (MCL_aux (MCL_forwards (mpexp, exp), (l, ()))) ->
+       if forwards then
+         [realise_single_mpexp mpexp (mk_lit_exp L_true)]
+       else
+         []
+    | (MCL_aux (MCL_backwards (mpexp, exp), (l, ()))) ->
+       if forwards then
+         []
+       else
+         [realise_single_mpexp mpexp (mk_lit_exp L_true)]
   in
   let arg_id = mk_id "arg#" in
   let arg_exp = (mk_exp (E_id arg_id)) in
@@ -4017,21 +4048,36 @@ let rewrite_defs_realise_mappings (Defs defs) =
     | MPat_aux (MPat_when (mpat, guard), aux_annot) ->
        MPat_aux (MPat_when (mk_mpat (MP_string_append [mpat; mk_mpat (MP_id placeholder_id)]), guard), aux_annot)
   in
-  let realise_prefix_mapcl forwards id (MCL_aux (MCL_mapcl (mpexp1, mpexp2), (l, ()))) =
-    let mpexp = if forwards then mpexp1 else mpexp2 in
-    let other = if forwards then mpexp2 else mpexp1 in
+  let realise_prefix_mapcl forwards id mapcl =
     let strlen = (
         mk_mpat (MP_app ( mk_id "sub_nat",
-                     [
-                       mk_mpat (MP_app ( mk_id "string_length" , [mk_mpat (MP_id arg_id        )]));
-                       mk_mpat (MP_app ( mk_id "string_length" , [mk_mpat (MP_id placeholder_id)]));
-                     ]
+                          [
+                            mk_mpat (MP_app ( mk_id "string_length" , [mk_mpat (MP_id arg_id        )]));
+                            mk_mpat (MP_app ( mk_id "string_length" , [mk_mpat (MP_id placeholder_id)]));
+                          ]
           ))
       ) in
-    match other with
-    | MPat_aux (MPat_pat mpat2, _)
-      | MPat_aux (MPat_when (mpat2, _), _)->
-       realise_mpexps true (append_placeholder mpexp) (mk_mpexp (MPat_pat (mk_mpat (MP_app ((mk_id "Some"), [ mk_mpat (MP_tup [mpat2; strlen]) ])))))
+    match mapcl with
+    | (MCL_aux (MCL_bidir (mpexp1, mpexp2), (l, ()))) -> begin
+       let mpexp = if forwards then mpexp1 else mpexp2 in
+       let other = if forwards then mpexp2 else mpexp1 in
+       match other with
+       | MPat_aux (MPat_pat mpat2, _)
+         | MPat_aux (MPat_when (mpat2, _), _)->
+          [realise_mpexps true (append_placeholder mpexp) (mk_mpexp (MPat_pat (mk_mpat (MP_app ((mk_id "Some"), [ mk_mpat (MP_tup [mpat2; strlen]) ])))))]
+      end
+    | (MCL_aux (MCL_forwards (mpexp, exp), (l, ()))) -> begin
+        if forwards then
+          [realise_single_mpexp (append_placeholder mpexp) (mk_exp (E_app ((mk_id "Some"), [mk_exp (E_tuple [exp; exp_of_mpat strlen])])))]
+        else
+          []
+      end
+    | (MCL_aux (MCL_backwards (mpexp, exp), (l, ()))) -> begin
+        if forwards then
+          []
+        else
+          [realise_single_mpexp (append_placeholder mpexp) (mk_exp (E_app ((mk_id "Some"), [mk_exp (E_tuple [exp; exp_of_mpat strlen])])))]
+      end
   in
   let realise_mapdef (MD_aux (MD_mapping (id, _, mapcls), ((l, (tannot:tannot)) as annot))) =
     let forwards_id = mk_id (string_of_id id ^ "_forwards") in
@@ -4066,12 +4112,12 @@ let rewrite_defs_realise_mappings (Defs defs) =
     let backwards_matches_spec, env = Type_check.check_val_spec env backwards_matches_spec in
 
     let no_tannot = (Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown)) in
-    let forwards_match = mk_exp (E_case (arg_exp, (List.map (fun mapcl -> strip_mapcl mapcl |> realise_mapcl true forwards_id) mapcls))) in
-    let backwards_match = mk_exp (E_case (arg_exp, (List.map (fun mapcl -> strip_mapcl mapcl |> realise_mapcl false backwards_id) mapcls))) in
+    let forwards_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_mapcl true forwards_id) mapcls) |> List.flatten))) in
+    let backwards_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_mapcl false backwards_id) mapcls) |> List.flatten))) in
 
     let wildcard = mk_pexp (Pat_exp (mk_pat P_wild, mk_exp (E_lit (mk_lit L_false)))) in
-    let forwards_matches_match = mk_exp (E_case (arg_exp, (List.map (fun mapcl -> strip_mapcl mapcl |> realise_bool_mapcl true forwards_matches_id) mapcls) @ [wildcard])) in
-    let backwards_matches_match = mk_exp (E_case (arg_exp, (List.map (fun mapcl -> strip_mapcl mapcl |> realise_bool_mapcl false backwards_matches_id) mapcls) @ [wildcard])) in
+    let forwards_matches_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_bool_mapcl true forwards_matches_id) mapcls) |> List.flatten) @ [wildcard])) in
+    let backwards_matches_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_bool_mapcl false backwards_matches_id) mapcls) |> List.flatten) @ [wildcard])) in
 
     let forwards_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl forwards_id arg_pat forwards_match]), (l, ()))) in
     let backwards_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl backwards_id arg_pat backwards_match]), (l, ()))) in
@@ -4094,7 +4140,7 @@ let rewrite_defs_realise_mappings (Defs defs) =
               let forwards_prefix_typ = Typ_aux (Typ_fn (typ1, app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
               let forwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
               let forwards_prefix_spec, env = Type_check.check_val_spec env forwards_prefix_spec in
-              let forwards_prefix_match = mk_exp (E_case (arg_exp, (List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl true prefix_id) mapcls) @ [prefix_wildcard])) in
+              let forwards_prefix_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl true prefix_id) mapcls) |> List.flatten) @ [prefix_wildcard])) in
               let forwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl prefix_id arg_pat forwards_prefix_match]), (l, ()))) in
               typ_debug (lazy (Printf.sprintf "forwards prefix matches for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef forwards_prefix_fun |> Pretty_print_sail.to_string)));
               let forwards_prefix_fun, _ = Type_check.check_fundef env forwards_prefix_fun in
@@ -4104,7 +4150,7 @@ let rewrite_defs_realise_mappings (Defs defs) =
                 let backwards_prefix_typ = Typ_aux (Typ_fn (typ2, app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
                 let backwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
                 let backwards_prefix_spec, env = Type_check.check_val_spec env backwards_prefix_spec in
-                let backwards_prefix_match = mk_exp (E_case (arg_exp, (List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl false prefix_id) mapcls) @ [prefix_wildcard])) in
+                let backwards_prefix_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl false prefix_id) mapcls) |> List.flatten) @ [prefix_wildcard])) in
                 let backwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl prefix_id arg_pat backwards_prefix_match]), (l, ()))) in
                 typ_debug (lazy (Printf.sprintf "backwards prefix matches for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef backwards_prefix_fun |> Pretty_print_sail.to_string)));
                 let backwards_prefix_fun, _ = Type_check.check_fundef env backwards_prefix_fun in
diff --git a/src/type_check.ml b/src/type_check.ml
index dbbc704c..885e4496 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -4180,22 +4180,39 @@ let check_funcl env (FCL_aux (FCL_Funcl (id, pexp), (l, _))) typ =
 
 
 let check_mapcl : 'a. Env.t -> 'a mapcl -> typ -> tannot mapcl =
-  fun env (MCL_aux (MCL_mapcl (mpexp1, mpexp2), (l, _))) typ ->
-        match typ with
-        | Typ_aux (Typ_bidir (typ1, typ2), _) ->
-           begin
-             let testing_env = Env.set_allow_unknowns true env in
-             let left_mpat, _, _ = destruct_mpexp mpexp1 in
-             let _, left_id_env, _ = bind_mpat true Env.empty testing_env (strip_mpat left_mpat) typ1 in
-             let right_mpat, _, _ = destruct_mpexp mpexp2 in
-             let _, right_id_env, _ = bind_mpat true Env.empty testing_env (strip_mpat right_mpat) typ2 in
-
-             let typed_mpexp1, prop_eff1 = propagate_mpexp_effect (check_mpexp right_id_env env (strip_mpexp mpexp1) typ1) in
-             let typed_mpexp2, prop_eff2 = propagate_mpexp_effect (check_mpexp left_id_env env (strip_mpexp mpexp2) typ2) in
-             MCL_aux (MCL_mapcl (typed_mpexp1, typed_mpexp2), (l, Some ((env, typ, union_effects prop_eff1 prop_eff2), Some typ)))
-           end
-        | _ -> typ_error l ("Function clause must have function type: " ^ string_of_typ typ ^ " is not a function type")
-
+  fun env (MCL_aux (cl, (l, _))) typ ->
+    match typ with
+    | Typ_aux (Typ_bidir (typ1, typ2), _) -> begin
+        match cl with
+        | MCL_bidir (mpexp1, mpexp2) -> begin
+            let testing_env = Env.set_allow_unknowns true env in
+            let left_mpat, _, _ = destruct_mpexp mpexp1 in
+            let _, left_id_env, _ = bind_mpat true Env.empty testing_env (strip_mpat left_mpat) typ1 in
+            let right_mpat, _, _ = destruct_mpexp mpexp2 in
+            let _, right_id_env, _ = bind_mpat true Env.empty testing_env (strip_mpat right_mpat) typ2 in
+
+            let typed_mpexp1, prop_eff1 = propagate_mpexp_effect (check_mpexp right_id_env env (strip_mpexp mpexp1) typ1) in
+            let typed_mpexp2, prop_eff2 = propagate_mpexp_effect (check_mpexp left_id_env env (strip_mpexp mpexp2) typ2) in
+            MCL_aux (MCL_bidir (typed_mpexp1, typed_mpexp2), (l, Some ((env, typ, union_effects prop_eff1 prop_eff2), Some typ)))
+          end
+        | MCL_forwards (mpexp, exp) -> begin
+            let mpat, _, _ = destruct_mpexp mpexp in
+            let _, mpat_env, _ = bind_mpat false Env.empty env (strip_mpat mpat) typ1 in
+            let typed_mpexp, prop_eff1 = propagate_mpexp_effect (check_mpexp Env.empty env (strip_mpexp mpexp) typ1) in
+            let typed_exp = propagate_exp_effect (check_exp mpat_env (strip_exp exp) typ2) in
+            let prop_effs = union_effects prop_eff1 (effect_of typed_exp) in
+            MCL_aux (MCL_forwards (typed_mpexp, typed_exp), (l, Some ((env, typ, prop_effs), Some typ)))
+          end
+        | MCL_backwards (mpexp, exp) -> begin
+            let mpat, _, _ = destruct_mpexp mpexp in
+            let _, mpat_env, _ = bind_mpat false Env.empty env (strip_mpat mpat) typ2 in
+            let typed_mpexp, prop_eff1 = propagate_mpexp_effect (check_mpexp Env.empty env (strip_mpexp mpexp) typ2) in
+            let typed_exp = propagate_exp_effect (check_exp mpat_env (strip_exp exp) typ1) in
+            let prop_effs = union_effects prop_eff1 (effect_of typed_exp) in
+            MCL_aux (MCL_backwards (typed_mpexp, typed_exp), (l, Some ((env, typ, prop_effs), Some typ)))
+          end
+      end
+    | _ -> typ_error l ("Mapping clause must have mapping type: " ^ string_of_typ typ ^ " is not a mapping type")        
 
 let funcl_effect (FCL_aux (FCL_Funcl (id, typed_pexp), (l, annot))) =
   match annot with
@@ -4203,7 +4220,7 @@ let funcl_effect (FCL_aux (FCL_Funcl (id, typed_pexp), (l, annot))) =
   | None -> no_effect (* Maybe could be assert false. This should never happen *)
 
 
-let mapcl_effect (MCL_aux (MCL_mapcl _, (l, annot))) =
+let mapcl_effect (MCL_aux (_, (l, annot))) =
   match annot with
   | Some ((_, _, eff), _) -> eff
   | None -> no_effect (* Maybe could be assert false. This should never happen *)