open Unif module type tipo = sig open Unif type tipo = Vvar of string | Intero | Booleano | Mkprod of tipo * tipo | Mkarrow of tipo * tipo val up: gterm -> tipo val down: tipo -> gterm val uppairlist: (gterm * gterm) list -> (tipo * tipo) list end module Tipi : tipo = struct open Unif type tipo = Vvar of string | Intero | Booleano | Mkprod of tipo * tipo | Mkarrow of tipo * tipo let rec up t = match t with (Gvar(x)) -> Vvar(x) |(Node("Intero",[])) -> Intero |(Node("Booleano",[])) -> Booleano |(Node("Mkprod",[x;y])) -> Mkprod(up(x),up(y)) |(Node("Mkarrow",[x;y])) -> Mkarrow(up(x),up(y)) |(_) -> failwith("term with wrong signature") let rec down t = match t with (Vvar(x)) -> Gvar(x) |(Intero) -> Node("Intero",[]) |(Booleano) -> Node("Booleano",[]) |(Mkprod(x,y)) -> Node("Mkprod",[down(x);down(y)]) |(Mkarrow(x,y)) -> Node("Mkarrow",[down(x);down(y)]) let rec uppairlist (l) = match l with |[] -> [] |(t1,t2)::l1 -> (up(t1),up(t2)) :: (uppairlist l1) end