(* $Header: /me/Eci/Slides/RCS/lambdav.ml,v 1.5 95/08/14 22:19:00 me Exp $ *) (* Traduction des constantes, operateurs de base et point fixe *) let zero = "\f.\x.x";; let truev = "\x.\y.(x itev3)";; let falsev = "\x.\y.(y itev3)";; let Thetav = "(\x.\f.f(\g.x x f g))(\x.\f.f(\g.x x f g))";; let iszero = "\x.(x(\y.false))true";; let pred = "\m.\f.\x.snd (m(\c.(pair (f(fst c))(fst c)))(pair x x))";; let add = "\m1.\m2.\f.\x.(m1 f) (m2 f x)";; let mult = "\m1.\m2.\f.\x. m1 (m2 f) x";; let exp = "\m1.\m2.m1 m2";; let lfst = "\p.p(\x.\y.x)";; let lsnd = "\p.p(\x.\y.y)";; let pair = "\x.\y.\z.z x y";; (* Analyse lexicale *) (* syntaxe abstraite des lambda termes *) type Ident == string;; type Lterm = Var of Ident | App of Lterm*Lterm | Abs of Ident*Lterm;; (* tokens *) type token_type = IDENT of string | BSLASH | DOT | LPAREN | RPAREN | IF | THEN | ELSE | TRUE | FALSE | THETAV | ADD | MULT | EXP | PRED | ISZERO | ZERO | FST | SND | PAIR ;; (* lexing *) let ident_token = let rec ident nom = function ((`a`..`z`|`A`..`Z`|`0`..`9` as c)::rest) -> ident (nom^(make_string 1 c)) rest | l -> (nom,l) in function ((`a`..`z`|`A`..`Z` as c)::rest) -> let (nom,r) = ident (make_string 1 c) rest in match nom with "if" -> (IF,r) | "then" -> (THEN,r) | "else" -> (ELSE,r) | "true" -> (TRUE,r) | "false" -> (FALSE,r) | "Thetav" -> (THETAV,r) | "add" -> (ADD,r) | "mult" -> (MULT,r) | "exp" -> (EXP,r) | "pred" -> (PRED,r) | "iszero" -> (ISZERO,r) | "zero" -> (ZERO,r) | "fst" -> (FST,r) | "snd" -> (SND,r) | "pair" -> (PAIR,r) | _ -> (IDENT nom,r);; let rec next_token = fun (`.`::rest) -> (DOT,rest) | (`\\`::rest) -> (BSLASH,rest) | (`(`::rest) -> (LPAREN,rest) | (`)`::rest) -> (RPAREN,rest) | (` `::rest) -> next_token rest | l -> try ident_token l with _ -> failwith "Bad identifier";; (* explode convertit un "string" en liste de caracteres *) let rec explode = fun "" -> [] | s -> (nth_char s 0)::(explode (sub_string s 1 ((string_length s)-1) ));; (* lex convertit une liste de caracteres en une liste de tokens *) let tl_of_cl = let rec iter l s = (try (let (t1,s1) = next_token s in iter (l@[t1]) s1) with _ -> l) in fun s -> iter [] s;; let lex = tl_of_cl;; (* Analyse syntaxique LL *) (* parsing *) let rec expr = function s -> let (e1,r1) = expr0 s in restapp e1 r1 and restapp e1 s = try let (e2,r) = expr0 s in (restapp (App (e1,e2))) r with _ -> (e1,s) and expr0 = fun (BSLASH::(IDENT s)::DOT::rest) -> let (e,r) = expr rest in (Abs(s,e),r) | (IF::rest) -> let (e1,(THEN::r1)) = expr rest in let (e2,(ELSE::r2)) = expr r1 in let (e3,r3) = expr r2 in ((App(App(e1,(Abs("itev",e2))),(Abs("itev",e3)))),r3) | (TRUE::rest) -> (analyseur truev,rest) | (FALSE::rest) -> (analyseur falsev,rest) | (THETAV::rest) -> (analyseur Thetav,rest) | (PRED::rest) -> (analyseur pred,rest) | (ADD::rest) -> (analyseur add,rest) | (MULT::rest) -> (analyseur mult,rest) | (EXP::rest) -> (analyseur exp,rest) | (ISZERO::rest) -> (analyseur iszero,rest) | (ZERO::rest) -> (analyseur zero,rest) | (FST::rest) -> (analyseur lfst,rest) | (SND::rest) -> (analyseur lsnd,rest) | (PAIR::rest) -> (analyseur pair,rest) | ((IDENT s)::rest) -> (Var s,rest) | (LPAREN::rest) -> let (e1,(RPAREN::r1)) = expr rest in (e1,r1) and analyseur s = fst (expr (lex (explode s)));; (* Pretty printing du resultat *) (* impression de l'arbre *) let rec print_expr = function Abs(s, a) -> "\\"^s^".("^( print_expr a)^")" | App(e1, e2) -> "("^( print_expr e1)^" "^(print_expr e2)^")" | Var v -> v ;; let rec print_expr_krivine = function Abs(s, a) -> "\\"^s^"."^( print_expr a) | App(e1, e2) -> "("^( print_expr e1)^") "^(print_expr e2) | Var v -> v ;; (* Section deux: EVALUATION *) (* 1) evaluateur call-by-value, comme defini en cours *) (* une substitution est une paire (variable, lambda terme) *) type Subst == Ident*Lterm;; (* generation de variables fraiches *) let genvar = let numvar = ref 0 in fun _ -> let nv = "_v"^(string_of_int !numvar) in numvar:=!numvar+1;nv;; let substs = ref 0 and alphas = ref 0;; let incsub () = substs := !substs+1 and incalpha () = alphas := !alphas +1 and reset () = substs := 0; alphas := 0;; (* l'operacion de substitution *) let rec subst = fun (Var v, (i,t)) -> incsub();if v=i then t else Var v | (App(e1,e2),sub) -> incsub();App((subst (e1,sub)), (subst (e2,sub))) | (Abs(v,e),sub) -> incsub(); incalpha(); let w = genvar() (* alpha conversion *) in Abs (w, (subst ((subst (e, (v,Var w))),sub)));; (* call-by-value *) let rec eval = fun (App(e1,e2)) -> (let e1' = eval e1 and e2' = eval e2 in match e1' with (Abs(v,e)) -> eval (subst (e,(v,e2'))) | _ -> App(e1',e2')) | e -> e;; let evcount e = reset(); let v = eval e in (v,!substs,!alphas);; (* call-by-name *) let rec evaln = fun (App(e1,e2)) -> (let e1' = evaln e1 in match e1' with (Abs(v,e)) -> evaln (subst (e,(v,e2))) | _ -> App(e1',e2)) | e -> e;; let evncount e = reset(); let v = evaln e in (v,!substs,!alphas);; (* Quelques lambda termes pour tester *) let Thetav = "(\x.\f.f(\g.x x f g))(\x.\f.f(\g.x x f g))";; let is0 = "\x.(x(\y.false))true";; let zero = "\f.\x.x";; let add = "\m1.\m2.\f.\x.(m1 f) (m2 f x)";; let mult = "\m1.\m2.\f.\x. m1 (m2 f) x";; let exp = "\m1.\m2.m1 m2";; let exp23=analyseur "(exp (\f.\x.f (f x)) (\f.\x.f (f (f x))) f x)";; let exp23lazy=analyseur "(exp (\f.\x.f (f x)) (\f.\x.f (f (f x))) (\f.f) x)";; let exp2_3=print_expr (eval (analyseur "(exp (\f.\x.f (f x)) (\f.\x.f (f (f x))) f x)"));; (* la factorielle *) let fact = analyseur ("Thetav(\f.\x.(if iszero x then (\f.\x.f x) else mult x (f (pred x))))");; (* factoriel de deux *) let fact2 = analyseur ("(Thetav(\f.\x.(if iszero x then (\f.\x.f x) else mult x (f (pred x)))))(\f.\x.(f (f x))) f x");; (* factoriel de deux applique a l'identite et a une variable, pour forcer l'evaluation lazy *) let fact2lazy = analyseur ("(Thetav(\f.\x.(if iszero x then (\f.\x.f x) else mult x (f (pred x)))))(\f.\x.(f (f x))) (\f.f) x");; (* factoriel de trois *) let fact3 = analyseur ("(Thetav(\f.\x.(if iszero x then (\f.\x.f x) else mult x (f (pred x)))))(\f.\x.(f (f (f x)))) f x");; (* factoriel de trois lazy *) let fact3lazy = analyseur ("(Thetav(\f.\x.(if iszero x then (\f.\x.f x) else mult x (f (pred x)))))(\f.\x.(f (f (f x)))) (\f.f) x");; (* La machine de Krivine *) (* evaluation call-by-name SANS faire les substitutions betement *) (* Quelques definitions: *) (* une Closure est un terme avec son environnement *) (* un environnement associe une Closure a chaque variable *) (* le stack contenant des Closures, est realise ici par une liste *) type Closure = Cl of Lterm * Env and Env == (Closure * Ident) list;; type Stack == Closure list;; (* l'evaluateur applique les transitiones de la machine, jusqu'au *) (* blocage, quand aucune transition ne peut s'appliquer *) let evalK = let rec evalKaux = fun (App(M,N), e ,Stack ) -> evalKaux (M, e,(Cl(N,e))::Stack) | (Abs(v,M), e ,s::Stack) -> evalKaux (M,(s,v)::e, Stack ) | ( Var x ,(Cl(M,e),v)::r,Stack ) -> if x = v then evalKaux ( M ,e,Stack) else evalKaux (Var x,r,Stack) | s -> s in fun t -> evalKaux (t,([]:Env),([]:Stack));; (* ici on modifie l'evaluateur pour rendre aussi le nombre d'etapes *) (* de reduction *) let evalKcount = let rec evalKaux = fun (App(M,N), e ,Stack ,n) -> evalKaux (M, e,(Cl(N,e))::Stack,n+1) | (Abs(v,M), e ,s::Stack,n) -> evalKaux (M,(s,v)::e, Stack ,n+1) | ( Var x ,(Cl(M,e),v)::r,Stack ,n) -> if x = v then evalKaux ( M ,e,Stack,n+1) else evalKaux (Var x,r,Stack,n+1) | s -> s in fun t -> evalKaux (t,([]:Env),([]:Stack),0);; (* MAIS, on peut ecrire ce code bien mieux!!!! *) (* Monadic approach (voir Moggi 1990 ou Wadler 1992 (POPL)) *) (* a: definition de la fonction de transition pure *) let Kstep = fun (* CODE ENV STACK CODE ENV STACK *) (App(M,N), e ,Stack ) -> (M , e ,(Cl(N,e))::Stack) | (Abs(v,M), e ,s::Stack) -> (M ,(s,v)::e, Stack ) | ( Var x ,(Cl(M,e),v)::r,Stack ) -> if x = v then ( M ,e,Stack) else (Var x,r,Stack) ;; (* b: ecriture de la boucle parametree par la monade *) let rec evalloop muM step = fun x -> try let s = muM step x in evalloop muM step s with _ -> x;; (* c: on definit les differents eta et mu *) (* Ex 1: on garde une liste d'etats *) let etal = fun t -> [(t,[],[])] and mul = fun f -> fun [] -> [] | (a::r) -> (f a)::(a::r);; let evalKlist = fun x -> evalloop mul Kstep (etal x);; (* affichage de la liste en syntaxe concrete *) type cclosure = Clc of string * cenv and cenv == (cclosure * Ident) list;; let rec p_clos = fun (Cl(t,e)) -> Clc(print_expr t,p_env e) and p_env e = map (fun (c,v) -> (p_clos c,v)) e;; let evalKclist = fun x -> let l = evalloop mul Kstep (etal x) in map (fun (c,e,s) -> (print_expr c,p_env e,map p_clos s)) (rev l);; (* Ex 2: on compte les transitions *) let etalc = fun t -> [((t,[],[]),0)] and mulc = fun f -> fun [] -> [] | ((a,n)::r) -> ((f a),n+1)::((a,n)::r);; let evalKlistcount = fun x -> evalloop mulc Kstep (etalc x);; (* Ex 3: afficher le terme a chaque etape *) (* il nous fau tpour cela la substitution simultanee ...*) let rec simsubst = fun (Var v, [(i,t)]) -> if v=i then t else Var v | (Var v, ((i,t)::rest)) -> if v=i then t else simsubst(Var v,rest) | (App(e1,e2),sub) -> App((simsubst (e1,sub)), (simsubst (e2,sub))) | (Abs(v,e),sub) -> let w = genvar() in Abs (w, (simsubst ((subst (e, (v,Var w))),sub)));; (* ... pour decoder la pile (Stack) *) let rec unfoldC = fun (Cl(t,[])) -> t | (Cl(t,env)) -> let substs=map (fun (c,v) -> (v,unfoldC c)) env in simsubst(t,substs);; (* et relire le terme que l'on evalue *) let KtoLambda = fun (trm,env,s) -> let t = unfoldC (Cl(trm,env)) and s'= map unfoldC s in it_list (fun t' -> fun t'' -> App(t',t'')) t s';; let etap = fun t -> (t,[],[]) and mup = fun f -> fun a -> print_string(print_expr (KtoLambda a));print_newline();(f a);; let evalKprint = fun x -> evalloop mup Kstep (etap x);;