Lines Matching defs:defs
55 fun sub_cnf f con defs (a, b) =
57 val (defs, a) = f defs a
58 val (defs, b) = f defs b
61 (defs, tm)
64 fun def_step (defs as (vec, n, ds), tm) =
72 | SOME (v, _) => (defs, v);
74 fun gen_cnf defs tm =
76 def_step (sub_cnf gen_cnf conjunction defs (dest_conj tm))
78 def_step (sub_cnf gen_cnf disjunction defs (dest_disj tm))
80 def_step (sub_cnf gen_cnf beq defs (dest_beq tm))
82 (defs, tm);
84 fun disj_cnf defs tm =
85 if is_disj tm then sub_cnf disj_cnf disjunction defs (dest_disj tm)
86 else gen_cnf defs tm;
88 fun conj_cnf defs tm =
89 if is_conj tm then sub_cnf conj_cnf conjunction defs (dest_conj tm)
90 else disj_cnf defs tm;
146 (*val (defs, tm') = conj_cnf (genvar (num --> bool), zero, []) tm*)
147 val (defs, tm') = conj_cnf ((!dcnfgv)(), zero, []) tm
148 val (vec, n, ds) = defs