75 "~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) = (ctxt, sel, oris, pbl, ((#ppc o get_pbt) cpI), ct); |
75 "~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) = (ctxt, sel, oris, pbl, ((#ppc o get_pbt) cpI), ct); |
76 val SOME t = parseNEW ctxt str; |
76 val SOME t = parseNEW ctxt str; |
77 is_known ctxt sel oris t; |
77 is_known ctxt sel oris t; |
78 "~~~~~ fun is_known, args:"; val (ctxt, sel, ori, t) = (ctxt, sel, oris, t); |
78 "~~~~~ fun is_known, args:"; val (ctxt, sel, ori, t) = (ctxt, sel, oris, t); |
79 val _ = tracing ("RM is_known: t=" ^ UnparseC.term t); |
79 val _ = tracing ("RM is_known: t=" ^ UnparseC.term t); |
80 val ots = (Library.distinct op = o flat o (map #5)) (ori:ori list); |
80 val ots = (Library.distinct op = o flat o (map #5)) (ori:O_Model.T); |
81 val oids = ((map (fst o dest_Free)) o Library.distinct op = o flat o (map vars)) ots; |
81 val oids = ((map (fst o dest_Free)) o Library.distinct op = o flat o (map vars)) ots; |
82 val (d, ts) = I_Model.split_dts t; |
82 val (d, ts) = I_Model.split_dts t; |
83 "~~~~~ fun I_Model.split_dts, args:"; val (t as d $ arg) = t; |
83 "~~~~~ fun I_Model.split_dts, args:"; val (t as d $ arg) = t; |
84 (*if is_dsc d then () else error "TODO";*) |
84 (*if is_dsc d then () else error "TODO";*) |
85 if is_dsc d then () else error "TODO"; |
85 if is_dsc d then () else error "TODO"; |