List.exists
(fun (_,_,ty) ->
try
- let s,_ = CicTypeChecker.type_of_aux' metas ctx ty CicUniv.empty_ugraph
+ let s,_ = CicTypeChecker.type_of_aux' metas ctx ty CicUniv.oblivion_ugraph
in s = Cic.Sort(Cic.Prop)
with _ ->
prerr_endline ("ERROR typing " ^ CicPp.ppterm ty); assert false) metas
in
if (not b) then
begin
- prerr_endline ("extended context " ^ msg);
- prerr_endline (CicMetaSubst.ppmetasenv [] menv);
+ debug_print (lazy ("extended context " ^ msg));
+ debug_print (lazy (CicMetaSubst.ppmetasenv [] menv));
end;
b
| None -> false
Founif.matching
metasenv metas context term (S.lift lift_amount c) ugraph
in
- check_metasenv "founif :" metasenv';
+ if Utils.debug_metas then
+ check_metasenv "founif :" metasenv';
Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
in
let c, other =
can be either Founif.matching or Inference.unification
*)
(* XXX termty unused *)
-let rec find_all_matches ?(unif_fun=Founif.unification)
+let rec find_all_matches ?(unif_fun=Founif.unification) ?(demod=false)
metasenv context ugraph lift_amount term termty =
let module C = Cic in
let module U = Utils in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
(* prerr_endline ("matching " ^ CicPp.ppterm term); *)
- let cmp = !Utils.compare_terms in
+ let cmp x y =
+ let r = !Utils.compare_terms x y in
+(*
+ prerr_endline (
+ CicPp.ppterm x ^ " " ^
+ Utils.string_of_comparison r ^ " " ^
+ CicPp.ppterm y );
+*)
+ r
+ in
let check = match termty with C.Implicit None -> false | _ -> true in
function
| [] -> []
let c' = apply_subst s c
and other' = apply_subst s other in
let order = cmp c' other' in
- if order <> U.Lt && order <> U.Le then
+ if (demod && order = U.Gt) ||
+ (not demod && (order <> U.Lt && order <> U.Le))
+ then
res::(find_all_matches ~unif_fun metasenv context ugraph
lift_amount term termty tl)
else
find_all_matches ~unif_fun metasenv context ugraph
- lift_amount term termty tl
+ lift_amount term termty tl
with
| Founif.MatchingFailure
| CicUnification.UnificationFailure _
;;
let find_all_matches
- ?unif_fun metasenv context ugraph lift_amount term termty l
+ ?unif_fun ?demod metasenv context ugraph lift_amount term termty l
=
find_all_matches
- ?unif_fun metasenv context ugraph lift_amount term termty l
+ ?unif_fun ?demod metasenv context ugraph lift_amount term termty l
(*prerr_endline "CANDIDATES:";
List.iter (fun (_,x)->prerr_endline (Founif.string_of_equality x)) l;
prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
let _, context, ugraph = env in
let metasenv = tmetas in
- check_for_duplicates metasenv "subsumption_aux_all";
+ if Utils.debug_metas then
+ check_for_duplicates metasenv "subsumption_aux_all";
let predicate, unif_fun =
if use_unification then
Unification, Founif.unification
;;
let unification_all x y z =
- prerr_endline "unification_all"; subsumption_aux_all true x y z
+ subsumption_aux_all true x y z
;;
let rec demodulation_aux bag ?from ?(typecheck=false)
let module S = CicSubstitution in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
- (* prerr_endline ("demodulating " ^ CicPp.ppterm term); *)
- check_for_duplicates metasenv "in input a demodulation aux";
+ if Utils.debug_metas then
+ check_for_duplicates metasenv "in input a demodulation aux";
let candidates =
get_candidates
~env:(metasenv,context,ugraph) (* Unification *) Matching table term
- in let candidates = List.filter (fun _,x -> not (not_unit_eq context x)) candidates
- in
+ in
+(* let candidates = List.filter (fun _,x -> not (not_unit_eq context x)) candidates in *)
let res =
match term with
| C.Meta _ -> None
exception Foo
(** demodulation, when target is an equality *)
-let rec demodulation_equality bag ?from eq_uri newmeta env table target =
- (*
- prerr_endline ("demodulation_eq:\n");
- Index.iter table (fun l ->
- let l = Index.PosEqSet.elements l in
- let l =
- List.map (fun (p,e) ->
- Utils.string_of_pos p ^ Equality.string_of_equality e) l in
- prerr_endline (String.concat "\n" l)
- );
- *)
+let rec demodulation_equality bag ?from eq_uri env table target =
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
if Utils.debug_metas then
ignore(check_target bag context target "demod equalities input");
let metasenv' = (* metasenv @ *) metas in
- let maxmeta = ref newmeta in
- let build_newtarget is_left (t, subst, menv, ug, eq_found) =
+ let build_newtarget bag is_left (t, subst, menv, ug, eq_found) =
if Utils.debug_metas then
begin
let pos, equality = eq_found in
let (_, proof',
(ty, what, other, _), menv',id') = Equality.open_equality equality in
+ (*
let ty =
- try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
- with CicUtil.Meta_not_found _ -> ty
- in
+ try fst (CicTypeChecker.type_of_aux' menv' 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 left, right = if is_left then newterm, right else left, newterm in
let ordering = !Utils.compare_terms left right in
let stat = (eq_ty, left, right, ordering) in
- let res =
+ let bag, res =
let w = Utils.compute_equality_weight stat in
- (Equality.mk_equality bag (w, newproof, stat,newmenv))
+ Equality.mk_equality bag (w, newproof, stat,newmenv)
in
if Utils.debug_metas then
ignore(check_target bag context res "buildnew_target output");
- !maxmeta, res
+ bag, res
in
-
let res =
demodulation_aux bag ~from:"from3" metasenv' context ugraph table 0 left
in
if Utils.debug_res then check_res res "demod result";
- let newmeta, newtarget =
+ let bag, newtarget =
match res with
| Some t ->
- let newmeta, newtarget = build_newtarget true t in
+ let bag, newtarget = build_newtarget bag true t in
(* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
if (Equality.is_weak_identity newtarget) (* || *)
(*Equality.meta_convertibility_eq target newtarget*) then
- newmeta, newtarget
+ bag, newtarget
else
- demodulation_equality bag ?from eq_uri newmeta env table newtarget
+ demodulation_equality bag ?from eq_uri env table newtarget
| None ->
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 ->
- let newmeta, newtarget = build_newtarget false t in
+ let bag, newtarget = build_newtarget bag false t in
if (Equality.is_weak_identity newtarget) ||
(Equality.meta_convertibility_eq target newtarget) then
- newmeta, newtarget
+ bag, newtarget
else
- demodulation_equality bag ?from eq_uri newmeta env table newtarget
+ demodulation_equality bag ?from eq_uri env table newtarget
| None ->
- newmeta, target
+ bag, target
in
(* newmeta, newtarget *)
- newmeta,newtarget
+ bag, newtarget
;;
(**
| C.Meta (i, l) -> res, lifted_term
| term ->
let termty, ugraph =
-(* C.Implicit None, ugraph *)
- CicTypeChecker.type_of_aux' metasenv context term ugraph
+ C.Implicit None, ugraph
+(* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
in
let candidates = get_candidates Unification table term in
+ (* List.iter (fun (_,e) -> debug_print (lazy (Equality.string_of_equality e))) candidates; *)
let r =
if subterms_only then
[]
index: its updated value is also returned
*)
let superposition_right bag
- ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
+ ?(subterms_only=false) eq_uri (metasenv, context, ugraph) table target=
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
if Utils.debug_metas then
ignore (check_target bag context target "superpositionright");
let metasenv' = newmetas in
- let maxmeta = ref newmeta in
let res1, res2 =
match ordering with
| U.Gt ->
in
(res left right), (res right left)
in
- let build_new ordering (bo, s, m, ug, eq_found) =
+ let build_new bag ordering (bo, s, m, ug, eq_found) =
if Utils.debug_metas then
ignore (check_target bag context (snd eq_found) "buildnew1" );
(s,(Equality.SuperpositionRight,
id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
in
- let newmeta, newequality =
+ let bag, newequality =
let left, right =
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 = (* Founif.filter s *) m in
let stat = (eq_ty, left, right, neworder) in
- let eq' =
+ let bag, eq' =
let w = Utils.compute_equality_weight stat in
Equality.mk_equality bag (w, newproof, stat, newmenv) in
if Utils.debug_metas then
ignore (check_target bag context eq' "buildnew3");
- let newm, eq' = Equality.fix_metas bag !maxmeta eq' in
+ let bag, eq' = Equality.fix_metas bag eq' in
if Utils.debug_metas then
ignore (check_target bag context eq' "buildnew4");
- newm, eq'
+ bag, eq'
in
- maxmeta := newmeta;
if Utils.debug_metas then
ignore(check_target bag context newequality "buildnew2");
- newequality
+ bag, newequality
+ in
+ let bag, new1 =
+ List.fold_right
+ (fun x (bag,acc) ->
+ let bag, e = build_new bag U.Gt x in
+ bag, e::acc) res1 (bag,[])
+ in
+ let bag, new2 =
+ List.fold_right
+ (fun x (bag,acc) ->
+ let bag, e = build_new bag U.Lt x in
+ bag, e::acc) res2 (bag,[])
in
- let new1 = List.map (build_new U.Gt) res1
- and new2 = List.map (build_new U.Lt) res2 in
let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
- (!maxmeta,
- (List.filter ok (new1 @ new2)))
+ bag, List.filter ok (new1 @ new2)
;;
(** demodulation, when the target is a theorem *)
;;
let rec demod bag env table goal =
- let goalproof,menv,t = goal in
+ let _,menv,t = goal in
let _, context, ugraph = env in
- let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:true)in
+ let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:false)in
match res with
| Some newt ->
let newg =
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 superposition_left bag (metasenv, context, ugraph) table goal =
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));
*)
-(*
- if expansionsl <> [] then prerr_endline "expansionl";
- if expansionsr <> [] then prerr_endline "expansionr";
-*)
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"; *)
+ | Utils.Gt ->
let big,small,possmall = l,r,Utils.Right in
let expansions, _ = betaexpand_term menv context ugraph table 0 big in
List.map
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,[])
+ (fun g (b,acc) ->
+ let b,g = Equality.fix_metas_goal b g in
+ b,g::acc)
+ newgoals (bag,[])
;;
(** demodulation, when the target is a goal *)
| 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 termty, ugraph = C.Implicit None, ugraph in
let res =
find_all_matches
- metasenv context ugraph lift_amount term termty candidates
+ ~unif_fun:Founif.matching ~demod:true
+ metasenv context ugraph lift_amount term termty candidates
in
match term with
| C.Appl l ->
- let res, _, _ =
+ 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
+ (fun (res,b,l,r) t ->
+ if not b then res,b,l,r
+ else
+ let demods_for_t =
+ demodulation_all_aux
+ metasenv context ugraph table lift_amount t
+ in
+ let b = demods_for_t = [] in
+ res @
+ List.map
+ (fun (rel, s, m, ug, c) ->
+ (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
+ demods_for_t, b, l@[List.hd r], List.tl r)
+ (res, true, [], 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 demod_all steps bag env table goal =
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]
+ let is_visited l (_,_,t) =
+ List.exists (fun (_,_,s) -> Equality.meta_convertibility s t) l
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))
+ let rec aux steps visited nf bag = function
+ | _ when steps = 0 -> visited, bag, nf
+ | [] -> visited, bag, nf
+ | goal :: rest when is_visited visited goal-> aux steps visited nf bag rest
+ | goal :: rest ->
+ let visited = goal :: visited in
+ let _,menv,t = goal in
+ let res = demodulation_all_aux menv context ugraph table 0 t in
+ let steps = if res = [] then steps-1 else steps in
+ let new_goals =
+ List.map (build_newg bag context goal Equality.Demodulation) res
+ in
+ let nf = if new_goals = [] then goal :: nf else nf in
+ aux steps visited nf bag (new_goals @ rest)
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
+ aux steps [] [] bag [goal]
+;;
+
+let combine_demodulation_proofs bag env goal (pl,ml,l) (pr,mr,r) =
+ let proof,m,eq,ty,left,right = open_goal goal in
+ let pl =
+ List.map
+ (fun (rule,pos,id,subst,pred) ->
+ let pred =
+ match pred with
+ | Cic.Lambda (name,src,tgt) ->
+ Cic.Lambda (name,src,
+ Cic.Appl[eq;ty;tgt;CicSubstitution.lift 1 right])
+ | _ -> assert false
+ in
+ rule,pos,id,subst,pred)
+ pl
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
+ let pr =
+ List.map
+ (fun (rule,pos,id,subst,pred) ->
+ let pred =
+ match pred with
+ | Cic.Lambda (name,src,tgt) ->
+ Cic.Lambda (name,src,
+ Cic.Appl[eq;ty;CicSubstitution.lift 1 l;tgt])
+ | _ -> assert false
+ in
+ rule,pos,id,subst,pred)
+ pr
+ in
+ (pr@pl@proof, m, Cic.Appl [eq;ty;l;r])
+;;
+
+let demodulation_all_goal bag env table goal maxnf =
+ let proof,menv,eq,ty,left,right = open_goal goal in
+ let v1, bag, l_demod = demod_all maxnf bag env table ([],menv,left) in
+ let v2, bag, r_demod = demod_all maxnf bag env table ([],menv,right) in
+ let l_demod = if l_demod = [] then [ [], menv, left ] else l_demod in
+ let r_demod = if r_demod = [] then [ [], menv, right ] else r_demod in
+ List.fold_left
+ (fun acc (_,_,l as ld) ->
+ List.fold_left
+ (fun acc (_,_,r as rd) ->
+ combine_demodulation_proofs bag env goal ld rd :: acc)
+ acc r_demod)
+ [] l_demod
+;;
+
+let solve_demodulating bag env table initgoal steps =
+ let proof,menv,eq,ty,left,right = open_goal initgoal in
+ let uri =
+ match eq with
+ | Cic.MutInd (u,_,_) -> u
+ | _ -> assert false
+ in
+ let _, context, ugraph = env in
+ let v1, bag, l_demod = demod_all steps bag env table ([],menv,left) in
+ let v2, bag, r_demod = demod_all steps bag env table ([],menv,right) in
+ let is_solved left right ml mr =
+ let m = ml @ (List.filter
+ (fun (x,_,_) -> not (List.exists (fun (y,_,_) -> x=y)ml)) mr)
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)
+ try
+ let s,_,_ =
+ Founif.unification [] m context left right CicUniv.empty_ugraph in
+ Some (bag, m,s,Equality.Exact (Equality.refl_proof uri ty left))
+ with CicUnification.UnificationFailure _ ->
+ let solutions =
+ unification_all env table (Equality.mk_tmp_equality
+ (0,(Cic.Implicit None,left,right,Utils.Incomparable),m))
+ in
+ if solutions = [] then None
+ else
+ let s, e, swapped = List.hd solutions in
+ let _,p,(ty,l,r,_),me,id = Equality.open_equality e in
+ let bag, p =
+ if swapped then Equality.symmetric bag ty l id uri me else bag, p
+ in
+ Some (bag, m,s, p)
in
- aux steps L initgoal
+ let newgoal =
+ HExtlib.list_findopt
+ (fun (pr,mr,r) _ ->
+ try
+ let pl,ml,l,bag,m,s,p =
+ match
+ HExtlib.list_findopt (fun (pl,ml,l) _ ->
+ match is_solved l r ml mr with
+ | None -> None
+ | Some (bag,m,s,p) -> Some (pl,ml,l,bag,m,s,p)
+ ) l_demod
+ with Some x -> x | _ -> raise Not_found
+ in
+ let pl =
+ List.map
+ (fun (rule,pos,id,subst,pred) ->
+ let pred =
+ match pred with
+ | Cic.Lambda (name,src,tgt) ->
+ Cic.Lambda (name,src,
+ Cic.Appl[eq;ty;tgt;CicSubstitution.lift 1 right])
+ | _ -> assert false
+ in
+ rule,pos,id,subst,pred)
+ pl
+ in
+ let pr =
+ List.map
+ (fun (rule,pos,id,subst,pred) ->
+ let pred =
+ match pred with
+ | Cic.Lambda (name,src,tgt) ->
+ Cic.Lambda (name,src,
+ Cic.Appl[eq;ty;CicSubstitution.lift 1 l;tgt])
+ | _ -> assert false
+ in
+ rule,pos,id,subst,pred)
+ pr
+ in
+ Some (bag,pr@pl@proof,m,s,p)
+ with Not_found -> None)
+ r_demod
+ in
+ newgoal
;;
-let get_stats () = "" ;;
+
+
projects / helm.git / blobdiff