pieuvre/pieuvre.ml

open Structs
open Str


exception TODOException;;
exception IllegalVarNameException of var

(* Affiche un λ-terme avec la même syntaxe qu’en entrée *)
let rec string_of_ty (t: ty) : string =
    match t with
        | TSimple(tn) -> tn
        | TImpl(t1,t2) -> "(" ^ (string_of_ty t1) ^ " -> " ^ (string_of_ty t2) ^ ")"
        | TFalse -> "⊥"
;;

(* Affiche un λ-terme avec la même syntaxe qu’en entrée *)
let rec string_of_lam (l: lam) : string = match l with
    | LFun(v,t,l') -> "λ"^v^":"^(string_of_ty t)^" . "^(string_of_lam l')
    | LApp(l1, l2) -> (string_of_lam l1)^" "^(string_of_lam l2)
    | LVar(v) -> v
    | LExf(l',t) -> "exf("^(string_of_lam l')^" : "^(string_of_ty t)^")"
;;

let split, tsplit =
    let splitter regex x =
    if string_match regex x 0
        then
            let xStr = matched_group 1 x in
            let xInt = matched_group 2 x in
            (xStr, int_of_string xInt)

    else raise (IllegalVarNameException(x))
    in (splitter varRegex, splitter tvarRegex);;

(* Renvoie un nom non utilisé dans la formule l qui commence par x *)
let findFreeName (l: lam) (x: var) =
    let xStr = fst (split x) in
    let maxi = ref 0 in
    let rec finder l = match l with
        | LFun(v,t,l') -> (finder (LVar(v));finder l')
        | LApp(l1, l2) -> (finder l1;finder l2)
        | LVar(v) -> let (vS,vI) = split v in
            if xStr=vS then maxi := max !maxi vI
        | LExf(l',t) -> finder l'
    in
    finder l;
    xStr ^ (string_of_int (!maxi+1))
;;

(* Renvoie un nom de type simple non utilisé dans le type t qui commence par x *)
let findTFreeName (t: ty) (x: tvar) =
    let xStr = fst (tsplit x) in
    let maxi = ref 0 in
    let rec finder t = match t with
        | TImpl(t1, t2) -> (finder t1;finder t2)
        | TSimple(y) -> let (yS,yI) = split y in
            if xStr=yS then maxi := max !maxi yI
        | TFalse -> () (* Le faux ne réserve pas de variables *)
    in
    finder t;
    xStr ^ (string_of_int (!maxi+1))
;;

(* Renvoie l[s/x] *)
let rec replace (l: lam) (x: var) (s: lam) = match l with
    | LFun(v,t,l') ->
        if(v=x)
        then let y=findFreeName l' v in
            LFun(v,t,replace l' v (LVar(y)))
            (* Pas besoin replace les x, ils ont tous été déjà remplacés *)
        else LFun(v,t,replace l' x s)
    | LApp(l1, l2) -> LApp(replace l1 x s, replace l2 x s)
    | LVar(v) -> if v=x then s else LVar(v)
    | LExf(l',t) -> LExf(replace l' x s, t)
;;

(* Teste si les deux λ-termes l1 et l2 sont α-convertibles *)
let rec alpha (l1: lam) (l2: lam) : bool =
    match (l1,l2) with
        | (LFun(v1,t1,l1'),LFun(v2,t2,l2')) ->
            (t1 = t2) &&
            (* On trouve un nom libre dans les deux sous-termes *)
            let v' = findFreeName (LApp(l1', l2')) v1 in
            alpha (replace l1 v1 (LVar(v'))) (replace l2 v2 (LVar(v')))
        | (LApp(lf1,lx1),LApp(lf2,lx2)) -> (alpha lf1 lf2) && (alpha lx1 lx2)
        | (LVar(x1),LVar(x2)) -> x1 = x2
        | (LExf(l1', t1),LExf(l2', t2)) -> t1=t2 && (alpha l1' l2')
        | _ -> false (* Les deux formules n'ont pas la même structure *)
;;

(* Fait un pas de β-réduction, et renvoie None si on a une forme normale *)
let rec betastep (l: lam) : lam option = match l with
    | LFun(v,t,l') -> betastep l'
    | LApp(lf,lx) ->
        begin
        match (betastep lf) with
        | Some lf' -> Some (LApp(lf',lx))
        | None ->
            match (betastep lx) with
            | Some lx' -> Some (LApp(lf, lx'))
            | None ->
                match lf with
                | LFun(x,_,corps) -> Some (replace corps x lx)
                | _ -> None (* On ne peut pas β-réduire *)
        end
    | LVar(x) -> None
    | LExf(l',_) -> betastep l'
;;

(* Affiche les réductions du λ-terme l jusqu’à atteindre une forme normale, ou part en boucle infinie *)
let rec reduce (l:lam) : unit =
    print_string (string_of_lam l);
    print_newline ();
    match (betastep l) with
    | Some l' -> reduce l'
    | None -> ()
;;

(* Calcule le type du λ-terme l sous l'environnement env. 7
Renvoie None si la formule n'est pas typable ou si la formule n'est pas close (sous d'environnement)*)
let rec computeType (env: gam) (l: lam) : ty option =
    match l with
    | LFun(x,tx,l') -> Option.bind (computeType ((x,tx)::env) l') (fun ty -> Some (TImpl(tx,ty)))
    | LApp(lf,lx) ->
        let tx = computeType env lx in
        let tf = computeType env lf in
        begin
            match tf with
            | Some TImpl(tx',ty') -> if Some tx'=tx then Some ty' else None
            | _ -> None (* Si none, l'argument n'est pas typable, si Some _, on ne peut typer l'application *)
        end
    | LVar(x) ->
        begin
        match env with
        | (y,ty)::env' -> if x=y then Some ty
            else computeType env' l
        | [] -> None
        end
    | LExf(l',t) ->
        match (computeType env l') with
        | Some TFalse -> Some t (* On applique le ExFalso *)
        | _ -> None (* Le ex falso a le mauvais type *)
;;

(* Vérifie que le λ-terme l sous l'environnement env a bien le type t *)
let typecheck (env: gam) (l: lam) (t: ty) : bool = (computeType env l = Some t);