Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
295c2913
Commit
295c2913
authored
Jan 26, 2016
by
Stefan Berghofer
Browse files
Improved error messages
parent
34ca0de3
Changes
1
Hide whitespace changes
Inline
Side-by-side
lib/isabelle/why3.ML.2015
View file @
295c2913
...
...
@@ -423,6 +423,129 @@ fun read_decl ctxt = variant
(map (elem "eqn" (fn atts => fn [t] =>
(get_name'' atts, expand_cases ctxt (read_prop ctxt t)))) xs))];
(**** pretty printing ****)
fun string_of_status NONE = "(* unproved *)"
| string_of_status (SOME _) = "(* proved *)";
fun pretty_typ s [] = Pretty.str s
| pretty_typ s [v] = Pretty.block
[Pretty.str v, Pretty.brk 1, Pretty.str s]
| pretty_typ s vs = Pretty.block
[Pretty.list "(" ")" (map Pretty.str vs), Pretty.brk 1, Pretty.str s];
fun blocks prfx1 prfx2 xs f = fst (fold_map (fn x => fn prfx =>
(Pretty.block (Pretty.str prfx :: Pretty.brk 1 :: f x),
prfx2))
xs prfx1);
fun pretty_decl (p, f) ctxt (Lemma ((s, _), prems, concls)) =
let
val SOME (opt, _, _) = lookup_vc (Proof_Context.theory_of ctxt) s;
val ctxt' = fold Variable.auto_fixes (prems @ concls) ctxt;
val (context, stmt) = mk_vc true prems concls
in
if p opt then
SOME (Pretty.big_list ("lemma " ^ s ^ ": " ^ f opt)
(Element.pretty_ctxt ctxt' context @
Element.pretty_stmt ctxt' stmt))
else NONE
end
| pretty_decl _ ctxt (Axiom ((s, _), ts)) =
let val ctxt' = fold Variable.auto_fixes ts ctxt
in SOME (Pretty.block
([Pretty.str "axiomatization where", Pretty.brk 1,
Pretty.str s, Pretty.str ":", Pretty.brk 1] @
separate (Pretty.brk 1)
(map (Pretty.quote o Syntax.pretty_term ctxt') ts)))
end
| pretty_decl _ ctxt (Typedecl ((s, _), args, opt_rhs)) = SOME (Pretty.block
(case opt_rhs of
NONE => [Pretty.str "typedecl", Pretty.brk 1,
pretty_typ s args]
| SOME T => [Pretty.str "type_synonym", Pretty.brk 1,
pretty_typ s args, Pretty.str " =", Pretty.brk 1,
Pretty.quote (Syntax.pretty_typ ctxt T)]))
| pretty_decl _ ctxt (Param ((s, _), T)) = SOME (Pretty.block
[Pretty.str "axiomatization", Pretty.brk 1,
Pretty.str s, Pretty.str " ::", Pretty.brk 1,
Pretty.quote (Syntax.pretty_typ ctxt T)])
| pretty_decl _ ctxt (Definition (_, eqn)) =
let
val ctxt' = Variable.auto_fixes eqn ctxt;
val (s, T) = head_of_eqn eqn
in SOME (Pretty.block [Pretty.str "definition ", Pretty.str s,
Pretty.str " ::", Pretty.brk 1,
Pretty.quote (Syntax.pretty_typ ctxt' T),
Pretty.str " where", Pretty.fbrk,
Pretty.quote (Syntax.pretty_term ctxt' eqn)])
end
| pretty_decl _ ctxt (Datatype dts) = SOME (Pretty.chunks
(blocks "datatype" "and" dts (fn ((s, _), args, constrs) =>
[pretty_typ s args,
Pretty.str " =", Pretty.brk 1] @
Pretty.separate " |"
(map (fn ((s', _), Ts) => Pretty.block
(separate (Pretty.brk 1) (Pretty.str s' ::
(map (Pretty.quote o
Syntax.pretty_typ ctxt) Ts))))
constrs))))
| pretty_decl _ ctxt (Inductive (coind, preds)) =
let val ctxt' = fold (fold (Variable.auto_fixes o snd) o #3) preds ctxt
in
SOME (Pretty.chunks
(blocks ((coind ? prefix "co") "inductive") "and" preds
(fn ((s, _), T, _) =>
[Pretty.str s, Pretty.str " ::", Pretty.brk 1,
Pretty.quote (Syntax.pretty_typ ctxt' T)]) @
Pretty.str "where" ::
blocks " " "|" (maps #3 preds) (fn ((s, _), t) =>
[Pretty.str s, Pretty.str ":",
Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt' t)])))
end
| pretty_decl _ ctxt (Function eqnss) =
let val ctxt' = fold (fold Variable.auto_fixes o snd) eqnss ctxt
in
SOME (Pretty.chunks
(blocks "fun" "and" eqnss (fn (_, t :: _) =>
let val (s, T) = head_of_eqn t
in
[Pretty.str s, Pretty.str " ::", Pretty.brk 1,
Pretty.quote (Syntax.pretty_typ ctxt' T)]
end) @
Pretty.str "where" ::
blocks " " "|" (maps snd eqnss)
(single o Pretty.quote o Syntax.pretty_term ctxt')))
end;
fun path_of_decl (Lemma ((_, SOME (s, _)), _, _)) = s
| path_of_decl (Axiom ((_, SOME (s, _)), _)) = s
| path_of_decl (Typedecl ((_, SOME (s, _)), _, _)) = s
| path_of_decl (Param ((_, SOME (s, _)), _)) = s
| path_of_decl (Definition (SOME (s, _), _)) = s
| path_of_decl (Datatype (((_, SOME (s, _)), _, _) :: _)) = s
| path_of_decl (Inductive (_, ((_, SOME (s, _)), _, _) :: _)) = s
| path_of_decl (Function ((SOME (s, _), _) :: _)) = s
| path_of_decl _ = "local";
fun show_status thy sel =
(case Why3_Data.get thy of
{env = SOME {decls, ...}, ...} =>
let
val ctxt = Proof_Context.init_global thy;
val decls' = AList.coalesce (op =)
(map (fn d => (path_of_decl d, d)) decls)
in
Pretty.writeln (Pretty.chunks2 (maps (fn (s, ds) =>
Pretty.str ("(**** " ^ s ^ " ****)") ::
map_filter (pretty_decl sel ctxt) ds) decls'))
end
| _ => ());
(**** processing declarations ****)
fun rename_const ps = map_aterms
(fn t as Const (p as (_, T)) => (case AList.lookup (op =) ps p of
SOME s => Free (s, T)
...
...
@@ -444,7 +567,12 @@ fun lookup_list sel lookup xs =
fun fact_binding s = Binding.qualify false "facts" (Binding.name s);
fun mk_decl _ (Axiom ((s, id), ts)) thy =
fun err_decl thy s decl =
error (Pretty.string_of (Pretty.blk (0,
[Pretty.str s, Pretty.fbrk, Pretty.fbrk,
the (pretty_decl (K true, K "") (Proof_Context.init_global thy) decl)])));
fun mk_decl _ (decl as Axiom ((s, id), ts)) thy =
(case lookup_thm thy id of
NONE =>
(thy |> Specification.axiomatization
...
...
@@ -454,7 +582,7 @@ fun mk_decl _ (Axiom ((s, id), ts)) thy =
if length thms = length ts andalso
forall (Pattern.matches thy o apfst Thm.prop_of) (thms ~~ ts)
then (thy, false)
else err
or
("Failed to match axiom " ^ string_of_id id))
else err
_decl thy
("Failed to match axiom " ^ string_of_id id)
decl
)
| mk_decl realize (Typedecl ((s, id), args, opt_rhs)) thy =
(case opt_rhs of
NONE =>
...
...
@@ -480,7 +608,7 @@ fun mk_decl _ (Axiom ((s, id), ts)) thy =
add_const s,
true)
| SOME s' => (add_const_raw NONE (s, s') thy, false))
| mk_decl _ (Definition (id, eqn)) thy =
| mk_decl _ (
decl as
Definition (id, eqn)) thy =
let val (s, _) = head_of_eqn eqn
in
case lookup_def thy id of
...
...
@@ -491,15 +619,17 @@ fun mk_decl _ (Axiom ((s, id), ts)) thy =
true)
| SOME [th] =>
let val p as (s', _) = head_of_eqn' (Thm.prop_of th)
handle TERM _ => error ("Bad equation for " ^ string_of_id id)
handle TERM _ => err_decl thy
("Bad equation for " ^ string_of_id id) decl
in
if Pattern.matches thy (rename_const [(p, s)] (Thm.prop_of th), eqn)
then (add_const_raw NONE (s, s') thy, false)
else error ("Failed to match definition " ^ string_of_id id)
else err_decl thy
("Failed to match definition " ^ string_of_id id) decl
end
| _ => err
or
("Single theorem expected for " ^ string_of_id id)
| _ => err
_decl thy
("Single theorem expected for " ^ string_of_id id)
decl
end
| mk_decl _ (Datatype dts) thy =
| mk_decl _ (
decl as
Datatype dts) thy =
(case lookup_list (snd o #1) (lookup_type' thy) dts of
NONE =>
(thy |> BNF_LFP_Compat.add_datatype [BNF_LFP_Compat.Keep_Nesting]
...
...
@@ -517,7 +647,8 @@ fun mk_decl _ (Axiom ((s, id), ts)) thy =
(fold (fn (((s, id), args, constrs), s') =>
let
val (args', constrs') = BNF_LFP_Compat.the_spec thy s';
fun err () = error ("Failed to match type " ^ string_of_id id);
fun err () = err_decl thy
("Failed to match type " ^ string_of_id id) decl;
val _ =
length args = length args' andalso
length constrs = length constrs' orelse err ();
...
...
@@ -538,7 +669,7 @@ fun mk_decl _ (Axiom ((s, id), ts)) thy =
end) dts' thy,
false)
end)
| mk_decl _ (Inductive (coind, preds)) thy =
| mk_decl _ (
decl as
Inductive (coind, preds)) thy =
(case lookup_list (snd o #1) (lookup_def thy) preds of
NONE =>
(thy |> Inductive.add_inductive_global
...
...
@@ -553,7 +684,7 @@ fun mk_decl _ (Axiom ((s, id), ts)) thy =
let val cmap = map (fn (((s, id), _, _), th :: _) =>
(th |> Thm.concl_of |> HOLogic.dest_Trueprop |> head_of |>
dest_Const handle TERM _ =>
err
or
("Bad introduction rule for " ^ string_of_id id),
err
_decl thy
("Bad introduction rule for " ^ string_of_id id)
decl
,
s)) preds'
in
app (fn (((_, id), _, intrs), intrs') =>
...
...
@@ -562,10 +693,11 @@ fun mk_decl _ (Axiom ((s, id), ts)) thy =
Pattern.matches thy (rename_const cmap (Thm.prop_of th), t))
(intrs, intrs')
then ()
else error ("Failed to match predicate " ^ string_of_id id)) preds';
else err_decl thy
("Failed to match predicate " ^ string_of_id id) decl) preds';
(fold (add_const_raw NONE o swap o apfst fst) cmap thy, false)
end)
| mk_decl _ (Function eqnss) thy =
| mk_decl _ (
decl as
Function eqnss) thy =
let val eqnss' = map (head_of_eqn o hd o snd) eqnss
in
case lookup_list fst (lookup_def thy) eqnss of
...
...
@@ -579,7 +711,7 @@ fun mk_decl _ (Axiom ((s, id), ts)) thy =
| SOME eqnss'' =>
let val cmap = map2 (fn ((id, _), th :: _) => fn (s, _) =>
(th |> Thm.prop_of |> head_of_eqn' handle TERM _ =>
err
or
("Bad equation for " ^ string_of_id id),
err
_decl thy
("Bad equation for " ^ string_of_id id)
decl
,
s)) eqnss'' eqnss'
in
app (fn ((id, eqns), eqns') =>
...
...
@@ -588,7 +720,8 @@ fun mk_decl _ (Axiom ((s, id), ts)) thy =
Pattern.matches thy (rename_const cmap (Thm.prop_of th), t))
(eqns, eqns')
then ()
else error ("Failed to match function " ^ string_of_id id)) eqnss'';
else err_decl thy
("Failed to match function " ^ string_of_id id) decl) eqnss'';
(fold (add_const_raw NONE o swap o apfst fst) cmap thy, false)
end
end
...
...
@@ -667,126 +800,6 @@ fun process_decls consts types x path = elem "theory" (fn atts =>
| _ => error "Bad theory specification")) x
(**** pretty printing ****)
fun string_of_status NONE = "(* unproved *)"
| string_of_status (SOME _) = "(* proved *)";
fun pretty_typ s [] = Pretty.str s
| pretty_typ s [v] = Pretty.block
[Pretty.str v, Pretty.brk 1, Pretty.str s]
| pretty_typ s vs = Pretty.block
[Pretty.list "(" ")" (map Pretty.str vs), Pretty.brk 1, Pretty.str s];
fun blocks prfx1 prfx2 xs f = fst (fold_map (fn x => fn prfx =>
(Pretty.block (Pretty.str prfx :: Pretty.brk 1 :: f x),
prfx2))
xs prfx1);
fun pretty_decl (p, f) ctxt (Lemma ((s, _), prems, concls)) =
let
val SOME (opt, _, _) = lookup_vc (Proof_Context.theory_of ctxt) s;
val ctxt' = fold Variable.auto_fixes (prems @ concls) ctxt;
val (context, stmt) = mk_vc true prems concls
in
if p opt then
SOME (Pretty.big_list ("lemma " ^ s ^ ": " ^ f opt)
(Element.pretty_ctxt ctxt' context @
Element.pretty_stmt ctxt' stmt))
else NONE
end
| pretty_decl _ ctxt (Axiom ((s, _), ts)) =
let val ctxt' = fold Variable.auto_fixes ts ctxt
in SOME (Pretty.block
([Pretty.str "axiomatization where", Pretty.brk 1,
Pretty.str s, Pretty.str ":", Pretty.brk 1] @
separate (Pretty.brk 1)
(map (Pretty.quote o Syntax.pretty_term ctxt') ts)))
end
| pretty_decl _ ctxt (Typedecl ((s, _), args, opt_rhs)) = SOME (Pretty.block
(case opt_rhs of
NONE => [Pretty.str "typedecl", Pretty.brk 1,
pretty_typ s args]
| SOME T => [Pretty.str "type_synonym", Pretty.brk 1,
pretty_typ s args, Pretty.str " =", Pretty.brk 1,
Pretty.quote (Syntax.pretty_typ ctxt T)]))
| pretty_decl _ ctxt (Param ((s, _), T)) = SOME (Pretty.block
[Pretty.str "axiomatization", Pretty.brk 1,
Pretty.str s, Pretty.str " ::", Pretty.brk 1,
Pretty.quote (Syntax.pretty_typ ctxt T)])
| pretty_decl _ ctxt (Definition (_, eqn)) =
let
val ctxt' = Variable.auto_fixes eqn ctxt;
val (s, T) = head_of_eqn eqn
in SOME (Pretty.block [Pretty.str "definition ", Pretty.str s,
Pretty.str " ::", Pretty.brk 1,
Pretty.quote (Syntax.pretty_typ ctxt' T),
Pretty.str " where", Pretty.fbrk,
Pretty.quote (Syntax.pretty_term ctxt' eqn)])
end
| pretty_decl _ ctxt (Datatype dts) = SOME (Pretty.chunks
(blocks "datatype" "and" dts (fn ((s, _), args, constrs) =>
[pretty_typ s args,
Pretty.str " =", Pretty.brk 1] @
Pretty.separate " |"
(map (fn ((s', _), Ts) => Pretty.block
(separate (Pretty.brk 1) (Pretty.str s' ::
(map (Pretty.quote o
Syntax.pretty_typ ctxt) Ts))))
constrs))))
| pretty_decl _ ctxt (Inductive (coind, preds)) =
let val ctxt' = fold (fold (Variable.auto_fixes o snd) o #3) preds ctxt
in
SOME (Pretty.chunks
(blocks ((coind ? prefix "co") "inductive") "and" preds
(fn ((s, _), T, _) =>
[Pretty.str s, Pretty.str " ::", Pretty.brk 1,
Pretty.quote (Syntax.pretty_typ ctxt' T)]) @
Pretty.str "where" ::
blocks " " "|" (maps #3 preds) (fn ((s, _), t) =>
[Pretty.str s, Pretty.str ":",
Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt' t)])))
end
| pretty_decl _ ctxt (Function eqnss) =
let val ctxt' = fold (fold Variable.auto_fixes o snd) eqnss ctxt
in
SOME (Pretty.chunks
(blocks "fun" "and" eqnss (fn (_, t :: _) =>
let val (s, T) = head_of_eqn t
in
[Pretty.str s, Pretty.str " ::", Pretty.brk 1,
Pretty.quote (Syntax.pretty_typ ctxt' T)]
end) @
Pretty.str "where" ::
blocks " " "|" (maps snd eqnss)
(single o Pretty.quote o Syntax.pretty_term ctxt')))
end;
fun path_of_decl (Lemma ((_, SOME (s, _)), _, _)) = s
| path_of_decl (Axiom ((_, SOME (s, _)), _)) = s
| path_of_decl (Typedecl ((_, SOME (s, _)), _, _)) = s
| path_of_decl (Param ((_, SOME (s, _)), _)) = s
| path_of_decl (Definition (SOME (s, _), _)) = s
| path_of_decl (Datatype (((_, SOME (s, _)), _, _) :: _)) = s
| path_of_decl (Inductive (_, ((_, SOME (s, _)), _, _) :: _)) = s
| path_of_decl (Function ((SOME (s, _), _) :: _)) = s
| path_of_decl _ = "local";
fun show_status thy sel =
(case Why3_Data.get thy of
{env = SOME {decls, ...}, ...} =>
let
val ctxt = Proof_Context.init_global thy;
val decls' = AList.coalesce (op =)
(map (fn d => (path_of_decl d, d)) decls)
in
Pretty.writeln (Pretty.chunks2 (maps (fn (s, ds) =>
Pretty.str ("(**** " ^ s ^ " ****)") ::
map_filter (pretty_decl sel ctxt) ds) decls'))
end
| _ => ());
(**** commands ****)
fun why3_open ((files, consts), types) thy =
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment