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 pp _ = ();;
-let fix_sorts metasenv subst context meta t =
+let fix_sorts swap metasenv subst context meta t =
let rec aux () = function
| NCic.Sort (NCic.Type u) as orig ->
- (match NCicEnvironment.sup u with
- | None -> raise (fail_exc metasenv subst context meta t)
- | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1))
+ if swap then
+ match NCicEnvironment.sup u with
+ | None -> raise (fail_exc metasenv subst context meta t)
+ | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1)
+ else
+ NCic.Sort (NCic.Type (
+ match NCicEnvironment.sup NCicEnvironment.type0 with
+ | Some x -> x
+ | _ -> assert false))
| NCic.Meta _ as orig -> orig
| t -> NCicUtils.map (fun _ _ -> ()) () aux t
in
if swap then unify test_eq_only m s c t2 t1
else unify test_eq_only m s c t1 t2
in
- let fix_sorts t =
- if swap then fix_sorts metasenv subst context (NCic.Meta (n,lc)) t
- else
- NCic.Sort (NCic.Type (
- match NCicEnvironment.sup NCicEnvironment.type0 with Some x ->x| _ ->
- assert false))
- in
let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
let metasenv, subst, t =
match ty with
- | NCic.Implicit (`Typeof _) -> metasenv, subst, fix_sorts t
+ | NCic.Implicit (`Typeof _) ->
+ metasenv,subst,fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t
| _ ->
pp (lazy ("typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
let t, ty_t =
try t, NCicTypeChecker.typeof ~subst ~metasenv context t
with NCicTypeChecker.TypeCheckerFailure _ ->
- let ft = fix_sorts t in
- if ft == t then assert false else
+ let ft =
+ fix_sorts swap metasenv subst context (NCic.Meta (n,lc)) t
+ in
+ if ft == t then assert false
+ else
try
pp (lazy ("typeof: " ^
NCicPp.ppterm ~metasenv ~subst ~context ft));
ft, NCicTypeChecker.typeof ~subst ~metasenv context ft
- with NCicTypeChecker.TypeCheckerFailure msg ->
- prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context ft);
- prerr_endline (Lazy.force msg);
+ with NCicTypeChecker.TypeCheckerFailure _ ->
assert false
in
let lty = NCicSubstitution.subst_meta lc ty in
pp (lazy("On the types: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context:ctx ty ^ " ~~~ " ^
NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
^ NCicPp.ppterm ~metasenv ~subst ~context ty_t));
let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in