To annotate D in C, annotate D-tree in empty
assignment
{} and obtain its type pdec. Then annotate C-tree in
pdec; if it has type comm, annotate D in C with
type comm.
Declaration:
p |- E: Texp
p |- fun I=E: {I:Texp}dec
p |- D_1: p_1dec
p |- D_2: p_2dec
p |- D_1,D_2: (p_1 U p_2)dec
p |- D_1: p_1dec
pU p |- D_2: p_2dec
p |- D_1,D_2: (p_1 U p_2)dec
p_1 U p_2 := p_1 union p_2, if {I
|(I:H) inp_1}
intersect {I
|(I:H) in p_2} = {} (else undefined)
Construction and combination of type assignments.Wolfgang.Schreiner@risc.uni-linz.ac.at Id: abstraction.tex,v 1.1 1996/03/05 08:55:21 schreine Exp schreine