Untitled

open Common

let rec gather_exp_ty_substitution gamma exp tau =
    let judgment = ExpJudgment(gamma, exp, tau) in
    match exp with 
    | ConstExp c ->
         let tau' = const_signature c in
         (match unify [(tau, freshInstance tau')]
          with None       -> None
             | Some sigma -> Some(Proof([],judgment), sigma))

    | VarExp (x) -> 
        let found_x = lookup_env gamma x in
        (match found_x with 
            | None -> None
            | Some gamma_x -> 
                (match unify [(tau, freshInstance (gamma_x) )]
                with None       -> None
                    | Some sigma -> Some(Proof([],judgment), sigma)))
    | BinOpAppExp (op, e1, e2) -> 
        let tau' = binop_signature op in  
        let tau1 = fresh() in 
        let tau2 = fresh() in 
        (match gather_exp_ty_substitution gamma e1 (tau1) with
            | None -> None
            | Some (proof1, sigma1) -> 
                (match gather_exp_ty_substitution (env_lift_subst sigma1 gamma) e2 (tau2) with 
                    | None -> None
                    | Some (proof2, sigma2) -> 
                        let sigma12 = subst_compose sigma1 sigma2 in 
                        let fun_ty = mk_fun_ty tau1 (mk_fun_ty tau2 tau) in
                        let mono = monoTy_lift_subst sigma12 fun_ty in 
                        let uni = unify [(mono, freshInstance tau')] in 
                        (match uni with 
                            | None -> None 
                            | Some (sigma3) -> 
                                let sigma321 = subst_compose sigma3 sigma12 in 
                                Some(Proof([proof1; proof2], judgment), sigma321)
                        )
                )
        )
    | MonOpAppExp (op, e1) -> 
        let tau' = monop_signature op in 
        let tau1 = fresh() in 
        (match gather_exp_ty_substitution gamma e1 tau1 with 
            | None -> None 
            | Some (proof1, sigma1) -> 
                let fun_ty = mk_fun_ty tau1 tau in 
                let mono = monoTy_lift_subst sigma1 fun_ty in 
                let uni = unify [(mono, freshInstance tau')] in 
                (match uni with 
                    | None -> None 
                    | Some (sigma2) -> 
                        let sigma21 = subst_compose sigma2 sigma1 in 
                        Some(Proof([proof1], judgment), sigma21)
                )
        )   
    | IfExp (e1, e2, e3) -> 
        (match gather_exp_ty_substitution gamma e1 bool_ty with 
            | None -> None 
            | Some (proof1, sigma1) ->
                let env_lift1 = env_lift_subst sigma1 gamma in 
                let mono1 = monoTy_lift_subst sigma1 tau in 
                (match gather_exp_ty_substitution env_lift1 e2 mono1 with 
                    | None -> None 
                    | Some (proof2, sigma2) ->
                        let sigma21 = subst_compose sigma2 sigma1 in
                        let env_lift2 = env_lift_subst sigma21 gamma in 
                        let mono2 = monoTy_lift_subst sigma21 tau in 
                        (match gather_exp_ty_substitution env_lift2 e3 mono2 with
                            | None -> None 
                            | Some (proof3, sigma3) -> 
                                let sigma321 = subst_compose sigma3 sigma21 in 
                                Some(Proof([proof1; proof2; proof3], judgment), sigma321)
                        ) 
                )
        )
    | FunExp (x, e1) ->
        let tau1 = fresh() in 
        let tau2 = fresh() in 
        let poly = polyTy_of_monoTy tau1 in 
        let new_gamma = ins_env gamma x poly in 
        (match gather_exp_ty_substitution new_gamma e1 tau2 with
            | None -> None 
            | Some (proof1, sigma1) ->
                let fun_ty = mk_fun_ty tau1 tau2 in 
                let mono_tau = monoTy_lift_subst sigma1 tau in 
                let mono_fun = monoTy_lift_subst sigma1 fun_ty in 
                let uni = unify[(mono_tau, mono_fun)] in 
                (match uni with 
                    | None -> None 
                    | Some (sigma2) ->
                        let sigma21 = subst_compose sigma2 sigma1 in 
                        Some(Proof([proof1], judgment), sigma21)       
                )
        )
    | AppExp (e1, e2) ->
        let tau1 = fresh() in 
        let fun_ty = mk_fun_ty tau1 tau in 
        (match gather_exp_ty_substitution gamma e1 fun_ty with 
            | None -> None 
            | Some (proof1, sigma1) -> 
                let mono_tau = monoTy_lift_subst sigma1 tau1 in 
                let new_gamma = env_lift_subst sigma1 gamma in 
                (match gather_exp_ty_substitution new_gamma e2 mono_tau with 
                    | None -> None 
                    | Some(proof2, sigma2) -> 
                        let sigma21 = subst_compose sigma2 sigma1 in 
                        Some(Proof([proof1; proof2], judgment), sigma21)
                )
        )
    | RaiseExp (e) ->
        (match gather_exp_ty_substitution gamma e int_ty with 
            | None -> None 
            | Some (proof, sigma) -> Some(Proof([proof], judgment), sigma)
        )
    | LetInExp (x, e1, e2) -> 
        let tau1 = fresh() in 
        (match gather_exp_ty_substitution gamma e1 tau1 with 
            | None -> None 
            | Some(proof1, sigma1) ->
                let sig1_gamma = env_lift_subst sigma1 gamma in 
                let sig_tau1 = monoTy_lift_subst sigma1 tau1 in 
                let gen1 = gen sig1_gamma sig_tau1 in 
                let new_sig1_gamma = ins_env sig1_gamma x gen1 in 
                let sig_tau = monoTy_lift_subst sigma1 tau in 
                (match gather_exp_ty_substitution new_sig1_gamma e2 sig_tau with 
                    | None -> None 
                    | Some(proof2, sigma2) -> 
                        let sigma21 = subst_compose sigma2 sigma1 in
                        Some(Proof([proof1; proof2], judgment), sigma21)
                )
        ) 
    | LetRecInExp (f, x, e1, e2) -> 
        let tau1 = fresh() in
        let tau2 = fresh() in 
        let mono_fun_tau1_tau2 = mk_fun_ty tau1 tau2 in 
        let poly_fun_tau1_tau2 = polyTy_of_monoTy mono_fun_tau1_tau2 in 
        let x_tau1 = polyTy_of_monoTy tau1 in
        let sum1 = ins_env gamma f poly_fun_tau1_tau2 in 
        let sum = ins_env sum1 x x_tau1 in 
        (match gather_exp_ty_substitution sum e1 tau2 with 
            | None -> None 
            | Some(proof1, sigma1) -> 
                let sig1_gamma = env_lift_subst sigma1 gamma in  
                let sig1_fun_tau1_tau2 = monoTy_lift_subst sigma1 mono_fun_tau1_tau2 in 
                let gen1 = gen sig1_gamma sig1_fun_tau1_tau2 in 

                let sum2 = ins_env sig1_gamma f gen1 in 
                let sig1_tau = monoTy_lift_subst sigma1 tau in 
                (match gather_exp_ty_substitution sum2 e2 sig1_tau with 
                    | None -> None 
                    | Some(proof2, sigma2) -> 
                        let sigma21 = subst_compose sigma2 sigma1 in 
                        Some(Proof([proof1; proof2], judgment), sigma21)
                )       
        )


        
    | _ -> raise (Failure "Not implemented yet")