Lines Matching refs:exp
67 type spec_type = {body : term, dst : term, entry : term, exit : term, exp : term, thm : thm}
80 {entry = entry_l, exit = exit_l, body = instr, thm = spec_thm, exp = src, dst = dest}
88 val exp = mk_plet (#dst spec1, #exp spec1,
89 mk_comb(mk_pabs (#dst spec1, #exp spec2), #dst spec1))
90 val value = mk_pair(exp, #dst spec2)
102 {entry = #entry spec1, exit = #exit spec2, body = union_body, thm = spec_thm, exp = exp, dst = #dst spec2}
138 val exp = mk_cond (mk_comb(c,args),
139 mk_comb(mk_pabs(args, #exp spec1), args),
140 mk_comb(mk_pabs(args, #exp spec2), args))
141 val value = mk_pair(exp, dest)
150 val exp' = mk_cond (J, #exp spec1, #exp spec2)
157 {entry = entry_l, exit = exit_l, body = b2, thm = spec_thm, exp = exp', dst = dest}
189 {entry = entry_l, exit = exit_l, body = inst [alpha |-> !VarType] nop, exp = t, dst = t,
193 else if is_let t then (* exp = LET (\v. N) M *)
207 {entry = entry_l, exit = exit_l, body = t, thm = mk_thm ([],``T``), exp = t, dst = t}