(* Exercices de programmation du chapitre 1 *) (* La syntaxe abstraite des expressions mini-ML *) type expression = Var of string | Const of int | Op of string | Fun of string * expression | App of expression * expression | Paire of expression * expression | Let of string * expression * expression (* Substitution d'une variable x par une expression b dans une expression a *) let rec subst a x b = match a with Var v -> if v = x then b else a | Const n -> a | Op o -> a | Fun(v, a1) -> if v = x then a else Fun(v, subst a1 x b) | App(a1, a2) -> App(subst a1 x b, subst a2 x b) | Paire(a1, a2) -> Paire(subst a1 x b, subst a2 x b) | Let(v, a1, a2) -> Let(v, subst a1 x b, if v = x then a2 else subst a2 x b) (* La fonction partielle d'évaluation *) let rec valeur a = match a with Const c -> Const c | Op o -> Op o | Fun(x, a) -> Fun(x, a) | App(a1, a2) -> begin match valeur a1 with Fun(x, a) -> valeur (subst a x (valeur a2)) | Op "+" -> let (Paire(Const n1, Const n2)) = valeur a2 in Const(n1 + n2) | Op "fst" -> let (Paire(v1, v2)) = valeur a2 in v1 | Op "snd" -> let (Paire(v1, v2)) = valeur a2 in v2 end | Paire(a1, a2) -> Paire(valeur a1, valeur a2) | Let(x, a1, a2) -> valeur (subst a2 x (valeur a1)) (* L'algèbre de types *) type exprtype = Type_base of string | Type_var of string | Type_flèche of exprtype * exprtype | Type_produit of exprtype * exprtype type schéma = { quantif: string list; corps: exprtype } (* Calcul des variables libres *) let rec union l1 l2 = match l1 with [] -> l2 | hd :: tl -> union tl (if List.mem hd l2 then l2 else hd :: l2) let rec variables_libres t = match t with Type_base b -> [] | Type_var v -> [v] | Type_flèche(t1, t2) -> union (variables_libres t1) (variables_libres t2) | Type_produit(t1, t2) -> union (variables_libres t1) (variables_libres t2) let rec différence l1 l2 = match l1 with [] -> [] | hd :: tl -> if List.mem hd l2 then différence tl l2 else hd :: différence tl l2 let variables_libres_schéma s = différence (variables_libres s.corps) s.quantif let rec variables_libres_env env = match env with [] -> [] | (ident, schéma) :: reste -> union (variables_libres_schéma schéma) (variables_libres_env reste) (* Généralisation d'un type en un schéma *) let généralisation typ env = { quantif = différence (variables_libres typ) (variables_libres_env env); corps = typ } (* Prédicat d'instanciation. typ est une instance de sch = forall a1...aN. tau s'il existe une substitution S sur les a1...aN telle que typ = S(tau). Ici, nous construisons la substitution incrémentalement par récurrence sur typ et tau *) let instance typ sch = let subst = ref [] in let rec inst t1 t2 = match (t1, t2) with (Type_base b1, Type_base b2) -> b1 = b2 | (Type_var v, _) when List.mem v sch.quantif -> begin try List.assoc v !subst = t2 with Not_found -> subst := (v, t2) :: !subst; true end | (Type_var v, Type_var v') -> v = v' | (Type_flèche(r1, s1), Type_flèche(r2, s2)) -> inst r1 r2 && inst s1 s2 | (Type_produit(r1, s1), Type_produit(r2, s2)) -> inst r1 r2 && inst s1 s2 | (_, _) -> false in inst sch.corps typ