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 _ = ();;
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))
| _ ->
pp (lazy (
(NCicPp.ppterm ~metasenv ~subst ~context infty) ^ " === " ^
- (NCicPp.ppterm ~metasenv ~subst ~context expty)));
+ (NCicPp.ppterm ~metasenv ~subst:[] ~context expty)));
try
let metasenv, subst =
NCicUnification.unify hdb metasenv subst context infty expty
fun t as orig ->
(*D*)inside 'R'; try let rc =
pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t));
- pp (lazy (NCicPp.ppmetasenv ~subst metasenv));
+ pp (lazy (if expty = None then "NONE" else "SOME"));
+ if (List.exists (fun (i,_) -> i=29) subst) then
+ pp (lazy (NCicPp.ppsubst ~metasenv subst));
let metasenv, subst, t, infty =
match t with
| C.Rel n ->
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))))
let bo_ty = NCicSubstitution.subst ~avoid_beta_redexes:true t bo_ty in
metasenv, subst, C.LetIn (n, ty, t, bo), bo_ty
| C.Appl ((he as orig_he)::(_::_ as args)) ->
+ let upto =
+ match orig_he with C.Meta _ -> List.length args | _ -> 0
+ in
let metasenv, subst, he, ty_he =
typeof_aux metasenv subst context None he in
- eat_prods hdb ~localise ~look_for_coercion
- metasenv subst context orig_he he ty_he args
+ let metasenv, subst, t, ty =
+ eat_prods hdb ~localise ~look_for_coercion
+ metasenv subst context orig_he he ty_he args
+ in
+ let t = if upto > 0 then NCicReduction.head_beta_reduce ~upto t else t in
+ metasenv, subst, t, ty
| C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
| C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as r,
outtype,(term as orig_term),pl) as orig ->
let ind = if args = [] then C.Const r else C.Appl (C.Const r::args) in
let metasenv, subst, term, _ =
typeof_aux metasenv subst context (Some ind) term in
+ let parameters, arguments = HExtlib.split_nth leftno args in
+ let outtype =
+ match outtype with
+ | C.Implicit _ as ot ->
+ let rec aux = function
+ | [] -> NCic.Lambda ("_",NCic.Implicit `Type,ot)
+ | _::tl -> NCic.Lambda ("_",NCic.Implicit `Type,aux tl)
+ in
+ aux arguments
+ | _ -> outtype
+ in
let metasenv, subst, outtype, outsort =
typeof_aux metasenv subst context None outtype in
- let parameters, arguments = HExtlib.split_nth leftno args 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
if List.length pl <> constructorsno then
raise (RefineFailure (lazy (localise orig,
"Wrong number of cases in a match")));
+(*
+ let metasenv, subst =
+ match expty with
+ | None -> metasenv, subst
+ | Some expty ->
+ NCicUnification.unify hdb metasenv subst context resty expty
+ in
+*)
let _, metasenv, subst, pl_rev =
List.fold_left
(fun (j, metasenv, subst, branches) p ->
j+1, metasenv, subst, p :: branches)
(1, metasenv, subst, []) pl
in
- metasenv, subst,
- C.Match (r, outtype, term, List.rev pl_rev),
- NCicReduction.head_beta_reduce (C.Appl (outtype::arguments@[term]))
- | C.Match _ as orig ->
- prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context orig);
- assert false
+ 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 _ -> 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;
projects / helm.git / blobdiff