Merge branch 'master' of gaufre.informatique.univ-paris-diderot.fr:aguatto/compilation-m1-2023
This commit is contained in:
commit
fc0a2113d4
14 changed files with 757 additions and 0 deletions
8
cours/cours-04/.ocamlinit
Normal file
8
cours/cours-04/.ocamlinit
Normal file
|
@ -0,0 +1,8 @@
|
||||||
|
open Cours04;;
|
||||||
|
|
||||||
|
#install_printer Lang0.pp;;
|
||||||
|
#install_printer Lang1.pp;;
|
||||||
|
#install_printer Lang2.pp;;
|
||||||
|
#install_printer Lang2.pp_value;;
|
||||||
|
|
||||||
|
module R = Rewrite.Make(Lang1);;
|
46
cours/cours-04/Id.ml
Normal file
46
cours/cours-04/Id.ml
Normal file
|
@ -0,0 +1,46 @@
|
||||||
|
module S = struct
|
||||||
|
type t = string
|
||||||
|
|
||||||
|
let compare (x : t) y = Stdlib.compare x y
|
||||||
|
|
||||||
|
let pp = Fmt.string
|
||||||
|
end
|
||||||
|
|
||||||
|
include S
|
||||||
|
|
||||||
|
let fresh, reset =
|
||||||
|
let r = ref 0 in
|
||||||
|
(fun () -> incr r; Printf.sprintf "_x%d" !r),
|
||||||
|
(fun () -> r := 0)
|
||||||
|
|
||||||
|
type 'a subst = (t * 'a) list
|
||||||
|
|
||||||
|
let pp_subst pp_val =
|
||||||
|
let pp_kv ff (x, v) = Format.fprintf ff "%a\\%a" pp x pp_val v in
|
||||||
|
Fmt.(box (list ~sep:comma pp_kv))
|
||||||
|
|
||||||
|
let empty = []
|
||||||
|
|
||||||
|
let extend x v xs = (x, v) :: xs
|
||||||
|
|
||||||
|
let assoc = List.assoc
|
||||||
|
|
||||||
|
let singleton x v = [(x, v)]
|
||||||
|
|
||||||
|
let trim xs =
|
||||||
|
List.fold_right
|
||||||
|
(fun (x, v) xs -> (x, v) :: List.remove_assoc x xs)
|
||||||
|
xs
|
||||||
|
[]
|
||||||
|
|
||||||
|
let domain xs = trim xs |> List.map fst
|
||||||
|
|
||||||
|
type 'a rel = 'a -> 'a -> bool
|
||||||
|
|
||||||
|
let included r xs ys =
|
||||||
|
try List.for_all (fun (x, v) -> r v (List.assoc x ys)) (trim xs)
|
||||||
|
with Not_found -> false
|
||||||
|
|
||||||
|
let equal_subst eq xs ys = included eq xs ys && included eq ys xs
|
||||||
|
|
||||||
|
module Set = Set.Make(S)
|
31
cours/cours-04/Id.mli
Normal file
31
cours/cours-04/Id.mli
Normal file
|
@ -0,0 +1,31 @@
|
||||||
|
type t = string
|
||||||
|
|
||||||
|
val compare : t -> t -> int
|
||||||
|
|
||||||
|
val pp : t Fmt.t
|
||||||
|
|
||||||
|
val fresh : unit -> t
|
||||||
|
|
||||||
|
type 'a subst = (t * 'a) list
|
||||||
|
|
||||||
|
val pp_subst : 'a Fmt.t -> 'a subst Fmt.t
|
||||||
|
|
||||||
|
val empty : 'a subst
|
||||||
|
|
||||||
|
val extend : t -> 'a -> 'a subst -> 'a subst
|
||||||
|
|
||||||
|
val assoc : t -> 'a subst -> 'a
|
||||||
|
|
||||||
|
val singleton : t -> 'a -> 'a subst
|
||||||
|
|
||||||
|
val domain : 'a subst -> t list
|
||||||
|
|
||||||
|
type 'a rel = 'a -> 'a -> bool
|
||||||
|
|
||||||
|
val included : 'a rel -> 'a subst rel
|
||||||
|
|
||||||
|
val equal_subst : 'a rel -> 'a subst rel
|
||||||
|
|
||||||
|
val reset : unit -> unit
|
||||||
|
|
||||||
|
module Set : Set.S with type elt = t
|
162
cours/cours-04/Lang0.ml
Normal file
162
cours/cours-04/Lang0.ml
Normal file
|
@ -0,0 +1,162 @@
|
||||||
|
type t =
|
||||||
|
| Var of Id.t
|
||||||
|
| Lit of int
|
||||||
|
| Add of t * t
|
||||||
|
| Let of t * bound1
|
||||||
|
|
||||||
|
and bound1 = { bound : Id.t; body : t; }
|
||||||
|
|
||||||
|
let rec pp ff = function
|
||||||
|
| Var x ->
|
||||||
|
Id.pp ff x
|
||||||
|
| Lit n ->
|
||||||
|
Format.fprintf ff "%d" n
|
||||||
|
| Add (e1, e2) ->
|
||||||
|
Format.fprintf ff "@[@[%a@]@ + @[%a@]@]"
|
||||||
|
pp e1
|
||||||
|
pp e2
|
||||||
|
| Let (e1, e2) ->
|
||||||
|
Format.fprintf ff "let(@[@[%a@],@ @[%a@]@])"
|
||||||
|
pp e1
|
||||||
|
pp_bound1 e2
|
||||||
|
|
||||||
|
and pp_bound1 ff { bound; body; } =
|
||||||
|
Format.fprintf ff "@[%a.@,@[%a@]@]"
|
||||||
|
Id.pp bound
|
||||||
|
pp body
|
||||||
|
|
||||||
|
let pp_substitution ff xs =
|
||||||
|
Fmt.list ~sep:Fmt.comma
|
||||||
|
(fun ff (x, e) ->
|
||||||
|
Format.fprintf ff "%a\\@[%a@]" Id.pp x pp e)
|
||||||
|
ff xs
|
||||||
|
|
||||||
|
module Build = struct
|
||||||
|
let v x = Var x
|
||||||
|
let l i = Lit i
|
||||||
|
let ( + ) e1 e2 = Add (e1, e2)
|
||||||
|
let ( let* ) e1 mk_e2 =
|
||||||
|
let bound = Id.fresh () in
|
||||||
|
Let (e1, { bound; body = mk_e2 (Var bound); })
|
||||||
|
end
|
||||||
|
|
||||||
|
let rec subst s = function
|
||||||
|
| Var x ->
|
||||||
|
begin try Id.assoc x s with Not_found -> Var x end
|
||||||
|
| Lit k ->
|
||||||
|
Lit k
|
||||||
|
| Add (e1, e2) ->
|
||||||
|
Add (subst s e1, subst s e2)
|
||||||
|
| Let (e1, e2) ->
|
||||||
|
Let (subst s e1, subst_bound1 s e2)
|
||||||
|
|
||||||
|
and subst_bound1 s { bound = x; body; } =
|
||||||
|
let x' = Id.fresh () in
|
||||||
|
{ bound = x'; body = subst (Id.extend x (Var x') s) body; }
|
||||||
|
|
||||||
|
let%expect_test "subst" =
|
||||||
|
Id.reset ();
|
||||||
|
let print_subst e x e' =
|
||||||
|
Format.printf "@[(@[%a@])[%a\\@[%a@]]@ = @[%a@]@]@."
|
||||||
|
pp e
|
||||||
|
Id.pp x
|
||||||
|
pp e'
|
||||||
|
pp (subst [(x, e')] e)
|
||||||
|
in
|
||||||
|
let open Build in
|
||||||
|
print_subst (l 1 + v "x") "x" (v "y");
|
||||||
|
[%expect {| (1 + x)[x\y] = 1 + y |}];
|
||||||
|
print_subst (Let (l 2, { bound = "y"; body = l 1 + v "x" + v "y"; }))
|
||||||
|
"x" (v "y");
|
||||||
|
[%expect {| (let(2, y.1 + x + y))[x\y] = let(2, _x1.1 + y + _x1) |}];
|
||||||
|
();;
|
||||||
|
|
||||||
|
let rec equal e e' =
|
||||||
|
match e, e' with
|
||||||
|
| Var x, Var x' ->
|
||||||
|
x = x'
|
||||||
|
| Lit i, Lit i' ->
|
||||||
|
i = i'
|
||||||
|
| Add (e1, e2), Add (e1', e2') ->
|
||||||
|
equal e1 e1' && equal e2 e2'
|
||||||
|
| Let (e1, e2), Let (e1', e2') ->
|
||||||
|
equal e1 e1' && equal_bound1 e2 e2'
|
||||||
|
| _ ->
|
||||||
|
false
|
||||||
|
|
||||||
|
and equal_bound1 { bound = x; body = e; } { bound = x'; body = e'; } =
|
||||||
|
let y = Id.fresh () in
|
||||||
|
equal
|
||||||
|
(subst Id.(singleton x (Var y)) e)
|
||||||
|
(subst Id.(singleton x' (Var y)) e')
|
||||||
|
|
||||||
|
and equal_subst sub1 sub2 = Id.equal_subst equal sub1 sub2
|
||||||
|
|
||||||
|
let%expect_test "equal" =
|
||||||
|
Id.reset ();
|
||||||
|
let print_equal e1 e2 =
|
||||||
|
Format.printf "@[@[%a@]@ = @[%a@]: %b@]@."
|
||||||
|
pp e1
|
||||||
|
pp e2
|
||||||
|
(equal e1 e2)
|
||||||
|
in
|
||||||
|
let open Build in
|
||||||
|
print_equal (let* x = l 1 in x) (let* y = l 1 in y);
|
||||||
|
[%expect {| let(1, _x2._x2) = let(1, _x1._x1): true |}];
|
||||||
|
print_equal (let* x = l 1 in x) (let* y = l 2 in y);
|
||||||
|
[%expect {| let(1, _x5._x5) = let(2, _x4._x4): false |}];
|
||||||
|
print_equal
|
||||||
|
(let* x = l 1 in let* k = l 2 in x + k)
|
||||||
|
(let* y = l 1 in let* k = l 2 in y + k);
|
||||||
|
[%expect {|
|
||||||
|
let(1, _x8.let(2, _x9._x8 + _x9)) = let(1, _x6.let(2, _x7._x6 + _x7)): true |}];
|
||||||
|
print_equal
|
||||||
|
(let* x = l 1 in let* k = l 2 in x + k)
|
||||||
|
(let* y = l 1 in let* k = l 2 in k + y);
|
||||||
|
[%expect {|
|
||||||
|
let(1, _x16.let(2, _x17._x16 + _x17))
|
||||||
|
= let(1, _x14.let(2, _x15._x15 + _x14)): false |}];;
|
||||||
|
|
||||||
|
let rec free_vars : t -> Id.Set.t = function
|
||||||
|
| Var x -> Id.Set.singleton x
|
||||||
|
| Lit _ -> Id.Set.empty
|
||||||
|
| Add (e1, e2) -> Id.Set.union (free_vars e1) (free_vars e2)
|
||||||
|
| Let (e1, e2) -> Id.Set.union (free_vars e1) (free_vars_bound1 e2)
|
||||||
|
|
||||||
|
and free_vars_bound1 { bound; body; } =
|
||||||
|
Id.Set.remove bound (free_vars body)
|
||||||
|
|
||||||
|
let%expect_test "free_vars" =
|
||||||
|
Id.reset ();
|
||||||
|
let print_free_vars e =
|
||||||
|
Format.printf "@[free_vars (@[%a@])@ = {@[%a@]}@]@."
|
||||||
|
pp e
|
||||||
|
Fmt.(list ~sep:comma Id.pp) (free_vars e |> Id.Set.to_seq |> List.of_seq)
|
||||||
|
in
|
||||||
|
let open Build in
|
||||||
|
print_free_vars (l 1 + l 2);
|
||||||
|
[%expect {| free_vars (1 + 2) = {} |}];
|
||||||
|
print_free_vars (let* x = l 12 in l 1 + x + v "y");
|
||||||
|
[%expect {| free_vars (let(12, _x1.1 + _x1 + y)) = {y} |}];
|
||||||
|
print_free_vars (let* x = l 12 in let* y = v "z" in l 1 + x + y);
|
||||||
|
[%expect {| free_vars (let(12, _x2.let(z, _x3.1 + _x2 + _x3))) = {z} |}];
|
||||||
|
()
|
||||||
|
|
||||||
|
let close_with { bound; body; } e = subst Id.(singleton bound e) body
|
||||||
|
|
||||||
|
let rec eval : t -> int =
|
||||||
|
function
|
||||||
|
| Var _ -> failwith "open term"
|
||||||
|
| Lit k -> k
|
||||||
|
| Add (e1, e2) -> eval e1 + eval e2
|
||||||
|
| Let (e, b) -> eval (close_with b e)
|
||||||
|
|
||||||
|
(* Tests fixtures *)
|
||||||
|
|
||||||
|
let e1, e2, e3, e4 =
|
||||||
|
Id.reset ();
|
||||||
|
let open Build in
|
||||||
|
(l 1 + l 1),
|
||||||
|
(let* x = l 1 + l 1 in x),
|
||||||
|
(let* x = l 1 + l 1 in l 40 + x),
|
||||||
|
(let* x = l 1 + l 1 in let* y = x + l 1 in let* x = l 3 in x + y)
|
180
cours/cours-04/Lang1.ml
Normal file
180
cours/cours-04/Lang1.ml
Normal file
|
@ -0,0 +1,180 @@
|
||||||
|
type t =
|
||||||
|
| Var of Id.t
|
||||||
|
| Lit of int
|
||||||
|
| Add of t * t
|
||||||
|
| Let of t * bound1
|
||||||
|
| Hole of t Id.subst
|
||||||
|
|
||||||
|
and bound1 = B of Id.t * t
|
||||||
|
|
||||||
|
let rec pp ff = function
|
||||||
|
| Var x ->
|
||||||
|
Id.pp ff x
|
||||||
|
| Lit n ->
|
||||||
|
Format.fprintf ff "%d" n
|
||||||
|
| Add (e1, e2) ->
|
||||||
|
Format.fprintf ff "add(@[@[%a@],@ @[%a@]@])"
|
||||||
|
pp e1
|
||||||
|
pp e2
|
||||||
|
| Let (e1, e2) ->
|
||||||
|
Format.fprintf ff "let(@[@[%a@],@ @[%a@]@])"
|
||||||
|
pp e1
|
||||||
|
pp_bound1 e2
|
||||||
|
| Hole s ->
|
||||||
|
Format.fprintf ff "[]{@[%a@]}"
|
||||||
|
pp_substitution s
|
||||||
|
|
||||||
|
and pp_bound1 ff (B (x, e)) =
|
||||||
|
Format.fprintf ff "@[%a.@,@[%a@]@]"
|
||||||
|
Id.pp x
|
||||||
|
pp e
|
||||||
|
|
||||||
|
and pp_substitution ff xs =
|
||||||
|
Fmt.list ~sep:Fmt.comma
|
||||||
|
(fun ff (x, e) ->
|
||||||
|
Format.fprintf ff "%a\\@[%a@]" Id.pp x pp e)
|
||||||
|
ff xs
|
||||||
|
|
||||||
|
module Builder = struct
|
||||||
|
let v x = Var x
|
||||||
|
let l i = Lit i
|
||||||
|
let ( + ) e1 e2 = Add (e1, e2)
|
||||||
|
let ( let* ) e1 mk_e2 = let x = Id.fresh () in Let (e1, B (x, mk_e2 (Var x)))
|
||||||
|
let h = Hole []
|
||||||
|
end
|
||||||
|
|
||||||
|
let rec subst s = function
|
||||||
|
| Var x ->
|
||||||
|
begin try Id.assoc x s with Not_found -> Var x end
|
||||||
|
| Lit k ->
|
||||||
|
Lit k
|
||||||
|
| Add (e1, e2) ->
|
||||||
|
Add (subst s e1, subst s e2)
|
||||||
|
| Let (e1, e2) ->
|
||||||
|
Let (subst s e1, subst_bound1 s e2)
|
||||||
|
| Hole s' ->
|
||||||
|
Hole (compose s' s)
|
||||||
|
|
||||||
|
and subst_bound1 s (B (x, e)) =
|
||||||
|
let x' = Id.fresh () in
|
||||||
|
B (x', subst (Id.extend x (Var x') s) e)
|
||||||
|
|
||||||
|
and compose s1 s2 =
|
||||||
|
match s1 with
|
||||||
|
| [] -> s2
|
||||||
|
| (x, t) :: s1 -> (x, subst s2 t) :: compose s1 s2
|
||||||
|
|
||||||
|
let rec equal e e' =
|
||||||
|
match e, e' with
|
||||||
|
| Var x, Var x' ->
|
||||||
|
x = x'
|
||||||
|
| Lit i, Lit i' ->
|
||||||
|
i = i'
|
||||||
|
| Add (e1, e2), Add (e1', e2') ->
|
||||||
|
equal e1 e1' && equal e2 e2'
|
||||||
|
| Let (e1, e2), Let (e1', e2') ->
|
||||||
|
equal e1 e1' && equal_bound1 e2 e2'
|
||||||
|
| Hole sub1, Hole sub2 ->
|
||||||
|
equal_subst sub1 sub2
|
||||||
|
| _ ->
|
||||||
|
false
|
||||||
|
|
||||||
|
and equal_bound1 (B (x, e)) (B (x', e')) =
|
||||||
|
let y = Id.fresh () in
|
||||||
|
equal
|
||||||
|
(subst Id.(singleton x (Var y)) e)
|
||||||
|
(subst Id.(singleton x' (Var y)) e')
|
||||||
|
|
||||||
|
and equal_subst sub1 sub2 = Id.equal_subst equal sub1 sub2
|
||||||
|
|
||||||
|
let%expect_test "e1" =
|
||||||
|
Id.reset ();
|
||||||
|
let print e1 e2 =
|
||||||
|
Format.printf "@[@[%a@]@ = @[%a@]: %b@]@."
|
||||||
|
pp e1
|
||||||
|
pp e2
|
||||||
|
(equal e1 e2)
|
||||||
|
in
|
||||||
|
let open Builder in
|
||||||
|
print (let* x = l 1 in x) (let* y = l 1 in y);
|
||||||
|
[%expect {| let(1, _x2._x2) = let(1, _x1._x1): true |}];
|
||||||
|
print (let* x = l 1 in x) (let* y = l 2 in y);
|
||||||
|
[%expect {| let(1, _x5._x5) = let(2, _x4._x4): false |}];
|
||||||
|
print
|
||||||
|
(let* x = l 1 in let* k = l 2 in x + k)
|
||||||
|
(let* y = l 1 in let* k = l 2 in y + k);
|
||||||
|
[%expect {|
|
||||||
|
let(1, _x8.let(2, _x9.add(_x8, _x9)))
|
||||||
|
= let(1, _x6.let(2, _x7.add(_x6, _x7))): true |}];
|
||||||
|
print
|
||||||
|
(let* x = l 1 in let* k = l 2 in x + k)
|
||||||
|
(let* y = l 1 in let* k = l 2 in k + y);
|
||||||
|
[%expect {|
|
||||||
|
let(1, _x16.let(2, _x17.add(_x16, _x17)))
|
||||||
|
= let(1, _x14.let(2, _x15.add(_x15, _x14))): false |}];;
|
||||||
|
|
||||||
|
let close_with (B (x, e)) e' = subst Id.(singleton x e') e
|
||||||
|
|
||||||
|
let rec plug k e =
|
||||||
|
match k with
|
||||||
|
| (Var _ | Lit _) as k -> k
|
||||||
|
| Add (k1, k2) -> Add (plug k1 e, plug k2 e)
|
||||||
|
| Let (k1, k2) -> Let (plug k1 e, plug_bound1 k2 e)
|
||||||
|
| Hole s -> subst s e
|
||||||
|
|
||||||
|
and plug_bound1 (B (x, k)) e = B (x, plug k e)
|
||||||
|
|
||||||
|
let beta0 : t -> t option
|
||||||
|
= function
|
||||||
|
| Add (Lit k1, Lit k2) ->
|
||||||
|
Some (Lit (k1 + k2))
|
||||||
|
| Let (e1, e2) ->
|
||||||
|
Some (close_with e2 e1)
|
||||||
|
| _ ->
|
||||||
|
None
|
||||||
|
|
||||||
|
let wrap f (k, e) = (f k, e)
|
||||||
|
|
||||||
|
let rec decompose t =
|
||||||
|
Seq.cons (Hole [], t) (decompose_subterms t)
|
||||||
|
|
||||||
|
and decompose_subterms = function
|
||||||
|
| Var _ | Lit _ | Hole _ ->
|
||||||
|
Seq.empty
|
||||||
|
| Add (e1, e2) ->
|
||||||
|
Seq.interleave
|
||||||
|
(decompose e1 |> Seq.map (wrap (fun k -> Add (k, e2))))
|
||||||
|
(decompose e2 |> Seq.map (wrap (fun k -> Add (e1, k))))
|
||||||
|
| Let (e1, B (x, e2)) ->
|
||||||
|
Seq.interleave
|
||||||
|
(decompose e1 |> Seq.map (wrap (fun k -> Let (k, B (x, e2)))))
|
||||||
|
(decompose e2 |> Seq.map (wrap (fun k -> Let (e1, B (x, k)))))
|
||||||
|
|
||||||
|
let rewrite e =
|
||||||
|
decompose e
|
||||||
|
|> Seq.filter_map (fun (k, e) -> beta0 e |> Option.map (fun e -> (k, e)))
|
||||||
|
|> Seq.map (fun (k, e) -> plug k e)
|
||||||
|
|
||||||
|
(* Test fixtures *)
|
||||||
|
|
||||||
|
let e1, e2, e3, e4 =
|
||||||
|
Id.reset ();
|
||||||
|
let open Builder in
|
||||||
|
(l 1 + l 1),
|
||||||
|
(let* x = l 1 + l 1 in x),
|
||||||
|
(let* x = l 1 + l 1 in l 40 + x),
|
||||||
|
(let* x = l 1 + l 1 in let* y = x + l 1 in let* x = l 3 in x + y)
|
||||||
|
|
||||||
|
let%expect_test "rew0" =
|
||||||
|
Id.reset ();
|
||||||
|
let e = Builder.(let* x = l 1 + l 1 in l 28 + l 12 + x) in
|
||||||
|
Format.printf "%a@." pp e;
|
||||||
|
[%expect {| let(add(1, 1), _x1.add(add(28, 12), _x1)) |}];
|
||||||
|
Format.printf "@[@[%a@]@ -> @[<hv 2>%a@]@]@."
|
||||||
|
pp e
|
||||||
|
Fmt.(list ~sep:comma pp) (rewrite e |> List.of_seq);
|
||||||
|
[%expect {|
|
||||||
|
let(add(1, 1), _x1.add(add(28, 12), _x1))
|
||||||
|
-> add(add(28, 12), add(1, 1)),
|
||||||
|
let(2, _x1.add(add(28, 12), _x1)),
|
||||||
|
let(add(1, 1), _x1.add(40, _x1)) |}]
|
194
cours/cours-04/Lang2.ml
Normal file
194
cours/cours-04/Lang2.ml
Normal file
|
@ -0,0 +1,194 @@
|
||||||
|
(** {2 Abstract Syntax Trees} *)
|
||||||
|
|
||||||
|
type t = Var of Id.t (* occurrence "x", "y", etc. *)
|
||||||
|
| Int of int (* constante litérale "42", etc. *)
|
||||||
|
| Add of t * t (* somme "e1 + e2" *)
|
||||||
|
| Bool of bool (* booléen litéral "true", "false" *)
|
||||||
|
| If of t * t * t (* conditionnelle *)
|
||||||
|
| Let of t * bound1 (* déf. locale "let e1 be x in e2" *)
|
||||||
|
| Fun of bound1 (* fonction anonyme "fun x -> e" *)
|
||||||
|
| App of t * t (* application "e1 e2" *)
|
||||||
|
| Ref of t (* allocation "ref e" *)
|
||||||
|
| Read of t (* déréférencement "!e" *)
|
||||||
|
| Asgn of t * t (* assignation "e1 := e2" *)
|
||||||
|
| Unit (* 0-uplet *)
|
||||||
|
| Seq of t * t (* séquence "e1; e2" *)
|
||||||
|
|
||||||
|
and bound1 = { bound : Id.t; body : t; }
|
||||||
|
|
||||||
|
(** {2 Evaluation} *)
|
||||||
|
|
||||||
|
type env = (Id.t * value) list
|
||||||
|
|
||||||
|
and value =
|
||||||
|
| VInt of int
|
||||||
|
| VBool of bool
|
||||||
|
| VFun of bound1 * env
|
||||||
|
| VRef of value ref
|
||||||
|
| VUnit
|
||||||
|
|
||||||
|
let rec eval env = function
|
||||||
|
| Var x -> List.assoc x env
|
||||||
|
| Int n -> VInt n
|
||||||
|
| Add (e1, e2) -> add_values (eval env e1) (eval env e2)
|
||||||
|
| Bool b -> VBool b
|
||||||
|
| If (e1, e2, e3) -> if_value (eval env e1) env e2 e3
|
||||||
|
| Let (e, b) -> eval_bound1 env b (eval env e)
|
||||||
|
| Fun b -> VFun (b, env)
|
||||||
|
| App (e1, e2) -> app_values (eval env e1) (eval env e2)
|
||||||
|
| Ref e -> VRef (ref (eval env e))
|
||||||
|
| Read e -> read_value (eval env e)
|
||||||
|
| Asgn (e1, e2) -> asgn_values (eval env e1) (eval env e2)
|
||||||
|
| Unit -> VUnit
|
||||||
|
| Seq (e1, e2) -> seq_value (eval env e1) env e2
|
||||||
|
|
||||||
|
and eval_bound1 env { bound; body; } v =
|
||||||
|
eval ((bound, v) :: env) body
|
||||||
|
|
||||||
|
and add_values v1 v2 =
|
||||||
|
match v1, v2 with
|
||||||
|
| VInt n1, VInt n2 -> VInt (n1 + n2)
|
||||||
|
| _ -> failwith "ill-typed"
|
||||||
|
|
||||||
|
and if_value v1 env e2 e3 =
|
||||||
|
match v1 with
|
||||||
|
| VBool true -> eval env e2
|
||||||
|
| VBool false -> eval env e3
|
||||||
|
| _ -> failwith "ill-typed"
|
||||||
|
|
||||||
|
and app_values v1 v2 =
|
||||||
|
match v1 with
|
||||||
|
| VFun (b, env) -> eval_bound1 env b v2
|
||||||
|
| _ -> failwith "ill-typed"
|
||||||
|
|
||||||
|
and read_value v =
|
||||||
|
match v with VRef r -> !r | _ -> failwith "ill-typed"
|
||||||
|
|
||||||
|
and asgn_values v1 v2 =
|
||||||
|
match v1 with VRef r -> r := v2; VUnit | _ -> failwith "ill-typed"
|
||||||
|
|
||||||
|
and seq_value v1 env e2 =
|
||||||
|
match v1 with VUnit -> eval env e2 | _ -> failwith "ill-typed"
|
||||||
|
|
||||||
|
(** {2 Pretty-printing} *)
|
||||||
|
|
||||||
|
let rec pp ff =
|
||||||
|
let pp_maybe_paren ?(space = true) prefix pp ff e =
|
||||||
|
match e with
|
||||||
|
| Var _ | Int _ | Bool _ | Unit ->
|
||||||
|
Format.fprintf ff "@[%s%a@[%a@]@]"
|
||||||
|
prefix
|
||||||
|
Fmt.(if space then sp else nop) ()
|
||||||
|
pp e
|
||||||
|
| _ ->
|
||||||
|
Format.fprintf ff "@[%s(@[%a@])@]"
|
||||||
|
prefix
|
||||||
|
pp e
|
||||||
|
in
|
||||||
|
function
|
||||||
|
| Var x ->
|
||||||
|
Id.pp ff x
|
||||||
|
| Int n ->
|
||||||
|
Format.fprintf ff "%d" n
|
||||||
|
| Add (e1, e2) ->
|
||||||
|
Format.fprintf ff "(@[@[%a@] +@ @[%a@]@])"
|
||||||
|
pp e1
|
||||||
|
pp e2
|
||||||
|
| Bool b ->
|
||||||
|
Format.fprintf ff "%b" b
|
||||||
|
| If (e1, e2, e3) ->
|
||||||
|
Format.fprintf ff "if(@[@[%a@],@ @[%a@],@ @[%a@]@])"
|
||||||
|
pp e1
|
||||||
|
pp e2
|
||||||
|
pp e3
|
||||||
|
| Let (e1, e2) ->
|
||||||
|
Format.fprintf ff "let(@[@[%a@],@ @[%a@]@])"
|
||||||
|
pp e1
|
||||||
|
pp_bound1 e2
|
||||||
|
| Fun b ->
|
||||||
|
Format.fprintf ff "fun(@[%a@])"
|
||||||
|
pp_bound1 b
|
||||||
|
| App (e1, e2) ->
|
||||||
|
Format.fprintf ff "(@[@[%a@]@ @[%a@]@])"
|
||||||
|
pp e1
|
||||||
|
pp e2
|
||||||
|
| Ref e ->
|
||||||
|
pp_maybe_paren "ref" pp ff e
|
||||||
|
| Read e ->
|
||||||
|
pp_maybe_paren ~space:false "!" pp ff e
|
||||||
|
| Asgn (e1, e2) ->
|
||||||
|
Format.fprintf ff "(@[@[%a@]@ := @[%a@]@])"
|
||||||
|
pp e1
|
||||||
|
pp e2
|
||||||
|
| Unit ->
|
||||||
|
Format.fprintf ff "()"
|
||||||
|
| Seq (e1, e2) ->
|
||||||
|
Format.fprintf ff "(@[@[%a@];@ @[%a@]@])"
|
||||||
|
pp e1
|
||||||
|
pp e2
|
||||||
|
|
||||||
|
and pp_bound1 ff { bound; body; } =
|
||||||
|
Format.fprintf ff "@[%a.@,@[%a@]@]"
|
||||||
|
Id.pp bound
|
||||||
|
pp body
|
||||||
|
|
||||||
|
let rec pp_value ff = function
|
||||||
|
| VInt n ->
|
||||||
|
Format.fprintf ff "%d" n
|
||||||
|
| VBool b ->
|
||||||
|
Format.fprintf ff "%b" b
|
||||||
|
| VRef _ ->
|
||||||
|
Format.fprintf ff "ref(..)"
|
||||||
|
| VUnit ->
|
||||||
|
Format.fprintf ff "()"
|
||||||
|
| VFun (b, env) ->
|
||||||
|
Format.fprintf ff "@[<v 2>fun(@[%a@])@,[@[%a@]]@]"
|
||||||
|
pp_bound1 b
|
||||||
|
pp_env env
|
||||||
|
|
||||||
|
and pp_env ff env =
|
||||||
|
let pp_binding ff (x, v) =
|
||||||
|
Format.fprintf ff "@[<hv 2>%a@ = @[%a@]@]"
|
||||||
|
Id.pp x
|
||||||
|
pp_value v
|
||||||
|
in
|
||||||
|
Fmt.(list ~sep:comma pp_binding) ff env
|
||||||
|
|
||||||
|
(** {2 AST Building Helpers} *)
|
||||||
|
|
||||||
|
module Build = struct
|
||||||
|
let fresh_bound1 mk =
|
||||||
|
let x = Id.fresh () in { bound = x; body = mk (Var x); }
|
||||||
|
|
||||||
|
let v x = Var x
|
||||||
|
let i n = Int n
|
||||||
|
let ( + ) e1 e2 = Add (e1, e2)
|
||||||
|
let b b = Bool b
|
||||||
|
let if_ e1 e2 e3 = If (e1, e2, e3)
|
||||||
|
let ( let* ) e1 mk_e2 = Let (e1, fresh_bound1 mk_e2)
|
||||||
|
let fun_ mk_body = Fun (fresh_bound1 mk_body)
|
||||||
|
let app f args = List.fold_left (fun f arg -> App (f, arg)) f args
|
||||||
|
let ref_ e = Ref e
|
||||||
|
let ( ! ) e = Read e
|
||||||
|
let ( := ) e1 e2 = Asgn (e1, e2)
|
||||||
|
let s = function
|
||||||
|
| [] -> Unit
|
||||||
|
| e :: es -> List.fold_left (fun e1 e2 -> Seq (e1, e2)) e es
|
||||||
|
end
|
||||||
|
|
||||||
|
(** {2 Tests} *)
|
||||||
|
|
||||||
|
let print_eval e =
|
||||||
|
let v = eval [] e in
|
||||||
|
Format.printf "@[<hv 2>@[%a@]@ => @[%a@]@]@."
|
||||||
|
pp e
|
||||||
|
pp_value v
|
||||||
|
|
||||||
|
let%expect_test "test" =
|
||||||
|
Id.reset ();
|
||||||
|
let open Build in
|
||||||
|
print_eval (i 1 + i 2);
|
||||||
|
[%expect {| (1 + 2) => 3 |}];
|
||||||
|
print_eval (let* x = ref_ (i 1) in
|
||||||
|
s [x := i 2; !x] + !x);
|
||||||
|
[%expect {| let(ref 1, _x1.(((_x1 := 2); !_x1) + !_x1)) => 3 |}]
|
57
cours/cours-04/Rewrite.ml
Normal file
57
cours/cours-04/Rewrite.ml
Normal file
|
@ -0,0 +1,57 @@
|
||||||
|
module type LANG = sig
|
||||||
|
type t
|
||||||
|
val pp : t Fmt.t
|
||||||
|
val equal : t -> t -> bool
|
||||||
|
val rewrite : t -> t Seq.t
|
||||||
|
end
|
||||||
|
|
||||||
|
module Make(L : LANG) = struct
|
||||||
|
type graph = (L.t * L.t) Seq.t
|
||||||
|
|
||||||
|
let rec reductions t =
|
||||||
|
let open Seq in
|
||||||
|
let* t' = L.rewrite t in
|
||||||
|
cons (t, t') (reductions t')
|
||||||
|
|
||||||
|
let is_normal t =
|
||||||
|
L.rewrite t |> Seq.uncons |> Option.is_none
|
||||||
|
|
||||||
|
let normal_forms t =
|
||||||
|
let open Seq in
|
||||||
|
reductions t |> map snd |> filter is_normal |> Seq.dedup L.equal
|
||||||
|
|
||||||
|
let to_graphviz g =
|
||||||
|
let b = Buffer.create 100 in
|
||||||
|
let ff = Format.formatter_of_buffer b in
|
||||||
|
|
||||||
|
(* Disable line breaks. *)
|
||||||
|
let ff_funs = Format.pp_get_formatter_out_functions ff () in
|
||||||
|
Format.pp_set_formatter_out_functions
|
||||||
|
ff
|
||||||
|
{ ff_funs with
|
||||||
|
out_newline = (fun _ -> ());
|
||||||
|
out_indent = (fun _ -> ());
|
||||||
|
out_spaces = (fun _ -> ());
|
||||||
|
};
|
||||||
|
|
||||||
|
Format.fprintf ff "strict digraph {\n";
|
||||||
|
Format.fprintf ff " overlap=scale;\n";
|
||||||
|
Format.fprintf ff " splines=true;\n";
|
||||||
|
Format.fprintf ff " rankdir=\"LR\";\n";
|
||||||
|
Seq.iter (fun (t, t') ->
|
||||||
|
Format.fprintf ff "\"%a\" -> \"%a\";\n"
|
||||||
|
L.pp t
|
||||||
|
L.pp t') g;
|
||||||
|
Format.fprintf ff "}@.";
|
||||||
|
Buffer.contents b
|
||||||
|
|
||||||
|
let display ?(verbose = false) ?(max = 20) g =
|
||||||
|
let gv_fn, oc = Filename.open_temp_file "red" ".dot" in
|
||||||
|
let pdf_fn = Filename.temp_file "graph" ".pdf" in
|
||||||
|
output_string oc @@ to_graphviz @@ Seq.take max g;
|
||||||
|
close_out oc;
|
||||||
|
if verbose then Printf.eprintf "Graph in %s, PDF in %s\n" gv_fn pdf_fn;
|
||||||
|
flush stderr;
|
||||||
|
ignore @@ Unix.system Printf.(sprintf "dot -Tpdf %s > %s" gv_fn pdf_fn);
|
||||||
|
ignore @@ Unix.system Printf.(sprintf "xdg-open %s" pdf_fn)
|
||||||
|
end
|
14
cours/cours-04/Rewrite.mli
Normal file
14
cours/cours-04/Rewrite.mli
Normal file
|
@ -0,0 +1,14 @@
|
||||||
|
module type LANG = sig
|
||||||
|
type t
|
||||||
|
val pp : t Fmt.t
|
||||||
|
val equal : t -> t -> bool
|
||||||
|
val rewrite : t -> t Seq.t
|
||||||
|
end
|
||||||
|
|
||||||
|
module Make(L : LANG) : sig
|
||||||
|
type graph = (L.t * L.t) Seq.t
|
||||||
|
val reductions : L.t -> graph
|
||||||
|
val is_normal : L.t -> bool
|
||||||
|
val normal_forms : L.t -> L.t Seq.t
|
||||||
|
val display : ?verbose:bool -> ?max:int -> graph -> unit
|
||||||
|
end
|
46
cours/cours-04/Seq.ml
Normal file
46
cours/cours-04/Seq.ml
Normal file
|
@ -0,0 +1,46 @@
|
||||||
|
include Stdlib.Seq
|
||||||
|
|
||||||
|
let hd xs = uncons xs |> Option.map fst
|
||||||
|
let tl xs = uncons xs |> Option.map snd
|
||||||
|
|
||||||
|
let rec const x () = cons x (const x) ()
|
||||||
|
|
||||||
|
let rec nth : type a. int -> a t -> a option =
|
||||||
|
fun n xs ->
|
||||||
|
if n = 0 then hd xs else tl xs |> Option.map (nth (n - 1)) |> Option.join
|
||||||
|
|
||||||
|
let join : type a. a t t -> a t =
|
||||||
|
let rec aux todo n k xss =
|
||||||
|
let continue () = aux [] (n + 1) n (append List.(to_seq @@ rev todo) xss) in
|
||||||
|
if k < 0 then continue ()
|
||||||
|
else
|
||||||
|
begin match uncons xss, todo with
|
||||||
|
| None, [] ->
|
||||||
|
empty
|
||||||
|
| None, _ :: _ ->
|
||||||
|
continue ()
|
||||||
|
| Some (xs, xss), _ ->
|
||||||
|
begin match uncons xs with
|
||||||
|
| None -> aux todo n (k - 1) xss
|
||||||
|
| Some (x, xs) -> fun () -> cons x (aux (xs :: todo) n (k - 1) xss) ()
|
||||||
|
end
|
||||||
|
end
|
||||||
|
in
|
||||||
|
fun xss () -> aux [] 1 0 xss ()
|
||||||
|
|
||||||
|
let ( let* ) xs f = map f xs |> concat
|
||||||
|
|
||||||
|
let rec combine f xs ys =
|
||||||
|
match uncons xs, uncons ys with
|
||||||
|
| Some (x, xs), Some (y, ys) -> fun () -> cons (f x y) (combine f xs ys) ()
|
||||||
|
| None, _ | _, None -> empty
|
||||||
|
|
||||||
|
let rec dedup eq xs =
|
||||||
|
match uncons xs with
|
||||||
|
| None -> xs
|
||||||
|
| Some (x, xs) -> cons x (filter (fun x' -> not (eq x x')) (dedup eq xs))
|
||||||
|
|
||||||
|
let rec nat : int t = fun () -> cons 0 (map ((+) 1) nat) ()
|
||||||
|
|
||||||
|
let nats : (int * int) t t =
|
||||||
|
combine (fun x ys -> map (fun y -> (x, y)) ys) nat (const nat)
|
5
cours/cours-04/dune
Normal file
5
cours/cours-04/dune
Normal file
|
@ -0,0 +1,5 @@
|
||||||
|
(library
|
||||||
|
(name cours04)
|
||||||
|
(libraries fmt unix)
|
||||||
|
(inline_tests)
|
||||||
|
(preprocess (pps ppx_expect)))
|
1
cours/cours-04/dune-project
Normal file
1
cours/cours-04/dune-project
Normal file
|
@ -0,0 +1 @@
|
||||||
|
(lang dune 2.0)
|
BIN
cours/cours-interpretation.pdf
Normal file
BIN
cours/cours-interpretation.pdf
Normal file
Binary file not shown.
|
@ -51,3 +51,16 @@
|
||||||
|
|
||||||
- En cours : questions/réponses au sujet du jalon 1 et introduction à
|
- En cours : questions/réponses au sujet du jalon 1 et introduction à
|
||||||
l'interprétation des programmes Hopix.
|
l'interprétation des programmes Hopix.
|
||||||
|
* Cours 04 <2023-10-11>
|
||||||
|
On discute de la gestion de la syntaxe et en particulier des lieurs, voir les
|
||||||
|
[[file:cours-semantique.pdf][transparents]].
|
||||||
|
* Cours 05 <2023-10-18>
|
||||||
|
On revient sur la gestion de la liaison, et de l'évaluation, voir les
|
||||||
|
[[file:cours-semantique.pdf][transparents]].
|
||||||
|
* Cours 06 <2023-10-25>
|
||||||
|
On termine les transparents précédents sur l'écriture d'évaluateurs.
|
||||||
|
|
||||||
|
Attention : le fichier contenant les diapos a été renommé, c'est désormais
|
||||||
|
[[file:cours-interpretation.pdf][transparents]].
|
||||||
|
|
||||||
|
On décrit le jalon 2.
|
||||||
|
|
Binary file not shown.
Reference in a new issue