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
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 module S = CicSubstitution in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
- 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
| 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 rec demod bag env table goal =
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 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
- ~unif_fun:Founif.matching
+ ~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
| t -> res
let is_visited l (_,_,t) =
List.exists (fun (_,_,s) -> Equality.meta_convertibility s t) l
in
- let rec aux steps visited bag = function
- | _ when steps = 0 -> visited, bag, []
- | [] -> visited, bag, []
- | goal :: rest when is_visited visited goal -> aux steps visited bag rest
+ 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 new_goals =
List.map (build_newg bag context goal Equality.Demodulation) res
in
- (* we need this cause an equation E like
- F ?x => F ?y
- can add a meta for y in a goal without instantiating it
- P (F true) ----> P (F ?y)
- and this may cause duplicated in metasenvs
- demodulating again with E
- *)
- let bag, new_goals =
- List.fold_right
- (fun g (bag,acc) ->
- let bag, g = Equality.fix_metas_goal bag g in
- bag, g::acc)
- new_goals (bag,[])
+ let nf = if new_goals = [] then goal :: nf else nf in
+ aux steps visited nf bag (new_goals @ rest)
+ in
+ 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
- let visited, bag, res = aux steps visited bag (new_goals @ rest) in
- visited, bag, goal :: res
+ rule,pos,id,subst,pred)
+ pl
in
- aux steps [] bag [goal]
+ 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
projects / helm.git / blobdiff