]> matita.cs.unibo.it Git - helm.git/blob - matita/components/grafite_engine/nCicCoercDeclaration.ml
one main property of lift closed
[helm.git] / matita / components / grafite_engine / nCicCoercDeclaration.ml
1 (*
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.                     
5     ||I||                                                                
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_______________________________________________________________ *)
11
12 (* let debug s = prerr_endline (Lazy.force s) ;;*)
13 let debug _ = ();;
14
15 let skel_dummy = NCic.Implicit `Type;;
16
17 let product f l1 l2 =
18   List.fold_left
19     (fun acc x ->
20       List.fold_left 
21         (fun acc y ->
22            f x y :: acc)
23         acc l2)
24     [] l1  
25 ;;
26
27 let pos_in_list x l =
28       match 
29         HExtlib.list_findopt (fun y i -> if y = x then Some i else None) l
30       with
31       | Some i -> i
32       | None -> assert false
33 ;;
34
35 let rec count_prod = function
36   | NCic.Prod (_,_,x) -> 1 + count_prod x
37   | _ -> 0
38 ;;
39
40 let term_at i t =
41   match t with
42   | NCic.Appl l -> 
43       (match 
44         HExtlib.list_findopt (fun y j -> if i+1=j then Some y else None) l
45       with
46       | Some i -> i
47       | None -> assert false)
48   | _ -> assert false
49 ;;
50
51 let rec cleanup_funclass_skel = function
52     | NCic.Prod (_,_,t) -> 
53         NCic.Prod ("_",skel_dummy, cleanup_funclass_skel t)
54     | _ -> skel_dummy
55 ;;
56
57 let src_tgt_of_ty_cpos_arity status 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
64   in
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
69   in
70   let mask t =
71     let rec aux () = function
72       | NCic.Meta _ 
73       | NCic.Implicit _ as x -> x
74       | NCic.Rel _ -> skel_dummy
75       | t -> NCicUtils.map status (fun _ () -> ()) () aux t
76     in
77      aux () t
78   in 
79   mask (pi_nth 0 cpos ty), 
80   mask (pi_tail 0 tpos ty)
81 ;;
82
83 let rec cleanup_skel status () = function
84   | NCic.Meta _ -> skel_dummy
85   | t -> NCicUtils.map status (fun _ () -> ()) () (cleanup_skel status) t
86 ;;
87
88 let close_in_context status 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 status (m_subst (List.length ctx)) ctx ty in
94         let m_subst m = 
95           (i,(tag,[],NCic.Rel (m-List.length ctx),ty))::(m_subst m)
96         in
97         NCic.Lambda (name, ty, aux m_subst subst ((name,NCic.Decl ty)::ctx) tl)
98    | [] -> 
99            (* STRONG ASSUMPTION: 
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 status subst ctx
104              (NCicSubstitution.lift status (List.length ctx) t)
105    | _ -> assert false
106   in
107   aux (fun _ -> []) [] [] metasenv
108 ;;
109
110 let toposort status metasenv = 
111   let module T = HTopoSort.Make(
112     struct type t = int * NCic.conjecture let compare (i,_) (j,_) = i-j end) 
113   in
114   let deps (_,(_,_,t)) =
115     List.filter (fun (j,_) -> 
116       List.mem j (NCicUntrusted.metas_of_term status [] [] t)) metasenv
117   in
118   T.topological_sort metasenv deps
119 ;;
120
121 let only_head = function
122   | NCic.Appl (h::tl) -> 
123       NCic.Appl (h :: HExtlib.mk_list skel_dummy (List.length tl))
124   | t -> t
125 ;;
126
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
132          else
133            (try 
134             let metasenv,subst,status,src =
135               GrafiteDisambiguate.disambiguate_nterm 
136                 status None ctx [] [] ("",0,src) in
137             let src = NCicUntrusted.apply_subst status 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 status () src in
141             status, src, cpos
142            with 
143            | NCicUnification.UnificationFailure _
144            | NCicUnification.Uncertain _
145            | MultiPassDisambiguator.DisambiguationError _ ->
146                raise (GrafiteTypes.Command_error "bad source pattern"))
147       | _ -> assert false
148     in
149       aux 0 [] ty
150   in
151   let status, tgt, arity = 
152     let metasenv,subst,status,tgt =
153       GrafiteDisambiguate.disambiguate_nterm 
154         status None [] [] [] ("",0,tgt) in
155     let tgt = NCicUntrusted.apply_subst status subst [] tgt in
156     (* CHECK che sia unificabile mancante *)
157     let rec count_prod = function
158       | NCic.Prod (_,_,x) -> 1 + count_prod x
159       | _ -> 0
160     in
161     let arity = count_prod tgt in
162     let tgt=
163       if arity > 0 then cleanup_funclass_skel tgt 
164       else cleanup_skel status () tgt 
165     in
166      status, tgt, arity
167   in
168   status, src, tgt, cpos, arity
169 ;;
170
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)
176   in
177    diverge (mk "") 0
178 ;;
179
180 exception Stop;;
181
182 let close_graph name t s d to_s from_d p a status =
183   let c =
184     List.find 
185      (function (_,_,NCic.Appl (x::_),_,_) -> x = t | _ -> assert false) 
186       (NCicCoercion.look_for_coercion status [] [] [] s d)
187   in
188   let compose_names a b = a ^ "__o__" ^ b in
189   let composites = 
190     let to_s_o_c = 
191       product 
192         (fun (n1,m1,t1,_,j) (n,mc,c,_,i) -> 
193           compose_names n1 n,m1@mc,c,[i,t1],j,a) 
194         to_s [c]
195     in
196     let c_o_from_d = 
197       product 
198         (fun (n,mc,c,_,j) (n1,m1,t1,ty,i) -> 
199           compose_names n n1,m1@mc,t1,[i,c],j,count_prod ty) 
200         [c] from_d
201     in
202     let to_s_o_c_o_from_d =
203       product 
204         (fun (n1,m1,t1,_,j) (n,m,t,upl,i,a)-> 
205           compose_names n1 n,m@m1,t,(i,t1)::upl,j,a)
206         to_s c_o_from_d
207     in
208     to_s_o_c @ c_o_from_d @ to_s_o_c_o_from_d
209   in
210   let composites =
211     HExtlib.filter_map
212      (fun (name,metasenv, bo, upl, p, arity) ->
213         try
214          let metasenv, subst = 
215            List.fold_left 
216             (fun (metasenv,subst) (a,b) ->
217                 NCicUnification.unify status metasenv subst [] a b)
218             (metasenv,[]) upl
219          in
220          let bo = NCicUntrusted.apply_subst status subst [] bo in
221          let p = NCicUntrusted.apply_subst status subst [] p in
222          let metasenv = NCicUntrusted.apply_subst_metasenv status subst metasenv in
223          let metasenv = toposort status metasenv in
224          let bo = close_in_context status bo metasenv in
225          let pos = 
226            match p with 
227            | NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv) 
228            | t -> raise Stop
229          in
230          let ty = NCicTypeChecker.typeof status ~metasenv:[] ~subst:[] [] bo in
231          let src,tgt = src_tgt_of_ty_cpos_arity status ty pos arity in
232          let src = only_head src in
233          let tgt = only_head tgt in
234          debug (lazy(
235            "composite " ^ name ^ ": "^
236            status#ppterm ~metasenv:[] ~subst:[] ~context:[] bo ^ " : " ^
237            status#ppterm ~metasenv:[] ~subst:[] ~context:[] ty ^ " as " ^
238            status#ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
239            status#ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^
240            " cpos=" ^ string_of_int pos ^ " arity=" ^ string_of_int arity));
241          let uri = fresh_uri status name ".con" in
242          let obj_kind = NCic.Constant 
243            ([],name,Some bo,ty,(`Generated,`Definition,`Coercion arity)) 
244          in
245          let height = NCicTypeChecker.height_of_obj_kind status uri [] obj_kind in
246          let obj = uri,height,[],[],obj_kind in
247          let c = 
248            NCic.Const 
249              (NReference.reference_of_spec uri (NReference.Def height))
250          in
251          Some (obj,name,c,src,tgt,pos,arity)
252        with 
253        | NCicTypeChecker.TypeCheckerFailure _
254        | NCicUnification.UnificationFailure _ 
255        | NCicUnification.Uncertain _ | Stop -> None
256      ) composites
257   in
258     composites
259 ;;
260
261 (* idempotent *)
262 let basic_index_ncoercion (name,_compose,t,s,d,position,arity) status =
263   NCicCoercion.index_coercion status name t s d arity position
264 ;;
265
266 let basic_eval_ncoercion (name,compose,t,s,d,p,a) status =
267   let to_s = 
268     NCicCoercion.look_for_coercion status [] [] [] skel_dummy s
269   in
270   let from_d = 
271     NCicCoercion.look_for_coercion status [] [] [] d skel_dummy
272   in
273   let status = NCicCoercion.index_coercion status name t s d a p in
274   let composites =
275    if compose then close_graph name t s d to_s from_d p a status else [] in
276   List.fold_left 
277     (fun (uris,infos,st) ((uri,_,_,_,_ as obj),name,t,s,d,p,a) -> 
278       let info = name,compose,t,s,d,p,a in
279       let st = NCicLibrary.add_obj st obj in
280       let st = basic_index_ncoercion info st in
281       uri::uris, info::infos, st)
282     ([],[],status) composites
283 ;;
284
285 let record_ncoercion =
286  let aux (name,compose,t,s,d,p,a) ~refresh_uri_in_term =
287   let t = refresh_uri_in_term t in
288   let s = refresh_uri_in_term s in
289   let d = refresh_uri_in_term d in
290    basic_index_ncoercion (name,compose,t,s,d,p,a)
291  in
292  let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term
293   ~refresh_uri_in_reference ~alias_only status
294  =
295   if not alias_only then
296    List.fold_right (aux ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))) l status
297   else
298    status
299  in
300   GrafiteTypes.Serializer.register#run "ncoercion" aux_l
301 ;;
302
303 let basic_eval_and_record_ncoercion infos status =
304  let uris, cinfos, status = basic_eval_ncoercion infos status in
305   NCicLibrary.dump_obj status (record_ncoercion (infos::cinfos)), uris
306 ;;
307
308 let basic_eval_and_record_ncoercion_from_t_cpos_arity 
309       status (name,compose,t,cpos,arity) 
310 =
311   let ty = NCicTypeChecker.typeof status ~subst:[] ~metasenv:[] [] t in
312   let src,tgt = src_tgt_of_ty_cpos_arity status ty cpos arity in
313   let status, uris =
314    basic_eval_and_record_ncoercion (name,compose,t,src,tgt,cpos,arity) status
315   in
316    status,uris
317 ;;
318
319 let eval_ncoercion (status: #GrafiteTypes.status) name compose t ty (id,src) tgt = 
320  let metasenv,subst,status,ty =
321   GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,ty) in
322  assert (metasenv=[]);
323  let ty = NCicUntrusted.apply_subst status subst [] ty in
324  let metasenv,subst,status,t =
325   GrafiteDisambiguate.disambiguate_nterm status (Some ty) [] [] [] ("",0,t) in
326  assert (metasenv=[]);
327  let t = NCicUntrusted.apply_subst status 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
330  let status, uris =
331   basic_eval_and_record_ncoercion (name,compose,t,src,tgt,cpos,arity) status
332  in
333   status,uris
334 ;;
335