Merge and function application
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)
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)
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)
Previous slide
Next slide
Back to first slide
View graphic version