]> matita.cs.unibo.it Git - helm.git/blob - matita/components/ng_refiner/nCicMetaSubst.ml
- support for candidates of reducibility continues ...
[helm.git] / matita / components / ng_refiner / nCicMetaSubst.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 (* $Id$ *)
13
14 let debug = ref false;;
15 let indent = ref "";;
16 let times = ref [];;
17 let pp s =
18  if !debug then
19   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
20 ;;
21 let inside c =
22  if !debug then
23   begin
24    let time1 = Unix.gettimeofday () in
25    indent := !indent ^ String.make 1 c;
26    times := time1 :: !times;
27    prerr_endline ("{{{" ^ !indent ^ " ")
28   end
29 ;;
30 let outside exc_opt =
31  if !debug then
32   begin
33    let time2 = Unix.gettimeofday () in
34    let time1 =
35     match !times with time1::tl -> times := tl; time1 | [] -> assert false in
36    prerr_endline ("}}} " ^ string_of_float (time2 -. time1));
37    (match exc_opt with
38    | Some e ->  prerr_endline ("exception raised: " ^ Printexc.to_string e)
39    | None -> ());
40    try
41     indent := String.sub !indent 0 (String.length !indent -1)
42    with
43     Invalid_argument _ -> indent := "??"; ()
44   end
45 ;;
46
47 exception MetaSubstFailure of string Lazy.t
48 exception Uncertain of string Lazy.t
49
50 let newmeta,maxmeta = 
51   let maxmeta = ref 0 in
52   (fun () -> incr maxmeta; !maxmeta),
53   (fun () -> !maxmeta)
54 ;;
55
56 exception NotFound of [`NotInTheList | `NotWellTyped];;
57
58 let position to_skip n (shift, lc) =
59   match lc with
60   | NCic.Irl len when n <= shift + to_skip || n > shift + len ->
61      raise (NotFound `NotInTheList)
62   | NCic.Irl _ -> n - shift
63   | NCic.Ctx tl ->
64       let rec aux to_skip k = function 
65          | [] -> raise (NotFound `NotInTheList)
66          | _ :: tl when to_skip > 0 -> aux (to_skip - 1) (k+1) tl
67          | (NCic.Rel m)::_ when m + shift = n -> k
68          | _::tl -> aux to_skip (k+1) tl 
69       in
70        aux to_skip 1 tl
71 ;;
72
73 let pack_lc orig = 
74   let rec are_contiguous k = function
75     | [] -> true
76     | (NCic.Rel j) :: tl when j = k+1 -> are_contiguous j tl
77     | _ -> false
78   in
79   match orig with
80   | _, NCic.Ctx [] -> 0, NCic.Irl 0
81   | shift, NCic.Ctx (NCic.Rel k::tl as l) when are_contiguous k tl ->
82       shift+k-1, NCic.Irl (List.length l)
83   | _ -> orig
84 ;;
85
86
87
88 let mk_perforated_irl shift len restrictions =
89   let rec aux n =
90     if n = 0 then [] else
91      if List.mem (n+shift) restrictions then aux (n-1)
92      else (NCic.Rel n) :: aux (n-1)
93   in
94     pack_lc (shift, NCic.Ctx (List.rev (aux len)))
95 ;;
96
97 exception Occur;;
98
99 let purge_restricted restrictions more_restrictions l =
100  if more_restrictions = [] then l
101  else
102   begin
103    pp (lazy ("TO BE RESTRICTED: " ^ 
104     (String.concat "," (List.map string_of_int restrictions))));
105    pp (lazy ("MORE RESTRICTIONS: " ^ 
106     (String.concat "," (List.map string_of_int more_restrictions))));
107    let shift,lc = l in
108    let lc = NCicUtils.expand_local_context lc in
109     let rec aux n lc =
110      match lc with
111         [] -> []
112       | _ when List.mem n restrictions -> aux (n+1) lc
113       | _::tl when List.mem n more_restrictions -> aux (n+1) tl
114       | he::tl -> he::aux (n+1) tl
115     in
116     pack_lc (shift, NCic.Ctx (aux 1 lc))
117   end
118 ;;
119
120 let rec force_does_not_occur status metasenv subst restrictions t =
121  let rec aux k ms = function
122     | NCic.Rel r when List.mem (r - k) restrictions -> raise Occur
123     | NCic.Rel r as orig ->
124         let amount = 
125           List.length (List.filter (fun x -> x < r - k) restrictions) 
126         in
127         if amount > 0 then ms, NCic.Rel (r - amount) else ms, orig
128     | NCic.Meta (n, (shift,lc as l)) as orig ->
129        (try
130          let _,_,bo,_ = NCicUtils.lookup_subst n subst in
131           aux k ms (NCicSubstitution.subst_meta status l bo)
132         with
133          NCicUtils.Subst_not_found _ ->
134           (* we ignore the subst since restrict will take care of already
135            * instantiated/restricted metavariabels *)
136           let l = NCicUtils.expand_local_context lc in
137           let sl = List.map (NCicSubstitution.lift status shift) l in 
138           let (metasenv,subst as ms), _, restrictions_for_n, l' =
139              List.fold_right
140                (fun t (ms, i, restrictions_for_n, l) ->
141                  try 
142               (*pp (lazy ("L'ORLO DELLA FOSSA: k= " ^ string_of_int k ^ " shift=" ^
143                string_of_int shift ^ " t=" ^ status#ppterm ~metasenv ~subst ~context:[] t));*)
144                    let ms, t = aux k ms t in
145               (*pp (lazy ("LA FOSSA: " ^ status#ppterm ~metasenv ~subst ~context:[] t));*)
146                    ms, i-1, restrictions_for_n, t::l
147                  with Occur ->
148                    ms, i-1, i::restrictions_for_n, l)
149                sl (ms, List.length l, [], [])
150           in
151           if restrictions_for_n = [] then
152             ms, if sl = l' then orig else (
153                 (*pp (lazy ("FINITO: " ^ status#ppterm ~metasenv:[] ~subst:[]
154                   ~context:[] (NCic.Meta (n,pack_lc (0, NCic.Ctx l')))));*)
155               NCic.Meta (n, pack_lc (0, NCic.Ctx l'))
156             )
157           else
158             let l' = pack_lc (0, NCic.Ctx l') in
159             let _ = pp (lazy ("restrictions for n are:" ^ String.concat "," (List.map string_of_int restrictions_for_n))) in
160             let metasenv, subst, newmeta, more_restricted = 
161               restrict status metasenv subst n restrictions_for_n in
162             let _ = pp (lazy ("more restricted: " ^String.concat "," (List.map string_of_int more_restricted))) in
163             let l' = purge_restricted restrictions more_restricted l' in
164               (metasenv, subst), NCic.Meta (newmeta, l'))
165     | t -> NCicUntrusted.map_term_fold_a status (fun _ k -> k+1) k aux ms t
166  in
167    aux 0 (metasenv,subst) t 
168
169 and force_does_not_occur_in_context status metasenv subst restrictions = function
170   | name, NCic.Decl t as orig ->
171       (* pp (lazy ("CCC: hd is" ^ status#ppterm ~metasenv:[] ~subst:[] ~context:[] t ^
172       "\nCCC: restrictions are:" ^ String.concat "," (List.map string_of_int restrictions)));*)
173       let (metasenv, subst), t' =
174         force_does_not_occur status metasenv subst restrictions t in
175       metasenv, subst, (if t == t' then orig else (name,NCic.Decl t'))
176   | name, NCic.Def (bo, ty) as orig ->
177       let (metasenv, subst), bo' =
178         force_does_not_occur status metasenv subst restrictions bo in
179       let (metasenv, subst), ty' =
180         force_does_not_occur status metasenv subst restrictions ty in
181       metasenv, subst, 
182        (if bo == bo' && ty == ty' then orig else (name, NCic.Def (bo', ty')))
183
184 and erase_in_context status metasenv subst pos restrictions = function
185   | [] -> metasenv, subst, restrictions, []
186   | hd::tl as orig ->
187       let metasenv, subst, restricted, tl' = 
188         erase_in_context status metasenv subst (pos+1) restrictions tl in
189       if List.mem pos restricted then
190         metasenv, subst, restricted, tl'
191       else
192         try
193           let metasenv, subst, hd' =
194             let delifted_restricted = 
195               List.map ((+) ~-pos) (List.filter ((<=) pos) restricted) in
196             force_does_not_occur_in_context 
197               status metasenv subst delifted_restricted hd
198           in
199            metasenv, subst, restricted, 
200             (if hd' == hd && tl' == tl then orig else (hd' :: tl'))
201         with Occur ->
202             metasenv, subst, (pos :: restricted), tl'
203
204 and restrict status metasenv subst i (restrictions as orig) =
205   assert (restrictions <> []);
206   try 
207     let name, ctx, bo, ty = NCicUtils.lookup_subst i subst in
208       try 
209         let metasenv, subst, restrictions, newctx = 
210           erase_in_context status metasenv subst 1 restrictions ctx in
211         let (metasenv, subst), newty =  
212           force_does_not_occur status metasenv subst restrictions ty in
213         let (metasenv, subst), newbo =  
214           force_does_not_occur status metasenv subst restrictions bo in
215         let j = newmeta () in
216         let subst_entry_j = j, (name, newctx, newbo, newty) in
217         let reloc_irl = mk_perforated_irl 0 (List.length ctx) restrictions in
218         let subst_entry_i = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in
219         let new_subst = 
220           subst_entry_j :: List.map 
221             (fun (n,_) as orig -> if i = n then subst_entry_i else orig) subst
222         in
223         let diff = List.filter (fun x -> not (List.mem x orig)) restrictions in
224         metasenv, new_subst, j, diff
225       with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf
226             ("Cannot restrict the context of the metavariable ?%d over "^^
227             "the hypotheses %s since ?%d is already instantiated "^^
228             "with %s and at least one of the hypotheses occurs in "^^
229             "the substituted term") i  (String.concat ", " 
230             (List.map (fun x -> fst (List.nth ctx (x-1))) restrictions)) i
231             (status#ppterm ~metasenv ~subst ~context:ctx bo))))
232   with NCicUtils.Subst_not_found _ -> 
233     try 
234       let name, ctx, ty = NCicUtils.lookup_meta i metasenv in
235       try
236         let metasenv, subst, restrictions, newctx = 
237           erase_in_context status metasenv subst 1 restrictions ctx in
238         let (metasenv, subst), newty =  
239           force_does_not_occur status metasenv subst restrictions ty in
240         let j = newmeta () in
241         let metasenv_entry = j, (name, newctx, newty) in
242         let reloc_irl = 
243           mk_perforated_irl 0 (List.length ctx) restrictions in
244         let subst_entry = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in
245          (* pp (lazy ("BBB: dopo1 \n" ^  NCicPp.ppsubst ~metasenv [subst_entry]));
246           pp (lazy ("BBB: dopo2 \n" ^  NCicPp.ppsubst ~metasenv (subst_entry::subst)));
247           pp (lazy ("BBB: dopo metasenv\n" ^  NCicPp.ppmetasenv ~subst [metasenv_entry]));*)
248         let diff = List.filter (fun x -> not (List.mem x orig)) restrictions in
249         List.map 
250           (fun (n,_) as orig -> if i = n then metasenv_entry else orig) 
251           metasenv,
252         subst_entry :: subst, j, diff
253       with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf
254           ("Cannot restrict the context of the metavariable ?%d "^^
255           "over the hypotheses %s since metavariable's type depends "^^
256           "on at least one of them") i (String.concat ", " 
257           (List.map (fun x -> fst (List.nth ctx (x-1))) restrictions)))))
258     with 
259     | NCicUtils.Meta_not_found _ -> assert false
260 ;;
261
262 let rec is_flexible status context ~subst = function 
263   | NCic.Meta (i,_) ->
264       (try 
265         let _,_,t,_ = List.assoc i subst in
266         is_flexible status context ~subst t
267       with Not_found -> true)
268   | NCic.Appl (NCic.Meta (i,_) :: args)-> 
269       (try 
270         let _,_,t,_ = List.assoc i subst in
271         is_flexible status context ~subst 
272           (NCicReduction.head_beta_reduce status ~delta:max_int 
273             (NCic.Appl (t :: args)))
274       with Not_found -> true)
275    (* this is a cheap whd, it only performs zeta-reduction.
276     * 
277     * it works when the **omissis** disambiguation algorithm
278     * is run on `let x := K a b in t`, K is substituted for a 
279     * ? and thus in t metavariables have a flexible Rel
280     *)
281   | NCic.Rel i ->
282       (try
283          match List.nth context (i-1)
284          with 
285          | _,NCic.Def (bo,_) ->
286                is_flexible status context ~subst
287                  (NCicSubstitution.lift status i bo)
288          | _ -> false
289       with 
290       | Failure _ -> 
291           prerr_endline (Printf.sprintf "Rel %d inside context:\n%s" i  
292             (status#ppcontext ~subst ~metasenv:[] context));
293           assert false
294       | Invalid_argument _ -> assert false)
295   | _ -> false
296 ;;
297
298 let is_out_scope = function `OutScope _ -> true | _ -> false;;
299 let is_out_scope_tag = List.exists is_out_scope;;
300 let int_of_out_scope_tag tag = 
301  match List.filter is_out_scope tag with [`OutScope n] -> n | _ -> assert false
302 ;;
303
304
305 exception Found;;
306 exception TypeNotGood;;
307
308 (* INVARIANT: we suppose that t is not another occurrence of Meta(n,_), 
309    otherwise the occur check does not make sense in case of unification
310    of ?n with ?n *)
311 let delift status ~unify metasenv subst context n l t =
312   (*D*)  inside 'D'; try let rc =  
313   let is_in_scope_meta subst = function
314     | NCic.Meta (i,_) ->
315         (try 
316            let tag, _, _, _ = NCicUtils.lookup_subst i subst in 
317             List.mem `InScope tag
318         with NCicUtils.Subst_not_found _ -> false)
319     | _ -> false
320   in
321   let contains_in_scope subst t = 
322     let rec aux _ () = function
323       | NCic.Meta _ as t ->
324           if is_in_scope_meta subst t then raise Found
325           else ()
326       | t -> 
327           if is_in_scope_meta subst t then raise Found
328           else NCicUtils.fold (fun _ () -> ()) () aux () t
329     in
330     try aux () () t; false with Found -> true
331   in
332   let unify_list in_scope = 
333     match l with
334     | _, NCic.Irl _ -> fun _ _ _ _ _ -> None
335     | shift, NCic.Ctx l -> fun metasenv subst context k t ->
336        if is_flexible status context ~subst t || contains_in_scope subst t then None else
337          let lb = 
338            List.map (fun t -> 
339             let t = NCicSubstitution.lift status (k+shift) t in
340             t, is_flexible status context ~subst t) 
341            l 
342          in
343          HExtlib.list_findopt
344           (fun (li,flexible) i ->
345             if flexible || i < in_scope then None else
346              match unify metasenv subst context li t with
347              | Some (metasenv,subst) -> 
348                  Some ((metasenv, subst), NCic.Rel (i+1+k))
349              | None -> None)
350           lb
351   in
352   let rec aux (context,k,in_scope) (metasenv, subst as ms) t = 
353    match unify_list in_scope metasenv subst context k t with
354    | Some x -> x
355    | None -> 
356     match t with 
357     | NCic.Rel n as t when n <= k -> ms, t
358     | NCic.Rel n -> 
359         (try
360           match List.nth context (n-1) with
361           | _,NCic.Def (bo,_) -> 
362                 (try ms, NCic.Rel ((position in_scope (n-k) l) + k)
363                  with (NotFound `NotInTheList) ->
364                 (* CSC: This bit of reduction hurts performances since it is
365                  * possible to  have an exponential explosion of the size of the
366                  * proof. required for nat/nth_prime.ma *)
367                   aux (context,k,in_scope) ms (NCicSubstitution.lift status n bo))
368           | _,NCic.Decl _ -> ms, NCic.Rel ((position in_scope (n-k) l) + k)
369         with Failure _ -> assert false) (*Unbound variable found in delift*)
370     | NCic.Meta (i,_) when i=n ->
371          raise (MetaSubstFailure (lazy (Printf.sprintf (
372            "Cannot unify the metavariable ?%d with a term that has "^^
373            "as subterm %s in which the same metavariable "^^
374            "occurs (occur check)") i 
375             (status#ppterm ~context ~metasenv ~subst t))))
376     | NCic.Meta (i,l1) as orig ->
377         (try
378            let tag,c,t,ty = NCicUtils.lookup_subst i subst in
379            let in_scope, clear = 
380             if List.mem `InScope tag then 0, true
381             else if is_out_scope_tag tag then int_of_out_scope_tag tag,true
382             else in_scope, false
383            in
384            let ms = 
385              if not clear then ms
386              else 
387                metasenv, 
388                (i,([],c,t,ty)) :: List.filter (fun j,_ -> i <> j) subst
389            in
390            aux (context,k,in_scope) ms (NCicSubstitution.subst_meta status l1 t)
391          with NCicUtils.Subst_not_found _ ->
392            if snd l1 = NCic.Irl 0 || snd l1 = NCic.Ctx [] then ms, orig
393            else
394               let shift1,lc1 = l1 in
395               let shift,lc = l in
396               let shift = shift + k in
397               match lc, lc1 with
398               | NCic.Irl len, NCic.Irl len1 
399                 when shift1 + len1 < shift || shift1 > shift + len ->
400                   let restrictions = HExtlib.list_seq 1 (len1 + 1) in
401                   let metasenv, subst, newmeta, more_restricted = 
402                    restrict status metasenv subst i restrictions in
403                   let l' = (0,NCic.Irl (max 0 (k-shift1))) in
404                   let l' = purge_restricted restrictions more_restricted l' in
405                   (metasenv, subst),NCic.Meta (newmeta,l')
406               | NCic.Irl len, NCic.Irl len1 ->
407                   let low_restrictions, new_shift = 
408                     if k <= shift1 && shift1 < shift then 
409                       HExtlib.list_seq 1 (shift - shift1 + 1), k
410                     else if shift1 < k (* <= shift *) then
411                       let save_below = k - shift1 in
412                       HExtlib.list_seq (save_below + 1) (shift - shift1 + 1),
413                       shift1
414                     else [], shift1 - shift + k
415                   in
416                   let high_restrictions = 
417                     let last = shift + len in
418                     let last1 = shift1 + len1 in
419                     if last1 > last then
420                       let high_gap = last1 - last in
421                       HExtlib.list_seq (len1 - high_gap + 1) (len1 + 1)
422                     else []
423                   in
424                   let restrictions = low_restrictions @ high_restrictions in
425                   if restrictions = [] then
426                     if shift = k then ms, orig
427                     else ms, NCic.Meta (i, (new_shift, lc1))
428                   else
429                     let metasenv, subst, newmeta, more_restricted = 
430                      restrict status metasenv subst i restrictions in
431                     let newlc_len = len1 - List.length restrictions in 
432                     let l' = new_shift, NCic.Irl newlc_len in
433                     let l' = purge_restricted restrictions more_restricted l' in
434                     (metasenv, subst),NCic.Meta(newmeta,l')
435
436               | _ ->
437                   let lc1 = NCicUtils.expand_local_context lc1 in
438                   let lc1 = List.map (NCicSubstitution.lift status shift1) lc1 in
439                   let rec deliftl tbr j ms = function
440                     | [] -> ms, tbr, []
441                     | t::tl ->
442                         let ms, tbr, tl = deliftl tbr (j+1) ms tl in
443                         try 
444                           let ms, t = aux (context,k,in_scope) ms t in 
445                           ms, tbr, t::tl
446                         with
447                         | (NotFound `NotInTheList) | MetaSubstFailure _ -> ms, j::tbr, tl
448                   in
449                   let (metasenv, subst), to_be_r, lc1' = deliftl [] 1 ms lc1 in
450                   pp (lazy ("TO BE RESTRICTED: " ^ 
451                    (String.concat "," (List.map string_of_int to_be_r))));
452                   let l1 = pack_lc (0, NCic.Ctx lc1') in
453                   pp (lazy ("newmeta:" ^ status#ppterm
454                    ~metasenv ~subst ~context (NCic.Meta (999,l1))));
455                   pp (lazy (status#ppmetasenv ~subst metasenv));
456                   if to_be_r = [] then
457                     (metasenv, subst), 
458                     (if lc1' = lc1 then orig else NCic.Meta (i,l1))
459                   else
460                     let metasenv, subst, newmeta, more_restricted = 
461                      restrict status metasenv subst i to_be_r in
462                     let l1 = purge_restricted to_be_r more_restricted l1 in
463                      (metasenv, subst), NCic.Meta(newmeta,l1))
464
465     | t -> 
466         NCicUntrusted.map_term_fold_a status
467           (fun e (c,k,s) -> (e::c,k+1,s)) (context,k,in_scope) aux ms t
468   in
469 (*
470   prerr_endline (
471     "DELIFTO " ^ status#ppterm ~metasenv ~subst ~context t ^ " w.r.t. " ^
472     status#ppterm ~metasenv ~subst ~context (NCic.Meta(n,l)) ^ " i.e. " ^
473     String.concat ", " (List.map (status#ppterm ~metasenv ~subst ~context) ( 
474       let shift, lc = l in
475       (List.map (NCicSubstitution.lift status shift) 
476         (NCicUtils.expand_local_context lc))
477   )));
478 *)
479    try
480 (*assert (try n = -1 or (ignore(NCicUtils.lookup_meta n metasenv); true) with NCicUtils.Meta_not_found _ -> false);*)
481     let ((metasenv,subst),t) as res = aux (context,0,0) (metasenv,subst) t in
482     if (try n <> -1 && (ignore(NCicUtils.lookup_meta n metasenv); false)
483         with NCicUtils.Meta_not_found _ -> true)
484     then
485      let _,context,bo,_ = NCicUtils.lookup_subst n subst in
486       match unify metasenv subst context bo t with
487          None -> raise (NotFound `NotWellTyped)
488        | Some (metasenv,subst) -> (metasenv,subst),t
489     else
490     (try
491       let _,context,ty = NCicUtils.lookup_meta n metasenv in
492       let ty' =
493        match t with
494           NCic.Sort _ -> (* could be algebraic *) NCic.Implicit `Closed
495         | _ -> NCicTypeChecker.typeof status ~subst ~metasenv context t in
496        (match ty,ty' with
497            NCic.Implicit _,_ ->
498             (match ty' with
499                 NCic.Sort _ | NCic.Meta _ | NCic.Implicit _ -> res
500               | _ -> raise TypeNotGood)
501          | _,NCic.Implicit _ ->
502             (match ty with
503                 NCic.Sort _ | NCic.Meta _ | NCic.Implicit _ -> res
504               | _ -> raise TypeNotGood)
505          | _ ->
506            if
507             NCicReduction.are_convertible status ~metasenv ~subst context ty' ty
508            then
509             res
510            else
511             raise TypeNotGood)
512      with
513         NCicUtils.Meta_not_found _ ->
514          (* Fake metavariable used in NTacStatus and NCicRefiner :-( *)
515          assert (n = -1); res
516       | TypeNotGood
517       | NCicTypeChecker.AssertFailure _
518       | NCicReduction.AssertFailure _
519       | NCicTypeChecker.TypeCheckerFailure _ ->
520          raise (NotFound `NotWellTyped))
521    with NotFound reason ->
522       (* This is the case where we fail even first order unification. *)
523       (* The reason is that our delift function is weaker than first  *)
524       (* order (in the sense of alpha-conversion). See comment above  *)
525       (* related to the delift function.                              *)
526       let reason =
527        match reason with
528           `NotInTheList -> "some variable cannot be delifted"
529         | `NotWellTyped -> "the unifier found is not well typed" in
530       let msg = (lazy (Printf.sprintf
531         ("Error trying to abstract %s over [%s]: %s")
532         (status#ppterm ~metasenv ~subst
533         ~context t) (String.concat "; " (List.map (status#ppterm ~metasenv
534         ~subst ~context) (let shift, lc = l in List.map (NCicSubstitution.lift
535         status shift) (NCicUtils.expand_local_context lc)))) reason))
536       in
537       let shift, lc = l in
538       let lc = NCicUtils.expand_local_context lc in
539       let l = List.map (NCicSubstitution.lift status shift) lc in
540        if
541         List.exists (fun t-> NCicUntrusted.metas_of_term status subst context t <> [])l
542        then
543         raise (Uncertain msg)
544        else
545         raise (MetaSubstFailure msg)
546  (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
547 ;;
548
549 let mk_meta ?(attrs=[]) metasenv context ?with_type kind = 
550   assert(kind <> `IsSort || context = []);
551   let n = newmeta () in
552   let ty= match with_type with None-> NCic.Implicit (`Typeof n)| Some x ->x in
553   let len = List.length context in
554   let attrs = NCicUntrusted.set_kind kind attrs in
555   let menv_entry = (n, (attrs, context, ty)) in
556   menv_entry :: metasenv, n, NCic.Meta (n, (0,NCic.Irl len)), ty
557 ;;
558
559 let extend_meta metasenv n =
560  try
561   let attrs,cc,ty = NCicUtils.lookup_meta n metasenv in 
562   (match ty with 
563   | NCic.Implicit (`Typeof _) -> 
564       let mk_meta context kind =
565         let metasenv, _, ty, _ = mk_meta metasenv context kind in
566         (n, (attrs, cc, ty)) :: List.filter (fun x,_ -> x <> n) metasenv, ty
567       in
568       (match NCicUntrusted.kind_of_meta attrs with
569        | `IsSort 
570        | `IsType -> mk_meta [] `IsSort
571        | `IsTerm -> mk_meta cc `IsType)
572   | ty -> metasenv, ty)
573  with NCicUtils.Meta_not_found _ -> assert false
574 ;;
575
576 let saturate status ?(delta=0) metasenv subst context ty goal_arity =
577  assert (goal_arity >= 0);
578   let rec aux metasenv = function
579    | NCic.Prod (name,s,t) as ty ->
580        let metasenv1, _, arg,_ = 
581           mk_meta ~attrs:[`Name name] metasenv context ~with_type:s `IsTerm in
582        let t, metasenv1, args, pno = 
583            aux metasenv1 (NCicSubstitution.subst status arg t) 
584        in
585        if pno + 1 = goal_arity then
586          ty, metasenv, [], goal_arity+1
587        else
588          t, metasenv1, arg::args, pno+1
589    | ty ->
590         match NCicReduction.whd status ~subst context ty ~delta with
591         | NCic.Prod _ as ty -> aux metasenv ty
592         | ty -> ty, metasenv, [], 0
593   in
594   let res, newmetasenv, arguments, _ = aux metasenv ty in
595   res, newmetasenv, arguments
596 ;;