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 (* TODO: all newast's must be returned to the caller in some way
13 * e.g. modifying the status? *)
15 (* let debug s = prerr_endline (Lazy.force s) ;;*)
18 let skel_dummy = NCic.Implicit `Type;;
32 HExtlib.list_findopt (fun y i -> if y = x then Some i else None) l
35 | None -> assert false
38 let rec count_prod = function
39 | NCic.Prod (_,_,x) -> 1 + count_prod x
47 HExtlib.list_findopt (fun y j -> if i+1=j then Some y else None) l
50 | None -> assert false)
54 let rec cleanup_funclass_skel = function
55 | NCic.Prod (_,_,t) ->
56 NCic.Prod ("_",skel_dummy, cleanup_funclass_skel t)
60 let src_tgt_of_ty_cpos_arity status ty cpos arity =
61 let pis = count_prod ty in
62 let tpos = pis - arity in
63 let rec pi_nth i j = function
64 | NCic.Prod (_,s,_) when i = j -> s
65 | NCic.Prod (_,_,t) -> pi_nth (i+1) j t
66 | t -> assert (i = j); t
68 let rec pi_tail i j = function
69 | NCic.Prod (_,_,_) as t when i = j -> cleanup_funclass_skel t
70 | NCic.Prod (_,_,t) -> pi_tail (i+1) j t
71 | t -> assert (i = j); t
74 let rec aux () = function
76 | NCic.Implicit _ as x -> x
77 | NCic.Rel _ -> skel_dummy
78 | t -> NCicUtils.map status (fun _ () -> ()) () aux t
82 mask (pi_nth 0 cpos ty),
83 mask (pi_tail 0 tpos ty)
86 let rec cleanup_skel status () = function
87 | NCic.Meta _ -> skel_dummy
88 | t -> NCicUtils.map status (fun _ () -> ()) () (cleanup_skel status) t
91 let close_in_context status t metasenv =
92 let rec aux m_subst subst ctx = function
93 | (i,(tag,[],ty)) :: tl ->
94 let name = "x" ^ string_of_int (List.length ctx) in
95 let subst = (i,(tag,[],NCic.Rel (List.length tl+1),ty))::subst in
96 let ty = NCicUntrusted.apply_subst status (m_subst (List.length ctx)) ctx ty in
98 (i,(tag,[],NCic.Rel (m-List.length ctx),ty))::(m_subst m)
100 NCic.Lambda (name, ty, aux m_subst subst ((name,NCic.Decl ty)::ctx) tl)
102 (* STRONG ASSUMPTION:
103 since metas occurring in t have an empty context,
104 the substitution i build makes sense (i.e, the Rel
105 I pun in the subst will not be lifted by subst_meta *)
106 NCicUntrusted.apply_subst status subst ctx
107 (NCicSubstitution.lift status (List.length ctx) t)
110 aux (fun _ -> []) [] [] metasenv
113 let toposort status metasenv =
114 let module T = HTopoSort.Make(
115 struct type t = int * NCic.conjecture let compare (i,_) (j,_) = i-j end)
117 let deps (_,(_,_,t)) =
118 List.filter (fun (j,_) ->
119 List.mem j (NCicUntrusted.metas_of_term status [] [] t)) metasenv
121 T.topological_sort metasenv deps
124 let only_head = function
125 | NCic.Appl (h::tl) ->
126 NCic.Appl (h :: HExtlib.mk_list skel_dummy (List.length tl))
130 let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
131 let status, src, cpos =
132 let rec aux cpos ctx = function
133 | NCic.Prod (name,ty,bo) ->
134 if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo
137 let metasenv,subst,status,src =
138 GrafiteDisambiguate.disambiguate_nterm
139 status None ctx [] [] ("",0,src) in
140 let src = NCicUntrusted.apply_subst status subst [] src in
141 (* CHECK that the declared pattern matches the abstraction *)
142 let _ = NCicUnification.unify status metasenv subst ctx ty src in
143 let src = cleanup_skel status () src in
146 | NCicUnification.UnificationFailure _
147 | NCicUnification.Uncertain _
148 | MultiPassDisambiguator.DisambiguationError _ ->
149 raise (GrafiteTypes.Command_error "bad source pattern"))
154 let status, tgt, arity =
155 let metasenv,subst,status,tgt =
156 GrafiteDisambiguate.disambiguate_nterm
157 status None [] [] [] ("",0,tgt) in
158 let tgt = NCicUntrusted.apply_subst status subst [] tgt in
159 (* CHECK che sia unificabile mancante *)
160 let rec count_prod = function
161 | NCic.Prod (_,_,x) -> 1 + count_prod x
164 let arity = count_prod tgt in
166 if arity > 0 then cleanup_funclass_skel tgt
167 else cleanup_skel status () tgt
171 status, src, tgt, cpos, arity
174 let fresh_uri status prefix suffix =
175 let mk x = NUri.uri_of_string (status#baseuri ^ "/" ^ prefix ^ x ^ suffix) in
176 let rec diverge u i =
177 if NCicLibrary.aliases_of u = [] then u
178 else diverge (mk ("__" ^ string_of_int i)) (i+1)
185 let close_graph name t s d to_s from_d p a status =
188 (function (_,_,NCic.Appl (x::_),_,_) -> x = t | _ -> assert false)
189 (NCicCoercion.look_for_coercion status [] [] [] s d)
191 let compose_names a b = a ^ "__o__" ^ b in
195 (fun (n1,m1,t1,_,j) (n,mc,c,_,i) ->
196 compose_names n1 n,m1@mc,c,[i,t1],j,a)
201 (fun (n,mc,c,_,j) (n1,m1,t1,ty,i) ->
202 compose_names n n1,m1@mc,t1,[i,c],j,count_prod ty)
205 let to_s_o_c_o_from_d =
207 (fun (n1,m1,t1,_,j) (n,m,t,upl,i,a)->
208 compose_names n1 n,m@m1,t,(i,t1)::upl,j,a)
211 to_s_o_c @ c_o_from_d @ to_s_o_c_o_from_d
215 (fun (name,metasenv, bo, upl, p, arity) ->
217 let metasenv, subst =
219 (fun (metasenv,subst) (a,b) ->
220 NCicUnification.unify status metasenv subst [] a b)
223 let bo = NCicUntrusted.apply_subst status subst [] bo in
224 let p = NCicUntrusted.apply_subst status subst [] p in
225 let metasenv = NCicUntrusted.apply_subst_metasenv status subst metasenv in
226 let metasenv = toposort status metasenv in
227 let bo = close_in_context status bo metasenv in
230 | NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv)
233 let ty = NCicTypeChecker.typeof status ~metasenv:[] ~subst:[] [] bo in
234 let src,tgt = src_tgt_of_ty_cpos_arity status ty pos arity in
235 let src = only_head src in
236 let tgt = only_head tgt in
238 "composite " ^ name ^ ": "^
239 status#ppterm ~metasenv:[] ~subst:[] ~context:[] bo ^ " : " ^
240 status#ppterm ~metasenv:[] ~subst:[] ~context:[] ty ^ " as " ^
241 status#ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
242 status#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 status 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 _ | Stop -> 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_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 ~refresh_uri_in_reference ~alias_only status
297 if not alias_only then
298 List.fold_right (aux ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))) l status
302 GrafiteTypes.Serializer.register#run "ncoercion" aux_l
305 let basic_eval_and_record_ncoercion infos status =
306 let uris, cinfos, status = basic_eval_ncoercion infos status in
307 NCicLibrary.dump_obj status (record_ncoercion (infos::cinfos)), uris
310 let basic_eval_and_record_ncoercion_from_t_cpos_arity
311 status (name,t,cpos,arity)
313 let ty = NCicTypeChecker.typeof status ~subst:[] ~metasenv:[] [] t in
314 let src,tgt = src_tgt_of_ty_cpos_arity status ty cpos arity in
316 basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status
321 let eval_ncoercion (status: #GrafiteTypes.status) name t ty (id,src) tgt =
322 let metasenv,subst,status,ty =
323 GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,ty) in
324 assert (metasenv=[]);
325 let ty = NCicUntrusted.apply_subst status subst [] ty in
326 let metasenv,subst,status,t =
327 GrafiteDisambiguate.disambiguate_nterm status (Some ty) [] [] [] ("",0,t) in
328 assert (metasenv=[]);
329 let t = NCicUntrusted.apply_subst status subst [] t in
330 let status, src, tgt, cpos, arity =
331 src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt in
333 basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status