let occ_nbr t = occ_nbr t 0;;
let goal_occ_nbr t = function
- | (_,Terms.Equation (l,r,_,_),_,_) ->
+ | (_,[],[Terms.Equation (l,r,_,_),_],_,_) ->
occ_nbr t l + occ_nbr t r
| _ -> assert false
;;
in
match l with
| [] -> acc
- | (_,hd,_,_)::tl ->
- match hd with
- | Terms.Equation (l,r,_,_) ->
+ | (_,nlit,plit,_,_)::tl ->
+ match nlit,plit with
+ | [],[Terms.Equation (l,r,_,_),_] ->
parse_symbols (aux (aux acc l) r) tl
- | Terms.Predicate _ -> assert false;
+ | _ -> assert false;
;;
let goal_pos t goal =
in
aux []
(match goal with
- | _,Terms.Equation (l,r,ty,_),_,_ -> Terms.Node [ Terms.Leaf B.eqP; ty; l; r ]
- | _,Terms.Predicate p,_,_ -> p)
+ | _,[],[Terms.Equation (l,r,ty,_),_],_,_ ->
+ Terms.Node [ Terms.Leaf B.eqP; ty; l; r ]
+ | _ -> assert false)
;;
let parse_symbols l goal =
let rec dependencies op clauses acc =
match clauses with
| [] -> acc
- | (_,lit,_,_)::tl ->
- match lit with
- | Terms.Predicate _ -> assert false
- | Terms.Equation (l,r,_,_) ->
- match l,r with
+ | (_,nlit,plit,_,_)::tl ->
+ match nlit,plit with
+ | [],[Terms.Equation (l,r,_,_),_] ->
+ (match l,r with
| (Terms.Node (Terms.Leaf op1::_),Terms.Node
(Terms.Leaf op2::_)) ->
if (B.eq op1 op) && not (B.eq op2 op) then
dependencies op tl (op1::acc)
else
dependencies op tl acc
- | _ -> dependencies op tl acc
+ | _ -> dependencies op tl acc)
+ | _ -> assert false
;;
let dependencies op clauses = HExtlib.list_uniq (List.sort Pervasives.compare (dependencies op clauses []));;