Commit 2e20446f authored by MARCHE Claude's avatar MARCHE Claude

Defunctionalization: problem with Ocaml extraction of lambda's

parent 18f79f2f
...@@ -192,12 +192,16 @@ pvsbin/ ...@@ -192,12 +192,16 @@ pvsbin/
/examples/why3bench.html /examples/why3bench.html
/examples/why3regtests.err /examples/why3regtests.err
/examples/why3regtests.out /examples/why3regtests.out
/examples/*/*.ml
/examples/*/*.opt /examples/*/*.opt
/examples/*/*.byte /examples/*/*.byte
/examples/in_progress/*/*.opt
/examples/in_progress/*/*.byte
/examples/*/*.html /examples/*/*.html
/examples/*/*/*.html /examples/*/*/*.html
/examples/*/*/*/*.html /examples/*/*/*/*.html
/examples/*/style.css
/examples/*/*/style.css
/examples/*/*/*/style.css
/examples/*/*.tex /examples/*/*.tex
/examples/*/*/*.tex /examples/*/*/*.tex
/examples/*/*/*/*.tex /examples/*/*/*/*.tex
......
...@@ -109,6 +109,36 @@ ...@@ -109,6 +109,36 @@
** support de Yices 2 ? interesserait Cesar ** support de Yices 2 ? interesserait Cesar
==================== Roadmap for release 0.91 ========================
HighOrd: Coq output and OCaml extraction should produce lambda's from lambda's
and no epsilon
* terminaison
** generer une obligation de preuve de well-foundedness quand on utilise
un variant avec "with R" (une seule fois pour chaque R !)
** quand une definition logique recursive ne peut pas etre verifiee
bien-fondee statiquement, generer une obligation de preuve
(feature wish de F Besson)
* Coq tactic
** ajout de bases de hint
* replayer
** deplacer option -bench dans une commande de why3session
* IDE
** todo: run detection immediately at start up if conf file absent or
outdated. should become doable with the new Session module
** "detect provers" menu
* Contre-exemples de Alt-Ergo
* detect editors
*** check if coqide and also emacs/proof-general is installed
==================== Roadmap for release 0.90 ======================== ==================== Roadmap for release 0.90 ========================
== New Features to announce == == New Features to announce ==
...@@ -220,33 +250,10 @@ ...@@ -220,33 +250,10 @@
vers ite qui est supporté par pas mal de prouveurs vers ite qui est supporté par pas mal de prouveurs
** introduire des symboles _match non polymorphes differents pour ** introduire des symboles _match non polymorphes differents pour
chaque instance necessaires. plutot qu'un seul symbole _match chaque instance necessaires. plutot qu'un seul symbole _match
poymorphe. polymorphe.
* extraction vers Caml * extraction vers Caml
** utiliser ZArith ** DONE utiliser ZArith
* replayer
** deplacer option -bench dans une commande de why3session
* terminaison
** generer une obligation de preuve de well-foundedness quand on utilise
un variant avec "with R" (une seule fois pour chaque R !)
** quand une definition logique recursive ne peut pas etre verifiee
bien-fondee statiquement, generer une obligation de preuve
(feature wish de F Besson)
* Coq tactic
** ajout de bases de hint
* IDE
** todo: run detection immediately at start up if conf file absent or
outdated. should become doable with the new Session module
** "detect provers" menu
* Contre-exemples de Alt-Ergo
* detect editors
*** check if coqide and also emacs/proof-general is installed
* bug #15629 * bug #15629
......
...@@ -190,45 +190,43 @@ module Defunctionalization ...@@ -190,45 +190,43 @@ module Defunctionalization
use import Expr use import Expr
use import DirectSem use import DirectSem
(* (**
Exercise 2: Exercise 2:
De-functionalize the continuation of eval_1. De-functionalize the continuation of [eval_1].
cont ::= ... cont ::= ...
continue_2 : cont -> value -> value [continue_2 : cont -> value -> value]
eval_2 : expression -> cont -> value [eval_2 : expression -> cont -> value]
interpret_2 : program -> value [interpret_2 : program -> value]
Le type de donnees ("data type") cont represente The data type cont represents the grammar of contexts.
la grammaire des contextes.
Les deux fonctions mutuellement recursives eval_2 The two mutually recursive functions [eval_2] and [continue_2]
et continue_2 implementent une machine abstraite, implement an abstract machine, that is a state transition system.
c'est à dire un système de transition d'etats.
*) *)
type cont = A1 expr cont | A2 int cont | I type cont = A1 expr cont | A2 int cont | I
(* (**
On voudrait ecrire One would want to write in Why:
function eval_cont (c:cont) (v:int) : int = [function eval_cont (c:cont) (v:int) : int =
match c with match c with
| A1 e2 k -> | A1 e2 k ->
let v2 = eval_0 e2 in let v2 = eval_0 e2 in
eval_cont (A2 v k) v2 eval_cont (A2 v k) v2
| A2 v1 k -> eval_cont k (v1 - v) | A2 v1 k -> eval_cont k (v1 - v)
| I -> v | I -> v
end end]
Mais la recursion n'etant pas structurelle, le noyau de Why3 la refuse But since the recursion is not structural, Why3 kernel rejects it
(les definitions dans la logique doivent etre totales) (definitions in the logic part of the language must be total)
On remplace par une definition relationnelle, inductive. We replace that with a relational definition, an inductive one.
*) *)
...@@ -242,7 +240,7 @@ inductive eval_cont cont int int = ...@@ -242,7 +240,7 @@ inductive eval_cont cont int int =
| a3 : | a3 :
forall v:int. eval_cont I v v forall v:int. eval_cont I v v
(* fonctions servant de mesure pour la preuve de terminaison *) (** Some functions to serve as measures for the termination proof *)
function size_e (e:expr) : int = function size_e (e:expr) : int =
match e with match e with
...@@ -274,8 +272,8 @@ let rec lemma size_c_pos (c:cont) : unit ...@@ -274,8 +272,8 @@ let rec lemma size_c_pos (c:cont) : unit
| A2 _ k -> size_c_pos k | A2 _ k -> size_c_pos k
end end
(* programs WhyML (declarés avec "let" au lieu de "function"), (** WhyML programs (declared with "let" instead of "function"),
mutuellement recursifs resultant de la defonctionalisation *) mutually recursive, resulting from de-functionalization *)
let rec continue_2 (c:cont) (v:int) : int let rec continue_2 (c:cont) (v:int) : int
variant { size_c c } variant { size_c c }
...@@ -296,8 +294,8 @@ with eval_2 (e:expr) (c:cont) : int ...@@ -296,8 +294,8 @@ with eval_2 (e:expr) (c:cont) : int
| Sub e1 e2 -> eval_2 e1 (A1 e2 c) | Sub e1 e2 -> eval_2 e1 (A1 e2 c)
end end
(* L'interprete. La post-condition specifie que ce program calcule (** The interpreter. The post-condition specifies that this program
la meme chose que eval_0 *) computes the same thing as [eval_0] *)
let interpret_2 (p:prog) : int let interpret_2 (p:prog) : int
ensures { result = eval_0 p } ensures { result = eval_0 p }
...@@ -312,6 +310,8 @@ let u4 () = interpret_2 p4 ...@@ -312,6 +310,8 @@ let u4 () = interpret_2 p4
end end
module SemErreur module SemErreur
use import Expr use import Expr
......
...@@ -11,8 +11,7 @@ CMX = $(addsuffix .cmx, $(OBJ)) ...@@ -11,8 +11,7 @@ CMX = $(addsuffix .cmx, $(OBJ))
ZARITH = $(shell ocamlfind query -i-format zarith) ZARITH = $(shell ocamlfind query -i-format zarith)
# NUMLIB = zarith NUMLIB = zarith
NUMLIB = nums
WHY3 = $(shell ocamlfind query -i-format why3) WHY3 = $(shell ocamlfind query -i-format why3)
OCAMLOPT = ocamlopt -noassert -inline 1000 OCAMLOPT = ocamlopt -noassert -inline 1000
...@@ -22,6 +21,7 @@ all: $(MAIN).opt ...@@ -22,6 +21,7 @@ all: $(MAIN).opt
doc: doc:
why3doc ../defunctionalization.mlw why3doc ../defunctionalization.mlw
why3session html ../defunctionalization.mlw why3session html ../defunctionalization.mlw
firefox defunctionalization.mlw.html defunctionalization.html
$(MAIN).byte: $(CMO) $(MAIN).cmo $(MAIN).byte: $(CMO) $(MAIN).cmo
ocamlc -g $(ZARITH) $(WHY3) $(NUMLIB).cma why3extract.cma -o $@ $^ ocamlc -g $(ZARITH) $(WHY3) $(NUMLIB).cma why3extract.cma -o $@ $^
......
...@@ -17,7 +17,7 @@ let rec p_expr fmt e = ...@@ -17,7 +17,7 @@ let rec p_expr fmt e =
match e with match e with
| Cte n -> fprintf fmt "%s" (Why3__BigInt.to_string n) | Cte n -> fprintf fmt "%s" (Why3__BigInt.to_string n)
| Sub(e1,e2) -> | Sub(e1,e2) ->
fprintf fmt "%a - %a" p_expr e1 p_expr e2 fprintf fmt "(%a - %a)" p_expr e1 p_expr e2
let p_prog fmt p = p_expr fmt p let p_prog fmt p = p_expr fmt p
...@@ -26,7 +26,7 @@ let p_value fmt v = ...@@ -26,7 +26,7 @@ let p_value fmt v =
let run s f p = let run s f p =
let v = f p in let v = f p in
printf "%s (%a): %a@." s p_prog p p_value v printf "%s %a : %a@." s p_prog p p_value v
let () = let () =
printf "Exercise 0: direct semantics@."; printf "Exercise 0: direct semantics@.";
......
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