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 COT : Set.OrderedType with type t = NCic.term * int * int =
16 type t = NCic.term * int * int
17 let compare = Pervasives.compare
20 module CoercionSet = Set.Make(COT)
23 Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(CoercionSet)
27 let index_coercion (db_src,db_tgt) c src tgt arity arg =
28 let data = (c,arity,arg) in
29 let db_src = DB.index db_src src data in
30 let db_tgt = DB.index db_tgt tgt data in
36 (fun db (_,tgt,clist) ->
38 (fun db (uri,_,arg) ->
39 let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in
40 let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in
42 let cty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] c in
44 NCicMetaSubst.saturate ~delta:max_int [] [] [] cty (arity+1)
46 | NCic.Prod (_, src, tgt),_,_ ->
47 src, NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt
50 NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t);
54 prerr_endline (Printf.sprintf "indicizzo %s %d %d"
55 (UriManager.string_of_uri uri) arity arg);
57 index_coercion db c src tgt arity arg)
59 (DB.empty,DB.empty) (CoercDb.to_list ())
62 let look_for_coercion (db_src,db_tgt) metasenv subst context infty expty =
63 let set_src = DB.retrieve_unifiables db_src infty in
64 let set_tgt = DB.retrieve_unifiables db_tgt expty in
65 let candidates = CoercionSet.inter set_src set_tgt in
68 let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t in
69 let ty, metasenv, args =
70 NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity
73 NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^
74 NCicPp.ppterm ~metasenv ~subst ~context
75 (NCicUntrusted.mk_appl t args) ^ " --- " ^
76 string_of_int (List.length args) ^ " == " ^ string_of_int arg); *)
77 metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
78 (CoercionSet.elements candidates)