Commit c7053bd6 authored by Sylvain Dailler's avatar Sylvain Dailler

Merge branch 'apply_let'

parents b5ae3f8e f431ccc7
module Ex1
use int.Int
function f int : int
predicate p int
axiom B: forall y. let x = f y in x >= 0 -> p y
goal g : p 42
end
module Ex2
function f int : int
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
module Ex3
type a constant a0: a
type b constant b0: b
type c constant c0: c
function f unit : b
function g unit : c
predicate p a b c
axiom a : forall a.
let b = f () in
let c = g () in
p a b c ->
false
goal g : false
end
<?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.mlw">
<theory name="Ex1">
<goal name="g">
</goal>
</theory>
<theory name="Ex2">
<goal name="g">
</goal>
</theory>
<theory name="Ex3">
<goal name="g">
</goal>
</theory>
</file>
</why3session>
This diff is collapsed.
val intros: Term.term ->
Term.term list * Term.vsymbol list * (Term.vsymbol * Term.term) list * Term.term
(* intros returns a tuple containing:
- list of premises of the term,
- list of universally quantified variables at head of the terms,
- list of let-binding at head of the term,
- the term without premises/let-binding and forall variables at head.
*)
val rewrite_list: Term.term list option -> bool -> bool -> Decl.prsymbol list ->
Decl.prsymbol option -> Task.task list Trans.trans
(* [rewrite_list with_terms rev opt hl h1]
@param opt: If set, all the rewritings are optional
@param rev: If set, all the rewritings are from right to left
@param with_terms: A list of terms to instantiate variables that cannot be
matched (TODO this probably does not work: remove this argument ?)
@param hl: list of rewrite hypothesis
@param h1: hypothesis to rewrite in
*)
val term_decl: Theory.tdecl -> Term.term
(* Return the term associated to a prop declaration or raise an error in every
other cases *)
......@@ -605,7 +605,9 @@ let reflection_by_lemma pr env : Task.task Trans.tlist = Trans.store (fun task -
| (_, t) -> t
| exception Not_found -> raise (Exit "lemma not found")
in
let (lp, lv, rt) = Apply.intros l in
(* TODO solve llet assert *)
let (lp, lv, llet, rt) = Apply.intros l in
assert (llet = []);
let nt = Args_wrapper.build_naming_tables task in
let crc = nt.Trans.coercion in
let renv = reify_term (init_renv kn crc lv env prev) g rt in
......@@ -664,7 +666,9 @@ let reflection_by_function do_trans s env = Trans.store (fun task ->
Debug.dprintf debug_refl "new post@.";
Debug.dprintf debug_refl "post: %a, %a@."
Pretty.print_vs vres Pretty.print_term p;
let (lp, lv, rt) = Apply.intros p in
(* TODO solve this llet assert *)
let (lp, lv, llet, rt) = Apply.intros p in
assert (llet = []);
let lv = lv @ args in
let renv = reify_term (init_renv kn crc lv env prev) g rt in
Debug.dprintf debug_refl "computing args@.";
......
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