Lines Matching refs:dst
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)
96 EXISTS_TAC (#exit spec1) THEN EXISTS_TAC (#dst spec1) THEN
102 {entry = #entry spec1, exit = #exit spec2, body = union_body, thm = spec_thm, exp = exp, dst = #dst 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,
198 val spec2 = gen_code (new_l, N, exit_l) (#dst spec1, output)
207 {entry = entry_l, exit = exit_l, body = t, thm = mk_thm ([],``T``), exp = t, dst = t}