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) =
- 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)
Index.t ->
Cic.term * Index.key * Cic.metasenv ->
'a * (Cic.term * Index.key * Cic.metasenv)
-val demodulate_tac:
- dbd:HMysql.dbd ->
- pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
+
try
unification metasenv context t1 t2 ugraph
with CicUtil.Meta_not_found _ as exn ->
- Printf.eprintf "t1 = %s\nt2 = %s\nmetasenv = %s\n%!"
+ Printf.eprintf "t1 == %s\nt2 = %s\nmetasenv == %s\n%!"
(CicPp.ppterm t1) (CicPp.ppterm t2) (CicMetaSubst.ppmetasenv [] metasenv);
raise exn
in
type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
+let is_weak_identity (metasenv, context, ugraph) = function
+ | (_, _, (ty, left, right, _), menv, _) ->
+ (left = right ||
+ (meta_convertibility left right))
+ (* the test below is not a good idea since it stops
+ demodulation too early *)
+ (* (fst (CicReduction.are_convertible
+ ~metasenv:(metasenv @ menv) context left right ugraph)))*)
+;;
let is_identity (metasenv, context, ugraph) = function
| (_, _, (ty, left, right, _), menv, _) ->
(left = right ||
- (* (meta_convertibility left right) || *)
- (fst (CicReduction.are_convertible
+ (* (meta_convertibility left right)) *)
+ (fst (CicReduction.are_convertible
~metasenv:(metasenv @ menv) context left right ugraph)))
;;
(** meta convertibility between two equations *)
val meta_convertibility_eq: equality -> equality -> bool
+val is_weak_identity: environment -> equality -> bool
val is_identity: environment -> equality -> bool
val string_of_equality: ?env:environment -> equality -> string
;;
+let rec simpl env e others others_simpl =
+ let active = others @ others_simpl in
+ let tbl =
+ List.fold_left
+ (fun t (_, e) -> Indexing.index t e)
+ Indexing.empty active
+ in
+ let res = forward_simplify env e (active, tbl) in
+ match others with
+ | hd::tl -> (
+ match res with
+ | None -> simpl env hd tl others_simpl
+ | Some e -> simpl env hd tl (e::others_simpl)
+ )
+ | [] -> (
+ match res with
+ | None -> others_simpl
+ | Some e -> e::others_simpl
+ )
+;;
+
+let simplify_equalities env equalities =
+ debug_print
+ (lazy
+ (Printf.sprintf "equalities:\n%s\n"
+ (String.concat "\n"
+ (List.map string_of_equality equalities))));
+ debug_print (lazy "SIMPLYFYING EQUALITIES...");
+ match equalities with
+ | [] -> []
+ | hd::tl ->
+ let others = List.map (fun e -> (Positive, e)) tl in
+ let res =
+ List.rev (List.map snd (simpl env (Positive, hd) others []))
+ in
+ debug_print
+ (lazy
+ (Printf.sprintf "equalities AFTER:\n%s\n"
+ (String.concat "\n"
+ (List.map string_of_equality res))));
+ res
+;;
+
(* applies equality to goal to see if the goal can be closed *)
let apply_equality_to_goal env equality goal =
let module C = Cic in
in
(*try*)
let goal = Inference.BasicProof new_meta_goal, [], goal in
- let equalities =
- let equalities = equalities @ library_equalities in
- debug_print
- (lazy
- (Printf.sprintf "equalities:\n%s\n"
- (String.concat "\n"
- (List.map string_of_equality equalities))));
- debug_print (lazy "SIMPLYFYING EQUALITIES...");
- let rec simpl e others others_simpl =
- let active = others @ others_simpl in
- let tbl =
- List.fold_left
- (fun t (_, e) -> Indexing.index t e)
- Indexing.empty active
- in
- let res = forward_simplify env e (active, tbl) in
- match others with
- | hd::tl -> (
- match res with
- | None -> simpl hd tl others_simpl
- | Some e -> simpl hd tl (e::others_simpl)
- )
- | [] -> (
- match res with
- | None -> others_simpl
- | Some e -> e::others_simpl
- )
- in
- match equalities with
- | [] -> []
- | hd::tl ->
- let others = List.map (fun e -> (Positive, e)) tl in
- let res =
- List.rev (List.map snd (simpl (Positive, hd) others []))
- in
- debug_print
- (lazy
- (Printf.sprintf "equalities AFTER:\n%s\n"
- (String.concat "\n"
- (List.map string_of_equality res))));
- res
- in
+ let equalities = simplify_equalities env (equalities@library_equalities) in
let active = make_active () in
let passive = make_passive [] equalities in
Printf.printf "\ncurrent goal: %s\n"
let library_equalities = List.map snd library_equalities in
let t2 = Unix.gettimeofday () in
maxmeta := maxm+2;
- let equalities =
- let equalities = equalities @ library_equalities in
- debug_print
- (lazy
- (Printf.sprintf "equalities:\n%s\n"
- (String.concat "\n"
- (List.map string_of_equality equalities))));
- debug_print (lazy "SIMPLYFYING EQUALITIES...");
- let rec simpl e others others_simpl =
- let active = others @ others_simpl in
- let tbl =
- List.fold_left
- (fun t (_, e) -> Indexing.index t e)
- Indexing.empty active
- in
- let res = forward_simplify env e (active, tbl) in
- match others with
- | hd::tl -> (
- match res with
- | None -> simpl hd tl others_simpl
- | Some e -> simpl hd tl (e::others_simpl)
- )
- | [] -> (
- match res with
- | None -> others_simpl
- | Some e -> e::others_simpl
- )
- in
- match equalities with
- | [] -> []
- | hd::tl ->
- let others = List.map (fun e -> (Positive, e)) tl in
- let res =
- List.rev (List.map snd (simpl (Positive, hd) others []))
- in
- debug_print
- (lazy
- (Printf.sprintf "equalities AFTER:\n%s\n"
- (String.concat "\n"
- (List.map string_of_equality res))));
- res
- in
+ let equalities = simplify_equalities env (equalities@library_equalities) in
debug_print
(lazy
(Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)));
let env = (metasenv, context, ugraph) in
(*try*)
let goal = Inference.BasicProof new_meta_goal, [], goal in
- let equalities =
- let equalities = equalities @ library_equalities in
- debug_print
- (lazy
- (Printf.sprintf "equalities:\n%s\n"
- (String.concat "\n"
- (List.map string_of_equality equalities))));
- debug_print (lazy "SIMPLYFYING EQUALITIES...");
- let rec simpl e others others_simpl =
- let active = others @ others_simpl in
- let tbl =
- List.fold_left
- (fun t (_, e) -> Indexing.index t e)
- Indexing.empty active
- in
- let res = forward_simplify env e (active, tbl) in
- match others with
- | hd::tl -> (
- match res with
- | None -> simpl hd tl others_simpl
- | Some e -> simpl hd tl (e::others_simpl)
- )
- | [] -> (
- match res with
- | None -> others_simpl
- | Some e -> e::others_simpl
- )
- in
- match equalities with
- | [] -> []
- | hd::tl ->
- let others = List.map (fun e -> (Positive, e)) tl in
- let res =
- List.rev (List.map snd (simpl (Positive, hd) others []))
- in
- debug_print
- (lazy
- (Printf.sprintf "equalities AFTER:\n%s\n"
- (String.concat "\n"
- (List.map string_of_equality res))));
- res
- in
+ let equalities = simplify_equalities env (equalities@library_equalities) in
let active = make_active () in
let passive = make_passive [] equalities in
Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e)))
*)
;;
+
+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
+ if library_equalities = [] then prerr_endline "VUOTA!!!";
+ 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 env = (metasenv, context, CicUniv.empty_ugraph) in
+ let equalities = simplify_equalities env (equalities@library_equalities) in
+ let table =
+ List.fold_left
+ (fun tbl eq -> Indexing.index tbl eq)
+ Indexing.empty equalities
+ in
+ let newmeta,(newproof,newmetasenv, newty) = Indexing.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
+ let extended_metasenv = (maxm,context,newty)::metasenv in
+ 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 if newty = ty then
+ raise (ProofEngineTypes.Fail (lazy "no progress"))
+ else ProofEngineTypes.apply_tactic
+ (ReductionTactics.simpl_tac ~pattern)
+ initialstatus
+;;
+
+let demodulate_tac ~dbd ~pattern =
+ ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern)
+;;
Cic.term -> Cic.conjecture list -> CicUniv.universe_graph -> unit
val main: HMysql.dbd ->
bool -> Cic.term -> Cic.conjecture list -> CicUniv.universe_graph -> unit
+val demodulate_tac:
+ dbd:HMysql.dbd ->
+ pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
(* $Id$ *)
-let debug = true;;
+let debug = false;;
let debug_print s = if debug then prerr_endline (Lazy.force s);;
HelmLibraryObjects.Peano.pred_URI, 12;
HelmLibraryObjects.Peano.plus_URI, 15;
HelmLibraryObjects.Peano.minus_URI, 18;
- HelmLibraryObjects.Peano.mult_URI, 21
+ HelmLibraryObjects.Peano.mult_URI, 21;
+ UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind#xpointer(1/1)",103;
+ UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)",106;
+ UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)",109;
+ UriManager.uri_of_string "cic:/matita/nat/nat/pred.con",112;
+ UriManager.uri_of_string "cic:/matita/nat/plus/plus.con",115;
+ UriManager.uri_of_string "cic:/matita/nat/minus/minus.con",118;
+ UriManager.uri_of_string "cic:/matita/nat/times/times.con",121;
]
;;
match t with
Cic.Const _
| Cic.MutInd _
- | Cic.MutConstruct _ -> true
+ | Cic.MutConstruct _
+ | Cic.Rel _ -> true
| _ -> false
-let sig_order t1 t2 =
+let sig_order_const t1 t2 =
try
let u1 = CicUtil.uri_of_term t1 in
let u2 = CicUtil.uri_of_term t2 in
Invalid_argument _
| Not_found -> Incomparable
-let rec rpo t1 t2 =
+let sig_order t1 t2 =
+ match t1, t2 with
+ Cic.Rel n, Cic.Rel m when n < m -> Gt (* inverted order *)
+ | Cic.Rel n, Cic.Rel m when n = m -> Incomparable
+ | Cic.Rel n, Cic.Rel m when n > m -> Lt
+ | Cic.Rel _, _ -> Gt
+ | _, Cic.Rel _ -> Lt
+ | _,_ -> sig_order_const t1 t2
+
+let rec rpo_lt t1 t2 =
let module C = Cic in
- match t1,t2 with
- C.Meta (_, _), C.Meta (_,_) -> Incomparable
- | C.Meta (_,_) as t1,t2 when TermSet.mem t1 (metas_of_term t2)
- -> Lt
- | t1, (C.Meta (_,_) as t2) when TermSet.mem t2 (metas_of_term t1)
- -> Gt
- | C.Appl (h1::arg1),C.Appl (h2::arg2) when h1=h2 ->
- (match lex arg1 arg2 with
- | Lt when (check Gt t2 arg1) -> Lt
- | Gt when (check Gt t1 arg2) -> Gt
- | _ -> Incomparable )
- | C.Appl (h1::arg1),C.Appl (h2::arg2) ->
- (match sig_order h1 h2 with
- | Lt when (check Gt t2 arg1) -> Lt
- | Gt when (check Gt t1 arg2) -> Gt
- | _ -> Incomparable )
- | C.Appl (h1::arg1), t2 when atomic t2 ->
- (match sig_order h1 t2 with
- | Lt when (check Gt t2 arg1) -> Lt
- | Gt -> Gt
- | _ -> Incomparable )
- | t1 , C.Appl (h2::arg2) when atomic t1 ->
- (match sig_order t1 h2 with
- | Lt -> Lt
- | Gt when (check Gt t1 arg2) -> Gt
- | _ -> Incomparable )
- | C.Appl [] , _ -> assert false
- | _ , C.Appl [] -> assert false
- | _,_ -> Incomparable
-
-and lex l1 l2 =
+ let first_trie =
+ match t1,t2 with
+ C.Meta (_, _), C.Meta (_,_) -> false
+ | C.Meta (_,_) , t2 -> TermSet.mem t1 (metas_of_term t2)
+ | t1, C.Meta (_,_) -> false
+ | C.Appl [h1;a1],C.Appl [h2;a2] when h1=h2 ->
+ rpo_lt a1 a2
+ | C.Appl (h1::arg1),C.Appl (h2::arg2) when h1=h2 ->
+ if lex_lt arg1 arg2 then
+ check_lt arg1 t2
+ else false
+ | C.Appl (h1::arg1),C.Appl (h2::arg2) ->
+ (match sig_order h1 h2 with
+ | Lt -> check_lt arg1 t2
+ | _ -> false)
+ | C.Appl (h1::arg1), t2 when atomic t2 ->
+ (match sig_order h1 t2 with
+ | Lt -> check_lt arg1 t2
+ | _ -> false)
+ | t1 , C.Appl (h2::arg2) when atomic t1 ->
+ (match sig_order t1 h2 with
+ | Lt -> true
+ | _ -> false )
+ | C.Appl [] , _ -> assert false
+ | _ , C.Appl [] -> assert false
+ | t1, t2 when (atomic t1 && atomic t2 && t1<>t2) ->
+ (match sig_order t1 t2 with
+ | Lt -> true
+ | _ -> false)
+ | _,_ -> false
+ in
+ if first_trie then true else
+ match t2 with
+ C.Appl (_::args) ->
+ List.exists (fun a -> t1 = a || rpo_lt t1 a) args
+ | _ -> false
+
+and lex_lt l1 l2 =
match l1,l2 with
- [],[] -> Incomparable
+ [],[] -> false
| [],_ -> assert false
| _, [] -> assert false
- | a1::l1, a2::l2 when a1 = a2 -> lex l1 l2
- | a1::_, a2::_ -> rpo a1 a2
-
-and check o t l =
+ | a1::l1, a2::l2 when a1 = a2 -> lex_lt l1 l2
+ | a1::_, a2::_ -> rpo_lt a1 a2
+
+and check_lt l t =
List.fold_left
- (fun b a -> b && (rpo t a = o))
+ (fun b a -> b && (rpo_lt a t))
true l
;;
+let rpo t1 t2 =
+ if rpo_lt t2 t1 then Gt
+ else if rpo_lt t1 t2 then Lt
+ else Incomparable
+
(*********************** fine rpo *****************************)
(* settable by the user... *)
-let compare_terms = ref nonrec_kbo;;
+(* let compare_terms = ref nonrec_kbo;; *)
(* let compare_terms = ref ao;; *)
-(* let compare_terms = ref rpo;; *)
+let compare_terms = ref rpo;;
-let guarded_simpl context t = t
-(*
+let guarded_simpl ?(debug=false) context t =
let t' = ProofEngineReduction.simpl context t in
- let simpl_order = !compare_terms t t' in
- if simpl_order = Gt then
- (* prerr_endline ("reduce: "^(CicPp.ppterm t)^(CicPp.ppterm t')); *)
- t'
- else t *)
+ if t = t' then t else
+ begin
+ let simpl_order = !compare_terms t t' in
+ if debug then
+ prerr_endline ("comparing "^(CicPp.ppterm t)^(CicPp.ppterm t'));
+ if simpl_order = Gt then (if debug then prerr_endline "GT";t')
+ else (if debug then prerr_endline "NO_GT";t)
+ end
;;
type equality_sign = Negative | Positive;;
(** term-ordering function settable by the user *)
val compare_terms: (Cic.term -> Cic.term -> comparison) ref
-val guarded_simpl: Cic.context -> Cic.term -> Cic.term
+val guarded_simpl: ?debug:bool -> Cic.context -> Cic.term -> Cic.term
type equality_sign = Negative | Positive
projects / helm.git / commitdiff