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 module COT : Set.OrderedType with type t = NCic.term * int * int * NCic.term *
20 type t = NCic.term * int * int * NCic.term * NCic.term
21 let compare = Pervasives.compare
24 module CoercionSet = Set.Make(COT)
27 Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(CoercionSet)
31 let empty_db = DB.empty,DB.empty
35 inherit NCicUnifHint.status
38 method set_coerc_db v = {< db = v >}
39 method set_coercion_status
40 : 'status. < coerc_db : db; uhint_db: NCicUnifHint.db; .. > as 'status ->
42 = fun o -> {< db = o#coerc_db >}#set_unifhint_status o
45 let index_coercion status c src tgt arity arg =
46 let db_src,db_tgt = status#coerc_db in
47 let data = (c,arity,arg,src,tgt) in
49 let debug s = prerr_endline (Lazy.force s) in
50 debug (lazy ("INDEX:" ^
51 NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
52 NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ " := " ^
53 NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c ^ " " ^
54 string_of_int arg ^ " " ^ string_of_int arity));
56 let db_src = DB.index db_src src data in
57 let db_tgt = DB.index db_tgt tgt data in
58 status#set_coerc_db (db_src, db_tgt)
61 let index_old_db odb (status : #status) =
63 (fun status (_,tgt,clist) ->
65 (fun status (uri,_,arg) ->
67 let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in
68 let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in
70 let cty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] c in
71 let scty, metasenv,_ =
72 NCicMetaSubst.saturate ~delta:max_int [] [] [] cty (arity+1)
75 | NCic.Prod (_, src, tgt) ->
77 NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt
80 debug (lazy (Printf.sprintf "indicizzo %s (%d)) : %s ===> %s"
81 (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] scty) (arity+1)
82 (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] src)
83 (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] tgt));
88 NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t));
91 index_coercion status c src tgt arity arg
93 | NCicEnvironment.BadDependency _
94 | NCicTypeChecker.TypeCheckerFailure _ -> status)
96 status (CoercDb.to_list odb)
99 let look_for_coercion status metasenv subst context infty expty =
100 let db_src,db_tgt = status#coerc_db in
101 match infty, expty with
102 | (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)),
103 (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> []
106 debug (lazy ("LOOK FOR COERCIONS: " ^
107 NCicPp.ppterm ~metasenv ~subst ~context infty ^ " |===> " ^
108 NCicPp.ppterm ~metasenv ~subst ~context expty));
110 let src_class = infty :: NCicUnifHint.eq_class_of status infty in
111 let tgt_class = expty :: NCicUnifHint.eq_class_of status expty in
116 CoercionSet.union (DB.retrieve_unifiables db_src infty) set)
117 CoercionSet.empty src_class
122 CoercionSet.union (DB.retrieve_unifiables db_tgt expty) set)
123 CoercionSet.empty tgt_class
125 let candidates = CoercionSet.inter set_src set_tgt in
127 debug (lazy ("CANDIDATES: " ^
128 String.concat "," (List.map (fun (t,_,_,_,_) ->
129 NCicPp.ppterm ~metasenv ~subst ~context t)
130 (CoercionSet.elements candidates))));
133 (fun (t,arity,arg,_,_) ->
135 try NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t
136 with NCicTypeChecker.TypeCheckerFailure s ->
137 prerr_endline ("illtyped coercion: "^Lazy.force s);
138 prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
141 let ty, metasenv, args =
142 NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity
146 NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^
147 NCicPp.ppterm ~metasenv ~subst ~context
148 (NCicUntrusted.mk_appl t args) ^ " --- " ^
149 string_of_int (List.length args) ^ " == " ^ string_of_int arg));
151 metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
152 (CoercionSet.elements candidates)
155 (* CSC: very inefficient implementation!
156 Enrico, can we use a discrimination tree here? *)
157 let match_coercion status ~metasenv ~subst ~context t =
159 DB.fold (fst (status#coerc_db)) (fun _ v l -> (CoercionSet.elements v)@l) []
161 (HExtlib.list_findopt
162 (fun (p,arity,cpos,_,_) _ ->
166 NCic.Appl lp, NCic.Appl lt ->
167 (match fst (HExtlib.split_nth (List.length lp) lt) with
170 | _,NCic.Appl (he::_) -> he
173 let b = NCicReduction.alpha_eq metasenv subst context p t in
174 if not b then None else
175 let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] p in
177 let rec aux = function NCic.Prod (_,_,t) -> 1+aux t | _ -> 0 in
180 Some (p,pis - arity - cpos - 1,cpos)
182 Failure _ -> None (* raised by split_nth *)
186 let generate_dot_file status =
187 let module Pp = GraphvizPp.Dot in
188 let buf = Buffer.create 10240 in
189 let fmt = Format.formatter_of_buffer buf in
190 Pp.header ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
191 ~edge_attrs:["fontsize", "10"] fmt;
192 let src_db, _ = status#coerc_db in
193 let edges = ref [] in
194 DB.iter src_db (fun _ dataset ->
197 (fun (t,a,g,sk,dk) ->
198 prerr_endline (let p = NCicPp.ppterm ~metasenv:[] ~context:[]
199 ~subst:[] in p t ^ " ::: " ^ p sk ^ " |--> " ^ p dk);
200 let eq_s=List.sort compare (sk::NCicUnifHint.eq_class_of status sk) in
201 let eq_t=List.sort compare (dk::NCicUnifHint.eq_class_of status dk) in
204 (CoercionSet.elements dataset);
216 let names = ref [] in
219 try List.assoc l !names
222 names := (l,"node"^string_of_int!id) :: !names;
228 ~attrs:["label",String.concat "\\n"
230 NCicPp.ppterm ~metasenv:[] ~subst:[]
231 ~context:[] t ~margin:max_int
236 (fun ((t,a,b),src,tgt) ->
237 Pp.edge (mangle src) (mangle tgt)
239 NCicPp.ppterm ~metasenv:[]
240 ~subst:[] ~context:[] t] fmt)