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 let debug s = prerr_endline (Lazy.force s);;
17 let convert_term = ref (fun _ _ -> assert false);;
18 let set_convert_term f = convert_term := f;;
20 module COT : Set.OrderedType
21 with type t = string * NCic.term * int * int * NCic.term *
24 type t = string * NCic.term * int * int * NCic.term * NCic.term
25 let compare = Pervasives.compare
28 module CoercionSet = Set.Make(COT)
31 Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(CoercionSet)
35 let empty_db = DB.empty,DB.empty
39 inherit NCicUnifHint.g_status
45 inherit NCicUnifHint.status
48 method set_coerc_db v = {< db = v >}
49 method set_coercion_status
50 : 'status. #g_status as 'status -> 'self
51 = fun o -> {< db = o#coerc_db >}#set_unifhint_status o
54 let index_coercion status name c src tgt arity arg =
55 let db_src,db_tgt = status#coerc_db in
56 let data = (name,c,arity,arg,src,tgt) in
57 debug (lazy ("INDEX:" ^
58 NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
59 NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ " := " ^
60 NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c ^ " " ^
61 string_of_int arg ^ " " ^ string_of_int arity));
62 let db_src = DB.index db_src src data in
63 let db_tgt = DB.index db_tgt tgt data in
64 status#set_coerc_db (db_src, db_tgt)
67 let look_for_coercion status metasenv subst context infty expty =
68 let db_src,db_tgt = status#coerc_db in
70 NCicUntrusted.apply_subst subst context infty,
71 NCicUntrusted.apply_subst subst context expty
73 | (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)),
74 (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> []
77 debug (lazy ("LOOK FOR COERCIONS: " ^
78 NCicPp.ppterm ~metasenv ~subst ~context infty ^ " |===> " ^
79 NCicPp.ppterm ~metasenv ~subst ~context expty));
81 let src_class = infty :: NCicUnifHint.eq_class_of status infty in
82 let tgt_class = expty :: NCicUnifHint.eq_class_of status expty in
87 CoercionSet.union (DB.retrieve_unifiables db_src infty) set)
88 CoercionSet.empty src_class
93 CoercionSet.union (DB.retrieve_unifiables db_tgt expty) set)
94 CoercionSet.empty tgt_class
97 debug (lazy ("CANDIDATES SRC: " ^
98 String.concat "," (List.map (fun (name,t,_,_,_,_) ->
99 name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t)
100 (CoercionSet.elements set_src))));
101 debug (lazy ("CANDIDATES TGT: " ^
102 String.concat "," (List.map (fun (name,t,_,_,_,_) ->
103 name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t)
104 (CoercionSet.elements set_tgt))));
106 let candidates = CoercionSet.inter set_src set_tgt in
108 debug (lazy ("CANDIDATES: " ^
109 String.concat "," (List.map (fun (name,t,_,_,_,_) ->
110 name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t)
111 (CoercionSet.elements candidates))));
114 (fun (name,t,arity,arg,_,_) ->
116 try NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t
117 with NCicTypeChecker.TypeCheckerFailure s ->
118 prerr_endline ("illtyped coercion: "^Lazy.force s);
119 prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
122 let ty, metasenv, args =
123 NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity
127 NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^
128 NCicPp.ppterm ~metasenv ~subst ~context
129 (NCicUntrusted.mk_appl t args) ^ " --- " ^
130 string_of_int (List.length args) ^ " == " ^ string_of_int arg));
132 name,metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
133 (CoercionSet.elements candidates)
136 (* CSC: very inefficient implementation!
137 Enrico, can we use a discrimination tree here? *)
138 let match_coercion status ~metasenv ~subst ~context t =
140 DB.fold (fst (status#coerc_db)) (fun _ v l -> (CoercionSet.elements v)@l) []
142 (HExtlib.list_findopt
143 (fun (_,p,arity,cpos,_,_) _ ->
147 NCic.Appl lp, NCic.Appl lt ->
148 (match fst (HExtlib.split_nth (List.length lp) lt) with
151 | _,NCic.Appl (he::_) -> he
154 let b = NCicReduction.alpha_eq metasenv subst context p t in
155 if not b then None else
156 let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] p in
158 let rec aux = function NCic.Prod (_,_,t) -> 1+aux t | _ -> 0 in
161 Some (p,pis - arity - cpos - 1,cpos)
163 Failure _ -> None (* raised by split_nth *)
167 let generate_dot_file status fmt =
168 let module Pp = GraphvizPp.Dot in
169 let src_db, _ = status#coerc_db in
170 let edges = ref [] in
171 DB.iter src_db (fun _ dataset ->
174 (fun (name,t,a,g,sk,dk) ->
175 debug(lazy (let p = NCicPp.ppterm ~metasenv:[] ~context:[]
176 ~subst:[] in p t ^ " ::: " ^ p sk ^ " |--> " ^ p dk));
177 let eq_s= sk::NCicUnifHint.eq_class_of status sk in
178 let eq_t= dk::NCicUnifHint.eq_class_of status dk in
179 (name,t,a,g),eq_s,eq_t
181 (CoercionSet.elements dataset);
193 let names = ref [] in
196 try List.assoc l !names
199 names := (l,"node"^string_of_int!id) :: !names;
205 ~attrs:["label",String.concat "\\n"
207 NCicPp.ppterm ~metasenv:[] ~subst:[]
208 ~context:[] t ~margin:max_int
213 (fun ((name,_,_,_),src,tgt) ->
214 Pp.edge (mangle src) (mangle tgt)
215 ~attrs:["label", name] fmt)