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.
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_______________________________________________________________ *)
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;;
19 module Ref = NReference
21 type 'a expected_type = [ `XTNone (* unknown *)
22 | `XTSome of 'a (* the given term *)
23 | `XTSort (* any sort *)
24 | `XTInd (* any (co)inductive type *)
27 let debug = ref false;;
32 prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
37 let time1 = Unix.gettimeofday () in
38 indent := !indent ^ String.make 1 c;
39 times := time1 :: !times;
40 prerr_endline ("{{{" ^ !indent ^ " ")
46 let time2 = Unix.gettimeofday () in
48 match !times with time1::tl -> times := tl; time1 | [] -> assert false in
49 prerr_endline ("}}} " ^ string_of_float (time2 -. time1));
50 if not ok then prerr_endline "exception raised!";
52 indent := String.sub !indent 0 (String.length !indent -1)
54 Invalid_argument _ -> indent := "??"; ()
59 let wrap_exc msg = function
60 | NCicUnification.Uncertain _ -> Uncertain msg
61 | NCicUnification.UnificationFailure _ -> RefineFailure msg
62 | NCicTypeChecker.TypeCheckerFailure _ -> RefineFailure msg
66 let exp_implicit status ~localise metasenv subst context with_type t =
69 let metasenv,subst,expty =
73 | `XTNone -> metasenv,subst,None
75 let (metasenv,subst),typ =
77 NCicMetaSubst.delift status
78 ~unify:(fun m s c t1 t2 ->
79 try Some (NCicUnification.unify status m s c t1 t2)
80 with NCicUnification.UnificationFailure _ | NCicUnification.Uncertain _ -> None)
81 metasenv subst context (-1) (0,C.Irl 0) typ
83 NCicMetaSubst.MetaSubstFailure _
84 | NCicMetaSubst.Uncertain _ ->
85 raise (RefineFailure (lazy (localise t,"Trying to create a closed meta with a non closed type: " ^ status#ppterm ~metasenv ~subst ~context typ)))
88 metasenv,subst,Some typ
90 NCicMetaSubst.mk_meta metasenv [] ?with_type:expty `IsTerm,subst
92 let with_type = match with_type with `XTSome t -> Some t | _ -> None in
93 NCicMetaSubst.mk_meta metasenv context ?with_type `IsType,subst
95 let with_type = match with_type with `XTSome t -> Some t | _ -> None in
96 NCicMetaSubst.mk_meta metasenv context ?with_type `IsTerm,subst
98 let with_type = match with_type with `XTSome t -> Some t | _ -> None in
100 ~attrs:[`Name s] metasenv context ?with_type `IsTerm,subst
102 raise (RefineFailure (lazy (localise t, "A vector of implicit terms " ^
103 "can only be used in argument position")))
107 let check_allowed_sort_elimination status localise r orig =
110 | C.Appl l -> C.Appl (l @ [arg])
111 | t -> C.Appl [t;arg] in
112 (* ctx, ind_type @ lefts, sort_of_ind_ty@lefts, outsort *)
113 let rec aux metasenv subst context ind arity1 arity2 =
114 (*D*)inside 'S'; try let rc =
115 let arity1 = NCicReduction.whd status ~subst context arity1 in
116 pp (lazy(status#ppterm ~subst ~metasenv ~context arity1 ^ " elimsto " ^
117 status#ppterm ~subst ~metasenv ~context arity2 ^ "\nMENV:\n"^
118 status#ppmetasenv ~subst metasenv));
120 | C.Prod (name,so1,de1) (* , t ==?== C.Prod _ *) ->
121 let metasenv, _, meta, _ =
122 NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) `IsType
124 let metasenv, subst =
125 try NCicUnification.unify status metasenv subst context
126 arity2 (C.Prod (name, so1, meta))
127 with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf
128 "expected %s, found %s" (* XXX localizzare meglio *)
129 (status#ppterm ~subst ~metasenv ~context (C.Prod (name, so1, meta)))
130 (status#ppterm ~subst ~metasenv ~context arity2))) exc)
132 aux metasenv subst ((name, C.Decl so1)::context)
133 (mkapp (NCicSubstitution.lift status 1 ind) (C.Rel 1)) de1 meta
134 | C.Sort _ (* , t ==?== C.Prod _ *) ->
135 let metasenv, _, meta, _ = NCicMetaSubst.mk_meta metasenv [] `IsSort in
136 let metasenv, subst =
137 try NCicUnification.unify status metasenv subst context
138 arity2 (C.Prod ("_", ind, meta))
139 with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf
140 "expected %s, found %s" (* XXX localizzare meglio *)
141 (status#ppterm ~subst ~metasenv ~context (C.Prod ("_", ind, meta)))
142 (status#ppterm ~subst ~metasenv ~context arity2))) exc)
144 (try NCicTypeChecker.check_allowed_sort_elimination status
145 ~metasenv ~subst r context ind arity1 arity2;
147 with exc -> raise (wrap_exc (lazy (localise orig,
148 "Sort elimination not allowed ")) exc))
150 (*D*)in outside true; rc with exc -> outside false; raise exc
155 (* CSC: temporary thing, waiting for better times *)
156 let mk_fresh_name context name =
158 let rex = Str.regexp "[0-9']*$" in
159 let rex2 = Str.regexp "'*$" in
160 let basename = Str.global_replace rex "" in
162 ignore (Str.search_forward rex name 0);
163 let n = Str.matched_string name in
164 let n = Str.global_replace rex2 "" n in
165 if n = "" then 0 else int_of_string n
167 let name' = basename name in
168 let name' = if name' = "_" then "H" else name' in
171 (fun last (name,_) ->
172 if basename name = name' then
173 max last (suffix name)
178 name' ^ (if last = -1 then "" else string_of_int (last + 1))
179 with exn -> prerr_endline ("XXX" ^ Printexc.to_string exn); assert false
181 let rec typeof (status:#NCicCoercion.status)
182 ?(localise=fun _ -> Stdpp.dummy_loc)
183 metasenv subst context term expty
185 let force_ty skip_lambda skip_appl metasenv subst context orig t infty expty =
186 (*D*)inside 'F'; try let rc =
190 | C.Implicit _ -> assert false
191 | C.Lambda _ when skip_lambda -> metasenv, subst, t, expty
192 | C.Appl _ when skip_appl -> metasenv, subst, t, expty
194 pp (lazy ("forcing infty=expty: "^
195 (status#ppterm ~metasenv ~subst ~context infty) ^ " === " ^
196 (status#ppterm ~metasenv ~subst:[] ~context expty)));
198 let metasenv, subst =
199 (*D*)inside 'U'; try let rc =
200 NCicUnification.unify status metasenv subst context infty expty
201 (*D*)in outside true; rc with exc -> outside false; raise exc
203 metasenv, subst, t, expty
205 | NCicUnification.Uncertain _
206 | NCicUnification.UnificationFailure _ as exc ->
207 try_coercions status ~localise
208 metasenv subst context t orig infty (`XTSome expty) exc)
209 | `XTNone -> metasenv, subst, t, infty
212 | C.Implicit _ -> assert false
214 pp (lazy ("forcing infty=any sort: "^
215 (status#ppterm ~metasenv ~subst ~context infty) ^ " === any sort"));
216 force_to_sort status metasenv subst context t orig localise infty)
219 | C.Implicit _ -> assert false
221 pp (lazy ("forcing infty=any (co)inductive type: "^
222 (status#ppterm ~metasenv ~subst ~context infty) ^ " === any (co)inductive type"));
223 force_to_inductive status metasenv subst context t orig localise infty)
224 (*D*)in outside true; rc with exc -> outside false; raise exc
226 let rec typeof_aux metasenv subst context expty =
228 (*D*)inside 'R'; try let rc =
229 pp (lazy (status#ppterm ~metasenv ~subst ~context t ^ " ::exp:: " ^
230 match expty with `XTSort -> "Any sort" | `XTInd -> "Any (co)inductive type"
231 | `XTNone -> "None" | `XTSome e ->
232 status#ppterm ~metasenv ~subst ~context e));
233 let metasenv, subst, t, infty =
238 match List.nth context (n - 1) with
239 | (_,C.Decl ty) -> NCicSubstitution.lift status n ty
240 | (_,C.Def (_,ty)) -> NCicSubstitution.lift status n ty
242 raise (RefineFailure (lazy (localise t,"unbound variable"))))
244 metasenv, subst, t, infty
246 (try metasenv, subst, t, C.Sort (NCicEnvironment.typeof_sort s)
248 | NCicEnvironment.UntypableSort msg ->
249 raise (RefineFailure (lazy (localise t, Lazy.force msg)))
250 | NCicEnvironment.AssertFailure msg -> raise (AssertFailure msg))
251 | C.Implicit infos ->
252 let (metasenv,_,t,ty),subst =
253 exp_implicit status ~localise metasenv subst context expty t infos
256 | `XTSome _ -> metasenv, subst, t, ty
257 | _ -> typeof_aux metasenv subst context expty t)
258 | C.Meta (n,l) as t ->
261 let _,_,_,ty = NCicUtils.lookup_subst n subst in metasenv, ty
262 with NCicUtils.Subst_not_found _ ->
263 NCicMetaSubst.extend_meta metasenv n
265 metasenv, subst, t, NCicSubstitution.subst_meta status l ty
267 metasenv, subst, t, NCicTypeChecker.typeof status ~subst ~metasenv context t
268 | C.Prod (name,(s as orig_s),(t as orig_t)) ->
269 let metasenv, subst, s, s1 = typeof_aux metasenv subst context `XTSort s in
270 let metasenv, subst, s, s1 =
272 metasenv subst context s orig_s localise s1 in
273 let context1 = (name,(C.Decl s))::context in
274 let metasenv, subst, t, s2 = typeof_aux metasenv subst context1 `XTSort t in
275 let metasenv, subst, t, s2 =
277 metasenv subst context1 t orig_t localise s2 in
278 let metasenv, subst, s, t, ty =
279 sort_of_prod status localise metasenv subst
280 context orig_s orig_t (name,s) t (s1,s2)
282 metasenv, subst, C.Prod(name,s,t), ty
283 | C.Lambda (n,(s as orig_s),t) as orig ->
284 let exp_s, exp_ty_t, force_after =
288 | `XTNone -> `XTNone, `XTNone, false
290 match NCicReduction.whd status ~subst context expty with
291 | C.Prod (_,s,t) -> `XTSome s, `XTSome t, false
292 | _ -> `XTNone, `XTNone, true
294 let (metasenv,subst), s =
297 (* optimized case: implicit and implicitly typed meta
298 * the optimization prevents proliferation of metas *)
300 | C.Implicit _ -> (metasenv,subst),exp_s
302 let metasenv, subst, s = match s with
304 when (try (match NCicUtils.lookup_meta n metasenv with
305 | _,_,C.Implicit (`Typeof _) -> true
308 | _ -> false) -> metasenv, subst, s
309 | _ -> check_type status ~localise metasenv subst context s in
311 pp(lazy("Force source to: "^status#ppterm ~metasenv ~subst
313 NCicUnification.unify ~test_eq_only:true status metasenv subst context s exp_s, s
314 with exc -> raise (wrap_exc (lazy (localise orig_s, Printf.sprintf
315 "Source type %s was expected to be %s" (status#ppterm ~metasenv
316 ~subst ~context s) (status#ppterm ~metasenv ~subst ~context
321 let metasenv, subst, s =
322 check_type status ~localise metasenv subst context s in
325 let context_for_t = (n,C.Decl s) :: context in
326 let metasenv, subst, t, ty_t =
327 typeof_aux metasenv subst context_for_t exp_ty_t t
330 force_ty false true metasenv subst context orig
331 (C.Lambda(n,s,t)) (C.Prod (n,s,ty_t)) expty
333 metasenv, subst, C.Lambda(n,s,t), C.Prod (n,s,ty_t)
334 | C.LetIn (n,ty,t,bo) ->
335 let metasenv, subst, ty =
336 check_type status ~localise metasenv subst context ty in
337 let metasenv, subst, t, _ =
338 typeof_aux metasenv subst context (`XTSome ty) t in
339 let context1 = (n, C.Def (t,ty)) :: context in
340 let metasenv, subst, expty1 =
344 NCicUnification.delift_type_wrt_terms
345 status metasenv subst context1 (NCicSubstitution.lift status 1 x)
346 [NCicSubstitution.lift status 1 t]
349 | _ -> metasenv, subst, expty
351 let metasenv, subst, bo, bo_ty =
352 typeof_aux metasenv subst context1 expty1 bo
354 let bo_ty = NCicSubstitution.subst status ~avoid_beta_redexes:true t bo_ty in
355 metasenv, subst, C.LetIn (n, ty, t, bo), bo_ty
356 | C.Appl ((he as orig_he)::(_::_ as args)) ->
357 let upto = match orig_he with C.Meta _ -> List.length args | _ -> 0 in
359 if upto > 0 then NCicReduction.head_beta_reduce status ~upto t else t
361 let refine_appl metasenv subst args =
362 let metasenv, subst, he, ty_he =
363 typeof_aux metasenv subst context `XTNone he in
364 let metasenv, subst, t, ty =
365 eat_prods status ~localise force_ty metasenv subst context expty t
366 orig_he he ty_he args in
367 metasenv, subst, hbr t, ty
369 if args = [C.Implicit `Vector] && expty <> `XTNone then
370 (* we try here to expand the vector a 0 implicits, but we use
371 * the expected type *)
373 let metasenv, subst, he, ty_he =
374 typeof_aux metasenv subst context expty he in
375 metasenv, subst, hbr he, ty_he
376 with Uncertain _ | RefineFailure _ -> refine_appl metasenv subst args
378 (* CSC: whd can be useful on he too... *)
380 C.Const (Ref.Ref (uri1,Ref.Con _)) -> (
383 match NCicReduction.whd status ~subst context expty with
384 C.Appl (C.Const (Ref.Ref (uri2,Ref.Ind _) as ref)::expargs)
385 when NUri.eq uri1 uri2 ->
387 let _,leftno,_,_,_ = NCicEnvironment.get_checked_indtys status ref in
388 let leftexpargs,_ = HExtlib.split_nth leftno expargs in
389 let rec instantiate metasenv subst revargs args =
392 (* some checks are re-done here, but it would be complex
393 to avoid them (e.g. we did not check yet that the
394 constructor is a constructor for that inductive type)*)
395 refine_appl metasenv subst ((List.rev revargs)@args)
396 | (exparg::expargs) as allexpargs ->
398 [] -> raise (Failure "Not enough args")
399 | (C.Implicit `Vector::args) as allargs ->
401 instantiate metasenv subst revargs args allexpargs
403 Sys.Break as exn -> raise exn
405 instantiate metasenv subst revargs
406 (C.Implicit `Term :: allargs) allexpargs)
408 let metasenv,subst,arg,_ =
409 typeof_aux metasenv subst context `XTNone arg in
411 NCicUnification.unify status metasenv subst context
414 instantiate metasenv subst(arg::revargs) args expargs
416 instantiate metasenv subst [] args leftexpargs
418 | Sys.Break as exn -> raise exn
420 refine_appl metasenv subst args (* to try coercions *))
421 | _ -> refine_appl metasenv subst args)
424 | `XTInd -> refine_appl metasenv subst args)
425 | _ -> refine_appl metasenv subst args)
426 | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
427 | C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as r,
428 outtype,(term as orig_term),pl) as orig ->
429 let _, leftno, itl, _, _ = NCicEnvironment.get_checked_indtys status r in
430 let _, _, arity, cl = List.nth itl tyno in
431 let constructorsno = List.length cl in
432 let _, metasenv, args =
433 NCicMetaSubst.saturate status metasenv subst context arity 0 in
434 let ind = if args = [] then C.Const r else C.Appl (C.Const r::args) in
435 let metasenv, subst, term, _ =
436 typeof_aux metasenv subst context (`XTSome ind) term in
437 let parameters, arguments = HExtlib.split_nth leftno args in
440 | C.Implicit _ as ot ->
441 let rec aux = function
442 | [] -> C.Lambda ("_",C.Implicit `Type,ot)
443 | _::tl -> C.Lambda ("_",C.Implicit `Type,aux tl)
448 let metasenv, subst, outtype, outsort =
449 typeof_aux metasenv subst context `XTNone outtype in (* this cannot be `XTSort *)
451 (* next lines are to do a subst-expansion of the outtype, so
452 that when it becomes a beta-abstraction, the beta-redex is
453 fired during substitution *)
454 let _,fresh_metanoouttype,newouttype,_ =
455 NCicMetaSubst.mk_meta metasenv context `IsTerm in
457 (fresh_metanoouttype,([`Name "outtype"],context,outtype,outsort))
459 let outtype = newouttype in
461 (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
463 if parameters = [] then C.Const r
464 else C.Appl ((C.Const r)::parameters) in
465 let metasenv, subst, ind, ind_ty =
466 typeof_aux metasenv subst context `XTNone ind in (* FG: this cannot be `XTSort *)
467 let metasenv, subst =
468 check_allowed_sort_elimination status localise r orig_term metasenv subst
469 context ind ind_ty outsort
471 (* let's check if the type of branches are right *)
472 if List.length pl <> constructorsno then
473 raise (RefineFailure (lazy (localise orig,
474 "Wrong number of cases in a match")));
476 let metasenv, subst =
478 | None -> metasenv, subst
480 NCicUnification.unify status metasenv subst context resty expty
483 let _, metasenv, subst, pl =
485 (fun p (j, metasenv, subst, branches) ->
487 let cons = Ref.mk_constructor j r in
488 if parameters = [] then C.Const cons
489 else C.Appl (C.Const cons::parameters)
491 let metasenv, subst, cons, ty_cons =
492 typeof_aux metasenv subst context `XTNone cons in (* FG: this cannot be `XTInd *)
494 NCicTypeChecker.type_of_branch status
495 ~subst context leftno outtype cons ty_cons in
496 pp (lazy ("TYPEOFBRANCH: " ^
497 status#ppterm ~metasenv ~subst ~context p ^ " ::inf:: " ^
498 status#ppterm ~metasenv ~subst ~context ty_branch ));
499 let metasenv, subst, p, _ =
500 typeof_aux metasenv subst context (`XTSome ty_branch) p in
501 j-1, metasenv, subst, p :: branches)
502 pl (List.length pl, metasenv, subst, [])
504 let resty = C.Appl (outtype::arguments@[term]) in
505 let resty = NCicReduction.head_beta_reduce status ~subst resty in
506 metasenv, subst, C.Match (r, outtype, term, pl),resty
507 | C.Match _ -> assert false
509 pp (lazy (status#ppterm ~metasenv ~subst ~context t ^ " ::inf:: "^
510 status#ppterm ~metasenv ~subst ~context infty ));
511 force_ty true true metasenv subst context orig t infty expty
512 (*D*)in outside true; rc with exc -> outside false; raise exc
514 typeof_aux metasenv subst context expty term
516 and check_type status ~localise metasenv subst context (ty as orig_ty) =
517 let metasenv, subst, ty, sort =
518 typeof status ~localise metasenv subst context ty `XTSort
520 let metasenv, subst, ty, _ =
521 force_to_sort status metasenv subst context ty orig_ty localise sort
525 and try_coercions status
526 ~localise metasenv subst context t orig_t infty expty exc
528 let cs_subst = NCicSubstitution.subst status ~avoid_beta_redexes:true in
532 pp (lazy "WWW: trying coercions -- preliminary unification");
533 let metasenv, subst =
534 NCicUnification.unify status metasenv subst context infty expty
535 in metasenv, subst, t, expty
536 | _ -> raise (Failure "Special case XTProd, XTSort or XTInd"))
539 (* we try with a coercion *)
540 let rec first exc = function
542 pp (lazy "WWW: no more coercions!");
543 raise (wrap_exc (lazy
546 `XTSome expty -> status#ppterm ~metasenv ~subst ~context expty
547 | `XTSort -> "[[sort]]"
548 | `XTProd -> "[[prod]]"
549 | `XTInd -> "[[ind]]" in
550 (localise orig_t, Printf.sprintf
551 "The term\n%s\nhas type\n%s\nbut is here used with type\n%s"
552 (status#ppterm ~metasenv ~subst ~context t)
553 (status#ppterm ~metasenv ~subst ~context infty)
555 | (_,metasenv, newterm, newtype, meta)::tl ->
557 pp (lazy("K=" ^ status#ppterm ~metasenv ~subst ~context newterm));
558 pp (lazy ( "UNIFICATION in CTX:\n"^
559 status#ppcontext ~metasenv ~subst context
561 status#ppmetasenv metasenv ~subst
563 status#ppterm ~metasenv ~subst ~context t ^ " === " ^
564 status#ppterm ~metasenv ~subst ~context meta ^ "\n"));
565 let metasenv, subst =
566 NCicUnification.unify status metasenv subst context t meta in
569 pp (lazy ( "UNIFICATION in CTX:\n"^
570 status#ppcontext ~metasenv ~subst context
572 status#ppmetasenv metasenv ~subst
574 status#ppterm ~metasenv ~subst ~context newtype ^ " === " ^
575 status#ppterm ~metasenv ~subst ~context expty ^ "\n"));
577 NCicUnification.unify status metasenv subst context newtype expty
579 metasenv, subst, newterm, newtype
581 (match NCicReduction.whd status ~subst context newtype with
582 C.Sort _ -> metasenv,subst,newterm,newtype
585 (match NCicReduction.whd status ~subst context newtype with
586 C.Const (Ref.Ref (_, Ref.Ind _)) -> metasenv,subst,newterm,newtype
589 (match NCicReduction.whd status ~subst context newtype with
590 C.Prod _ -> metasenv,subst,newterm,newtype
593 | NCicUnification.UnificationFailure _ -> first exc tl
594 | NCicUnification.Uncertain _ as exc -> first exc tl
598 pp (lazy "WWW: trying coercions -- inner check");
599 match infty, expty, t with
600 (* `XTSort|`XTProd|`XTInd + Match not implemented *)
601 | _,`XTSome expty, C.Match (Ref.Ref (_,Ref.Ind (_,tyno,leftno)) as r,outty,m,pl) ->
602 (*{{{*) pp (lazy "CASE");
603 (* {{{ helper functions *)
604 let get_cl_and_left_p refit outty =
606 | NReference.Ref (uri, NReference.Ind (_,tyno,leftno)) ->
607 let _, leftno, itl, _, _ = NCicEnvironment.get_checked_indtys status r in
608 let _, _, ty, cl = List.nth itl tyno in
609 let constructorsno = List.length cl in
612 match NCicReduction.whd status ~subst ~delta:max_int ctx t with
613 | C.Prod (name,src,tgt) ->
614 let ctx = (name, (C.Decl src)) :: ctx in
620 let rec skip_lambda_delifting t n =
623 | C.Lambda (_,_,t),n ->
624 pp (lazy ("WWW: failing term? "^ status#ppterm ~subst:[] ~metasenv:[] ~context:[] t));
625 skip_lambda_delifting
626 (* substitute dangling indices with a dummy *)
627 (NCicSubstitution.subst status (C.Sort C.Prop) t) (n - 1)
630 let get_l_r_p n = function
631 | C.Lambda (_,C.Const (Ref.Ref (_,Ref.Ind (_,_,_))),_) -> [],[]
633 (C.Const (Ref.Ref (_,Ref.Ind (_,_,_))) :: args),_) ->
634 HExtlib.split_nth n args
637 let pis = count_pis ty in
638 let rno = pis - leftno in
639 let t = skip_lambda_delifting outty rno in
640 let left_p, _ = get_l_r_p leftno t in
641 let instantiate_with_left cl =
645 (fun t p -> match t with
652 let cl = instantiate_with_left (List.map (fun (_,_,x) -> x) cl) in
653 cl, left_p, leftno, rno
656 (*{{{*) pp (lazy "CASE");
657 let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
660 let rec mkr n = function
661 | [] -> [] | _::tl -> C.Rel n :: mkr (n+1) tl
663 pp (lazy ("input replace: " ^ status#ppterm ~context:ctx ~metasenv:[] ~subst:[] bo));
665 NCicRefineUtil.replace_lifting status
666 ~equality:(fun _ -> NCicRefineUtil.alpha_equivalence status)
668 ~what:(matched::right_p)
669 ~with_what:(C.Rel 1::List.rev (mkr 2 right_p))
672 pp (lazy ("output replace: " ^ status#ppterm ~context:ctx ~metasenv:[] ~subst:[] bo));
674 | C.Lambda (name, src, tgt),_ ->
676 keep_lambdas_and_put_expty
677 ((name, C.Decl src)::ctx) tgt (NCicSubstitution.lift status 1 bo)
678 (List.map (NCicSubstitution.lift status 1) right_p) (NCicSubstitution.lift status 1 matched) (n-1))
681 (*let eq = C.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.ind(1,0,2)")) in
682 let eq_refl = C.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.con(0,1,2)")) in*)
683 let eq = C.Const (NReference.reference_of_string ("cic:/matita/basics/jmeq/jmeq.ind(1,0,2)")) in
684 let eq_refl = C.Const (NReference.reference_of_string ("cic:/matita/basics/jmeq/jmeq.con(0,1,2)")) in
686 metasenv subst context cty outty mty m i
688 let rec aux context outty par j mty m = function
689 | C.Prod (name, src, tgt) ->
692 ((name, C.Decl src) :: context)
693 (NCicSubstitution.lift status 1 outty) (C.Rel j::par) (j+1)
694 (NCicSubstitution.lift status 1 mty) (NCicSubstitution.lift status 1 m) tgt
696 C.Prod (name, src, t), k
697 | C.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r) ->
699 let k = C.Const(Ref.mk_constructor i r) in
700 NCicUntrusted.mk_appl k par
702 (* the type has no parameters, so kty = mty
704 try NCicTypechecker.typeof ~subst ~metasenv context k
705 with NCicTypeChecker.TypeCheckerFailure _ -> assert false
708 C.Appl [eq; mty; m; mty; k],
709 (NCicSubstitution.lift status 1
710 (NCicReduction.head_beta_reduce status ~delta:max_int
711 (NCicUntrusted.mk_appl outty [k])))),[mty,m,mty,k]
712 | C.Appl (C.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r)::pl) ->
713 let left_p,right_p = HExtlib.split_nth leftno pl in
714 let has_rights = right_p <> [] in
716 let k = C.Const(Ref.mk_constructor i r) in
717 NCicUntrusted.mk_appl k (left_p@par)
721 NCicTypeChecker.typeof status ~subst ~metasenv context k
723 | C.Appl (C.Const (Ref.Ref (_,Ref.Ind (_,_,_)))::args) ->
724 snd (HExtlib.split_nth leftno args)
726 with NCicTypeChecker.TypeCheckerFailure _-> assert false
730 | C.Appl (C.Const (Ref.Ref (_,Ref.Ind (_,_,_)))::args) ->
731 snd (HExtlib.split_nth leftno args)
735 (fun x y (tacc,pacc) ->
737 try NCicTypeChecker.typeof status ~subst ~metasenv context x
738 with NCicTypeChecker.TypeCheckerFailure _ -> assert false
741 try NCicTypeChecker.typeof status ~subst ~metasenv context y
742 with NCicTypeChecker.TypeCheckerFailure _ -> assert false
744 C.Prod ("_", C.Appl [eq;xty;x;yty;y],
745 NCicSubstitution.lift status 1 tacc), (xty,x,yty,y)::pacc)
746 (orig_right_p @ [m]) (right_p @ [k])
747 (NCicReduction.head_beta_reduce status ~delta:max_int
748 (NCicUntrusted.mk_appl outty (right_p@[k])), [])
750 (* if has_rights then
751 NCicReduction.head_beta_reduce status ~delta:max_int
752 (C.Appl (outty ::right_p @ [k])),k
755 C.Appl [eq; mty; m; k],
756 (NCicSubstitution.lift status 1
757 (NCicReduction.head_beta_reduce status ~delta:max_int
758 (C.Appl (outty ::right_p @ [k]))))),k*)
761 aux context outty [] 1 mty m cty
763 let add_lambda_for_refl_m pbo eqs cty =
764 (* k lives in the right context *)
765 (* if rno <> 0 then pbo else *)
766 let rec aux = function
767 | C.Lambda (name,src,bo), C.Prod (_,_,ty) ->
770 | t,_ -> snd (List.fold_right
771 (fun (xty,x,yty,y) (n,acc) -> n+1, C.Lambda ("p" ^ string_of_int n,
772 C.Appl [eq; xty; x; yty; y],
773 NCicSubstitution.lift status 1 acc)) eqs (1,t))
775 C.Appl [eq; mty; m; k],NCicSubstitution.lift status 1 t)*)
779 let add_pi_for_refl_m context new_outty mty m lno rno =
780 (*if rno <> 0 then new_outty else*)
781 let rec aux context mty m = function
782 | C.Lambda (name, src, tgt) ->
783 let context = (name, C.Decl src)::context in
784 C.Lambda (name, src, aux context (NCicSubstitution.lift status 1 mty) (NCicSubstitution.lift status 1 m) tgt)
788 | C.Appl (_::params) -> (snd (HExtlib.split_nth lno params))@[m]
792 List.map (fun x -> C.Rel x)
793 (List.rev (HExtlib.list_seq 1 (rno+2))) in
797 try NCicTypeChecker.typeof status ~subst ~metasenv context x
798 with NCicTypeChecker.TypeCheckerFailure _ -> assert false
801 try NCicTypeChecker.typeof status ~subst ~metasenv context y
802 with NCicTypeChecker.TypeCheckerFailure _ -> assert false
805 ("_", C.Appl [eq;xty;x;yty;y],
806 (NCicSubstitution.lift status 1 acc)))
809 ("_", C.Appl [eq;mty;m;C.Rel 1],
810 NCicSubstitution.lift status 1 t)*)
812 aux context mty m new_outty
813 in (* }}} end helper functions *)
814 (* constructors types with left params already instantiated *)
815 let outty = NCicUntrusted.apply_subst status subst context outty in
816 let cl, left_p, leftno,rno =
817 get_cl_and_left_p r outty
822 NCicTypeChecker.typeof status ~subst ~metasenv context m
824 | (C.Const (Ref.Ref (_,Ref.Ind (_,_,_))) | C.Meta _) as mty -> [], mty
825 | C.Appl ((C.Const (Ref.Ref (_,Ref.Ind (_,_,_)))|C.Meta _)::args) as mty ->
826 snd (HExtlib.split_nth leftno args), mty
828 with NCicTypeChecker.TypeCheckerFailure _ ->
829 raise (AssertFailure(lazy "already ill-typed matched term"))
831 let mty = NCicUntrusted.apply_subst status subst context mty in
832 let outty = NCicUntrusted.apply_subst status subst context outty in
833 let expty = NCicUntrusted.apply_subst status subst context expty in
835 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
838 (lazy ("CASE: new_outty: " ^ status#ppterm
839 ~context ~metasenv ~subst new_outty));
840 let _,pl,subst,metasenv =
842 (fun cty pbo (i, acc, s, menv) ->
843 pp (lazy ("begin iteration"));
844 (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
845 * (new_)outty right_par (K_i left_par k_par) *)
847 add_params menv s context cty outty mty m i in
849 (lazy ("CASE: infty_pbo: "^ status#ppterm
850 ~context ~metasenv ~subst infty_pbo));
851 let expty_pbo, eqs = (* k is (K_i left_par k_par) *)
852 add_params menv s context cty new_outty mty m i in
854 (lazy ("CASE: expty_pbo: "^ status#ppterm
855 ~context ~metasenv ~subst expty_pbo));
856 let pbo = add_lambda_for_refl_m pbo eqs cty in
858 (lazy ("CASE: pbo: " ^ status#ppterm
859 ~context ~metasenv ~subst pbo));
860 let metasenv, subst, pbo, _ =
861 try_coercions status ~localise menv s context pbo
862 orig_t (*??*) infty_pbo (`XTSome expty_pbo) exc
865 (lazy ("CASE: pbo2: " ^ status#ppterm
866 ~context ~metasenv ~subst pbo));
867 (i-1, pbo::acc, subst, metasenv))
868 cl pl (List.length pl, [], subst, metasenv)
870 (*let metasenv, subst =
872 NCicUnification.unify status metasenv subst context outty new_outty
873 with _ -> raise (RefineFailure (lazy (localise orig_t, "try_coercions")))
875 let new_outty = add_pi_for_refl_m context new_outty mty m leftno rno in
876 pp (lazy ("CASE: new_outty: " ^ (status#ppterm
877 ~metasenv ~subst ~context new_outty)));
880 (fun t -> NCicTypeChecker.typeof status ~subst ~metasenv context t) right_p in
882 List.map2 (fun x y -> C.Appl[eq_refl;x;y]) (right_tys@[mty])
884 let t = C.Appl (C.Match(r,new_outty,m,pl) :: eqs)
886 metasenv, subst, t, expty (*}}}*)
887 | _,`XTSome expty,C.LetIn(name,ty,t,bo) ->
889 let name' = mk_fresh_name context name in
890 let context_bo = (name', C.Def (t,ty)) :: context in
891 let metasenv, subst, bo2, _ =
892 try_coercions status ~localise metasenv subst context_bo
893 bo orig_t (NCicSubstitution.lift status 1 infty)
894 (`XTSome (NCicSubstitution.lift status 1 expty)) exc
896 let coerced = C.LetIn (name',ty,t,bo2) in
897 pp (lazy ("LETIN: coerced = " ^ status#ppterm ~metasenv ~subst ~context coerced));
898 metasenv, subst, coerced, expty
899 | C.Prod (nameprod, src, ty),`XTSome (C.Prod (_, src2, ty2) as expty), _ ->
900 (*{{{*) pp (lazy "LAM");
901 pp (lazy ("LAM: t = " ^ status#ppterm ~metasenv ~subst ~context t));
902 let namename = match t with C.Lambda (n,_,_) -> n | _ -> nameprod in
903 let name_con = mk_fresh_name context namename in
904 let context_src2 = ((name_con, C.Decl src2) :: context) in
905 (* contravariant part: the argument of f:src->ty *)
906 let metasenv, subst, rel1, _ =
907 try_coercions status ~localise metasenv subst context_src2
908 (C.Rel 1) orig_t (NCicSubstitution.lift status 1 src2)
909 (`XTSome (NCicSubstitution.lift status 1 src)) exc
911 (* covariant part: the result of f(c x); x:src2; (c x):src *)
914 | C.Lambda (n,_,bo) -> n, cs_subst rel1 (NCicSubstitution.lift_from status 2 1 bo)
915 | _ -> name_con, NCicUntrusted.mk_appl (NCicSubstitution.lift status 1 t) [rel1]
917 (* we fix the possible dependency problem in the source ty *)
918 let ty = cs_subst rel1 (NCicSubstitution.lift_from status 2 1 ty) in
919 let metasenv, subst, bo, _ =
920 try_coercions status ~localise metasenv subst context_src2
921 bo orig_t ty (`XTSome ty2) exc
923 let coerced = C.Lambda (name_t,src2, bo) in
924 pp (lazy ("LAM: coerced = " ^ status#ppterm ~metasenv ~subst ~context coerced));
925 metasenv, subst, coerced, expty (*}}}*)
930 `XTSome expty -> expty
933 (match NCicEnvironment.get_universes () with
935 | _ -> assert false))
936 | `XTProd -> C.Prod ("_",C.Implicit `Type,C.Implicit `Type)
938 pp(lazy("try_coercion " ^
939 status#ppterm ~metasenv ~subst ~context infty ^ " |---> " ^
940 status#ppterm ~metasenv ~subst ~context expty));
942 (NCicCoercion.look_for_coercion
943 status metasenv subst context infty expty)
945 and force_to_sort status metasenv subst context t orig_t localise ty =
947 let metasenv, subst, ty =
948 NCicUnification.sortfy status (Failure "sortfy") metasenv subst context ty in
949 metasenv, subst, t, ty
953 (lazy (localise orig_t,
954 "The type of " ^ status#ppterm ~metasenv ~subst ~context t ^
955 " is not a sort: " ^ status#ppterm ~metasenv ~subst ~context ty)) in
956 let ty = NCicReduction.whd status ~subst context ty in
958 if NCicUnification.could_reduce status ~subst context ty then
963 try_coercions status ~localise metasenv subst context
964 t orig_t ty `XTSort exn
966 and force_to_inductive status metasenv subst context t orig_t localise ty =
968 let metasenv, subst, ty =
969 NCicUnification.indfy status (Failure "indfy") metasenv subst context ty in
970 metasenv, subst, t, ty
974 (lazy (localise orig_t,
975 "The type of " ^ status#ppterm ~metasenv ~subst ~context t ^
976 " is not a (co)inductive type: " ^ status#ppterm ~metasenv ~subst ~context ty)) in
977 let ty = NCicReduction.whd status ~subst context ty in
978 (* prerr_endline ("#### " ^ status#ppterm ~metasenv ~subst ~context ty); *)
980 if NCicUnification.could_reduce status ~subst context ty then
986 (* FG: this should be as follows but the case `XTInd is not imp;emented yet
987 try_coercions status ~localise metasenv subst context
988 t orig_t ty `XTInd exn
991 and sort_of_prod status localise metasenv subst context orig_s orig_t (name,s)
994 (* force to sort is done in the Prod case in typeof *)
996 | C.Sort _, C.Sort C.Prop -> metasenv, subst, s, t, t2
997 | C.Sort (C.Type u1), C.Sort (C.Type u2) ->
998 metasenv, subst, s, t, C.Sort (C.Type (NCicEnvironment.max u1 u2))
999 | C.Sort C.Prop,C.Sort (C.Type _) -> metasenv, subst, s, t, t2
1000 | C.Meta _, C.Sort _
1001 | C.Meta _, C.Meta (_,(_,_))
1002 | C.Sort _, C.Meta (_,(_,_)) -> metasenv, subst, s, t, t2
1003 | x, (C.Sort _ | C.Meta _) | _, x ->
1004 let y, context, orig =
1005 if x == t1 then s, context, orig_s
1006 else t, ((name,C.Decl s)::context), orig_t
1008 raise (RefineFailure (lazy (localise orig,Printf.sprintf
1009 "%s is expected to be a type, but its type is %s that is not a sort"
1010 (status#ppterm ~subst ~metasenv ~context y)
1011 (status#ppterm ~subst ~metasenv ~context x))))
1013 and guess_name status subst ctx ty =
1014 let aux initial = "#" ^ String.make 1 initial in
1016 | C.Const (NReference.Ref (u,_))
1017 | C.Appl (C.Const (NReference.Ref (u,_)) :: _) ->
1018 aux (String.sub (NUri.name_of_uri u) 0 1).[0]
1019 | C.Prod _ -> aux 'f'
1022 let _,_,t,_ = NCicUtils.lookup_subst n subst in
1023 guess_name status subst ctx (NCicSubstitution.subst_meta status lc t)
1024 with NCicUtils.Subst_not_found _ -> aux 'M')
1027 and eat_prods status ~localise force_ty metasenv subst context expty orig_t orig_he he ty_he args =
1028 (*D*)inside 'E'; try let rc =
1029 let rec aux metasenv subst args_so_far he ty_he xxx =
1030 (*D*)inside 'V'; try let rc =
1033 let res = NCicUntrusted.mk_appl he (List.rev args_so_far) in
1034 pp(lazy("FORCE FINAL APPL: " ^
1035 status#ppterm ~metasenv ~subst ~context res ^
1036 " of type " ^ status#ppterm ~metasenv ~subst ~context ty_he
1037 ^ " to type " ^ match expty with `XTSort -> "Any sort" | `XTInd -> "Any (co)inductive type"
1038 | `XTNone -> "None" | `XTSome x ->
1039 status#ppterm ~metasenv ~subst ~context x));
1040 (* whatever the term is, we force the type. in case of ((Lambda..) ?...)
1041 * the application may also be a lambda! *)
1042 force_ty false false metasenv subst context orig_t res ty_he expty
1043 | C.Implicit `Vector::tl ->
1044 let has_some_more_pis x =
1045 match NCicReduction.whd status ~subst context x with
1046 | C.Meta _ | C.Appl (C.Meta _::_) -> false
1050 aux metasenv subst args_so_far he ty_he tl
1053 | RefineFailure _ as exc when has_some_more_pis ty_he ->
1055 aux metasenv subst args_so_far he ty_he
1056 (C.Implicit `Term :: C.Implicit `Vector :: tl)
1058 Uncertain msg | RefineFailure msg -> raise (wrap_exc msg exc))
1059 | RefineFailure msg when not (has_some_more_pis ty_he) ->
1060 (* instantiating the head could change the has_some_more_pis flag *)
1061 raise (Uncertain msg))
1063 match NCicReduction.whd status ~subst context ty_he with
1065 let metasenv, subst, arg, _ =
1066 typeof status ~localise metasenv subst context arg (`XTSome s) in
1067 let t = NCicSubstitution.subst status ~avoid_beta_redexes:true arg t in
1068 aux metasenv subst (arg :: args_so_far) he t tl
1070 | C.Appl (C.Meta _ :: _) as t ->
1071 let metasenv, subst, arg, ty_arg =
1072 typeof status ~localise metasenv subst context arg `XTNone in
1073 let name = guess_name status subst context ty_arg in
1074 let metasenv, _, meta, _ =
1075 NCicMetaSubst.mk_meta metasenv
1076 ((name,C.Decl ty_arg) :: context) `IsType
1078 let flex_prod = C.Prod (name, ty_arg, meta) in
1079 (* next line grants that ty_args is a type *)
1080 let metasenv,subst, flex_prod, _ =
1081 typeof status ~localise metasenv subst context flex_prod `XTSort in
1083 pp (lazy ( "UNIFICATION in CTX:\n"^
1084 status#ppcontext ~metasenv ~subst context
1086 status#ppterm ~metasenv ~subst ~context t ^ " === " ^
1087 status#ppterm ~metasenv ~subst ~context flex_prod ^ "\n"));
1089 let metasenv, subst =
1090 try NCicUnification.unify status metasenv subst context t flex_prod
1091 with exc -> raise (wrap_exc (lazy (localise orig_he, Printf.sprintf
1092 ("The term %s has an inferred type %s, but is applied to the" ^^
1093 " argument %s of type %s")
1094 (status#ppterm ~metasenv ~subst ~context he)
1095 (status#ppterm ~metasenv ~subst ~context t)
1096 (status#ppterm ~metasenv ~subst ~context arg)
1097 (status#ppterm ~metasenv ~subst ~context ty_arg)))
1099 | NCicUnification.UnificationFailure m ->
1100 NCicUnification.Uncertain m
1102 (* XXX coerce to funclass *)
1104 let meta = NCicSubstitution.subst status ~avoid_beta_redexes:true arg meta in
1105 aux metasenv subst (arg :: args_so_far) he meta tl
1106 | C.Match (_,_,C.Meta _,_)
1107 | C.Match (_,_,C.Appl (C.Meta _ :: _),_)
1108 | C.Appl (C.Const (NReference.Ref (_, NReference.Fix _)) :: _) ->
1109 raise (Uncertain (lazy (localise orig_he, Printf.sprintf
1110 ("The term %s is here applied to %d arguments but expects " ^^
1111 "only %d arguments") (status#ppterm ~metasenv ~subst ~context he)
1112 (List.length args) (List.length args_so_far))))
1114 let metasenv, subst, newhead, newheadty =
1115 try_coercions status ~localise metasenv subst context
1116 (NCicUntrusted.mk_appl he (List.rev args_so_far)) orig_he ty
1118 (RefineFailure (lazy (localise orig_he, Printf.sprintf
1119 ("The term %s is here applied to %d arguments but expects " ^^
1120 "only %d arguments") (status#ppterm ~metasenv ~subst ~context he)
1121 (List.length args) (List.length args_so_far))))
1123 aux metasenv subst [] newhead newheadty (arg :: tl)
1124 (*D*)in outside true; rc with exc -> outside false; raise exc
1126 (* We need to reverse the order of the new created metas since they
1127 are pushed on top of the metasenv in the wrong order *)
1128 let highest_meta = NCicMetaSubst.maxmeta () in
1129 let metasenv, subst, newhead, newheadty =
1130 aux metasenv subst [] he ty_he args in
1131 let metasenv_old,metasenv_new =
1132 List.partition (fun (i,_) -> i <= highest_meta) metasenv
1134 (List.rev metasenv_new) @ metasenv_old, subst, newhead, newheadty
1135 (*D*)in outside true; rc with exc -> outside false; raise exc
1138 let rec first f l1 l2 =
1140 | x1::tl1, x2::tl2 ->
1141 (try f x1 x2 with Not_found -> first f tl1 tl2)
1142 | _ -> raise Not_found
1145 let rec find add dt t =
1150 | C.Meta (_,(_,C.Ctx dl)), C.Meta (_,(_,C.Ctx l))
1151 | C.Appl dl,C.Appl l -> dl,l
1152 | C.Lambda (_,ds,dt), C.Lambda (_,s,t)
1153 | C.Prod (_,ds,dt), C.Prod (_,s,t) -> [ds;dt],[s;t]
1154 | C.LetIn (_,ds,db,dt), C.LetIn (_,s,b,t) -> [ds;db;dt],[s;b;t]
1155 | C.Match (_,dot,dt,dl), C.Match (_,ot,t,l) -> (dot::dt::dl),(ot::t::l)
1156 | _ -> raise Not_found
1158 first (find add) dl l
1161 let relocalise old_localise dt t add =
1163 (try find add dt t with Not_found -> assert false)
1166 let undebruijnate status inductive ref t rev_fl =
1167 let len = List.length rev_fl in
1168 NCicSubstitution.psubst status (fun x -> x)
1170 (fun (_,_,rno,_,_,_) i ->
1171 let i = len - i - 1 in
1173 (if inductive then NReference.mk_fix i rno ref
1174 else NReference.mk_cofix i ref))
1181 status ?(localise=fun _ -> Stdpp.dummy_loc) (uri,height,metasenv,subst,obj)
1184 | C.Constant (relevance, name, bo, ty, attr) ->
1185 let metasenv, subst, ty =
1186 check_type status ~localise metasenv subst [] ty in
1187 let metasenv, subst, bo, ty, height =
1190 let metasenv, subst, bo, ty =
1191 typeof status ~localise metasenv subst [] bo (`XTSome ty) in
1192 let height = (* XXX recalculate *) height in
1193 metasenv, subst, Some bo, ty, height
1194 | None -> metasenv, subst, None, ty, 0
1196 uri, height, metasenv, subst,
1197 C.Constant (relevance, name, bo, ty, attr)
1198 | C.Fixpoint (inductive, fl, attr) ->
1199 let len = List.length fl in
1200 let types, metasenv, subst, rev_fl =
1202 (fun (types, metasenv, subst, fl) (relevance,name,k,ty,bo) ->
1203 let metasenv, subst, ty =
1204 check_type status ~localise metasenv subst [] ty in
1205 let dbo = NCicTypeChecker.debruijn status uri len [] ~subst bo in
1206 let localise = relocalise localise dbo bo in
1207 (name,C.Decl ty)::types,
1208 metasenv, subst, (relevance,name,k,ty,dbo,localise)::fl
1209 ) ([], metasenv, subst, []) fl (* XXX kl rimosso nel nucleo *)
1211 let metasenv, subst, fl =
1213 (fun (metasenv,subst,fl) (relevance,name,k,ty,dbo,localise) ->
1214 let metasenv, subst, dbo, ty =
1215 typeof status ~localise metasenv subst types dbo (`XTSome ty)
1217 metasenv, subst, (relevance,name,k,ty,dbo)::fl)
1218 (metasenv, subst, []) rev_fl
1220 let height = (* XXX recalculate *) height in
1223 (fun (relevance,name,k,ty,dbo) ->
1225 undebruijnate status inductive
1226 (NReference.reference_of_spec uri
1227 (if inductive then NReference.Fix (0,k,0)
1228 else NReference.CoFix 0)) dbo rev_fl
1230 relevance,name,k,ty,bo)
1233 uri, height, metasenv, subst,
1234 C.Fixpoint (inductive, fl, attr)
1235 | C.Inductive (ind, leftno, itl, attr) ->
1236 let len = List.length itl in
1237 let metasenv,subst,rev_itl,tys =
1239 (fun (metasenv,subst,res,ctx) (relevance,n,ty,cl) ->
1240 let metasenv, subst, ty =
1241 check_type status ~localise metasenv subst [] ty in
1242 metasenv,subst,(relevance,n,ty,cl)::res,(n,C.Decl ty)::ctx
1243 ) (metasenv,subst,[],[]) itl in
1244 let metasenv,subst,itl,_ =
1246 (fun (metasenv,subst,res,i) (it_relev,n,ty,cl) ->
1247 let context,ty_sort = NCicReduction.split_prods status ~subst [] ~-1 ty in
1248 let sx_context_ty_rev,_= HExtlib.split_nth leftno (List.rev context) in
1249 let metasenv,subst,cl =
1251 (fun (k_relev,n,te) (metasenv,subst,res) ->
1253 try snd (HExtlib.split_nth leftno k_relev)
1254 with Failure _ -> k_relev in
1255 let te = NCicTypeChecker.debruijn status uri len [] ~subst te in
1256 let metasenv, subst, te =
1257 check_type status ~localise metasenv subst tys te in
1258 let context,te = NCicReduction.split_prods status ~subst tys leftno te in
1259 let _,chopped_context_rev =
1260 HExtlib.split_nth (List.length tys) (List.rev context) in
1261 let sx_context_te_rev,_ =
1262 HExtlib.split_nth leftno chopped_context_rev in
1263 let metasenv,subst,_ =
1266 (fun (metasenv,subst,context) item1 item2 ->
1267 let (metasenv,subst),convertible =
1269 match item1,item2 with
1270 (n1,C.Decl ty1),(n2,C.Decl ty2) ->
1272 NCicUnification.unify status ~test_eq_only:true metasenv
1273 subst context ty1 ty2,true
1275 (metasenv,subst),false
1276 | (n1,C.Def (bo1,ty1)),(n2,C.Def (bo2,ty2)) ->
1278 let metasenv,subst =
1279 NCicUnification.unify status ~test_eq_only:true metasenv
1280 subst context ty1 ty2
1282 NCicUnification.unify status ~test_eq_only:true metasenv
1283 subst context bo1 bo2,true
1285 (metasenv,subst),false
1286 | _,_ -> (metasenv,subst),false
1288 | NCicUnification.Uncertain _
1289 | NCicUnification.UnificationFailure _ ->
1290 (metasenv,subst),false
1295 | _,C.Def (b,_) -> b in
1296 if not convertible then
1297 raise (RefineFailure (lazy (localise term2,
1298 ("Mismatch between the left parameters of the constructor " ^
1299 "and those of its inductive type"))))
1301 metasenv,subst,item1::context
1302 ) (metasenv,subst,tys) sx_context_ty_rev sx_context_te_rev
1303 with Invalid_argument "List.fold_left2" -> assert false in
1304 let metasenv, subst =
1305 let rec aux context (metasenv,subst) = function
1306 | C.Meta _ -> metasenv, subst
1307 | C.Implicit _ -> metasenv, subst
1308 | C.Appl (C.Rel i :: args) as t
1309 when i > List.length context - len ->
1310 let lefts, _ = HExtlib.split_nth leftno args in
1311 let ctxlen = List.length context in
1312 let (metasenv, subst), _ =
1314 (fun ((metasenv, subst),l) arg ->
1315 NCicUnification.unify status
1316 ~test_eq_only:true metasenv subst context arg
1317 (C.Rel (ctxlen - len - l)), l+1
1319 ((metasenv, subst), 0) lefts
1322 | t -> NCicUtils.fold (fun e c -> e::c) context aux
1325 aux context (metasenv,subst) te
1327 let con_sort= NCicTypeChecker.typeof status ~subst ~metasenv context te in
1329 NCicReduction.whd status ~subst context con_sort,
1330 NCicReduction.whd status ~subst [] ty_sort
1332 (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) ->
1333 if not (NCicEnvironment.universe_leq u1 u2) then
1336 (lazy(localise te, "The type " ^
1337 status#ppterm ~metasenv ~subst ~context s1 ^
1338 " of the constructor is not included in the inductive"^
1340 status#ppterm ~metasenv ~subst ~context s2)))
1341 | C.Sort _, C.Sort C.Prop
1342 | C.Sort _, C.Sort C.Type _ -> ()
1347 "Wrong constructor or inductive arity shape"))));
1348 (* let's check also the positivity conditions *)
1351 (NCicTypeChecker.are_all_occurrences_positive status
1352 ~subst context uri leftno (i+leftno) leftno (len+leftno) te)
1357 "Non positive occurence in " ^
1358 status#ppterm ~metasenv ~subst ~context te)))
1360 let relsno = List.length itl + leftno in
1362 NCicSubstitution.psubst status
1367 C.Const (NReference.reference_of_spec uri
1368 (NReference.Ind (ind,relsno - i,leftno))))
1369 (HExtlib.list_seq 1 (relsno+1))
1373 (fun (name,decl) te ->
1375 C.Decl ty -> C.Prod (name,ty,te)
1376 | C.Def (bo,ty) -> C.LetIn (name,ty,bo,te)
1377 ) sx_context_te_rev te
1379 metasenv,subst,(k_relev,n,te)::res
1380 ) cl (metasenv,subst,[])
1382 metasenv,subst,(it_relev,n,ty,cl)::res,i+1
1383 ) (metasenv,subst,[],1) rev_itl
1385 uri, height, metasenv, subst, C.Inductive (ind, leftno, itl, attr)
1388 (* vim:set foldmethod=marker: *)