+(*****************************************************************************)
+(** OPERATIONS ON GOALS **)
+(** **)
+(** DEMODULATION_GOAL & SUPERPOSITION_LEFT **)
+(*****************************************************************************)
+
+let open_goal g =
+ match g with
+ | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
+ assert (LibraryObjects.is_eq_URI uri);
+ proof,menv,eq,ty,l,r
+ | _ -> assert false
+;;
+
+let ty_of_goal (_,_,ty) = ty ;;
+
+(* checks if two goals are metaconvertible *)
+let goal_metaconvertibility_eq g1 g2 =
+ Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
+;;
+
+(* when the betaexpand_term function is called on the left/right side of the
+ * goal, the predicate has to be fixed
+ * C[x] ---> (eq ty unchanged C[x])
+ * [posu] is the side of the [unchanged] term in the original goal
+ *)
+let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
+ let _,_,eq,ty,l,r = open_goal goal in
+ let unchanged = if posu = Utils.Left then l else r in
+ let unchanged = CicSubstitution.lift 1 unchanged in
+ let ty = CicSubstitution.lift 1 ty in
+ let pred =
+ match posu with
+ | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
+ | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
+ in
+ (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 context goal posu expansion =
+ let goalproof,_,_,_,_,_ = open_goal goal in
+ let (t,subst,menv,ug,(eq_found,eq_URI)) = 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 name = Cic.Name "x" in
+ let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
+ bo, (newgoalproofstep::goalproof)
+ in
+ let newmetasenv = (* Inference.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 (metasenv, context, ugraph) table goal =
+ let proof,menv,eq,ty,l,r = open_goal goal in
+ let c =
+ Utils.compare_weights ~normalize:true
+ (Utils.weight_of_term l) (Utils.weight_of_term r)
+ in
+ let big,small,possmall =
+ match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left
+ in
+ let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+ List.map (build_newgoal context goal possmall) expansions
+;;
+
+(** demodulation, when the target is a goal *)
+let rec demodulation_goal env table goal =
+ let goalproof,menv,_,_,left,right = open_goal goal in
+ let metasenv, context, ugraph = env in
+(* let term = Utils.guarded_simpl (~debug:true) context term in*)
+ let do_right () =
+ let resright = demodulation_aux menv context ugraph table 0 right in
+ match resright with
+ | Some t ->
+ let newg = build_newgoal context goal Utils.Left t in
+ if goal_metaconvertibility_eq goal newg then
+ false, goal
+ else
+ true, snd (demodulation_goal env table newg)
+ | None -> false, goal
+ in
+ let resleft = demodulation_aux menv context ugraph table 0 left in
+ match resleft with
+ | Some t ->
+ let newg = build_newgoal context goal Utils.Right t in
+ if goal_metaconvertibility_eq goal newg then
+ do_right ()
+ else
+ true, snd (demodulation_goal env table newg)
+ | None -> do_right ()
+;;
+
+let get_stats () = <:show<Indexing.>> ;;