let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
let cmp = !Utils.compare_terms in
+ ignore(CicTypeChecker.type_of_aux' metasenv context term);
let check = match termty with C.Implicit None -> false | _ -> true in
function
| [] -> None
let t2 = Unix.gettimeofday () in
match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
r
- with Inference.MatchingFailure as e ->
+ with
+ | Inference.MatchingFailure as e ->
let t2 = Unix.gettimeofday () in
match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
- raise e
+ raise e
+ | CicUtil.Meta_not_found _ as exn ->
+ prerr_endline "siam qua"; raise exn
in
Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
(candidate, eq_URI))
let module HL = HelmLibraryObjects in
let module U = Utils in
let metasenv, context, ugraph = env in
- let _, proof, (eq_ty, left, right, order), metas, args = target in
+ let w, proof, (eq_ty, left, right, order), metas, args = target in
+ (* first, we simplify *)
+ let right = U.guarded_simpl context right in
+ let left = U.guarded_simpl context left in
+ let w = Utils.compute_equality_weight eq_ty left right in
+ let order = !Utils.compare_terms left right in
+ let target = w, proof, (eq_ty, left, right, order), metas, args in
+
let metasenv' = metasenv @ metas in
let maxmeta = ref newmeta in
in
let left, right = if is_left then newterm, right else left, newterm in
let m = (Inference.metas_of_term left) @ (Inference.metas_of_term right) in
- let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv')
+ (* let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv') *)
+ let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metasenv' @ menv')
and newargs = args
in
let ordering = !Utils.compare_terms left right in
match res with
| Some t ->
let newmeta, newtarget = build_newtarget true t in
- if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
+ if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
(Inference.meta_convertibility_eq target newtarget) then
newmeta, newtarget
else
match res with
| Some t ->
let newmeta, newtarget = build_newtarget false t in
- if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
+ if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
(Inference.meta_convertibility_eq target newtarget) then
newmeta, newtarget
else
newmeta, target
in
(* newmeta, newtarget *)
- (* tentiamo di normalizzare *)
- let w, p, (ty, left, right, o), m, a = newtarget in
- let left = U.guarded_simpl context left in
- let right = U.guarded_simpl context right in
- let w' = Utils.compute_equality_weight ty left right in
- let o' = !Utils.compare_terms left right in
- newmeta, (w', p, (ty, left, right, o'), m, a)
+ newmeta,newtarget
;;
in
let new1 = List.map (build_new U.Gt) res1
and new2 = List.map (build_new U.Lt) res2 in
+(*
let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in
+*)
+ let ok e = not (Inference.is_identity (metasenv', context, ugraph) e) in
(!maxmeta,
(List.filter ok (new1 @ new2)))
;;
let metasenv, context, ugraph = env in
let maxmeta = ref newmeta in
let proof, metas, term = goal in
+ let term = Utils.guarded_simpl (~debug:true) context term in
+ let goal = proof, metas, term 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
bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
in
let m = Inference.metas_of_term newterm in
- let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
+ let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv')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
- begin
- Printf.eprintf "reducing %s to %s \n"
- (CicPp.ppterm term) (CicPp.ppterm newg);
- demodulation_goal newmeta env table newgoal
- end
+ demodulation_goal newmeta env table newgoal
| None ->
newmeta, goal
;;
in
let m = Inference.metas_of_term newterm in
- let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
+ let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv') in
!maxmeta, (newterm, newty, newmetasenv)
in
let res =
newmeta, theorem
;;
-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 = 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, [], ty in
- let equalities = equalities @ library_equalities in
- let table =
- List.fold_left
- (fun tbl eq -> index tbl eq)
- empty equalities
- in
- let newmeta,(newproof,newmetasenv, newty) = demodulation_goal
- maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal
- in
- 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