(* $Id: terms.mli 9822 2009-06-03 15:37:06Z tassi $ *)
-let eqPref = ref (fun _ -> assert false);;
-let set_eqP t = eqPref := fun _ -> t;;
-
-let default_eqP() =
- let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
- let ref = NReference.reference_of_spec uri (NReference.Ind(true,0,2)) in
- 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 eqnew = function
- _ ->
- let r = f(UriManager.uri_of_string
- "cic:/matita/logic/equality/eq.ind#xpointer(1/1)")
- in
- NCic.Const r
- in
- eqPref := eqnew
-;;
-
+let reference_of_oxuri = ref (fun _ -> assert false);;
+let set_reference_of_oxuri f = reference_of_oxuri := f;;
module type NCicContext =
sig
type t = NCic.term
- 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 eq x y = NCicReduction.alpha_eq C.metasenv C.subst C.context x y;;
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 -> compare_refs r1 r2
- (*NReference.compare r1 r2*)
+ | NCic.Const r1, NCic.Const 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
| ( NCic.Meta _ | NCic.Appl _ ), NCic.Const _ -> 1
| NCic.Appl _, NCic.Meta _ -> ~-1
| NCic.Meta _, NCic.Appl _ -> 1
- | _ -> Pervasives.compare x y
- (* was assert false, but why? *)
-
+ | _ -> assert false
;;
let compare x y =
- if NCicReduction.alpha_eq [] [] [] x y then 0
- (* if x = y then 0 *)
+ if NCicReduction.alpha_eq C.metasenv C.subst C.context x y then 0
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;;
let saturate t ty =
let sty, _, args =
- NCicMetaSubst.saturate ~delta:0 C.metasenv C.subst C.context
+ NCicMetaSubst.saturate ~delta:max_int C.metasenv C.subst C.context
ty 0
in
let proof =
let sty = embed sty in
proof, sty
;;
-
+
+ let eqP =
+ let r =
+ !reference_of_oxuri
+ (UriManager.uri_of_string
+ "cic:/matita/logic/equality/eq.ind#xpointer(1/1)")
+ in
+ NCic.Const r
+ ;;
+
end