]> matita.cs.unibo.it Git - helm.git/blob - matita/components/ng_refiner/nCicCoercion.ml
Proved old axiom.
[helm.git] / matita / components / ng_refiner / nCicCoercion.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: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *)
13
14 let debug s = prerr_endline (Lazy.force s);;
15 let debug _ = ();;
16
17 let convert_term = ref (fun _ _ -> assert false);;
18 let set_convert_term f = convert_term := f;;
19
20 module COT : Set.OrderedType 
21 with type t = string * NCic.term * int * int  * NCic.term * NCic.term = 
22   struct
23      type t = string * NCic.term * int * int * NCic.term * NCic.term
24      let compare = Pervasives.compare
25   end
26
27 module CoercionSet = Set.Make(COT)
28
29 module DB = 
30   Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(CoercionSet)
31
32 type db = DB.t * DB.t
33
34 let empty_db = DB.empty,DB.empty
35
36 class type g_status =
37  object
38   inherit NCicUnifHint.g_status
39   method coerc_db: db
40  end
41
42 class virtual status =
43  object
44   inherit NCicUnifHint.status
45   val db = empty_db
46   method coerc_db = db
47   method set_coerc_db v = {< db = v >}
48   method set_coercion_status
49    : 'status. #g_status as 'status -> 'self
50    = fun o -> {< db = o#coerc_db >}#set_unifhint_status o
51  end
52
53 let index_coercion (status:#status) name c src tgt arity arg =
54   let db_src,db_tgt = status#coerc_db in
55   let data = (name,c,arity,arg,src,tgt) in
56   debug (lazy ("INDEX:" ^ 
57     status#ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
58     status#ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ "  :=  " ^
59     status#ppterm ~metasenv:[] ~subst:[] ~context:[] c ^ " " ^ 
60     string_of_int arg ^ " " ^ string_of_int arity));
61   let db_src = DB.index db_src src data in
62   let db_tgt = DB.index db_tgt tgt data in
63   status#set_coerc_db (db_src, db_tgt)
64 ;;
65
66 let look_for_coercion status metasenv subst context infty expty =
67  let db_src,db_tgt = status#coerc_db in
68   match 
69     NCicUntrusted.apply_subst status subst context infty, 
70     NCicUntrusted.apply_subst status subst context expty 
71   with
72   | (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)), 
73     (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> [] 
74   | infty, expty ->
75
76     debug (lazy ("LOOK FOR COERCIONS: " ^ 
77       status#ppterm ~metasenv ~subst ~context infty ^ "  |===> " ^
78       status#ppterm ~metasenv ~subst ~context expty));
79
80     let src_class = infty :: NCicUnifHint.eq_class_of status infty in
81     let tgt_class = expty :: NCicUnifHint.eq_class_of status expty in
82
83     let set_src = 
84       List.fold_left 
85         (fun set infty -> 
86           DB.Collector.union (DB.retrieve_unifiables_sorted db_src infty) set)
87         DB.Collector.empty src_class
88     in
89     let set_tgt = 
90       List.fold_left 
91         (fun set expty -> 
92           DB.Collector.union (DB.retrieve_unifiables_sorted db_tgt expty) set)
93         DB.Collector.empty tgt_class
94     in
95
96     debug (lazy ("CANDIDATES SRC: " ^ 
97       String.concat "," (List.map (fun (name,t,_,_,_,_) ->
98         name ^ " :: " ^ status#ppterm ~metasenv ~subst ~context t) 
99       (DB.Collector.to_list set_src))));
100     debug (lazy ("CANDIDATES TGT: " ^ 
101       String.concat "," (List.map (fun (name,t,_,_,_,_) ->
102         name ^ " :: " ^ status#ppterm ~metasenv ~subst ~context t) 
103       (DB.Collector.to_list set_tgt))));
104
105     let candidates = DB.Collector.inter set_src set_tgt in
106
107     debug (lazy ("CANDIDATES: " ^ 
108       String.concat "," (List.map (fun (name,t,_,_,_,_) ->
109         name ^ " :: " ^ status#ppterm ~metasenv ~subst ~context t) 
110       candidates)));
111
112     List.map
113       (fun (name,t,arity,arg,_,_) ->
114           let ty =
115             try NCicTypeChecker.typeof status ~metasenv:[] ~subst:[] [] t 
116             with NCicTypeChecker.TypeCheckerFailure s ->
117              prerr_endline ("illtyped coercion: "^Lazy.force s);
118              prerr_endline (status#ppterm ~metasenv:[] ~subst:[] ~context:[] t);
119              assert false
120           in
121           let ty, metasenv, args = 
122            NCicMetaSubst.saturate status ~delta:max_int metasenv subst context ty arity
123           in
124
125           debug (lazy (
126             status#ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^ 
127             status#ppterm ~metasenv ~subst ~context
128             (NCicUntrusted.mk_appl t args) ^ " --- " ^ 
129               string_of_int (List.length args) ^ " == " ^ string_of_int arg)); 
130              
131           name,metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
132       candidates
133 ;;
134
135 (* CSC: very inefficient implementation!
136    Enrico, can we use a discrimination tree here? *)
137 let match_coercion status ~metasenv ~subst ~context t =
138  let db =
139   DB.fold (fst (status#coerc_db)) (fun _ v l -> (CoercionSet.elements v)@l) []
140  in
141     (HExtlib.list_findopt
142       (fun (_,p,arity,cpos,_,_) _ ->
143         try
144          let t =
145           match p,t with
146              NCic.Appl lp, NCic.Appl lt ->
147               (match fst (HExtlib.split_nth (List.length lp) lt) with
148                   [t] -> t
149                 | l -> NCic.Appl l)
150            | _,NCic.Appl (he::_) -> he
151            | _,_ -> t
152          in
153          let b = NCicReduction.alpha_eq status metasenv subst context p t in
154          if not b then None else
155          let ty = NCicTypeChecker.typeof status ~metasenv:[] ~subst:[] [] p in
156          let pis = 
157            let rec aux = function NCic.Prod (_,_,t) -> 1+aux t | _ -> 0 in
158            aux ty
159          in
160          Some (p,pis - arity - cpos - 1,cpos)
161         with
162          Failure _ -> None (* raised by split_nth *)
163       ) db)
164 ;;
165
166 let generate_dot_file (status:#status) fmt =
167   let module Pp = GraphvizPp.Dot in
168   let src_db, _ = status#coerc_db in
169   let edges = ref [] in
170   DB.iter src_db (fun _ dataset -> 
171      edges := !edges @ 
172       List.map
173         (fun (name,t,a,g,sk,dk) -> 
174           debug(lazy (let p = status#ppterm ~metasenv:[] ~context:[]
175                 ~subst:[] in p t ^ " ::: " ^ p sk ^ " |--> " ^ p dk));
176           let eq_s= sk::NCicUnifHint.eq_class_of status sk in
177           let eq_t= dk::NCicUnifHint.eq_class_of status dk in
178           (name,t,a,g),eq_s,eq_t
179           )
180         (CoercionSet.elements dataset);
181     );
182   let nodes = 
183     HExtlib.list_uniq
184      (List.sort compare 
185        (List.flatten
186          (List.map
187            (fun (_,a,b) ->
188              [a;b]
189             )
190            !edges)))
191   in
192   let names = ref [] in
193   let id = ref 0 in
194   let mangle l =
195     try List.assoc l !names
196     with Not_found ->
197       incr id;
198       names := (l,"node"^string_of_int!id) :: !names;
199       List.assoc l !names
200   in
201   List.iter 
202     (fun cl -> 
203       Pp.node (mangle cl) 
204       ~attrs:["label",String.concat "\\n"
205         (List.map (fun t->
206           status#ppterm ~metasenv:[] ~subst:[]
207            ~context:[] t ~margin:max_int
208         ) cl)]
209       fmt)
210     nodes;
211   List.iter 
212     (fun ((name,_,_,_),src,tgt) ->
213        Pp.edge (mangle src) (mangle tgt)
214        ~attrs:["label", name] fmt)
215     !edges;
216 ;;