]> matita.cs.unibo.it Git - helm.git/blob - matitaB/components/ng_refiner/nCicRefiner.ml
Debugging code commented out.
[helm.git] / matitaB / components / ng_refiner / nCicRefiner.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 exception RefineFailure of (Stdpp.location * string) Lazy.t;;
15 exception Uncertain of (Stdpp.location * string) Lazy.t;;
16 exception AssertFailure of string Lazy.t;;
17
18 module C = NCic
19 module Ref = NReference
20
21 let debug = ref false;;
22 let indent = ref "";;
23 let times = ref [];;
24 let pp s =
25  if !debug then
26   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
27 ;;
28 let inside c =
29  if !debug then
30   begin
31    let time1 = Unix.gettimeofday () in
32    indent := !indent ^ String.make 1 c;
33    times := time1 :: !times;
34    prerr_endline ("{{{" ^ !indent ^ " ")
35   end
36 ;;
37 let outside ok =
38  if !debug then
39   begin
40    let time2 = Unix.gettimeofday () in
41    let time1 =
42     match !times with time1::tl -> times := tl; time1 | [] -> assert false in
43    prerr_endline ("}}} " ^ string_of_float (time2 -. time1));
44    if not ok then prerr_endline "exception raised!";
45    try
46     indent := String.sub !indent 0 (String.length !indent -1)
47    with
48     Invalid_argument _ -> indent := "??"; ()
49  end
50 ;;
51
52
53 let wrap_exc msg = function
54   | NCicUnification.Uncertain _ -> Uncertain msg
55   | NCicUnification.UnificationFailure _ -> RefineFailure msg
56   | NCicTypeChecker.TypeCheckerFailure _ -> RefineFailure msg
57   | e -> raise e
58 ;;
59
60 let exp_implicit status ~localise metasenv subst context with_type t =
61  function      
62   | `Closed ->
63       let metasenv,subst,expty =
64        match with_type with
65           None -> metasenv,subst,None
66         | Some typ ->
67            let (metasenv,subst),typ =
68             try
69              NCicMetaSubst.delift status
70               ~unify:(fun m s c t1 t2 ->
71                 try Some (NCicUnification.unify status m s c t1 t2)
72                 with NCicUnification.UnificationFailure _ | NCicUnification.Uncertain _ -> None)
73               metasenv subst context 0 (0,NCic.Irl 0) typ
74             with
75               NCicMetaSubst.MetaSubstFailure _
76             | NCicMetaSubst.Uncertain _ ->
77                raise (RefineFailure (lazy (localise t,"Trying to create a closed meta with a non closed type: " ^ status#ppterm ~metasenv ~subst ~context typ)))
78
79            in
80             metasenv,subst,Some typ
81       in
82        NCicMetaSubst.mk_meta metasenv [] ?with_type:expty `IsTerm,subst
83   | `Type -> NCicMetaSubst.mk_meta metasenv context ?with_type `IsType,subst
84   | `Term -> NCicMetaSubst.mk_meta metasenv context ?with_type `IsTerm,subst
85   | `Tagged s ->
86       NCicMetaSubst.mk_meta 
87         ~attrs:[`Name s] metasenv context ?with_type `IsTerm,subst
88   | `Vector ->
89       raise (RefineFailure (lazy (localise t, "A vector of implicit terms " ^
90        "can only be used in argument position")))
91   | _ -> assert false
92 ;;
93
94 let check_allowed_sort_elimination status localise r orig =
95    let mkapp he arg =
96      match he with
97      | C.Appl l -> C.Appl (l @ [arg])
98      | t -> C.Appl [t;arg] in
99    (* ctx, ind_type @ lefts, sort_of_ind_ty@lefts, outsort *)
100    let rec aux metasenv subst context ind arity1 arity2 =
101      (*D*)inside 'S'; try let rc = 
102      let arity1 = NCicReduction.whd status ~subst context arity1 in
103      pp (lazy(status#ppterm ~subst ~metasenv ~context arity1 ^ "   elimsto   " ^
104         status#ppterm ~subst ~metasenv ~context arity2 ^ "\nMENV:\n"^
105         status#ppmetasenv ~subst metasenv));
106      match arity1 with
107      | C.Prod (name,so1,de1) (* , t ==?== C.Prod _ *) ->
108         let metasenv, _, meta, _ = 
109           NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) `IsType 
110         in
111         let metasenv, subst = 
112           try NCicUnification.unify status metasenv subst context 
113                 arity2 (C.Prod (name, so1, meta)) 
114           with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf
115             "expected %s, found %s" (* XXX localizzare meglio *)
116             (status#ppterm ~subst ~metasenv ~context (C.Prod (name, so1, meta)))
117             (status#ppterm ~subst ~metasenv ~context arity2))) exc)
118         in
119         aux metasenv subst ((name, C.Decl so1)::context)
120          (mkapp (NCicSubstitution.lift status 1 ind) (C.Rel 1)) de1 meta
121      | C.Sort _ (* , t ==?== C.Prod _ *) ->
122         let metasenv, _, meta, _ = NCicMetaSubst.mk_meta metasenv [] `IsSort in
123         let metasenv, subst = 
124           try NCicUnification.unify status metasenv subst context 
125                 arity2 (C.Prod ("_", ind, meta)) 
126           with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf
127             "expected %s, found %s" (* XXX localizzare meglio *)
128             (status#ppterm ~subst ~metasenv ~context (C.Prod ("_", ind, meta)))
129             (status#ppterm ~subst ~metasenv ~context arity2))) exc)
130         in
131         (try NCicTypeChecker.check_allowed_sort_elimination status
132             ~metasenv ~subst r context ind arity1 arity2; 
133             metasenv, subst
134         with exc -> raise (wrap_exc (lazy (localise orig, 
135           "Sort elimination not allowed ")) exc))
136      | _ -> assert false
137      (*D*)in outside true; rc with exc -> outside false; raise exc
138    in
139     aux
140 ;;
141
142 let rec typeof (status:#NCicCoercion.status)
143   ?(localise=fun _ -> Stdpp.dummy_loc) 
144   metasenv subst context term expty 
145 =
146   let force_ty skip_lambda skip_appl metasenv subst context orig t infty expty =
147     (*D*)inside 'F'; try let rc = 
148     match expty with
149     | Some expty ->
150        (match t with
151        | C.Implicit _ -> assert false
152        | C.Lambda _ when skip_lambda -> metasenv, subst, t, expty
153        | C.Appl _ when skip_appl -> metasenv, subst, t, expty
154        | _ ->
155           pp (lazy ("forcing infty=expty: "^
156           (status#ppterm ~metasenv ~subst ~context infty) ^  " === " ^
157           (status#ppterm ~metasenv ~subst:[] ~context expty)));
158            try 
159              let metasenv, subst =
160     (*D*)inside 'U'; try let rc = 
161                NCicUnification.unify status metasenv subst context infty expty 
162     (*D*)in outside true; rc with exc -> outside false; raise exc
163              in
164              metasenv, subst, t, expty
165            with 
166            | NCicUnification.Uncertain _ 
167            | NCicUnification.UnificationFailure _ as exc -> 
168              try_coercions status ~localise 
169                metasenv subst context t orig infty expty true exc)
170     | None -> metasenv, subst, t, infty
171     (*D*)in outside true; rc with exc -> outside false; raise exc
172   in
173   let rec typeof_aux metasenv subst context expty = 
174     fun t as orig -> 
175     (*D*)inside 'R'; try let rc = 
176     pp (lazy (status#ppterm ~metasenv ~subst ~context t ^ " ::exp:: " ^
177        match expty with None -> "None" | Some e -> 
178        status#ppterm ~metasenv ~subst ~context e));
179     let metasenv, subst, t, infty = 
180     match t with
181     | C.Rel n ->
182         let infty = 
183          (try
184            match List.nth context (n - 1) with
185            | (_,C.Decl ty) -> NCicSubstitution.lift status n ty
186            | (_,C.Def (_,ty)) -> NCicSubstitution.lift status n ty
187          with Failure _ -> 
188            raise (RefineFailure (lazy (localise t,"unbound variable"))))
189         in
190         metasenv, subst, t, infty
191     | C.Sort s -> 
192          (try metasenv, subst, t, C.Sort (NCicEnvironment.typeof_sort s)
193          with 
194          | NCicEnvironment.UntypableSort msg -> 
195               raise (RefineFailure (lazy (localise t, Lazy.force msg)))
196          | NCicEnvironment.AssertFailure msg -> raise (AssertFailure msg))
197     | C.Implicit infos -> 
198          let (metasenv,_,t,ty),subst =
199            exp_implicit status ~localise metasenv subst context expty t infos
200          in
201          if expty = None then
202           typeof_aux metasenv subst context None t
203          else
204           metasenv, subst, t, ty 
205     | C.Meta (n,l) as t -> 
206        let metasenv, ty =
207         try
208          let _,_,_,ty = NCicUtils.lookup_subst n subst in metasenv, ty 
209         with NCicUtils.Subst_not_found _ ->
210          NCicMetaSubst.extend_meta metasenv n
211        in
212        metasenv, subst, t, NCicSubstitution.subst_meta status l ty
213     | C.Const _ -> 
214        metasenv, subst, t, NCicTypeChecker.typeof status ~subst ~metasenv context t
215     | C.Prod (name,(s as orig_s),(t as orig_t)) ->
216        let metasenv, subst, s, s1 = typeof_aux metasenv subst context None s in
217        let metasenv, subst, s, s1 = 
218          force_to_sort status 
219            metasenv subst context s orig_s localise s1 in
220        let context1 = (name,(C.Decl s))::context in
221        let metasenv, subst, t, s2 = typeof_aux metasenv subst context1 None t in
222        let metasenv, subst, t, s2 = 
223          force_to_sort status 
224            metasenv subst context1 t orig_t localise s2 in
225        let metasenv, subst, s, t, ty = 
226          sort_of_prod status localise metasenv subst 
227            context orig_s orig_t (name,s) t (s1,s2)
228        in
229        metasenv, subst, NCic.Prod(name,s,t), ty
230     | C.Lambda (n,(s as orig_s),t) as orig ->
231        let exp_s, exp_ty_t, force_after =
232          match expty with
233          | None -> None, None, false
234          | Some expty -> 
235              match NCicReduction.whd status ~subst context expty with
236              | C.Prod (_,s,t) -> Some s, Some t, false
237              | _ -> None, None, true 
238        in
239        let (metasenv,subst), s = 
240          match exp_s with 
241          | Some exp_s ->
242              (* optimized case: implicit and implicitly typed meta
243               * the optimization prevents proliferation of metas  *)
244              (match s with
245               | C.Implicit _ -> (metasenv,subst),exp_s
246               | _ ->
247                   let metasenv, subst, s = match s with 
248                     | C.Meta (n,_) 
249                         when (try (match NCicUtils.lookup_meta n metasenv with
250                               | _,_,C.Implicit (`Typeof _) -> true
251                               | _ -> false)
252                         with 
253                           | _ -> false) -> metasenv, subst, s
254                     | _ ->  check_type status ~localise metasenv subst context s in
255                   (try 
256                     pp(lazy("Force source to: "^status#ppterm ~metasenv ~subst
257                        ~context exp_s));
258                     NCicUnification.unify ~test_eq_only:true status metasenv subst context s exp_s,s
259                   with exc -> raise (wrap_exc (lazy (localise orig_s, Printf.sprintf
260                     "Source type %s was expected to be %s" (status#ppterm ~metasenv
261                     ~subst ~context s) (status#ppterm ~metasenv ~subst ~context
262                     exp_s))) exc)))
263          | None -> 
264              let metasenv, subst, s = 
265                check_type status ~localise metasenv subst context s in
266              (metasenv, subst), s
267        in
268        let context_for_t = (n,C.Decl s) :: context in
269        let metasenv, subst, t, ty_t = 
270          typeof_aux metasenv subst context_for_t exp_ty_t t 
271        in
272        if force_after then
273          force_ty false true metasenv subst context orig 
274            (C.Lambda(n,s,t)) (C.Prod (n,s,ty_t)) expty
275        else 
276          metasenv, subst, C.Lambda(n,s,t), C.Prod (n,s,ty_t)
277     | C.LetIn (n,ty,t,bo) ->
278        let metasenv, subst, ty = 
279          check_type status ~localise metasenv subst context ty in
280        let metasenv, subst, t, _ = 
281          typeof_aux metasenv subst context (Some ty) t in
282        let context1 = (n, C.Def (t,ty)) :: context in
283        let metasenv, subst, expty1 = 
284          match expty with 
285          | None -> metasenv, subst, None 
286          | Some x -> 
287              let m, s, x = 
288                NCicUnification.delift_type_wrt_terms 
289                 status metasenv subst context1 (NCicSubstitution.lift status 1 x)
290                 [NCicSubstitution.lift status 1 t]
291              in
292                m, s, Some x
293        in
294        let metasenv, subst, bo, bo_ty = 
295          typeof_aux metasenv subst context1 expty1 bo 
296        in
297        let bo_ty = NCicSubstitution.subst status ~avoid_beta_redexes:true t bo_ty in
298        metasenv, subst, C.LetIn (n, ty, t, bo), bo_ty
299     | C.Appl ((he as orig_he)::(_::_ as args)) ->
300        let upto = match orig_he with C.Meta _ -> List.length args | _ -> 0 in
301        let hbr t = 
302          if upto > 0 then NCicReduction.head_beta_reduce status ~upto t else t 
303        in
304        let refine_appl metasenv subst args =
305          let metasenv, subst, he, ty_he = 
306             typeof_aux metasenv subst context None he in
307          let metasenv, subst, t, ty = 
308            eat_prods status ~localise force_ty metasenv subst context expty t
309             orig_he he ty_he args in
310          metasenv, subst, hbr t, ty
311        in
312        if args = [C.Implicit `Vector] && expty <> None then
313          (* we try here to expand the vector a 0 implicits, but we use
314           * the expected type *)
315          try
316            let metasenv, subst, he, ty_he = 
317               typeof_aux metasenv subst context expty he in
318            metasenv, subst, hbr he, ty_he
319          with Uncertain _ | RefineFailure _ -> refine_appl metasenv subst args
320        else
321         (* CSC: whd can be useful on he too... *)
322         (match he with
323             C.Const (Ref.Ref (uri1,Ref.Con _)) -> (
324              match
325               HExtlib.map_option (NCicReduction.whd status ~subst context) expty
326              with
327                 Some (C.Appl(C.Const(Ref.Ref (uri2,Ref.Ind _) as ref)::expargs))
328                 when NUri.eq uri1 uri2 ->
329                 (try
330                  let _,leftno,_,_,_ = NCicEnvironment.get_checked_indtys status ref in
331                  let leftexpargs,_ = HExtlib.split_nth leftno expargs in
332                   let rec instantiate metasenv subst revargs args =
333                    function
334                      [] ->
335                       (* some checks are re-done here, but it would be complex
336                          to avoid them (e.g. we did not check yet that the
337                          constructor is a constructor for that inductive type)*)
338                       refine_appl metasenv subst ((List.rev revargs)@args)
339                    | (exparg::expargs) as allexpargs ->
340                       match args with
341                          [] -> raise (Failure "Not enough args")
342                        | (C.Implicit `Vector::args) as allargs ->
343                           (try
344                             instantiate metasenv subst revargs args allexpargs
345                            with
346                               Sys.Break as exn -> raise exn
347                             | _ ->
348                              instantiate metasenv subst revargs
349                               (C.Implicit `Term :: allargs) allexpargs)
350                        | arg::args ->
351                           let metasenv,subst,arg,_ =
352                            typeof_aux metasenv subst context None arg in
353                           let metasenv,subst =
354                            NCicUnification.unify status metasenv subst context
355                             arg exparg
356                           in
357                            instantiate metasenv subst(arg::revargs) args expargs
358                   in
359                    instantiate metasenv subst [] args leftexpargs 
360                 with
361                  | Sys.Break as exn -> raise exn
362                  | _ ->
363                     refine_appl metasenv subst args (* to try coercions *))
364               | _ -> refine_appl metasenv subst args)
365           | _ -> refine_appl metasenv subst args)
366    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
367    | C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as r,
368           outtype,(term as orig_term),pl) as orig ->
369       let _, leftno, itl, _, _ = NCicEnvironment.get_checked_indtys status r in
370       let _, _, arity, cl = List.nth itl tyno in
371       let constructorsno = List.length cl in
372       let _, metasenv, args = 
373         NCicMetaSubst.saturate status metasenv subst context arity 0 in
374       let ind = if args = [] then C.Const r else C.Appl (C.Const r::args) in
375       let metasenv, subst, term, _ = 
376         typeof_aux metasenv subst context (Some ind) term in
377       let parameters, arguments = HExtlib.split_nth leftno args in
378       let outtype =  
379         match outtype with
380         | C.Implicit _ as ot -> 
381              let rec aux = function
382                | [] -> NCic.Lambda ("_",NCic.Implicit `Type,ot)
383                | _::tl -> NCic.Lambda ("_",NCic.Implicit `Type,aux tl)
384              in
385                aux arguments
386         | _ -> outtype
387       in 
388       let metasenv, subst, outtype, outsort = 
389         typeof_aux metasenv subst context None outtype in
390
391       (* next lines are to do a subst-expansion of the outtype, so
392          that when it becomes a beta-abstraction, the beta-redex is
393          fired during substitution *)
394       let _,fresh_metanoouttype,newouttype,_ =
395        NCicMetaSubst.mk_meta metasenv context `IsTerm in
396       let subst =
397        (fresh_metanoouttype,([`Name "outtype"],context,outtype,outsort))
398          ::subst in
399       let outtype = newouttype in
400
401       (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
402       let ind =
403         if parameters = [] then C.Const r
404         else C.Appl ((C.Const r)::parameters) in
405       let metasenv, subst, ind, ind_ty = 
406         typeof_aux metasenv subst context None ind in
407       let metasenv, subst = 
408          check_allowed_sort_elimination status localise r orig_term metasenv subst 
409            context ind ind_ty outsort 
410       in
411       (* let's check if the type of branches are right *)
412       if List.length pl <> constructorsno then
413        raise (RefineFailure (lazy (localise orig, 
414          "Wrong number of cases in a match")));
415 (*
416       let metasenv, subst =
417         match expty with
418         | None -> metasenv, subst
419         | Some expty -> 
420            NCicUnification.unify status metasenv subst context resty expty 
421       in
422 *)
423       let _, metasenv, subst, pl =
424         List.fold_right
425           (fun p (j, metasenv, subst, branches) ->
426               let cons = 
427                 let cons = Ref.mk_constructor j r in
428                 if parameters = [] then C.Const cons
429                 else C.Appl (C.Const cons::parameters)
430               in
431               let metasenv, subst, cons, ty_cons = 
432                 typeof_aux metasenv subst context None cons in
433               let ty_branch = 
434                 NCicTypeChecker.type_of_branch status
435                   ~subst context leftno outtype cons ty_cons in
436               pp (lazy ("TYPEOFBRANCH: " ^
437                status#ppterm ~metasenv ~subst ~context p ^ " ::inf:: " ^
438                status#ppterm ~metasenv ~subst ~context ty_branch ));
439               let metasenv, subst, p, _ = 
440                 typeof_aux metasenv subst context (Some ty_branch) p in
441               j-1, metasenv, subst, p :: branches)
442           pl (List.length pl, metasenv, subst, [])
443       in
444       let resty = C.Appl (outtype::arguments@[term]) in
445       let resty = NCicReduction.head_beta_reduce status ~subst resty in
446       metasenv, subst, C.Match (r, outtype, term, pl),resty
447     | C.Match _ -> assert false
448     in
449     pp (lazy (status#ppterm ~metasenv ~subst ~context t ^ " ::inf:: "^
450          status#ppterm ~metasenv ~subst ~context infty ));
451       force_ty true true metasenv subst context orig t infty expty
452     (*D*)in outside true; rc with exc -> outside false; raise exc
453   in
454     typeof_aux metasenv subst context expty term
455
456 and check_type status ~localise metasenv subst context (ty as orig_ty) =
457   let metasenv, subst, ty, sort = 
458     typeof status ~localise metasenv subst context ty None
459   in
460   let metasenv, subst, ty, _ = 
461     force_to_sort status metasenv subst context ty orig_ty localise sort
462   in
463     metasenv, subst, ty
464
465 and try_coercions status 
466   ~localise 
467   metasenv subst context t orig_t infty expty perform_unification exc 
468 =
469   let cs_subst = NCicSubstitution.subst status ~avoid_beta_redexes:true in
470   try 
471     pp (lazy "WWW: trying coercions -- preliminary unification");
472     let metasenv, subst = 
473       NCicUnification.unify status metasenv subst context infty expty
474     in metasenv, subst, t, expty
475   with
476   | exn ->
477   (* we try with a coercion *)
478   let rec first exc = function
479   | [] ->   
480       pp (lazy "WWW: no more coercions!");      
481       raise (wrap_exc (lazy (localise orig_t, Printf.sprintf
482         "The term\n%s\nhas type\n%s\nbut is here used with type\n%s"
483         (status#ppterm ~metasenv ~subst ~context t)
484         (status#ppterm ~metasenv ~subst ~context infty)
485         (status#ppterm ~metasenv ~subst ~context expty))) exc)
486   | (_,metasenv, newterm, newtype, meta)::tl ->
487       try 
488           pp (lazy("K=" ^ status#ppterm ~metasenv ~subst ~context newterm));
489           pp (lazy ( "UNIFICATION in CTX:\n"^ 
490             status#ppcontext ~metasenv ~subst context
491             ^ "\nMENV: " ^
492             status#ppmetasenv metasenv ~subst
493             ^ "\nOF: " ^
494             status#ppterm ~metasenv ~subst ~context t ^  " === " ^
495             status#ppterm ~metasenv ~subst ~context meta ^ "\n"));
496         let metasenv, subst = 
497           NCicUnification.unify status metasenv subst context t meta
498         in
499           pp (lazy ( "UNIFICATION in CTX:\n"^ 
500             status#ppcontext ~metasenv ~subst context
501             ^ "\nMENV: " ^
502             status#ppmetasenv metasenv ~subst
503             ^ "\nOF: " ^
504             status#ppterm ~metasenv ~subst ~context newtype ^  " === " ^
505             status#ppterm ~metasenv ~subst ~context expty ^ "\n"));
506         let metasenv, subst = 
507           if perform_unification then
508             NCicUnification.unify status metasenv subst context newtype expty
509           else metasenv, subst
510         in
511         metasenv, subst, newterm, newtype
512       with 
513       | NCicUnification.UnificationFailure _ -> first exc tl
514       | NCicUnification.Uncertain _ as exc -> first exc tl
515   in
516   
517   try 
518     pp (lazy "WWW: trying coercions -- inner check");
519     match infty, expty, t with
520     | _,_, NCic.Match (Ref.Ref (_,Ref.Ind (_,tyno,leftno)) as r,outty,m,pl) ->
521         (*{{{*) pp (lazy "CASE");
522         (* {{{ helper functions *)
523         let get_cl_and_left_p refit outty =
524           match refit with
525           | NReference.Ref (uri, NReference.Ind (_,tyno,leftno)) ->
526              let _, leftno, itl, _, _ = NCicEnvironment.get_checked_indtys status r in
527              let _, _, ty, cl = List.nth itl tyno in
528              let constructorsno = List.length cl in
529               let count_pis t =
530                 let rec aux ctx t = 
531                   match NCicReduction.whd status ~subst ~delta:max_int ctx t with
532                   | NCic.Prod (name,src,tgt) ->
533                       let ctx = (name, (NCic.Decl src)) :: ctx in
534                       1 + aux ctx tgt
535                   | _ -> 0
536                 in
537                   aux [] t
538               in
539               let rec skip_lambda_delifting t n =
540                 match t,n with
541                 | _,0 -> t
542                 | NCic.Lambda (_,_,t),n ->
543                     pp (lazy ("WWW: failing term? "^ status#ppterm ~subst:[] ~metasenv:[] ~context:[] t)); 
544                     skip_lambda_delifting
545                       (* substitute dangling indices with a dummy *)
546                       (NCicSubstitution.subst status (NCic.Sort NCic.Prop) t) (n - 1)
547                 | _ -> assert false
548               in
549               let get_l_r_p n = function
550                 | NCic.Lambda (_,NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_))),_) -> [],[]
551                 | NCic.Lambda (_,NCic.Appl 
552                     (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_))) :: args),_) ->
553                     HExtlib.split_nth n args
554                 | _ -> assert false
555               in
556               let pis = count_pis ty in
557               let rno = pis - leftno in
558               let t = skip_lambda_delifting outty rno in
559               let left_p, _ = get_l_r_p leftno t in
560               let instantiate_with_left cl =
561                 List.map 
562                   (fun ty -> 
563                     List.fold_left 
564                       (fun t p -> match t with
565                         | NCic.Prod (_,_,t) ->
566                             cs_subst p t
567                         | _-> assert false)
568                       ty left_p) 
569                   cl 
570               in
571               let cl = instantiate_with_left (List.map (fun (_,_,x) -> x) cl) in
572               cl, left_p, leftno, rno
573           | _ -> raise exn
574         in
575         let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
576           match t,n with
577           | _,0 ->
578             let rec mkr n = function 
579               | [] -> [] | _::tl -> NCic.Rel n :: mkr (n+1) tl
580             in
581             pp (lazy ("input replace: " ^ status#ppterm ~context:ctx ~metasenv:[] ~subst:[] bo));
582             let bo =
583             NCicRefineUtil.replace_lifting status
584               ~equality:(fun _ -> NCicRefineUtil.alpha_equivalence status)
585               ~context:ctx
586               ~what:(matched::right_p)
587               ~with_what:(NCic.Rel 1::List.rev (mkr 2 right_p))
588               ~where:bo
589             in
590             pp (lazy ("output replace: " ^ status#ppterm ~context:ctx ~metasenv:[] ~subst:[] bo));
591             bo
592           | NCic.Lambda (name, src, tgt),_ ->
593               NCic.Lambda (name, src,
594                keep_lambdas_and_put_expty 
595                 ((name, NCic.Decl src)::ctx) tgt (NCicSubstitution.lift status 1 bo)
596                 (List.map (NCicSubstitution.lift status 1) right_p) (NCicSubstitution.lift status 1 matched) (n-1))
597           | _ -> assert false
598         in
599         (*let eq = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.ind(1,0,2)")) in
600         let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.con(0,1,2)")) in*)
601         let eq = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/jmeq/jmeq.ind(1,0,2)")) in
602         let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/jmeq/jmeq.con(0,1,2)")) in
603         let add_params 
604           metasenv subst context cty outty mty m i 
605         =
606           let rec aux context outty par j mty m = function
607             | NCic.Prod (name, src, tgt) ->
608                 let t,k = 
609                   aux 
610                     ((name, NCic.Decl src) :: context)
611                     (NCicSubstitution.lift status 1 outty) (NCic.Rel j::par) (j+1) 
612                     (NCicSubstitution.lift status 1 mty) (NCicSubstitution.lift status 1 m) tgt
613                 in
614                 NCic.Prod (name, src, t), k
615             | NCic.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r) ->
616                 let k = 
617                   let k = NCic.Const(Ref.mk_constructor i r) in
618                   NCicUntrusted.mk_appl k par
619                 in
620                 (* the type has no parameters, so kty = mty
621                 let kty = 
622                   try NCicTypechecker.typeof ~subst ~metasenv context k
623                   with NCicTypeChecker.TypeCheckerFailure _ -> assert false
624                 in *)
625                 NCic.Prod ("p", 
626                  NCic.Appl [eq; mty; m; mty; k],
627                  (NCicSubstitution.lift status 1
628                   (NCicReduction.head_beta_reduce status ~delta:max_int 
629                    (NCicUntrusted.mk_appl outty [k])))),[mty,m,mty,k]
630             | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r)::pl) ->
631                 let left_p,right_p = HExtlib.split_nth leftno pl in
632                 let has_rights = right_p <> [] in
633                 let k = 
634                   let k = NCic.Const(Ref.mk_constructor i r) in
635                   NCicUntrusted.mk_appl k (left_p@par)
636                 in
637                 let right_p = 
638                   try match 
639                     NCicTypeChecker.typeof status ~subst ~metasenv context k
640                   with
641                   | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_)))::args) ->
642                       snd (HExtlib.split_nth leftno args)
643                   | _ -> assert false
644                   with NCicTypeChecker.TypeCheckerFailure _-> assert false
645                 in
646                 let orig_right_p =
647                   match mty with
648                   | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_)))::args) ->
649                       snd (HExtlib.split_nth leftno args)
650                   | _ -> assert false
651                 in
652                 List.fold_right2 
653                   (fun x y (tacc,pacc) ->
654                     let xty = 
655                     try NCicTypeChecker.typeof status ~subst ~metasenv context x
656                       with NCicTypeChecker.TypeCheckerFailure _ -> assert false
657                     in
658                     let yty = 
659                     try NCicTypeChecker.typeof status ~subst ~metasenv context y
660                       with NCicTypeChecker.TypeCheckerFailure _ -> assert false
661                     in
662                     NCic.Prod ("_", NCic.Appl [eq;xty;x;yty;y],
663                      NCicSubstitution.lift status 1 tacc), (xty,x,yty,y)::pacc) 
664                   (orig_right_p @ [m]) (right_p @ [k]) 
665                   (NCicReduction.head_beta_reduce status ~delta:max_int
666                       (NCicUntrusted.mk_appl outty (right_p@[k])), [])  
667
668   (*              if has_rights then
669                   NCicReduction.head_beta_reduce status ~delta:max_int
670                     (NCic.Appl (outty ::right_p @ [k])),k
671                 else
672                   NCic.Prod ("p", 
673                    NCic.Appl [eq; mty; m; k],
674                    (NCicSubstitution.lift status 1
675                     (NCicReduction.head_beta_reduce status ~delta:max_int 
676                      (NCic.Appl (outty ::right_p @ [k]))))),k*)
677             | _ -> assert false
678           in
679             aux context outty [] 1 mty m cty
680         in
681         let add_lambda_for_refl_m pbo eqs cty =
682           (* k lives in the right context *)
683           (* if rno <> 0 then pbo else *)
684           let rec aux = function 
685             | NCic.Lambda (name,src,bo), NCic.Prod (_,_,ty) ->
686                 NCic.Lambda (name,src,
687                 (aux (bo,ty)))
688             | t,_ -> snd (List.fold_right
689                 (fun (xty,x,yty,y) (n,acc) -> n+1, NCic.Lambda ("p" ^ string_of_int n,
690                   NCic.Appl [eq; xty; x; yty; y],
691                   NCicSubstitution.lift status 1 acc)) eqs (1,t))
692                 (*NCic.Lambda ("p",
693                   NCic.Appl [eq; mty; m; k],NCicSubstitution.lift status 1 t)*)
694           in
695           aux (pbo,cty)
696         in
697         let add_pi_for_refl_m context new_outty mty m lno rno =
698           (*if rno <> 0 then new_outty else*)
699             let rec aux context mty m = function
700               | NCic.Lambda (name, src, tgt) ->
701                   let context = (name, NCic.Decl src)::context in
702                   NCic.Lambda (name, src, aux context (NCicSubstitution.lift status 1 mty) (NCicSubstitution.lift status 1 m) tgt)
703               | t -> 
704                   let lhs =
705                     match mty with
706                     | NCic.Appl (_::params) -> (snd (HExtlib.split_nth lno params))@[m]
707                     | _ -> [m]
708                   in
709                   let rhs = 
710                     List.map (fun x -> NCic.Rel x) 
711                       (List.rev (HExtlib.list_seq 1 (rno+2))) in
712                   List.fold_right2
713                     (fun x y acc ->
714                       let xty = 
715                     try NCicTypeChecker.typeof status ~subst ~metasenv context x
716                         with NCicTypeChecker.TypeCheckerFailure _ -> assert false
717                       in
718                       let yty = 
719                     try NCicTypeChecker.typeof status ~subst ~metasenv context y
720                         with NCicTypeChecker.TypeCheckerFailure _ -> assert false
721                       in
722                       NCic.Prod
723                       ("_", NCic.Appl [eq;xty;x;yty;y],
724                        (NCicSubstitution.lift status 1 acc)))
725                     lhs rhs t
726   (*                NCic.Prod 
727                     ("_", NCic.Appl [eq;mty;m;NCic.Rel 1],
728                     NCicSubstitution.lift status 1 t)*)
729             in
730               aux context mty m new_outty
731         in (* }}} end helper functions *)
732         (* constructors types with left params already instantiated *)
733         let outty = NCicUntrusted.apply_subst status subst context outty in
734         let cl, left_p, leftno,rno = 
735           get_cl_and_left_p r outty
736         in
737         let right_p, mty = 
738           try
739             match 
740               NCicTypeChecker.typeof status ~subst ~metasenv context m
741             with
742             | (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_))) | NCic.Meta _) as mty -> [], mty
743             | NCic.Appl ((NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_)))|NCic.Meta _)::args) as mty ->
744                 snd (HExtlib.split_nth leftno args), mty
745             | _ -> assert false
746           with NCicTypeChecker.TypeCheckerFailure _ -> 
747              raise (AssertFailure(lazy "already ill-typed matched term"))
748         in
749         let mty = NCicUntrusted.apply_subst status subst context mty in
750         let outty = NCicUntrusted.apply_subst status subst context outty in
751         let expty = NCicUntrusted.apply_subst status subst context expty in
752         let new_outty =
753          keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
754         in
755         pp 
756           (lazy ("CASE: new_outty: " ^ status#ppterm 
757            ~context ~metasenv ~subst new_outty));
758         let _,pl,subst,metasenv = 
759           List.fold_right2
760             (fun cty pbo (i, acc, s, menv) -> 
761                pp (lazy ("begin iteration"));
762               (* Pi k_par, (Pi H:m=(K_i left_par k_par)), 
763                *   (new_)outty right_par (K_i left_par k_par) *)
764                let infty_pbo, _ = 
765                  add_params menv s context cty outty mty m i in
766                pp 
767                 (lazy ("CASE: infty_pbo: "^ status#ppterm
768                  ~context ~metasenv ~subst infty_pbo));
769                let expty_pbo, eqs = (* k is (K_i left_par k_par) *)
770                  add_params menv s context cty new_outty mty m i in
771                pp 
772                 (lazy ("CASE: expty_pbo: "^ status#ppterm
773                  ~context ~metasenv ~subst expty_pbo));
774                let pbo = add_lambda_for_refl_m pbo eqs cty in
775                pp 
776                  (lazy ("CASE: pbo: " ^ status#ppterm
777                  ~context ~metasenv ~subst pbo));
778                let metasenv, subst, pbo, _ =
779                  try_coercions status ~localise menv s context pbo 
780                  orig_t (*??*) infty_pbo expty_pbo perform_unification exc
781                in
782                pp 
783                  (lazy ("CASE: pbo2: " ^ status#ppterm 
784                  ~context ~metasenv ~subst pbo));
785                (i-1, pbo::acc, subst, metasenv))
786             cl pl (List.length pl, [], subst, metasenv)
787         in
788         (*let metasenv, subst = 
789           try 
790             NCicUnification.unify status metasenv subst context outty new_outty 
791           with _ -> raise (RefineFailure (lazy (localise orig_t, "try_coercions")))
792         in*)
793         let new_outty = add_pi_for_refl_m context new_outty mty m leftno rno in
794         pp (lazy ("CASE: new_outty: " ^ (status#ppterm 
795            ~metasenv ~subst ~context new_outty)));
796         let right_tys = 
797           List.map 
798             (fun t -> NCicTypeChecker.typeof status ~subst ~metasenv context t) right_p in
799         let eqs = 
800           List.map2 (fun x y -> NCic.Appl[eq_refl;x;y]) (right_tys@[mty]) 
801             (right_p@[m]) in
802         let t = NCic.Appl (NCic.Match(r,new_outty,m,pl) :: eqs) 
803         in
804         metasenv, subst, t, expty (*}}}*)
805     | NCic.Prod (nameprod, src, ty),NCic.Prod (_, src2, ty2), _ -> 
806         let rec mk_fresh_name ctx firstch n =
807           let candidate = (String.make 1 firstch) ^ (string_of_int n) in
808           if (List.for_all (fun (s,_) -> s <> candidate) ctx) then candidate
809           else mk_fresh_name ctx firstch (n+1)
810         in
811         (*{{{*) pp (lazy "LAM");
812         pp (lazy ("LAM: t = " ^ status#ppterm ~metasenv ~subst ~context t));
813         let name_con = mk_fresh_name context 'c' 0
814           (*FreshNamesGenerator.mk_fresh_name 
815             ~subst metasenv context ~typ:src2 Cic.Anonymous*)
816         in
817         let context_src2 = ((name_con, NCic.Decl src2) :: context) in
818         (* contravariant part: the argument of f:src->ty *)
819         let metasenv, subst, rel1, _ = 
820           try_coercions status ~localise metasenv subst context_src2
821            (NCic.Rel 1) orig_t (NCicSubstitution.lift status 1 src2) 
822            (NCicSubstitution.lift status 1 src) perform_unification exc
823         in
824         (* covariant part: the result of f(c x); x:src2; (c x):src *)
825         let name_t, bo = 
826           match t with
827           | NCic.Lambda (n,_,bo) -> n, cs_subst rel1 (NCicSubstitution.lift_from status 2 1 bo)
828           | _ -> name_con, NCicUntrusted.mk_appl (NCicSubstitution.lift status 1 t) [rel1]
829         in
830         (* we fix the possible dependency problem in the source ty *)
831         let ty = cs_subst rel1 (NCicSubstitution.lift_from status 2 1 ty) in
832         let metasenv, subst, bo, _ = 
833           try_coercions status ~localise metasenv subst context_src2
834             bo orig_t ty ty2 perform_unification exc
835         in
836         let coerced = NCic.Lambda (name_t,src2, bo) in
837         pp (lazy ("LAM: coerced = " ^ status#ppterm ~metasenv ~subst ~context coerced));
838         metasenv, subst, coerced, expty (*}}}*)
839     | _ -> raise exc
840   with exc2 ->    
841   pp(lazy("try_coercion " ^ 
842     status#ppterm ~metasenv ~subst ~context infty ^ " |---> " ^
843     status#ppterm ~metasenv ~subst ~context expty));
844     first exc
845       (NCicCoercion.look_for_coercion 
846         status metasenv subst context infty expty)
847
848 and force_to_sort status metasenv subst context t orig_t localise ty =
849   try 
850     let metasenv, subst, ty = 
851       NCicUnification.sortfy status (Failure "sortfy") metasenv subst context ty in
852       metasenv, subst, t, ty
853   with
854       Failure _ -> 
855         let ty = NCicReduction.whd status ~subst context ty in
856           try_coercions status ~localise metasenv subst context
857             t orig_t ty (NCic.Sort (NCic.Type 
858               (match NCicEnvironment.get_universes () with
859                | x::_ -> x 
860                | _ -> assert false))) false 
861              (Uncertain (lazy (localise orig_t, 
862              "The type of " ^ status#ppterm ~metasenv ~subst ~context t ^
863              " is not a sort: " ^ status#ppterm ~metasenv ~subst ~context ty)))
864
865 and sort_of_prod status localise metasenv subst context orig_s orig_t (name,s)
866  t (t1, t2) 
867 =
868    (* force to sort is done in the Prod case in typeof *)
869    match t1, t2 with
870    | C.Sort _, C.Sort C.Prop -> metasenv, subst, s, t, t2
871    | C.Sort (C.Type u1), C.Sort (C.Type u2) ->
872         metasenv, subst, s, t, C.Sort (C.Type (NCicEnvironment.max u1 u2)) 
873    | C.Sort C.Prop,C.Sort (C.Type _) -> metasenv, subst, s, t, t2
874    | C.Meta _, C.Sort _ 
875    | C.Meta _, C.Meta (_,(_,_))
876    | C.Sort _, C.Meta (_,(_,_)) -> metasenv, subst, s, t, t2 
877    | x, (C.Sort _ | C.Meta _) | _, x -> 
878       let y, context, orig = 
879         if x == t1 then s, context, orig_s 
880         else t, ((name,C.Decl s)::context), orig_t
881       in
882       raise (RefineFailure (lazy (localise orig,Printf.sprintf
883         "%s is expected to be a type, but its type is %s that is not a sort" 
884          (status#ppterm ~subst ~metasenv ~context y) 
885          (status#ppterm ~subst ~metasenv ~context x))))
886
887 and guess_name status subst ctx ty = 
888   let aux initial = "#" ^ String.make 1 initial in
889   match ty with
890   | C.Const (NReference.Ref (u,_))
891   | C.Appl (C.Const (NReference.Ref (u,_)) :: _) ->
892       aux (String.sub (NUri.name_of_uri u) 0 1).[0] 
893   | C.Prod _ -> aux 'f' 
894   | C.Meta (n,lc) -> 
895       (try
896          let _,_,t,_ = NCicUtils.lookup_subst n subst in
897          guess_name status subst ctx (NCicSubstitution.subst_meta status lc t)
898       with NCicUtils.Subst_not_found _ -> aux 'M')
899   | _ -> aux 'H' 
900
901 and eat_prods status ~localise force_ty metasenv subst context expty orig_t orig_he he ty_he args =
902   (*D*)inside 'E'; try let rc = 
903   let rec aux metasenv subst args_so_far he ty_he xxx =
904   (*D*)inside 'V'; try let rc = 
905    match xxx with
906   | [] ->
907      let res = NCicUntrusted.mk_appl he (List.rev args_so_far) in
908      pp(lazy("FORCE FINAL APPL: " ^ 
909        status#ppterm ~metasenv ~subst ~context res ^
910        " of type " ^ status#ppterm ~metasenv ~subst ~context ty_he
911        ^ " to type " ^ match expty with None -> "None" | Some x -> 
912        status#ppterm ~metasenv ~subst ~context x));
913      (* whatever the term is, we force the type. in case of ((Lambda..) ?...)
914       * the application may also be a lambda! *)
915      force_ty false false metasenv subst context orig_t res ty_he expty
916   | NCic.Implicit `Vector::tl ->
917       let has_some_more_pis x =
918         match NCicReduction.whd status ~subst context x with
919         |  NCic.Meta _ | NCic.Appl (NCic.Meta _::_) -> false
920         | _ -> true
921       in
922      (try
923        aux metasenv subst args_so_far he ty_he tl
924       with
925       | Uncertain _
926       | RefineFailure _ as exc when has_some_more_pis ty_he ->
927           (try
928            aux metasenv subst args_so_far he ty_he
929             (NCic.Implicit `Term :: NCic.Implicit `Vector :: tl)
930           with
931            Uncertain msg | RefineFailure msg -> raise (wrap_exc msg exc))
932      | RefineFailure msg when not (has_some_more_pis ty_he) ->
933         (* instantiating the head could change the has_some_more_pis flag *)
934         raise (Uncertain msg))
935   | arg::tl ->
936       match NCicReduction.whd status ~subst context ty_he with 
937       | C.Prod (_,s,t) ->
938           let metasenv, subst, arg, _ = 
939             typeof status ~localise metasenv subst context arg (Some s) in
940           let t = NCicSubstitution.subst status ~avoid_beta_redexes:true arg t in
941           aux metasenv subst (arg :: args_so_far) he t tl
942       | C.Meta _
943       | C.Appl (C.Meta _ :: _) as t ->
944           let metasenv, subst, arg, ty_arg = 
945             typeof status ~localise metasenv subst context arg None in
946           let name = guess_name status subst context ty_arg in
947           let metasenv, _, meta, _ = 
948             NCicMetaSubst.mk_meta metasenv 
949               ((name,C.Decl ty_arg) :: context) `IsType
950           in
951           let flex_prod = C.Prod (name, ty_arg, meta) in
952           (* next line grants that ty_args is a type *)
953           let metasenv,subst, flex_prod, _ =
954            typeof status ~localise metasenv subst context flex_prod None in
955 (*
956           pp (lazy ( "UNIFICATION in CTX:\n"^ 
957             status#ppcontext ~metasenv ~subst context
958             ^ "\nOF: " ^
959             status#ppterm ~metasenv ~subst ~context t ^  " === " ^
960             status#ppterm ~metasenv ~subst ~context flex_prod ^ "\n"));
961 *)
962           let metasenv, subst =
963              try NCicUnification.unify status metasenv subst context t flex_prod 
964              with exc -> raise (wrap_exc (lazy (localise orig_he, Printf.sprintf
965               ("The term %s has an inferred type %s, but is applied to the" ^^
966                " argument %s of type %s")
967               (status#ppterm ~metasenv ~subst ~context he)
968               (status#ppterm ~metasenv ~subst ~context t)
969               (status#ppterm ~metasenv ~subst ~context arg)
970               (status#ppterm ~metasenv ~subst ~context ty_arg))) 
971                  (match exc with
972                  | NCicUnification.UnificationFailure m -> 
973                      NCicUnification.Uncertain m
974                  | x -> x))
975               (* XXX coerce to funclass *)
976           in
977           let meta = NCicSubstitution.subst status ~avoid_beta_redexes:true arg meta in
978           aux metasenv subst (arg :: args_so_far) he meta tl
979       | C.Match (_,_,C.Meta _,_) 
980       | C.Match (_,_,C.Appl (C.Meta _ :: _),_) 
981       | C.Appl (C.Const (NReference.Ref (_, NReference.Fix _)) :: _) ->
982           raise (Uncertain (lazy (localise orig_he, Printf.sprintf
983             ("The term %s is here applied to %d arguments but expects " ^^
984             "only %d arguments") (status#ppterm ~metasenv ~subst ~context he)
985             (List.length args) (List.length args_so_far))))
986       | ty ->
987           let metasenv, subst, newhead, newheadty = 
988             try_coercions status ~localise metasenv subst context
989               (NCicUntrusted.mk_appl he (List.rev args_so_far)) orig_he ty
990               (NCic.Prod ("_",NCic.Implicit `Term,NCic.Implicit `Term))
991               false
992               (RefineFailure (lazy (localise orig_he, Printf.sprintf
993                ("The term %s is here applied to %d arguments but expects " ^^
994                "only %d arguments") (status#ppterm ~metasenv ~subst ~context he)
995                (List.length args) (List.length args_so_far))))
996           in
997            aux metasenv subst [] newhead newheadty (arg :: tl)
998   (*D*)in outside true; rc with exc -> outside false; raise exc
999   in
1000    (* We need to reverse the order of the new created metas since they
1001       are pushed on top of the metasenv in the wrong order *)
1002    let highest_meta = NCicMetaSubst.maxmeta () in
1003    let metasenv, subst, newhead, newheadty = 
1004     aux metasenv subst [] he ty_he args in
1005    let metasenv_old,metasenv_new =
1006     List.partition (fun (i,_) -> i <= highest_meta) metasenv
1007    in
1008     (List.rev metasenv_new) @ metasenv_old, subst, newhead, newheadty
1009   (*D*)in outside true; rc with exc -> outside false; raise exc
1010 ;;
1011
1012 let rec first f l1 l2 =
1013   match l1,l2 with
1014   | x1::tl1, x2::tl2 -> 
1015       (try f x1 x2 with Not_found -> first f tl1 tl2)
1016   | _ -> raise Not_found
1017 ;;
1018
1019 let rec find add dt t =
1020   if dt == add then t
1021   else
1022     let dl, l = 
1023       match dt, t with
1024       | C.Meta (_,(_,C.Ctx dl)), C.Meta (_,(_,C.Ctx l))
1025       | C.Appl dl,C.Appl l -> dl,l
1026       | C.Lambda (_,ds,dt), C.Lambda (_,s,t) 
1027       | C.Prod (_,ds,dt), C.Prod (_,s,t) -> [ds;dt],[s;t]
1028       | C.LetIn (_,ds,db,dt), C.LetIn (_,s,b,t) -> [ds;db;dt],[s;b;t] 
1029       | C.Match (_,dot,dt,dl),  C.Match (_,ot,t,l) -> (dot::dt::dl),(ot::t::l)
1030       | _ -> raise Not_found
1031     in
1032       first (find add) dl l
1033 ;;
1034
1035 let relocalise old_localise dt t add = 
1036   old_localise 
1037     (try find add dt t with Not_found -> assert false)
1038 ;;
1039
1040 let undebruijnate status inductive ref t rev_fl =
1041   let len = List.length rev_fl in 
1042   NCicSubstitution.psubst status (fun x -> x) 
1043    (HExtlib.list_mapi 
1044       (fun (_,_,rno,_,_,_) i -> 
1045          let i = len - i - 1 in
1046          NCic.Const 
1047            (if inductive then NReference.mk_fix i rno ref
1048             else NReference.mk_cofix i ref))
1049       rev_fl)
1050     t
1051 ;; 
1052
1053
1054 let typeof_obj 
1055   status ?(localise=fun _ -> Stdpp.dummy_loc) (uri,height,metasenv,subst,obj)
1056
1057   match obj with 
1058   | C.Constant (relevance, name, bo, ty, attr) ->
1059        let metasenv, subst, ty = 
1060          check_type status ~localise metasenv subst [] ty in
1061        let metasenv, subst, bo, ty, height = 
1062          match bo with
1063          | Some bo ->
1064              let metasenv, subst, bo, ty = 
1065                typeof status ~localise metasenv subst [] bo (Some ty) in
1066              let height = (* XXX recalculate *) height in
1067                metasenv, subst, Some bo, ty, height
1068          | None -> metasenv, subst, None, ty, 0
1069        in
1070        uri, height, metasenv, subst, 
1071          C.Constant (relevance, name, bo, ty, attr)
1072   | C.Fixpoint (inductive, fl, attr) -> 
1073       let len = List.length fl in
1074       let types, metasenv, subst, rev_fl =
1075         List.fold_left
1076          (fun (types, metasenv, subst, fl) (relevance,name,k,ty,bo) ->
1077            let metasenv, subst, ty = 
1078              check_type status ~localise metasenv subst [] ty in
1079            let dbo = NCicTypeChecker.debruijn status uri len [] ~subst bo in
1080            let localise = relocalise localise dbo bo in
1081             (name,C.Decl ty)::types,
1082               metasenv, subst, (relevance,name,k,ty,dbo,localise)::fl
1083          ) ([], metasenv, subst, []) fl (* XXX kl rimosso nel nucleo *)
1084       in
1085       let metasenv, subst, fl = 
1086         List.fold_left 
1087           (fun (metasenv,subst,fl) (relevance,name,k,ty,dbo,localise) ->
1088             let metasenv, subst, dbo, ty = 
1089               typeof status ~localise metasenv subst types dbo (Some ty)
1090             in
1091             metasenv, subst, (relevance,name,k,ty,dbo)::fl)
1092           (metasenv, subst, []) rev_fl
1093       in
1094       let height = (* XXX recalculate *) height in
1095       let fl =
1096         List.map 
1097           (fun (relevance,name,k,ty,dbo) ->
1098             let bo = 
1099               undebruijnate status inductive 
1100                (NReference.reference_of_spec uri 
1101                  (if inductive then NReference.Fix (0,k,0) 
1102                   else NReference.CoFix 0)) dbo rev_fl
1103             in
1104               relevance,name,k,ty,bo)
1105           fl
1106       in
1107        uri, height, metasenv, subst, 
1108          C.Fixpoint (inductive, fl, attr)
1109   | C.Inductive (ind, leftno, itl, attr) ->
1110      let len = List.length itl in
1111      let metasenv,subst,rev_itl,tys =
1112       List.fold_left
1113        (fun (metasenv,subst,res,ctx) (relevance,n,ty,cl) ->
1114           let metasenv, subst, ty = 
1115             check_type status ~localise metasenv subst [] ty in
1116           metasenv,subst,(relevance,n,ty,cl)::res,(n,NCic.Decl ty)::ctx
1117        ) (metasenv,subst,[],[]) itl in
1118      let metasenv,subst,itl,_ =
1119       List.fold_left
1120        (fun (metasenv,subst,res,i) (it_relev,n,ty,cl) ->
1121          let context,ty_sort = NCicReduction.split_prods status ~subst [] ~-1 ty in
1122          let sx_context_ty_rev,_= HExtlib.split_nth leftno (List.rev context) in
1123          let metasenv,subst,cl =
1124           List.fold_right
1125            (fun (k_relev,n,te) (metasenv,subst,res) ->
1126              let k_relev =
1127               try snd (HExtlib.split_nth leftno k_relev)
1128               with Failure _ -> k_relev in
1129              let te = NCicTypeChecker.debruijn status uri len [] ~subst te in
1130              let metasenv, subst, te = 
1131                check_type status ~localise metasenv subst tys te in
1132              let context,te = NCicReduction.split_prods status ~subst tys leftno te in
1133              let _,chopped_context_rev =
1134               HExtlib.split_nth (List.length tys) (List.rev context) in
1135              let sx_context_te_rev,_ =
1136               HExtlib.split_nth leftno chopped_context_rev in
1137              let metasenv,subst,_ =
1138               try
1139                List.fold_left2
1140                 (fun (metasenv,subst,context) item1 item2 ->
1141                   let (metasenv,subst),convertible =
1142                    try
1143                     match item1,item2 with
1144                       (n1,C.Decl ty1),(n2,C.Decl ty2) ->
1145                         if n1 = n2 then
1146                          NCicUnification.unify status ~test_eq_only:true metasenv
1147                           subst context ty1 ty2,true
1148                         else
1149                          (metasenv,subst),false
1150                     | (n1,C.Def (bo1,ty1)),(n2,C.Def (bo2,ty2)) ->
1151                         if n1 = n2 then
1152                          let metasenv,subst =
1153                           NCicUnification.unify status ~test_eq_only:true metasenv
1154                            subst context ty1 ty2
1155                          in
1156                           NCicUnification.unify status ~test_eq_only:true metasenv
1157                            subst context bo1 bo2,true
1158                         else
1159                          (metasenv,subst),false
1160                     | _,_ -> (metasenv,subst),false
1161                    with
1162                    | NCicUnification.Uncertain _
1163                    | NCicUnification.UnificationFailure _ ->
1164                       (metasenv,subst),false
1165                   in
1166                    let term2 =
1167                     match item2 with
1168                        _,C.Decl t -> t
1169                      | _,C.Def (b,_) -> b in
1170                    if not convertible then
1171                     raise (RefineFailure (lazy (localise term2,
1172                      ("Mismatch between the left parameters of the constructor " ^
1173                       "and those of its inductive type"))))
1174                    else
1175                     metasenv,subst,item1::context
1176                 ) (metasenv,subst,tys) sx_context_ty_rev sx_context_te_rev
1177               with Invalid_argument "List.fold_left2" -> assert false in
1178              let metasenv, subst =
1179                 let rec aux context (metasenv,subst) = function
1180                   | NCic.Meta _ -> metasenv, subst
1181                   | NCic.Implicit _ -> metasenv, subst
1182                   | NCic.Appl (NCic.Rel i :: args) as t
1183                       when i > List.length context - len ->
1184                       let lefts, _ = HExtlib.split_nth leftno args in
1185                       let ctxlen = List.length context in
1186                       let (metasenv, subst), _ = 
1187                         List.fold_left
1188                         (fun ((metasenv, subst),l) arg ->
1189                           NCicUnification.unify status 
1190                            ~test_eq_only:true metasenv subst context arg 
1191                              (NCic.Rel (ctxlen - len - l)), l+1
1192                           )
1193                         ((metasenv, subst), 0) lefts
1194                       in
1195                       metasenv, subst
1196                   | t -> NCicUtils.fold (fun e c -> e::c) context aux
1197                   (metasenv,subst) t
1198                 in
1199                aux context (metasenv,subst) te
1200              in
1201              let con_sort= NCicTypeChecker.typeof status ~subst ~metasenv context te in
1202               (match
1203                 NCicReduction.whd status ~subst context con_sort,
1204                 NCicReduction.whd status ~subst [] ty_sort
1205                with
1206                   (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) ->
1207                    if not (NCicEnvironment.universe_leq u1 u2) then
1208                     raise
1209                      (RefineFailure
1210                        (lazy(localise te, "The type " ^
1211                          status#ppterm ~metasenv ~subst ~context s1 ^
1212                          " of the constructor is not included in the inductive"^
1213                          " type sort " ^
1214                          status#ppterm ~metasenv ~subst ~context s2)))
1215                 | C.Sort _, C.Sort C.Prop
1216                 | C.Sort _, C.Sort C.Type _ -> ()
1217                 | _, _ ->
1218                    raise
1219                     (RefineFailure
1220                       (lazy (localise te,
1221                         "Wrong constructor or inductive arity shape"))));
1222               (* let's check also the positivity conditions *)
1223               if 
1224                not
1225                (NCicTypeChecker.are_all_occurrences_positive status
1226                  ~subst context uri leftno (i+leftno) leftno (len+leftno) te) 
1227               then
1228                 raise
1229                   (RefineFailure
1230                     (lazy (localise te,
1231                       "Non positive occurence in " ^
1232                         status#ppterm ~metasenv ~subst ~context te)))
1233               else
1234                let relsno = List.length itl + leftno in
1235                let te = 
1236                  NCicSubstitution.psubst status
1237                   (fun i ->
1238                     if i <= leftno  then
1239                      NCic.Rel i
1240                     else
1241                      NCic.Const (NReference.reference_of_spec uri
1242                       (NReference.Ind (ind,relsno - i,leftno))))
1243                   (HExtlib.list_seq 1 (relsno+1))
1244                    te in
1245                let te =
1246                 List.fold_right
1247                  (fun (name,decl) te ->
1248                    match decl with
1249                       NCic.Decl ty -> NCic.Prod (name,ty,te)
1250                     | NCic.Def (bo,ty) -> NCic.LetIn (name,ty,bo,te)
1251                  ) sx_context_te_rev te
1252                in
1253                 metasenv,subst,(k_relev,n,te)::res
1254               ) cl (metasenv,subst,[])
1255          in
1256           metasenv,subst,(it_relev,n,ty,cl)::res,i+1
1257        ) (metasenv,subst,[],1) rev_itl
1258      in
1259       uri, height, metasenv, subst, C.Inductive (ind, leftno, itl, attr)
1260 ;;
1261
1262 (* vim:set foldmethod=marker: *)