as above, but finds all the matching equalities, and the matching condition
can be either Founif.matching or 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
(*
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
in
let leftr =
match left with
- | Cic.Meta _ when not use_unification -> []
+ | Cic.Meta _ (*when not use_unification*) -> []
| _ ->
let leftc = get_candidates predicate table left in
find_all_matches ~unif_fun
in
let rightr =
match right with
- | Cic.Meta _ when not use_unification -> []
+ | Cic.Meta _ (*when not use_unification*) -> []
| _ ->
let rightc = get_candidates predicate table right in
find_all_matches ~unif_fun
(** 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 module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
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 =
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' =
;;
(** demodulation, when the target is a theorem *)
-let rec demodulation_theorem bag newmeta env table theorem =
+let rec demodulation_theorem bag env table theorem =
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
+ let eq_uri =
+ match LibraryObjects.eq_URI() with
+ | Some u -> u
+ | None -> assert false in
let metasenv, context, ugraph = env in
- let maxmeta = ref newmeta in
- let term, termty, metas = theorem in
- let metasenv' = metas in
-
+ let proof, theo, metas = theorem in
let build_newtheorem (t, subst, menv, ug, eq_found) =
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, newty =
- let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
-(* let bo' = apply_subst subst t in *)
-(* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
-(*
- let newproofold =
- Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
- Equality.BasicProof (Equality.empty_subst,term))
- in
- (Equality.build_proof_term_old newproofold, bo)
-*)
- (* TODO, not ported to the new proofs *)
- if true then assert false; term, bo
- in
- !maxmeta, (newterm, newty, menv)
- in
- let res =
- demodulation_aux bag (* ~typecheck:true *) metasenv' context ugraph table 0 termty
+ let peq =
+ match proof' with
+ | Equality.Exact p -> p
+ | _ -> assert false in
+ let what, other =
+ if pos = Utils.Left then what, other else other, what in
+ let newtheo = apply_subst subst (S.subst other t) in
+ let name = C.Name "x" in
+ let body = apply_subst subst t in
+ let pred = C.Lambda(name,ty,body) in
+ let newproof =
+ match pos with
+ | Utils.Left ->
+ Equality.mk_eq_ind eq_uri ty what pred proof other peq
+ | Utils.Right ->
+ Equality.mk_eq_ind eq_uri ty what pred proof other peq
+ in
+ newproof,newtheo
in
+ let res = demodulation_aux bag metas context ugraph table 0 theo in
match res with
| Some t ->
- let newmeta, newthm = build_newtheorem t in
- let newt, newty, _ = newthm in
- if Equality.meta_convertibility termty newty then
- newmeta, newthm
+ let newproof, newtheo = build_newtheorem t in
+ if Equality.meta_convertibility theo newtheo then
+ newproof, newtheo
else
- demodulation_theorem bag newmeta env table newthm
+ demodulation_theorem bag env table (newproof,newtheo,[])
| None ->
- newmeta, theorem
+ proof,theo
;;
(*****************************************************************************)
Utils.guarded_simpl context
(apply_subst subst (CicSubstitution.subst other t))
in
- let bo' = (*apply_subst subst*) t in
- (* patch??
- let bo' = t in
- let ty = apply_subst subst ty 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)
| 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