+(*****************************************************************************)
+(** 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 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*)
+ let do_right () =
+ let resright = demodulation_aux bag menv context ugraph table 0 right in
+ match resright with
+ | Some t ->
+ let newg =
+ build_newgoal bag context goal Utils.Left Equality.Demodulation t
+ in
+ if goal_metaconvertibility_eq goal newg then
+ false, goal
+ else
+ true, snd (demodulation_goal bag env table newg)
+ | None -> false, goal
+ in
+ let resleft = demodulation_aux bag menv context ugraph table 0 left in
+ match resleft with
+ | Some t ->
+ let newg = build_newgoal bag context goal Utils.Right Equality.Demodulation t in
+ if goal_metaconvertibility_eq goal newg then
+ do_right ()
+ else
+ true, snd (demodulation_goal bag env table newg)
+ | None -> do_right ()
+;;
+
+type next = L | R
+type solved = Yes of Equality.goal | No of Equality.goal list
+
+(* returns all the 1 step demodulations *)
+module C = Cic;;
+module S = CicSubstitution;;
+let rec demodulation_all_aux
+ metasenv context ugraph table lift_amount term
+=
+ let candidates =
+ get_candidates ~env:(metasenv,context,ugraph) Matching table term
+ in
+ match term with
+ | C.Meta _ -> []
+ | _ ->
+ let termty, ugraph = C.Implicit None, ugraph in
+ let res =
+ find_all_matches
+ metasenv context ugraph lift_amount term termty candidates
+ in
+ match term with
+ | C.Appl l ->
+ let res, _, _ =
+ List.fold_left
+ (fun (res,l,r) t ->
+ res @
+ List.map
+ (fun (rel, s, m, ug, c) ->
+ (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
+ (demodulation_all_aux
+ metasenv context ugraph table lift_amount t),
+ l@[List.hd r], List.tl r)
+ (res, [], List.map (S.lift 1) l) l
+ in
+ res
+ | C.Prod (nn, s, t)
+ | C.Lambda (nn, s, t) ->
+ let context = (Some (nn, C.Decl s))::context in
+ let mk s t =
+ match term with
+ | Cic.Prod _ -> Cic.Prod (nn,s,t) | _ -> Cic.Lambda (nn,s,t)
+ in
+ res @
+ List.map
+ (fun (rel, subst, m, ug, c) ->
+ mk (S.lift 1 s) rel, subst, m, ug, c)
+ (demodulation_all_aux
+ metasenv context ugraph table (lift_amount+1) t)
+ (* we could demodulate also in s, but then t may be badly
+ * typed... *)
+ | t -> res
+;;
+
+let solve_demodulating bag env table initgoal steps =
+ let _, context, ugraph = env in
+ let solved goal res side =
+ let newg = build_newgoal bag context goal side Equality.Demodulation res in
+ match newg with
+ | (goalproof,m,Cic.Appl[Cic.MutInd(uri,n,ens);eq_ty;left;right])
+ when LibraryObjects.is_eq_URI uri ->
+ (try
+ let _ =
+ Founif.unification m m context left right CicUniv.empty_ugraph
+ in
+ Yes newg
+ with CicUnification.UnificationFailure _ -> No [newg])
+ | _ -> No [newg]
+ in
+ let solved goal res_list side =
+ let newg = List.map (fun x -> solved goal x side) res_list in
+ try
+ List.find (function Yes _ -> true | _ -> false) newg
+ with Not_found ->
+ No (List.flatten (List.map (function No s -> s | _-> assert false) newg))
+ in
+ let rec first f l =
+ match l with
+ | [] -> None
+ | x::tl ->
+ match f x with
+ | None -> first f tl
+ | Some x as ok -> ok
+ in
+ let rec aux steps next goal =
+ if steps = 0 then None else
+ let goalproof,menv,_,_,left,right = open_goal goal in
+ let do_step t =
+ demodulation_all_aux menv context ugraph table 0 t
+ in
+ match next with
+ | L ->
+ (match do_step left with
+ | _::_ as res ->
+ (match solved goal res Utils.Right with
+ | No newgoals ->
+ (match first (aux (steps - 1) L) newgoals with
+ | Some g as success -> success
+ | None -> aux steps R goal)
+ | Yes newgoal -> Some newgoal)
+ | [] -> aux steps R goal)
+ | R ->
+ (match do_step right with
+ | _::_ as res ->
+ (match solved goal res Utils.Left with
+ | No newgoals ->
+ (match first (aux (steps - 1) L) newgoals with
+ | Some g as success -> success
+ | None -> None)
+ | Yes newgoal -> Some newgoal)
+ | [] -> None)
+ in
+ aux steps L initgoal
+;;
+
+let get_stats () = "" ;;