Merge branch 'jalon2/anri' of gaufre.informatique.univ-paris-diderot.fr:Anri/compilation-m1-2023 into jalon2/anri

This commit is contained in:
Nicolas PENELOUX 2023-11-06 18:04:43 +01:00
commit 37bf60305c
14 changed files with 757 additions and 0 deletions

View 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
View 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
View 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
View 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
View 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
View 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
View 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

View 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
View 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
View file

@ -0,0 +1,5 @@
(library
(name cours04)
(libraries fmt unix)
(inline_tests)
(preprocess (pps ppx_expect)))

View file

@ -0,0 +1 @@
(lang dune 2.0)

Binary file not shown.

View file

@ -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.