+let unopt exc = function None -> raise exc | Some x -> x ;;
+
+let fix metasenv subst is_sup test_eq_only exc t =
+ (*D*) inside 'f'; try let rc =
+ pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context:[] t));
+ let rec aux test_eq_only metasenv = function
+ | NCic.Prod (n,so,ta) ->
+ let metasenv,so = aux true metasenv so in
+ let metasenv,ta = aux test_eq_only metasenv ta in
+ metasenv,NCic.Prod (n,so,ta)
+ | NCic.Sort (NCic.Type [(`CProp|`Type),_]) as orig when test_eq_only ->
+ metasenv,orig
+ | NCic.Sort (NCic.Type _) when test_eq_only -> raise exc
+ | NCic.Sort (NCic.Type u) when is_sup ->
+ metasenv, NCic.Sort (NCic.Type (unopt exc (NCicEnvironment.sup u)))
+ | NCic.Sort (NCic.Type u) ->
+ metasenv, NCic.Sort (NCic.Type
+ (unopt exc (NCicEnvironment.inf ~strict:false u)))
+ | NCic.Meta (n,_) as orig ->
+ (try
+ let _,_,_,_ = NCicUtils.lookup_subst n subst in metasenv,orig
+ with NCicUtils.Subst_not_found _ ->
+ let metasenv, _ = NCicMetaSubst.extend_meta metasenv n in
+ metasenv, orig)
+ | t ->
+ NCicUntrusted.map_term_fold_a (fun _ x -> x) test_eq_only aux metasenv t
+ in
+ aux test_eq_only metasenv t
+ (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
+;;
+
+let metasenv_to_subst n (kind,context,ty) metasenv subst =
+ let infos,metasenv = List.partition (fun (n',_) -> n = n') metasenv in
+ let attrs,octx,oty = match infos with [_,infos] -> infos | _ -> assert false in
+ if octx=context && oty=ty then
+ (n,(NCicUntrusted.set_kind kind attrs, octx, oty))::metasenv,subst
+ else
+ let metasenv, _, bo, _ =
+ NCicMetaSubst.mk_meta metasenv context ~attrs ~with_type:ty kind in
+ let subst = (n,(NCicUntrusted.set_kind kind attrs,octx,bo,oty))::subst in
+ metasenv,subst
+;;
+
+let rec sortfy exc metasenv subst context t =
+ let t = NCicReduction.whd ~subst context t in
+ let metasenv,subst =
+ match t with
+ | NCic.Sort _ -> metasenv, subst
+ | NCic.Meta (n,_) ->
+ let attrs, context, ty = NCicUtils.lookup_meta n metasenv in
+ let kind = NCicUntrusted.kind_of_meta attrs in
+ if kind = `IsSort then
+ metasenv,subst
+ else
+ (match ty with
+ | NCic.Implicit (`Typeof _) ->
+ metasenv_to_subst n (`IsSort,[],ty) metasenv subst
+ | ty ->
+ let metasenv,subst,ty = sortfy exc metasenv subst context ty in
+ metasenv_to_subst n (`IsSort,[],ty) metasenv subst)
+ | NCic.Implicit _ -> assert false
+ | _ -> raise exc
+ in
+ metasenv,subst,t
+
+let tipify exc metasenv subst context t ty =
+ let is_type attrs =
+ match NCicUntrusted.kind_of_meta attrs with
+ `IsType | `IsSort -> true
+ | `IsTerm -> false
+ in
+ let rec optimize_meta metasenv subst =
+ function
+ NCic.Meta (n,lc) ->
+ (try
+ let attrs,_,_ = NCicUtils.lookup_meta n metasenv in
+ if is_type attrs then
+ metasenv,subst,true
+ else
+ let _,cc,ty = NCicUtils.lookup_meta n metasenv in
+ let metasenv,subst,ty = sortfy exc metasenv subst cc ty in
+ let metasenv =
+ NCicUntrusted.replace_in_metasenv n
+ (fun attrs,cc,_ -> NCicUntrusted.set_kind `IsType attrs, cc, ty)
+ metasenv