From 08227192a8068ac34b618cc218982e02b353127e Mon Sep 17 00:00:00 2001 From: Jon French Date: Fri, 8 Jun 2018 16:35:31 +0100 Subject: type checking mappings: allow inferring based on the other side's id inferences --- src/ast_util.ml | 5 ++- src/ast_util.mli | 1 + src/type_check.ml | 117 ++++++++++++++++++++++++++++++++++++------------------ 3 files changed, 84 insertions(+), 39 deletions(-) (limited to 'src') diff --git a/src/ast_util.ml b/src/ast_util.ml index 82e39022..2b275f35 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -273,6 +273,7 @@ let mk_id_typ id = Typ_aux (Typ_id id, Parse_ast.Unknown) let mk_ord ord_aux = Ord_aux (ord_aux, Parse_ast.Unknown) +let unknown_typ = mk_typ Typ_internal_unknown let int_typ = mk_id_typ (mk_id "int") let nat_typ = mk_id_typ (mk_id "nat") let unit_typ = mk_id_typ (mk_id "unit") @@ -601,6 +602,7 @@ and string_of_nexp_aux = function let rec string_of_typ = function | Typ_aux (typ, l) -> string_of_typ_aux typ and string_of_typ_aux = function + | Typ_internal_unknown -> "" | Typ_id id -> string_of_id id | Typ_var kid -> string_of_kid kid | Typ_tup typs -> "(" ^ string_of_list ", " string_of_typ typs ^ ")" @@ -986,6 +988,7 @@ let rec tyvars_of_nc (NC_aux (nc, _)) = let rec tyvars_of_typ (Typ_aux (t,_)) = match t with + | Typ_internal_unknown -> KidSet.empty | Typ_id _ -> KidSet.empty | Typ_var kid -> KidSet.singleton kid | Typ_fn (t1,t2,_) -> KidSet.union (tyvars_of_typ t1) (tyvars_of_typ t2) @@ -1034,7 +1037,7 @@ let rec undefined_of_typ mwords l annot (Typ_aux (typ_aux, _) as typ) = initial_check.ml. i.e. the rewriter should only encounter this case when re-writing those functions. *) wrap (E_id (prepend_id "typ_" (id_of_kid kid))) typ - | Typ_bidir _ | Typ_fn _ | Typ_exist _ -> assert false (* Typ_exist should be re-written *) + | Typ_internal_unknown | Typ_bidir _ | Typ_fn _ | Typ_exist _ -> assert false (* Typ_exist should be re-written *) and undefined_of_typ_args mwords l annot (Typ_arg_aux (typ_arg_aux, _) as typ_arg) = match typ_arg_aux with | Typ_arg_nexp n -> [E_aux (E_sizeof n, (l, annot (atom_typ n)))] diff --git a/src/ast_util.mli b/src/ast_util.mli index 6fb1c576..d23d56da 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -113,6 +113,7 @@ val mk_typ_arg : typ_arg_aux -> typ_arg val mk_id_typ : id -> typ (* Sail builtin types. *) +val unknown_typ : typ val int_typ : typ val nat_typ : typ val atom_typ : nexp -> typ diff --git a/src/type_check.ml b/src/type_check.ml index 6351e7d8..814672f1 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -160,6 +160,10 @@ let is_list (Typ_aux (typ_aux, _)) = when string_of_id f = "list" -> Some typ | _ -> None +let is_unknown_type = function + | (Typ_aux (Typ_internal_unknown, _)) -> true + | _ -> false + (* An index_sort is a more general form of range type: it can either be IS_int, which represents every natural number, or some set of natural numbers given by an IS_prop expression of the form @@ -228,6 +232,7 @@ and strip_order_aux = function | Ord_inc -> Ord_inc | Ord_dec -> Ord_dec and strip_typ_aux : typ_aux -> typ_aux = function + | Typ_internal_unknown -> Typ_internal_unknown | Typ_id id -> Typ_id (strip_id id) | Typ_var kid -> Typ_var (strip_kid kid) | Typ_fn (typ1, typ2, effect) -> Typ_fn (strip_typ typ1, strip_typ typ2, strip_effect effect) @@ -297,6 +302,7 @@ and nc_subst_nexp_aux l sv subst = function let rec typ_subst_nexp sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_nexp_aux sv subst typ, l) and typ_subst_nexp_aux sv subst = function + | Typ_internal_unknown -> Typ_internal_unknown | Typ_id v -> Typ_id v | Typ_var kid -> Typ_var kid | Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_nexp sv subst typ1, typ_subst_nexp sv subst typ2, effs) @@ -313,6 +319,7 @@ and typ_subst_arg_nexp_aux sv subst = function let rec typ_subst_typ sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_typ_aux sv subst typ, l) and typ_subst_typ_aux sv subst = function + | Typ_internal_unknown -> Typ_internal_unknown | Typ_id v -> Typ_id v | Typ_var kid -> if Kid.compare kid sv = 0 then subst else Typ_var kid | Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_typ sv subst typ1, typ_subst_typ sv subst typ2, effs) @@ -335,6 +342,7 @@ let order_subst sv subst (Ord_aux (ord, l)) = Ord_aux (order_subst_aux sv subst let rec typ_subst_order sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_order_aux sv subst typ, l) and typ_subst_order_aux sv subst = function + | Typ_internal_unknown -> Typ_internal_unknown | Typ_id v -> Typ_id v | Typ_var kid -> Typ_var kid | Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_order sv subst typ1, typ_subst_order sv subst typ2, effs) @@ -350,6 +358,7 @@ and typ_subst_arg_order_aux sv subst = function let rec typ_subst_kid sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_kid_aux sv subst typ, l) and typ_subst_kid_aux sv subst = function + | Typ_internal_unknown -> Typ_internal_unknown | Typ_id v -> Typ_id v | Typ_var kid -> if Kid.compare kid sv = 0 then Typ_var subst else Typ_var kid | Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_kid sv subst typ1, typ_subst_kid sv subst typ2, effs) @@ -425,6 +434,7 @@ module Env : sig val add_extern : id -> (string -> string option) -> t -> t val get_extern : id -> t -> string -> string val get_default_order : t -> order + val set_default_order : order_aux -> t -> t val set_default_order_inc : t -> t val set_default_order_dec : t -> t val add_enum : id -> id list -> t -> t @@ -444,6 +454,8 @@ module Env : sig val add_smt_op : id -> string -> t -> t val get_smt_op : id -> t -> string val have_smt_op : id -> t -> bool + val allow_unknowns : t -> bool + val set_allow_unknowns : bool -> t -> t (* Well formedness-checks *) val wf_typ : ?exs:KidSet.t -> t -> typ -> unit val wf_nexp : ?exs:KidSet.t -> t -> nexp -> unit @@ -486,6 +498,7 @@ end = struct ret_typ : typ option; poly_undefineds : bool; prove : t -> n_constraint -> bool; + allow_unknowns : bool; } let empty = @@ -513,10 +526,14 @@ end = struct ret_typ = None; poly_undefineds = false; prove = (fun _ _ -> false); + allow_unknowns = false; } let add_prover f env = { env with prove = f } + let allow_unknowns env = env.allow_unknowns + let set_allow_unknowns b env = { env with allow_unknowns = b } + let get_typ_var kid env = try KBindings.find kid env.typ_vars with | Not_found -> typ_error (kid_loc kid) ("No kind identifier " ^ string_of_kid kid) @@ -620,6 +637,7 @@ end = struct let rec expand_synonyms env (Typ_aux (typ, l) as t) = (* typ_debug (lazy ("Expanding synonyms for " ^ string_of_typ t)); *) match typ with + | Typ_internal_unknown -> Typ_aux (Typ_internal_unknown, l) | Typ_tup typs -> Typ_aux (Typ_tup (List.map (expand_synonyms env) typs), l) | Typ_fn (typ1, typ2, effs) -> Typ_aux (Typ_fn (expand_synonyms env typ1, expand_synonyms env typ2, effs), l) | Typ_bidir (typ1, typ2) -> Typ_aux (Typ_bidir (expand_synonyms env typ1, expand_synonyms env typ2), l) @@ -672,6 +690,7 @@ end = struct (** Map over all nexps in a type - excluding those in existential constraints **) let rec map_nexps f (Typ_aux (typ_aux, l) as typ) = match typ_aux with + | Typ_internal_unknown | Typ_id _ | Typ_var _ -> typ | Typ_fn (arg_typ, ret_typ, effect) -> Typ_aux (Typ_fn (map_nexps f arg_typ, map_nexps f ret_typ, effect), l) | Typ_bidir (typ1, typ2) -> Typ_aux (Typ_bidir (map_nexps f typ1, map_nexps f typ2), l) @@ -1437,6 +1456,7 @@ let order_frees (Ord_aux (ord_aux, l)) = let rec typ_nexps (Typ_aux (typ_aux, l)) = match typ_aux with + | Typ_internal_unknown -> [] | Typ_id v -> [] | Typ_var kid -> [] | Typ_tup typs -> List.concat (List.map typ_nexps typs) @@ -1454,6 +1474,7 @@ and typ_arg_nexps (Typ_arg_aux (typ_arg_aux, l)) = let rec typ_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) = match typ_aux with + | Typ_internal_unknown -> KidSet.empty | Typ_id v -> KidSet.empty | Typ_var kid when KidSet.mem kid exs -> KidSet.empty | Typ_var kid -> KidSet.singleton kid @@ -1696,6 +1717,8 @@ let rec unify l env typ1 typ2 = let rec unify_typ l (Typ_aux (typ1_aux, _) as typ1) (Typ_aux (typ2_aux, _) as typ2) = typ_debug (lazy ("UNIFYING TYPES " ^ string_of_typ typ1 ^ " AND " ^ string_of_typ typ2)); match typ1_aux, typ2_aux with + | Typ_internal_unknown, _ + | _, Typ_internal_unknown when Env.allow_unknowns env -> KBindings.empty | Typ_id v1, Typ_id v2 -> if Id.compare v1 v2 = 0 then KBindings.empty else unify_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2) @@ -1844,6 +1867,7 @@ let rec alpha_equivalent env typ1 typ2 = let rec relabel (Typ_aux (aux, l) as typ) = let relabelled_aux = match aux with + | Typ_internal_unknown -> Typ_internal_unknown | Typ_id _ | Typ_var _ -> aux | Typ_fn (typ1, typ2, eff) -> Typ_fn (relabel typ1, relabel typ2, eff) | Typ_bidir (typ1, typ2) -> Typ_bidir (relabel typ1, relabel typ2) @@ -2301,9 +2325,9 @@ let strip_pat : 'a pat -> unit pat = function pat -> map_pat_annot (fun (l, _) - let strip_pexp : 'a pexp -> unit pexp = function pexp -> map_pexp_annot (fun (l, _) -> (l, ())) pexp let strip_lexp : 'a lexp -> unit lexp = function lexp -> map_lexp_annot (fun (l, _) -> (l, ())) lexp -let strip_mpat : 'a mpat -> unit mpat = function mpat -> map_mpat_annot (fun (l, _) -> (l, ())) mpat -let strip_mpexp : 'a mpexp -> unit mpexp = function mpexp -> map_mpexp_annot (fun (l, _) -> (l, ())) mpexp -let strip_mapcl : 'a mapcl -> unit mapcl = function mapcl -> map_mapcl_annot (fun (l, _) -> (l, ())) mapcl +let strip_mpat : 'a. 'a mpat -> unit mpat = function mpat -> map_mpat_annot (fun (l, _) -> (l, ())) mpat +let strip_mpexp : 'a. 'a mpexp -> unit mpexp = function mpexp -> map_mpexp_annot (fun (l, _) -> (l, ())) mpexp +let strip_mapcl : 'a. 'a mapcl -> unit mapcl = function mapcl -> map_mapcl_annot (fun (l, _) -> (l, ())) mapcl let fresh_var = let counter = ref 0 in @@ -2562,9 +2586,9 @@ and check_case env pat_typ pexp typ = check_case env pat_typ (Pat_aux (Pat_when (mk_pat (P_id (mk_id "p#")), guard, case), annot)) typ | _ -> raise typ_exn -and check_mpexp env mpexp typ = +and check_mpexp other_env env mpexp typ = let mpat,guard,((l,_) as annot) = destruct_mpexp mpexp in - match bind_mpat env mpat typ with + match bind_mpat false other_env env mpat typ with | checked_mpat, env, guards -> let guard = match guard, guards with | None, h::t -> Some (h,t) @@ -3506,7 +3530,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ = typ_debug (lazy ("RETURNING AFTER COERCION " ^ string_of_typ (typ_of exp))); exp, !all_unifiers -and bind_mpat env (MP_aux (mpat_aux, (l, ())) as mpat) (Typ_aux (typ_aux, _) as typ) = +and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (Typ_aux (typ_aux, _) as typ) = let (Typ_aux (typ_aux, _) as typ), env = bind_existential typ env in typ_print (lazy ("Binding " ^ string_of_mpat mpat ^ " to " ^ string_of_typ typ)); let annot_mpat mpat typ = MP_aux (mpat, (l, Some (env, typ, no_effect))) in @@ -3515,7 +3539,7 @@ and bind_mpat env (MP_aux (mpat_aux, (l, ())) as mpat) (Typ_aux (typ_aux, _) as | _ -> typ_error l "Cannot switch type for unannotated mapping-pattern" in let bind_tuple_mpat (tpats, env, guards) mpat typ = - let tpat, env, guards' = bind_mpat env mpat typ in tpat :: tpats, env, guards' @ guards + let tpat, env, guards' = bind_mpat allow_unknown other_env env mpat typ in tpat :: tpats, env, guards' @ guards in match mpat_aux with | MP_id v -> @@ -3537,8 +3561,8 @@ and bind_mpat env (MP_aux (mpat_aux, (l, ())) as mpat) (Typ_aux (typ_aux, _) as begin match Env.expand_synonyms env typ with | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_typ ltyp, _)]), _) when Id.compare f (mk_id "list") = 0 -> - let hd_mpat, env, hd_guards = bind_mpat env hd_mpat ltyp in - let tl_mpat, env, tl_guards = bind_mpat env tl_mpat typ in + let hd_mpat, env, hd_guards = bind_mpat allow_unknown other_env env hd_mpat ltyp in + let tl_mpat, env, tl_guards = bind_mpat allow_unknown other_env env tl_mpat typ in 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 @@ -3549,7 +3573,7 @@ and bind_mpat env (MP_aux (mpat_aux, (l, ())) as mpat) (Typ_aux (typ_aux, _) as let rec process_mpats env = function | [] -> [], env, [] | pat :: pats -> - let pat', env, guards = bind_mpat env pat typ in + let pat', env, guards = bind_mpat allow_unknown other_env env pat typ in let pats', env, guards' = process_mpats env pats in pat' :: pats', env, guards @ guards' in @@ -3564,7 +3588,7 @@ and bind_mpat env (MP_aux (mpat_aux, (l, ())) as mpat) (Typ_aux (typ_aux, _) as let rec process_mpats env = function | [] -> [], env, [] | (pat :: mpats) -> - let mpat', env, guards = bind_mpat env mpat ltyp in + let mpat', env, guards = bind_mpat allow_unknown other_env env mpat ltyp in let mpats', env, guards' = process_mpats env mpats in mpat' :: mpats', env, guards @ guards' in @@ -3671,14 +3695,14 @@ and bind_mpat env (MP_aux (mpat_aux, (l, ())) as mpat) (Typ_aux (typ_aux, _) as | Typ_aux (typ, _) -> typ_error l ("unifying mapping type, expanded synonyms to non-mapping type??") end - | MP_app (f, _) when not (Env.is_union_constructor f env || Env.is_mapping f env)-> + | MP_app (f, _) when not (Env.is_union_constructor f env || Env.is_mapping f env) -> typ_error l (string_of_id f ^ " is not a union constructor or mapping in mapping-pattern " ^ string_of_mpat mpat) (* This is a special case for flow typing when we match a constant numeric literal. *) | MP_lit (L_aux (L_num n, _) as lit) when is_atom typ -> let nexp = match destruct_atom_nexp env typ with Some n -> n | None -> assert false in annot_mpat (MP_lit lit) (atom_typ (nconstant n)), Env.add_constraint (nc_eq nexp (nconstant n)) env, [] | _ -> - let (inferred_mpat, env, guards) = infer_mpat env mpat in + let (inferred_mpat, env, guards) = infer_mpat allow_unknown other_env env mpat in match subtyp l env typ (typ_of_mpat inferred_mpat) with | () -> switch_typ inferred_mpat (typ_of_mpat inferred_mpat), env, guards | exception (Type_error _ as typ_exn) -> @@ -3686,17 +3710,23 @@ and bind_mpat env (MP_aux (mpat_aux, (l, ())) as mpat) (Typ_aux (typ_aux, _) as | MP_lit lit -> let var = fresh_var () in let guard = mk_exp (E_app_infix (mk_exp (E_id var), mk_id "==", mk_exp (E_lit lit))) in - let (typed_mpat, env, guards) = bind_mpat env (mk_mpat (MP_id var)) typ in + let (typed_mpat, env, guards) = bind_mpat allow_unknown other_env env (mk_mpat (MP_id var)) typ in typed_mpat, env, guard::guards | _ -> raise typ_exn -and infer_mpat env (MP_aux (mpat_aux, (l, ())) as mpat) = +and infer_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) = let annot_mpat mpat typ = MP_aux (mpat, (l, Some (env, typ, no_effect))) in match mpat_aux with | MP_id v -> begin match Env.lookup_id v env with | Local (Immutable, _) | Unbound -> - typ_error l ("Cannot infer identifier in mapping-pattern " ^ string_of_mpat mpat ^ " - try adding a type annotation") + begin match Env.lookup_id v other_env with + | Local (Immutable, typ) -> annot_mpat (MP_typ (annot_mpat (MP_id v) typ, typ)) typ, env, [] + | Unbound -> + if allow_unknown then annot_mpat (MP_id v) unknown_typ, env, [] else + typ_error l ("Cannot infer identifier in mapping-pattern " ^ string_of_mpat mpat ^ " - try adding a type annotation") + | _ -> assert false + end | Local (Mutable, _) | Register _ -> typ_error l ("Cannot shadow mutable local or register in mapping-pattern " ^ string_of_mpat mpat) | Enum enum -> annot_mpat (MP_id v) enum, env, [] @@ -3705,11 +3735,11 @@ and infer_mpat env (MP_aux (mpat_aux, (l, ())) as mpat) = annot_mpat (MP_lit lit) (infer_lit env lit), env, [] | MP_typ (mpat, typ_annot) -> Env.wf_typ env typ_annot; - let (typed_mpat, env, guards) = bind_mpat env mpat typ_annot in + let (typed_mpat, env, guards) = bind_mpat allow_unknown other_env env mpat typ_annot in annot_mpat (MP_typ (typed_mpat, typ_annot)) typ_annot, env, guards | MP_vector (mpat :: mpats) -> let fold_mpats (mpats, env, guards) mpat = - let typed_mpat, env, guards' = bind_mpat env mpat bit_typ in + let typed_mpat, env, guards' = bind_mpat allow_unknown other_env env mpat bit_typ in mpats @ [typed_mpat], env, guards' @ guards in let mpats, env, guards = List.fold_left fold_mpats ([], env, []) (mpat :: mpats) in @@ -3719,22 +3749,25 @@ and infer_mpat env (MP_aux (mpat_aux, (l, ())) as mpat) = annot_mpat (MP_vector mpats) (dvector_typ env len etyp), env, guards | MP_vector_concat (mpat :: mpats) -> let fold_mpats (mpats, env, guards) mpat = - let inferred_mpat, env, guards' = infer_mpat env mpat in + let inferred_mpat, env, guards' = infer_mpat allow_unknown other_env env mpat in mpats @ [inferred_mpat], env, guards' @ guards in let inferred_mpats, env, guards = List.fold_left fold_mpats ([], env, []) (mpat :: mpats) in - let (len, _, vtyp) = destruct_vec_typ l env (typ_of_mpat (List.hd inferred_mpats)) in - let fold_len len mpat = - let (len', _, vtyp') = destruct_vec_typ l env (typ_of_mpat mpat) in - typ_equality l env vtyp vtyp'; - nsum len len' - 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 + if allow_unknown && List.exists (fun mpat -> is_unknown_type (typ_of_mpat mpat)) inferred_mpats then + annot_mpat (MP_vector_concat inferred_mpats) unknown_typ, env, guards (* hack *) + else + let (len, _, vtyp) = destruct_vec_typ l env (typ_of_mpat (List.hd inferred_mpats)) in + let fold_len len mpat = + let (len', _, vtyp') = destruct_vec_typ l env (typ_of_mpat mpat) in + typ_equality l env vtyp vtyp'; + nsum len len' + 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 mpats -> let fold_pats (pats, env, guards) pat = - let inferred_pat, env, guards' = infer_mpat env pat in + let inferred_pat, env, guards' = infer_mpat allow_unknown other_env env pat in typ_equality l env (typ_of_mpat inferred_pat) string_typ; pats @ [inferred_pat], env, guards' @ guards in @@ -3743,7 +3776,8 @@ and infer_mpat env (MP_aux (mpat_aux, (l, ())) as mpat) = 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) + | _ -> + typ_error l ("Couldn't infer type of mapping-pattern " ^ string_of_mpat mpat) (**************************************************************************) (* 6. Effect system *) @@ -4139,15 +4173,22 @@ let check_funcl env (FCL_aux (FCL_Funcl (id, pexp), (l, _))) typ = | _ -> typ_error l ("Function clause must have function type: " ^ string_of_typ typ ^ " is not a function type") -let check_mapcl env (MCL_aux (MCL_mapcl (mpexp1, mpexp2), (l, _))) typ = - match typ with - | Typ_aux (Typ_bidir (typ1, typ2), _) -> - begin - let typed_mpexp1, prop_eff1 = propagate_mpexp_effect (check_mpexp env (strip_mpexp mpexp1) typ1) in - let typed_mpexp2, prop_eff2 = propagate_mpexp_effect (check_mpexp env (strip_mpexp mpexp2) typ2) in - MCL_aux (MCL_mapcl (typed_mpexp1, typed_mpexp2), (l, Some (env, typ, union_effects prop_eff1 prop_eff2))) - end - | _ -> typ_error l ("Function clause must have function type: " ^ string_of_typ typ ^ " is not a function type") +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))) + end + | _ -> typ_error l ("Function clause must have function type: " ^ string_of_typ typ ^ " is not a function type") let funcl_effect (FCL_aux (FCL_Funcl (id, typed_pexp), (l, annot))) = -- cgit v1.2.3