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
37 | NCic.Appl l -> pos_in_list x l
41 let rec count_prod = function
42 | NCic.Prod (_,_,x) -> 1 + count_prod x
50 HExtlib.list_findopt (fun y j -> if i+1=j then Some y else None) l
53 | None -> assert false)
57 let rec cleanup_funclass_skel = function
58 | NCic.Prod (_,_,t) ->
59 NCic.Prod ("_",skel_dummy, cleanup_funclass_skel t)
63 let src_tgt_of_ty_cpos_arity ty cpos arity =
64 let pis = count_prod ty in
65 let tpos = pis - arity in
66 let rec pi_nth i j = function
67 | NCic.Prod (_,s,_) when i = j -> s
68 | NCic.Prod (_,_,t) -> pi_nth (i+1) j t
69 | t -> assert (i = j); t
71 let rec pi_tail i j = function
72 | NCic.Prod (_,_,_) as t when i = j -> cleanup_funclass_skel t
73 | NCic.Prod (_,_,t) -> pi_tail (i+1) j t
74 | t -> assert (i = j); t
77 let rec aux () = function
79 | NCic.Implicit _ as x -> x
80 | NCic.Rel _ -> skel_dummy
81 | t -> NCicUtils.map (fun _ () -> ()) () aux t
85 mask (pi_nth 0 cpos ty),
86 mask (pi_tail 0 tpos ty)
89 let rec cleanup_skel () = function
90 | NCic.Meta _ -> skel_dummy
91 | t -> NCicUtils.map (fun _ () -> ()) () cleanup_skel t
94 let close_in_context t metasenv =
95 let rec aux m_subst subst ctx = function
96 | (i,(tag,[],ty)) :: tl ->
97 let name = "x" ^ string_of_int (List.length ctx) in
98 let subst = (i,(tag,[],NCic.Rel (List.length tl+1),ty))::subst in
99 let ty = NCicUntrusted.apply_subst (m_subst (List.length ctx)) ctx ty in
101 (i,(tag,[],NCic.Rel (m-List.length ctx),ty))::(m_subst m)
103 NCic.Lambda (name, ty, aux m_subst subst ((name,NCic.Decl ty)::ctx) tl)
105 (* STRONG ASSUMPTION:
106 since metas occurring in t have an empty context,
107 the substitution i build makes sense (i.e, the Rel
108 I pun in the subst will not be lifted by subst_meta *)
109 NCicUntrusted.apply_subst subst ctx
110 (NCicSubstitution.lift (List.length ctx) t)
113 aux (fun _ -> []) [] [] metasenv
116 let toposort metasenv =
117 let module T = HTopoSort.Make(
118 struct type t = int * NCic.conjecture let compare (i,_) (j,_) = i-j end)
120 let deps (_,(_,_,t)) =
121 List.filter (fun (j,_) ->
122 List.mem j (NCicUntrusted.metas_of_term [] [] t)) metasenv
124 T.topological_sort metasenv deps
127 let only_head = function
128 | NCic.Appl (h::tl) ->
129 NCic.Appl (h :: HExtlib.mk_list skel_dummy (List.length tl))
133 let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
134 let status, src, cpos =
135 let rec aux cpos ctx = function
136 | NCic.Prod (name,ty,bo) ->
137 if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo
140 let metasenv,subst,status,src =
141 GrafiteDisambiguate.disambiguate_nterm
142 None status ctx [] [] ("",0,src) in
143 let src = NCicUntrusted.apply_subst subst [] src in
144 (* CHECK that the declared pattern matches the abstraction *)
145 let _ = NCicUnification.unify status metasenv subst ctx ty src in
146 let src = cleanup_skel () src in
149 | NCicUnification.UnificationFailure _
150 | NCicUnification.Uncertain _
151 | MultiPassDisambiguator.DisambiguationError _ ->
152 raise (GrafiteTypes.Command_error "bad source pattern"))
157 let status, tgt, arity =
158 let metasenv,subst,status,tgt =
159 GrafiteDisambiguate.disambiguate_nterm
160 None status [] [] [] ("",0,tgt) in
161 let tgt = NCicUntrusted.apply_subst subst [] tgt in
162 (* CHECK che sia unificabile mancante *)
163 let rec count_prod = function
164 | NCic.Prod (_,_,x) -> 1 + count_prod x
167 let arity = count_prod tgt in
169 if arity > 0 then cleanup_funclass_skel tgt
170 else cleanup_skel () tgt
174 status, src, tgt, cpos, arity
177 let fresh_uri status prefix suffix =
178 let mk x = NUri.uri_of_string (status#baseuri ^ "/" ^ prefix ^ x ^ suffix) in
179 let rec diverge u i =
180 if NCicLibrary.aliases_of u = [] then u
181 else diverge (mk ("__" ^ string_of_int i)) (i+1)
187 let close_graph name t s d to_s from_d p a status =
190 (function (_,_,NCic.Appl (x::_),_,_) -> x = t | _ -> assert false)
191 (NCicCoercion.look_for_coercion status [] [] [] s d)
193 let compose_names a b = a ^ "__o__" ^ b in
197 (fun (n1,m1,t1,_,j) (n,mc,c,_,i) ->
198 compose_names n1 n,m1@mc,c,[i,t1],j,a)
203 (fun (n,mc,c,_,j) (n1,m1,t1,ty,i) ->
204 compose_names n1 n,m1@mc,t1,[i,c],j,count_prod ty)
207 let to_s_o_c_o_from_d =
209 (fun (n1,m1,t1,_,j) (n,m,t,upl,i,a)->
210 compose_names n n1,m@m1,t,(i,t1)::upl,j,a)
213 to_s_o_c @ c_o_from_d @ to_s_o_c_o_from_d
217 (fun (name,metasenv, bo, upl, p, arity) ->
219 let metasenv, subst =
221 (fun (metasenv,subst) (a,b) ->
222 NCicUnification.unify status metasenv subst [] a b)
225 let bo = NCicUntrusted.apply_subst subst [] bo in
226 let metasenv = toposort metasenv in
227 let bo = close_in_context bo metasenv in
230 | NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv)
233 let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] bo in
234 let src,tgt = src_tgt_of_ty_cpos_arity ty pos arity in
235 let src = only_head src in
236 let tgt = only_head tgt in
239 NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] bo ^ " : " ^
240 NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty ^ " as " ^
241 NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
242 NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^
243 " cpos=" ^ string_of_int pos ^ " arity=" ^ string_of_int arity));
244 let uri = fresh_uri status name ".con" in
245 let obj_kind = NCic.Constant
246 ([],name,Some bo,ty,(`Generated,`Definition,`Coercion arity))
248 let height = NCicTypeChecker.height_of_obj_kind uri [] obj_kind in
249 let obj = uri,height,[],[],obj_kind in
252 (NReference.reference_of_spec uri (NReference.Def height))
254 Some (obj,name,c,src,tgt,pos,arity)
256 | NCicTypeChecker.TypeCheckerFailure _
257 | NCicUnification.UnificationFailure _
258 | NCicUnification.Uncertain _ -> None
265 let basic_index_ncoercion (name,t,s,d,position,arity) status =
266 NCicCoercion.index_coercion status name t s d arity position
269 let basic_eval_ncoercion (name,t,s,d,p,a) status =
271 NCicCoercion.look_for_coercion status [] [] [] skel_dummy s
274 NCicCoercion.look_for_coercion status [] [] [] d skel_dummy
276 let status = NCicCoercion.index_coercion status name t s d a p in
277 let composites = close_graph name t s d to_s from_d p a status in
279 (fun (uris,infos,st) ((uri,_,_,_,_ as obj),name,t,s,d,p,a) ->
280 let info = name,t,s,d,p,a in
281 let st = NCicLibrary.add_obj st obj in
282 let st = basic_index_ncoercion info st in
283 uri::uris, info::infos, st)
284 ([],[],status) composites
287 let record_ncoercion =
288 let aux (name,t,s,d,p,a) ~refresh_uri_in_universe ~refresh_uri_in_term =
289 let t = refresh_uri_in_term t in
290 let s = refresh_uri_in_term s in
291 let d = refresh_uri_in_term d in
292 basic_index_ncoercion (name,t,s,d,p,a)
294 let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term =
295 List.fold_right (aux ~refresh_uri_in_universe ~refresh_uri_in_term) l
297 NRstatus.Serializer.register "ncoercion" aux_l
300 let basic_eval_and_record_ncoercion infos status =
301 let uris, cinfos, status = basic_eval_ncoercion infos status in
302 let dump = record_ncoercion (infos::cinfos) :: status#dump in
303 status#set_dump dump, uris
306 let basic_eval_and_record_ncoercion_from_t_cpos_arity
307 status (name,t,cpos,arity)
309 let ty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] t in
310 let src,tgt = src_tgt_of_ty_cpos_arity ty cpos arity in
312 basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status
317 let eval_ncoercion status name t ty (id,src) tgt =
319 let metasenv,subst,status,ty =
320 GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,ty) in
321 assert (metasenv=[]);
322 let ty = NCicUntrusted.apply_subst subst [] ty in
323 let metasenv,subst,status,t =
324 GrafiteDisambiguate.disambiguate_nterm (Some ty) status [] [] [] ("",0,t) in
325 assert (metasenv=[]);
326 let t = NCicUntrusted.apply_subst subst [] t in
328 let status, src, tgt, cpos, arity =
329 src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt in
331 basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status