let eqP = assert false;;
+ let is_eq = assert false;;
+
let saturate = assert false;;
end
aux (aux [] ty) proofterm
in
let lit =
- match ty with
- | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
+ match B.is_eq ty with
+ | Some(ty,l,r) ->
let o = Order.compare_terms l r in
Terms.Equation (l, r, ty, o)
- | t -> Terms.Predicate t
+ | None -> Terms.Predicate ty
in
let proof = Terms.Exact proofterm in
fresh_unit_clause maxvar (0, lit, varlist, proof)
NCic.Const ref
;;
+let equivalence_relation =
+ let uri = NUri.uri_of_string "cic:/matita/ng/properties/relations/eq_rel.con"
+ in
+ let ref = NReference.reference_of_spec uri (NReference.Fix(0,1,2))
+ in NCic.Const ref
+
+let setoid_eq =
+ let uri = NUri.uri_of_string "cic:/matita/ng/sets/setoids/eq.con" in
+ let ref = NReference.reference_of_spec uri (NReference.Fix(0,0,2))
+ in NCic.Const ref
+
let set_default_eqP() = eqPref := default_eqP
let set_reference_of_oxuri f =
let eq x y = x = y;;
(* NCicReduction.alpha_eq C.metasenv C.subst C.context x y;; *)
+ let height_of_ref = function
+ | NReference.Def h -> h
+ | NReference.Fix(_,_,h) -> h
+ | _ -> 0
+
+ let compare_refs (NReference.Ref (u1,r1)) (NReference.Ref (u2,r2)) =
+ let x = height_of_ref r2 - height_of_ref r1 in
+ if x = 0 then
+ Hashtbl.hash (NUri.string_of_uri u1,r1) -
+ Hashtbl.hash (NUri.string_of_uri u2,r2)
+ else x
+
let rec compare x y =
match x,y with
| NCic.Rel i, NCic.Rel j -> j-i
| NCic.Meta (i,_), NCic.Meta (j,_) -> i-j
- | NCic.Const r1, NCic.Const r2 -> NReference.compare r1 r2
+ | NCic.Const r1, NCic.Const r2 -> compare_refs r1 r2
+ (*NReference.compare r1 r2*)
| NCic.Appl l1, NCic.Appl l2 -> FoUtils.lexicograph compare l1 l2
| NCic.Rel _, ( NCic.Meta _ | NCic.Const _ | NCic.Appl _ ) -> ~-1
| ( NCic.Meta _ | NCic.Const _ | NCic.Appl _ ), NCic.Rel _ -> 1
else compare x y
;;
+ let eqP = (!eqPref)()
+ ;;
+
+ let is_eq = function
+ | Terms.Node [ Terms.Leaf eqt ; ty; l; r ] when eq eqP eqt ->
+ Some (ty,l,r)
+ | Terms.Node [ Terms.Leaf eqt ; _; Terms.Node [Terms.Leaf eqt2 ; ty]; l; r]
+ when eq equivalence_relation eqt && eq setoid_eq eqt2 ->
+ Some (ty,l,r)
+ | _ -> None
+
let pp t =
NCicPp.ppterm ~context:C.context ~metasenv:C.metasenv ~subst:C.subst t;;
proof, sty
;;
- let eqP = (!eqPref)()
- ;;
-
end
let bag,clause = P.mk_passive bag (t,ty) in
if Terms.is_eq_clause clause then
P.forward_infer_step (P.replace_bag s bag) clause 0
- else (prerr_endline "not eq"; s)
+ else (debug (lazy "not eq"); s)
;;
let index_obj s uri =
let obj = NCicEnvironment.get_checked_obj uri in
+ debug (lazy ("indexing : " ^ (NUri.string_of_uri uri)));
+ debug (lazy ("no : " ^ (string_of_int (fst (Obj.magic uri)))));
match obj with
| (_,d,[],[],NCic.Constant(_,_,Some(_),ty,_)) ->
let nref = NReference.reference_of_spec uri (NReference.Def d) in
NCic.Lambda("x", hole_type, aux ft (List.rev p1))
;;
+(*
+ let mk_morphism eq amount ft p1 vl =
+ let rec aux t p =
+ match p with
+ | [] -> eq
+ | n::tl ->
+ match t with
+ | Terms.Leaf _
+ | Terms.Var _ -> assert false
+ | Terms.Node l ->
+ let dag,arity = ____ in
+ let l =
+ HExtlib.list_rev_mapi_filter
+ (fun t i ->
+ if i < arity then None
+ else if i = n then Some (aux t tl)
+ else Some (NCic.Appl [refl ...]))
+ l
+ in
+ NCic.Appl (dag::l)
+ in aux ft (List.rev pl)
+ ;;
+*)
+
let mk_proof (bag : NCic.term Terms.bag) mp subst steps =
let module Subst = FoSubst in
let position i l =
else
l,r,eq_ind ()
in
- NCic.LetIn ("clause_" ^ string_of_int id,
- close_with_forall vl (extract amount vl lit),
+ let body = aux ongoal
+ ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl
+ in
+ if NCicUntrusted.count_occurrences [] 0 body <= 1 then
+ NCicSubstitution.subst
+ ~avoid_beta_redexes:true ~no_implicit:false
+ (close_with_lambdas vl (NCic.Appl
+ [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]))
+ body
+ else
+ NCic.LetIn ("clause_" ^ string_of_int id,
+ close_with_forall vl (extract amount vl lit),
(* NCic.Implicit `Type, *)
- close_with_lambdas vl
- (NCic.Appl [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]),
- aux ongoal
- ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
+ close_with_lambdas vl (NCic.Appl
+ [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]),
+ body)
in
aux false [] steps, proof_type
;;
(* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
-(* let debug s = prerr_endline (Lazy.force s) ;; *)
-let debug _ = ();;
+let print s = prerr_endline (Lazy.force s) ;;
+(* let debug = print *)
+let debug s = ();;
let monster = 100;;
(add_passive_goals g_passives new_goals)
;;
+ let pp_clauses actives passives =
+ let actives_l, _ = actives in
+ let passive_t,_,_ = passives in
+ let wset = IDX.elems passive_t in
+ ("Actives :" ^ (String.concat ";\n"
+ (List.map Pp.pp_unit_clause actives_l)))
+ ^
+ ("Passives:" ^(String.concat ";\n"
+ (List.map (fun _,cl -> Pp.pp_unit_clause cl)
+ (IDX.ClauseSet.elements wset))))
+ ;;
+
let forward_infer_step
((bag,maxvar,actives,passives,g_actives,g_passives) as s)
current iterno =
* P' = P + new' *)
debug (lazy "Forward infer step...");
debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives)))));
- let id,_,_,_ = current in
- let _ = Terms.get_from_bag id bag in
-
+ debug (lazy (pp_clauses actives passives));
match Sup.keep_simplified current actives bag maxvar
with
| _,None -> s
| bag,Some (current,actives) ->
- debug (lazy "simplified...");
+ debug (lazy ("simplified to " ^ (Pp.pp_unit_clause current)));
let bag, maxvar, actives, new_clauses =
Sup.infer_right bag maxvar current actives
in
(passive_set_cardinal passives)))
;;
-
+
(* we just check if any of the active goals is subsumed by a
passive clause, or if any of the passive goal is subsumed
by an active or passive clause *)
(lazy
("Passives:" ^(String.concat ";\n"
(List.map (fun _,cl -> Pp.pp_unit_clause cl)
- (IDX.ClauseSet.elements wset))))) in
+ (IDX.ClauseSet.elements wset))))) in
let g_passives =
WeightPassiveSet.fold
(fun (_,x) acc ->
if List.exists (Sup.are_alpha_eq x) g_actives then acc
else x::acc)
(fst g_passives) []
- in
+ in
ignore
(List.iter
(fun x ->
let bag,maxvar,actives,passives,g_actives,g_passives = status in
match
Sup.simplify_goal
- ~no_demod:false maxvar (snd actives) bag g_actives current
+ ~no_demod maxvar (snd actives) bag g_actives current
with
| None -> status
| Some (bag,g_current) ->
let _ =
debug (lazy("Selected goal : " ^ Pp.pp_unit_clause current))
in
- (* awe work both on the original goal and the demodulated one*)
- let acc = check_and_infer ~no_demod:true iterno acc current
- in check_and_infer ~no_demod:false iterno acc current)
+ (* we work both on the original goal and the demodulated one*)
+ let acc = check_and_infer ~no_demod:false iterno acc current
+ in check_and_infer ~no_demod:true iterno acc current)
status passive_goals
in
goal_narrowing iterno max_steps timeout newstatus
let bag, clause =
if no_demod then bag, clause else demodulate bag clause table
in
+ let _ = debug ("demodulated goal : "
+ ^ Pp.pp_unit_clause clause)
+ in
if List.exists (are_alpha_eq clause) g_actives then None
else match (is_identity_goal clause) with
| Some subst -> raise (Success (bag,maxvar,clause,subst))
val eq : t -> t -> bool
val compare : t -> t -> int
val eqP : t
+ val is_eq: t foterm -> (t foterm* t foterm *t foterm) option
val pp : t -> string
type input
val embed : input -> t foterm
(* TODO: consider taking in input an imperative buffer for Format
* val pp : Format.formatter -> t -> unit
* *)
+ val is_eq : t foterm -> (t foterm * t foterm * t foterm) option
val pp : t -> string
type input
projects / helm.git / commitdiff