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 let debug s = prerr_endline (Lazy.force s) ;;
15 let skel_dummy = NCic.Implicit `Type;;
29 HExtlib.list_findopt (fun y i -> if y = x then Some i else None) l
32 | None -> assert false
35 let rec count_prod = function
36 | NCic.Prod (_,_,x) -> 1 + count_prod x
44 HExtlib.list_findopt (fun y j -> if i+1=j then Some y else None) l
47 | None -> assert false)
51 let rec cleanup_funclass_skel = function
52 | NCic.Prod (_,_,t) ->
53 NCic.Prod ("_",skel_dummy, cleanup_funclass_skel t)
57 let src_tgt_of_ty_cpos_arity ty cpos arity =
58 let pis = count_prod ty in
59 let tpos = pis - arity in
60 let rec pi_nth i j = function
61 | NCic.Prod (_,s,_) when i = j -> s
62 | NCic.Prod (_,_,t) -> pi_nth (i+1) j t
63 | t -> assert (i = j); t
65 let rec pi_tail i j = function
66 | NCic.Prod (_,_,_) as t when i = j -> cleanup_funclass_skel t
67 | NCic.Prod (_,_,t) -> pi_tail (i+1) j t
68 | t -> assert (i = j); t
71 let rec aux () = function
73 | NCic.Implicit _ as x -> x
74 | NCic.Rel _ -> skel_dummy
75 | t -> NCicUtils.map (fun _ () -> ()) () aux t
79 mask (pi_nth 0 cpos ty),
80 mask (pi_tail 0 tpos ty)
83 let rec cleanup_skel () = function
84 | NCic.Meta _ -> skel_dummy
85 | t -> NCicUtils.map (fun _ () -> ()) () cleanup_skel t
88 let close_in_context t metasenv =
89 let rec aux m_subst subst ctx = function
90 | (i,(tag,[],ty)) :: tl ->
91 let name = "x" ^ string_of_int (List.length ctx) in
92 let subst = (i,(tag,[],NCic.Rel (List.length tl+1),ty))::subst in
93 let ty = NCicUntrusted.apply_subst (m_subst (List.length ctx)) ctx ty in
95 (i,(tag,[],NCic.Rel (m-List.length ctx),ty))::(m_subst m)
97 NCic.Lambda (name, ty, aux m_subst subst ((name,NCic.Decl ty)::ctx) tl)
100 since metas occurring in t have an empty context,
101 the substitution i build makes sense (i.e, the Rel
102 I pun in the subst will not be lifted by subst_meta *)
103 NCicUntrusted.apply_subst subst ctx
104 (NCicSubstitution.lift (List.length ctx) t)
107 aux (fun _ -> []) [] [] metasenv
110 let toposort metasenv =
111 let module T = HTopoSort.Make(
112 struct type t = int * NCic.conjecture let compare (i,_) (j,_) = i-j end)
114 let deps (_,(_,_,t)) =
115 List.filter (fun (j,_) ->
116 List.mem j (NCicUntrusted.metas_of_term [] [] t)) metasenv
118 T.topological_sort metasenv deps
121 let only_head = function
122 | NCic.Appl (h::tl) ->
123 NCic.Appl (h :: HExtlib.mk_list skel_dummy (List.length tl))
127 let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
128 let status, src, cpos =
129 let rec aux cpos ctx = function
130 | NCic.Prod (name,ty,bo) ->
131 if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo
134 let metasenv,subst,status,src =
135 GrafiteDisambiguate.disambiguate_nterm
136 None status ctx [] [] ("",0,src) in
137 let src = NCicUntrusted.apply_subst subst [] src in
138 (* CHECK that the declared pattern matches the abstraction *)
139 let _ = NCicUnification.unify status metasenv subst ctx ty src in
140 let src = cleanup_skel () src in
143 | NCicUnification.UnificationFailure _
144 | NCicUnification.Uncertain _
145 | MultiPassDisambiguator.DisambiguationError _ ->
146 raise (GrafiteTypes.Command_error "bad source pattern"))
151 let status, tgt, arity =
152 let metasenv,subst,status,tgt =
153 GrafiteDisambiguate.disambiguate_nterm
154 None status [] [] [] ("",0,tgt) in
155 let tgt = NCicUntrusted.apply_subst subst [] tgt in
156 (* CHECK che sia unificabile mancante *)
157 let rec count_prod = function
158 | NCic.Prod (_,_,x) -> 1 + count_prod x
161 let arity = count_prod tgt in
163 if arity > 0 then cleanup_funclass_skel tgt
164 else cleanup_skel () tgt
168 status, src, tgt, cpos, arity
171 let fresh_uri status prefix suffix =
172 let mk x = NUri.uri_of_string (status#baseuri ^ "/" ^ prefix ^ x ^ suffix) in
173 let rec diverge u i =
174 if NCicLibrary.aliases_of u = [] then u
175 else diverge (mk ("__" ^ string_of_int i)) (i+1)
181 let close_graph name t s d to_s from_d p a status =
184 (function (_,_,NCic.Appl (x::_),_,_) -> x = t | _ -> assert false)
185 (NCicCoercion.look_for_coercion status [] [] [] s d)
187 let compose_names a b = a ^ "__o__" ^ b in
191 (fun (n1,m1,t1,_,j) (n,mc,c,_,i) ->
192 compose_names n1 n,m1@mc,c,[i,t1],j,a)
197 (fun (n,mc,c,_,j) (n1,m1,t1,ty,i) ->
198 compose_names n1 n,m1@mc,t1,[i,c],j,count_prod ty)
201 let to_s_o_c_o_from_d =
203 (fun (n1,m1,t1,_,j) (n,m,t,upl,i,a)->
204 compose_names n n1,m@m1,t,(i,t1)::upl,j,a)
207 to_s_o_c @ c_o_from_d @ to_s_o_c_o_from_d
211 (fun (name,metasenv, bo, upl, p, arity) ->
213 let metasenv, subst =
215 (fun (metasenv,subst) (a,b) ->
216 NCicUnification.unify status metasenv subst [] a b)
219 let bo = NCicUntrusted.apply_subst subst [] bo in
220 let p = NCicUntrusted.apply_subst subst [] p in
221 let metasenv = NCicUntrusted.apply_subst_metasenv subst metasenv in
222 let metasenv = toposort metasenv in
223 let bo = close_in_context bo metasenv in
226 | NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv)
229 let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] bo in
230 let src,tgt = src_tgt_of_ty_cpos_arity ty pos arity in
231 let src = only_head src in
232 let tgt = only_head tgt in
235 NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] bo ^ " : " ^
236 NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty ^ " as " ^
237 NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
238 NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^
239 " cpos=" ^ string_of_int pos ^ " arity=" ^ string_of_int arity));
240 let uri = fresh_uri status name ".con" in
241 let obj_kind = NCic.Constant
242 ([],name,Some bo,ty,(`Generated,`Definition,`Coercion arity))
244 let height = NCicTypeChecker.height_of_obj_kind uri [] obj_kind in
245 let obj = uri,height,[],[],obj_kind in
248 (NReference.reference_of_spec uri (NReference.Def height))
250 Some (obj,name,c,src,tgt,pos,arity)
252 | NCicTypeChecker.TypeCheckerFailure _
253 | NCicUnification.UnificationFailure _
254 | NCicUnification.Uncertain _ -> None
261 let basic_index_ncoercion (name,t,s,d,position,arity) status =
262 NCicCoercion.index_coercion status name t s d arity position
265 let basic_eval_ncoercion (name,t,s,d,p,a) status =
267 NCicCoercion.look_for_coercion status [] [] [] skel_dummy s
270 NCicCoercion.look_for_coercion status [] [] [] d skel_dummy
272 let status = NCicCoercion.index_coercion status name t s d a p in
273 let composites = close_graph name t s d to_s from_d p a status in
275 (fun (uris,infos,st) ((uri,_,_,_,_ as obj),name,t,s,d,p,a) ->
276 let info = name,t,s,d,p,a in
277 let st = NCicLibrary.add_obj st obj in
278 let st = basic_index_ncoercion info st in
279 uri::uris, info::infos, st)
280 ([],[],status) composites
283 let record_ncoercion =
284 let aux (name,t,s,d,p,a) ~refresh_uri_in_universe ~refresh_uri_in_term =
285 let t = refresh_uri_in_term t in
286 let s = refresh_uri_in_term s in
287 let d = refresh_uri_in_term d in
288 basic_index_ncoercion (name,t,s,d,p,a)
290 let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term =
291 List.fold_right (aux ~refresh_uri_in_universe ~refresh_uri_in_term) l
293 NCicLibrary.Serializer.register#run "ncoercion"
294 object(self : 'a NCicLibrary.register_type)
299 let basic_eval_and_record_ncoercion infos status =
300 let uris, cinfos, status = basic_eval_ncoercion infos status in
301 let dump = record_ncoercion (infos::cinfos) :: status#dump in
302 status#set_dump dump, uris
305 let basic_eval_and_record_ncoercion_from_t_cpos_arity
306 status (name,t,cpos,arity)
308 let ty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] t in
309 let src,tgt = src_tgt_of_ty_cpos_arity ty cpos arity in
311 basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status
316 let eval_ncoercion status name t ty (id,src) tgt =
318 let metasenv,subst,status,ty =
319 GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,ty) in
320 assert (metasenv=[]);
321 let ty = NCicUntrusted.apply_subst subst [] ty in
322 let metasenv,subst,status,t =
323 GrafiteDisambiguate.disambiguate_nterm (Some ty) status [] [] [] ("",0,t) in
324 assert (metasenv=[]);
325 let t = NCicUntrusted.apply_subst subst [] t in
327 let status, src, tgt, cpos, arity =
328 src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt in
330 basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status