| `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Term)
| `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type)
| `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term)
+ | `Tagged s ->
+ NCicMetaSubst.mk_meta ~attrs:[`Name s] metasenv context (foo `Term)
| `Vector ->
raise (RefineFailure (lazy (localise t, "A vector of implicit terms " ^
"can only be used in argument position")))
raise (RefineFailure (lazy (localise t,"unbound variable"))))
in
metasenv, subst, t, infty
- | C.Sort (C.Type [false,u]) -> metasenv,subst,t,(C.Sort (C.Type [true, u]))
- | C.Sort (C.Type _) ->
- raise (AssertFailure (lazy ("Cannot type an inferred type: "^
- NCicPp.ppterm ~subst ~metasenv ~context t)))
- | C.Sort _ -> metasenv,subst,t,(C.Sort (C.Type NCicEnvironment.type0))
+ | C.Sort s ->
+ (try metasenv, subst, t, C.Sort (NCicEnvironment.typeof_sort s)
+ with
+ | NCicEnvironment.UntypableSort msg ->
+ raise (RefineFailure (lazy (localise t, Lazy.force msg)))
+ | NCicEnvironment.AssertFailure msg -> raise (AssertFailure msg))
| C.Implicit infos ->
let metasenv,_,t,ty =
exp_implicit ~localise metasenv context expty t infos
| None -> metasenv, subst, None
| Some x ->
let m, s, x =
- NCicUnification.delift_term_wrt_terms
- rdb metasenv subst context x [t]
+ NCicUnification.delift_type_wrt_terms
+ rdb metasenv subst context1 (NCicSubstitution.lift 1 x)
+ [NCicSubstitution.lift 1 t]
in
m, s, Some x
in
let metasenv =
List.filter (function (j,_) -> j <> metanoouttype) metasenv in
let subst =
- (metanoouttype,(Some "outtype",context,outtype,metaoutsort))::subst in
+ (metanoouttype,([`Name "outtype"],context,outtype,metaoutsort))::subst in
let outtype = newouttype in
(* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
(NCicPp.ppterm ~metasenv ~subst ~context expty))) exc)
| (_,metasenv, newterm, newtype, meta)::tl ->
try
+ pp (lazy("K=" ^ NCicPp.ppterm ~metasenv ~subst ~context newterm));
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"));
+ NCicPp.ppterm ~metasenv ~subst ~context t ^ " === " ^
+ NCicPp.ppterm ~metasenv ~subst ~context meta ^ "\n"));
let metasenv, subst =
- NCicUnification.unify rdb metasenv subst context meta t
+ NCicUnification.unify rdb metasenv subst context t meta
in
pp (lazy ( "UNIFICATION in CTX:\n"^
NCicPp.ppcontext ~metasenv ~subst context
match NCicReduction.whd ~subst context ty_he with
| C.Prod (_,s,t) ->
let metasenv, subst, arg, _ =
- typeof rdb ~localise
- metasenv subst context arg (Some s) in
+ typeof rdb ~localise metasenv subst context arg (Some s) in
let t = NCicSubstitution.subst ~avoid_beta_redexes:true arg t in
aux metasenv subst (arg :: args_so_far) he t tl
| C.Meta _
| C.Appl (C.Meta _ :: _) as t ->
let metasenv, subst, arg, ty_arg =
- typeof rdb ~localise
- metasenv subst context arg None in
+ typeof rdb ~localise metasenv subst context arg None in
let name = guess_name subst context ty_arg in
let metasenv, _, meta, _ =
NCicMetaSubst.mk_meta metasenv
let flex_prod = C.Prod (name, ty_arg, meta) in
(* next line grants that ty_args is a type *)
let metasenv,subst, flex_prod, _ =
- typeof rdb ~localise metasenv subst
- context flex_prod None in
+ typeof rdb ~localise metasenv subst context flex_prod None in
(*
pp (lazy ( "UNIFICATION in CTX:\n"^
NCicPp.ppcontext ~metasenv ~subst context
"and those of its inductive type"))))
else
metasenv,subst,item1::context
- ) (metasenv,subst,[]) sx_context_ty_rev sx_context_te_rev
+ ) (metasenv,subst,tys) sx_context_ty_rev sx_context_te_rev
with Invalid_argument "List.fold_left2" -> assert false in
let con_sort= NCicTypeChecker.typeof ~subst ~metasenv context te in
(match
uri, height, metasenv, subst, C.Inductive (ind, leftno, itl, attr)
;;
-NCicUnification.set_refiner_typeof typeof;;
-
(* vim:set foldmethod=marker: *)