Lines Matching defs:insts
522 fun term_pmatch lconsts env vtm ctm (sofar as (insts, homs)) =
532 else (safe_insert (vtm |-> ctm) insts, homs)
539 else (safe_insert (mk_dummy vty |-> mk_dummy cty) insts, homs)
547 val sofar' = (safe_insert (mk_dummy vty |-> mk_dummy cty) insts, homs)
559 val insts' = if vty = cty then insts
560 else safe_insert (mk_dummy vty |-> mk_dummy cty) insts
562 (insts', (env, ctm, vtm)::homs)
598 fun separate_insts tyavoids insts = let
599 val (realinsts, patterns) = partition (is_var o #redex) insts
666 fun term_homatch tyavoids lconsts tyins (insts, homs) = let
670 if null homs then insts
675 if aconv ctm vtm then term_homatch tyins (insts, tl homs)
679 val newinsts = (vtm |-> ctm)::insts
694 find_residue a insts
707 if aconv chop vhop then insts
708 else safe_insert (vhop |-> chop) insts
717 val vinsts = safe_insert (vhop |-> abstm) insts
730 (insts, (env, lc, lv)::(tl homs))
747 val insts = term_homatch tyavoids lconsts tyins pinsts_homs
749 separate_insts tyavoids insts