(* Source poly.ml *)

open S.Ast  (* Termes non-typés *)
open T.Type (* Types *)

(* Documentation du module 
Eq *)

(* Petite abréviation *)

module V = Eq.Vars (* Documentation du module Eq.Vars *)

(***************************************)
(* Divers calculs des variables libres *)
(***************************************)

(* Dans un type *)

let rec free t = match t with
  | Tvar n -> V.singleton n
  | Nat -> V.empty
  | Arrow (t1,t2) -> V.union (free t1) (free t2)

(* Dans un schéma de type *)
let free_scheme (xs,t) = V.diff (free t) (V.of_list xs)

(* Dans un environnement de typage *)
let free_env env =
  List.fold_right
    (fun (_,scr -> V.union (free_scheme scr)
    env V.empty

(*****************************************)
(* Diverses applications de substitution *)
(*****************************************)

(* À un schéma de type: on suppose que le support de s et vs sont disjoints *)

let subst_scheme s (xs,t) =
  assert (V.disjoint (Eq.dom s) (V.of_list xs)) ;
  (* Ce qui simplifie beaucoup... *)
  xs,Eq.subst_type s t

(* Application d'une substitution à un environnement *)
let subst_env s env =  List.map (fun (x,sc) -> x,subst_scheme s scenv

(****************************************)
(* 
Instance fraîche d'un schéma de type *)
(****************************************)

(* Fabriquer une substitution qui associe des variables fraîches aux
   variables de la liste xs *)

let subst_fresh xs =
  List.fold_right (fun x r ->
    Eq.comp
      (Eq.delta x (Tvar (Eq.fresh_var ())))
      rxs Eq.id

let
 freshen (xs,t) = Eq.subst_type (subst_fresh xst

(************************************************)
(* 
Généralisation d'un type en un schéma de type *)
(************************************************)

(* Assez sportif (pas de renommage), mais ils semble
   que cela fonctionne.
    1. La prise d'instance n'est en rien influencée le nom
       exact des xs (freshen ci-dessus)
    2. La substitution dans un schéma (subst_scheme)
       semble également correcte, car les variables quantifiée
       sont justement absentes de l'environnement *)


let generalize env t =
  let xs = V.elements (V.diff (free t) (free_env env)) in
  xs,t


(***************************)
(* Inféreur proprement dit *)
(***************************)


exception Error of string

let
 rec typeof s env t = match t with
(* Plus que facile *)
Num _ -> Nat,s
(* Pour l'application voir ci-après *)
App (t1,t2) -> typeof_app (typeof s env t1env t2
(* Les deux cas suivants sont des cas particuliers d'application *)
Op (_,t1,t2) ->
    let t_op = Arrow (NatArrow (Nat,Nat)) in
    let r = typeof_app (t_op,senv t1 in
    typeof_app r env t2
Ifz (t1,t2,t3) ->
    let t_if =
(* Type d'une occurrence d'une hypothétique fonction
   ifz : \forall A [Nat -> A -> A] *)

      let tv = Tvar (Eq.fresh_var ()) in
      Arrow (Nat,Arrow (tv,Arrow (tv,tv))) in
    let r = typeof_app (t_if,senv t1 in
    let r = typeof_app r env t2 in
    typeof_app r env t3
(* Pas grand chose à remarquer si ce n'est que env est étendu *)
Fun (x,t1) ->
    let tyx = Tvar (Eq.fresh_var ()) in
    let ty1,s = typeof s ((x,([],tyx))::envt1 in
    Arrow (tyx,ty1),s
(* Par l'opérateur de pt fixe Y: \forall A [(A -> A) -> A] *)
Fix (x,t) ->
    let t_fix =
      let tv = Eq.fresh_var () in
      Arrow (Arrow (Tvar tv,Tvar tv), Tvar tvin
    typeof_app (t_fix,senv (Fun (x,t))
(* Tout le polymorphisme est là, voir aussi freshen et generalize *)
Let (x,t1,t2) ->
    let ty1,s = typeof s env t1 in
    let sc1 = generalize (subst_env s env) (Eq.subst_type s ty1in
    typeof s ((x,sc1)::envt2
Var x ->
    let sc =
      try List.assoc x env
      with Not_found -> raise (Error ("Unbound var: "^x)) in
    freshen sc,s

(* Traitement de l'application, seul cas de résolution. *)
and typeof_app (ty_fun,senv t =    (* t_fun,s est le type de la fonction *)
  let ty_arg,s = typeof s env t in   (* typer l'argument *)
  let ty_res = Tvar (Eq.fresh_var ()) in
  let s = (* ajouter l'équation ty_fun = ty_arg -> ty_res *)
    Eq.mgu_incr ty_fun (Arrow (ty_arg,ty_res)) s in
  ty_ress

(***********************)
(* Fonctions exportées *)
(***********************)

(* Typer dans un environnement vide *)

let infer t =
  let ty,s = typeof Eq.id [] t in
  Eq.subst_type s ty

let
 verbose = List.mem "-v"  (Array.to_list Sys.argv)

(* Pour la boucle interactive *)
let infer_scheme env t =
  let ty,s = typeof Eq.id env t in
  let ty = Eq.subst_type s ty in
(* Généralisaton de toutes les variables de t,
   correct si env ne contient aucune variable libre,
   ce qui est le cas si les schema de types de env
   sont ainsi genéralisés. *)

  let xs = free ty in
  assert (V.disjoint (free_env envxs) ;
  V.elements xs,ty


(* Tests...

# Élémentaire
  Let x = 1;;
  Let y = 1+3;;
  Let z = x+y;;
;;

# fonctions
  Let id = Fun x -> x;;
  Let k1 = Fun x -> Fun y -> y;;
  Let k2 = Fun x -> Fun y -> x;;
  Let plus = Fun x -> Fun y -> x+y;;

# if + fonctions
  Let if1 = Fun x -> Fun y -> Ifz x Then y Else x;;
  Let if2 = Fun x -> Fun y -> Ifz x Then x Else y;;
  Let if3 = Fun x -> Fun y -> Fun z -> Ifz x Then y Else z;;

 Let f1 = Fun x -> Fun y -> x+0 In
 Let f2 = Fun x -> Fun y -> y+0 In
 Fun z -> Ifz z Then f1 Else f2
;;


# fonctions plus méchant
  Let t = Fun t -> Fun f -> t;;
  Let f = Fun t -> Fun f -> f;;
  Let not = Fun b -> Fun kt -> Fun kf -> b kf kt;;
  Let and = Fun b1 -> Fun b2 ->
     Fun kt -> Fun kf ->
       b1 (b2 kt kf) kf;;
  let or = Fun b1 -> Fun b2 ->  not (and (not b1) (not b2)) ;;

# Doit avoir le type de f
  Let b = and f (or t (or f f));;

# Généralisation
  Let test_gen1 = Fun x -> Let y = x in y;;
  Let test_gen2 =
    Let id = Fun x -> x In
    id id id id id

# Et encore
  Let app = Fun f -> Fun x -> f x;;
  let app1 = fun x ->
    let g = fun y -> x y in
    g;;

  Let app2 = Fun f ->
    Let g = Fun x -> f x In
    Let h = Fun x -> g x In
    h;;


  Let x = 1 In Fun f -> Fun z -> f x z;;

# Quelques pt. fixes
  Let Rec pow = Fun n -> Ifz n Then 1 Else 2 * pow (n-1);;
  Let Rec loop = loop;;
  Let Rec loop2 = Fun x -> loop2 x;;
  Let Rec loop3 = Fun x -> loop3 (x+x);;
  Let Rec loop4 = Fun x -> loop4 (loop4 (x+x));;

# Ne doit pas typer
  Let Rec f = Fun x -> Ifz x Then 0 Else f+1;;

# Casse tout
  Let pair =  Fun x -> Fun y -> Fun p -> p x y In
  Let x0 = Fix x -> x In
  Let x1 = pair x0 x0 In
  Let x2 = pair x1 x1 In
  Let x3 = pair x2 x2 In
  Let x4 = pair x3 x3 In
  Let x5 = pair x4 x4 In
  Let x6 = pair x5 x5 In
  Let x7 = pair x6 x6 In
  Let x8 = pair x7 x7 In
  Let x9 = pair x8 x8 In
  x9
  ;;

*)

This document was translated from LATEX by HEVEA.