NCicPp.ppmetasenv ~subst metasenv));
match arity1 with
| C.Prod (name,so1,de1) (* , t ==?== C.Prod _ *) ->
- let metasenv, meta, _ =
+ let metasenv, _, meta, _ =
NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) `Type
in
let metasenv, subst =
aux metasenv subst ((name, C.Decl so1)::context)
(mkapp (NCicSubstitution.lift 1 ind) (C.Rel 1)) de1 meta
| C.Sort _ (* , t ==?== C.Prod _ *) ->
- let metasenv, meta, _ = NCicMetaSubst.mk_meta metasenv [] `Type in
+ let metasenv, _, meta, _ = NCicMetaSubst.mk_meta metasenv [] `Type in
let metasenv, subst =
try NCicUnification.unify hdb metasenv subst context
arity2 (C.Prod ("_", ind, meta))
NCicPp.ppterm ~subst ~metasenv ~context t)))
| C.Sort _ -> metasenv,subst,t,(C.Sort (C.Type NCicEnvironment.type0))
| C.Implicit infos ->
- let metasenv,t,ty = exp_implicit metasenv context expty infos in
+ let metasenv,_,t,ty = exp_implicit metasenv context expty infos in
metasenv, subst, t, ty
| C.Meta (n,l) as t ->
let ty =
let _,_,_,ty = NCicUtils.lookup_subst n subst in ty
with NCicUtils.Subst_not_found _ -> try
let _,_,ty = NCicUtils.lookup_meta n metasenv in
- match ty with C.Implicit _ -> assert false | _ -> ty
+ match ty with C.Implicit _ ->
+ prerr_endline (string_of_int n);
+ prerr_endline (NCicPp.ppmetasenv ~subst metasenv);
+ prerr_endline (NCicPp.ppsubst ~metasenv subst);
+ assert false | _ -> ty
with NCicUtils.Meta_not_found _ ->
raise (AssertFailure (lazy (Printf.sprintf
"%s not found" (NCicPp.ppterm ~subst ~metasenv ~context t))))
in
let metasenv, subst, outtype, outsort =
typeof_aux metasenv subst context None outtype in
+
+ (* next lines are to do a subst-expansion of the outtype, so
+ that when it becomes a beta-abstraction, the beta-redex is
+ fired during substitution *)
+ (*CSC: this is instantiate! should we move it from tactics to the
+ refiner? I think so! *)
+ let metasenv,metanoouttype,newouttype,metaoutsort =
+ NCicMetaSubst.mk_meta metasenv context `Term in
+ let metasenv,subst =
+ NCicUnification.unify hdb metasenv subst context outsort metaoutsort in
+ let metasenv =
+ List.filter (function (j,_) -> j <> metanoouttype) metasenv in
+ let subst =
+ (metanoouttype,(Some "outtype",context,outtype,metaoutsort))::subst in
+ let outtype = newouttype in
+
(* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
let ind =
if parameters = [] then C.Const r
let resty = C.Appl (outtype::arguments@[term]) in
let resty = NCicReduction.head_beta_reduce ~subst resty in
metasenv, subst, C.Match (r, outtype, term, List.rev pl_rev),resty
- | C.Match _ as orig -> assert false
+ | C.Match _ -> assert false
in
pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " :: "^
NCicPp.ppterm ~metasenv ~subst ~context infty ));
let metasenv, subst, arg, ty_arg =
typeof hdb ~look_for_coercion ~localise
metasenv subst context arg None in
- let metasenv, meta, _ =
+ let metasenv, _, meta, _ =
NCicMetaSubst.mk_meta metasenv
(("_",C.Decl ty_arg) :: context) `Type
in
uri, height, metasenv, subst,
C.Fixpoint (inductive, fl, attr)
- | C.Inductive (ind, leftno, itl, attr) -> assert false
+ | C.Inductive (_ind, _leftno, _itl, _attr) -> assert false
(*
(* let's check if the arity of the inductive types are well formed *)
List.iter (fun (_,_,x,_) -> ignore (typeof ~subst ~metasenv [] x)) tyl;