From e68dbe5eb7cc14ba5853a5fa8c9a05b58ff6572d Mon Sep 17 00:00:00 2001
From: Sylvain Dailler <dailler@adacore.com>
Date: Fri, 1 Jun 2018 16:03:47 +0200
Subject: [PATCH] tactic apply: add appropriate exception. simplify code and
 allow inductive

As a side effect, this also modifies reflection.ml accordingly.
---
 examples/bts/126_apply.mlw             |  16 ++++++++++
 examples/bts/126_apply/why3session.xml |  41 +++++++++++++++++++++++++
 examples/bts/126_apply/why3shapes.gz   | Bin 0 -> 235 bytes
 src/session/itp_server.ml              |   2 ++
 src/transform/apply.ml                 |  25 ++++-----------
 src/transform/args_wrapper.ml          |   1 +
 src/transform/args_wrapper.mli         |   1 +
 src/transform/reflection.ml            |  10 +++---
 8 files changed, 73 insertions(+), 23 deletions(-)
 create mode 100644 examples/bts/126_apply.mlw
 create mode 100644 examples/bts/126_apply/why3session.xml
 create mode 100644 examples/bts/126_apply/why3shapes.gz

diff --git a/examples/bts/126_apply.mlw b/examples/bts/126_apply.mlw
new file mode 100644
index 0000000000..4e0303ca6d
--- /dev/null
+++ b/examples/bts/126_apply.mlw
@@ -0,0 +1,16 @@
+
+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
diff --git a/examples/bts/126_apply/why3session.xml b/examples/bts/126_apply/why3session.xml
new file mode 100644
index 0000000000..c4094e6eec
--- /dev/null
+++ b/examples/bts/126_apply/why3session.xml
@@ -0,0 +1,41 @@
+<?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>
diff --git a/examples/bts/126_apply/why3shapes.gz b/examples/bts/126_apply/why3shapes.gz
new file mode 100644
index 0000000000000000000000000000000000000000..d461d058c9e552304313e060f7e909f82212c410
GIT binary patch
literal 235
zcmb2|=3oGW|FQj+dCrDBF2C!!zGrGodKC1;AV%dt?`oA3AC(U<GA&O$`aSJfRayV6
zPRE1SxK<Z3cb#i=DDD2bRqm*`)ta1+l>2M8+_ZG@Jk4z4ZZH4%-;M9@Z$~FSR1MT#
zm~(pP@z;yD<u<sUe44U9Z;wQ>i)VlrYqQVM5XmYp9jyiRc@`%=_&v0lTeQwfR4m6|
z>~6aI`}idfKJ`R;Oe}t4G<#N#%&Te>xd%3OTi>^?XMEhl`fh@3nwtV|-7nD@$vgfP
p{xPaL$(h3=5XVwo8q(Q3F~IHEj-$^X|112<AaXomR|O*j0|3+<ZSepA

literal 0
HcmV?d00001

diff --git a/src/session/itp_server.ml b/src/session/itp_server.ml
index b04ae219c4..e6ba1c6cb1 100644
--- a/src/session/itp_server.ml
+++ b/src/session/itp_server.ml
@@ -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, ""
   | Args_wrapper.Arg_qid_not_found q ->
       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 ->
       Pp.sprintf "Transformation raised a general error: %s \n" s, Loc.dummy_position, ""
   | Args_wrapper.Arg_theory_not_found s ->
diff --git a/src/transform/apply.ml b/src/transform/apply.ml
index ab70f09900..a8536b0412 100644
--- a/src/transform/apply.ml
+++ b/src/transform/apply.ml
@@ -43,20 +43,6 @@ let term_decl d =
   | Decl ({d_node = Dprop (_pk, _pr, t)}) -> t
   | _ -> 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
    not part of the substitution and try to match them with the list of values
    from wt (ordered). *)
@@ -156,13 +142,14 @@ let matching_with_terms ~trans_name slv lv left_term right_term withed_terms =
       with values found in 2).
  *)
 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 = term_decl g in
-  let d = find_hypothesis name task in
-  if d = None then raise (Arg_error "apply");
-  let d = Opt.get d in
-  let t = term_decl d in
+  let t =
+    match find_prop_decl kn pr with
+    | (_, t) -> t
+    | exception Not_found -> raise (Arg_pr_not_found pr)
+  in
   let (lp, lv, nt) = intros t 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
diff --git a/src/transform/args_wrapper.ml b/src/transform/args_wrapper.ml
index ba30f16d07..1f5997b620 100644
--- a/src/transform/args_wrapper.ml
+++ b/src/transform/args_wrapper.ml
@@ -22,6 +22,7 @@ exception Arg_expected of string * string
 exception Arg_theory_not_found of string
 exception Arg_expected_none of string
 exception Arg_qid_not_found of Ptree.qualid
+exception Arg_pr_not_found of prsymbol
 exception Arg_error of string
 
 let () = Exn_printer.register
diff --git a/src/transform/args_wrapper.mli b/src/transform/args_wrapper.mli
index 919a1f9c48..1133993d97 100644
--- a/src/transform/args_wrapper.mli
+++ b/src/transform/args_wrapper.mli
@@ -23,6 +23,7 @@ exception Parse_error of string
 exception Arg_expected of string * string
 exception Arg_theory_not_found 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_error of string
 
diff --git a/src/transform/reflection.ml b/src/transform/reflection.ml
index 0fdb4484dd..c08931090a 100644
--- a/src/transform/reflection.ml
+++ b/src/transform/reflection.ml
@@ -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 = Apply.term_decl g in
   Debug.dprintf debug_refl "start@.";
-  let d = Apply.find_hypothesis pr.pr_name prev in
-  if d = None then raise (Exit "lemma not found");
-  let d = Opt.get d in
-  let l = Apply.term_decl d in
+  let l =
+    let kn' = task_known prev in (* TODO Do we want kn here ? *)
+    match find_prop_decl kn' pr with
+    | (_, t) -> t
+    | exception Not_found -> raise (Exit "lemma not found")
+  in
   let (lp, lv, rt) = Apply.intros l in
   let nt = Args_wrapper.build_naming_tables task in
   let crc = nt.Trans.coercion in
-- 
GitLab