+ (pred, subst, menv, ug, eq_f)
+;;
+
+(* ginve the old [goal], the side that has not changed [posu] and the
+ * expansion builds a new goal *)
+let build_newgoal bag context goal posu rule expansion =
+ let goalproof,_,_,_,_,_ = open_goal goal in
+ let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
+ let pos, equality = eq_found in
+ let (_, proof', (ty, what, other, _), menv',id) =
+ Equality.open_equality equality in
+ let what, other = if pos = Utils.Left then what, other else other, what in
+ let newterm, newgoalproof =
+ let bo =
+ Utils.guarded_simpl context
+ (apply_subst subst (CicSubstitution.subst other t))
+ in
+ let bo' = apply_subst subst t in
+ let ty = apply_subst subst ty in
+ let name = Cic.Name "x" in
+ let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
+ bo, (newgoalproofstep::goalproof)
+ in
+ let newmetasenv = (* Founif.filter subst *) menv in
+ (newgoalproof, newmetasenv, newterm)
+;;
+
+(**
+ superposition_left
+ returns a list of new clauses inferred with a left superposition step
+ the negative equation "target" and one of the positive equations in "table"
+*)
+let superposition_left bag (metasenv, context, ugraph) table goal maxmeta =
+ let names = Utils.names_of_context context in
+ let proof,menv,eq,ty,l,r = open_goal goal in
+ let c = !Utils.compare_terms l r in
+ let newgoals =
+ if c = Utils.Incomparable then
+ begin
+ let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
+ let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
+ (* prerr_endline "incomparable";
+ prerr_endline (string_of_int (List.length expansionsl));
+ prerr_endline (string_of_int (List.length expansionsr));
+ *)
+ List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
+ @
+ List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
+ end
+ else
+ match c with
+ | Utils.Gt -> (* prerr_endline "GT"; *)
+ let big,small,possmall = l,r,Utils.Right in
+ let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+ List.map
+ (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
+ expansions
+ | Utils.Lt -> (* prerr_endline "LT"; *)
+ let big,small,possmall = r,l,Utils.Left in
+ let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+ List.map
+ (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
+ expansions
+ | Utils.Eq -> []
+ | _ ->
+ prerr_endline
+ ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
+ assert false
+ in
+ (* rinfresco le meta *)
+ List.fold_right
+ (fun g (max,acc) ->
+ let max,g = Equality.fix_metas_goal max g in max,g::acc)
+ newgoals (maxmeta,[])
+;;
+
+(** demodulation, when the target is a goal *)
+let rec demodulation_goal bag env table goal =
+ let goalproof,menv,_,_,left,right = open_goal goal in
+ let _, context, ugraph = env in
+(* let term = Utils.guarded_simpl (~debug:true) context term in*)