+ in
+
+ try
+ pp (lazy "WWW: trying coercions -- inner check");
+ match infty, expty, t with
+ | _,_, NCic.Match (Ref.Ref (_,Ref.Ind (_,tyno,leftno)) as r,outty,m,pl) ->
+ (*{{{*) pp (lazy "CASE");
+ (* {{{ helper functions *)
+ let get_cl_and_left_p refit outty =
+ match refit with
+ | NReference.Ref (uri, NReference.Ind (_,tyno,leftno)) ->
+ let _, leftno, itl, _, _ = NCicEnvironment.get_checked_indtys r in
+ let _, _, ty, cl = List.nth itl tyno in
+ let constructorsno = List.length cl in
+ let count_pis t =
+ let rec aux ctx t =
+ match NCicReduction.whd ~subst ~delta:max_int ctx t with
+ | NCic.Prod (name,src,tgt) ->
+ let ctx = (name, (NCic.Decl src)) :: ctx in
+ 1 + aux ctx tgt
+ | _ -> 0
+ in
+ aux [] t
+ in
+ let rec skip_lambda_delifting t n =
+ match t,n with
+ | _,0 -> t
+ | NCic.Lambda (_,_,t),n ->
+ pp (lazy ("WWW: failing term? "^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:[] t));
+ skip_lambda_delifting
+ (* substitute dangling indices with a dummy *)
+ (NCicSubstitution.subst (NCic.Sort NCic.Prop) t) (n - 1)
+ | _ -> assert false
+ in
+ let get_l_r_p n = function
+ | NCic.Lambda (_,NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_))),_) -> [],[]
+ | NCic.Lambda (_,NCic.Appl
+ (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_))) :: args),_) ->
+ HExtlib.split_nth n args
+ | _ -> assert false
+ in
+ let pis = count_pis ty in
+ let rno = pis - leftno in
+ let t = skip_lambda_delifting outty rno in
+ let left_p, _ = get_l_r_p leftno t in
+ let instantiate_with_left cl =
+ List.map
+ (fun ty ->
+ List.fold_left
+ (fun t p -> match t with
+ | NCic.Prod (_,_,t) ->
+ cs_subst p t
+ | _-> assert false)
+ ty left_p)
+ cl
+ in
+ let cl = instantiate_with_left (List.map (fun (_,_,x) -> x) cl) in
+ cl, left_p, leftno, rno
+ | _ -> raise exn
+ in
+ let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
+ match t,n with
+ | _,0 ->
+ let rec mkr n = function
+ | [] -> [] | _::tl -> NCic.Rel n :: mkr (n+1) tl
+ in
+ pp (lazy ("input replace: " ^ NCicPp.ppterm ~context:ctx ~metasenv:[] ~subst:[] bo));
+ let bo =
+ NCicRefineUtil.replace_lifting
+ ~equality:(fun _ -> NCicRefineUtil.alpha_equivalence)
+ ~context:ctx
+ ~what:(matched::right_p)
+ ~with_what:(NCic.Rel 1::List.rev (mkr 2 right_p))
+ ~where:bo
+ in
+ pp (lazy ("output replace: " ^ NCicPp.ppterm ~context:ctx ~metasenv:[] ~subst:[] bo));
+ bo
+ | NCic.Lambda (name, src, tgt),_ ->
+ NCic.Lambda (name, src,
+ keep_lambdas_and_put_expty
+ ((name, NCic.Decl src)::ctx) tgt (NCicSubstitution.lift 1 bo)
+ (List.map (NCicSubstitution.lift 1) right_p) (NCicSubstitution.lift 1 matched) (n-1))
+ | _ -> assert false
+ in
+ (*let eq = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.ind(1,0,2)")) in
+ let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.con(0,1,2)")) in*)
+ let eq = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/jmeq/jmeq.ind(1,0,2)")) in
+ let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/jmeq/jmeq.con(0,1,2)")) in
+ let add_params
+ metasenv subst context cty outty mty m i
+ =
+ let rec aux context outty par j mty m = function
+ | NCic.Prod (name, src, tgt) ->
+ let t,k =
+ aux
+ ((name, NCic.Decl src) :: context)
+ (NCicSubstitution.lift 1 outty) (NCic.Rel j::par) (j+1)
+ (NCicSubstitution.lift 1 mty) (NCicSubstitution.lift 1 m) tgt
+ in
+ NCic.Prod (name, src, t), k
+ | NCic.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r) ->
+ let k =
+ let k = NCic.Const(Ref.mk_constructor i r) in
+ NCicUntrusted.mk_appl k par
+ in
+ (* the type has no parameters, so kty = mty
+ let kty =
+ try NCicTypechecker.typeof ~subst ~metasenv context k
+ with NCicTypeChecker.TypeCheckerFailure _ -> assert false
+ in *)
+ NCic.Prod ("p",
+ NCic.Appl [eq; mty; m; mty; k],
+ (NCicSubstitution.lift 1
+ (NCicReduction.head_beta_reduce ~delta:max_int
+ (NCicUntrusted.mk_appl outty [k])))),[mty,m,mty,k]
+ | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r)::pl) ->
+ let left_p,right_p = HExtlib.split_nth leftno pl in
+ let has_rights = right_p <> [] in
+ let k =
+ let k = NCic.Const(Ref.mk_constructor i r) in
+ NCicUntrusted.mk_appl k (left_p@par)
+ in
+ let right_p =
+ try match
+ NCicTypeChecker.typeof ~subst ~metasenv context k
+ with
+ | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_)))::args) ->
+ snd (HExtlib.split_nth leftno args)
+ | _ -> assert false
+ with NCicTypeChecker.TypeCheckerFailure _-> assert false
+ in
+ let orig_right_p =
+ match mty with
+ | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_)))::args) ->
+ snd (HExtlib.split_nth leftno args)
+ | _ -> assert false
+ in
+ List.fold_right2
+ (fun x y (tacc,pacc) ->
+ let xty =
+ try NCicTypeChecker.typeof ~subst ~metasenv context x
+ with NCicTypeChecker.TypeCheckerFailure _ -> assert false
+ in
+ let yty =
+ try NCicTypeChecker.typeof ~subst ~metasenv context y
+ with NCicTypeChecker.TypeCheckerFailure _ -> assert false
+ in
+ NCic.Prod ("_", NCic.Appl [eq;xty;x;yty;y],
+ NCicSubstitution.lift 1 tacc), (xty,x,yty,y)::pacc)
+ (orig_right_p @ [m]) (right_p @ [k])
+ (NCicReduction.head_beta_reduce ~delta:max_int
+ (NCicUntrusted.mk_appl outty (right_p@[k])), [])
+
+ (* if has_rights then
+ NCicReduction.head_beta_reduce ~delta:max_int
+ (NCic.Appl (outty ::right_p @ [k])),k
+ else
+ NCic.Prod ("p",
+ NCic.Appl [eq; mty; m; k],
+ (NCicSubstitution.lift 1
+ (NCicReduction.head_beta_reduce ~delta:max_int
+ (NCic.Appl (outty ::right_p @ [k]))))),k*)
+ | _ -> assert false
+ in
+ aux context outty [] 1 mty m cty
+ in
+ let add_lambda_for_refl_m pbo eqs cty =
+ (* k lives in the right context *)
+ (* if rno <> 0 then pbo else *)
+ let rec aux = function
+ | NCic.Lambda (name,src,bo), NCic.Prod (_,_,ty) ->
+ NCic.Lambda (name,src,
+ (aux (bo,ty)))
+ | t,_ -> snd (List.fold_right
+ (fun (xty,x,yty,y) (n,acc) -> n+1, NCic.Lambda ("p" ^ string_of_int n,
+ NCic.Appl [eq; xty; x; yty; y],
+ NCicSubstitution.lift 1 acc)) eqs (1,t))
+ (*NCic.Lambda ("p",
+ NCic.Appl [eq; mty; m; k],NCicSubstitution.lift 1 t)*)
+ in
+ aux (pbo,cty)
+ in
+ let add_pi_for_refl_m context new_outty mty m lno rno =
+ (*if rno <> 0 then new_outty else*)
+ let rec aux context mty m = function
+ | NCic.Lambda (name, src, tgt) ->
+ let context = (name, NCic.Decl src)::context in
+ NCic.Lambda (name, src, aux context (NCicSubstitution.lift 1 mty) (NCicSubstitution.lift 1 m) tgt)
+ | t ->
+ let lhs =
+ match mty with
+ | NCic.Appl (_::params) -> (snd (HExtlib.split_nth lno params))@[m]
+ | _ -> [m]
+ in
+ let rhs =
+ List.map (fun x -> NCic.Rel x)
+ (List.rev (HExtlib.list_seq 1 (rno+2))) in
+ List.fold_right2
+ (fun x y acc ->
+ let xty =
+ try NCicTypeChecker.typeof ~subst ~metasenv context x
+ with NCicTypeChecker.TypeCheckerFailure _ -> assert false
+ in
+ let yty =
+ try NCicTypeChecker.typeof ~subst ~metasenv context y
+ with NCicTypeChecker.TypeCheckerFailure _ -> assert false
+ in
+ NCic.Prod
+ ("_", NCic.Appl [eq;xty;x;yty;y],
+ (NCicSubstitution.lift 1 acc)))
+ lhs rhs t
+ (* NCic.Prod
+ ("_", NCic.Appl [eq;mty;m;NCic.Rel 1],
+ NCicSubstitution.lift 1 t)*)
+ in
+ aux context mty m new_outty
+ in (* }}} end helper functions *)
+ (* constructors types with left params already instantiated *)
+ let outty = NCicUntrusted.apply_subst subst context outty in
+ let cl, left_p, leftno,rno =
+ get_cl_and_left_p r outty
+ in
+ let right_p, mty =
+ try
+ match
+ NCicTypeChecker.typeof ~subst ~metasenv context m
+ with
+ | (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_))) | NCic.Meta _) as mty -> [], mty
+ | NCic.Appl ((NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_)))|NCic.Meta _)::args) as mty ->
+ snd (HExtlib.split_nth leftno args), mty
+ | _ -> assert false
+ with NCicTypeChecker.TypeCheckerFailure _ ->
+ raise (AssertFailure(lazy "already ill-typed matched term"))
+ in
+ let mty = NCicUntrusted.apply_subst subst context mty in
+ let outty = NCicUntrusted.apply_subst subst context outty in
+ let expty = NCicUntrusted.apply_subst subst context expty in
+ let new_outty =
+ keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
+ in
+ pp
+ (lazy ("CASE: new_outty: " ^ NCicPp.ppterm
+ ~context ~metasenv ~subst new_outty));
+ let _,pl,subst,metasenv =
+ List.fold_right2
+ (fun cty pbo (i, acc, s, menv) ->
+ pp (lazy ("begin iteration"));
+ (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
+ * (new_)outty right_par (K_i left_par k_par) *)
+ let infty_pbo, _ =
+ add_params menv s context cty outty mty m i in
+ pp
+ (lazy ("CASE: infty_pbo: "^ NCicPp.ppterm
+ ~context ~metasenv ~subst infty_pbo));
+ let expty_pbo, eqs = (* k is (K_i left_par k_par) *)
+ add_params menv s context cty new_outty mty m i in
+ pp
+ (lazy ("CASE: expty_pbo: "^ NCicPp.ppterm
+ ~context ~metasenv ~subst expty_pbo));
+ let pbo = add_lambda_for_refl_m pbo eqs cty in
+ pp
+ (lazy ("CASE: pbo: " ^ NCicPp.ppterm
+ ~context ~metasenv ~subst pbo));
+ let metasenv, subst, pbo, _ =
+ try_coercions rdb ~localise menv s context pbo
+ orig_t (*??*) infty_pbo expty_pbo perform_unification exc
+ in
+ pp
+ (lazy ("CASE: pbo2: " ^ NCicPp.ppterm
+ ~context ~metasenv ~subst pbo));
+ (i-1, pbo::acc, subst, metasenv))
+ cl pl (List.length pl, [], subst, metasenv)
+ in
+ (*let metasenv, subst =
+ try
+ NCicUnification.unify rdb metasenv subst context outty new_outty
+ with _ -> raise (RefineFailure (lazy (localise orig_t, "try_coercions")))
+ in*)
+ let new_outty = add_pi_for_refl_m context new_outty mty m leftno rno in
+ pp (lazy ("CASE: new_outty: " ^ (NCicPp.ppterm
+ ~metasenv ~subst ~context new_outty)));
+ let right_tys =
+ List.map
+ (fun t -> NCicTypeChecker.typeof ~subst ~metasenv context t) right_p in
+ let eqs =
+ List.map2 (fun x y -> NCic.Appl[eq_refl;x;y]) (right_tys@[mty])
+ (right_p@[m]) in
+ let t = NCic.Appl (NCic.Match(r,new_outty,m,pl) :: eqs)
+ in
+ metasenv, subst, t, expty (*}}}*)
+ | NCic.Prod (nameprod, src, ty),NCic.Prod (_, src2, ty2), _ ->
+ let rec mk_fresh_name ctx firstch n =
+ let candidate = (String.make 1 firstch) ^ (string_of_int n) in
+ if (List.for_all (fun (s,_) -> s <> candidate) ctx) then candidate
+ else mk_fresh_name ctx firstch (n+1)
+ in
+ (*{{{*) pp (lazy "LAM");
+ pp (lazy ("LAM: t = " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
+ let name_con = mk_fresh_name context 'c' 0
+ (*FreshNamesGenerator.mk_fresh_name
+ ~subst metasenv context ~typ:src2 Cic.Anonymous*)
+ in
+ let context_src2 = ((name_con, NCic.Decl src2) :: context) in
+ (* contravariant part: the argument of f:src->ty *)
+ let metasenv, subst, rel1, _ =
+ try_coercions rdb ~localise metasenv subst context_src2
+ (NCic.Rel 1) orig_t (NCicSubstitution.lift 1 src2)
+ (NCicSubstitution.lift 1 src) perform_unification exc
+ in
+ (* covariant part: the result of f(c x); x:src2; (c x):src *)
+ let name_t, bo =
+ match t with
+ | NCic.Lambda (n,_,bo) -> n, cs_subst rel1 (NCicSubstitution.lift_from 2 1 bo)
+ | _ -> name_con, NCicUntrusted.mk_appl (NCicSubstitution.lift 1 t) [rel1]
+ in
+ (* we fix the possible dependency problem in the source ty *)
+ let ty = cs_subst rel1 (NCicSubstitution.lift_from 2 1 ty) in
+ let metasenv, subst, bo, _ =
+ try_coercions rdb ~localise metasenv subst context_src2
+ bo orig_t ty ty2 perform_unification exc
+ in
+ let coerced = NCic.Lambda (name_t,src2, bo) in
+ pp (lazy ("LAM: coerced = " ^ NCicPp.ppterm ~metasenv ~subst ~context coerced));
+ metasenv, subst, coerced, expty (*}}}*)
+ | _ -> raise exc
+ with exc2 ->
+ pp(lazy("try_coercion " ^
+ NCicPp.ppterm ~metasenv ~subst ~context infty ^ " |---> " ^
+ NCicPp.ppterm ~metasenv ~subst ~context expty));