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 empty_db = DB.empty,DB.empty
33 method set_coerc_db v = {< db = v >}
34 method set_coercion_status
35 : 'status. < coerc_db : db; .. > as 'status -> 'self
36 = fun o -> {< db = o#coerc_db >}
39 let index_coercion status c src tgt arity arg =
40 let db_src,db_tgt = status#coerc_db in
41 let data = (c,arity,arg) in
43 prerr_endline ("INDEX:" ^
44 NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
45 NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ " := " ^
46 NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c);
48 let db_src = DB.index db_src src data in
49 let db_tgt = DB.index db_tgt tgt data in
50 status#set_coerc_db (db_src, db_tgt)
53 let index_old_db odb (status : #status) =
55 (fun status (_,tgt,clist) ->
57 (fun status (uri,_,arg) ->
59 let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in
60 let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in
62 let cty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] c in
63 let scty, metasenv,_ =
64 NCicMetaSubst.saturate ~delta:max_int [] [] [] cty (arity+1)
67 | NCic.Prod (_, src, tgt) ->
69 NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt
72 prerr_endline (Printf.sprintf "indicizzo %s (%d) : %s ===> %s"
73 (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] scty) (arity+1)
74 (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] src)
75 (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] tgt));
80 NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t);
83 index_coercion status c src tgt arity arg
85 | NCicEnvironment.BadDependency _
86 | NCicTypeChecker.TypeCheckerFailure _ -> status)
88 status (CoercDb.to_list odb)
91 let look_for_coercion status metasenv subst context infty expty =
92 let db_src,db_tgt = status#coerc_db in
93 match infty, expty with
94 | (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)),
95 (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> []
98 prerr_endline ("LOOK FOR COERCIONS: " ^
99 NCicPp.ppterm ~metasenv ~subst ~context infty ^ " |===> " ^
100 NCicPp.ppterm ~metasenv ~subst ~context expty);
102 let set_src = DB.retrieve_unifiables db_src infty in
103 let set_tgt = DB.retrieve_unifiables db_tgt expty in
104 let candidates = CoercionSet.inter set_src set_tgt in
106 prerr_endline ("CANDIDATES: " ^
107 String.concat "," (List.map (fun (t,_,_) ->
108 NCicPp.ppterm ~metasenv ~subst ~context t)
109 (CoercionSet.elements candidates)));
112 (fun (t,arity,arg) ->
113 let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t in
114 let ty, metasenv, args =
115 NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity
118 NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^
119 NCicPp.ppterm ~metasenv ~subst ~context
120 (NCicUntrusted.mk_appl t args) ^ " --- " ^
121 string_of_int (List.length args) ^ " == " ^ string_of_int arg); *)
122 metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
123 (CoercionSet.elements candidates)