Commit 540cad55 authored by Sylvain Dailler's avatar Sylvain Dailler

Trying to catch errors for transformations with arguments. It raises

problems illustrated by the example committed.

Trying to put second assert before use_th reports a parsing/typing error
that cannot be understood by a normal user (in my opinion).
parent b7c18ad8
......@@ -243,9 +243,9 @@ rule token = parse
let parse_term lb = Parser.term_eof token lb
let parse_term lb = Loc.with_location (Parser.term_eof token) lb
let parse_list_ident lb = Parser.ident_comma_list token lb
let parse_list_ident lb = Loc.with_location (Parser.ident_comma_list token) lb
let parse_logic_file env path lb =
open_file token (Lexing.from_string "") (Typing.open_file env path);
......@@ -237,6 +237,7 @@ let get_exception_message ses id fmt e =
Format.fprintf fmt "Following hypothesis was not found: %s \n" s
| Args_wrapper.Arg_theory_not_found (s) ->
Format.fprintf fmt "Theory not found: %s" s
| Loc.Located (loc, s) -> Format.fprintf fmt "Parsing error at %a: %a" Loc.report_position loc Exn_printer.exn_printer s
| e ->
bypass_pretty ses id fmt e
module Test
(* Inspired from isqrt *)
use import int.Int
function sqr (x:int) : int = x * x
lemma sqr_non_neg: forall x:int. sqr x >= 0
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
<why3session shape_version="4">
<file name="../test_args_parsing.mlw">
<theory name="Test" sum="8dec774bbde4869623e4ebbfa310d0c8">
<goal name="sqr_non_neg">
<transf name="assert" arg1="(exists x. x = 6.1)">
<goal name="sqr_non_neg.0">
<transf name="use_th" arg1="real.Real">
<goal name="sqr_non_neg.0.0">
<transf name="assert" arg1="(exists x. forall y. x = y + 5.3)">
<goal name="sqr_non_neg.0.0.0">
<goal name="sqr_non_neg.0.0.1">
<goal name="sqr_non_neg.1">
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment