open Structs
open Str


exception TODOException;;
exception IllegalVarNameException of var

(* Casse un objet option *)
let optionmatch (nonefun: 'b option) (somefun: 'a -> 'b option) (o: 'a option) : 'b option =
    match o with
        | Some x -> somefun x
        | None -> nonefun
;;

(* 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) ^ ")"
        | TAnd(t1,t2) -> "(" ^ (string_of_ty t1) ^ " /\\ " ^ (string_of_ty t2) ^ ")"
        | TOr(t1,t2) -> "(" ^ (string_of_ty t1) ^  " \\/ " ^ (string_of_ty t2) ^ ")"
        | TFalse -> "False"
        | TTrue -> "True"
;;

(* 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)^")"
    | LCouple(lg,ld) -> "("^(string_of_lam lg)^","^(string_of_lam ld)^")"
    | LFst(ll) -> "fst("^(string_of_lam ll)^")"
    | LSnd(ll) -> "snd("^(string_of_lam ll)^")"
    | LIg(ll,t) -> "ig("^(string_of_lam ll)^","^(string_of_ty t)^")"
    | LId(ll,t) -> "id("^(string_of_lam ll)^","^(string_of_ty t)^")"
    | LCase(ll,lg,ld) -> "case("^(string_of_lam ll)^","^(string_of_lam lg)^","^(string_of_lam ld)^")"
;;

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, if xInt="" then 0 else (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'
        | LCouple(l1,l2) -> (finder l1;finder l2)
        | LFst(l') -> finder l'
        | LSnd(l') -> finder l'
        | LIg(l',t) -> finder l'
        | LId(l',t) -> finder l'
        | LCase(ll,lg,ld) -> (finder ll; finder lg; finder ld)

    in
    finder l;
    xStr ^ (string_of_int (!maxi+1))
;;

(* Renvoie un nom non utilisé dans la liste de nom donnée, basée sur le nom x *)
let findHypName (names: var list) (x: var) =
    let xStr = fst (split x) in
    let maxi = ref 0 in
    let rec finder l = match l with
        | [] -> ()
        | v::r ->
            begin
                let (vS,vI) = split v in
                (if xStr=vS then maxi := max !maxi vI);
                finder r
            end
    in
    finder names;
    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
        | TAnd(t1, t2) -> (finder t1;finder t2)
        | TOr(t1, t2) -> (finder t1;finder t2)
        | TTrue -> ()
        | 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)
    | LCouple(lg,ld) -> LCouple(replace lg x s, replace ld x s)
    | LFst(l') -> LFst(replace l' x s)
    | LSnd(l') -> LSnd(replace l' x s)
    | LIg(l',t) -> LIg(replace l' x s, t)
    | LId(l',t) -> LId(replace l' x s, t)
    | LCase(l',lg,ld) -> LCase(replace l' x s, replace lg x s, replace ld x s)

;;

(* 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')
        | (LFst(l1),LFst(l2)) -> alpha l1 l2
        | (LSnd(l1),LSnd(l2)) -> alpha l1 l2
        | (LIg(l1,t1),LIg(l2,t2)) -> t1=t2 && alpha l1 l2
        | (LId(l1,t1),LId(l2,t2)) -> t1=t2 && alpha l1 l2
        | (LCase(l1,lg1,ld1),LCase(l2,lg2,ld2)) -> (alpha l1 l2) && (alpha lg1 lg2) && (alpha ld1 ld2)

        | _ -> 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') -> Option.bind (betastep l') (fun l' -> Some (LFun(v,t,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',t) -> Option.bind (betastep l') (fun l' -> Some (LExf(l',t)))
    | LCouple(lg,ld) -> optionmatch (Option.bind (betastep ld) (fun lg' -> Some (LCouple(ld,lg')))) (fun lg' -> Some (LCouple(lg',ld))) (betastep lg)
    | LFst(ll) -> begin
        match (ll,betastep ll) with
        | (_,Some ll') -> Some (LFst(ll'))
        | (LCouple(lg,ld),None) -> Some lg
        | (_,None) -> None
        end
    | LSnd(ll) -> begin
        match (ll,betastep ll) with
        | (_,Some ll') -> Some (LFst(ll'))
        | (LCouple(lg,ld),None) -> Some ld
        | (_,None) -> None
        end
    | LIg(ll,t) -> Option.bind (betastep ll) (fun l' -> Some (LIg(ll,t)))
    | LId(ll,t) -> Option.bind (betastep ll) (fun l' -> Some (LId(ll,t)))
    | LCase(ll,lg,ld) ->  begin
        match (ll,betastep ll) with
        | (_,Some ll') -> Some (LFst(ll'))
        | (LIg(_,_),None) -> Some lg
        | (LId(_,_),None) -> Some ld
        | (_,None) -> None
        end

;;

(* 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.
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) -> begin
        match (computeType env l') with
        | Some TFalse -> Some t (* On applique le ExFalso *)
        | _ -> None (* Le ex falso a le mauvais type *)
        end
    | LCouple(lg,ld) -> Option.bind (computeType env lg) (fun tg -> Option.bind (computeType env ld) (fun td -> Some (TAnd(tg,td))))
    | LFst(l') -> Option.bind (computeType env l') (function TAnd(t1,t2) -> Some t1 | _ -> None)
    | LSnd(l') -> Option.bind (computeType env l') (function TAnd(t1,t2) -> Some t2 | _ -> None)
    | LIg(l',td) -> Option.bind (computeType env l') (fun tg -> Some (TOr(tg,td)))
    | LId(l',tg) -> Option.bind (computeType env l') (fun td -> Some (TOr(tg,td)))
    | LCase(l',lg,ld) -> begin
        match (computeType env l',computeType env lg,computeType env ld) with
        | (Some TOr(t1a,t1b),Some TImpl(t2a,t2c),Some TImpl(t3b,t3c)) when t1a=t2a && t1b=t3b && t2c=t3c -> Some t3c
        | _ -> None
        end

;;

(* 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;;