]> matita.cs.unibo.it Git - helm.git/blob - matitaB/components/ng_paramodulation/nCicBlob.ml
Fixed indentation, which is semantic in Haskell.
[helm.git] / matitaB / components / ng_paramodulation / nCicBlob.ml
1 (*
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.                     
5     ||I||                                                                
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_______________________________________________________________ *)
11
12 (* $Id: terms.mli 9822 2009-06-03 15:37:06Z tassi $ *)
13
14 let default_eqP =
15   let uri = NUri.uri_of_string "cic:/matita/basics/logic/eq.ind" in
16   let ref = NReference.reference_of_spec uri (NReference.Ind(true,0,2)) in
17     NCic.Const ref
18 ;;
19
20 let eqPref = ref default_eqP;;
21 let set_eqP t = eqPref := t;;
22
23 let equivalence_relation =
24   let uri = NUri.uri_of_string "cic:/matita/ng/properties/relations/eq_rel.con"
25   in
26   let ref = NReference.reference_of_spec uri (NReference.Fix(0,1,2)) 
27   in NCic.Const ref
28
29 let setoid_eq =
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)) 
32   in NCic.Const ref
33
34 let set_default_eqP() = eqPref := default_eqP
35
36 let saturate status metasenv subst context t ty = 
37   let sty, _, args = 
38     (* CSC: NCicPp.status is the best I can put here *)
39     NCicMetaSubst.saturate status ~delta:0 metasenv subst context ty 0
40   in
41   let proof = 
42     if args = [] then t 
43     else NCic.Appl (t :: args)
44   in
45   proof, sty
46 ;;
47   
48
49 module NCicBlob: Terms.Blob 
50 with type t = NCic.term and type input = NCic.term = struct
51
52   type t = NCic.term
53
54   let eq x y = x = y;;
55     (* NCicReduction.alpha_eq C.metasenv C.subst C.context x y;; *)
56
57   let height_of_ref = function
58     | NReference.Def h -> h
59     | NReference.Fix(_,_,h) -> h
60     | _ -> 0
61
62   let compare_refs (NReference.Ref (u1,r1)) (NReference.Ref (u2,r2)) =
63     let x = height_of_ref r2 - height_of_ref r1 in
64       if x = 0 then 
65         Hashtbl.hash (NUri.string_of_uri u1,r1) - 
66           Hashtbl.hash (NUri.string_of_uri u2,r2)
67       else x 
68
69   let rec compare x y = 
70     match x,y with
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? *)
84         
85   ;;
86   
87   let rec alpha_norm k = function
88     | NCic.Lambda (_,ty,t) -> 
89         NCic.Lambda("_",alpha_norm k ty,alpha_norm k t)
90     | NCic.Prod (_,ty,t) -> 
91         NCic.Prod("_",alpha_norm k ty,alpha_norm k t)
92     | NCic.LetIn (_,ty,t,b) -> 
93         NCic.LetIn("_",alpha_norm k ty,alpha_norm k t,alpha_norm k b)
94     | NCic.Meta (_,(_,NCic.Irl _)) as t -> t
95     | NCic.Meta (n,(s,NCic.Ctx tl)) as t -> 
96         let tl' = HExtlib.sharing_map (alpha_norm k) tl in
97         if tl == tl' then t else NCic.Meta (n,(s,NCic.Ctx tl'))
98     | t -> NCicUtils.map ~hbr:false (new NCicPp.status None)
99         (fun _ _ -> ()) () alpha_norm t
100
101   (* let compare x y = 
102     (* CSC: NCicPp.status is the best I can put here *)
103     (* WR: and I can't guess a user id, so I must put None *)
104     if NCicReduction.alpha_eq (new NCicPp.status None) [] [] [] x y  then 0 
105     (* if x = y  then 0 *)
106     else compare x y
107   ;; *)
108
109   let eqP = fun () -> !eqPref
110   ;;
111
112   let is_eq = function
113     | Terms.Node [ Terms.Leaf eqt ; ty; l; r ] when eq (eqP()) eqt ->
114         Some (ty,l,r) 
115     | Terms.Node [ Terms.Leaf eqt ; ty; l; r ] ->
116         None
117 (*
118     | Terms.Node [ Terms.Leaf eqt ; _; Terms.Node [Terms.Leaf eqt2 ; ty]; l; r]
119         when eq equivalence_relation eqt && eq setoid_eq eqt2 ->
120         Some (ty,l,r) *)
121     | _ -> None
122
123   let pp t = 
124     (* CSC: NCicPp.status is the best I can put here *)
125     (new NCicPp.status None)#ppterm ~context:[] ~metasenv:[] ~subst:[] t
126
127   type input = NCic.term
128
129   let rec embed = function
130     | NCic.Meta (i,_) -> Terms.Var i, [i]
131     | NCic.Appl l ->
132         let rec aux acc l = function
133           |[] -> acc@l
134           |hd::tl -> if List.mem hd l then aux acc l tl else aux (hd::acc) l tl
135         in
136         let res,vars = List.fold_left
137           (fun (r,v) t -> let r1,v1 = embed t in (r1::r),aux [] v v1) ([],[]) l
138         in (Terms.Node (List.rev res)), vars
139     | t -> Terms.Leaf (alpha_norm () t), []
140   ;;
141
142   let embed t = fst (embed t) ;;
143
144  end