Un interprete astratto per l’inferenza dei tipi Contenuti l’inferenza dei tipi come interprete astratto denotazionale


let sigma = unifylist((v1,Intero) :: (v2,Intero) :: (c1 @ c2)) in



Scaricare 1.21 Mb.
Pagina12/12
29.03.2019
Dimensione del file1.21 Mb.
1   ...   4   5   6   7   8   9   10   11   12

let sigma =

  • unifylist((v1,Intero) :: (v2,Intero) :: (c1 @ c2)) in

  • match sigma with

  • |Fail -> (Notype,[])

  • |Subst(s) -> (Intero,s)



  • Astrazione e applicazione

    • let rec makefun(Fun(ii,aa),r) =

    • let f1 =newvar() in let f2 =newvar() in

    • let body = sem aa (bind(r,ii,(f1,[]))) in

    • (match body with (t,c) ->

    • let sigma = unifylist( (t,f2) :: c) in

    • (match sigma with

    • |Fail -> (Notype,[])

    • |Subst(s) -> ((applysubst sigma(Mkarrow(f1,f2))),s)

    • let applyfun ((v1,c1),(v2,c2)) =

    • let f1 =newvar() in let f2 =newvar() in

    • let sigma =

    • unifylist((v1,Mkarrow(f1,f2))::(v2,f1)::(c1 @ c2)) in

    • match sigma with

    • |Fail -> (Notype,[])

    • |Subst(s) -> (applysubst sigma f2,s)



    Astrazione di valori e glb

    • let alfa x = match x with

    • | Int _ -> (Intero, [])

    • | Bool _ -> (Boolean, [])

    • let gci ((v1,c1),(v2,c2)) =

    • let sigma = unifylist((v1,v2) :: (c1 @ c2)) in

      • match sigma with
        • |Fail -> (Notype,[])
        • |Subst(s) -> (applysubst sigma v1,s)


    merge e condizionale

    • let valid x = false

    • let unsatisfiable x = false

    • let merge (a,b,c) = match a with

    • |(Notype,_) -> (Notype,[])

    • |(v0,c0) ->

    • let sigma = unifylist((v0,Intero)::c0) in

    • match sigma with

    • |Fail -> (Notype,[])

    • |Subst(s) -> match gci(b, c) with

    • |(Notype,_) -> (Notype,[])

    • |(v1,c1) -> let sigma1 = unifylist(c1@s) in

    • match sigma1 with

    • |Fail -> (Notype,[])

    • |Subst(s1) -> (applysubst sigma1 v1,s1)



    Calcolo del punto fisso astratto 1

    • let makefunrec (i, Fun(ii, aa), r) =

    • let functional ff =

    • sem (Fun(ii, aa)) (bind(r, i, ff)) in

    • let rec alfp ff =

    • let tnext = functional ff in

    • (match tnext with

    • |(Notype, _) -> (Notype,[])

    • | _ -> if abstreq(tnext,ff) then ff

    • else alfp tnext in

    • alfp (newvar(), [])



    Calcolo del punto fisso astratto 2

    • let makefunrec (i, Fun(ii, aa), r) =

    • let functional ff =

    • sem (Fun(ii, aa)) (bind(r, i, ff)) in

    • let rec alfp ff =

    • let tnext = functional ff in

    • (match tnext with

    • |(Notype, _) -> (Notype,[])

    • | _ -> if abstreq(tnext,ff) then ff

    • else alfp tnext in

    • alfp (newvar(), [])

    • dato che esistono catene crescenti infinite, il calcolo del punto fisso può divergere

    • abbiamo bisogno di un operatore di widening che garantisca la terminazione calcolando una approssimazione superiore del minimo punto fisso

      • un tipo meno generale


    Widening

    • let makefunrec (i, Fun(ii, aa), r) =

    • let functional ff =

    • sem (Fun(ii, aa)) (bind(r, i, ff)) in

    • let alfp ff =

    • let tnext = functional ff in

    • (match tnext with

    • |(Notype, _) -> (Notype,[])

    • | _ -> widening(ff, tnext) in

    • alfp (newvar(), [])

    • let widening ((f1,c1),(t,c)) =

      • let sigma = unifylist( (t,f1) :: (c@c1)) in
      • (match sigma with
        • |Fail -> (Notype,[])
        • |Subst(s) -> (applysubst sigma t,s))
    • questo widening (unificazione) è usato anche nell’algoritmo di inferenza di tipi di ML





    Condividi con i tuoi amici:
    1   ...   4   5   6   7   8   9   10   11   12


    ©astratto.info 2019
    invia messaggio

        Pagina principale