(* -------------------------------------------------------------------------- *) (* Et maintenant ... une machine abstraite pour call-by-value, la CAM *) (* i.e., la Categorical Abstract Machine (Curien '80) *) (* le code machine de la CAM *) type CamInst = Fst | Snd | Apply | Id | Cons | Push | Swap | Cur of CamInst list | Quote of Ident;; (* la compilation d'un lambda terme: est definie seulement pour les termes clos, *) (* mais ici, les variables libres on les traite comme des constantes predefinies *) type vartree = Emptytree | V of Ident | Node of vartree * vartree;; let rec Tcc = fun ((Var x),Emptytree) -> [Quote x] | ((Var x),Node(P1,P2))-> (match (P1,P2) with (_,V y) -> if y = x then [Snd] else tryTcc(x,P1,P2) | (V y,_) -> if y = x then [Fst] else tryTcc(x,P1,P2) | _ -> tryTcc(x,P1,P2)) | (App(M,N),P) -> [Push]@(Tcc(M,P))@[Swap]@(Tcc (N,P))@[Cons;Apply] | (Abs(x,M),P) -> [Cur(Tcc (M,Node(P,(V x))))] and tryTcc(x,P1,P2) = try [Fst]@(Tcc((Var x),P1)) with _ -> try [Snd]@(Tcc ((Var x),P2)) with _ -> [Quote x] ;; (* Mais ce sont des arbres un peu plats :-) *) (* autant utiliser des listes, non? *) let rec Tcc = fun ((Var x),[]) -> [Quote x] (* bof, a collapser, la! /\/\*) | ((Var x),(y::r))-> if y = x then [Snd] else Fst::(tryTcc(x,r)) | (App(M,N),P) -> [Push]@(Tcc(M,P))@[Swap]@(Tcc (N,P))@[Cons;Apply] | (Abs(x,M),P) -> [Cur(Tcc (M,x::P))] and tryTcc(x,r) = match r with [] -> [Quote x] | (y::r') -> if x =y then [Snd] else [Fst]@(tryTcc(x,r')) ;; (* Les valeurs de la CAM *) type CAMValue = Empty | Base of Ident | Pair of CAMValue * CAMValue | Close of CAMValue * CamInst list;; (* la CAM via monadic approach *) (* la fonction de transition de la CAM *) let CAMstep = fun (* CODE ACCUMULATOR ENV CODE ACCUMULATOR ENV *) ((Fst::C) , (Pair(s,t)) , E ) -> ( C , s , E ) | ((Snd::C) , (Pair(s,t)) , E ) -> ( C , t , E ) | ((Id::C) , s , E ) -> ( C , s , E ) | (((Quote c)::C) , s , E ) -> ( C , (Base c) , E ) | ((Cur(C)::C1) , s , E ) -> ( C1 , (Close(s,C)), E ) | ((Push::C) , s , E ) -> ( C , s , (s::E) ) | ((Swap::C) , s , (t::E) ) -> ( C , t , (s::E) ) | ((Cons::C) , s , (t::E) ) -> ( C , (Pair(t,s)) , E ) | ((Apply::C1) , (Pair(Close(s,C),t)) , E ) -> ( C@C1 , (Pair(s,t)) , E );; (* le resultat *) let evalCAM = let etal = fun t -> (Tcc(t,[]),Empty,[]) and mul = fun f -> fun a -> (f a) in fun x -> evalloop mul CAMstep (etal x);; (* le resultat avec compteur d'etapes de reduction *) let evalCAMcount = let etal = fun t -> ((Tcc(t,[]),Empty,[]),0) and mul = fun f -> fun (a,n) -> ((f a),n+1) in fun x -> evalloop mul CAMstep (etal x);; (* la liste de resultats *) let evalCAMlist = let etal = fun t -> [(Tcc(t,[]),Empty,[])] and mul = fun f -> fun [] -> [] | (a::r) -> (f a)::(a::r) in fun x -> evalloop mul CAMstep (etal x);; (* la liste de resultats *) let evalCAMlist2 a b= let etal = fun t -> [(Tcc(t,[]),a,b)] and mul = fun f -> fun [] -> [] | (a::r) -> (f a)::(a::r) in fun x -> evalloop mul CAMstep (etal x);; (* la liste de resultats avec compteur d'etapes *) let evalCAMlistcount = let etal = fun t -> [((Tcc(t,[]),Empty,[]),0)] and mul = fun f -> fun [] -> [] | ((a,n)::r) -> ((f a),n+1)::((a,n)::r) in fun x -> evalloop mul CAMstep (etal x);;