Raw text file

(* Section 3 *)

let rec list_remove_all e = function
  | [] -> []
  | e' :: q ->
      if e = e' then list_remove_all e q
      else e' :: list_remove_all e q

(****************************************************)

type var
type typeconstr


(* Solution using polymorphic variants *)
module VP = struct

type monotype = [ `Var of var | `Constr of typeconstr * monotype list ]

type ('a, 'b) bound = [ `Bound of (var * 'a) * 'b ]
type bot = [ `Bottom ]

type polytype = [ monotype | bot | (polytype, polytype) bound ]


(* Free type variables *)
let rec ftv_monotype : monotype -> _ = function
  | `Var v -> [v]
  | `Constr (_, l) -> List.concat (List.map ftv_monotype l)
and ftv_polytype : polytype -> _ = function
  | #monotype as m -> ftv_monotype m
  | `Bottom -> []
  | `Bound ((v, t), t') ->
      ftv_polytype t @ (list_remove_all v (ftv_polytype t'))


(* Substitution of a variable by a monotype *)
let rec expand_mono_in_mono (v, m) = function
  | `Var v' -> if v = v' then m else `Var v'
  | `Constr (c, l) -> `Constr (c, List.map (expand_mono_in_mono (v, m)) l)
and expand_mono_in_poly (v, m) : polytype -> _ = function
  | #monotype as m' -> (expand_mono_in_mono (v, m) m' :> polytype)
  | `Bottom -> `Bottom
  | `Bound ((v', t), t') ->
      `Bound ((v', expand_mono_in_poly (v, m) t),
              if v = v' then t' else expand_mono_in_poly (v, m) t')


(* Types for the normal form *)
type constr = [ `Constr of typeconstr * monotype list ]

type nf_polytype = [ monotype | bot | (bot_poly, constr_poly) bound ]
and bot_poly  =    [            bot | (bot_poly, constr_poly) bound ]
and constr_poly =  [ constr   |       (bot_poly, constr_poly) bound ]


let rec nf : polytype -> nf_polytype = function
  | #bot | #monotype as t -> t
  | `Bound ((v, t), t') ->
      match nf t with
        | #monotype as m' -> nf (expand_mono_in_poly (v, m') t') (* Eq-Mono*)
        | #bot_poly as t ->
            match nf t' with
              | `Var v' ->
                  if v = v' then t (* Eq-Var *)
                  else `Var v' (* Eq-Free *)
              | #bot -> `Bottom (* Eq-Free *)
              | #constr_poly as t' ->
                  let ftv = ftv_polytype (t' : constr_poly :> polytype) in
                  if List.mem v ftv then `Bound ((v, t), t')
                  else t' (* Eq-Free *)
end


(* Solution using standard inductive *)
module IND = struct

type monotype = Var of var | Constr of constr
and constr = typeconstr * monotype list

type ('a, 'b) bound = (var * 'a) * 'b

type polytype =
    Mono of monotype  | Bot  | Bound of  (polytype, polytype)    bound
type nf_poly =
    Mono1 of monotype | Bot1 | Bound1 of (bot_poly, constr_poly) bound
and constr_poly =
    Constr3 of constr |        Bound3 of (bot_poly, constr_poly) bound
and bot_poly =          Bot2 | Bound2 of (bot_poly, constr_poly) bound


(* Substitution of variables by monotypes *)
let rec expand_mono_in_mono (v, m) = function
  | Var v' -> if v = v' then m else Var v'
  | Constr (c, l) -> Constr (c, List.map (expand_mono_in_mono (v, m)) l)

let rec expand_mono_in_poly (v, m) = function
  | Mono m' -> Mono (expand_mono_in_mono (v, m) m')
  | Bot -> Bot
  | Bound ((v', t), t') ->
      Bound ((v', expand_mono_in_poly (v, m) t),
             if v = v' then t' else expand_mono_in_poly (v, m) t')


(* Free type variables on bounds, monotypes, polytypes dans subsets
   of polytypes. We try to reuse as much code as possible *)
let ftv_bound ((v, t), t' : (_, _) bound) f1 f2 =
  f1 t @ (list_remove_all v (f2 t'))

let rec ftv_monotype = function
  | Var v -> [v]
  | Constr (_, l) -> ftv_list_monotype l
and ftv_list_monotype l = List.concat (List.map ftv_monotype l)
(* Not used in the solution
and ftv_polytype = function
  | Mono m -> ftv_monotype m
  | Bot -> []
  | Bound b -> ftv_bound b ftv_polytype ftv_polytype
*)

let rec ftv_poly = function
  | Bot2 -> []
  | Bound2 b -> ftv_bound' b
and ftv_constr = function
  | Constr3 (_, l) -> ftv_list_monotype l
  | Bound3 b -> ftv_bound' b
and ftv_bound' b = ftv_bound b ftv_poly ftv_constr


(* Projection of constr_poly and bot_poly into nf_poly. In constant time *)
let bot_to_nf = function
  | Bot2 -> Bot1
  | Bound2 b -> Bound1 b
let constr_to_nf = function
  | Constr3 b -> Mono1 (Constr b)
  | Bound3 b -> Bound1 b


let rec nf = function
  | Mono m -> Mono1 m
  | Bot -> Bot1
  | Bound ((v, t), t') ->
      let aux1 nft =
        let aux2 nft' =
          let ftv = ftv_constr nft' in
          if List.mem v ftv then Bound1 ((v, nft), nft')
          else (constr_to_nf nft')
        in
        match nf t' with
          | Bot1 -> Bot1
          | Mono1 (Var v') ->
              if v = v' then (bot_to_nf nft)
              else (Mono1 (Var v'))
          | Mono1 (Constr b) -> aux2 (Constr3 b)
          | Bound1 b' -> aux2 (Bound3 b')
      in
      match nf t with
        | Mono1 m -> nf (expand_mono_in_poly (v, m) t')
        | Bound1 b -> aux1 (Bound2 b)
        | Bot1 -> aux1 Bot2


end

This document was generated using caml2html