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 basic_eval_ncoercion (name,t,s,d,p,a) status =
135 NCicCoercion.look_for_coercion status [] [] [] skel_dummy s
138 NCicCoercion.look_for_coercion status [] [] [] d skel_dummy
140 let status = NCicCoercion.index_coercion status name t s d a p in
143 (function (_,_,NCic.Appl (x::_),_,_) -> x = t | _ -> assert false)
144 (NCicCoercion.look_for_coercion status [] [] [] s d)
146 let compose_names a b = a ^ "__o__" ^ b in
150 (fun (n1,m1,t1,_,j) (n,mc,c,_,i) ->
151 compose_names n1 n,m1@mc,c,[i,t1],j,a)
156 (fun (n,mc,c,_,j) (n1,m1,t1,ty,i) ->
157 compose_names n1 n,m1@mc,t1,[i,c],j,count_prod ty)
160 let to_s_o_c_o_from_d =
162 (fun (n1,m1,t1,_,j) (n,m,t,upl,i,a)->
163 compose_names n n1,m@m1,t,(i,t1)::upl,j,a)
166 to_s_o_c @ c_o_from_d @ to_s_o_c_o_from_d
170 (fun (name,metasenv, bo, upl, p, arity) ->
172 let metasenv, subst =
174 (fun (metasenv,subst) (a,b) ->
175 NCicUnification.unify status metasenv subst [] a b)
178 let bo = NCicUntrusted.apply_subst subst [] bo in
179 let metasenv = toposort metasenv in
180 let bo = close_in_context bo metasenv in
183 | NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv)
186 let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] bo in
187 let src,tgt = src_tgt_of_ty_cpos_arity ty pos arity in
188 let src = only_head src in
189 let tgt = only_head tgt in
192 NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] bo ^ " : " ^
193 NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty ^ " as " ^
194 NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
195 NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^
196 " cpos=" ^ string_of_int pos ^ " arity=" ^ string_of_int arity));
197 Some (name,bo,src,tgt,arity,pos)
199 | NCicTypeChecker.TypeCheckerFailure _
200 | NCicUnification.UnificationFailure _
201 | NCicUnification.Uncertain _ -> None
205 (fun st (name,t,s,d,a,p) -> NCicCoercion.index_coercion st name t s d a p)
209 let inject_ncoercion =
210 let basic_eval_ncoercion (name,t,s,d,p,a) ~refresh_uri_in_universe
213 let t = refresh_uri_in_term t in
214 let s = refresh_uri_in_term s in
215 let d = refresh_uri_in_term d in
216 basic_eval_ncoercion (name,t,s,d,p,a)
218 NRstatus.Serializer.register "ncoercion" basic_eval_ncoercion
221 let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
222 let status, src, cpos =
223 let rec aux cpos ctx = function
224 | NCic.Prod (name,ty,bo) ->
225 if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo
228 let metasenv,subst,status,src =
229 GrafiteDisambiguate.disambiguate_nterm
230 None status ctx [] [] ("",0,src) in
231 let src = NCicUntrusted.apply_subst subst [] src in
232 (* CHECK that the declared pattern matches the abstraction *)
233 let _ = NCicUnification.unify status metasenv subst ctx ty src in
234 let src = cleanup_skel () src in
237 | NCicUnification.UnificationFailure _
238 | NCicUnification.Uncertain _
239 | MultiPassDisambiguator.DisambiguationError _ ->
240 raise (GrafiteTypes.Command_error "bad source pattern"))
245 let status, tgt, arity =
246 let metasenv,subst,status,tgt =
247 GrafiteDisambiguate.disambiguate_nterm
248 None status [] [] [] ("",0,tgt) in
249 let tgt = NCicUntrusted.apply_subst subst [] tgt in
250 (* CHECK che sia unificabile mancante *)
251 let rec count_prod = function
252 | NCic.Prod (_,_,x) -> 1 + count_prod x
255 let arity = count_prod tgt in
257 if arity > 0 then cleanup_funclass_skel tgt
258 else cleanup_skel () tgt
262 status, src, tgt, cpos, arity
265 let basic_eval_and_inject_ncoercion infos status =
266 let status = basic_eval_ncoercion infos status in
267 let dump = inject_ncoercion infos::status#dump in
271 let basic_eval_and_inject_ncoercion_from_t_cpos_arity
272 status (name,t,cpos,arity)
274 let ty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] t in
275 let src,tgt = src_tgt_of_ty_cpos_arity ty cpos arity in
276 basic_eval_and_inject_ncoercion (name,t,src,tgt,cpos,arity) status
279 let eval_ncoercion status name t ty (id,src) tgt =
281 let metasenv,subst,status,ty =
282 GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,ty) in
283 assert (metasenv=[]);
284 let ty = NCicUntrusted.apply_subst subst [] ty in
285 let metasenv,subst,status,t =
286 GrafiteDisambiguate.disambiguate_nterm (Some ty) status [] [] [] ("",0,t) in
287 assert (metasenv=[]);
288 let t = NCicUntrusted.apply_subst subst [] t in
290 let status, src, tgt, cpos, arity =
291 src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt in
293 basic_eval_and_inject_ncoercion (name,t,src,tgt,cpos,arity) status