]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_unification/cicMetaSubst.ml
rebuilt
[helm.git] / helm / ocaml / cic_unification / cicMetaSubst.ml
1
2 open Printf
3
4 exception AssertFailure of string
5 exception MetaSubstFailure of string
6
7 let debug_print = prerr_endline
8
9 type substitution = (int * Cic.term) list
10
11 (*** Functions to apply a substitution ***)
12
13 let apply_subst_gen ~appl_fun subst term =
14  let rec um_aux =
15   let module C = Cic in
16   let module S = CicSubstitution in 
17    function
18       C.Rel _ as t -> t
19     | C.Var _  as t -> t
20     | C.Meta (i, l) -> 
21         (try
22           let t = List.assoc i subst in
23           um_aux (S.lift_meta l t)
24         with Not_found -> (* not constrained variable, i.e. free in subst*)
25           let l' =
26             List.map (function None -> None | Some t -> Some (um_aux t)) l
27           in
28            C.Meta (i,l'))
29     | C.Sort _ as t -> t
30     | C.Implicit _ -> assert false
31     | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
32     | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
33     | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
34     | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t)
35     | C.Appl (hd :: tl) -> appl_fun um_aux hd tl
36     | C.Appl _ -> assert false
37     | C.Const (uri,exp_named_subst) ->
38        let exp_named_subst' =
39          List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
40        in
41        C.Const (uri, exp_named_subst')
42     | C.MutInd (uri,typeno,exp_named_subst) ->
43        let exp_named_subst' =
44          List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
45        in
46        C.MutInd (uri,typeno,exp_named_subst')
47     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
48        let exp_named_subst' =
49          List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
50        in
51        C.MutConstruct (uri,typeno,consno,exp_named_subst')
52     | C.MutCase (sp,i,outty,t,pl) ->
53        let pl' = List.map um_aux pl in
54        C.MutCase (sp, i, um_aux outty, um_aux t, pl')
55     | C.Fix (i, fl) ->
56        let fl' =
57          List.map (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo)) fl
58        in
59        C.Fix (i, fl')
60     | C.CoFix (i, fl) ->
61        let fl' =
62          List.map (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo)) fl
63        in
64        C.CoFix (i, fl')
65  in
66  um_aux term
67 ;;
68
69 let apply_subst =
70   let appl_fun um_aux he tl =
71     let tl' = List.map um_aux tl in
72       begin
73        match um_aux he with
74           Cic.Appl l -> Cic.Appl (l@tl')
75         | he' -> Cic.Appl (he'::tl')
76       end
77   in
78   apply_subst_gen ~appl_fun
79 ;;
80
81 (* apply_subst_reducing subst (Some (mtr,reductions_no)) t              *)
82 (* performs as (apply_subst subst t) until it finds an application of   *)
83 (* (META [meta_to_reduce]) that, once unwinding is performed, creates   *)
84 (* a new beta-redex; in this case up to [reductions_no] consecutive     *)
85 (* beta-reductions are performed.                                       *)
86 (* Hint: this function is usually called when [reductions_no]           *)
87 (*  eta-expansions have been performed and the head of the new          *)
88 (*  application has been unified with (META [meta_to_reduce]):          *)
89 (*  during the unwinding the eta-expansions are undone.                 *)
90
91 let apply_subst_reducing meta_to_reduce =
92   let appl_fun um_aux he tl =
93     let tl' = List.map um_aux tl in
94     let t' =
95      match um_aux he with
96         Cic.Appl l -> Cic.Appl (l@tl')
97       | he' -> Cic.Appl (he'::tl')
98     in
99      begin
100       match meta_to_reduce, he with
101          Some (mtr,reductions_no), Cic.Meta (m,_) when m = mtr ->
102           let rec beta_reduce =
103            function
104               (n,(Cic.Appl (Cic.Lambda (_,_,t)::he'::tl'))) when n > 0 ->
105                 let he'' = CicSubstitution.subst he' t in
106                  if tl' = [] then
107                   he''
108                  else
109                   beta_reduce (n-1,Cic.Appl(he''::tl'))
110             | (_,t) -> t
111           in
112            beta_reduce (reductions_no,t')
113        | _,_ -> t'
114      end
115   in
116   apply_subst_gen ~appl_fun
117
118 let rec apply_subst_context subst context =
119   List.fold_right
120     (fun item context ->
121       match item with
122       | Some (n, Cic.Decl t) ->
123           let t' = apply_subst subst t in
124           Some (n, Cic.Decl t') :: context
125       | Some (n, Cic.Def (t, ty)) ->
126           let ty' =
127             match ty with
128             | None -> None
129             | Some ty -> Some (apply_subst subst ty)
130           in
131           let t' = apply_subst subst t in
132           Some (n, Cic.Def (t', ty')) :: context
133       | None -> None :: context)
134     context []
135
136 let apply_subst_metasenv subst metasenv =
137   List.map
138     (fun (n, context, ty) ->
139       (n, apply_subst_context subst context, apply_subst subst ty))
140     (List.filter
141       (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
142       metasenv)
143
144 (***** Pretty printing functions ******)
145
146 let ppsubst subst =
147   String.concat "\n"
148     (List.map
149       (fun (idx, term) -> Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
150       subst)
151 ;;
152
153 let ppterm subst term = CicPp.ppterm (apply_subst subst term)
154
155 let ppterm_in_context subst term name_context =
156  CicPp.pp (apply_subst subst term) name_context
157
158 let ppcontext' ?(sep = "\n") subst context =
159  let separate s = if s = "" then "" else s ^ sep in
160   List.fold_right 
161    (fun context_entry (i,name_context) ->
162      match context_entry with
163         Some (n,Cic.Decl t) ->
164          sprintf "%s%s : %s" (separate i) (CicPp.ppname n)
165           (ppterm_in_context subst t name_context), (Some n)::name_context
166       | Some (n,Cic.Def (bo,ty)) ->
167          sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n)
168           (match ty with
169               None -> "_"
170             | Some ty -> ppterm_in_context subst ty name_context)
171           (ppterm_in_context subst bo name_context), (Some n)::name_context
172        | None ->
173           sprintf "%s_ :? _" (separate i), None::name_context
174     ) context ("",[])
175
176 let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context)
177
178 let ppmetasenv ?(sep = "\n") metasenv subst =
179   String.concat sep
180     (List.map
181       (fun (i, c, t) ->
182         let context,name_context = ppcontext' ~sep:"; " subst c in
183          sprintf "%s |- ?%d: %s" context i
184           (ppterm_in_context subst t name_context))
185       (List.filter
186         (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
187         metasenv))
188
189 (* From now on we recreate a kernel abstraction where substitutions are part of
190  * the calculus *)
191
192 let lift subst n term =
193   let term = apply_subst subst term in
194   try
195     CicSubstitution.lift n term
196   with e ->
197     raise (MetaSubstFailure ("Lift failure: " ^ Printexc.to_string e))
198
199 let subst subst t1 t2 =
200   let t1 = apply_subst subst t1 in
201   let t2 = apply_subst subst t2 in
202   try
203     CicSubstitution.subst t1 t2
204   with e ->
205     raise (MetaSubstFailure ("Subst failure: " ^ Printexc.to_string e))
206
207 let whd subst context term =
208   let term = apply_subst subst term in
209   let context = apply_subst_context subst context in
210   try
211     CicReduction.whd context term
212   with e ->
213     raise (MetaSubstFailure ("Weak head reduction failure: " ^
214       Printexc.to_string e))
215
216 let are_convertible subst context t1 t2 =
217   let context = apply_subst_context subst context in
218   let t1 = apply_subst subst t1 in
219   let t2 = apply_subst subst t2 in
220   CicReduction.are_convertible context t1 t2
221
222 let tempi_type_of_aux_subst = ref 0.0;;
223 let tempi_type_of_aux = ref 0.0;;
224
225 let type_of_aux' metasenv subst context term =
226 let time1 = Unix.gettimeofday () in
227   let term = apply_subst subst term in
228   let context = apply_subst_context subst context in
229   let metasenv =
230     List.map
231       (fun (i, c, t) -> (i, apply_subst_context subst c, apply_subst subst t))
232       (List.filter
233         (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
234         metasenv)
235   in
236 let time2 = Unix.gettimeofday () in
237 let res =
238   try
239     CicTypeChecker.type_of_aux' metasenv context term
240   with CicTypeChecker.TypeCheckerFailure msg ->
241     raise (MetaSubstFailure ("Type checker failure: " ^ msg))
242 in
243 let time3 = Unix.gettimeofday () in
244  tempi_type_of_aux_subst := !tempi_type_of_aux_subst +. time3 -. time1 ; 
245  tempi_type_of_aux := !tempi_type_of_aux +. time2 -. time1 ; 
246  res
247
248 (**** DELIFT ****)
249 (* the delift function takes in input a metavariable index, an ordered list of
250  * optional terms [t1,...,tn] and a term t, and substitutes every tk = Some
251  * (rel(nk)) with rel(k).  Typically, the list of optional terms is the explicit
252  * substitution that is applied to a metavariable occurrence and the result of
253  * the delift function is a term the implicit variable can be substituted with
254  * to make the term [t] unifiable with the metavariable occurrence.  In general,
255  * the problem is undecidable if we consider equivalence in place of alpha
256  * convertibility. Our implementation, though, is even weaker than alpha
257  * convertibility, since it replace the term [tk] if and only if [tk] is a Rel
258  * (missing all the other cases). Does this matter in practice?
259  * The metavariable index is the index of the metavariable that must not occur
260  * in the term (for occur check).
261  *)
262
263 exception NotInTheList;;
264
265 let position n =
266   let rec aux k =
267    function 
268        [] -> raise NotInTheList
269      | (Some (Cic.Rel m))::_ when m=n -> k
270      | _::tl -> aux (k+1) tl in
271   aux 1
272 ;;
273
274 exception Occur;;
275
276 let rec force_does_not_occur subst to_be_restricted t =
277  let module C = Cic in
278  let more_to_be_restricted = ref [] in
279  let rec aux k = function
280       C.Rel r when List.mem (r - k) to_be_restricted -> raise Occur
281     | C.Rel _
282     | C.Sort _ as t -> t
283     | C.Implicit _ -> assert false
284     | C.Meta (n, l) ->
285        (* we do not retrieve the term associated to ?n in subst since *)
286        (* in this way we can restrict if something goes wrong         *)
287        let l' =
288          let i = ref 0 in
289          List.map
290            (function t ->
291              incr i ;
292              match t with
293                 None -> None
294               | Some t ->
295                  try
296                    Some (aux k t)
297                  with Occur ->
298                    more_to_be_restricted := (n,!i) :: !more_to_be_restricted;
299                    None)
300            l
301        in
302         C.Meta (n, l')
303     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
304     | C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest)
305     | C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest)
306     | C.LetIn (name,so,dest) -> C.LetIn (name, aux k so, aux (k+1) dest)
307     | C.Appl l -> C.Appl (List.map (aux k) l)
308     | C.Var (uri,exp_named_subst) ->
309         let exp_named_subst' =
310           List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
311         in
312         C.Var (uri, exp_named_subst')
313     | C.Const (uri, exp_named_subst) ->
314         let exp_named_subst' =
315           List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
316         in
317         C.Const (uri, exp_named_subst')
318     | C.MutInd (uri,tyno,exp_named_subst) ->
319         let exp_named_subst' =
320           List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
321         in
322         C.MutInd (uri, tyno, exp_named_subst')
323     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
324         let exp_named_subst' =
325           List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
326         in
327         C.MutConstruct (uri, tyno, consno, exp_named_subst')
328     | C.MutCase (uri,tyno,out,te,pl) ->
329         C.MutCase (uri, tyno, aux k out, aux k te, List.map (aux k) pl)
330     | C.Fix (i,fl) ->
331        let len = List.length fl in
332        let k_plus_len = k + len in
333        let fl' =
334          List.map
335           (fun (name,j,ty,bo) -> (name, j, aux k ty, aux k_plus_len bo)) fl
336        in
337        C.Fix (i, fl')
338     | C.CoFix (i,fl) ->
339        let len = List.length fl in
340        let k_plus_len = k + len in
341        let fl' =
342          List.map
343           (fun (name,ty,bo) -> (name, aux k ty, aux k_plus_len bo)) fl
344        in
345        C.CoFix (i, fl')
346  in
347  let res = aux 0 t in
348  (!more_to_be_restricted, res)
349  
350 let rec restrict subst to_be_restricted metasenv =
351   let names_of_context_indexes context indexes =
352     String.concat ", "
353       (List.map
354         (fun i ->
355           try
356            match List.nth context i with
357            | None -> assert false
358            | Some (n, _) -> CicPp.ppname n
359           with
360            Failure _ -> assert false
361         ) indexes)
362   in
363   let force_does_not_occur_in_context to_be_restricted = function
364     | None -> [], None
365     | Some (name, Cic.Decl t) ->
366         let (more_to_be_restricted, t') =
367           force_does_not_occur subst to_be_restricted t
368         in
369         more_to_be_restricted, Some (name, Cic.Decl t')
370     | Some (name, Cic.Def (bo, ty)) ->
371         let (more_to_be_restricted, bo') =
372           force_does_not_occur subst to_be_restricted bo
373         in
374         let more_to_be_restricted, ty' =
375           match ty with
376           | None ->  more_to_be_restricted, None
377           | Some ty ->
378               let more_to_be_restricted', ty' =
379                 force_does_not_occur subst to_be_restricted ty
380               in
381               more_to_be_restricted @ more_to_be_restricted',
382               Some ty'
383         in
384         more_to_be_restricted, Some (name, Cic.Def (bo', ty'))
385   in
386   let rec erase i to_be_restricted n = function
387     | [] -> [], to_be_restricted, []
388     | hd::tl ->
389         let more_to_be_restricted,restricted,tl' =
390          erase (i+1) to_be_restricted n tl
391         in
392         let restrict_me = List.mem i restricted in
393         if restrict_me then
394          more_to_be_restricted, restricted, None:: tl'
395         else
396           (try
397             let more_to_be_restricted', hd' =
398               let delifted_restricted =
399                let rec aux =
400                 function
401                    [] -> []
402                  | j::tl when j > i -> (j - i)::aux tl
403                  | _::tl -> aux tl
404                in
405                 aux restricted
406               in
407                force_does_not_occur_in_context delifted_restricted hd
408             in
409              more_to_be_restricted @ more_to_be_restricted',
410              restricted, hd' :: tl'
411           with Occur ->
412             more_to_be_restricted, (i :: restricted), None :: tl')
413   in
414   let (more_to_be_restricted, metasenv, subst) =
415     List.fold_right
416       (fun (n, context, t) (more, metasenv, subst) ->
417         let to_be_restricted =
418           List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
419         in
420         let (more_to_be_restricted, restricted, context') =
421          (* just an optimization *)
422          if to_be_restricted = [] then
423           [],[],context
424          else
425           erase 1 to_be_restricted n context
426         in
427         try
428           let more_to_be_restricted', t' =
429             force_does_not_occur subst restricted t
430           in
431           let metasenv' = (n, context', t') :: metasenv in
432           (try
433             let s = List.assoc n subst in
434             try
435               let more_to_be_restricted'', s' =
436                 force_does_not_occur subst restricted s
437               in
438               let subst' = (n, s') :: (List.remove_assoc n subst) in
439               let more =
440                 more @ more_to_be_restricted @ more_to_be_restricted' @
441                   more_to_be_restricted''
442               in
443               (more, metasenv', subst')
444             with Occur ->
445               raise (MetaSubstFailure (sprintf
446                 "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term"
447                 n (names_of_context_indexes context to_be_restricted) n
448                 (ppterm subst s)))
449            with Not_found -> (more @ more_to_be_restricted @ more_to_be_restricted', metasenv', subst))
450         with Occur ->
451           raise (MetaSubstFailure (sprintf
452             "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them"
453             n (names_of_context_indexes context to_be_restricted))))
454       metasenv ([], [], subst)
455   in
456   match more_to_be_restricted with
457   | [] -> (metasenv, subst)
458   | _ -> restrict subst more_to_be_restricted metasenv
459 ;;
460
461 (*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)
462 let delift n subst context metasenv l t =
463  let module S = CicSubstitution in
464   let l =
465    let (_, canonical_context, _) = CicUtil.lookup_meta n metasenv in
466    List.map2 (fun ct lt ->
467      match (ct, lt) with
468      | None, _ -> None
469      | Some _, _ -> lt)
470      canonical_context l
471   in
472   let to_be_restricted = ref [] in
473   let rec deliftaux k =
474    let module C = Cic in
475     function
476        C.Rel m -> 
477          if m <=k then
478           C.Rel m   (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *)
479                     (*CSC: deliftato la regola per il LetIn                 *)
480                     (*CSC: FALSO! La regola per il LetIn non lo fa          *)
481          else
482           (match List.nth context (m-k-1) with
483             Some (_,C.Def (t,_)) ->
484              (*CSC: Hmmm. This bit of reduction is not in the spirit of    *)
485              (*CSC: first order unification. Does it help or does it harm? *)
486              deliftaux k (S.lift m t)
487           | Some (_,C.Decl t) ->
488              C.Rel ((position (m-k) l) + k)
489           | None -> raise (MetaSubstFailure "RelToHiddenHypothesis"))
490      | C.Var (uri,exp_named_subst) ->
491         let exp_named_subst' =
492          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
493         in
494          C.Var (uri,exp_named_subst')
495      | C.Meta (i, l1) as t -> 
496         if i = n then
497           raise (MetaSubstFailure (sprintf
498             "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
499             i (ppterm subst t)))
500         else
501          (* I do not consider the term associated to ?i in subst since *)
502          (* in this way I can restrict if something goes wrong.        *)
503           let rec deliftl j =
504            function
505               [] -> []
506             | None::tl -> None::(deliftl (j+1) tl)
507             | (Some t)::tl ->
508                let l1' = (deliftl (j+1) tl) in
509                 try
510                  Some (deliftaux k t)::l1'
511                 with
512                    NotInTheList
513                  | MetaSubstFailure _ ->
514                     to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
515           in
516            let l' = deliftl 1 l1 in
517             C.Meta(i,l')
518      | C.Sort _ as t -> t
519      | C.Implicit _ as t -> t
520      | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
521      | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
522      | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
523      | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
524      | C.Appl l -> C.Appl (List.map (deliftaux k) l)
525      | C.Const (uri,exp_named_subst) ->
526         let exp_named_subst' =
527          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
528         in
529          C.Const (uri,exp_named_subst')
530      | C.MutInd (uri,typeno,exp_named_subst) ->
531         let exp_named_subst' =
532          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
533         in
534          C.MutInd (uri,typeno,exp_named_subst')
535      | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
536         let exp_named_subst' =
537          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
538         in
539          C.MutConstruct (uri,typeno,consno,exp_named_subst')
540      | C.MutCase (sp,i,outty,t,pl) ->
541         C.MutCase (sp, i, deliftaux k outty, deliftaux k t,
542          List.map (deliftaux k) pl)
543      | C.Fix (i, fl) ->
544         let len = List.length fl in
545         let liftedfl =
546          List.map
547           (fun (name, i, ty, bo) ->
548            (name, i, deliftaux k ty, deliftaux (k+len) bo))
549            fl
550         in
551          C.Fix (i, liftedfl)
552      | C.CoFix (i, fl) ->
553         let len = List.length fl in
554         let liftedfl =
555          List.map
556           (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo))
557            fl
558         in
559          C.CoFix (i, liftedfl)
560   in
561    let res =
562     try
563      deliftaux 0 t
564     with
565      NotInTheList ->
566       (* This is the case where we fail even first order unification. *)
567       (* The reason is that our delift function is weaker than first  *)
568       (* order (in the sense of alpha-conversion). See comment above  *)
569       (* related to the delift function.                              *)
570 debug_print "!!!!!!!!!!! First Order UnificationFailure, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ;
571       raise (MetaSubstFailure (sprintf
572         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
573         (ppterm subst t)
574         (String.concat "; "
575           (List.map
576             (function Some t -> ppterm subst t | None -> "_")
577             l))))
578    in
579    let (metasenv, subst) = restrict subst !to_be_restricted metasenv in
580     res, metasenv, subst
581 ;;
582
583 (**** END OF DELIFT ****)
584
585
586 (** {2 Format-like pretty printers} *)
587
588 let fpp_gen ppf s =
589   Format.pp_print_string ppf s;
590   Format.pp_print_newline ppf ();
591   Format.pp_print_flush ppf ()
592
593 let fppsubst ppf subst = fpp_gen ppf (ppsubst subst)
594 let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term)
595 let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv metasenv [])
596