Commit e68dbe5e authored by Sylvain Dailler's avatar Sylvain Dailler

tactic apply: add appropriate exception. simplify code and allow inductive

As a side effect, this also modifies reflection.ml accordingly.
parent 3805da95
module A
use import int.Int
inductive even (n: int) =
| Zero : even 0
| Pair : forall n. even n -> even (n+2)
goal a: even 4
inductive unit = tt : unit
goal g : unit
end
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../126_apply.mlw" proved="true">
<theory name="A" proved="true">
<goal name="a" proved="true">
<transf name="replace" proved="true" arg1="4" arg2="(2+2)">
<goal name="a.0" proved="true">
<transf name="apply" proved="true" arg1="Pair">
<goal name="a.0.0" proved="true">
<transf name="replace" proved="true" arg1="2" arg2="(0 + 2)">
<goal name="a.0.0.0" proved="true">
<transf name="apply" proved="true" arg1="Pair">
<goal name="a.0.0.0.0" proved="true">
<transf name="apply" proved="true" arg1="Zero">
</transf>
</goal>
</transf>
</goal>
<goal name="a.0.0.1" proved="true">
<transf name="compute_in_goal" proved="true" >
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="a.1" proved="true">
<transf name="compute_in_goal" proved="true" >
</transf>
</goal>
</transf>
</goal>
<goal name="g" proved="true">
<transf name="apply" proved="true" arg1="tt">
</transf>
</goal>
</theory>
</file>
</why3session>
...@@ -247,6 +247,8 @@ let get_exception_message ses id e = ...@@ -247,6 +247,8 @@ let get_exception_message ses id e =
Pp.sprintf "Error in transformation %s. Cannot infer type of polymorphic element" s, Loc.dummy_position, "" Pp.sprintf "Error in transformation %s. Cannot infer type of polymorphic element" s, Loc.dummy_position, ""
| Args_wrapper.Arg_qid_not_found q -> | Args_wrapper.Arg_qid_not_found q ->
Pp.sprintf "Following hypothesis was not found: %a \n" Typing.print_qualid q, Loc.dummy_position, "" Pp.sprintf "Following hypothesis was not found: %a \n" Typing.print_qualid q, Loc.dummy_position, ""
| Args_wrapper.Arg_pr_not_found pr ->
Pp.sprintf "Property not found: %a" (print_pr ses id) pr, Loc.dummy_position, ""
| Args_wrapper.Arg_error s -> | Args_wrapper.Arg_error s ->
Pp.sprintf "Transformation raised a general error: %s \n" s, Loc.dummy_position, "" Pp.sprintf "Transformation raised a general error: %s \n" s, Loc.dummy_position, ""
| Args_wrapper.Arg_theory_not_found s -> | Args_wrapper.Arg_theory_not_found s ->
......
...@@ -43,20 +43,6 @@ let term_decl d = ...@@ -43,20 +43,6 @@ let term_decl d =
| Decl ({d_node = Dprop (_pk, _pr, t)}) -> t | Decl ({d_node = Dprop (_pk, _pr, t)}) -> t
| _ -> raise (Arg_trans "term_decl") | _ -> raise (Arg_trans "term_decl")
let pr_prsymbol pr =
match pr with
| Decl {d_node = Dprop (_pk, pr, _t)} -> Some pr
| _ -> None
(* Looks for the hypothesis name and return it. If not found return None *)
let find_hypothesis (name:Ident.ident) task =
let ndecl = ref None in
let _ = task_iter (fun x -> if (
match (pr_prsymbol x.td_node) with
| None -> false
| Some pr -> Ident.id_equal pr.pr_name name) then ndecl := Some x) task in
!ndecl
(* [with_terms subst_ty subst lv wt]: Takes the list of variables in lv that are (* [with_terms subst_ty subst lv wt]: Takes the list of variables in lv that are
not part of the substitution and try to match them with the list of values not part of the substitution and try to match them with the list of values
from wt (ordered). *) from wt (ordered). *)
...@@ -156,13 +142,14 @@ let matching_with_terms ~trans_name slv lv left_term right_term withed_terms = ...@@ -156,13 +142,14 @@ let matching_with_terms ~trans_name slv lv left_term right_term withed_terms =
with values found in 2). with values found in 2).
*) *)
let apply pr withed_terms : Task.task Trans.tlist = Trans.store (fun task -> let apply pr withed_terms : Task.task Trans.tlist = Trans.store (fun task ->
let name = pr.pr_name in let kn = task_known task in
let g, task = Task.task_separate_goal task in let g, task = Task.task_separate_goal task in
let g = term_decl g in let g = term_decl g in
let d = find_hypothesis name task in let t =
if d = None then raise (Arg_error "apply"); match find_prop_decl kn pr with
let d = Opt.get d in | (_, t) -> t
let t = term_decl d in | exception Not_found -> raise (Arg_pr_not_found pr)
in
let (lp, lv, nt) = intros t in let (lp, lv, nt) = intros t in
let slv = List.fold_left (fun acc v -> Svs.add v acc) Svs.empty lv in let slv = List.fold_left (fun acc v -> Svs.add v acc) Svs.empty lv in
match matching_with_terms ~trans_name:"apply" slv lv nt g withed_terms with match matching_with_terms ~trans_name:"apply" slv lv nt g withed_terms with
......
...@@ -22,6 +22,7 @@ exception Arg_expected of string * string ...@@ -22,6 +22,7 @@ exception Arg_expected of string * string
exception Arg_theory_not_found of string exception Arg_theory_not_found of string
exception Arg_expected_none of string exception Arg_expected_none of string
exception Arg_qid_not_found of Ptree.qualid exception Arg_qid_not_found of Ptree.qualid
exception Arg_pr_not_found of prsymbol
exception Arg_error of string exception Arg_error of string
let () = Exn_printer.register let () = Exn_printer.register
......
...@@ -23,6 +23,7 @@ exception Parse_error of string ...@@ -23,6 +23,7 @@ exception Parse_error of string
exception Arg_expected of string * string exception Arg_expected of string * string
exception Arg_theory_not_found of string exception Arg_theory_not_found of string
exception Arg_expected_none of string exception Arg_expected_none of string
exception Arg_pr_not_found of Decl.prsymbol
exception Arg_qid_not_found of Ptree.qualid exception Arg_qid_not_found of Ptree.qualid
exception Arg_error of string exception Arg_error of string
......
...@@ -579,10 +579,12 @@ let reflection_by_lemma pr env : Task.task Trans.tlist = Trans.store (fun task - ...@@ -579,10 +579,12 @@ let reflection_by_lemma pr env : Task.task Trans.tlist = Trans.store (fun task -
let g, prev = Task.task_separate_goal task in let g, prev = Task.task_separate_goal task in
let g = Apply.term_decl g in let g = Apply.term_decl g in
Debug.dprintf debug_refl "start@."; Debug.dprintf debug_refl "start@.";
let d = Apply.find_hypothesis pr.pr_name prev in let l =
if d = None then raise (Exit "lemma not found"); let kn' = task_known prev in (* TODO Do we want kn here ? *)
let d = Opt.get d in match find_prop_decl kn' pr with
let l = Apply.term_decl d in | (_, t) -> t
| exception Not_found -> raise (Exit "lemma not found")
in
let (lp, lv, rt) = Apply.intros l in let (lp, lv, rt) = Apply.intros l in
let nt = Args_wrapper.build_naming_tables task in let nt = Args_wrapper.build_naming_tables task in
let crc = nt.Trans.coercion in let crc = nt.Trans.coercion 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