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


let unsatisfiable x = match x with Bool g -> not g



Scaricare 1.21 Mb.
Pagina4/12
29.03.2019
Dimensione del file1.21 Mb.
1   2   3   4   5   6   7   8   9   ...   12

let unsatisfiable x = match x with Bool g -> not g

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



  • Il dominio concreto

    • ricordiamo la struttura del dominio concreto eval

    • type eval = Int of int | Bool of bool | Unbound

    • | Funval of efun

    • and efun = eval -> eval

    • una operazione primitiva

    • let plus (x,y) = match (x,y) with

    • |(Int nx, Int ny) -> Int(nx + ny)

    • | _ -> Unbound



    La semantica denotazionale modificata 1

    • let rec sem (e:exp) (r:eval env) =

    • match e with

    • | Eint(n) -> alfa(Int(n))

    • | Ebool(b) -> alfa(Bool(b))

    • | Den(i) -> applyenv(r,i)

    • | Iszero(a) -> iszero((sem a r) )

    • | Eq(a,b) -> equ((sem a r) ,(sem b r) )

    • | Prod(a,b) -> mult((sem a r), (sem b r))

    • | Sum(a,b) -> plus((sem a r), (sem b r))

    • | Diff(a,b) -> diff((sem a r), (sem b r))

    • | Minus(a) -> minus((sem a r))

    • | And(a,b) -> et((sem a r), (sem b r))

    • | Or(a,b) -> vel((sem a r), (sem b r))

    • | Not(a) -> non((sem a r))

    • | Ifthenelse(a,b,c) -> let g = sem a r in

    • if typecheck("bool",g) then

    • (if valid(g) then sem b r else

    • (if unsatisfiable(g) then sem c r

    • else merge(g, sem b r, sem c r)))

    • else failwith ("nonboolean guard")

    • | Fun(i,a) -> makefun(Fun(i,a), r)

    • | Appl(a,b) -> applyfun(sem a r, sem b r)



    La semantica denotazionale modificata 2

    1   2   3   4   5   6   7   8   9   ...   12


    ©astratto.info 2019
    invia messaggio

        Pagina principale