Lines Matching refs:src
71 fun mk_instr_spec (entry_l,exit_l) (dest,src) =
74 val value = mk_pair (src, dest)
75 val instr = list_mk_comb (inst [alpha |-> ty] asg_tm, [entry_l, dest, src, exit_l])
80 {entry = entry_l, exit = exit_l, body = instr, thm = spec_thm, exp = src, dst = dest}
123 fun mk_cond_spec (entry_l,exit_l) (dest,src) args =
125 val (J,M1,M2) = dest_cond src
164 mk_spec (entry_l,exit_l) (dest,src) args =
165 if is_atomic src orelse is_pair src then
166 mk_instr_spec (entry_l,exit_l) (dest,src)
168 else if is_cond src then (* t = if P then M else N *)
169 mk_cond_spec (entry_l,exit_l) (dest,src) args
171 else if is_comb src then
172 let val (operator, operands) = strip_comb src
175 mk_instr_spec (entry_l,exit_l) (dest,src)
241 let val [entry_l, dest, src, exit_l] = xs
242 in indent_label entry_l ^ term_to_string dest ^ " := " ^ term_to_string src ^