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: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *)
14 module Ref = NReference
16 let debug s = prerr_endline (Lazy.force s);;
19 module HOT : Set.OrderedType
20 with type t = int * NCic.term * NCic.term * NCic.term =
22 (* precedence, skel1, skel2, term *)
23 type t = int * NCic.term * NCic.term * NCic.term
24 let compare = Pervasives.compare
27 module EOT : Set.OrderedType
28 with type t = int * NCic.term =
30 type t = int * NCic.term
31 let compare = Pervasives.compare
34 module HintSet = Set.Make(HOT)
35 module EqSet = Set.Make(EOT)
38 Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(HintSet)
41 Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(EqSet)
44 HDB.t * (* hint database: (dummy A B)[?] |-> \forall X.(summy a b)[X] *)
45 EQDB.t (* eqclass DB: A[?] |-> \forall X.B[X] and viceversa *)
47 exception HintNotValid
49 let skel_dummy = NCic.Implicit `Type;;
56 class virtual status =
59 val db = HDB.empty, EQDB.empty
61 method set_uhint_db v = {< db = v >}
62 method set_unifhint_status
63 : 'status. #g_status as 'status -> 'self
64 = fun o -> {< db = o#uhint_db >}
68 let uri = NUri.uri_of_string "cic:/matita/dummy/dec.con" in
69 NCic.Const (Ref.reference_of_spec uri Ref.Decl);;
71 let pair t1 t2 = (NCic.Appl [dummy;t1;t2]) ;;
73 let index_hint status context t1 t2 precedence =
76 | NCic.Meta _ | NCic.Appl (NCic.Meta _ :: _) -> false | _ -> true)
79 | NCic.Meta _ | NCic.Appl (NCic.Meta _ :: _) -> false | _ -> true)
81 (* here we do not use skel_dummy since it could cause an assert false in
82 * the subst function that lives in the kernel *)
83 let hole = NCic.Meta (-1,(0,NCic.Irl 0)) in
85 List.fold_left (fun t _ -> NCicSubstitution.subst status hole t) t1 context
88 List.fold_left (fun t _ -> NCicSubstitution.subst status hole t) t2 context
90 let rec cleanup_skeleton () = function
91 | NCic.Meta _ -> skel_dummy
92 | t -> NCicUtils.map status (fun _ () -> ()) () cleanup_skeleton t
94 let t1_skeleton = cleanup_skeleton () t1_skeleton in
95 let t2_skeleton = cleanup_skeleton () t2_skeleton in
96 let src = pair t1_skeleton t2_skeleton in
97 let ctx2abstractions context t =
101 | NCic.Decl ty -> NCic.Prod (n,ty,t)
102 | NCic.Def (b,ty) -> NCic.LetIn (n,ty,b,t))
106 precedence, t1_skeleton, t2_skeleton, ctx2abstractions context (pair t1 t2)
108 let data_t1 = t2_skeleton in
109 let data_t2 = t1_skeleton in
111 debug(lazy ("INDEXING: " ^
112 status#ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " |==> " ^
113 status#ppterm ~metasenv:[] ~subst:[] ~context:[]
114 (let _,x,_,_ = data_hint in x)));
116 status#set_uhint_db (
117 HDB.index (fst (status#uhint_db)) src data_hint,
119 (EQDB.index (snd (status#uhint_db)) t2_skeleton (precedence, data_t2))
120 t1_skeleton (precedence, data_t1))
123 let add_user_provided_hint status t precedence =
125 let rec aux ctx = function
127 (match List.rev l with
131 NCicTypeChecker.typeof status ~metasenv:[] ~subst:[] ctx a
134 NCicTypeChecker.typeof status ~metasenv:[] ~subst:[] ctx b
136 NCicReduction.are_convertible status
137 ~metasenv:[] ~subst:[] ctx ty_a ty_b
139 NCicReduction.are_convertible status
140 ~metasenv:[] ~subst:[] ctx a b
142 else raise HintNotValid
144 | NCic.Prod (n,s,t) -> aux ((n, NCic.Decl s) :: ctx) t
145 | NCic.LetIn (n,ty,t,b) -> aux ((n, NCic.Def (t,ty)) :: ctx) b
150 index_hint status c a b precedence
157 (let rec aux = function
158 | u1 :: tl -> List.map (f u1) tl :: aux tl
162 let mk_hint (u1,_,_) (u2,_,_) =
163 let l = OCic2NCic.convert_obj u1
164 (fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph u1)) in
165 let r = OCic2NCic.convert_obj u2
166 (fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph u2)) in
167 match List.hd l,List.hd r with
168 | (_,h1,_,_,NCic.Constant (_,_,Some l,_,_)),
169 (_,h2,_,_,NCic.Constant (_,_,Some r,_,_)) ->
170 let rec aux ctx t1 t2 =
172 | NCic.Lambda (n1,s1,b1), NCic.Lambda(_,s2,b2) ->
173 if NCicReduction.are_convertible ~subst:[] ~metasenv:[] ctx s1 s2
174 then aux ((n1, NCic.Decl s1) :: ctx) b1 b2
177 if NCicReduction.are_convertible ~subst:[] ~metasenv:[] ctx b1 b2
180 function 0 -> [] | n -> NCic.Rel n :: mk_rels (n-1)
183 NCic.Appl (NCic.Const(OCic2NCic.reference_of_ouri
184 u1 (Ref.Def h1)) :: mk_rels (List.length ctx))
187 NCic.Appl (NCic.Const(OCic2NCic.reference_of_ouri
188 u2 (Ref.Def h2)) :: mk_rels (List.length ctx))
190 [ctx,b1,b2; ctx,b1,n2; ctx,n1,b2; ctx,n1,n2]
200 if List.length l > 1 then
203 [] (CoercDb.to_list (CoercDb.dump ()))
205 prerr_endline "MISTERO";
209 | (ctx,b1,b2) -> index_hint db ctx b1 b2 0)
210 !user_db (List.flatten hints)
215 let saturate status ?(delta=0) metasenv subst context ty goal_arity =
216 assert (goal_arity >= 0);
217 let rec aux metasenv = function
218 | NCic.Prod (name,s,t) as ty ->
219 let metasenv1, _, arg,_ =
220 NCicMetaSubst.mk_meta ~attrs:[`Name name] metasenv context
223 let t, metasenv1, args, pno =
224 aux metasenv1 (NCicSubstitution.subst status arg t)
226 if pno + 1 = goal_arity then
227 ty, metasenv, [], goal_arity+1
229 t, metasenv1, arg::args, pno+1
231 match NCicReduction.whd status ~subst context ty ~delta with
232 | NCic.Prod _ as ty -> aux metasenv ty
233 | _ -> ty, metasenv, [], 0 (* differs from the other impl in this line*)
235 let res, newmetasenv, arguments, _ = aux metasenv ty in
236 res, newmetasenv, arguments
239 let eq_class_of (status:#status) t1 =
241 if NDiscriminationTree.NCicIndexable.path_string_of t1 =
242 [Discrimination_tree.Variable]
244 [] (* if the trie is unable to handle the key, we skip the query since
245 it sould retulr the whole content of the trie *)
247 let candidates = EQDB.retrieve_unifiables (snd status#uhint_db) t1 in
248 let candidates = EqSet.elements candidates in
249 let candidates = List.sort (fun (x,_) (y,_) -> compare x y) candidates in
250 List.map snd candidates
252 debug(lazy("eq_class of: " ^ status#ppterm ~metasenv:[] ~context:[] ~subst:[]
253 t1 ^ " is\n" ^ String.concat "\n"
254 (List.map (status#ppterm ~metasenv:[] ~context:[] ~subst:[]) eq_class)));
258 let look_for_hint (status:#status) metasenv subst context t1 t2 =
259 if NDiscriminationTree.NCicIndexable.path_string_of t1 =
260 [Discrimination_tree.Variable] ||
261 NDiscriminationTree.NCicIndexable.path_string_of t2 =
262 [Discrimination_tree.Variable] then [] else begin
264 debug(lazy ("KEY1: "^status#ppterm ~metasenv ~subst ~context t1));
265 debug(lazy ("KEY2: "^status#ppterm ~metasenv ~subst ~context t2));
269 prerr_endline ("ENTRY: " ^
270 NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
271 String.concat "|" (List.map (status#ppterm ~metasenv:[] ~subst:[]
272 ~context:[]) (HintSet.elements ds))));
274 let candidates1 = HDB.retrieve_unifiables (fst status#uhint_db) (pair t1 t2) in
275 let candidates2 = HDB.retrieve_unifiables (fst status#uhint_db) (pair t2 t1) in
277 List.map (fun (prec,_,_,ty) ->
278 prec,true,saturate status ~delta:max_int metasenv subst context ty 0)
279 (HintSet.elements candidates1)
282 List.map (fun (prec,_,_,ty) ->
283 prec,false,saturate status ~delta:max_int metasenv subst context ty 0)
284 (HintSet.elements candidates2)
288 (fun (p,b,(t,m,_)) ->
289 let rec aux () (m,l as acc) = function
290 | NCic.Meta _ as t -> acc, t
291 | NCic.LetIn (name,ty,bo,t) ->
293 NCicMetaSubst.mk_meta ~attrs:[`Name name] m context
294 ~with_type:ty `IsTerm
296 let t = NCicSubstitution.subst status i t in
297 aux () (m, (i,bo)::l) t
298 | t -> NCicUntrusted.map_term_fold_a status (fun _ () -> ()) () aux acc t
300 let (m,l), t = aux () (m,[]) t in
302 (candidates1 @ candidates2)
307 | (prec,true,(NCic.Appl [_; t1; t2],metasenv,l))-> prec,metasenv,(t1,t2),l
308 | (prec,false,(NCic.Appl [_; t1; t2],metasenv,l))-> prec,metasenv,(t2,t1),l
313 List.sort (fun (x,_,_,_) (y,_,_,_) -> Pervasives.compare x y) rc
315 let rc = List.map (fun (_,x,y,z) -> x,y,z) rc in
317 debug(lazy ("Hints:"^
318 String.concat "\n" (List.map
319 (fun (metasenv, (t1, t2), premises) ->
320 ("\t" ^ String.concat "; "
321 (List.map (fun (a,b) ->
322 status#ppterm ~margin:max_int ~metasenv ~subst ~context a ^
324 status#ppterm ~margin:max_int ~metasenv ~subst ~context b)
327 status#ppterm ~margin:max_int ~metasenv ~subst ~context t1 ^
328 " = "^status#ppterm ~margin:max_int ~metasenv ~subst ~context t2))
337 let rec aux ctx = function
338 | NCic.Prod (name, ty, rest) -> aux ((name, NCic.Decl ty) :: ctx) rest
343 let recproblems, concl =
344 let rec aux ctx = function
345 | NCic.LetIn (name,ty,bo,rest) -> aux ((name, NCic.Def(bo,ty))::ctx) rest
350 let buff = Buffer.create 100 in
351 let fmt = Format.formatter_of_buffer buff in
354 (* pp_ctx [] context *)
358 (* pp_ctx context recproblems *)
360 F.fprintf "\vdash@;";
361 status#ppterm ~fmt ~context:(recproblems@context) ~subst:[] ~metasenv:[];
363 F.fprintf formatter "@?";
364 prerr_endline (Buffer.contents buff);
369 let generate_dot_file (status:#status) fmt =
370 let module Pp = GraphvizPp.Dot in
371 let h_db, _ = status#uhint_db in
372 let names = ref [] in
375 try List.assoc l !names
378 names := (l,"node"^string_of_int!id) :: !names;
381 let nodes = ref [] in
382 let edges = ref [] in
383 HDB.iter h_db (fun _key dataset ->
385 (fun (precedence, l,r, hint) ->
387 Str.global_substitute (Str.regexp "\n") (fun _ -> "")
389 ~margin:max_int ~metasenv:[] ~context:[] ~subst:[] l)
392 Str.global_substitute (Str.regexp "\n") (fun _ -> "")
394 ~margin:max_int ~metasenv:[] ~context:[] ~subst:[] r)
397 string_of_int precedence ^ "..." ^
398 Str.global_substitute (Str.regexp "\n") (fun _ -> "")
400 ~margin:max_int ~metasenv:[] ~context:[] ~subst:[] hint)*)
402 nodes := (mangle l,l) :: (mangle r,r) :: !nodes;
403 edges := (mangle l, mangle r, shint, precedence, hint) :: !edges)
404 (HintSet.elements dataset);
406 List.iter (fun x, l -> Pp.node x ~attrs:["label",l] fmt) !nodes;
407 List.iter (fun x, y, _l, _, _ ->
408 Pp.raw (Printf.sprintf "%s -- %s [ label=\"%s\" ];\n" x y "?") fmt)
410 edges := List.sort (fun (_,_,_,p1,_) (_,_,_,p2,_) -> p1 - p2) !edges;
411 List.iter (fun _x, _y, _, p, l -> pp_hint l p) !edges;