;;
let unify a b c d = wrap "unify" (unify a b c) d;;
-let fix_sorts (ctx,t) =
+let fix_sorts status (ctx,t) =
let f () =
- let t = NCicUnification.fix_sorts t in
- ctx,t
+ let name,height,metasenv,subst,obj = status#obj in
+ let metasenv, t =
+ NCicUnification.fix_sorts metasenv subst t in
+ let status = status#set_obj (name,height,metasenv,subst,obj) in
+ status, (ctx,t)
in
wrap "fix_sorts" f ()
;;
to_subst status i (gname,context,t,gty)
;;
-let mk_meta status ?(attrs=[]) ctx bo_or_ty =
+let mk_meta status ?(attrs=[]) ctx bo_or_ty kind =
match bo_or_ty with
| `Decl ty ->
let status, (_,ty) = relocate status ctx ty in
let n,h,metasenv,subst,o = status#obj in
let metasenv, _, instance, _ =
- NCicMetaSubst.mk_meta ~attrs metasenv ctx (`WithType ty)
+ NCicMetaSubst.mk_meta ~attrs metasenv ctx ~with_type:ty kind
in
let status = status#set_obj (n,h,metasenv,subst,o) in
status, (ctx,instance)
let status, (_,ty) = typeof status ctx bo in
let n,h,metasenv,subst,o = status#obj in
let metasenv, metano, instance, _ =
- NCicMetaSubst.mk_meta ~attrs metasenv ctx (`WithType ty) in
+ NCicMetaSubst.mk_meta ~attrs metasenv ctx ~with_type:ty kind in
let metasenv = List.filter (fun j,_ -> j <> metano) metasenv in
let subst = (metano, (attrs, ctx, bo_, ty)) :: subst in
let status = status#set_obj (n,h,metasenv,subst,o) in
;;
let mk_in_scope status t =
- mk_meta status ~attrs:[`InScope] (ctx_of t) (`Def t)
+ mk_meta status ~attrs:[`InScope] (ctx_of t) (`Def t) `IsTerm
;;
let mk_out_scope n status t =
- mk_meta status ~attrs:[`OutScope n] (ctx_of t) (`Def t)
+ mk_meta status ~attrs:[`OutScope n] (ctx_of t) (`Def t) `IsTerm
;;
(* the following unification problem will be driven by