diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast.ml | 1 | ||||
| -rw-r--r-- | src/ast_util.ml | 1 | ||||
| -rw-r--r-- | src/initial_check.ml | 1 | ||||
| -rw-r--r-- | src/monomorphise.ml | 3 | ||||
| -rw-r--r-- | src/pretty_print_common.ml | 1 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 1 | ||||
| -rw-r--r-- | src/pretty_print_lem_ast.ml | 3 | ||||
| -rw-r--r-- | src/pretty_print_ocaml.ml | 1 | ||||
| -rw-r--r-- | src/type_check.ml | 9 |
9 files changed, 2 insertions, 19 deletions
@@ -238,7 +238,6 @@ and typ_arg_aux = (* Type constructor arguments of all kinds *) Typ_arg_nexp of nexp | Typ_arg_typ of typ | Typ_arg_order of order - | Typ_arg_effect of effect and typ_arg = Typ_arg_aux of typ_arg_aux * l diff --git a/src/ast_util.ml b/src/ast_util.ml index 8071ee7d..0c6461d1 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -222,7 +222,6 @@ and string_of_typ_arg_aux = function | Typ_arg_nexp n -> string_of_nexp n | Typ_arg_typ typ -> string_of_typ typ | Typ_arg_order o -> string_of_order o - | Typ_arg_effect eff -> string_of_effect eff and string_of_n_constraint = function | NC_aux (NC_fixed (n1, n2), _) -> string_of_nexp n1 ^ " = " ^ string_of_nexp n2 | NC_aux (NC_not_equal (n1, n2), _) -> string_of_nexp n1 ^ " != " ^ string_of_nexp n2 diff --git a/src/initial_check.ml b/src/initial_check.ml index aeca186d..357ed100 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -301,7 +301,6 @@ and to_ast_typ_arg (k_env : kind Envmap.t) (def_ord : order) (kind : kind) (arg | K_Typ -> Typ_arg_typ (to_ast_typ k_env def_ord arg) | K_Nat -> Typ_arg_nexp (to_ast_nexp k_env arg) | K_Ord -> Typ_arg_order (to_ast_order k_env def_ord arg) - | K_Efct -> Typ_arg_effect (to_ast_effects k_env arg) | _ -> raise (Reporting_basic.err_unreachable l ("To_ast_typ_arg received Lam kind or infer kind: " ^ kind_to_string kind))), l) diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 27b5237e..2849b466 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -56,8 +56,7 @@ let subst_src_typ substs t = match ta with | Typ_arg_nexp ne -> Typ_arg_aux (Typ_arg_nexp (s_snexp ne),l) | Typ_arg_typ t -> Typ_arg_aux (Typ_arg_typ (s_styp t),l) - | Typ_arg_order _ - | Typ_arg_effect _ -> targ + | Typ_arg_order _ -> targ in s_styp t let make_vector_lit sz i = diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml index bd43c1a7..70f5b749 100644 --- a/src/pretty_print_common.ml +++ b/src/pretty_print_common.ml @@ -189,7 +189,6 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint = | Typ_arg_typ t -> app_typ t | Typ_arg_nexp n -> nexp n | Typ_arg_order o -> doc_ord o - | Typ_arg_effect e -> doc_effects e (* same trick to handle precedence of nexp *) and nexp ne = sum_typ ne diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 586773ca..9b66331b 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -208,7 +208,6 @@ let doc_typ_lem, doc_atomic_typ_lem = | Typ_arg_typ t -> app_typ regtypes true t | Typ_arg_nexp n -> empty | Typ_arg_order o -> empty - | Typ_arg_effect e -> empty in typ', atomic_typ (* Check for variables in types that would be pretty-printed. diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml index 018a93f5..adddcee6 100644 --- a/src/pretty_print_lem_ast.ml +++ b/src/pretty_print_lem_ast.ml @@ -210,8 +210,7 @@ and pp_format_typ_arg_lem (Typ_arg_aux(t,l)) = (match t with | Typ_arg_typ(t) -> "(Typ_arg_typ " ^ pp_format_typ_lem t ^ ")" | Typ_arg_nexp(n) -> "(Typ_arg_nexp " ^ pp_format_nexp_lem n ^ ")" - | Typ_arg_order(o) -> "(Typ_arg_order " ^ pp_format_ord_lem o ^ ")" - | Typ_arg_effect(e) -> "(Typ_arg_effect " ^ pp_format_effects_lem e ^ ")") ^ " " ^ + | Typ_arg_order(o) -> "(Typ_arg_order " ^ pp_format_ord_lem o ^ ")"); (pp_format_l_lem l) ^ ")" and pp_format_nexp_constraint_lem (NC_aux(nc,l)) = "(NC_aux " ^ diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml index fc02f568..b331a6cf 100644 --- a/src/pretty_print_ocaml.ml +++ b/src/pretty_print_ocaml.ml @@ -121,7 +121,6 @@ let doc_typ_ocaml, doc_atomic_typ_ocaml = | Typ_arg_typ t -> app_typ t | Typ_arg_nexp n -> empty | Typ_arg_order o -> empty - | Typ_arg_effect e -> empty in typ, atomic_typ let doc_lit_ocaml in_pat (L_aux(l,_)) = diff --git a/src/type_check.ml b/src/type_check.ml index d59d4c75..2cfdb899 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -320,7 +320,6 @@ and typ_subst_arg_nexp_aux sv subst = function | Typ_arg_nexp nexp -> Typ_arg_nexp (nexp_subst sv subst nexp) | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_nexp sv subst typ) | Typ_arg_order ord -> Typ_arg_order ord - | Typ_arg_effect eff -> Typ_arg_effect eff 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 @@ -336,7 +335,6 @@ and typ_subst_arg_typ_aux sv subst = function | Typ_arg_nexp nexp -> Typ_arg_nexp nexp | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_typ sv subst typ) | Typ_arg_order ord -> Typ_arg_order ord - | Typ_arg_effect eff -> Typ_arg_effect eff let order_subst_aux sv subst = function | Ord_var kid -> if Kid.compare kid sv = 0 then subst else Ord_var kid @@ -359,7 +357,6 @@ and typ_subst_arg_order_aux sv subst = function | Typ_arg_nexp nexp -> Typ_arg_nexp nexp | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_order sv subst typ) | Typ_arg_order ord -> Typ_arg_order (order_subst sv subst ord) - | Typ_arg_effect eff -> Typ_arg_effect eff 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 @@ -376,7 +373,6 @@ and typ_subst_arg_kid_aux sv subst = function | Typ_arg_nexp nexp -> Typ_arg_nexp (nexp_subst sv (Nexp_var subst) nexp) | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_kid sv subst typ) | Typ_arg_order ord -> Typ_arg_order (order_subst sv (Ord_var subst) ord) - | Typ_arg_effect eff -> Typ_arg_effect eff let quant_item_subst_kid_aux sv subst = function | QI_id (KOpt_aux (KOpt_none kid, l)) as qid -> @@ -584,7 +580,6 @@ end = struct | Typ_arg_nexp nexp -> wf_nexp ~exs:exs env nexp | Typ_arg_typ typ -> wf_typ ~exs:exs env typ | Typ_arg_order ord -> wf_order env ord - | Typ_arg_effect _ -> () (* Check: is this ever used? *) and wf_nexp ?exs:(exs=KidSet.empty) env (Nexp_aux (nexp_aux, l)) = match nexp_aux with | Nexp_id _ -> () @@ -1075,7 +1070,6 @@ and normalize_typ_arg env (Typ_arg_aux (typ_arg, _)) = | Typ_arg_nexp n -> Tnf_arg_nexp n | Typ_arg_typ typ -> Tnf_arg_typ (normalize_typ env typ) | Typ_arg_order o -> Tnf_arg_order o - | Typ_arg_effect e -> Tnf_arg_effect e (* Here's how the constraint generation works for subtyping @@ -1260,7 +1254,6 @@ and typ_arg_frees ?exs:(exs=KidSet.empty) (Typ_arg_aux (typ_arg_aux, l)) = | Typ_arg_nexp n -> nexp_frees ~exs:exs n | Typ_arg_typ typ -> typ_frees ~exs:exs typ | Typ_arg_order ord -> order_frees ord - | Typ_arg_effect _ -> assert false let rec nexp_identical (Nexp_aux (nexp1, _)) (Nexp_aux (nexp2, _)) = match nexp1, nexp2 with @@ -1302,7 +1295,6 @@ and typ_arg_identical (Typ_arg_aux (arg1, _)) (Typ_arg_aux (arg2, _)) = | Typ_arg_nexp n1, Typ_arg_nexp n2 -> nexp_identical n1 n2 | Typ_arg_typ typ1, Typ_arg_typ typ2 -> typ_identical typ1 typ2 | Typ_arg_order ord1, Typ_arg_order ord2 -> ord_identical ord1 ord2 - | Typ_arg_effect _, Typ_arg_effect _ -> assert false type uvar = | U_nexp of nexp @@ -1477,7 +1469,6 @@ let rec unify l env typ1 typ2 = end | Typ_arg_typ typ1, Typ_arg_typ typ2 -> unify_typ l typ1 typ2 | Typ_arg_order ord1, Typ_arg_order ord2 -> unify_order l ord1 ord2 - | Typ_arg_effect _, Typ_arg_effect _ -> assert false | _, _ -> unify_error l (string_of_typ_arg typ_arg1 ^ " cannot be unified with type argument " ^ string_of_typ_arg typ_arg2) in match destruct_exist env typ2 with |