From 3b37cf28565752ba941c21b62df9ba2de5294e66 Mon Sep 17 00:00:00 2001 From: Jon French Date: Tue, 28 Aug 2018 18:42:42 +0100 Subject: fix some compiler not-matched warnings about Typ_bidir and Typ_internal_unknown --- src/extra_pervasives.ml | 52 ++++++++++++++++++++++++++++++++++++++++++++++ src/monomorphise.ml | 25 +++++++++++++++++++--- src/ocaml_backend.ml | 8 +++++-- src/pretty_print_common.ml | 11 +++++++--- src/pretty_print_coq.ml | 15 ++++++++++--- src/pretty_print_lem.ml | 13 +++++++++--- src/pretty_print_sail.ml | 3 ++- src/spec_analysis.ml | 7 +++++-- src/specialize.ml | 10 +++++++++ src/type_check.ml | 8 ++++++- 10 files changed, 134 insertions(+), 18 deletions(-) create mode 100644 src/extra_pervasives.ml (limited to 'src') diff --git a/src/extra_pervasives.ml b/src/extra_pervasives.ml new file mode 100644 index 00000000..a7808a95 --- /dev/null +++ b/src/extra_pervasives.ml @@ -0,0 +1,52 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +let unreachable l pos msg = + raise (Reporting_basic.err_unreachable l pos msg) diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 55031ff9..2723d143 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -59,6 +59,7 @@ open Ast open Ast_util module Big_int = Nat_big_num open Type_check +open Extra_pervasives let size_set_limit = 64 @@ -135,11 +136,13 @@ let subst_src_typ substs t = | Typ_var _ -> ty | Typ_fn (t1,t2,e) -> re (Typ_fn (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_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 (kids,nc,t) -> let substs = List.fold_left (fun sub v -> KBindings.remove v sub) substs kids in re (Typ_exist (kids,nc,s_styp substs t)) + | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown" and s_starg substs (Typ_arg_aux (ta,l) as targ) = match ta with | Typ_arg_nexp ne -> Typ_arg_aux (Typ_arg_nexp (subst_nexp substs ne),l) @@ -313,6 +316,8 @@ let rec inst_src_type insts (Typ_aux (ty,l) as typ) = -> insts,typ | Typ_fn _ -> raise (Reporting_basic.err_general l "Function type in constructor") + | Typ_bidir _ -> + raise (Reporting_basic.err_general l "Mapping type in constructor") | Typ_tup ts -> let insts,ts = List.fold_right @@ -325,13 +330,15 @@ let rec inst_src_type insts (Typ_aux (ty,l) as typ) = (fun arg (insts,args) -> let insts,arg = inst_src_typ_arg insts arg in insts,arg::args) args (insts,[]) in insts, Typ_aux (Typ_app (id,ts),l) - | Typ_exist (kids, nc, t) -> + | Typ_exist (kids, nc, t) -> begin let kid_insts, insts' = peel (kids,insts) in let kids', t' = apply_kid_insts kid_insts t in (* TODO: subst in nc *) match kids' with | [] -> insts', t' | _ -> insts', Typ_aux (Typ_exist (kids', nc, t'), l) + end + | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown" and inst_src_typ_arg insts (Typ_arg_aux (ta,l) as tyarg) = match ta with | Typ_arg_nexp _ @@ -341,15 +348,17 @@ and inst_src_typ_arg insts (Typ_arg_aux (ta,l) as tyarg) = let insts', typ' = inst_src_type insts typ in insts', Typ_arg_aux (Typ_arg_typ typ',l) -let rec contains_exist (Typ_aux (ty,_)) = +let rec contains_exist (Typ_aux (ty,l)) = match ty with | Typ_id _ | Typ_var _ -> false | Typ_fn (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 + | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown" and contains_exist_arg (Typ_arg_aux (arg,_)) = match arg with | Typ_arg_nexp _ @@ -385,6 +394,8 @@ let split_src_type id ty (TypQ_aux (q,ql)) = -> (KidSet.empty,[[],typ]) | Typ_fn _ -> raise (Reporting_basic.err_general l ("Function type in constructor " ^ i)) + | Typ_bidir _ -> + raise (Reporting_basic.err_general l ("Mapping type in constructor " ^ i)) | Typ_tup ts -> let (vars,tys) = List.split (List.map size_nvars_ty ts) in let insttys = List.map (fun x -> let (insts,tys) = List.split x in @@ -421,6 +432,7 @@ let split_src_type id ty (TypQ_aux (q,ql)) = let tys = List.concat (List.map (fun instty -> List.map (ty_and_inst instty) insts) tys) in let free = List.fold_left (fun vars k -> KidSet.remove k vars) vars kids in (free,tys) + | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown" in (* Only single-variable prenex-form for now *) let size_nvars_ty (Typ_aux (ty,l) as typ) = @@ -2164,7 +2176,8 @@ let rec sizes_of_typ (Typ_aux (t,l)) = | Typ_var _ -> KidSet.empty | Typ_fn _ -> raise (Reporting_basic.err_general l - "Function type on expressinon") + "Function type on expression") + | Typ_bidir _ -> raise (Reporting_basic.err_general l "Mapping type on expression") | Typ_tup typs -> kidset_bigunion (List.map sizes_of_typ typs) | Typ_exist (kids,_,typ) -> List.fold_left (fun s k -> KidSet.remove k s) (sizes_of_typ typ) kids @@ -2174,6 +2187,7 @@ let rec sizes_of_typ (Typ_aux (t,l)) = KidSet.of_list (size_nvars_nexp size) | Typ_app (_,tas) -> kidset_bigunion (List.map sizes_of_typarg tas) + | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown" and sizes_of_typarg (Typ_arg_aux (ta,_)) = match ta with Typ_arg_nexp _ @@ -4148,6 +4162,10 @@ let replace_nexp_in_typ env typ orig new_nexp = let f1, arg = aux arg in let f2, res = aux res in f1 || f2, Typ_aux (Typ_fn (arg, res, eff),l) + | Typ_bidir (t1, t2) -> + let f1, t1 = aux t1 in + let f2, t2 = aux t2 in + f1 || f2, Typ_aux (Typ_bidir (t1, t2), 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) @@ -4157,6 +4175,7 @@ let replace_nexp_in_typ env typ orig new_nexp = | Typ_app (id, targs) -> let fs, targs = List.split (List.map aux_targ targs) in List.exists (fun x -> x) fs, Typ_aux (Typ_app (id, targs),l) + | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown" and aux_targ (Typ_arg_aux (ta,l) as typ_arg) = match ta with | Typ_arg_nexp nexp -> diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 9757ec32..6e5eb774 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -98,7 +98,7 @@ let ocaml_string_parens inside = string "\"(\" ^ " ^^ inside ^^ string " ^ \")\" let ocaml_string_comma = string " ^ \", \" ^ " -let rec ocaml_string_typ (Typ_aux (typ_aux, _)) arg = +let rec ocaml_string_typ (Typ_aux (typ_aux, l)) arg = match typ_aux with | Typ_id id when string_of_id id = "exception" -> string "Printexc.to_string" ^^ space ^^ arg | Typ_id id -> ocaml_string_of id ^^ space ^^ arg @@ -118,8 +118,10 @@ let rec ocaml_string_typ (Typ_aux (typ_aux, _)) 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_var kid -> string "\"VAR\"" | Typ_exist _ -> assert false + | Typ_internal_unknown -> raise (Reporting_basic.err_unreachable l __POS__ "escaped Typ_internal_unknown") let ocaml_typ_id ctx = function | id when Id.compare id (mk_id "string") = 0 -> string "string" @@ -134,15 +136,17 @@ let ocaml_typ_id ctx = function | id when Id.compare id (mk_id "register") = 0 -> string "ref" | id -> zencode ctx id -let rec ocaml_typ ctx (Typ_aux (typ_aux, _)) = +let rec ocaml_typ ctx (Typ_aux (typ_aux, l)) = match typ_aux with | Typ_id id -> ocaml_typ_id ctx id | Typ_app (id, []) -> ocaml_typ_id ctx id | 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 (typ1, typ2, _) -> separate space [ocaml_typ ctx typ1; string "->"; ocaml_typ ctx typ2] + | Typ_bidir (t1, t2) -> raise (Reporting_basic.err_general l "Ocaml doesn't support bidir types") | Typ_var kid -> zencode_kid kid | Typ_exist _ -> assert false + | Typ_internal_unknown -> raise (Reporting_basic.err_unreachable l __POS__ "escaped Typ_internal_unknown") and ocaml_typ_arg ctx (Typ_arg_aux (typ_arg_aux, _) as typ_arg) = match typ_arg_aux with | Typ_arg_typ typ -> ocaml_typ ctx typ diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml index b449c72a..2c6c1381 100644 --- a/src/pretty_print_common.ml +++ b/src/pretty_print_common.ml @@ -54,6 +54,7 @@ open PPrint let pipe = string "|" let arrow = string "->" +let bidir = string "<->" let dotdot = string ".." let coloncolon = string "::" let coloneq = string ":=" @@ -128,7 +129,9 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint = let rec typ ty = fn_typ ty and fn_typ ((Typ_aux (t, _)) as ty) = match t with | Typ_fn(arg,ret,efct) -> - separate space [tup_typ arg; arrow; fn_typ ret; string "effect"; doc_effects efct] + separate space [tup_typ arg; arrow; fn_typ ret; string "effect"; doc_effects efct] + | Typ_bidir (t1, t2) -> + separate space [tup_typ t1; bidir; tup_typ t2] | _ -> tup_typ ty and tup_typ ((Typ_aux (t, _)) as ty) = match t with | Typ_exist (kids, nc, ty) -> @@ -149,10 +152,12 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint = and atomic_typ ((Typ_aux (t, _)) as ty) = match t with | Typ_id id -> doc_id id | Typ_var v -> doc_var v - | Typ_app _ | Typ_tup _ | Typ_fn _ | Typ_exist _ -> + | Typ_app _ | Typ_tup _ | Typ_fn _ | Typ_bidir _ | Typ_exist _ -> (* exhaustiveness matters here to avoid infinite loops * if we add a new Typ constructor *) - group (parens (typ ty)) + group (parens (typ ty)) + | Typ_internal_unknown -> string "UNKNOWN" + and doc_typ_arg (Typ_arg_aux(t,_)) = match t with (* Be careful here because typ_arg is implemented as nexp in the * parser - in practice falling through app_typ after all the proper nexp diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index b47ac21c..adfb378a 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -54,6 +54,7 @@ open Ast_util open Rewriter open PPrint open Pretty_print_common +open Extra_pervasives module StringSet = Set.Make(String) @@ -255,7 +256,7 @@ let rec orig_nexp (Nexp_aux (nexp, l)) = (* Returns the set of type variables that will appear in the Lem output, which may be smaller than those in the Sail type. May need to be updated with doc_typ_lem *) -let rec lem_nexps_of_typ (Typ_aux (t,_)) = +let rec lem_nexps_of_typ (Typ_aux (t,l)) = let trec = lem_nexps_of_typ in match t with | Typ_id _ -> NexpSet.empty @@ -281,6 +282,8 @@ let rec lem_nexps_of_typ (Typ_aux (t,_)) = List.fold_left (fun s ta -> NexpSet.union s (lem_nexps_of_typ_arg ta)) NexpSet.empty tas | Typ_exist (kids,_,t) -> trec t + | Typ_bidir _ -> unreachable l __POS__ "Coq doesn't support bidir types" + | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown" and lem_nexps_of_typ_arg (Typ_arg_aux (ta,_)) = match ta with | Typ_arg_nexp nexp -> NexpSet.singleton (nexp_simp (orig_nexp nexp)) @@ -312,6 +315,8 @@ let drop_duplicate_atoms kids ty = (* Don't recurse into type arguments, removing stuff there would be weird (and difficult) *) | Typ_app _ -> Some full_typ + | Typ_bidir _ -> unreachable l __POS__ "Coq doesn't support bidir types" + | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown" in aux_typ ty (* Follows Coq precedence levels *) @@ -478,7 +483,9 @@ let doc_typ, doc_atomic_typ = match nc with (* | NC_aux (NC_true,_) -> List.fold_left add_tyvar (string "Z") (List.tl kids)*) | _ -> List.fold_left add_tyvar (doc_arithfact ctx nc) kids - end + end + | Typ_bidir _ -> unreachable l __POS__ "Coq doesn't support bidir types" + | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown" and doc_typ_arg (Typ_arg_aux(t,_)) = match t with | Typ_arg_typ t -> app_typ true t | Typ_arg_nexp n -> doc_nexp ctx n @@ -603,7 +610,7 @@ let doc_typquant ctx (TypQ_aux(tq,_)) typ = match tq with machine words. Often these will be unnecessary, but this simple approach will do for now. *) -let rec typeclass_nexps (Typ_aux(t,_)) = +let rec typeclass_nexps (Typ_aux(t,l)) = match t with | Typ_id _ | Typ_var _ @@ -620,6 +627,8 @@ let rec typeclass_nexps (Typ_aux(t,_)) = NexpSet.singleton (orig_nexp size_nexp) | Typ_app _ -> NexpSet.empty | Typ_exist (kids,_,t) -> NexpSet.empty (* todo *) + | Typ_bidir _ -> unreachable l __POS__ "Coq doesn't support bidir types" + | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown" let doc_typschm ctx quants (TypSchm_aux(TypSchm_ts(tq,t),_)) = let pt = doc_typ ctx t in diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index c20fe5f4..70db46b8 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -54,6 +54,7 @@ open Ast_util open Rewriter open PPrint open Pretty_print_common +open Extra_pervasives (**************************************************************************** * PPrint-based sail-to-lem pprinter @@ -213,7 +214,7 @@ let rec orig_nexp (Nexp_aux (nexp, l)) = (* Returns the set of type variables that will appear in the Lem output, which may be smaller than those in the Sail type. May need to be updated with doc_typ_lem *) -let rec lem_nexps_of_typ (Typ_aux (t,_)) = +let rec lem_nexps_of_typ (Typ_aux (t,l)) = let trec = lem_nexps_of_typ in match t with | Typ_id _ -> NexpSet.empty @@ -239,6 +240,8 @@ let rec lem_nexps_of_typ (Typ_aux (t,_)) = List.fold_left (fun s ta -> NexpSet.union s (lem_nexps_of_typ_arg ta)) NexpSet.empty tas | Typ_exist (kids,_,t) -> trec t + | Typ_bidir _ -> raise (Reporting_basic.err_unreachable l __POS__ "Lem doesn't support bidir types") + | Typ_internal_unknown -> raise (Reporting_basic.err_unreachable l __POS__ "escaped Typ_internal_unknown") and lem_nexps_of_typ_arg (Typ_arg_aux (ta,_)) = match ta with | Typ_arg_nexp nexp -> NexpSet.singleton (nexp_simp (orig_nexp nexp)) @@ -322,7 +325,9 @@ let doc_typ_lem, doc_atomic_typ_lem = ("Existential type variable(s) " ^ String.concat ", " (List.map string_of_kid bad) ^ " escape into Lem")) - end + end + | Typ_bidir _ -> unreachable l __POS__ "Lem doesn't support bidir types" + | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown" and doc_typ_arg_lem (Typ_arg_aux(t,_)) = match t with | Typ_arg_typ t -> app_typ true t | Typ_arg_nexp n -> doc_nexp_lem (nexp_simp n) @@ -433,7 +438,7 @@ let doc_typquant_lem (TypQ_aux(tq,_)) vars_included typ = match tq with machine words. Often these will be unnecessary, but this simple approach will do for now. *) -let rec typeclass_nexps (Typ_aux(t,_)) = +let rec typeclass_nexps (Typ_aux(t,l)) = if !opt_mwords then match t with | Typ_id _ @@ -457,6 +462,8 @@ let rec typeclass_nexps (Typ_aux(t,_)) = in List.fold_left add_arg_nexps NexpSet.empty args | Typ_exist (kids,_,t) -> NexpSet.empty (* todo *) + | Typ_bidir _ -> unreachable l __POS__ "Lem doesn't support bidir types" + | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown" else NexpSet.empty let doc_typclasses_lem t = diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 06f1d768..b84bc3be 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -135,7 +135,7 @@ let doc_nc = in nc0 -let rec doc_typ (Typ_aux (typ_aux, _)) = +let rec doc_typ (Typ_aux (typ_aux, l)) = match typ_aux with | Typ_id id -> doc_id id | Typ_app (id, []) -> doc_id id @@ -161,6 +161,7 @@ let rec doc_typ (Typ_aux (typ_aux, _)) = separate space [doc_typ typ1; string "->"; doc_typ typ2; string "effect"; ocaml_eff] | Typ_bidir (typ1, typ2) -> separate space [doc_typ typ1; string "<->"; doc_typ typ2] + | Typ_internal_unknown -> raise (Reporting_basic.err_unreachable l __POS__ "escaped Typ_internal_unknown") and doc_typ_arg (Typ_arg_aux (ta_aux, _)) = match ta_aux with | Typ_arg_typ typ -> doc_typ typ diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index f6da074c..44440ecf 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -51,6 +51,7 @@ open Ast open Util open Ast_util +open Extra_pervasives module Nameset = Set.Make(String) @@ -84,7 +85,7 @@ let conditional_add_exp = conditional_add false let nameset_bigunion = List.fold_left Nameset.union mt -let rec free_type_names_t consider_var (Typ_aux (t, _)) = match t with +let rec free_type_names_t consider_var (Typ_aux (t, l)) = match t with | Typ_var name -> if consider_var then Nameset.add (string_of_kid name) mt else mt | Typ_id name -> Nameset.add (string_of_id name) mt | Typ_fn (t1,t2,_) -> Nameset.union (free_type_names_t consider_var t1) @@ -94,6 +95,7 @@ let rec free_type_names_t consider_var (Typ_aux (t, _)) = match t with | 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 (kids,_,t') -> List.fold_left (fun s kid -> Nameset.remove (string_of_kid kid) s) (free_type_names_t consider_var t') kids + | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown" and free_type_names_ts consider_var ts = nameset_bigunion (List.map (free_type_names_t consider_var) ts) and free_type_names_maybe_t consider_var = function | Some t -> free_type_names_t consider_var t @@ -111,7 +113,7 @@ let rec free_type_names_tannot consider_var tannot = | Some (_, t, _) -> free_type_names_t consider_var t -let rec fv_of_typ consider_var bound used (Typ_aux (t,_)) : Nameset.t = +let rec fv_of_typ consider_var bound used (Typ_aux (t,l)) : Nameset.t = match t with | Typ_var (Kid_aux (Var v,l)) -> if consider_var @@ -124,6 +126,7 @@ let rec fv_of_typ consider_var bound used (Typ_aux (t,_)) : Nameset.t = | 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) | Typ_exist (kids,_,t') -> fv_of_typ consider_var (List.fold_left (fun b (Kid_aux (Var v,_)) -> Nameset.add v b) bound kids) used t' + | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown" and fv_of_targ consider_var bound used (Ast.Typ_arg_aux(targ,_)) : Nameset.t = match targ with | Typ_arg_typ t -> fv_of_typ consider_var bound used t diff --git a/src/specialize.ml b/src/specialize.ml index 9723689f..81c8b0b0 100644 --- a/src/specialize.ml +++ b/src/specialize.ml @@ -51,6 +51,7 @@ open Ast open Ast_util open Rewriter +open Extra_pervasives let is_typ_ord_uvar = function | Type_check.U_typ _ -> true @@ -65,6 +66,8 @@ let rec nexp_simp_typ (Typ_aux (typ_aux, l)) = | Typ_app (f, args) -> Typ_app (f, List.map nexp_simp_typ_arg args) | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc, nexp_simp_typ typ) | Typ_fn (typ1, typ2, effect) -> Typ_fn (nexp_simp_typ typ1, nexp_simp_typ typ2, effect) + | Typ_bidir (t1, t2) -> Typ_bidir (nexp_simp_typ t1, nexp_simp_typ t2) + | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown" in Typ_aux (typ_aux, l) and nexp_simp_typ_arg (Typ_arg_aux (typ_arg_aux, l)) = @@ -136,8 +139,11 @@ let string_of_instantiation instantiation = | Typ_app (id, args) -> string_of_id id ^ "(" ^ Util.string_of_list ", " string_of_typ_arg args ^ ")" | Typ_fn (typ_arg, typ_ret, eff) -> string_of_typ typ_arg ^ " -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff + | Typ_bidir (t1, t2) -> + string_of_typ t1 ^ " <-> " ^ string_of_typ t2 | 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" and string_of_typ_arg = function | Typ_arg_aux (typ_arg, l) -> string_of_typ_arg_aux typ_arg and string_of_typ_arg_aux = function @@ -252,6 +258,8 @@ let rec typ_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) = | Typ_app (f, args) -> List.fold_left KidSet.union KidSet.empty (List.map (typ_arg_frees ~exs:exs) args) | Typ_exist (kids, nc, typ) -> typ_frees ~exs:(KidSet.of_list kids) typ | Typ_fn (typ1, typ2, _) -> KidSet.union (typ_frees ~exs:exs typ1) (typ_frees ~exs:exs typ2) + | Typ_bidir (t1, t2) -> KidSet.union (typ_frees ~exs:exs t1) (typ_frees ~exs:exs t2) + | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown" and typ_arg_frees ?exs:(exs=KidSet.empty) (Typ_arg_aux (typ_arg_aux, l)) = match typ_arg_aux with | Typ_arg_nexp n -> KidSet.empty @@ -266,6 +274,8 @@ let rec typ_int_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) = | Typ_app (f, args) -> List.fold_left KidSet.union KidSet.empty (List.map (typ_arg_int_frees ~exs:exs) args) | Typ_exist (kids, nc, typ) -> typ_int_frees ~exs:(KidSet.of_list kids) typ | Typ_fn (typ1, typ2, _) -> KidSet.union (typ_int_frees ~exs:exs typ1) (typ_int_frees ~exs:exs typ2) + | Typ_bidir (t1, t2) -> KidSet.union (typ_int_frees ~exs:exs t1) (typ_int_frees ~exs:exs t2) + | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown" and typ_arg_int_frees ?exs:(exs=KidSet.empty) (Typ_arg_aux (typ_arg_aux, l)) = match typ_arg_aux with | Typ_arg_nexp n -> KidSet.diff (tyvars_of_nexp n) exs diff --git a/src/type_check.ml b/src/type_check.ml index a731130a..dbbc704c 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -52,6 +52,8 @@ open Ast open Util open Ast_util open Lazy +open Extra_pervasives + module Big_int = Nat_big_num (* opt_tc_debug controls the verbosity of the type checker. 0 is @@ -707,6 +709,7 @@ end = struct | Typ_tup _ | Typ_app _ -> Typ_exist (existentials, List.fold_left nc_and (List.hd constrs) (List.tl constrs), typ) | Typ_exist (kids, nc, typ) -> Typ_exist (kids @ existentials, List.fold_left nc_and nc constrs, typ) | Typ_fn _ | Typ_bidir _ | Typ_id _ | Typ_var _ -> assert false (* These must be simple *) + | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown" in Typ_aux (typ_aux, l) @@ -744,6 +747,7 @@ end = struct wf_constraint ~exs:(KidSet.of_list kids) env nc; wf_typ ~exs:(KidSet.of_list kids) { env with constraints = nc :: env.constraints } typ | Typ_exist (_, _, _) -> typ_error l ("Nested existentials are not allowed") + | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown" and wf_typ_arg ?exs:(exs=KidSet.empty) env (Typ_arg_aux (typ_arg_aux, _)) = match typ_arg_aux with | Typ_arg_nexp nexp -> wf_nexp ~exs:exs env nexp @@ -1277,7 +1281,7 @@ let destruct_vector env typ = in destruct_vector' (Env.expand_synonyms env typ) -let rec is_typ_monomorphic (Typ_aux (typ, _)) = +let rec is_typ_monomorphic (Typ_aux (typ, l)) = match typ with | Typ_id _ -> true | Typ_tup typs -> List.for_all is_typ_monomorphic typs @@ -1285,6 +1289,7 @@ let rec is_typ_monomorphic (Typ_aux (typ, _)) = | Typ_fn (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 -> unreachable l __POS__ "escaped Typ_internal_unknown" and is_typ_arg_monomorphic (Typ_arg_aux (arg, _)) = match arg with | Typ_arg_nexp _ -> true @@ -1827,6 +1832,7 @@ let rec kid_order kids (Typ_aux (aux, l) as typ) = | Typ_app (_, args) -> List.fold_left (fun (ord, kids) arg -> let (ord', kids) = kid_order_arg kids arg in (ord @ ord', kids)) ([], kids) args | Typ_fn _ | Typ_bidir _ | Typ_exist _ -> typ_error l ("Existential or function type cannot appear within existential type: " ^ string_of_typ typ) + | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown" and kid_order_arg kids (Typ_arg_aux (aux, l) as arg) = match aux with | Typ_arg_typ typ -> kid_order kids typ -- cgit v1.2.3