Commit b3eaa866 authored by MARCHE Claude's avatar MARCHE Claude

improve error message for 'apply' transformation

this goes towards solving issue #19
parent 65d5c037
module Issue19
use import int.Int
axiom H : forall x y z. x < y -> y < z -> x < z
goal g: 0 < 2
(* we want to do
apply H with 1
to generate two new goals "0 < 1" and "1 < 2"
*)
type t
predicate r t t
axiom trans: forall x y z. r x y -> r y z -> r x z
constant a:t
constant b:t
constant c:t
axiom a1: r a b
axiom a2: r b c
goal test: r a c
(* apply trans with b *)
end
\ No newline at end of file
......@@ -88,6 +88,12 @@ let apply pr : Task.task Trans.tlist = Trans.store (fun task ->
else ()); raise (Arg_trans_pattern ("apply", p1, p2))
| Reduction_engine.NoMatch None -> raise (Arg_trans ("apply"))
in
Svs.iter
(fun v ->
try ignore (Mvs.find v subst)
with Not_found ->
raise (Arg_trans ("no instance found for " ^ v.vs_name.Ident.id_string)))
lv;
let inst_nt = t_ty_subst subst_ty subst nt in
if (Term.t_equal_nt_nl inst_nt g) then
let nlp = List.map (t_ty_subst subst_ty subst) lp in
......
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