From bc6b51d70a783df161f8fb43264ea1558ff37bac Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 16 Jan 2020 19:14:22 +0000 Subject: Allow effects on mappings --- src/ast_util.ml | 22 +++++++++++--------- src/initial_check.ml | 2 +- src/jib/jib_optimize.ml | 1 + src/monomorphise.ml | 6 +++--- src/ocaml_backend.ml | 4 ++-- src/parse_ast.ml | 8 ++++---- src/parser.mly | 8 ++++++-- src/pretty_print_sail.ml | 9 +++++--- src/rewrites.ml | 4 ++-- src/slice.ml | 2 +- src/spec_analysis.ml | 6 +++--- src/specialize.ml | 12 +++++------ src/type_check.ml | 53 ++++++++++++++++++++++++------------------------ 13 files changed, 74 insertions(+), 63 deletions(-) (limited to 'src') diff --git a/src/ast_util.ml b/src/ast_util.ml index d00120de..8d06b23e 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -847,7 +847,7 @@ and string_of_typ_aux = function | Typ_fn (typ_args, typ_ret, eff) -> "(" ^ string_of_list ", " string_of_typ typ_args ^ ") -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff - | Typ_bidir (typ1, typ2) -> string_of_typ typ1 ^ " <-> " ^ string_of_typ typ2 + | Typ_bidir (typ1, typ2, eff) -> string_of_typ typ1 ^ " <-> " ^ string_of_typ typ2 ^ " effect " ^ string_of_effect eff | Typ_exist (kids, nc, typ) -> "{" ^ string_of_list " " string_of_kinded_id kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ ^ "}" and string_of_typ_arg = function @@ -1170,10 +1170,12 @@ and typ_compare (Typ_aux (t1,_)) (Typ_aux (t2,_)) = | 0 -> effect_compare e1 e2 | n -> n) | n -> n) - | Typ_bidir (t1,t2), Typ_bidir (t3,t4) -> + | Typ_bidir (t1,t2,e1), Typ_bidir (t3,t4,e2) -> (match typ_compare t1 t3 with - | 0 -> typ_compare t2 t3 - | n -> n) + | 0 -> (match typ_compare t2 t4 with + | 0 -> effect_compare e1 e2 + | n -> n) + | n -> n) | Typ_tup ts1, Typ_tup ts2 -> Util.compare_list typ_compare ts1 ts2 | Typ_exist (ks1,nc1,t1), Typ_exist (ks2,nc2,t2) -> (match Util.compare_list KOpt.compare ks1 ks2 with @@ -1378,7 +1380,7 @@ and kopts_of_typ (Typ_aux (t,_)) = | Typ_id _ -> KOptSet.empty | Typ_var kid -> KOptSet.singleton (mk_kopt K_type kid) | Typ_fn (ts, t, _) -> List.fold_left KOptSet.union (kopts_of_typ t) (List.map kopts_of_typ ts) - | Typ_bidir (t1, t2) -> KOptSet.union (kopts_of_typ t1) (kopts_of_typ t2) + | Typ_bidir (t1, t2, _) -> KOptSet.union (kopts_of_typ t1) (kopts_of_typ t2) | Typ_tup ts -> List.fold_left (fun s t -> KOptSet.union s (kopts_of_typ t)) KOptSet.empty ts @@ -1438,11 +1440,11 @@ and tyvars_of_typ (Typ_aux (t,_)) = | Typ_id _ -> KidSet.empty | Typ_var kid -> KidSet.singleton kid | Typ_fn (ts, t, _) -> List.fold_left KidSet.union (tyvars_of_typ t) (List.map tyvars_of_typ ts) - | Typ_bidir (t1, t2) -> KidSet.union (tyvars_of_typ t1) (tyvars_of_typ t2) + | Typ_bidir (t1, t2, _) -> KidSet.union (tyvars_of_typ t1) (tyvars_of_typ t2) | Typ_tup ts -> List.fold_left (fun s t -> KidSet.union s (tyvars_of_typ t)) KidSet.empty ts - | Typ_app (_,tas) -> + | Typ_app (_,tas) -> List.fold_left (fun s ta -> KidSet.union s (tyvars_of_typ_arg ta)) KidSet.empty tas | Typ_exist (kids, nc, t) -> @@ -1761,7 +1763,7 @@ and locate_typ f (Typ_aux (typ_aux, l)) = | Typ_var kid -> Typ_var (locate_kid f kid) | Typ_fn (arg_typs, ret_typ, effect) -> Typ_fn (List.map (locate_typ f) arg_typs, locate_typ f ret_typ, locate_effect f effect) - | Typ_bidir (typ1, typ2) -> Typ_bidir (locate_typ f typ1, locate_typ f typ2) + | Typ_bidir (typ1, typ2, effect) -> Typ_bidir (locate_typ f typ1, locate_typ f typ2, locate_effect f effect) | Typ_tup typs -> Typ_tup (List.map (locate_typ f) typs) | Typ_exist (kopts, constr, typ) -> Typ_exist (List.map (locate_kinded_id f) kopts, locate_nc f constr, locate_typ f typ) | Typ_app (id, typ_args) -> Typ_app (locate_id f id, List.map (locate_typ_arg f) typ_args) @@ -1980,7 +1982,7 @@ and typ_subst_aux sv subst = function | _ -> Typ_var kid end | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst sv subst) arg_typs, typ_subst sv subst ret_typ, effs) - | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst sv subst typ1, typ_subst sv subst typ2) + | Typ_bidir (typ1, typ2, effs) -> Typ_bidir (typ_subst sv subst typ1, typ_subst sv subst typ2, effs) | Typ_tup typs -> Typ_tup (List.map (typ_subst sv subst) typs) | Typ_app (f, args) -> Typ_app (f, List.map (typ_arg_subst sv subst) args) | Typ_exist (kopts, nc, typ) when KidSet.mem sv (KidSet.of_list (List.map kopt_kid kopts)) -> @@ -2078,7 +2080,7 @@ let subst_kids_nc, subst_kids_typ, subst_kids_typ_arg = | Typ_var _ -> ty | Typ_fn (t1,t2,e) -> re (Typ_fn (List.map (s_styp substs) t1, s_styp substs t2,e)) - | Typ_bidir (t1, t2) -> re (Typ_bidir (s_styp substs t1, s_styp substs t2)) + | Typ_bidir (t1,t2,e) -> re (Typ_bidir (s_styp substs t1, s_styp substs t2,e)) | Typ_tup ts -> re (Typ_tup (List.map (s_styp substs) ts)) | Typ_app (id,tas) -> re (Typ_app (id,List.map (s_starg substs) tas)) | Typ_exist (kopts,nc,t) -> diff --git a/src/initial_check.ml b/src/initial_check.ml index 7012e915..f808af49 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -153,7 +153,7 @@ let rec to_ast_typ ctx (P.ATyp_aux (aux, l)) = | _ -> [to_ast_typ ctx from_typ] in Typ_fn (from_typs, to_ast_typ ctx to_typ, to_ast_effects effects) - | P.ATyp_bidir (typ1, typ2) -> Typ_bidir (to_ast_typ ctx typ1, to_ast_typ ctx typ2) + | P.ATyp_bidir (typ1, typ2, effects) -> Typ_bidir (to_ast_typ ctx typ1, to_ast_typ ctx typ2, to_ast_effects effects) | P.ATyp_tup typs -> Typ_tup (List.map (to_ast_typ ctx) typs) | P.ATyp_app (P.Id_aux (P.Id "int", il), [n]) -> Typ_app (Id_aux (Id "atom", il), [to_ast_typ_arg ctx n K_int]) diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml index 75ef8a19..874835b1 100644 --- a/src/jib/jib_optimize.ml +++ b/src/jib/jib_optimize.ml @@ -247,6 +247,7 @@ let ssa_name i = function | Name (id, _) -> Name (id, i) | Have_exception _ -> Have_exception i | Current_exception _ -> Current_exception i + | Throw_location _ -> Throw_location i | Return _ -> Return i let inline cdefs should_inline instrs = diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 645f6f72..e328cce1 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -219,7 +219,7 @@ let rec contains_exist (Typ_aux (ty,l)) = | Typ_var _ -> false | Typ_fn (t1,t2,_) -> List.exists contains_exist t1 || contains_exist t2 - | Typ_bidir (t1, t2) -> contains_exist t1 || contains_exist t2 + | Typ_bidir (t1, t2, _) -> contains_exist t1 || contains_exist t2 | Typ_tup ts -> List.exists contains_exist ts | Typ_app (_,args) -> List.exists contains_exist_arg args | Typ_exist _ -> true @@ -3530,10 +3530,10 @@ let replace_nexp_in_typ env typ orig new_nexp = let f1 = List.exists fst arg' in let f2, res = aux res in f1 || f2, Typ_aux (Typ_fn (List.map snd arg', res, eff),l) - | Typ_bidir (t1, t2) -> + | Typ_bidir (t1, t2, eff) -> let f1, t1 = aux t1 in let f2, t2 = aux t2 in - f1 || f2, Typ_aux (Typ_bidir (t1, t2), l) + f1 || f2, Typ_aux (Typ_bidir (t1, t2, eff), l) | Typ_tup typs -> let fs, typs = List.split (List.map aux typs) in List.exists (fun x -> x) fs, Typ_aux (Typ_tup typs,l) diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 8899695f..98a43ebc 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -118,7 +118,7 @@ let rec ocaml_string_typ (Typ_aux (typ_aux, l)) arg = parens (separate space [string "fun"; parens (separate (comma ^^ space) args); string "->"; body]) ^^ space ^^ arg | Typ_fn (typ1, typ2, _) -> string "\"FN\"" - | Typ_bidir (t1, t2) -> string "\"BIDIR\"" + | Typ_bidir (t1, t2, _) -> string "\"BIDIR\"" | Typ_var kid -> string "\"VAR\"" | Typ_exist _ -> assert false | Typ_internal_unknown -> raise (Reporting.err_unreachable l __POS__ "escaped Typ_internal_unknown") @@ -144,7 +144,7 @@ let rec ocaml_typ ctx (Typ_aux (typ_aux, l)) = | Typ_app (id, typs) -> parens (separate_map (string ", ") (ocaml_typ_arg ctx) typs) ^^ space ^^ ocaml_typ_id ctx id | Typ_tup typs -> parens (separate_map (string " * ") (ocaml_typ ctx) typs) | Typ_fn (typs, typ, _) -> separate space [ocaml_typ ctx (Typ_aux (Typ_tup typs, l)); string "->"; ocaml_typ ctx typ] - | Typ_bidir (t1, t2) -> raise (Reporting.err_general l "Ocaml doesn't support bidir types") + | Typ_bidir _ -> raise (Reporting.err_general l "Ocaml doesn't support bidir types") | Typ_var kid -> zencode_kid kid | Typ_exist _ -> assert false | Typ_internal_unknown -> raise (Reporting.err_unreachable l __POS__ "escaped Typ_internal_unknown") diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 3147b7f4..6cb3f84d 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -154,12 +154,12 @@ atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders | ATyp_minus of atyp * atyp (* subtraction *) | ATyp_exp of atyp (* exponential *) | ATyp_neg of atyp (* Internal (but not M as I want a datatype constructor) negative nexp *) - | ATyp_inc (* increasing (little-endian) *) - | ATyp_dec (* decreasing (big-endian) *) + | ATyp_inc (* increasing *) + | ATyp_dec (* decreasing *) | ATyp_default_ord (* default order for increasing or decreasing signficant bits *) | ATyp_set of (base_effect) list (* effect set *) - | ATyp_fn of atyp * atyp * atyp (* Function type (first-order only in user code), last atyp is an effect *) - | ATyp_bidir of atyp * atyp (* Function type (first-order only in user code), last atyp is an effect *) + | ATyp_fn of atyp * atyp * atyp (* Function type, last atyp is an effect *) + | ATyp_bidir of atyp * atyp * atyp (* Mapping type, last atyp is an effect *) | ATyp_wild | ATyp_tup of (atyp) list (* Tuple type *) | ATyp_app of id * (atyp) list (* type constructor application *) diff --git a/src/parser.mly b/src/parser.mly index 0b09468c..6a579b7a 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -657,9 +657,13 @@ typschm: | Forall typquant Dot typ MinusGt typ Effect effect_set { (fun s e -> mk_typschm $2 (mk_typ (ATyp_fn ($4, $6, $8)) s e) s e) $startpos $endpos } | typ Bidir typ - { (fun s e -> mk_typschm mk_typqn (mk_typ (ATyp_bidir ($1, $3)) s e) s e) $startpos $endpos } + { (fun s e -> mk_typschm mk_typqn (mk_typ (ATyp_bidir ($1, $3, mk_typ (ATyp_set []) s e)) s e) s e) $startpos $endpos } | Forall typquant Dot typ Bidir typ - { (fun s e -> mk_typschm $2 (mk_typ (ATyp_bidir ($4, $6)) s e) s e) $startpos $endpos } + { (fun s e -> mk_typschm $2 (mk_typ (ATyp_bidir ($4, $6, mk_typ (ATyp_set []) s e)) s e) s e) $startpos $endpos } + | typ Bidir typ Effect effect_set + { (fun s e -> mk_typschm mk_typqn (mk_typ (ATyp_bidir ($1, $3, $5)) s e) s e) $startpos $endpos } + | Forall typquant Dot typ Bidir typ Effect effect_set + { (fun s e -> mk_typschm $2 (mk_typ (ATyp_bidir ($4, $6, $8)) s e) s e) $startpos $endpos } typschm_eof: | typschm Eof diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 322c60b7..7e98f4e3 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -170,6 +170,8 @@ let rec doc_nc nc = in atomic_nc (constraint_simp nc) +and doc_effects effs = braces (separate (comma ^^ space) (List.map (fun be -> string (string_of_base_effect be)) effs)) + and doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) = match typ_aux with | Typ_id id -> doc_id id @@ -194,13 +196,14 @@ and doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) = | Typ_fn (typs, typ, Effect_aux (Effect_set [], _)) -> separate space [doc_arg_typs typs; string "->"; doc_typ typ] | Typ_fn (typs, typ, Effect_aux (Effect_set effs, _)) -> - let ocaml_eff = braces (separate (comma ^^ space) (List.map (fun be -> string (string_of_base_effect be)) effs)) in if simple then separate space [doc_arg_typs typs; string "->"; doc_typ ~simple:simple typ] else - separate space [doc_arg_typs typs; string "->"; doc_typ typ; string "effect"; ocaml_eff] - | Typ_bidir (typ1, typ2) -> + separate space [doc_arg_typs typs; string "->"; doc_typ typ; string "effect"; doc_effects effs] + | Typ_bidir (typ1, typ2, Effect_aux (Effect_set [], _)) -> separate space [doc_typ typ1; string "<->"; doc_typ typ2] + | Typ_bidir (typ1, typ2, Effect_aux (Effect_set effs, _)) -> + separate space [doc_typ typ1; string "<->"; doc_typ typ2; string "effect"; doc_effects effs] | Typ_internal_unknown -> raise (Reporting.err_unreachable l __POS__ "escaped Typ_internal_unknown") and doc_typ_arg (A_aux (ta_aux, _)) = match ta_aux with diff --git a/src/rewrites.ml b/src/rewrites.ml index 20a1b336..35811b26 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -3133,7 +3133,7 @@ let rewrite_defs_mapping_patterns env = let x = Env.get_val_spec mapping_id env in let typ1, typ2 = match x with - | (_, Typ_aux(Typ_bidir(typ1, typ2), _)) -> typ1, typ2 + | (_, Typ_aux(Typ_bidir(typ1, typ2, _), _)) -> typ1, typ2 | (_, typ) -> raise (Reporting.err_unreachable (fst p_annot) __POS__ ("Must be bi-directional mapping: " ^ string_of_typ typ)) in @@ -3951,7 +3951,7 @@ let rewrite_defs_realise_mappings _ (Defs defs) = in let (typq, bidir_typ) = Env.get_val_spec id env in let (typ1, typ2, l) = match bidir_typ with - | Typ_aux (Typ_bidir (typ1, typ2), l) -> typ1, typ2, l + | Typ_aux (Typ_bidir (typ1, typ2, _), l) -> typ1, typ2, l | _ -> raise (Reporting.err_unreachable l __POS__ "non-bidir type of mapping?") in let forwards_typ = Typ_aux (Typ_fn ([typ1], typ2, no_effect), l) in diff --git a/src/slice.ml b/src/slice.ml index a38a207c..c249fb5a 100644 --- a/src/slice.ml +++ b/src/slice.ml @@ -130,7 +130,7 @@ and typ_ids' (Typ_aux (aux, _)) = IdSet.add id (List.fold_left IdSet.union IdSet.empty (List.map typ_arg_ids' args)) | Typ_fn (typs, typ, _) -> IdSet.union (typ_ids' typ) (List.fold_left IdSet.union IdSet.empty (List.map typ_ids' typs)) - | Typ_bidir (typ1, typ2) -> + | Typ_bidir (typ1, typ2, _) -> IdSet.union (typ_ids' typ1) (typ_ids' typ2) | Typ_tup typs -> List.fold_left IdSet.union IdSet.empty (List.map typ_ids' typs) diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index 40855eec..75f2ff6e 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -89,8 +89,8 @@ let rec free_type_names_t consider_var (Typ_aux (t, l)) = match t with | Typ_id name -> Nameset.add (string_of_id name) mt | Typ_fn (arg_typs,ret_typ,_) -> List.fold_left Nameset.union (free_type_names_t consider_var ret_typ) (List.map (free_type_names_t consider_var) arg_typs) - | Typ_bidir (t1, t2) -> Nameset.union (free_type_names_t consider_var t1) - (free_type_names_t consider_var t2) + | Typ_bidir (t1,t2,_) -> Nameset.union (free_type_names_t consider_var t1) + (free_type_names_t consider_var t2) | Typ_tup ts -> free_type_names_ts consider_var ts | Typ_app (name,targs) -> Nameset.add (string_of_id name) (free_type_names_t_args consider_var targs) | Typ_exist (kopts,_,t') -> List.fold_left (fun s kopt -> Nameset.remove (string_of_kid (kopt_kid kopt)) s) (free_type_names_t consider_var t') kopts @@ -121,7 +121,7 @@ let rec fv_of_typ consider_var bound used (Typ_aux (t,l)) : Nameset.t = | Typ_id id -> conditional_add_typ bound used id | Typ_fn(arg,ret,_) -> fv_of_typ consider_var bound (List.fold_left Nameset.union Nameset.empty (List.map (fv_of_typ consider_var bound used) arg)) ret - | Typ_bidir(t1, t2) -> fv_of_typ consider_var bound (fv_of_typ consider_var bound used t1) t2 (* TODO FIXME? *) + | Typ_bidir(t1,t2,_) -> fv_of_typ consider_var bound (fv_of_typ consider_var bound used t1) t2 (* TODO FIXME? *) | Typ_tup ts -> List.fold_right (fun t n -> fv_of_typ consider_var bound n t) ts used | Typ_app(id,targs) -> List.fold_right (fun ta n -> fv_of_targ consider_var bound n ta) targs (conditional_add_typ bound used id) diff --git a/src/specialize.ml b/src/specialize.ml index e2b0075d..d705b83a 100644 --- a/src/specialize.ml +++ b/src/specialize.ml @@ -92,7 +92,7 @@ let rec nexp_simp_typ (Typ_aux (typ_aux, l)) = | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc, nexp_simp_typ typ) | Typ_fn (arg_typs, ret_typ, effect) -> Typ_fn (List.map nexp_simp_typ arg_typs, nexp_simp_typ ret_typ, effect) - | Typ_bidir (t1, t2) -> Typ_bidir (nexp_simp_typ t1, nexp_simp_typ t2) + | Typ_bidir (t1, t2, effect) -> Typ_bidir (nexp_simp_typ t1, nexp_simp_typ t2, effect) | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown" in Typ_aux (typ_aux, l) @@ -170,8 +170,8 @@ let string_of_instantiation instantiation = | Typ_app (id, args) -> string_of_id id ^ "(" ^ Util.string_of_list "," string_of_typ_arg args ^ ")" | Typ_fn (arg_typs, ret_typ, eff) -> "(" ^ Util.string_of_list ", " string_of_typ arg_typs ^ ") -> " ^ string_of_typ ret_typ ^ " effect " ^ string_of_effect eff - | Typ_bidir (t1, t2) -> - string_of_typ t1 ^ " <-> " ^ string_of_typ t2 + | Typ_bidir (t1, t2, eff) -> + string_of_typ t1 ^ " <-> " ^ string_of_typ t2 ^ " effect " ^ string_of_effect eff | Typ_exist (kids, nc, typ) -> "exist " ^ Util.string_of_list " " kid_name kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ | Typ_internal_unknown -> "UNKNOWN" @@ -290,7 +290,7 @@ let rec typ_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) = | Typ_exist (kopts, nc, typ) -> typ_frees ~exs:(KidSet.of_list (List.map kopt_kid kopts)) typ | Typ_fn (arg_typs, ret_typ, _) -> List.fold_left KidSet.union (typ_frees ~exs:exs ret_typ) (List.map (typ_frees ~exs:exs) arg_typs) - | Typ_bidir (t1, t2) -> KidSet.union (typ_frees ~exs:exs t1) (typ_frees ~exs:exs t2) + | Typ_bidir (t1, t2, _) -> KidSet.union (typ_frees ~exs:exs t1) (typ_frees ~exs:exs t2) | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown" and typ_arg_frees ?exs:(exs=KidSet.empty) (A_aux (typ_arg_aux, l)) = match typ_arg_aux with @@ -308,7 +308,7 @@ let rec typ_int_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) = | Typ_exist (kopts, nc, typ) -> typ_int_frees ~exs:(KidSet.of_list (List.map kopt_kid kopts)) typ | Typ_fn (arg_typs, ret_typ, _) -> List.fold_left KidSet.union (typ_int_frees ~exs:exs ret_typ) (List.map (typ_int_frees ~exs:exs) arg_typs) - | Typ_bidir (t1, t2) -> KidSet.union (typ_int_frees ~exs:exs t1) (typ_int_frees ~exs:exs t2) + | Typ_bidir (t1, t2, _) -> KidSet.union (typ_int_frees ~exs:exs t1) (typ_int_frees ~exs:exs t2) | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown" and typ_arg_int_frees ?exs:(exs=KidSet.empty) (A_aux (typ_arg_aux, l)) = match typ_arg_aux with @@ -325,7 +325,7 @@ let rec remove_implicit (Typ_aux (aux, l) as t) = | Typ_internal_unknown -> Typ_aux (Typ_internal_unknown, l) | Typ_tup typs -> Typ_aux (Typ_tup (List.map remove_implicit typs), l) | Typ_fn (arg_typs, ret_typ, effs) -> Typ_aux (Typ_fn (List.map remove_implicit arg_typs, remove_implicit ret_typ, effs), l) - | Typ_bidir (typ1, typ2) -> Typ_aux (Typ_bidir (remove_implicit typ1, remove_implicit typ2), l) + | Typ_bidir (typ1, typ2, effs) -> Typ_aux (Typ_bidir (remove_implicit typ1, remove_implicit typ2, effs), l) | Typ_app (Id_aux (Id "implicit", _), args) -> Typ_aux (Typ_app (mk_id "atom", List.map remove_implicit_arg args), l) | Typ_app (id, args) -> Typ_aux (Typ_app (id, List.map remove_implicit_arg args), l) | Typ_id id -> Typ_aux (Typ_id id, l) diff --git a/src/type_check.ml b/src/type_check.ml index 2ba2166c..0871272b 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -238,7 +238,7 @@ and strip_typ_aux : typ_aux -> typ_aux = function | Typ_id id -> Typ_id (strip_id id) | Typ_var kid -> Typ_var (strip_kid kid) | Typ_fn (arg_typs, ret_typ, effect) -> Typ_fn (List.map strip_typ arg_typs, strip_typ ret_typ, strip_effect effect) - | Typ_bidir (typ1, typ2) -> Typ_bidir (strip_typ typ1, strip_typ typ2) + | Typ_bidir (typ1, typ2, effect) -> Typ_bidir (strip_typ typ1, strip_typ typ2, strip_effect effect) | Typ_tup typs -> Typ_tup (List.map strip_typ typs) | Typ_exist (kopts, constr, typ) -> Typ_exist ((List.map strip_kinded_id kopts), strip_n_constraint constr, strip_typ typ) @@ -272,7 +272,7 @@ let rec typ_constraints (Typ_aux (typ_aux, l)) = | Typ_exist (kids, nc, typ) -> typ_constraints typ | Typ_fn (arg_typs, ret_typ, _) -> List.concat (List.map typ_constraints arg_typs) @ typ_constraints ret_typ - | Typ_bidir (typ1, typ2) -> + | Typ_bidir (typ1, typ2, _) -> typ_constraints typ1 @ typ_constraints typ2 and typ_arg_nexps (A_aux (typ_arg_aux, l)) = match typ_arg_aux with @@ -291,7 +291,7 @@ let rec typ_nexps (Typ_aux (typ_aux, l)) = | Typ_exist (kids, nc, typ) -> typ_nexps typ | Typ_fn (arg_typs, ret_typ, _) -> List.concat (List.map typ_nexps arg_typs) @ typ_nexps ret_typ - | Typ_bidir (typ1, typ2) -> + | Typ_bidir (typ1, typ2, _) -> typ_nexps typ1 @ typ_nexps typ2 and typ_arg_nexps (A_aux (typ_arg_aux, l)) = match typ_arg_aux with @@ -427,7 +427,7 @@ module Env : sig val add_variant_clause : id -> type_union -> t -> t val get_variant : id -> t -> typquant * type_union list val get_scattered_variant_env : id -> t -> t - val add_mapping : id -> typquant * typ * typ -> t -> t + val add_mapping : id -> typquant * typ * typ * effect -> t -> t val add_union_id : id -> typquant * typ -> t -> t val get_union_id : id -> t -> typquant * typ val is_register : id -> t -> bool @@ -573,8 +573,8 @@ end = struct let builtin_mappings = List.fold_left (fun m (name, typ) -> Bindings.add (mk_id name) typ m) Bindings.empty [ - ("int", Typ_bidir(int_typ, string_typ)); - ("nat", Typ_bidir(nat_typ, string_typ)); + ("int", Typ_bidir(int_typ, string_typ, no_effect)); + ("nat", Typ_bidir(nat_typ, string_typ, no_effect)); ] let bound_typ_id env id = @@ -725,7 +725,7 @@ end = struct | 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 (arg_typs, ret_typ, effs) -> Typ_aux (Typ_fn (List.map (expand_synonyms env) arg_typs, expand_synonyms env ret_typ, effs), l) - | Typ_bidir (typ1, typ2) -> Typ_aux (Typ_bidir (expand_synonyms env typ1, expand_synonyms env typ2), l) + | Typ_bidir (typ1, typ2, effs) -> Typ_aux (Typ_bidir (expand_synonyms env typ1, expand_synonyms env typ2, effs), l) | Typ_app (id, args) -> (try begin match get_typ_synonym id env l env args with @@ -786,7 +786,7 @@ end = struct | Typ_internal_unknown | Typ_id _ | Typ_var _ -> typ | Typ_fn (arg_typs, ret_typ, effect) -> Typ_aux (Typ_fn (List.map (map_nexps f) arg_typs, map_nexps f ret_typ, effect), l) - | Typ_bidir (typ1, typ2) -> Typ_aux (Typ_bidir (map_nexps f typ1, map_nexps f typ2), l) + | Typ_bidir (typ1, typ2, effect) -> Typ_aux (Typ_bidir (map_nexps f typ1, map_nexps f typ2, effect), l) | Typ_tup typs -> Typ_aux (Typ_tup (List.map (map_nexps f) typs), l) | Typ_exist (kids, nc, typ) -> Typ_aux (Typ_exist (kids, nc, map_nexps f typ), l) | Typ_app (id, args) -> Typ_aux (Typ_app (id, List.map (map_nexps_arg f) args), l) @@ -819,9 +819,9 @@ end = struct typ_error env l ("Unbound type variable " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ) end | Typ_fn (arg_typs, ret_typ, effs) -> List.iter (wf_typ ~exs:exs env) arg_typs; wf_typ ~exs:exs env ret_typ - | Typ_bidir (typ1, typ2) when strip_typ typ1 = strip_typ typ2 -> + | Typ_bidir (typ1, typ2, _) when strip_typ typ1 = strip_typ typ2 -> typ_error env l "Bidirectional types cannot be the same on both sides" - | Typ_bidir (typ1, typ2) -> wf_typ ~exs:exs env typ1; wf_typ ~exs:exs env typ2 + | Typ_bidir (typ1, typ2, _) -> wf_typ ~exs:exs env typ1; wf_typ ~exs:exs env typ2 | Typ_tup typs -> List.iter (wf_typ ~exs:exs env) typs | Typ_app (id, [A_aux (A_nexp _, _) as arg]) when string_of_id id = "implicit" -> wf_typ_arg ~exs:exs env arg @@ -979,8 +979,8 @@ end = struct typ_print (lazy (adding ^ "val " ^ string_of_id id ^ " : " ^ string_of_bind (typq, typ))); { env with top_val_specs = Bindings.add id (typq, typ) env.top_val_specs } - | Typ_aux (Typ_bidir (typ1, typ2), l) -> - let env = add_mapping id (typq, typ1, typ2) env in + | Typ_aux (Typ_bidir (typ1, typ2, effect), l) -> + let env = add_mapping id (typq, typ1, typ2, effect) env in typ_print (lazy (adding ^ "mapping " ^ string_of_id id ^ " : " ^ string_of_bind (typq, typ))); { env with top_val_specs = Bindings.add id (typq, typ) env.top_val_specs } @@ -1002,16 +1002,16 @@ end = struct env *) - and add_mapping id (typq, typ1, typ2) env = + and add_mapping id (typq, typ1, typ2, effect) env = typ_print (lazy (adding ^ "mapping " ^ string_of_id id)); let forwards_id = mk_id (string_of_id id ^ "_forwards") in let forwards_matches_id = mk_id (string_of_id id ^ "_forwards_matches") in let backwards_id = mk_id (string_of_id id ^ "_backwards") in let backwards_matches_id = mk_id (string_of_id id ^ "_backwards_matches") in - let forwards_typ = Typ_aux (Typ_fn ([typ1], typ2, no_effect), Parse_ast.Unknown) in - let forwards_matches_typ = Typ_aux (Typ_fn ([typ1], bool_typ, no_effect), Parse_ast.Unknown) in - let backwards_typ = Typ_aux (Typ_fn ([typ2], typ1, no_effect), Parse_ast.Unknown) in - let backwards_matches_typ = Typ_aux (Typ_fn ([typ2], bool_typ, no_effect), Parse_ast.Unknown) in + let forwards_typ = Typ_aux (Typ_fn ([typ1], typ2, effect), Parse_ast.Unknown) in + let forwards_matches_typ = Typ_aux (Typ_fn ([typ1], bool_typ, effect), Parse_ast.Unknown) in + let backwards_typ = Typ_aux (Typ_fn ([typ2], typ1, effect), Parse_ast.Unknown) in + let backwards_matches_typ = Typ_aux (Typ_fn ([typ2], bool_typ, effect), Parse_ast.Unknown) in let env = { env with mappings = Bindings.add id (typq, typ1, typ2) env.mappings } |> add_val_spec forwards_id (typq, forwards_typ) @@ -1451,7 +1451,7 @@ let rec is_typ_monomorphic (Typ_aux (typ, l)) = | Typ_tup typs -> List.for_all is_typ_monomorphic typs | Typ_app (id, args) -> List.for_all is_typ_arg_monomorphic args | Typ_fn (arg_typs, ret_typ, _) -> List.for_all is_typ_monomorphic arg_typs && is_typ_monomorphic ret_typ - | Typ_bidir (typ1, typ2) -> is_typ_monomorphic typ1 && is_typ_monomorphic typ2 + | Typ_bidir (typ1, typ2, _) -> is_typ_monomorphic typ1 && is_typ_monomorphic typ2 | Typ_exist _ | Typ_var _ -> false | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown" and is_typ_arg_monomorphic (A_aux (arg, _)) = @@ -1650,9 +1650,10 @@ and typ_identical (Typ_aux (typ1, _)) (Typ_aux (typ2, _)) = List.for_all2 typ_identical arg_typs1 arg_typs2 && typ_identical ret_typ1 ret_typ2 && strip_effect eff1 = strip_effect eff2 - | Typ_bidir (typ1, typ2), Typ_bidir (typ3, typ4) -> + | Typ_bidir (typ1, typ2, eff1), Typ_bidir (typ3, typ4, eff2) -> typ_identical typ1 typ3 && typ_identical typ2 typ4 + && strip_effect eff1 = strip_effect eff2 | Typ_tup typs1, Typ_tup typs2 -> begin try List.for_all2 typ_identical typs1 typs2 with @@ -2050,7 +2051,7 @@ let rec alpha_equivalent env typ1 typ2 = | Typ_internal_unknown -> Typ_internal_unknown | Typ_id _ | Typ_var _ -> aux | Typ_fn (arg_typs, ret_typ, eff) -> Typ_fn (List.map relabel arg_typs, relabel ret_typ, eff) - | Typ_bidir (typ1, typ2) -> Typ_bidir (relabel typ1, relabel typ2) + | Typ_bidir (typ1, typ2, eff) -> Typ_bidir (relabel typ1, relabel typ2, eff) | Typ_tup typs -> Typ_tup (List.map relabel typs) | Typ_exist (kopts, nc, typ) -> let kind_map = List.fold_left (fun m kopt -> KBindings.add (kopt_kid kopt) (kopt_kind kopt) m) KBindings.empty kopts in @@ -3310,7 +3311,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) | _ -> [typ] in match Env.expand_synonyms env mapping_typ with - | Typ_aux (Typ_bidir (typ1, typ2), _) -> + | Typ_aux (Typ_bidir (typ1, typ2, _), _) -> begin try typ_debug (lazy ("Unifying " ^ string_of_bind (typq, mapping_typ) ^ " for pattern " ^ string_of_typ typ)); @@ -3404,7 +3405,7 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) = begin let (typq, mapping_typ) = Env.get_val_spec f env in match Env.expand_synonyms env mapping_typ with - | Typ_aux (Typ_bidir (typ1, typ2), _) -> + | Typ_aux (Typ_bidir (typ1, typ2, _), _) -> begin try bind_pat env pat typ2 @@ -4242,7 +4243,7 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) ( | _ -> [typ] in match Env.expand_synonyms env mapping_typ with - | Typ_aux (Typ_bidir (typ1, typ2), _) -> + | Typ_aux (Typ_bidir (typ1, typ2, _), _) -> begin try typ_debug (lazy ("Unifying " ^ string_of_bind (typq, mapping_typ) ^ " for mapping-pattern " ^ string_of_typ typ)); @@ -4341,7 +4342,7 @@ and infer_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) begin let (typq, mapping_typ) = Env.get_val_spec f env in match Env.expand_synonyms env mapping_typ with - | Typ_aux (Typ_bidir (typ1, typ2), _) -> + | Typ_aux (Typ_bidir (typ1, typ2, _), _) -> begin try bind_mpat allow_unknown other_env env mpat typ2 @@ -4835,7 +4836,7 @@ 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 (cl, (l, _))) typ -> match typ with - | Typ_aux (Typ_bidir (typ1, typ2), _) -> begin + | 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 @@ -5000,7 +5001,7 @@ let check_mapdef env (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, _)) as md raise err in let vtyp1, vtyp2, vl = match typ with - | Typ_aux (Typ_bidir (vtyp1, vtyp2), vl) -> vtyp1, vtyp2, vl + | Typ_aux (Typ_bidir (vtyp1, vtyp2, _), vl) -> vtyp1, vtyp2, vl | _ -> typ_error env l "Mapping val spec was not a mapping type" in begin match tannot_opt with -- cgit v1.2.3