]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_refiner/nCicRefiner.ml
Fixed a problem of lifting.
[helm.git] / helm / software / 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 indent = ref "";;
22 let inside c = indent := !indent ^ String.make 1 c;;
23 let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
24
25
26 (*
27 let pp s = 
28   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
29 ;;  
30 *)
31
32
33 let pp _ = ();;
34
35 let wrap_exc msg = function
36   | NCicUnification.Uncertain _ -> Uncertain msg
37   | NCicUnification.UnificationFailure _ -> RefineFailure msg
38   | NCicTypeChecker.TypeCheckerFailure _ -> RefineFailure msg
39   | e -> raise e
40 ;;
41
42 let exp_implicit metasenv context expty =
43  let foo x = match expty with Some t -> `WithType t | None -> x in
44  function      
45   | `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Term)
46   | `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type)
47   | `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term)
48   | _ -> assert false
49 ;;
50
51
52 let check_allowed_sort_elimination hdb localise r orig =
53    let mkapp he arg =
54      match he with
55      | C.Appl l -> C.Appl (l @ [arg])
56      | t -> C.Appl [t;arg] in
57    (* ctx, ind_type @ lefts, sort_of_ind_ty@lefts, outsort *)
58    let rec aux metasenv subst context ind arity1 arity2 =
59      (*D*)inside 'S'; try let rc = 
60      let arity1 = NCicReduction.whd ~subst context arity1 in
61      pp (lazy(NCicPp.ppterm ~subst ~metasenv ~context arity1 ^ "   elimsto   " ^
62         NCicPp.ppterm ~subst ~metasenv ~context arity2 ^ "\nMENV:\n"^
63         NCicPp.ppmetasenv ~subst metasenv));
64      match arity1 with
65      | C.Prod (name,so1,de1) (* , t ==?== C.Prod _ *) ->
66         let metasenv, meta, _ = 
67           NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) `Type 
68         in
69         let metasenv, subst = 
70           try NCicUnification.unify hdb metasenv subst context 
71                 arity2 (C.Prod (name, so1, meta)) 
72           with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf
73             "expected %s, found %s" (* XXX localizzare meglio *)
74             (NCicPp.ppterm ~subst ~metasenv ~context (C.Prod (name, so1, meta)))
75             (NCicPp.ppterm ~subst ~metasenv ~context arity2))) exc)
76         in
77         aux metasenv subst ((name, C.Decl so1)::context)
78          (mkapp (NCicSubstitution.lift 1 ind) (C.Rel 1)) de1 meta
79      | C.Sort _ (* , t ==?== C.Prod _ *) ->
80         let metasenv, meta, _ = NCicMetaSubst.mk_meta metasenv [] `Type in
81         let metasenv, subst = 
82           try NCicUnification.unify hdb metasenv subst context 
83                 arity2 (C.Prod ("_", ind, meta)) 
84           with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf
85             "expected %s, found %s" (* XXX localizzare meglio *)
86             (NCicPp.ppterm ~subst ~metasenv ~context (C.Prod ("_", ind, meta)))
87             (NCicPp.ppterm ~subst ~metasenv ~context arity2))) exc)
88         in
89         (try NCicTypeChecker.check_allowed_sort_elimination
90             ~metasenv ~subst r context ind arity1 arity2; 
91             metasenv, subst
92         with exc -> raise (wrap_exc (lazy (localise orig, 
93           "Sort elimination not allowed ")) exc))
94      | _ -> assert false
95      (*D*)in outside(); rc with exc -> outside (); raise exc
96    in
97     aux
98 ;;
99
100 let rec typeof hdb 
101   ?(localise=fun _ -> Stdpp.dummy_loc) 
102   ~look_for_coercion metasenv subst context term expty 
103 =
104   let force_ty skip_lambda metasenv subst context orig t infty expty =
105     (*D*)inside 'F'; try let rc = 
106     match expty with
107     | Some expty ->
108        (match t with
109        | C.Implicit _ -> assert false
110        | C.Lambda _ when skip_lambda -> metasenv, subst, t, expty
111        | _ ->
112           pp (lazy (
113           (NCicPp.ppterm ~metasenv ~subst ~context infty) ^  " === " ^
114           (NCicPp.ppterm ~metasenv ~subst ~context expty)));
115            try 
116              let metasenv, subst =
117                NCicUnification.unify hdb metasenv subst context infty expty 
118              in
119              metasenv, subst, t, expty
120            with exc -> 
121              try_coercions hdb ~look_for_coercion ~localise 
122                metasenv subst context t orig infty expty true exc)
123     | None -> metasenv, subst, t, infty
124     (*D*)in outside(); rc with exc -> outside (); raise exc
125   in
126   let rec typeof_aux metasenv subst context expty = 
127     fun t as orig -> 
128     (*D*)inside 'R'; try let rc = 
129     pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t));
130     pp (lazy (NCicPp.ppmetasenv ~subst metasenv));
131     let metasenv, subst, t, infty = 
132     match t with
133     | C.Rel n ->
134         let infty = 
135          (try
136            match List.nth context (n - 1) with
137            | (_,C.Decl ty) -> NCicSubstitution.lift n ty
138            | (_,C.Def (_,ty)) -> NCicSubstitution.lift n ty
139          with Failure _ -> 
140            raise (RefineFailure (lazy (localise t,"unbound variable"))))
141         in
142         metasenv, subst, t, infty
143     | C.Sort (C.Type [false,u]) -> metasenv,subst,t,(C.Sort (C.Type [true, u]))
144     | C.Sort (C.Type _) -> 
145         raise (AssertFailure (lazy ("Cannot type an inferred type: "^
146           NCicPp.ppterm ~subst ~metasenv ~context t)))
147     | C.Sort _ -> metasenv,subst,t,(C.Sort (C.Type NCicEnvironment.type0))
148     | C.Implicit infos -> 
149          let metasenv,t,ty = exp_implicit metasenv context expty infos in
150          metasenv, subst, t, ty 
151     | C.Meta (n,l) as t -> 
152        let ty =
153         try
154          let _,_,_,ty = NCicUtils.lookup_subst n subst in ty 
155         with NCicUtils.Subst_not_found _ -> try
156          let _,_,ty = NCicUtils.lookup_meta n metasenv in 
157          match ty with C.Implicit _ -> assert false | _ -> ty 
158         with NCicUtils.Meta_not_found _ ->
159          raise (AssertFailure (lazy (Printf.sprintf
160           "%s not found" (NCicPp.ppterm ~subst ~metasenv ~context t))))
161        in
162        metasenv, subst, t, NCicSubstitution.subst_meta l ty
163     | C.Const _ -> 
164        metasenv, subst, t, NCicTypeChecker.typeof ~subst ~metasenv context t
165     | C.Prod (name,(s as orig_s),(t as orig_t)) ->
166        let metasenv, subst, s, s1 = typeof_aux metasenv subst context None s in
167        let metasenv, subst, s, s1 = 
168          force_to_sort hdb ~look_for_coercion
169            metasenv subst context s orig_s localise s1 in
170        let context1 = (name,(C.Decl s))::context in
171        let metasenv, subst, t, s2 = typeof_aux metasenv subst context1 None t in
172        let metasenv, subst, t, s2 = 
173          force_to_sort hdb ~look_for_coercion
174            metasenv subst context1 t orig_t localise s2 in
175        let metasenv, subst, s, t, ty = 
176          sort_of_prod localise metasenv subst 
177            context orig_s orig_t (name,s) t (s1,s2)
178        in
179        metasenv, subst, NCic.Prod(name,s,t), ty
180     | C.Lambda (n,(s as orig_s),t) as orig ->
181        let exp_s, exp_ty_t, force_after =
182          match expty with
183          | None -> None, None, false
184          | Some expty -> 
185              match NCicReduction.whd ~subst context expty with
186              | C.Prod (_,s,t) -> Some s, Some t, false
187              | _ -> None, None, true 
188        in
189        let metasenv, subst, s, ty_s = 
190          typeof_aux metasenv subst context None s in
191        let metasenv, subst, s, _ = 
192          force_to_sort hdb ~look_for_coercion
193            metasenv subst context s orig_s localise ty_s in
194        let (metasenv,subst), exp_ty_t = 
195          match exp_s with 
196          | Some exp_s -> 
197              (try NCicUnification.unify hdb metasenv subst context s exp_s,exp_ty_t
198              with exc -> raise (wrap_exc (lazy (localise orig_s, Printf.sprintf
199                "Source type %s was expected to be %s" (NCicPp.ppterm ~metasenv
200                ~subst ~context s) (NCicPp.ppterm ~metasenv ~subst ~context
201                exp_s))) exc))
202          | None -> (metasenv, subst), None
203        in
204        let context_for_t = (n,C.Decl s) :: context in
205        let metasenv, subst, t, ty_t = 
206          typeof_aux metasenv subst context_for_t exp_ty_t t 
207        in
208        if force_after then
209          force_ty false metasenv subst context orig 
210            (C.Lambda(n,s,t)) (C.Prod (n,s,ty_t)) expty
211        else 
212          metasenv, subst, C.Lambda(n,s,t), C.Prod (n,s,ty_t)
213     | C.LetIn (n,(ty as orig_ty),t,bo) ->
214        let metasenv, subst, ty, ty_ty = 
215          typeof_aux metasenv subst context None ty in
216        let metasenv, subst, ty, _ = 
217          force_to_sort hdb ~look_for_coercion
218            metasenv subst context ty orig_ty localise ty_ty in
219        let metasenv, subst, t, _ = 
220          typeof_aux metasenv subst context (Some ty) t in
221        let context1 = (n, C.Def (t,ty)) :: context in
222        let metasenv, subst, bo, bo_ty = 
223          typeof_aux metasenv subst context1 None bo 
224        in
225        let bo_ty = NCicSubstitution.subst ~avoid_beta_redexes:true t bo_ty in
226        metasenv, subst, C.LetIn (n, ty, t, bo), bo_ty
227     | C.Appl ((he as orig_he)::(_::_ as args)) ->
228        let metasenv, subst, he, ty_he = 
229          typeof_aux metasenv subst context None he in
230        eat_prods hdb ~localise ~look_for_coercion 
231          metasenv subst context orig_he he ty_he args
232    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
233    | C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as r,
234           outtype,(term as orig_term),pl) as orig ->
235       let _, leftno, itl, _, _ = NCicEnvironment.get_checked_indtys r in
236       let _, _, arity, cl = List.nth itl tyno in
237       let constructorsno = List.length cl in
238       let _, metasenv, args = 
239         NCicMetaSubst.saturate metasenv subst context arity 0 in
240       let ind = if args = [] then C.Const r else C.Appl (C.Const r::args) in
241       let metasenv, subst, term, _ = 
242         typeof_aux metasenv subst context (Some ind) term in
243       let metasenv, subst, outtype, outsort = 
244         typeof_aux metasenv subst context None outtype in
245       let parameters, arguments = HExtlib.split_nth leftno args in
246       (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
247       let ind =
248         if parameters = [] then C.Const r
249         else C.Appl ((C.Const r)::parameters) in
250       let metasenv, subst, ind, ind_ty = 
251         typeof_aux metasenv subst context None ind in
252       let metasenv, subst = 
253          check_allowed_sort_elimination hdb localise r orig_term metasenv subst 
254            context ind ind_ty outsort 
255       in
256       (* let's check if the type of branches are right *)
257       if List.length pl <> constructorsno then
258        raise (RefineFailure (lazy (localise orig, 
259          "Wrong number of cases in a match")));
260       let _, metasenv, subst, pl_rev =
261         List.fold_left
262           (fun (j, metasenv, subst, branches) p ->
263               let cons = 
264                 let cons = Ref.mk_constructor j r in
265                 if parameters = [] then C.Const cons
266                 else C.Appl (C.Const cons::parameters)
267               in
268               let metasenv, subst, cons, ty_cons = 
269                 typeof_aux metasenv subst context None cons in
270               let ty_branch = 
271                 NCicTypeChecker.type_of_branch 
272                   ~subst context leftno outtype cons ty_cons in
273               pp (lazy ("TYPEOFBRANCH: " ^
274                NCicPp.ppterm ~metasenv ~subst ~context p ^ " ::: " ^
275                NCicPp.ppterm ~metasenv ~subst ~context ty_branch ));
276               let metasenv, subst, p, _ = 
277                 typeof_aux metasenv subst context (Some ty_branch) p in
278               j+1, metasenv, subst, p :: branches)
279           (1, metasenv, subst, []) pl
280       in
281       metasenv, subst, 
282       C.Match (r, outtype, term, List.rev pl_rev),
283       NCicReduction.head_beta_reduce (C.Appl (outtype::arguments@[term]))
284     | C.Match _ as orig -> 
285         prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context orig);
286         assert false
287     in
288     pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " :: "^
289          NCicPp.ppterm ~metasenv ~subst ~context infty ));
290       force_ty true metasenv subst context orig t infty expty
291     (*D*)in outside(); rc with exc -> outside (); raise exc
292   in
293     typeof_aux metasenv subst context expty term
294
295 and try_coercions hdb 
296   ~localise ~look_for_coercion 
297   metasenv subst context t orig_t infty expty perform_unification exc 
298 =
299   (* we try with a coercion *)
300   let rec first exc = function
301   | [] ->         
302       raise (wrap_exc (lazy (localise orig_t, Printf.sprintf
303         "The term %s has type %s but is here used with type %s"
304         (NCicPp.ppterm ~metasenv ~subst ~context t)
305         (NCicPp.ppterm ~metasenv ~subst ~context infty)
306         (NCicPp.ppterm ~metasenv ~subst ~context expty))) exc)
307   | (metasenv, newterm, newtype, meta)::tl ->
308       try 
309           pp (lazy ( "UNIFICATION in CTX:\n"^ 
310             NCicPp.ppcontext ~metasenv ~subst context
311             ^ "\nMENV: " ^
312             NCicPp.ppmetasenv metasenv ~subst
313             ^ "\nOF: " ^
314             NCicPp.ppterm ~metasenv ~subst ~context meta ^  " === " ^
315             NCicPp.ppterm ~metasenv ~subst ~context t ^ "\n"));
316         let metasenv, subst = 
317           NCicUnification.unify hdb metasenv subst context meta t
318         in
319           pp (lazy ( "UNIFICATION in CTX:\n"^ 
320             NCicPp.ppcontext ~metasenv ~subst context
321             ^ "\nMENV: " ^
322             NCicPp.ppmetasenv metasenv ~subst
323             ^ "\nOF: " ^
324             NCicPp.ppterm ~metasenv ~subst ~context newtype ^  " === " ^
325             NCicPp.ppterm ~metasenv ~subst ~context expty ^ "\n"));
326         let metasenv, subst = 
327           if perform_unification then
328             NCicUnification.unify hdb metasenv subst context newtype expty
329           else metasenv, subst
330         in
331         metasenv, subst, newterm, newtype
332       with 
333       | NCicUnification.UnificationFailure _ -> first exc tl
334       | NCicUnification.Uncertain _ as exc -> first exc tl
335   in 
336     first exc
337       (look_for_coercion metasenv subst context infty expty)
338
339 and force_to_sort hdb 
340   ~look_for_coercion metasenv subst context t orig_t localise ty 
341 =
342   match NCicReduction.whd ~subst context ty with
343   | C.Meta (_,(0,(C.Irl 0 | C.Ctx []))) as ty -> 
344      metasenv, subst, t, ty
345   | C.Meta (i,(_,(C.Irl 0 | C.Ctx []))) -> 
346      metasenv, subst, t, C.Meta(i,(0,C.Irl 0))
347   | C.Meta (i,(_,lc)) ->
348      let len = match lc with C.Irl len->len | C.Ctx l->List.length l in
349      let metasenv, subst, newmeta = 
350        if len > 0 then
351          NCicMetaSubst.restrict metasenv subst i (HExtlib.list_seq 1 (len+1)) 
352        else metasenv, subst, i
353      in
354      metasenv, subst, t, C.Meta (newmeta,(0,C.Irl 0))
355   | C.Sort _ as ty -> metasenv, subst, t, ty 
356   | ty -> 
357       try_coercions hdb ~localise ~look_for_coercion metasenv subst context
358         t orig_t ty (NCic.Sort (NCic.Type NCicEnvironment.type0)) false 
359          (Uncertain (lazy (localise orig_t, 
360          "The type of " ^ NCicPp.ppterm ~metasenv ~subst ~context t
361          ^ " is not a sort: " ^ NCicPp.ppterm ~metasenv ~subst ~context ty)))
362
363 and sort_of_prod 
364   localise metasenv subst context orig_s orig_t (name,s) t (t1, t2) 
365 =
366    (* force to sort is done in the Prod case in typeof *)
367    match t1, t2 with
368    | C.Sort _, C.Sort C.Prop -> metasenv, subst, s, t, t2
369    | C.Sort (C.Type u1), C.Sort (C.Type u2) ->
370         metasenv, subst, s, t, C.Sort (C.Type (NCicEnvironment.max u1 u2)) 
371    | C.Sort C.Prop,C.Sort (C.Type _) -> metasenv, subst, s, t, t2
372    | C.Meta _, C.Sort _ 
373    | C.Meta _, C.Meta (_,(_,_))
374    | C.Sort _, C.Meta (_,(_,_)) -> metasenv, subst, s, t, t2 
375    | x, (C.Sort _ | C.Meta _) | _, x -> 
376       let y, context, orig = 
377         if x == t1 then s, context, orig_s 
378         else t, ((name,C.Decl s)::context), orig_t
379       in
380       raise (RefineFailure (lazy (localise orig,Printf.sprintf
381         "%s is expected to be a type, but its type is %s that is not a sort" 
382          (NCicPp.ppterm ~subst ~metasenv ~context y) 
383          (NCicPp.ppterm ~subst ~metasenv ~context x))))
384
385 and eat_prods hdb
386   ~localise ~look_for_coercion metasenv subst context orig_he he ty_he args 
387 =
388   (*D*)inside 'E'; try let rc = 
389   let rec aux metasenv subst args_so_far he ty_he = function 
390   | []->metasenv, subst, NCicUntrusted.mk_appl he (List.rev args_so_far), ty_he
391   | arg::tl ->
392       match NCicReduction.whd ~subst context ty_he with 
393       | C.Prod (_,s,t) ->
394           let metasenv, subst, arg, _ = 
395             typeof hdb ~look_for_coercion ~localise 
396               metasenv subst context arg (Some s) in
397           let t = NCicSubstitution.subst ~avoid_beta_redexes:true arg t in
398           aux metasenv subst (arg :: args_so_far) he t tl
399       | C.Meta _
400       | C.Appl (C.Meta _ :: _) as t ->
401           let metasenv, subst, arg, ty_arg = 
402             typeof hdb ~look_for_coercion ~localise 
403               metasenv subst context arg None in
404           let metasenv, meta, _ = 
405             NCicMetaSubst.mk_meta metasenv 
406               (("_",C.Decl ty_arg) :: context) `Type
407           in
408           let flex_prod = C.Prod ("_", ty_arg, meta) in
409           (* next line grants that ty_args is a type *)
410           let metasenv,subst, flex_prod, _ =
411            typeof hdb ~look_for_coercion ~localise metasenv subst
412             context flex_prod None in
413           pp (lazy ( "UNIFICATION in CTX:\n"^ 
414             NCicPp.ppcontext ~metasenv ~subst context
415             ^ "\nOF: " ^
416             NCicPp.ppterm ~metasenv ~subst ~context t ^  " === " ^
417             NCicPp.ppterm ~metasenv ~subst ~context flex_prod ^ "\n"));
418           let metasenv, subst = 
419              try NCicUnification.unify hdb metasenv subst context t flex_prod 
420              with exc -> raise (wrap_exc (lazy (localise orig_he, Printf.sprintf
421               ("The term %s has an inferred type %s, but is applied to the" ^^
422                " argument %s of type %s")
423               (NCicPp.ppterm ~metasenv ~subst ~context he)
424               (NCicPp.ppterm ~metasenv ~subst ~context t)
425               (NCicPp.ppterm ~metasenv ~subst ~context arg)
426               (NCicPp.ppterm ~metasenv ~subst ~context ty_arg))) exc)
427               (* XXX coerce to funclass *)
428           in
429           let meta = NCicSubstitution.subst ~avoid_beta_redexes:true arg meta in
430           aux metasenv subst (arg :: args_so_far) he meta tl
431       | C.Match (_,_,C.Meta _,_) 
432       | C.Match (_,_,C.Appl (C.Meta _ :: _),_) 
433       | C.Appl (C.Const (NReference.Ref (_, NReference.Fix _)) :: _) ->
434           raise (Uncertain (lazy (localise orig_he, Printf.sprintf
435             ("The term %s is here applied to %d arguments but expects " ^^
436             "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he)
437             (List.length args) (List.length args_so_far))))
438       | ty ->
439           let metasenv, subst, newhead, newheadty = 
440             try_coercions hdb ~localise ~look_for_coercion metasenv subst context
441               (NCicUntrusted.mk_appl he (List.rev args_so_far)) orig_he ty
442               (NCic.Prod ("_",NCic.Implicit `Term,NCic.Implicit `Term))
443               false
444               (RefineFailure (lazy (localise orig_he, Printf.sprintf
445                ("The term %s is here applied to %d arguments but expects " ^^
446                "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he)
447                (List.length args) (List.length args_so_far))))
448           in
449           aux metasenv subst [] newhead newheadty (arg :: tl)
450   in
451    aux metasenv subst [] he ty_he args
452   (*D*)in outside(); rc with exc -> outside (); raise exc
453 ;;
454
455 let rec first f l1 l2 =
456   match l1,l2 with
457   | x1::tl1, x2::tl2 -> 
458       (try f x1 x2 with Not_found -> first f tl1 tl2)
459   | _ -> raise Not_found
460 ;;
461
462 let rec find add dt t =
463   if dt == add then t
464   else
465     let dl, l = 
466       match dt, t with
467       | C.Meta (_,(_,C.Ctx dl)), C.Meta (_,(_,C.Ctx l))
468       | C.Appl dl,C.Appl l -> dl,l
469       | C.Lambda (_,ds,dt), C.Lambda (_,s,t) 
470       | C.Prod (_,ds,dt), C.Prod (_,s,t) -> [ds;dt],[s;t]
471       | C.LetIn (_,ds,db,dt), C.LetIn (_,s,b,t) -> [ds;db;dt],[s;b;t] 
472       | C.Match (_,dot,dt,dl),  C.Match (_,ot,t,l) -> (dot::dt::dl),(ot::t::l)
473       | _ -> raise Not_found
474     in
475       first (find add) dl l
476 ;;
477
478 let relocalise old_localise dt t add = 
479   old_localise 
480     (try find add dt t with Not_found -> assert false)
481 ;;
482
483 let undebruijnate inductive ref t rev_fl =
484   NCicSubstitution.psubst (fun x -> x) 
485     (HExtlib.list_mapi 
486       (fun (_,_,rno,_,_,_) i -> 
487          NCic.Const 
488            (if inductive then NReference.mk_fix i rno ref
489             else NReference.mk_cofix i ref))
490       rev_fl)
491     t
492 ;; 
493
494
495 let typeof_obj hdb 
496   ?(localise=fun _ -> Stdpp.dummy_loc) 
497   ~look_for_coercion (uri,height,metasenv,subst, obj)
498
499   let check_type metasenv subst (ty as orig_ty) =  (* XXX fattorizza *)
500     let metasenv, subst, ty, sort = 
501       typeof hdb ~localise ~look_for_coercion metasenv subst [] ty None
502     in
503     let metasenv, subst, ty, _ = 
504       force_to_sort hdb ~look_for_coercion 
505         metasenv subst [] ty orig_ty localise sort
506     in
507       metasenv, subst, ty
508   in
509   match obj with 
510   | C.Constant (relevance, name, bo, ty , attr) ->
511        let metasenv, subst, ty = check_type metasenv subst ty in
512        let metasenv, subst, bo, ty, height = 
513          match bo with
514          | Some bo ->
515              let metasenv, subst, bo, ty = 
516                typeof hdb ~localise ~look_for_coercion 
517                  metasenv subst [] bo (Some ty)
518              in
519              let height = (* XXX recalculate *) height in
520                metasenv, subst, Some bo, ty, height
521          | None -> metasenv, subst, None, ty, 0
522        in
523        uri, height, metasenv, subst, 
524          C.Constant (relevance, name, bo, ty, attr)
525   | C.Fixpoint (inductive, fl, attr) -> 
526       let len = List.length fl in
527       let types, metasenv, subst, rev_fl =
528         List.fold_left
529          (fun (types, metasenv, subst, fl) (relevance,name,k,ty,bo) ->
530            let metasenv, subst, ty = check_type metasenv subst ty in
531            let dbo = NCicTypeChecker.debruijn uri len [] bo in
532            let localise = relocalise localise dbo bo in
533             (name,C.Decl ty)::types,
534               metasenv, subst, (relevance,name,k,ty,dbo,localise)::fl
535          ) ([], metasenv, subst, []) fl (* XXX kl rimosso nel nucleo *)
536       in
537       let metasenv, subst, fl = 
538         List.fold_left 
539           (fun (metasenv,subst,fl) (relevance,name,k,ty,dbo,localise) ->
540             let metasenv, subst, dbo, ty = 
541               typeof hdb ~localise ~look_for_coercion 
542                 metasenv subst types dbo (Some ty)
543             in
544             metasenv, subst, (relevance,name,k,ty,dbo)::fl)
545           (metasenv, subst, []) rev_fl
546       in
547       let height = (* XXX recalculate *) height in
548       let fl =
549         List.map 
550           (fun (relevance,name,k,ty,dbo) ->
551             let bo = 
552               undebruijnate inductive 
553                (NReference.reference_of_spec uri 
554                  (if inductive then NReference.Fix (0,k,0) 
555                   else NReference.CoFix 0)) dbo rev_fl
556             in
557               relevance,name,k,ty,bo)
558           fl
559       in
560        uri, height, metasenv, subst, 
561          C.Fixpoint (inductive, fl, attr)
562
563   | C.Inductive (ind, leftno, itl, attr) ->  assert false
564 (*
565   (* let's check if the arity of the inductive types are well formed *)
566   List.iter (fun (_,_,x,_) -> ignore (typeof ~subst ~metasenv [] x)) tyl;
567   (* let's check if the types of the inductive constructors are well formed. *)
568   let len = List.length tyl in
569   let tys = List.rev_map (fun (_,n,ty,_) -> (n,(C.Decl ty))) tyl in
570   ignore
571    (List.fold_right
572     (fun (it_relev,_,ty,cl) i ->
573        let context,ty_sort = split_prods ~subst [] ~-1 ty in
574        let sx_context_ty_rev,_ = HExtlib.split_nth leftno (List.rev context) in
575        List.iter
576          (fun (k_relev,_,te) ->
577            let _,k_relev = HExtlib.split_nth leftno k_relev in
578            let te = debruijn uri len [] te in
579            let context,te = split_prods ~subst tys leftno te in
580            let _,chopped_context_rev =
581             HExtlib.split_nth (List.length tys) (List.rev context) in
582            let sx_context_te_rev,_ =
583             HExtlib.split_nth leftno chopped_context_rev in
584            (try
585              ignore (List.fold_left2
586               (fun context item1 item2 ->
587                 let convertible =
588                  match item1,item2 with
589                    (n1,C.Decl ty1),(n2,C.Decl ty2) ->
590                      n1 = n2 && 
591                      R.are_convertible ~metasenv ~subst context ty1 ty2
592                  | (n1,C.Def (bo1,ty1)),(n2,C.Def (bo2,ty2)) ->
593                      n1 = n2
594                      && R.are_convertible ~metasenv ~subst context ty1 ty2
595                      && R.are_convertible ~metasenv ~subst context bo1 bo2
596                  | _,_ -> false
597                 in
598                  if not convertible then
599                   raise (TypeCheckerFailure (lazy
600                    ("Mismatch between the left parameters of the constructor " ^
601                     "and those of its inductive type")))
602                  else
603                   item1::context
604               ) [] sx_context_ty_rev sx_context_te_rev)
605             with Invalid_argument "List.fold_left2" -> assert false);
606            let con_sort = typeof ~subst ~metasenv context te in
607            (match R.whd ~subst context con_sort, R.whd ~subst [] ty_sort with
608                (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) ->
609                 if not (E.universe_leq u1 u2) then
610                  raise
611                   (TypeCheckerFailure
612                     (lazy ("The type " ^ PP.ppterm ~metasenv ~subst ~context s1^
613                       " of the constructor is not included in the inductive" ^
614                       " type sort " ^ PP.ppterm ~metasenv ~subst ~context s2)))
615              | C.Sort _, C.Sort C.Prop
616              | C.Sort _, C.Sort C.Type _ -> ()
617              | _, _ ->
618                 raise
619                  (TypeCheckerFailure
620                    (lazy ("Wrong constructor or inductive arity shape"))));
621            (* let's check also the positivity conditions *)
622            if 
623              not
624                (are_all_occurrences_positive ~subst context uri leftno
625                  (i+leftno) leftno (len+leftno) te) 
626            then
627              raise
628                (TypeCheckerFailure
629                  (lazy ("Non positive occurence in "^NUri.string_of_uri
630                  uri)))
631            else check_relevance ~subst ~metasenv context k_relev te) 
632          cl;
633         check_relevance ~subst ~metasenv [] it_relev ty;
634         i+1)
635     tyl 1)
636 *)
637
638
639 ;;
640
641
642
643 (* vim:set foldmethod=marker: *)