let inside c = indent := !indent ^ String.make 1 c;;
let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
+
(*
let pp s =
prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
;;
*)
+
let pp _ = ();;
let wrap_exc msg = function
metasenv, subst, t, NCicTypeChecker.typeof ~subst ~metasenv context t
| C.Prod (name,(s as orig_s),(t as orig_t)) ->
let metasenv, subst, s, s1 = typeof_aux metasenv subst context None s in
+ let metasenv, subst, s, s1 =
+ force_to_sort ~look_for_coercion
+ metasenv subst context s orig_s localise s1 in
let context1 = (name,(C.Decl s))::context in
let metasenv, subst, t, s2 = typeof_aux metasenv subst context1 None t in
+ let metasenv, subst, t, s2 =
+ force_to_sort ~look_for_coercion
+ metasenv subst context1 t orig_t localise s2 in
let metasenv, subst, s, t, ty =
- sort_of_prod ~look_for_coercion localise metasenv subst
+ sort_of_prod localise metasenv subst
context orig_s orig_t (name,s) t (s1,s2)
in
metasenv, subst, NCic.Prod(name,s,t), ty
(NCicPp.ppterm ~metasenv ~subst ~context expty))) exc)
| (metasenv, newterm, newtype, meta)::tl ->
try
+ pp (lazy ( "UNIFICATION in CTX:\n"^
+ NCicPp.ppcontext ~metasenv ~subst context
+ ^ "\nMENV: " ^
+ NCicPp.ppmetasenv metasenv ~subst
+ ^ "\nOF: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context meta ^ " === " ^
+ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\n"));
let metasenv, subst =
NCicUnification.unify metasenv subst context meta t
in
+ pp (lazy ( "UNIFICATION in CTX:\n"^
+ NCicPp.ppcontext ~metasenv ~subst context
+ ^ "\nMENV: " ^
+ NCicPp.ppmetasenv metasenv ~subst
+ ^ "\nOF: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context newtype ^ " === " ^
+ NCicPp.ppterm ~metasenv ~subst ~context expty ^ "\n"));
let metasenv, subst =
if perform_unification then
NCicUnification.unify metasenv subst context newtype expty
| ty ->
try_coercions ~localise ~look_for_coercion metasenv subst context
t orig_t ty (NCic.Sort (NCic.Type NCicEnvironment.type0)) false
- (RefineFailure (lazy (localise orig_t,
+ (Uncertain (lazy (localise orig_t,
"The type of " ^ NCicPp.ppterm ~metasenv ~subst ~context t
^ " is not a sort: " ^ NCicPp.ppterm ~metasenv ~subst ~context ty)))
-and sort_of_prod ~look_for_coercion
+and sort_of_prod
localise metasenv subst context orig_s orig_t (name,s) t (t1, t2)
=
- let metasenv, subst, s, t1 =
- force_to_sort
- ~look_for_coercion metasenv subst context s orig_s localise t1 in
- let metasenv, subst, t, t2 =
- force_to_sort ~look_for_coercion metasenv subst ((name,C.Decl s)::context)
- t orig_t localise t2 in
+ (* force to sort is done in the Prod case in typeof *)
match t1, t2 with
| C.Sort _, C.Sort C.Prop -> metasenv, subst, s, t, t2
| C.Sort (C.Type u1), C.Sort (C.Type u2) ->
- metasenv, subst, s, t, C.Sort (C.Type (u1@u2))
+ metasenv, subst, s, t, C.Sort (C.Type (NCicEnvironment.max u1 u2))
| C.Sort C.Prop,C.Sort (C.Type _) -> metasenv, subst, s, t, t2
| C.Meta _, C.Sort _
| C.Meta _, C.Meta (_,(_,_))
(("_",C.Decl ty_arg) :: context) `Type
in
let flex_prod = C.Prod ("_", ty_arg, meta) in
+ (* next line grants that ty_args is a type *)
+ let metasenv,subst, flex_prod, _ =
+ typeof ~look_for_coercion ~localise metasenv subst
+ context flex_prod None in
pp (lazy ( "UNIFICATION in CTX:\n"^
NCicPp.ppcontext ~metasenv ~subst context
^ "\nOF: " ^