let other' = U.guarded_simpl context (apply_subst s other) in *)
let other' = apply_subst s other in
let order = cmp c' other' in
- let names = U.names_of_context context in
if order = U.Gt then
res
else
let c' = apply_subst s c
and other' = apply_subst s other in
let order = cmp c' other' in
- let names = U.names_of_context context in
if order <> U.Lt && order <> U.Le then
res::(find_all_matches ~unif_fun metasenv context ugraph
lift_amount term termty tl)
let rec demodulation_aux ?(typecheck=false)
metasenv context ugraph table lift_amount term =
+ (* Printf.eprintf "term = %s\n" (CicPp.ppterm term); *)
+
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
let newgoal, newproof =
(* qua *)
let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in
- let t' =
- let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
- incr sup_r_counter;
- let l, r =
- if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
- (name, ty, S.lift 1 eq_ty, l, r)
- in
let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
incr sup_r_counter;
let bo'' =
and newargs = args @ args' in
let eq' =
let w = Utils.compute_equality_weight eq_ty left right in
- (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs)
- and env = (metasenv, context, ugraph) in
+ (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs) in
let newm, eq' = Inference.fix_metas !maxmeta eq' in
newm, eq'
in
let maxmeta = ref newmeta in
let proof, metas, term = goal in
let metasenv' = metasenv @ metas in
+ Printf.eprintf "siam qua\n";
let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
| Inference.ProofGoalBlock (_, parent_proof) ->
(* debug_print (lazy "replacing another ProofGoalBlock"); *)
Inference.ProofGoalBlock (pb, parent_proof)
- | (Inference.SubProof (term, meta_index, p) as subproof) ->
-(* debug_print *)
-(* (lazy *)
-(* (Printf.sprintf "replacing %s" *)
-(* (Inference.string_of_proof subproof))); *)
+ | Inference.SubProof (term, meta_index, p) ->
Inference.SubProof (term, meta_index, repl p)
| _ -> assert false
in repl proof
let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
!maxmeta, (newproof, newmetasenv, newterm)
in
+ Printf.eprintf "bum0\n";
let res =
demodulation_aux ~typecheck:true metasenv' context ugraph table 0 term
in
+ Printf.eprintf "bum\n";
match res with
| Some t ->
let newmeta, newgoal = build_newgoal t in
if Inference.meta_convertibility term newg then
newmeta, newgoal
else
- demodulation_goal newmeta env table newgoal
+ begin
+ Printf.eprintf "reducing %s to %s \n"
+ (CicPp.ppterm term) (CicPp.ppterm newg);
+ demodulation_goal newmeta env table newgoal
+ end
| None ->
newmeta, goal
;;
let module HL = HelmLibraryObjects in
let metasenv, context, ugraph = env in
let maxmeta = ref newmeta in
- let proof, metas, term = theorem in
let term, termty, metas = theorem in
let metasenv' = metasenv @ metas in
-
+
let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
let what, other = if pos = Utils.Left then what, other else other, what in
Inference.BasicProof term)
in
(Inference.build_proof_term newproof, bo)
- in
+ in
+
let m = Inference.metas_of_term newterm in
let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
!maxmeta, (newterm, newty, newmetasenv)
let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) =
let module I = Inference in
let curi,metasenv,pbo,pty = proof in
- let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let eq_indexes, equalities, maxm = I.find_equalities context proof in
let lib_eq_uris, library_equalities, maxm =
I.find_library_equalities dbd context (proof, goal) (maxm+2) in
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
let library_equalities = List.map snd library_equalities in
let goalterm = Cic.Meta (metano,irl) in
- let initgoal = Inference.BasicProof goalterm, [], goalterm in
+ let initgoal = Inference.BasicProof goalterm, [], ty in
let equalities = equalities @ library_equalities in
let table =
List.fold_left
(fun tbl eq -> index tbl eq)
empty equalities
in
- let _,(newproof, newty, newmetasenv) = demodulation_goal
+ let newmeta,(newproof,newmetasenv, newty) = demodulation_goal
maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal
in
- let proofterm = Inference.build_proof_term newproof in
- ProofEngineTypes.apply_tactic
- (PrimitiveTactics.apply_tac ~term:proofterm)
- initialstatus
+ if newmeta != maxm then
+ begin
+ let opengoal = Cic.Meta(maxm,irl) in
+ let proofterm =
+ Inference.build_proof_term ~noproof:opengoal newproof in
+ prerr_endline ("proffterm ="^(CicMetaSubst.ppterm_in_context [] proofterm context));
+ let extended_metasenv = (maxm,context,newty)::metasenv in
+ prerr_endline ("metasenv ="^(CicMetaSubst.ppmetasenv [] extended_metasenv));
+ let extended_status =
+ (curi,extended_metasenv,pbo,pty),goal in
+ let (status,newgoals) =
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.apply_tac ~term:proofterm)
+ extended_status in
+ (status,maxm::newgoals)
+ end
+ else raise (ProofEngineTypes.Fail (lazy "no progress"))
let demodulate_tac ~dbd ~pattern =
ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern)
projects / helm.git / blobdiff