(* $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
+;;
+
+
module type NCicContext =
sig
val metasenv : NCic.metasenv
val context : NCic.context
end
-module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
+module NCicBlob(C : NCicContext) : Terms.Blob
+with type t = NCic.term and type input = NCic.term = struct
type t = NCic.term
- let eq x y = NCicReduction.alpha_eq C.metasenv C.subst C.context x y;;
+ 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 -> i-j
+ | 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
| ( NCic.Meta _ | NCic.Appl _ ), NCic.Const _ -> 1
| NCic.Appl _, NCic.Meta _ -> ~-1
| NCic.Meta _, NCic.Appl _ -> 1
- | _ -> assert false
+ | _ -> Pervasives.compare x y
+ (* was assert false, but why? *)
+
;;
let compare x y =
- if NCicReduction.alpha_eq C.metasenv C.subst C.context x y then 0
+ (* if NCicReduction.alpha_eq C.metasenv C.subst C.context x y then 0 *)
+ if 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;;
+ type input = NCic.term
+
let rec embed = function
| NCic.Meta (i,_) -> Terms.Var i, [i]
| NCic.Appl l ->
let saturate t ty =
let sty, _, args =
- NCicMetaSubst.saturate ~delta:max_int C.metasenv C.subst C.context
+ NCicMetaSubst.saturate ~delta:0 C.metasenv C.subst C.context
ty 0
in
let proof =
let sty = embed sty in
proof, sty
;;
-
- let eqP =
- let r =
- OCic2NCic.reference_of_oxuri
- (UriManager.uri_of_string
- "cic:/matita/logic/equality/eq.ind#xpointer(1/1)")
- in
- NCic.Const r
- ;;
-
- let eq_ind =
- let r =
- OCic2NCic.reference_of_oxuri
- (UriManager.uri_of_string
- "cic:/matita/logic/equality/eq_ind.con")
- in
- NCic.Const r
- ;;
-
- let eq_ind_r =
- let r =
- OCic2NCic.reference_of_oxuri
- (UriManager.uri_of_string
- "cic:/matita/logic/equality/eq_elim_r.con")
- in
- NCic.Const r
- ;;
-
- let eq_refl =
- let r =
- OCic2NCic.reference_of_oxuri
- (UriManager.uri_of_string
- "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)")
- in
- NCic.Const r
- ;;
-
- let extract lift vl t =
- let rec pos i = function
- | [] -> raise Not_found
- | j :: tl when j <> i -> 1+ pos i tl
- | _ -> 1
- in
- let vl_len = List.length vl in
- let rec extract = function
- | Terms.Leaf x -> NCicSubstitution.lift (vl_len+lift) x
- | Terms.Var j ->
- (try NCic.Rel (pos j vl) with Not_found -> NCic.Implicit `Term)
- | Terms.Node l -> NCic.Appl (List.map extract l)
- in
- extract t
- ;;
-
- let rec ppfot = function
- | Terms.Leaf _ -> "."
- | Terms.Var i -> "?" ^ string_of_int i
- | Terms.Node l -> "(" ^ String.concat " " (List.map ppfot l) ^ ")"
- ;;
-
- let mk_predicate hole_type amount ft p1 vl =
- let rec aux t p =
- match p with
- | [] -> NCic.Rel 1
- | n::tl ->
- match t with
- | Terms.Leaf _
- | Terms.Var _ ->
- prerr_endline ("term: " ^ ppfot ft);
- prerr_endline ("path: " ^ String.concat ","
- (List.map string_of_int p1));
- assert false
- | Terms.Node l ->
- let l =
- HExtlib.list_mapi
- (fun t i ->
- if i = n then aux t tl
- else extract amount (0::vl) t)
- l
- in
- NCic.Appl l
- in
- NCic.Lambda("x", hole_type, aux ft (List.rev p1))
- ;;
-
- let mk_proof (bag : NCic.term Terms.bag) mp steps =
- let module Subst = FoSubst in
- let position i l =
- let rec aux = function
- | [] -> assert false
- | (j,_) :: tl when i = j -> 1
- | _ :: tl -> 1 + aux tl
- in
- aux l
- in
- let vars_of i l = fst (List.assoc i l) in
- let ty_of i l = snd (List.assoc i l) in
- let close_with_lambdas vl t =
- List.fold_left
- (fun t i ->
- NCic.Lambda ("x"^string_of_int i, NCic.Implicit `Type, t))
- t vl
- in
- let close_with_forall vl t =
- List.fold_left
- (fun t i ->
- NCic.Prod ("x"^string_of_int i, NCic.Implicit `Type, t))
- t vl
- in
- let get_literal id =
- let _, lit, vl, proof = Terms.M.find id bag in
- let lit =match lit with
- | Terms.Predicate t -> assert false
- | Terms.Equation (l,r,ty,_) ->
- Terms.Node [ Terms.Leaf eqP; ty; l; r]
- in
- lit, vl, proof
- in
- let rec aux ongoal seen = function
- | [] -> NCic.Rel 1
- | id :: tl ->
- let amount = List.length seen in
- let lit,vl,proof = get_literal id in
- if not ongoal && id = mp then
- ((*prerr_endline ("Reached meeting point, id=" ^ (string_of_int id));*)
- assert (vl = []);
- NCic.LetIn ("clause_" ^ string_of_int id,
- extract amount vl lit,
- (NCic.Appl [eq_refl;NCic.Implicit `Type;NCic.Implicit `Term]),
- aux true ((id,([],lit))::seen) (id::tl)))
- else
- match proof with
- | Terms.Exact _ when tl=[] ->
- (* prerr_endline ("Exact (tl=[]) for " ^ (string_of_int id));*)
- aux ongoal seen tl
- | Terms.Step _ when tl=[] -> assert false
- | Terms.Exact ft ->
- (* prerr_endline ("Exact for " ^ (string_of_int id));*)
- NCic.LetIn ("clause_" ^ string_of_int id,
- close_with_forall vl (extract amount vl lit),
- close_with_lambdas vl (extract amount vl ft),
- aux ongoal
- ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
- | Terms.Step (_, id1, id2, dir, pos, subst) ->
- let id, id1 = if ongoal then id1,id else id,id1 in
- let lit,vl,_ = get_literal id in
- let proof_of_id id =
- let vars = List.rev (vars_of id seen) in
- let args = List.map (Subst.apply_subst subst) vars in
- let args = List.map (extract amount vl) args in
- let rel_for_id = NCic.Rel (List.length vl + position id seen) in
- if args = [] then rel_for_id
- else NCic.Appl (rel_for_id::args)
- in
- let p_id1 = proof_of_id id1 in
- let p_id2 = proof_of_id id2 in
- let pred, hole_type, l, r =
- let id1_ty = ty_of id1 seen in
- let id2_ty,l,r =
- match ty_of id2 seen with
- | Terms.Node [ _; t; l; r ] ->
- extract amount vl (Subst.apply_subst subst t),
- extract amount vl (Subst.apply_subst subst l),
- extract amount vl (Subst.apply_subst subst r)
- | _ -> assert false
- in
- (*prerr_endline "mk_predicate :";
- if ongoal then prerr_endline "ongoal=true"
- else prerr_endline "ongoal=false";
- prerr_endline ("id=" ^ string_of_int id);
- prerr_endline ("id1=" ^ string_of_int id1);
- prerr_endline ("id2=" ^ string_of_int id2);
- prerr_endline ("Positions :" ^
- (String.concat ", "
- (List.map string_of_int pos)));*)
- mk_predicate
- id2_ty amount (Subst.apply_subst subst id1_ty) pos vl,
- id2_ty,
- l,r
- in
- let l, r, eq_ind =
- if (ongoal=true) = (dir=Terms.Left2Right) then
- r,l,eq_ind_r
- else
- l,r,eq_ind
- in
- 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)
- in
- aux false [] steps
- ;;
-
+
end
projects / helm.git / blobdiff