]> matita.cs.unibo.it Git - helm.git/blob - matita/components/grafite_engine/nCicCoercDeclaration.ml
advancement in match
[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 msg
144            | NCicUnification.Uncertain msg ->
145                raise (GrafiteTypes.Command_error ("bad source pattern: " ^ 
146 Lazy.force msg))
147             | MultiPassDisambiguator.DisambiguationError _ ->
148                raise (GrafiteTypes.Command_error ("bad source pattern: 
149 disambiguation error")))
150       | _ -> assert false
151     in
152       aux 0 [] ty
153   in
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
162       | _ -> 0
163     in
164     let arity = count_prod tgt in
165     let tgt=
166       if arity > 0 then cleanup_funclass_skel tgt 
167       else cleanup_skel status () tgt 
168     in
169      status, tgt, arity
170   in
171   status, src, tgt, cpos, arity
172 ;;
173
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)
179   in
180    diverge (mk "") 0
181 ;;
182
183 exception Stop;;
184
185 let close_graph name t s d to_s from_d p a status =
186   let c =
187     List.find 
188      (function (_,_,NCic.Appl (x::_),_,_) -> x = t | _ -> assert false) 
189       (NCicCoercion.look_for_coercion status [] [] [] s d)
190   in
191   let compose_names a b = a ^ "__o__" ^ b in
192   let composites = 
193     let to_s_o_c = 
194       product 
195         (fun (n1,m1,t1,_,j) (n,mc,c,_,i) -> 
196           compose_names n1 n,m1@mc,c,[i,t1],j,a) 
197         to_s [c]
198     in
199     let c_o_from_d = 
200       product 
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) 
203         [c] from_d
204     in
205     let to_s_o_c_o_from_d =
206       product 
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)
209         to_s c_o_from_d
210     in
211     to_s_o_c @ c_o_from_d @ to_s_o_c_o_from_d
212   in
213   let composites =
214     HExtlib.filter_map
215      (fun (name,metasenv, bo, upl, p, arity) ->
216         try
217          let metasenv, subst = 
218            List.fold_left 
219             (fun (metasenv,subst) (a,b) ->
220                 NCicUnification.unify status metasenv subst [] a b)
221             (metasenv,[]) upl
222          in
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
228          let pos = 
229            match p with 
230            | NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv) 
231            | t -> raise Stop
232          in
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
237          debug (lazy(
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)) 
247          in
248          let height = NCicTypeChecker.height_of_obj_kind status uri [] obj_kind in
249          let obj = uri,height,[],[],obj_kind in
250          let c = 
251            NCic.Const 
252              (NReference.reference_of_spec uri (NReference.Def height))
253          in
254          Some (obj,name,c,src,tgt,pos,arity)
255        with 
256        | NCicTypeChecker.TypeCheckerFailure _
257        | NCicUnification.UnificationFailure _ 
258        | NCicUnification.Uncertain _ | Stop -> None
259      ) composites
260   in
261     composites
262 ;;
263
264 (* idempotent *)
265 let basic_index_ncoercion (name,_compose,t,s,d,position,arity) status =
266   NCicCoercion.index_coercion status name t s d arity position
267 ;;
268
269 let basic_eval_ncoercion (name,compose,t,s,d,p,a) status =
270   let to_s = 
271     NCicCoercion.look_for_coercion status [] [] [] skel_dummy s
272   in
273   let from_d = 
274     NCicCoercion.look_for_coercion status [] [] [] d skel_dummy
275   in
276   let status = NCicCoercion.index_coercion status name t s d a p in
277   let composites =
278    if compose then close_graph name t s d to_s from_d p a status else [] in
279   List.fold_left 
280     (fun (uris,infos,st) ((uri,_,_,_,_ as obj),name,t,s,d,p,a) -> 
281       let info = name,compose,t,s,d,p,a in
282       let st = NCicLibrary.add_obj st obj in
283       let st = basic_index_ncoercion info st in
284       uri::uris, info::infos, st)
285     ([],[],status) composites
286 ;;
287
288 let record_ncoercion =
289  let aux (name,compose,t,s,d,p,a) ~refresh_uri_in_term =
290   let t = refresh_uri_in_term t in
291   let s = refresh_uri_in_term s in
292   let d = refresh_uri_in_term d in
293    basic_index_ncoercion (name,compose,t,s,d,p,a)
294  in
295  let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term
296   ~refresh_uri_in_reference ~alias_only status
297  =
298   if not alias_only then
299    List.fold_right (aux ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))) l status
300   else
301    status
302  in
303   GrafiteTypes.Serializer.register#run "ncoercion" aux_l
304 ;;
305
306 let basic_eval_and_record_ncoercion infos status =
307  let uris, cinfos, status = basic_eval_ncoercion infos status in
308   NCicLibrary.dump_obj status (record_ncoercion (infos::cinfos)), uris
309 ;;
310
311 let basic_eval_and_record_ncoercion_from_t_cpos_arity 
312       status (name,compose,t,cpos,arity) 
313 =
314   let ty = NCicTypeChecker.typeof status ~subst:[] ~metasenv:[] [] t in
315   let src,tgt = src_tgt_of_ty_cpos_arity status ty cpos arity in
316   let status, uris =
317    basic_eval_and_record_ncoercion (name,compose,t,src,tgt,cpos,arity) status
318   in
319    status,uris
320 ;;
321
322 let eval_ncoercion (status: #GrafiteTypes.status) name compose t ty (id,src) tgt = 
323  let metasenv,subst,status,ty =
324   GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,ty) in
325  assert (metasenv=[]);
326  let ty = NCicUntrusted.apply_subst status subst [] ty in
327  let metasenv,subst,status,t =
328   GrafiteDisambiguate.disambiguate_nterm status (Some ty) [] [] [] ("",0,t) in
329  assert (metasenv=[]);
330  let t = NCicUntrusted.apply_subst status subst [] t in
331  let status, src, tgt, cpos, arity = 
332    src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt in
333  let status, uris =
334   basic_eval_and_record_ncoercion (name,compose,t,src,tgt,cpos,arity) status
335  in
336   status,uris
337 ;;
338