| None -> ()
;;
-let check_target context target msg =
+let check_target bag context target msg =
let w, proof, (eq_ty, left, right, order), metas,_ =
Equality.open_equality target in
(* check that metas does not contains duplicates *)
let eqs = Equality.string_of_equality target in
let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right)
- @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof proof) in
+ @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof bag proof) in
let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
let _ = if menv <> metas then
begin
(*
try
ignore(CicTypeChecker.type_of_aux'
- metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph)
+ metas context (Founif.build_proof_term proof) CicUniv.empty_ugraph)
with e ->
prerr_endline msg;
- prerr_endline (Inference.string_of_proof proof);
- prerr_endline (CicPp.ppterm (Inference.build_proof_term proof));
+ prerr_endline (Founif.string_of_proof proof);
+ prerr_endline (CicPp.ppterm (Founif.build_proof_term proof));
prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right));
raise e
the build_newtarget functions]
))
*)
-let rec find_matches metasenv context ugraph lift_amount term termty =
+let rec find_matches bag metasenv context ugraph lift_amount term termty =
let module C = Cic in
let module U = Utils in
let module S = CicSubstitution in
Equality.open_equality equality
in
if Utils.debug_metas then
- ignore(check_target context (snd candidate) "find_matches");
+ ignore(check_target bag context (snd candidate) "find_matches");
if Utils.debug_res then
begin
let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
end;
if check && not (fst (CicReduction.are_convertible
~metasenv context termty ty ugraph)) then (
- find_matches metasenv context ugraph lift_amount term termty tl
+ find_matches bag metasenv context ugraph lift_amount term termty tl
) else
let do_match c =
let subst', metasenv', ugraph' =
- Inference.matching
+ Founif.matching
metasenv metas context term (S.lift lift_amount c) ugraph
in
Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
let res =
try
do_match c
- with Inference.MatchingFailure ->
- find_matches metasenv context ugraph lift_amount term termty tl
+ with Founif.MatchingFailure ->
+ find_matches bag metasenv context ugraph lift_amount term termty tl
in
if Utils.debug_res then ignore (check_res res "find1");
res
else
let res =
try do_match c
- with Inference.MatchingFailure -> None
+ with Founif.MatchingFailure -> None
in
if Utils.debug_res then ignore (check_res res "find2");
match res with
if order = U.Gt then
res
else
- find_matches
+ find_matches bag
metasenv context ugraph lift_amount term termty tl
| None ->
- find_matches metasenv context ugraph lift_amount term termty tl
+ find_matches bag metasenv context ugraph lift_amount term termty tl
;;
let find_matches metasenv context ugraph lift_amount term termty =
(*
as above, but finds all the matching equalities, and the matching condition
- can be either Inference.matching or Inference.unification
+ can be either Founif.matching or Inference.unification
*)
-let rec find_all_matches ?(unif_fun=Inference.unification)
+(* XXX termty unused *)
+let rec find_all_matches ?(unif_fun=Founif.unification)
metasenv context ugraph lift_amount term termty =
let module C = Cic in
let module U = Utils in
res::(find_all_matches ~unif_fun metasenv context ugraph
lift_amount term termty tl)
with
- | Inference.MatchingFailure
+ | Founif.MatchingFailure
| CicUnification.UnificationFailure _
| CicUnification.Uncertain _ ->
find_all_matches ~unif_fun metasenv context ugraph
find_all_matches ~unif_fun metasenv context ugraph
lift_amount term termty tl
with
- | Inference.MatchingFailure
+ | Founif.MatchingFailure
| CicUnification.UnificationFailure _
| CicUnification.Uncertain _ ->
find_all_matches ~unif_fun metasenv context ugraph
find_all_matches
?unif_fun metasenv context ugraph lift_amount term termty l
(*prerr_endline "CANDIDATES:";
- List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l;
+ List.iter (fun (_,x)->prerr_endline (Founif.string_of_equality x)) l;
prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
(List.length rc));*)
;;
(*
returns true if target is subsumed by some equality in table
*)
+(*
let print_res l =
prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
((pos,equation),_)) -> Equality.string_of_equality equation)l))
;;
+*)
let subsumption_aux use_unification env table target =
let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
- let metasenv, context, ugraph = env in
+ let _, context, ugraph = env in
let metasenv = tmetas in
let predicate, unif_fun =
if use_unification then
- Unification, Inference.unification
+ Unification, Founif.unification
else
- Matching, Inference.matching
+ Matching, Founif.matching
in
let leftr =
match left with
| None -> ok what leftorright tl
| Some s -> Some (s, equation, leftorright <> pos ))
with
- | Inference.MatchingFailure
+ | Founif.MatchingFailure
| CicUnification.UnificationFailure _ -> ok what leftorright tl
in
- match ok right Utils.Left leftr with
+ match ok right Utils.Left leftr with
| Some _ as res -> res
| None ->
let rightr =
subsumption_aux true x y z
;;
-let rec demodulation_aux ?from ?(typecheck=false)
+let subsumption_aux_all use_unification env table target =
+ let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
+ let _, context, ugraph = env in
+ let metasenv = tmetas in
+ let predicate, unif_fun =
+ if use_unification then
+ Unification, Founif.unification
+ else
+ Matching, Founif.matching
+ in
+ let leftr =
+ match left with
+ | Cic.Meta _ when not use_unification -> []
+ | _ ->
+ let leftc = get_candidates predicate table left in
+ find_all_matches ~unif_fun
+ metasenv context ugraph 0 left ty leftc
+ in
+ let rightr =
+ match right with
+ | Cic.Meta _ when not use_unification -> []
+ | _ ->
+ let rightc = get_candidates predicate table right in
+ find_all_matches ~unif_fun
+ metasenv context ugraph 0 right ty rightc
+ in
+ let rec ok_all what leftorright = function
+ | [] -> []
+ | (_, subst, menv, ug, (pos,equation))::tl ->
+ let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
+ try
+ let other = if pos = Utils.Left then r else l in
+ let what' = Subst.apply_subst subst what in
+ let other' = Subst.apply_subst subst other in
+ let subst', menv', ug' =
+ unif_fun metasenv m context what' other' ugraph
+ in
+ (match Subst.merge_subst_if_possible subst subst' with
+ | None -> ok_all what leftorright tl
+ | Some s ->
+ (s, equation, leftorright <> pos )::(ok_all what leftorright tl))
+ with
+ | Founif.MatchingFailure
+ | CicUnification.UnificationFailure _ -> (ok_all what leftorright tl)
+ in
+ (ok_all right Utils.Left leftr)@(ok_all left Utils.Right rightr )
+;;
+
+let subsumption_all x y z =
+ subsumption_aux_all false x y z
+;;
+
+let unification_all x y z =
+ subsumption_aux_all true x y z
+;;
+let rec demodulation_aux bag ?from ?(typecheck=false)
metasenv context ugraph table lift_amount term =
(* Printf.eprintf "term = %s\n" (CicPp.ppterm term);*)
let module C = Cic in
C.Implicit None, ugraph
in
let res =
- find_matches metasenv context ugraph lift_amount term termty candidates
+ find_matches bag metasenv context ugraph lift_amount term termty candidates
in
if Utils.debug_res then ignore(check_res res "demod1");
if res <> None then
(res, tl @ [S.lift 1 t])
else
let r =
- demodulation_aux ~from:"1" metasenv context ugraph table
+ demodulation_aux bag ~from:"1" metasenv context ugraph table
lift_amount t
in
match r with
)
| C.Prod (nn, s, t) ->
let r1 =
- demodulation_aux ~from:"2"
+ demodulation_aux bag ~from:"2"
metasenv context ugraph table lift_amount s in (
match r1 with
| None ->
let r2 =
- demodulation_aux metasenv
+ demodulation_aux bag metasenv
((Some (nn, C.Decl s))::context) ugraph
table (lift_amount+1) t
in (
)
| C.Lambda (nn, s, t) ->
let r1 =
- demodulation_aux
+ demodulation_aux bag
metasenv context ugraph table lift_amount s in (
match r1 with
| None ->
let r2 =
- demodulation_aux metasenv
+ demodulation_aux bag metasenv
((Some (nn, C.Decl s))::context) ugraph
table (lift_amount+1) t
in (
exception Foo
(** demodulation, when target is an equality *)
-let rec demodulation_equality ?from eq_uri newmeta env table target =
+let rec demodulation_equality bag ?from eq_uri newmeta env table target =
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
(* let w = Utils.compute_equality_weight stat in*)
(* let target = Equality.mk_equality (w, proof, stat, metas) in *)
if Utils.debug_metas then
- ignore(check_target context target "demod equalities input");
+ ignore(check_target bag context target "demod equalities input");
let metasenv' = (* metasenv @ *) metas in
let maxmeta = ref newmeta in
ignore(check_for_duplicates menv "input1");
ignore(check_disjoint_invariant subst menv "input2");
let substs = Subst.ppsubst subst in
- ignore(check_target context (snd eq_found) ("input3" ^ substs))
+ ignore(check_target bag context (snd eq_found) ("input3" ^ substs))
end;
let pos, equality = eq_found in
let (_, proof',
try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
with CicUtil.Meta_not_found _ -> ty
in
+ let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in
let what, other = if pos = Utils.Left then what, other else other, what in
let newterm, newproof =
let bo =
let stat = (eq_ty, left, right, ordering) in
let res =
let w = Utils.compute_equality_weight stat in
- (Equality.mk_equality (w, newproof, stat,newmenv))
+ (Equality.mk_equality bag (w, newproof, stat,newmenv))
in
if Utils.debug_metas then
- ignore(check_target context res "buildnew_target output");
+ ignore(check_target bag context res "buildnew_target output");
!maxmeta, res
in
- let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
+ let res =
+ demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left
+ in
if Utils.debug_res then check_res res "demod result";
let newmeta, newtarget =
match res with
| Some t ->
let newmeta, newtarget = build_newtarget true t in
- assert (not (Equality.meta_convertibility_eq target newtarget));
- if (Equality.is_weak_identity newtarget) ||
- (Equality.meta_convertibility_eq target newtarget) then
+ (* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
+ if (Equality.is_weak_identity newtarget) (* || *)
+ (*Equality.meta_convertibility_eq target newtarget*) then
newmeta, newtarget
else
- demodulation_equality ?from eq_uri newmeta env table newtarget
+ demodulation_equality bag ?from eq_uri newmeta env table newtarget
| None ->
- let res = demodulation_aux metasenv' context ugraph table 0 right in
+ let res = demodulation_aux bag metasenv' context ugraph table 0 right in
if Utils.debug_res then check_res res "demod result 1";
match res with
| Some t ->
(Equality.meta_convertibility_eq target newtarget) then
newmeta, newtarget
else
- demodulation_equality ?from eq_uri newmeta env table newtarget
+ demodulation_equality bag ?from eq_uri newmeta env table newtarget
| None ->
newmeta, target
in
the first free meta index, i.e. the first number above the highest meta
index: its updated value is also returned
*)
-let superposition_right
+let superposition_right bag
?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
let module C = Cic in
let module S = CicSubstitution in
Equality.open_equality target
in
if Utils.debug_metas then
- ignore (check_target context target "superpositionright");
+ ignore (check_target bag context target "superpositionright");
let metasenv' = newmetas in
let maxmeta = ref newmeta in
let res1, res2 =
in
let build_new ordering (bo, s, m, ug, eq_found) =
if Utils.debug_metas then
- ignore (check_target context (snd eq_found) "buildnew1" );
+ ignore (check_target bag context (snd eq_found) "buildnew1" );
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 ty, eq_ty = apply_subst s ty, apply_subst s eq_ty in
let newgoal, newproof =
(* qua *)
let bo' =
if ordering = U.Gt then newgoal, apply_subst s right
else apply_subst s left, newgoal in
let neworder = !Utils.compare_terms left right in
- let newmenv = (* Inference.filter s *) m in
+ let newmenv = (* Founif.filter s *) m in
let stat = (eq_ty, left, right, neworder) in
let eq' =
let w = Utils.compute_equality_weight stat in
- Equality.mk_equality (w, newproof, stat, newmenv) in
+ Equality.mk_equality bag (w, newproof, stat, newmenv) in
if Utils.debug_metas then
- ignore (check_target context eq' "buildnew3");
- let newm, eq' = Equality.fix_metas !maxmeta eq' in
+ ignore (check_target bag context eq' "buildnew3");
+ let newm, eq' = Equality.fix_metas bag !maxmeta eq' in
if Utils.debug_metas then
- ignore (check_target context eq' "buildnew4");
+ ignore (check_target bag context eq' "buildnew4");
newm, eq'
in
maxmeta := newmeta;
if Utils.debug_metas then
- ignore(check_target context newequality "buildnew2");
+ ignore(check_target bag context newequality "buildnew2");
newequality
in
let new1 = List.map (build_new U.Gt) res1
;;
(** demodulation, when the target is a theorem *)
-let rec demodulation_theorem newmeta env table theorem =
+let rec demodulation_theorem bag newmeta env table theorem =
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
!maxmeta, (newterm, newty, menv)
in
let res =
- demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
+ demodulation_aux bag (* ~typecheck:true *) metasenv' context ugraph table 0 termty
in
match res with
| Some t ->
if Equality.meta_convertibility termty newty then
newmeta, newthm
else
- demodulation_theorem newmeta env table newthm
+ demodulation_theorem bag newmeta env table newthm
| None ->
newmeta, theorem
;;
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);
+ (* assert (LibraryObjects.is_eq_URI uri); *)
proof,menv,eq,ty,l,r
| _ -> assert false
;;
(* ginve the old [goal], the side that has not changed [posu] and the
* expansion builds a new goal *)
-let build_newgoal context goal posu rule expansion =
+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
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 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 = (* Inference.filter subst *) menv in
+ let newmetasenv = (* Founif.filter subst *) menv in
(newgoalproof, newmetasenv, newterm)
;;
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 maxmeta =
+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
prerr_endline (string_of_int (List.length expansionsl));
prerr_endline (string_of_int (List.length expansionsr));
*)
- List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl
+ List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
@
- List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
+ List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
end
else
match c with
let big,small,possmall = l,r,Utils.Right in
let expansions, _ = betaexpand_term menv context ugraph table 0 big in
List.map
- (build_newgoal context goal possmall Equality.SuperpositionLeft)
+ (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 context goal possmall Equality.SuperpositionLeft)
+ (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
expansions
| Utils.Eq -> []
| _ ->
;;
(** demodulation, when the target is a goal *)
-let rec demodulation_goal env table 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 menv context ugraph table 0 right in
+ let resright = demodulation_aux bag menv context ugraph table 0 right in
match resright with
| Some t ->
let newg =
- build_newgoal context goal Utils.Left Equality.Demodulation t
+ 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 env table newg)
+ true, snd (demodulation_goal bag env table newg)
| None -> false, goal
in
- let resleft = demodulation_aux menv context ugraph table 0 left in
+ let resleft = demodulation_aux bag menv context ugraph table 0 left in
match resleft with
| Some t ->
- let newg = build_newgoal context goal Utils.Right Equality.Demodulation t in
+ 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 env table newg)
+ 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 () = "" ;;
projects / helm.git / blobdiff