Commit 55e0e0f9 authored by MARCHE Claude's avatar MARCHE Claude

Defunctionalization: refocus proved

parent beb4b0b8
......@@ -312,46 +312,21 @@ end
module SemErreur
(** {2 Semantics with errors} *)
module SemWithError
use import Expr
(*
2. Les expressions arithmetiques, avec des erreurs
-----------------------------------------------
Expressions:
n : nat
e : terme
e ::= n | e - e
Errors:
p : program
p ::= e
s : error
Exemples:
p0 = 0
p1 = 10 - 6
p2 = (10 - 6) - (7 - 2)
p3 = (7 - 2) - (10 - 6)
p4 = 10 - (2 - 3)
Values:
v : value
v ::= n
Erreurs:
s : erreur
Values expressibles:
Expressible values:
ve : expressible_value
ve ::= v | s
......@@ -382,22 +357,21 @@ e1 => n1 e2 => n2 n1 >= n2 n1 - n2 = n3
---------------------------------------------
e1 - e2 => n3
On interprète le program e en la value n si le jugement
We interpret the program e into value n if the judgement
e => n
est satisfait, et en l'erreur s si le jugement
holds, and into error s if the judgement
e => s
est satisfait.
holds.
Exercise 0:
Programr l'interprete ci-dessus
et le tester sur les exemples.
Program the interpretor above and test it on the examples.
eval_0 : terme -> expressible_value
eval_0 : expr -> expressible_value
interpret_0 : program -> expressible_value
*)
......@@ -428,13 +402,12 @@ let t4 () = interpret_0 p4
(*
Exercise 1:
CPS-transformer (en appel par value, de gauche a droite)
la fonction eval_0,
et l'appeler dans la fonction principale de l'interprete
avec comme continuation initiale la fonction identite.
CPS-transform (call by value, from left to right)
the function [eval_0], call it from the main interpreter
with the identity function as initial continuation.
eval_1 : terme -> (expressible_value -> 'a) -> 'a
interprète_1 : program -> expressible_value
eval_1 : expr -> (expressible_value -> 'a) -> 'a
interpret_1 : program -> expressible_value
*)
......@@ -475,14 +448,19 @@ lemma cps_correct: forall p. interpret_1 p = interpret_0 p
(*
Exercise 2:
Diviser la continuation
Divide the continuation
expressible_value -> 'a
en deux:
(value -> 'a) * (erreur -> 'a)
et adapter eval_1 et interprète_1.
eval_2 : terme -> (value -> 'a) -> (erreur -> 'a) -> 'a
interprète_2 : program -> expressible_value
in two:
(value -> 'a) * (error -> 'a)
and adapt [eval_1] and [interpret_1] as
eval_2 : expr -> (value -> 'a) -> (error -> 'a) -> 'a
interpret_2 : program -> expressible_value
*)
......@@ -515,7 +493,8 @@ with eval_2b (v1:int) (k:int -> 'a) (kerr : unit -> 'a) : int -> 'a =
function interpret_2 (p : prog) : value = eval_2 p (\ n. Vnum n) (\ u. Underflow)
function interpret_2 (p : prog) : value =
eval_2 p (\ n. Vnum n) (\ u. Underflow)
let rec lemma cps2_correct_expr (e:expr) (kerr:unit -> 'a): unit
variant { e }
......@@ -534,17 +513,15 @@ lemma cps2_correct: forall p. interpret_2 p = interpret_0 p
(*
Exercise 3:
Specialiser le co-domaine des continuations et de la fonction
d'evaluation pour qu'il ne soit plus polymorphique
mais qu'il soit expressible_value, et
court-circuiter la seconde continuation pour ne pas continuer
en cas d'erreur.
Specialize the codomain of the continuations and of the evaluation function
so that it is not polymorphic anymore but is [expressible_value], and
then short-circuit the second continuation to stop in case of error
eval_3 : terme -> (value -> expressible_value) -> expressible_value
interprète_3 : program -> expressible_value
eval_3 : expr -> (value -> expressible_value) -> expressible_value
interpret_3 : program -> expressible_value
(NB. Maintenant il n'y a plus qu'une continuation et elle n'est
appliquee que s'il n'y a pas eu d'erreur.)
NB: Now there is only one continuation and it is applied only in
absence of error.
*)
......@@ -582,54 +559,58 @@ lemma cps3_correct: forall p. interpret_3 p = interpret_0 p
(*
Exercise 4:
Defonctionaliser la continuation de eval_3.
De-functionalize the continuation of [eval_3].
cont ::= ...
continue_4 : cont -> value -> expressible_value
eval_4 : terme -> cont -> expressible_value
interprète_4 : program -> expressible_value
eval_4 : expr -> cont -> expressible_value
interprete_4 : program -> expressible_value
Le type de donnees ("data type") cont represente
la grammaire des contextes. (NB. A-t-il change
par rapport à l'exercice precedent?)
The data type [cont] represents the grammar of contexts.
(NB. has it changed w.r.t to previous exercise?)
Les deux fonctions mutuellement recursives eval_4
et continue_4 implementent une machine abstraite,
c'est à dire un système de transition d'etats,
qui s'arrête soit tout de suite en cas d'erreur,
soit à la fin du calcul.
The two mutually recursive functions [eval_4] and [continue_4]
implement an abstract machine, that is a transition system that
stops immediately in case of error, or and the end of computation.
----------
*)
Le lambda-calcul
----------------
Termes:
(* TODO *)
end
(** {2 The lambda-calculus} *)
(*
Terms:
n : int
x : identificateur
x : identifier
t : terme
t : term
t ::= x | \x.t | t t
p : program
p ::= t
où t est ferme (i.e., sans variables libres)
where t is ground (i.e. without any free variable)
Exemples:
Examples:
p0 = (\x.x)
p1 = (\x.x) (\x.x)
p2 = (\x.\f.f x) (\y.y) (\x.x)
Values et environnements:
Values and environments:
e : environnement
v ::= nil | (identificateur, value) :: environnement
e : environment
v ::= nil | (identifier, value) :: environment
v : value
v ::= (\x.t, e)
......@@ -684,7 +665,8 @@ Exercise 3:
*)
end
......@@ -814,6 +796,19 @@ let rec lemma recompose_values (c:context) (e1 e2:expr) : unit
| Right n c -> recompose_values c (Sub (Cte n) e1) (Sub (Cte n) e2)
end
let rec lemma recompose_inversion (c:context) (e:expr)
requires {
match c with Empty -> false | _ -> true end \/
match e with Cte _ -> false | Sub _ _ -> true end }
variant { c }
ensures { match recompose c e with
Cte _ -> false | Sub _ _ -> true end }
= match c with
| Empty -> ()
| Left c e2 -> recompose_inversion c (Sub e e2)
| Right n1 c -> recompose_inversion c (Sub (Cte n1) e)
end
(*
Decomposition:
......@@ -946,7 +941,10 @@ Exercise 2:
let refocus c e
diverges
raises { NoRedex -> is_a_value e }
ensures { let (c1,e1) = result in
recompose c1 e1 = recompose c e /\
is_a_redex e1 }
raises { NoRedex -> is_a_value (recompose c e) }
= decompose_term e c
let rec itere_opt (c:context) (e:expr) : int
......@@ -975,11 +973,9 @@ let rec normalize (e:expr)
Exercise 3:
Obtenir une machine abstraite.
----------
% fin de danvy-ex2.txt
*)
(* TODO *)
end
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