]> matita.cs.unibo.it Git - helm.git/blob - matitaB/components/ng_refiner/nCicMetaSubst.ml
Debugging code commented out.
[helm.git] / matitaB / 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 NotInTheList;;
57
58 let position to_skip n (shift, lc) =
59   match lc with
60   | NCic.Irl _ when to_skip > 0 -> assert false  (* unclear to me *)
61   | NCic.Irl len when n <= shift || n > shift + len -> raise NotInTheList
62   | NCic.Irl _ -> n - shift
63   | NCic.Ctx tl ->
64       let rec aux to_skip k = function 
65          | [] -> raise 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
307 (* INVARIANT: we suppose that t is not another occurrence of Meta(n,_), 
308    otherwise the occur check does not make sense in case of unification
309    of ?n with ?n *)
310 let delift status ~unify metasenv subst context n l t =
311   (*D*)  inside 'D'; try let rc =  
312   let is_in_scope_meta subst = function
313     | NCic.Meta (i,_) ->
314         (try 
315            let tag, _, _, _ = NCicUtils.lookup_subst i subst in 
316             List.mem `InScope tag
317         with NCicUtils.Subst_not_found _ -> false)
318     | _ -> false
319   in
320   let contains_in_scope subst t = 
321     let rec aux _ () = function
322       | NCic.Meta _ as t ->
323           if is_in_scope_meta subst t then raise Found
324           else ()
325       | t -> 
326           if is_in_scope_meta subst t then raise Found
327           else NCicUtils.fold (fun _ () -> ()) () aux () t
328     in
329     try aux () () t; false with Found -> true
330   in
331   let unify_list in_scope = 
332     match l with
333     | _, NCic.Irl _ -> fun _ _ _ _ _ -> None
334     | shift, NCic.Ctx l -> fun metasenv subst context k t ->
335        if is_flexible status context ~subst t || contains_in_scope subst t then None else
336          let lb = 
337            List.map (fun t -> 
338             let t = NCicSubstitution.lift status (k+shift) t in
339             t, is_flexible status context ~subst t) 
340            l 
341          in
342          HExtlib.list_findopt
343           (fun (li,flexible) i ->
344             if flexible || i < in_scope then None else
345              match unify metasenv subst context li t with
346              | Some (metasenv,subst) -> 
347                  Some ((metasenv, subst), NCic.Rel (i+1+k))
348              | None -> None)
349           lb
350   in
351   let rec aux (context,k,in_scope) (metasenv, subst as ms) t = 
352    match unify_list in_scope metasenv subst context k t with
353    | Some x -> x
354    | None -> 
355     match t with 
356     | NCic.Rel n as t when n <= k -> ms, t
357     | NCic.Rel n -> 
358         (try
359           match List.nth context (n-1) with
360           | _,NCic.Def (bo,_) -> 
361                 (try ms, NCic.Rel ((position in_scope (n-k) l) + k)
362                  with NotInTheList ->
363                 (* CSC: This bit of reduction hurts performances since it is
364                  * possible to  have an exponential explosion of the size of the
365                  * proof. required for nat/nth_prime.ma *)
366                   aux (context,k,in_scope) ms (NCicSubstitution.lift status n bo))
367           | _,NCic.Decl _ -> ms, NCic.Rel ((position in_scope (n-k) l) + k)
368         with Failure _ -> assert false) (*Unbound variable found in delift*)
369     | NCic.Meta (i,_) when i=n ->
370          raise (MetaSubstFailure (lazy (Printf.sprintf (
371            "Cannot unify the metavariable ?%d with a term that has "^^
372            "as subterm %s in which the same metavariable "^^
373            "occurs (occur check)") i 
374             (status#ppterm ~context ~metasenv ~subst t))))
375     | NCic.Meta (i,l1) as orig ->
376         (try
377            let tag,c,t,ty = NCicUtils.lookup_subst i subst in
378            let in_scope, clear = 
379             if List.mem `InScope tag then 0, true
380             else if is_out_scope_tag tag then int_of_out_scope_tag tag,true
381             else in_scope, false
382            in
383            let ms = 
384              if not clear then ms
385              else 
386                metasenv, 
387                (i,([],c,t,ty)) :: List.filter (fun j,_ -> i <> j) subst
388            in
389            aux (context,k,in_scope) ms (NCicSubstitution.subst_meta status l1 t)
390          with NCicUtils.Subst_not_found _ ->
391            if snd l1 = NCic.Irl 0 || snd l1 = NCic.Ctx [] then ms, orig
392            else
393               let shift1,lc1 = l1 in
394               let shift,lc = l in
395               let shift = shift + k in
396               match lc, lc1 with
397               | NCic.Irl len, NCic.Irl len1 
398                 when shift1 + len1 < shift || shift1 > shift + len ->
399                   let restrictions = HExtlib.list_seq 1 (len1 + 1) in
400                   let metasenv, subst, newmeta, more_restricted = 
401                    restrict status metasenv subst i restrictions in
402                   let l' = (0,NCic.Irl (max 0 (k-shift1))) in
403                   let l' = purge_restricted restrictions more_restricted l' in
404                   (metasenv, subst),NCic.Meta (newmeta,l')
405               | NCic.Irl len, NCic.Irl len1 ->
406                   let low_restrictions, new_shift = 
407                     if k <= shift1 && shift1 < shift then 
408                       HExtlib.list_seq 1 (shift - shift1 + 1), k
409                     else if shift1 < k (* <= shift *) then
410                       let save_below = k - shift1 in
411                       HExtlib.list_seq (save_below + 1) (shift - shift1 + 1),
412                       shift1
413                     else [], shift1 - shift + k
414                   in
415                   let high_restrictions = 
416                     let last = shift + len in
417                     let last1 = shift1 + len1 in
418                     if last1 > last then
419                       let high_gap = last1 - last in
420                       HExtlib.list_seq (len1 - high_gap + 1) (len1 + 1)
421                     else []
422                   in
423                   let restrictions = low_restrictions @ high_restrictions in
424                   if restrictions = [] then
425                     if shift = k then ms, orig
426                     else ms, NCic.Meta (i, (new_shift, lc1))
427                   else
428                     let metasenv, subst, newmeta, more_restricted = 
429                      restrict status metasenv subst i restrictions in
430                     let newlc_len = len1 - List.length restrictions in 
431                     let l' = new_shift, NCic.Irl newlc_len in
432                     let l' = purge_restricted restrictions more_restricted l' in
433                     (metasenv, subst),NCic.Meta(newmeta,l')
434
435               | _ ->
436                   let lc1 = NCicUtils.expand_local_context lc1 in
437                   let lc1 = List.map (NCicSubstitution.lift status shift1) lc1 in
438                   let rec deliftl tbr j ms = function
439                     | [] -> ms, tbr, []
440                     | t::tl ->
441                         let ms, tbr, tl = deliftl tbr (j+1) ms tl in
442                         try 
443                           let ms, t = aux (context,k,in_scope) ms t in 
444                           ms, tbr, t::tl
445                         with
446                         | NotInTheList | MetaSubstFailure _ -> ms, j::tbr, tl
447                   in
448                   let (metasenv, subst), to_be_r, lc1' = deliftl [] 1 ms lc1 in
449                   pp (lazy ("TO BE RESTRICTED: " ^ 
450                    (String.concat "," (List.map string_of_int to_be_r))));
451                   let l1 = pack_lc (0, NCic.Ctx lc1') in
452                   pp (lazy ("newmeta:" ^ status#ppterm
453                    ~metasenv ~subst ~context (NCic.Meta (999,l1))));
454                   pp (lazy (status#ppmetasenv ~subst metasenv));
455                   if to_be_r = [] then
456                     (metasenv, subst), 
457                     (if lc1' = lc1 then orig else NCic.Meta (i,l1))
458                   else
459                     let metasenv, subst, newmeta, more_restricted = 
460                      restrict status metasenv subst i to_be_r in
461                     let l1 = purge_restricted to_be_r more_restricted l1 in
462                      (metasenv, subst), NCic.Meta(newmeta,l1))
463
464     | t -> 
465         NCicUntrusted.map_term_fold_a status
466           (fun e (c,k,s) -> (e::c,k+1,s)) (context,k,in_scope) aux ms t
467   in
468 (*
469   prerr_endline (
470     "DELIFTO " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ " w.r.t. " ^
471     String.concat ", " (List.map (NCicPp.ppterm ~metasenv ~subst ~context) ( 
472       let shift, lc = l in
473       (List.map (NCicSubstitution.lift shift) 
474         (NCicUtils.expand_local_context lc))
475   )));
476 *)
477    try aux (context,0,0) (metasenv,subst) t
478    with NotInTheList ->
479       (* This is the case where we fail even first order unification. *)
480       (* The reason is that our delift function is weaker than first  *)
481       (* order (in the sense of alpha-conversion). See comment above  *)
482       (* related to the delift function.                              *)
483       let msg = (lazy (Printf.sprintf
484         ("Error trying to abstract %s over [%s]: the algorithm only tried to "^^
485         "abstract over bound variables") (status#ppterm ~metasenv ~subst
486         ~context t) (String.concat "; " (List.map (status#ppterm ~metasenv
487         ~subst ~context) (let shift, lc = l in List.map (NCicSubstitution.lift
488         status shift) (NCicUtils.expand_local_context lc))))))
489       in
490       let shift, lc = l in
491       let lc = NCicUtils.expand_local_context lc in
492       let l = List.map (NCicSubstitution.lift status shift) lc in
493        if
494         List.exists (fun t-> NCicUntrusted.metas_of_term status subst context t <> [])l
495        then
496         raise (Uncertain msg)
497        else
498         raise (MetaSubstFailure msg)
499  (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
500 ;;
501
502 let mk_meta ?(attrs=[]) metasenv context ?with_type kind = 
503   assert(kind <> `IsSort || context = []);
504   let n = newmeta () in
505   let ty= match with_type with None-> NCic.Implicit (`Typeof n)| Some x ->x in
506   let len = List.length context in
507   let attrs = NCicUntrusted.set_kind kind attrs in
508   let menv_entry = (n, (attrs, context, ty)) in
509   menv_entry :: metasenv, n, NCic.Meta (n, (0,NCic.Irl len)), ty
510 ;;
511
512 let extend_meta metasenv n =
513  try
514   let attrs,cc,ty = NCicUtils.lookup_meta n metasenv in 
515   (match ty with 
516   | NCic.Implicit (`Typeof _) -> 
517       let mk_meta context kind =
518         let metasenv, _, ty, _ = mk_meta metasenv context kind in
519         (n, (attrs, cc, ty)) :: List.filter (fun x,_ -> x <> n) metasenv, ty
520       in
521       (match NCicUntrusted.kind_of_meta attrs with
522        | `IsSort 
523        | `IsType -> mk_meta [] `IsSort
524        | `IsTerm -> mk_meta cc `IsType)
525   | ty -> metasenv, ty)
526  with NCicUtils.Meta_not_found _ -> assert false
527 ;;
528
529 let saturate status ?(delta=0) metasenv subst context ty goal_arity =
530  assert (goal_arity >= 0);
531   let rec aux metasenv = function
532    | NCic.Prod (name,s,t) as ty ->
533        let metasenv1, _, arg,_ = 
534           mk_meta ~attrs:[`Name name] metasenv context ~with_type:s `IsTerm in
535        let t, metasenv1, args, pno = 
536            aux metasenv1 (NCicSubstitution.subst status arg t) 
537        in
538        if pno + 1 = goal_arity then
539          ty, metasenv, [], goal_arity+1
540        else
541          t, metasenv1, arg::args, pno+1
542    | ty ->
543         match NCicReduction.whd status ~subst context ty ~delta with
544         | NCic.Prod _ as ty -> aux metasenv ty
545         | ty -> ty, metasenv, [], 0
546   in
547   let res, newmetasenv, arguments, _ = aux metasenv ty in
548   res, newmetasenv, arguments
549 ;;