summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/extra_pervasives.ml52
-rw-r--r--src/finite_map.ml216
-rw-r--r--src/isail.ml2
-rw-r--r--src/monomorphise.ml41
-rw-r--r--src/pp.ml80
-rw-r--r--src/pretty_print_coq.ml8
-rw-r--r--src/pretty_print_lem.ml2
-rw-r--r--src/reporting.ml41
-rw-r--r--src/reporting.mli8
-rw-r--r--src/rewriter.ml23
-rw-r--r--src/rewrites.ml10
-rw-r--r--src/sail.ml2
-rw-r--r--src/spec_analysis.ml5
-rw-r--r--src/specialize.ml7
-rw-r--r--src/type_check.ml7
15 files changed, 60 insertions, 444 deletions
diff --git a/src/extra_pervasives.ml b/src/extra_pervasives.ml
deleted file mode 100644
index 8001c647..00000000
--- a/src/extra_pervasives.ml
+++ /dev/null
@@ -1,52 +0,0 @@
-(**************************************************************************)
-(* 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.err_unreachable l pos msg)
diff --git a/src/finite_map.ml b/src/finite_map.ml
deleted file mode 100644
index 444e3790..00000000
--- a/src/finite_map.ml
+++ /dev/null
@@ -1,216 +0,0 @@
-(**************************************************************************)
-(* 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. *)
-(**************************************************************************)
-
-
-(**************************************************************************)
-(* Lem *)
-(* *)
-(* Dominic Mulligan, University of Cambridge *)
-(* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *)
-(* Gabriel Kerneis, University of Cambridge *)
-(* Kathy Gray, University of Cambridge *)
-(* Peter Boehm, University of Cambridge (while working on Lem) *)
-(* Peter Sewell, University of Cambridge *)
-(* Scott Owens, University of Kent *)
-(* Thomas Tuerk, University of Cambridge *)
-(* *)
-(* The Lem sources are copyright 2010-2013 *)
-(* by the UK authors above and Institut National de Recherche en *)
-(* Informatique et en Automatique (INRIA). *)
-(* *)
-(* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *)
-(* are distributed under the license below. The former are distributed *)
-(* under the LGPLv2, as in the LICENSE file. *)
-(* *)
-(* *)
-(* 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. *)
-(* 3. The names of the authors may not be used to endorse or promote *)
-(* products derived from this software without specific prior written *)
-(* permission. *)
-(* *)
-(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``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 AUTHORS 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. *)
-(**************************************************************************)
-
-
-(** finite map library *)
-
-module type Fmap = sig
- type k
- module S : Set.S with type elt = k
- type 'a t
- val empty : 'a t
- val is_empty : 'a t -> bool
- val from_list : (k * 'a) list -> 'a t
- val to_list : 'a t -> (k * 'a) list
- val from_list2 : k list -> 'a list -> 'a t
- val insert : 'a t -> (k * 'a) -> 'a t
- (* Keys from the right argument replace those from the left *)
- val union : 'a t -> 'a t -> 'a t
- (* Function merges the stored value when a key is in the right and the left map *)
- val union_merge : ('a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
- val intersect : 'a t -> 'a t -> 'a t
- (* Function merges the stored values for shared keys *)
- val intersect_merge : ('a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
- val big_union : 'a t list -> 'a t
- val big_union_merge : ('a -> 'a -> 'a) -> 'a t list -> 'a t
- val difference : 'a t -> 'a t -> 'a t
- val merge : (k -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
- val apply : 'a t -> k -> 'a option
- val in_dom : k -> 'a t -> bool
- val map : (k -> 'a -> 'b) -> 'a t -> 'b t
- val domains_overlap : 'a t -> 'b t -> k option
- val domains_disjoint : 'a t list -> bool
- val iter : (k -> 'a -> unit) -> 'a t -> unit
- val fold : ('b -> k -> 'a -> 'b) -> 'b -> 'a t -> 'b
- val remove : 'a t -> k -> 'a t
- val pp_map : (Format.formatter -> k -> unit) ->
- (Format.formatter -> 'a -> unit) ->
- Format.formatter ->
- 'a t ->
- unit
- val domain : 'a t -> S.t
-end
-
-module Fmap_map(Key : Set.OrderedType) : Fmap
- with type k = Key.t and module S = Set.Make(Key) = struct
-
- type k = Key.t
- module S = Set.Make(Key)
-
- module M = Map.Make(Key)
- module D = Util.Duplicate(S)
-
- type 'a t = 'a M.t
- let empty = M.empty
- let is_empty m = M.is_empty m
- let from_list l = List.fold_left (fun m (k,v) -> M.add k v m) M.empty l
- let from_list2 l1 l2 = List.fold_left2 (fun m k v -> M.add k v m) M.empty l1 l2
- let insert m (k,v) = M.add k v m
- let union m1 m2 =
- M.merge (fun k v1 v2 -> match v2 with | None -> v1 | Some _ -> v2) m1 m2
- let union_merge f m1 m2 =
- M.merge (fun k v1 v2 ->
- match v1,v2 with
- | None,None -> None
- | None,Some v | Some v,None -> Some v
- | Some v1, Some v2 -> Some (f v1 v2)) m1 m2
- let merge f m1 m2 = M.merge f m1 m2
- let apply m k =
- try
- Some(M.find k m)
- with
- | Not_found -> None
- let in_dom k m = M.mem k m
- let map f m = M.mapi f m
- let rec domains_overlap m1 m2 =
- M.fold
- (fun k _ res ->
- if M.mem k m1 then
- Some(k)
- else
- res)
- m2
- None
- let iter f m = M.iter f m
- let fold f m base = M.fold (fun k v res -> f res k v) base m
- let difference m1 m2 =
- M.fold (fun k v res ->
- if (M.mem k m2)
- then res
- else M.add k v res) m1 M.empty
- let intersect m1 m2 =
- M.fold (fun k v res ->
- if (M.mem k m2)
- then M.add k v res
- else res) m1 M.empty
- let intersect_merge f m1 m2 =
- M.fold (fun k v res ->
- match (apply m2 k) with
- | None -> res
- | Some v2 -> M.add k (f v v2) res) m1 M.empty
- let to_list m = M.fold (fun k v res -> (k,v)::res) m []
- let remove m k = M.remove k m
- let pp_map pp_key pp_val ppf m =
- let l = M.fold (fun k v l -> (k,v)::l) m [] in
- Format.fprintf ppf "@[%a@]"
- (Pp.lst "@\n"
- (fun ppf (k,v) ->
- Format.fprintf ppf "@[<2>%a@ |->@ %a@]"
- pp_key k
- pp_val v))
- l
- let big_union l = List.fold_left union empty l
- let big_union_merge f l = List.fold_left (union_merge f) empty l
- let domains_disjoint maps =
- match D.duplicates (List.concat (List.map (fun m -> List.map fst (M.bindings m)) maps)) with
- | D.No_dups _ -> true
- | D.Has_dups _ -> false
-
- let domain m =
- M.fold (fun k _ s -> S.add k s) m S.empty
-end
-
diff --git a/src/isail.ml b/src/isail.ml
index a3dfe680..d8cc448a 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -83,7 +83,7 @@ let rec user_input callback =
mode_clear ();
begin
try callback v with
- | Reporting.Fatal_error e -> Reporting.report_error e
+ | Reporting.Fatal_error e -> Reporting.print_error e
end;
user_input callback
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index fc2a9de6..eb50bac3 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -59,7 +59,6 @@ open Ast
open Ast_util
module Big_int = Nat_big_num
open Type_check
-open Extra_pervasives
let size_set_limit = 64
@@ -142,7 +141,7 @@ let subst_nc, subst_src_typ, subst_src_typ_arg =
| Typ_exist (kopts,nc,t) ->
let substs = List.fold_left (fun sub kopt -> KBindings.remove (kopt_kid kopt) sub) substs kopts in
re (Typ_exist (kopts,nc,s_styp substs t))
- | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
+ | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown"
and s_starg substs (A_aux (ta,l) as targ) =
match ta with
| A_nexp ne -> A_aux (A_nexp (subst_nexp substs ne),l)
@@ -181,7 +180,7 @@ let rec is_value (E_aux (e,(l,annot))) =
let is_constructor id =
match destruct_tannot annot with
| None ->
- (Reporting.print_err false true l "Monomorphisation"
+ (Reporting.print_err l "Monomorphisation"
("Missing type information for identifier " ^ string_of_id id);
false) (* Be conservative if we have no info *)
| Some (env,_,_) ->
@@ -341,7 +340,7 @@ let rec inst_src_type insts (Typ_aux (ty,l) as typ) =
| [] -> insts', t'
| _ -> insts', Typ_aux (Typ_exist (List.map (mk_kopt K_int) kids', nc, t'), l)
end
- | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
+ | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown"
and inst_src_typ_arg insts (A_aux (ta,l) as tyarg) =
match ta with
| A_nexp _
@@ -361,7 +360,7 @@ let rec contains_exist (Typ_aux (ty,l)) =
| 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"
+ | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown"
and contains_exist_arg (A_aux (arg,_)) =
match arg with
| A_nexp _
@@ -437,7 +436,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"
+ | Typ_internal_unknown -> Reporting.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) =
@@ -546,7 +545,7 @@ let refine_constructor refinements l env id args =
match List.find matches_refinement irefinements with
| (_,new_id,_) -> Some (E_app (new_id,args))
| exception Not_found ->
- (Reporting.print_err false true l "Monomorphisation"
+ (Reporting.print_err l "Monomorphisation"
("Unable to refine constructor " ^ string_of_id id);
None)
end
@@ -1536,7 +1535,7 @@ let split_defs all_errors splits defs =
and can_match_with_env ref_vars env (E_aux (e,(l,annot)) as exp0) cases (substs,ksubsts) assigns =
let rec findpat_generic check_pat description assigns = function
- | [] -> (Reporting.print_err false true l "Monomorphisation"
+ | [] -> (Reporting.print_err l "Monomorphisation"
("Failed to find a case for " ^ description); None)
| [Pat_aux (Pat_exp (P_aux (P_wild,_),exp),_)] -> Some (exp,[],[])
| (Pat_aux (Pat_exp (P_aux (P_typ (_,p),_),exp),ann))::tl ->
@@ -1583,7 +1582,7 @@ let split_defs all_errors splits defs =
| P_aux (P_app (id',[]),_) ->
if Id.compare id id' = 0 then DoesMatch ([],[]) else DoesNotMatch
| P_aux (_,(l',_)) ->
- (Reporting.print_err false true l' "Monomorphisation"
+ (Reporting.print_err l' "Monomorphisation"
"Unexpected kind of pattern for enumeration"; GiveUp)
in findpat_generic checkpat (string_of_id id) assigns cases
| _ -> None)
@@ -1606,11 +1605,11 @@ let split_defs all_errors splits defs =
DoesMatch ([id, E_aux (E_cast (typ,E_aux (e,(l,empty_tannot))),(l,empty_tannot))],
[kid,nexp])
| _ ->
- (Reporting.print_err false true lit_l "Monomorphisation"
+ (Reporting.print_err lit_l "Monomorphisation"
"Unexpected kind of literal for var match"; GiveUp)
end
| P_aux (_,(l',_)) ->
- (Reporting.print_err false true l' "Monomorphisation"
+ (Reporting.print_err l' "Monomorphisation"
"Unexpected kind of pattern for literal"; GiveUp)
in findpat_generic checkpat "literal" assigns cases
| E_vector es when List.for_all (function (E_aux (E_lit _,_)) -> true | _ -> false) es ->
@@ -1630,11 +1629,11 @@ let split_defs all_errors splits defs =
| _ -> DoesNotMatch) (DoesMatch ([],[])) matches in
(match final with
| GiveUp ->
- (Reporting.print_err false true l "Monomorphisation"
+ (Reporting.print_err l "Monomorphisation"
"Unexpected kind of pattern for vector literal"; GiveUp)
| _ -> final)
| _ ->
- (Reporting.print_err false true l "Monomorphisation"
+ (Reporting.print_err l "Monomorphisation"
"Unexpected kind of pattern for vector literal"; GiveUp)
in findpat_generic checkpat "vector literal" assigns cases
@@ -1652,7 +1651,7 @@ let split_defs all_errors splits defs =
DoesMatch ([id, E_aux (E_cast (typ,e_undef),(l,empty_tannot))],
KBindings.bindings ksubst)
| P_aux (_,(l',_)) ->
- (Reporting.print_err false true l' "Monomorphisation"
+ (Reporting.print_err l' "Monomorphisation"
"Unexpected kind of pattern for literal"; GiveUp)
in findpat_generic checkpat "literal" assigns cases
| _ -> None
@@ -1949,7 +1948,7 @@ let split_defs all_errors splits defs =
let overlap = List.exists (fun (v,_) -> List.mem v pvs) lvs in
let () =
if overlap then
- Reporting.print_err false true l "Monomorphisation"
+ Reporting.print_err l "Monomorphisation"
"Splitting a singleton pattern is not possible"
in p
in
@@ -2123,7 +2122,7 @@ let split_defs all_errors splits defs =
| DEF_internal_mutrec _
-> [d]
| DEF_fundef fd -> [DEF_fundef (map_fundef fd)]
- | DEF_mapdef (MD_aux (_, (l, _))) -> unreachable l __POS__ "mappings should be gone by now"
+ | DEF_mapdef (MD_aux (_, (l, _))) -> Reporting.unreachable l __POS__ "mappings should be gone by now"
| DEF_val lb -> [DEF_val (map_letbind lb)]
| DEF_scattered sd -> List.map (fun x -> DEF_scattered x) (map_scattered_def sd)
in
@@ -2203,7 +2202,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"
+ | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown"
and sizes_of_typarg (A_aux (ta,_)) =
match ta with
A_nexp _
@@ -3597,11 +3596,11 @@ let analyse_defs debug env (Defs defs) =
else ()
in
let splits = argset_to_list splits in
- if Failures.is_empty fails
+ if Failures.is_empty fails
then (true,splits,extras) else
begin
Failures.iter (fun l msgs ->
- Reporting.print_err false false l "Monomorphisation" (String.concat "\n" (StringSet.elements msgs)))
+ Reporting.print_err l "Monomorphisation" (String.concat "\n" (StringSet.elements msgs)))
fails;
(false, splits,extras)
end
@@ -3626,7 +3625,7 @@ let add_extra_splits extras (Defs defs) =
let loc = match Analysis.translate_loc l with
| Some l -> l
| None ->
- (Reporting.print_err false false l "Monomorphisation"
+ (Reporting.print_err l "Monomorphisation"
"Internal error: bad location for added case";
("",0))
in
@@ -4205,7 +4204,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"
+ | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown"
and aux_targ (A_aux (ta,l) as typ_arg) =
match ta with
| A_nexp nexp ->
diff --git a/src/pp.ml b/src/pp.ml
deleted file mode 100644
index b3eaf1fc..00000000
--- a/src/pp.ml
+++ /dev/null
@@ -1,80 +0,0 @@
-(**************************************************************************)
-(* 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. *)
-(**************************************************************************)
-
-(** pretty printing utilities *)
-
-open Format
-
-let pp_str ppf s =
- fprintf ppf "%s" s
-
-let rec lst sep f ppf = function
- | [] -> ()
- | [x] ->
- fprintf ppf "%a"
- f x
- | (h::t) ->
- f ppf h;
- fprintf ppf sep;
- lst sep f ppf t
-
-let opt f ppf = function
- | None ->
- fprintf ppf "None"
- | Some(x) ->
- fprintf ppf "Some(%a)"
- f x
-
-let pp_to_string pp =
- let b = Buffer.create 16 in
- let f = formatter_of_buffer b in
- pp f;
- pp_print_flush f ();
- Buffer.contents b
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index a5478c31..fa858eae 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -51,10 +51,10 @@
open Type_check
open Ast
open Ast_util
+open Reporting
open Rewriter
open PPrint
open Pretty_print_common
-open Extra_pervasives
module StringSet = Set.Make(String)
@@ -2008,8 +2008,8 @@ let merge_kids_atoms pats =
match Type_check.destruct_atom_nexp (env_of_annot ann) typ with
| Some (Nexp_aux (Nexp_var kid,l)) ->
if KidSet.mem kid seen then
- let () =
- Reporting.print_err false true l "merge_kids_atoms"
+ let () =
+ Reporting.print_err l "merge_kids_atoms"
("want to merge tyvar and argument for " ^ string_of_kid kid ^
" but rearranging arguments isn't supported yet") in
gone,map,seen
@@ -2420,7 +2420,7 @@ try
let generic_eq_types = types_used_with_generic_eq defs in
let doc_def = doc_def unimplemented generic_eq_types in
let () = if !opt_undef_axioms || IdSet.is_empty unimplemented then () else
- Reporting.print_err false false Parse_ast.Unknown "Warning"
+ Reporting.print_err Parse_ast.Unknown "Warning"
("The following functions were declared but are undefined:\n" ^
String.concat "\n" (List.map string_of_id (IdSet.elements unimplemented)))
in
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 90ae2dba..9281db31 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -51,10 +51,10 @@
open Type_check
open Ast
open Ast_util
+open Reporting
open Rewriter
open PPrint
open Pretty_print_common
-open Extra_pervasives
(****************************************************************************
* PPrint-based sail-to-lem pprinter
diff --git a/src/reporting.ml b/src/reporting.ml
index 7aa68296..0bc73ed6 100644
--- a/src/reporting.ml
+++ b/src/reporting.ml
@@ -97,26 +97,22 @@
type pos_or_loc = Loc of Parse_ast.l | Pos of Lexing.position
-let print_err_internal fatal verb_loc p_l m1 m2 =
+let print_err_internal p_l m1 m2 =
let open Error_format in
prerr_endline (m1 ^ ":");
begin match p_l with
| Loc l -> format_message (Location (l, Line m2)) err_formatter
| Pos p -> format_message (Location (Parse_ast.Range (p, p), Line m2)) err_formatter
- end;
- if fatal then exit 1 else ()
+ end
let loc_to_string ?code:(code=true) l =
let open Error_format in
- if code then
- let b = Buffer.create 160 in
- format_message (Location (l, Line "")) (buffer_formatter b);
- Buffer.contents b
- else
- "LOC"
+ let b = Buffer.create 160 in
+ format_message (Location (l, Line "")) (buffer_formatter b);
+ Buffer.contents b
-let print_err fatal verb_loc l m1 m2 =
- print_err_internal fatal verb_loc (Loc l) m1 m2
+let print_err l m1 m2 =
+ print_err_internal (Loc l) m1 m2
type error =
| Err_general of Parse_ast.l * string
@@ -130,14 +126,14 @@ type error =
let issues = "\n\nPlease report this as an issue on GitHub at https://github.com/rems-project/sail/issues"
let dest_err = function
- | Err_general (l, m) -> ("Error", false, Loc l, m)
+ | Err_general (l, m) -> ("Error", Loc l, m)
| Err_unreachable (l, (file, line, _, _), m) ->
- ((Printf.sprintf "Internal error: Unreachable code (at \"%s\" line %d)" file line), false, Loc l, m ^ issues)
- | Err_todo (l, m) -> ("Todo" ^ m, false, Loc l, "")
- | Err_syntax (p, m) -> ("Syntax error", false, Pos p, m)
- | Err_syntax_locn (l, m) -> ("Syntax error", false, Loc l, m)
- | Err_lex (p, s) -> ("Lexical error", false, Pos p, s)
- | Err_type (l, m) -> ("Type error", false, Loc l, m)
+ (Printf.sprintf "Internal error: Unreachable code (at \"%s\" line %d)" file line, Loc l, m ^ issues)
+ | Err_todo (l, m) -> ("Todo" ^ m, Loc l, "")
+ | Err_syntax (p, m) -> ("Syntax error", Pos p, m)
+ | Err_syntax_locn (l, m) -> ("Syntax error", Loc l, m)
+ | Err_lex (p, s) -> ("Lexical error", Pos p, s)
+ | Err_type (l, m) -> ("Type error", Loc l, m)
exception Fatal_error of error
@@ -147,10 +143,9 @@ let err_unreachable l ocaml_pos m = Fatal_error (Err_unreachable (l, ocaml_pos,
let err_general l m = Fatal_error (Err_general (l, m))
let err_typ l m = Fatal_error (Err_type (l,m))
-let report_error e =
- let (m1, verb_pos, pos_l, m2) = dest_err e in
- print_err_internal verb_pos false pos_l m1 m2
+let unreachable l pos msg =
+ raise (err_unreachable l pos msg)
let print_error e =
- let (m1, verb_pos, pos_l, m2) = dest_err e in
- print_err_internal verb_pos false pos_l m1 m2
+ let (m1, pos_l, m2) = dest_err e in
+ print_err_internal pos_l m1 m2
diff --git a/src/reporting.mli b/src/reporting.mli
index 4ce0ced8..2d886111 100644
--- a/src/reporting.mli
+++ b/src/reporting.mli
@@ -69,13 +69,13 @@ val loc_to_string : ?code:bool -> Parse_ast.l -> string
std-err. It starts with printing location information stored in [l]
It then prints "head: mes". If [fatal] is set, the program exists with error-code 1 afterwards.
*)
-val print_err : bool -> bool -> Parse_ast.l -> string -> string -> unit
+val print_err : Parse_ast.l -> string -> string -> unit
(** {2 Errors } *)
(** Errors stop execution and print a message; they typically have a location and message.
*)
-type error =
+type error =
(** General errors, used for multi purpose. If you are unsure, use this one. *)
| Err_general of Parse_ast.l * string
@@ -105,8 +105,6 @@ val err_unreachable : Parse_ast.l -> (string * int * int * int) -> string -> exn
(** [err_typ l m] is an abreviatiation for [Fatal_error (Err_type (l, m))] *)
val err_typ : Parse_ast.l -> string -> exn
-(** Report error should only be used by main to print the error in the end. Everywhere else,
- raising a [Fatal_error] exception is recommended. *)
-val report_error : error -> unit
+val unreachable : Parse_ast.l -> (string * int * int * int) -> string -> 'a
val print_error : error -> unit
diff --git a/src/rewriter.ml b/src/rewriter.ml
index a70f6fab..330a98f6 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -382,29 +382,6 @@ let rewriters_base =
let rewrite_defs (Defs defs) = rewrite_defs_base rewriters_base (Defs defs)
-module Envmap = Finite_map.Fmap_map(String)
-
-(* TODO: This seems to only consider a single assignment (or possibly two, in
- separate branches of an if-expression). Hence, it seems the result is always
- at most one variable. Is this intended?
- It is only used below when pulling out local variables inside if-expressions
- into the outer scope, which seems dubious. I comment it out for now. *)
-(*let rec introduced_variables (E_aux (exp,(l,annot))) =
- match exp with
- | E_cast (typ, exp) -> introduced_variables exp
- | E_if (c,t,e) -> Envmap.intersect (introduced_variables t) (introduced_variables e)
- | E_assign (lexp,exp) -> introduced_vars_le lexp exp
- | _ -> Envmap.empty
-
-and introduced_vars_le (LEXP_aux(lexp,annot)) exp =
- match lexp with
- | LEXP_id (Id_aux (Id id,_)) | LEXP_cast(_,(Id_aux (Id id,_))) ->
- (match annot with
- | Base((_,t),Emp_intro,_,_,_,_) ->
- Envmap.insert Envmap.empty (id,(t,exp))
- | _ -> Envmap.empty)
- | _ -> Envmap.empty*)
-
type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
{ p_lit : lit -> 'pat_aux
; p_wild : 'pat_aux
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 1e3d319a..16efcd55 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -54,7 +54,6 @@ open Ast_util
open Type_check
open Spec_analysis
open Rewriter
-open Extra_pervasives
let (>>) f g = fun x -> g(f(x))
@@ -4637,7 +4636,7 @@ let check_cases process is_wild loc_of cases =
let rec aux rps acc = function
| [] -> acc, rps
| [p] when is_wild p && match rps with [] -> true | _ -> false ->
- let () = Reporting.print_err false false
+ let () = Reporting.print_err
(loc_of p) "Match checking" "Redundant wildcard clause" in
acc, []
| h::t -> aux (process rps h) (h::acc) t
@@ -4677,7 +4676,7 @@ let rewrite_case (e,ann) =
let _ =
if !opt_coq_warn_nonexhaustive
- then Reporting.print_err false false
+ then Reporting.print_err
(fst ann) "Non-exhaustive matching" ("Example: " ^ string_of_rp example) in
let l = Parse_ast.Generated Parse_ast.Unknown in
@@ -4697,7 +4696,7 @@ let rewrite_case (e,ann) =
| (example::_) ->
let _ =
if !opt_coq_warn_nonexhaustive
- then Reporting.print_err false false
+ then Reporting.print_err
(fst ann) "Non-exhaustive let" ("Example: " ^ string_of_rp example) in
let l = Parse_ast.Generated Parse_ast.Unknown in
let p = P_aux (P_wild, (l, empty_tannot)) in
@@ -4727,7 +4726,7 @@ let rewrite_fun rewriters (FD_aux (FD_function (r,t,e,fcls),f_ann)) =
| (example::_) ->
let _ =
if !opt_coq_warn_nonexhaustive
- then Reporting.print_err false false
+ then Reporting.print_err
(fst f_ann) "Non-exhaustive matching" ("Example: " ^ string_of_rp example) in
let l = Parse_ast.Generated Parse_ast.Unknown in
@@ -4738,7 +4737,6 @@ let rewrite_fun rewriters (FD_aux (FD_function (r,t,e,fcls),f_ann)) =
let default = FCL_aux (FCL_Funcl (id,Pat_aux (Pat_exp (p,b),(l,empty_tannot))),fcl_ann) in
FD_aux (FD_function (r,t,e,fcls'@[default]),f_ann)
-
let rewrite =
let alg = { id_exp_alg with e_aux = rewrite_case } in
diff --git a/src/sail.ml b/src/sail.ml
index 2777b7a5..71bf4577 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -415,6 +415,6 @@ let _ = try
with Failure s -> raise (Reporting.err_general Parse_ast.Unknown ("Failure " ^ s))
end
with Reporting.Fatal_error e ->
- Reporting.report_error e;
+ Reporting.print_error e;
Interactive.opt_suppress_banner := true;
if !Interactive.opt_interactive then () else exit 1
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 940fbfe5..88e80dd2 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -51,7 +51,6 @@
open Ast
open Util
open Ast_util
-open Extra_pervasives
module Nameset = Set.Make(String)
@@ -95,7 +94,7 @@ let rec free_type_names_t consider_var (Typ_aux (t, l)) = 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 (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
- | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
+ | Typ_internal_unknown -> Reporting.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
@@ -130,7 +129,7 @@ let rec fv_of_typ consider_var bound used (Typ_aux (t,l)) : Nameset.t =
fv_of_typ consider_var
(List.fold_left (fun b (KOpt_aux (KOpt_kind (_, (Kid_aux (Var v,_))), _)) -> Nameset.add v b) bound kopts)
used t'
- | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
+ | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown"
and fv_of_targ consider_var bound used (Ast.A_aux(targ,_)) : Nameset.t = match targ with
| A_typ t -> fv_of_typ consider_var bound used t
diff --git a/src/specialize.ml b/src/specialize.ml
index 1ba57bd0..1881de5b 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -51,7 +51,6 @@
open Ast
open Ast_util
open Rewriter
-open Extra_pervasives
let is_typ_ord_uvar = function
| A_aux (A_typ _, _) -> true
@@ -68,7 +67,7 @@ let rec nexp_simp_typ (Typ_aux (typ_aux, l)) =
| 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_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
+ | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown"
in
Typ_aux (typ_aux, l)
and nexp_simp_typ_arg (A_aux (typ_arg_aux, l)) =
@@ -253,7 +252,7 @@ let rec typ_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) =
| 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_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
+ | 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
| A_nexp n -> KidSet.empty
@@ -270,7 +269,7 @@ let rec typ_int_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) =
| 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_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
+ | 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
| A_nexp n -> KidSet.diff (tyvars_of_nexp n) exs
diff --git a/src/type_check.ml b/src/type_check.ml
index b362e813..ad9fab34 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -52,7 +52,6 @@ open Ast
open Util
open Ast_util
open Lazy
-open Extra_pervasives
module Big_int = Nat_big_num
@@ -671,7 +670,7 @@ end = struct
wf_constraint ~exs:(KidSet.of_list (List.map kopt_kid kopts)) env nc;
wf_typ ~exs:(KidSet.of_list (List.map kopt_kid kopts)) { env with constraints = nc :: env.constraints } typ
| Typ_exist (_, _, _) -> typ_error env l ("Nested existentials are not allowed")
- | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
+ | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown"
and wf_typ_arg ?exs:(exs=KidSet.empty) env (A_aux (typ_arg_aux, _)) =
match typ_arg_aux with
| A_nexp nexp -> wf_nexp ~exs:exs env nexp
@@ -1232,7 +1231,7 @@ let rec is_typ_monomorphic (Typ_aux (typ, l)) =
| 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_exist _ | Typ_var _ -> false
- | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
+ | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown"
and is_typ_arg_monomorphic (A_aux (arg, _)) =
match arg with
| A_nexp _ -> true
@@ -1678,7 +1677,7 @@ let rec kid_order kind_map (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)) ([], kind_map) args
| Typ_fn _ | Typ_bidir _ | Typ_exist _ -> typ_error Env.empty l ("Existential or function type cannot appear within existential type: " ^ string_of_typ typ)
- | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
+ | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown"
and kid_order_arg kind_map (A_aux (aux, l) as arg) =
match aux with
| A_typ typ -> kid_order kind_map typ
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 06:06:42 +0000