2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
12 (* $Id: terms.mli 9822 2009-06-03 15:37:06Z tassi $ *)
14 let eqPref = ref (fun _ -> assert false);;
15 let set_eqP t = eqPref := fun _ -> t;;
18 let uri = NUri.uri_of_string "cic:/matita/basics/logic/eq.ind" in
19 let ref = NReference.reference_of_spec uri (NReference.Ind(true,0,2)) in
23 let equivalence_relation =
24 let uri = NUri.uri_of_string "cic:/matita/ng/properties/relations/eq_rel.con"
26 let ref = NReference.reference_of_spec uri (NReference.Fix(0,1,2))
30 let uri = NUri.uri_of_string "cic:/matita/ng/sets/setoids/eq.con" in
31 let ref = NReference.reference_of_spec uri (NReference.Fix(0,0,2))
34 let set_default_eqP() = eqPref := default_eqP
36 let saturate status metasenv subst context t ty =
38 (* CSC: NCicPp.status is the best I can put here *)
39 NCicMetaSubst.saturate status ~delta:0 metasenv subst context ty 0
43 else NCic.Appl (t :: args)
49 module NCicBlob: Terms.Blob
50 with type t = NCic.term and type input = NCic.term = struct
55 (* NCicReduction.alpha_eq C.metasenv C.subst C.context x y;; *)
57 let height_of_ref = function
58 | NReference.Def h -> h
59 | NReference.Fix(_,_,h) -> h
62 let compare_refs (NReference.Ref (u1,r1)) (NReference.Ref (u2,r2)) =
63 let x = height_of_ref r2 - height_of_ref r1 in
65 Hashtbl.hash (NUri.string_of_uri u1,r1) -
66 Hashtbl.hash (NUri.string_of_uri u2,r2)
71 | NCic.Rel i, NCic.Rel j -> j-i
72 | NCic.Meta (i,_), NCic.Meta (j,_) -> i-j
73 | NCic.Const r1, NCic.Const r2 -> compare_refs r1 r2
74 (*NReference.compare r1 r2*)
75 | NCic.Appl l1, NCic.Appl l2 -> FoUtils.lexicograph compare l1 l2
76 | NCic.Rel _, ( NCic.Meta _ | NCic.Const _ | NCic.Appl _ ) -> ~-1
77 | ( NCic.Meta _ | NCic.Const _ | NCic.Appl _ ), NCic.Rel _ -> 1
78 | NCic.Const _, ( NCic.Meta _ | NCic.Appl _ ) -> ~-1
79 | ( NCic.Meta _ | NCic.Appl _ ), NCic.Const _ -> 1
80 | NCic.Appl _, NCic.Meta _ -> ~-1
81 | NCic.Meta _, NCic.Appl _ -> 1
82 | _ -> Pervasives.compare x y
83 (* was assert false, but why? *)
88 (* CSC: NCicPp.status is the best I can put here *)
89 (* WR: and I can't guess a user id, so I must put None *)
90 if NCicReduction.alpha_eq (new NCicPp.status None) [] [] [] x y then 0
99 | Terms.Node [ Terms.Leaf eqt ; ty; l; r ] when eq eqP eqt ->
102 | Terms.Node [ Terms.Leaf eqt ; _; Terms.Node [Terms.Leaf eqt2 ; ty]; l; r]
103 when eq equivalence_relation eqt && eq setoid_eq eqt2 ->
108 (* CSC: NCicPp.status is the best I can put here *)
109 (new NCicPp.status None)#ppterm ~context:[] ~metasenv:[] ~subst:[] t
111 type input = NCic.term
113 let rec embed = function
114 | NCic.Meta (i,_) -> Terms.Var i, [i]
116 let rec aux acc l = function
118 |hd::tl -> if List.mem hd l then aux acc l tl else aux (hd::acc) l tl
120 let res,vars = List.fold_left
121 (fun (r,v) t -> let r1,v1 = embed t in (r1::r),aux [] v v1) ([],[]) l
122 in (Terms.Node (List.rev res)), vars
123 | t -> Terms.Leaf t, []
126 let embed t = fst (embed t) ;;