From 35ffacadfb5e2cbc9b02510447a038ce50bccd96 Mon Sep 17 00:00:00 2001
From: Sylvain Dailler <dailler@adacore.com>
Date: Thu, 20 Sep 2018 14:14:14 +0200
Subject: [PATCH] [transform apply] let is now a premise for applied condition
of apply
---
examples/bts/185_apply_let.mlw | 11 +++++++++++
examples/bts/185_apply_let/why3session.xml | 17 +++++++++++++++++
examples/bts/185_apply_let/why3shapes.gz | Bin 0 -> 96 bytes
src/transform/apply.ml | 4 ++++
4 files changed, 32 insertions(+)
create mode 100644 examples/bts/185_apply_let.mlw
create mode 100644 examples/bts/185_apply_let/why3session.xml
create mode 100644 examples/bts/185_apply_let/why3shapes.gz
diff --git a/examples/bts/185_apply_let.mlw b/examples/bts/185_apply_let.mlw
new file mode 100644
index 000000000..1cc058847
--- /dev/null
+++ b/examples/bts/185_apply_let.mlw
@@ -0,0 +1,11 @@
+module Test
+
+ function f int : int = 17
+ predicate p int int
+ axiom A: forall x y. x = f y -> p x y
+ axiom B: forall y. let x = f y in p x y
+
+ goal g : p 17 42
+
+
+end
diff --git a/examples/bts/185_apply_let/why3session.xml b/examples/bts/185_apply_let/why3session.xml
new file mode 100644
index 000000000..566ae5225
--- /dev/null
+++ b/examples/bts/185_apply_let/why3session.xml
@@ -0,0 +1,17 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="5">
+<file name="../185_apply_let.mlw" proved="true">
+<theory name="Test" proved="true">
+ <goal name="g" proved="true">
+ <transf name="apply" proved="true" arg1="B">
+ <goal name="g.0" proved="true">
+ <transf name="compute_in_goal" proved="true" >
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+</theory>
+</file>
+</why3session>
diff --git a/examples/bts/185_apply_let/why3shapes.gz b/examples/bts/185_apply_let/why3shapes.gz
new file mode 100644
index 0000000000000000000000000000000000000000..208b982bb8a95f1ffbd12f9b0133b29b78219ac0
GIT binary patch
literal 96
zcmb2|=3oGW|DvaN^EMdpupXGFY2=h-T^MB0V{g;R7HDL5;XWsKRnoGEh8DghyPCJS
zS6$F4bH6Nb>sf-=HW$&!H{GMRUO#$IB=7X58<h`hPW`JqY#&#DHX|^Gfq?-4pG+tN
literal 0
HcmV?d00001
diff --git a/src/transform/apply.ml b/src/transform/apply.ml
index cb55496d0..07cf91e60 100644
--- a/src/transform/apply.ml
+++ b/src/transform/apply.ml
@@ -35,6 +35,10 @@ let intros f =
| Tquant (Tforall, fq) ->
let vsl, _, fs = t_open_quant fq in
intros_aux lp (lv @ vsl) fs
+ | Tlet (t, tb) ->
+ let vs, t2 = t_open_bound tb in
+ let f = t_equ (t_var vs) t in
+ intros_aux (f :: lp) ([vs] @ lv) t2
| _ -> (lp, lv, f) in
intros_aux [] [] f
--
GitLab