diff options
Diffstat (limited to 'contrib/correctness/perror.ml')
| -rw-r--r-- | contrib/correctness/perror.ml | 172 |
1 files changed, 172 insertions, 0 deletions
diff --git a/contrib/correctness/perror.ml b/contrib/correctness/perror.ml new file mode 100644 index 00000000..40fe4c98 --- /dev/null +++ b/contrib/correctness/perror.ml @@ -0,0 +1,172 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: perror.ml,v 1.9.2.1 2004/07/16 19:30:01 herbelin Exp $ *) + +open Pp +open Util +open Names +open Nameops +open Term +open Himsg + +open Ptype +open Past + +let is_mutable = function Ref _ | Array _ -> true | _ -> false +let is_pure = function TypePure _ -> true | _ -> false + +let raise_with_loc = function + | None -> raise + | Some loc -> Stdpp.raise_with_loc loc + +let unbound_variable id loc = + raise_with_loc loc + (UserError ("Perror.unbound_variable", + (hov 0 (str"Unbound variable" ++ spc () ++ pr_id id ++ fnl ())))) + +let unbound_reference id loc = + raise_with_loc loc + (UserError ("Perror.unbound_reference", + (hov 0 (str"Unbound reference" ++ spc () ++ pr_id id ++ fnl ())))) + +let clash id loc = + raise_with_loc loc + (UserError ("Perror.clash", + (hov 0 (str"Clash with previous constant" ++ spc () ++ + str(string_of_id id) ++ fnl ())))) + +let not_defined id = + raise + (UserError ("Perror.not_defined", + (hov 0 (str"The object" ++ spc () ++ pr_id id ++ spc () ++ + str"is not defined" ++ fnl ())))) + +let check_for_reference loc id = function + Ref _ -> () + | _ -> Stdpp.raise_with_loc loc + (UserError ("Perror.check_for_reference", + hov 0 (pr_id id ++ spc () ++ + str"is not a reference"))) + +let check_for_array loc id = function + Array _ -> () + | _ -> Stdpp.raise_with_loc loc + (UserError ("Perror.check_for_array", + hov 0 (pr_id id ++ spc () ++ + str"is not an array"))) + +let is_constant_type s = function + TypePure c -> + let id = id_of_string s in + let c' = Constrintern.global_reference id in + Reductionops.is_conv (Global.env()) Evd.empty c c' + | _ -> false + +let check_for_index_type loc v = + let is_index = is_constant_type "Z" v in + if not is_index then + Stdpp.raise_with_loc loc + (UserError ("Perror.check_for_index", + hov 0 (str"This expression is an index" ++ spc () ++ + str"and should have type int (Z)"))) + +let check_no_effect loc ef = + if not (Peffect.get_writes ef = []) then + Stdpp.raise_with_loc loc + (UserError ("Perror.check_no_effect", + hov 0 (str"A boolean should not have side effects" +))) + +let should_be_boolean loc = + Stdpp.raise_with_loc loc + (UserError ("Perror.should_be_boolean", + hov 0 (str"This expression is a test:" ++ spc () ++ + str"it should have type bool"))) + +let test_should_be_annotated loc = + Stdpp.raise_with_loc loc + (UserError ("Perror.test_should_be_annotated", + hov 0 (str"This test should be annotated"))) + +let if_branches loc = + Stdpp.raise_with_loc loc + (UserError ("Perror.if_branches", + hov 0 (str"The two branches of an `if' expression" ++ spc () ++ + str"should have the same type"))) + +let check_for_not_mutable loc v = + if is_mutable v then + Stdpp.raise_with_loc loc + (UserError ("Perror.check_for_not_mutable", + hov 0 (str"This expression cannot be a mutable"))) + +let check_for_pure_type loc v = + if not (is_pure v) then + Stdpp.raise_with_loc loc + (UserError ("Perror.check_for_pure_type", + hov 0 (str"This expression must be pure" ++ spc () ++ + str"(neither a mutable nor a function)"))) + +let check_for_let_ref loc v = + if not (is_pure v) then + Stdpp.raise_with_loc loc + (UserError ("Perror.check_for_let_ref", + hov 0 (str"References can only be bound in pure terms"))) + +let informative loc s = + Stdpp.raise_with_loc loc + (UserError ("Perror.variant_informative", + hov 0 (str s ++ spc () ++ str"must be informative"))) + +let variant_informative loc = informative loc "Variant" +let should_be_informative loc = informative loc "This term" + +let app_of_non_function loc = + Stdpp.raise_with_loc loc + (UserError ("Perror.app_of_non_function", + hov 0 (str"This term cannot be applied" ++ spc () ++ + str"(either it is not a function" ++ spc () ++ + str"or it is applied to non pure arguments)"))) + +let partial_app loc = + Stdpp.raise_with_loc loc + (UserError ("Perror.partial_app", + hov 0 (str"This function does not have" ++ + spc () ++ str"the right number of arguments"))) + +let expected_type loc s = + Stdpp.raise_with_loc loc + (UserError ("Perror.expected_type", + hov 0 (str"Argument is expected to have type" ++ spc () ++ s))) + +let expects_a_type id loc = + Stdpp.raise_with_loc loc + (UserError ("Perror.expects_a_type", + hov 0 (str"The argument " ++ pr_id id ++ spc () ++ + str"in this application is supposed to be a type"))) + +let expects_a_term id = + raise + (UserError ("Perror.expects_a_type", + hov 0 (str"The argument " ++ pr_id id ++ spc () ++ + str"in this application is supposed to be a term"))) + +let should_be_a_variable loc = + Stdpp.raise_with_loc loc + (UserError ("Perror.should_be_a_variable", + hov 0 (str"Argument should be a variable"))) + +let should_be_a_reference loc = + Stdpp.raise_with_loc loc + (UserError ("Perror.should_be_a_reference", + hov 0 (str"Argument of function should be a reference"))) + + |