]> matita.cs.unibo.it Git - helm.git/blob - matita/components/ng_refiner/nCicUnifHint.ml
- a reinforement in a lemma on ldrop allows to prove a lemma on lsx :)
[helm.git] / matita / components / ng_refiner / nCicUnifHint.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 module HOT : Set.OrderedType 
18 with type t = int * NCic.term  * NCic.term * NCic.term = 
19   struct
20         (* precedence, skel1, skel2, term *)
21         type t = int * NCic.term * NCic.term * NCic.term
22         let compare = Pervasives.compare
23   end
24
25 module EOT : Set.OrderedType 
26 with type t = int * NCic.term =
27   struct
28         type t = int * NCic.term 
29         let compare = Pervasives.compare
30   end
31
32 module HintSet = Set.Make(HOT)
33 module EqSet = Set.Make(EOT)
34
35 module HDB = 
36   Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(HintSet)
37
38 module EQDB = 
39   Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(EqSet)
40
41 type db =
42   HDB.t * (* hint database: (dummy A B)[?] |-> \forall X.(summy a b)[X] *)
43   EQDB.t (* eqclass DB: A[?] |-> \forall X.B[X] and viceversa *)
44
45 exception HintNotValid
46
47 let skel_dummy = NCic.Implicit `Type;;
48
49 class type g_status =
50  object
51   method uhint_db: db
52  end
53
54 class virtual status =
55  object
56   inherit NCic.status
57   val db = HDB.empty, EQDB.empty
58   method uhint_db = db
59   method set_uhint_db v = {< db = v >}
60   method set_unifhint_status
61    : 'status. #g_status as 'status -> 'self
62    = fun o -> {< db = o#uhint_db >}
63  end
64
65 let dummy = NCic.Const (NReference.reference_of_string "cic:/dummy_conv.dec");;
66 let pair t1 t2 = (NCic.Appl [dummy;t1;t2]) ;;
67
68 let index_hint status context t1 t2 precedence =
69   assert (
70     (match t1 with
71     | NCic.Meta _ | NCic.Appl (NCic.Meta _ :: _) -> false | _ -> true)
72     &&
73     (match t2 with
74     | NCic.Meta _ | NCic.Appl (NCic.Meta _ :: _) -> false | _ -> true)
75   );
76   (* here we do not use skel_dummy since it could cause an assert false in 
77    * the subst function that lives in the kernel *)
78   let hole = NCic.Meta (-1,(0,NCic.Irl 0)) in
79   let t1_skeleton = 
80     List.fold_left (fun t _ -> NCicSubstitution.subst status hole t) t1 context
81   in
82   let t2_skeleton = 
83     List.fold_left (fun t _ -> NCicSubstitution.subst status hole t) t2 context
84   in
85   let rec cleanup_skeleton () = function
86     | NCic.Meta _ -> skel_dummy 
87     | t -> NCicUtils.map status (fun _ () -> ()) () cleanup_skeleton t
88   in
89   let t1_skeleton = cleanup_skeleton () t1_skeleton in
90   let t2_skeleton = cleanup_skeleton () t2_skeleton in
91   let src = pair t1_skeleton t2_skeleton in
92   let ctx2abstractions context t = 
93     List.fold_left 
94      (fun t (n,e) -> 
95         match e with
96         | NCic.Decl ty -> NCic.Prod (n,ty,t)
97         | NCic.Def (b,ty) -> NCic.LetIn (n,ty,b,t))
98       t context 
99   in
100   let data_hint = 
101     precedence, t1_skeleton, t2_skeleton, ctx2abstractions context (pair t1 t2)
102   in
103   let data_t1 = t2_skeleton in
104   let data_t2 = t1_skeleton in
105
106   debug(lazy ("INDEXING: " ^ 
107     status#ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " |==> " ^
108     status#ppterm ~metasenv:[] ~subst:[] ~context:[] 
109       (let _,x,_,_ = data_hint in x)));
110
111   status#set_uhint_db (
112       HDB.index (fst (status#uhint_db)) src data_hint,
113       EQDB.index  
114         (EQDB.index (snd (status#uhint_db)) t2_skeleton (precedence, data_t2))
115         t1_skeleton (precedence, data_t1))
116 ;;
117
118 let add_user_provided_hint status t precedence =
119   let c, a, b = 
120     let rec aux ctx = function
121       | NCic.Appl l ->
122           (match List.rev l with
123           | b::a::_ -> 
124               if
125                  let ty_a = 
126                    NCicTypeChecker.typeof status ~metasenv:[] ~subst:[] ctx a
127                  in
128                  let ty_b = 
129                    NCicTypeChecker.typeof status ~metasenv:[] ~subst:[] ctx b
130                  in
131                  NCicReduction.are_convertible status
132                   ~metasenv:[] ~subst:[] ctx ty_a ty_b              
133                  &&     
134                  NCicReduction.are_convertible status
135                   ~metasenv:[] ~subst:[] ctx a b              
136               then ctx, a, b
137               else raise HintNotValid
138           | _ -> assert false)
139       | NCic.Prod (n,s,t) -> aux ((n, NCic.Decl s) :: ctx) t
140       | NCic.LetIn (n,ty,t,b) -> aux  ((n, NCic.Def (t,ty)) :: ctx) b
141       | _ -> assert false
142     in
143       aux [] t
144   in
145    index_hint status c a b precedence
146 ;;
147
148 (*
149 let db () = 
150   let combine f l =
151    List.flatten
152      (let rec aux = function 
153       | u1 :: tl -> List.map (f u1) tl :: aux tl
154       | [] -> []
155      in aux l)
156   in
157   let mk_hint (u1,_,_) (u2,_,_) = 
158     let l = OCic2NCic.convert_obj u1 
159       (fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph u1)) in
160     let r = OCic2NCic.convert_obj u2 
161       (fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph u2)) in
162     match List.hd l,List.hd r with
163     | (_,h1,_,_,NCic.Constant (_,_,Some l,_,_)), 
164       (_,h2,_,_,NCic.Constant (_,_,Some r,_,_)) ->
165         let rec aux ctx t1 t2 =
166           match t1, t2 with
167           | NCic.Lambda (n1,s1,b1), NCic.Lambda(_,s2,b2) ->
168               if NCicReduction.are_convertible ~subst:[] ~metasenv:[] ctx s1 s2
169               then aux ((n1, NCic.Decl s1) :: ctx) b1 b2
170               else []
171           | b1,b2 -> 
172               if NCicReduction.are_convertible ~subst:[] ~metasenv:[] ctx b1 b2 
173               then begin
174               let rec mk_rels =  
175                  function 0 -> [] | n -> NCic.Rel n :: mk_rels (n-1) 
176               in 
177               let n1 = 
178                 NCic.Appl (NCic.Const(OCic2NCic.reference_of_ouri 
179                  u1 (NReference.Def h1)) :: mk_rels (List.length ctx))
180               in
181               let n2 = 
182                 NCic.Appl (NCic.Const(OCic2NCic.reference_of_ouri 
183                  u2 (NReference.Def h2)) :: mk_rels (List.length ctx))
184               in
185                 [ctx,b1,b2; ctx,b1,n2; ctx,n1,b2; ctx,n1,n2]
186               end else []
187         in
188           aux [] l r
189     | _ -> []
190   in
191   let _hints = 
192     List.fold_left 
193       (fun acc (_,_,l) -> 
194           acc @ 
195           if List.length l > 1 then 
196            combine mk_hint l
197           else [])
198       [] (CoercDb.to_list (CoercDb.dump ()))
199   in
200   prerr_endline "MISTERO";
201   assert false (* ERA
202   List.fold_left 
203     (fun db -> function 
204      | (ctx,b1,b2) -> index_hint db ctx b1 b2 0)
205     !user_db (List.flatten hints)
206 *)
207 ;;
208 *)
209
210 let saturate status ?(delta=0) metasenv subst context ty goal_arity =
211  assert (goal_arity >= 0);
212   let rec aux metasenv = function
213    | NCic.Prod (name,s,t) as ty ->
214        let metasenv1, _, arg,_ = 
215           NCicMetaSubst.mk_meta ~attrs:[`Name name] metasenv context
216            ~with_type:s `IsTerm 
217        in
218        let t, metasenv1, args, pno = 
219            aux metasenv1 (NCicSubstitution.subst status arg t) 
220        in
221        if pno + 1 = goal_arity then
222          ty, metasenv, [], goal_arity+1
223        else
224          t, metasenv1, arg::args, pno+1
225    | ty ->
226         match NCicReduction.whd status ~subst context ty ~delta with
227         | NCic.Prod _ as ty -> aux metasenv ty
228         | _ -> ty, metasenv, [], 0 (* differs from the other impl in this line*)
229   in
230   let res, newmetasenv, arguments, _ = aux metasenv ty in
231   res, newmetasenv, arguments
232 ;;
233
234 let eq_class_of (status:#status) t1 = 
235  let eq_class =
236   if NDiscriminationTree.NCicIndexable.path_string_of t1 = 
237      [Discrimination_tree.Variable]
238   then
239     [] (* if the trie is unable to handle the key, we skip the query since
240           it sould retulr the whole content of the trie *)
241   else
242     let candidates = EQDB.retrieve_unifiables (snd status#uhint_db) t1 in
243     let candidates = EqSet.elements candidates in
244     let candidates = List.sort (fun (x,_) (y,_) -> compare x y) candidates in
245     List.map snd candidates
246  in
247  debug(lazy("eq_class of: " ^ status#ppterm ~metasenv:[] ~context:[] ~subst:[]
248    t1 ^ " is\n" ^ String.concat "\n" 
249    (List.map (status#ppterm ~metasenv:[] ~context:[] ~subst:[]) eq_class)));
250  eq_class   
251 ;;
252
253 let look_for_hint (status:#status) metasenv subst context t1 t2 =
254   if NDiscriminationTree.NCicIndexable.path_string_of t1 =
255           [Discrimination_tree.Variable] || 
256      NDiscriminationTree.NCicIndexable.path_string_of t2 =
257              [Discrimination_tree.Variable] then [] else begin
258
259   debug(lazy ("KEY1: "^status#ppterm ~metasenv ~subst ~context t1));
260   debug(lazy ("KEY2: "^status#ppterm ~metasenv ~subst ~context t2));
261 (*
262   HDB.iter status
263    (fun p ds ->
264       prerr_endline ("ENTRY: " ^
265       NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
266       String.concat "|" (List.map (status#ppterm ~metasenv:[] ~subst:[]
267       ~context:[]) (HintSet.elements ds))));
268 *)
269   let candidates1 = HDB.retrieve_unifiables (fst status#uhint_db) (pair t1 t2) in
270   let candidates2 = HDB.retrieve_unifiables (fst status#uhint_db) (pair t2 t1) in
271   let candidates1 = 
272     List.map (fun (prec,_,_,ty) -> 
273        prec,true,saturate status ~delta:max_int metasenv subst context ty 0) 
274     (HintSet.elements candidates1) 
275   in
276   let candidates2 = 
277     List.map (fun (prec,_,_,ty) -> 
278        prec,false,saturate status ~delta:max_int metasenv subst context ty 0) 
279     (HintSet.elements candidates2) 
280   in
281   let rc = 
282     List.map
283       (fun (p,b,(t,m,_)) ->
284          let rec aux () (m,l as acc) = function
285            | NCic.Meta _ as t -> acc, t
286            | NCic.LetIn (name,ty,bo,t) ->
287                let m,_,i,_=
288                  NCicMetaSubst.mk_meta ~attrs:[`Name name] m context
289                   ~with_type:ty `IsTerm 
290                in
291                let t = NCicSubstitution.subst status i t in
292                aux () (m, (i,bo)::l) t
293            | t -> NCicUntrusted.map_term_fold_a status (fun _ () -> ()) () aux acc t
294          in
295          let (m,l), t = aux () (m,[]) t in
296          p,b,(t,m,l))
297    (candidates1 @ candidates2)
298   in
299   let rc = 
300   List.map
301    (function 
302     | (prec,true,(NCic.Appl [_; t1; t2],metasenv,l))-> prec,metasenv,(t1,t2),l
303     | (prec,false,(NCic.Appl [_; t1; t2],metasenv,l))-> prec,metasenv,(t2,t1),l
304     | _ -> assert false)
305     rc
306   in
307   let rc = 
308     List.sort (fun (x,_,_,_) (y,_,_,_) -> Pervasives.compare x y) rc
309   in 
310   let rc = List.map (fun (_,x,y,z) -> x,y,z) rc in
311
312   debug(lazy ("Hints:"^
313     String.concat "\n" (List.map 
314      (fun (metasenv, (t1, t2), premises) ->
315          ("\t" ^ String.concat ";  "
316                (List.map (fun (a,b) -> 
317                   status#ppterm ~margin:max_int ~metasenv ~subst ~context a ^
318                   " =?= "^
319                   status#ppterm ~margin:max_int ~metasenv ~subst ~context b)
320                premises) ^     
321              "  ==> "^
322              status#ppterm ~margin:max_int ~metasenv ~subst ~context t1 ^
323              " = "^status#ppterm ~margin:max_int ~metasenv ~subst ~context t2))
324     rc)));
325
326   rc
327              end
328 ;;
329
330 let pp_hint t p =
331   let context, t = 
332      let rec aux ctx = function
333        | NCic.Prod (name, ty, rest) -> aux ((name, NCic.Decl ty) :: ctx) rest
334        | t -> ctx, t
335      in
336       aux [] t
337   in
338   let recproblems, concl = 
339     let rec aux ctx = function
340       | NCic.LetIn (name,ty,bo,rest) -> aux ((name, NCic.Def(bo,ty))::ctx) rest
341       | t -> ctx, t
342     in
343       aux [] t
344   in
345   let buff = Buffer.create 100 in
346   let fmt = Format.formatter_of_buffer buff in
347 (*
348   F.fprintf "@[<hov>"
349    F.fprintf "@[<hov>"
350 (*    pp_ctx [] context *)
351    F.fprintf "@]"
352   F.fprintf "@;"
353    F.fprintf "@[<hov>"
354 (*    pp_ctx context recproblems *)
355    F.fprintf "@]"
356   F.fprintf "\vdash@;";
357     status#ppterm ~fmt ~context:(recproblems@context) ~subst:[] ~metasenv:[];
358   F.fprintf "@]"
359   F.fprintf formatter "@?";
360   prerr_endline (Buffer.contents buff);
361 *)
362 ()
363 ;;
364
365 let generate_dot_file (status:#status) fmt =
366   let module Pp = GraphvizPp.Dot in
367   let h_db, _ = status#uhint_db in
368   let names = ref [] in
369   let id = ref 0 in
370   let mangle l =
371     try List.assoc l !names
372     with Not_found ->
373       incr id;
374       names := (l,"node"^string_of_int!id) :: !names;
375       List.assoc l !names
376   in
377   let nodes = ref [] in
378   let edges = ref [] in
379   HDB.iter h_db (fun _key dataset -> 
380       List.iter
381         (fun (precedence, l,r, hint) ->
382             let l = 
383               Str.global_substitute (Str.regexp "\n") (fun _ -> "")
384                (status#ppterm 
385                 ~margin:max_int ~metasenv:[] ~context:[] ~subst:[] l) 
386             in
387             let r = 
388               Str.global_substitute (Str.regexp "\n") (fun _ -> "")
389                (status#ppterm 
390                 ~margin:max_int ~metasenv:[] ~context:[] ~subst:[] r)
391             in
392             let shint =  "???" (*
393               string_of_int precedence ^ "..." ^
394               Str.global_substitute (Str.regexp "\n") (fun _ -> "")
395                (status#ppterm 
396                 ~margin:max_int ~metasenv:[] ~context:[] ~subst:[] hint)*)
397             in
398             nodes := (mangle l,l) :: (mangle r,r) :: !nodes;
399             edges := (mangle l, mangle r, shint, precedence, hint) :: !edges)
400         (HintSet.elements dataset);
401     );
402   List.iter (fun x, l -> Pp.node x ~attrs:["label",l] fmt) !nodes;
403   List.iter (fun x, y, l, _, _ -> 
404       Pp.raw (Printf.sprintf "%s -- %s [ label=\"%s\" ];\n" x y "?") fmt)
405   !edges;
406   edges := List.sort (fun (_,_,_,p1,_) (_,_,_,p2,_) -> p1 - p2) !edges;
407   List.iter (fun x, y, _, p, l -> pp_hint l p) !edges;
408 ;;