From e62111335574a6ec78e5a4367a540e0529a00404 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Wed, 12 May 2010 18:39:05 +0000 Subject: [PATCH] Experimental support for Russell (coercions moving inside lambda & pattern matching etc.) added to the refiner. --- .../components/ng_kernel/nCicSubstitution.mli | 2 + helm/software/components/ng_refiner/.depend | 3 + helm/software/components/ng_refiner/Makefile | 1 + .../components/ng_refiner/nCicMetaSubst.mli | 2 + .../components/ng_refiner/nCicRefineUtil.ml | 141 ++++++++ .../components/ng_refiner/nCicRefineUtil.mli | 22 ++ .../components/ng_refiner/nCicRefiner.ml | 338 +++++++++++++++++- 7 files changed, 507 insertions(+), 2 deletions(-) create mode 100644 helm/software/components/ng_refiner/nCicRefineUtil.ml create mode 100644 helm/software/components/ng_refiner/nCicRefineUtil.mli diff --git a/helm/software/components/ng_kernel/nCicSubstitution.mli b/helm/software/components/ng_kernel/nCicSubstitution.mli index ad8074dc7..7e27a5d4c 100644 --- a/helm/software/components/ng_kernel/nCicSubstitution.mli +++ b/helm/software/components/ng_kernel/nCicSubstitution.mli @@ -17,6 +17,8 @@ val set_ppterm : (context:NCic.context -> ?inside_fix:bool -> NCic.term -> string) -> unit +val lift_from : ?no_implicit:bool -> int -> int -> NCic.term -> NCic.term + (* lift n t *) (* lifts [t] of [n] *) (* [from] default 1, lifts only indexes >= [from] *) diff --git a/helm/software/components/ng_refiner/.depend b/helm/software/components/ng_refiner/.depend index db7e52884..d3a179400 100644 --- a/helm/software/components/ng_refiner/.depend +++ b/helm/software/components/ng_refiner/.depend @@ -3,6 +3,7 @@ nCicMetaSubst.cmi: nCicUnifHint.cmi: nCicCoercion.cmi: nCicUnifHint.cmi nRstatus.cmi: nCicCoercion.cmi +nCicRefineUtil.cmi: nCicUnification.cmi: nRstatus.cmi nCicRefiner.cmi: nRstatus.cmi nDiscriminationTree.cmo: nDiscriminationTree.cmi @@ -17,6 +18,8 @@ nCicCoercion.cmx: nDiscriminationTree.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \ nCicCoercion.cmi nRstatus.cmo: nCicCoercion.cmi nRstatus.cmi nRstatus.cmx: nCicCoercion.cmx nRstatus.cmi +nCicRefineUtil.cmo: nCicMetaSubst.cmi nCicRefineUtil.cmi +nCicRefineUtil.cmx: nCicMetaSubst.cmx nCicRefineUtil.cmi nCicUnification.cmo: nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi nCicUnification.cmx: nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi nCicRefiner.cmo: nCicUnification.cmi nCicMetaSubst.cmi nCicCoercion.cmi \ diff --git a/helm/software/components/ng_refiner/Makefile b/helm/software/components/ng_refiner/Makefile index 7ff8f5fd0..bf1fe3be5 100644 --- a/helm/software/components/ng_refiner/Makefile +++ b/helm/software/components/ng_refiner/Makefile @@ -7,6 +7,7 @@ INTERFACE_FILES = \ nCicUnifHint.mli \ nCicCoercion.mli \ nRstatus.mli \ + nCicRefineUtil.mli \ nCicUnification.mli \ nCicRefiner.mli diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli index fd101414d..a195a2fd8 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.mli +++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli @@ -67,5 +67,7 @@ val saturate: NCic.context -> NCic.term -> int -> NCic.term * NCic.metasenv * NCic.term list +val pack_lc : int * NCic.lc_kind -> int * NCic.lc_kind + val is_out_scope_tag : NCic.meta_attrs -> bool val int_of_out_scope_tag : NCic.meta_attrs -> int diff --git a/helm/software/components/ng_refiner/nCicRefineUtil.ml b/helm/software/components/ng_refiner/nCicRefineUtil.ml new file mode 100644 index 000000000..745f57176 --- /dev/null +++ b/helm/software/components/ng_refiner/nCicRefineUtil.ml @@ -0,0 +1,141 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(* $Id: cicUtil.ml 10153 2009-07-28 15:17:51Z sacerdot $ *) + +exception Meta_not_found of int +exception Subst_not_found of int + +(* syntactic_equality up to the *) +(* distinction between fake dependent products *) +(* and non-dependent products, alfa-conversion *) +let alpha_equivalence = + let rec aux t t' = + if t = t' then true + else + match t,t' with + | NCic.Prod (_,s,t), NCic.Prod (_,s',t') -> + aux s s' && aux t t' + | NCic.Lambda (_,s,t), NCic.Lambda (_,s',t') -> + aux s s' && aux t t' + | NCic.LetIn (_,s,ty,t), NCic.LetIn(_,s',ty',t') -> + aux s s' && aux ty ty' && aux t t' + | NCic.Appl l, NCic.Appl l' when List.length l = List.length l' -> + (try + List.fold_left2 + (fun b t1 t2 -> b && aux t1 t2) true l l' + with + Invalid_argument _ -> false) + | NCic.Const ref1, NCic.Const ref2 -> t == t' + | NCic.Match (it,outt,t,pl), NCic.Match (it',outt',t',pl') -> + it == it' && + aux outt outt' && aux t t' && + (try + List.fold_left2 + (fun b t1 t2 -> b && aux t1 t2) true pl pl' + with + Invalid_argument _ -> false) + | NCic.Meta (n1,(s1, NCic.Irl _)), NCic.Meta (n2,(s2, NCic.Irl _)) + when n1 = n2 && s1 = s2 -> true + | NCic.Meta (i, (s,lc)), NCic.Meta (i', (s',lc')) -> + let lc = NCicUtils.expand_local_context lc in + let lc' = NCicUtils.expand_local_context lc' in + i = i' && + (try + List.fold_left2 + (fun b xt xt' -> b && aux (NCicSubstitution.lift s xt) (NCicSubstitution.lift s' xt')) + true lc lc' + with + Invalid_argument _ -> false) + | NCic.Appl [t], t' | t, NCic.Appl [t'] -> assert false + | NCic.Sort s, NCic.Sort s' -> s == s' + | _,_ -> false (* we already know that t != t' *) + in + aux +;; + +exception WhatAndWithWhatDoNotHaveTheSameLength;; + +let replace_lifting ~equality ~context ~what ~with_what ~where = + let find_image ctx what t = + let rec find_image_aux = + function + [],[] -> raise Not_found + | what::tl1,with_what::tl2 -> + if equality ctx what t then with_what else find_image_aux (tl1,tl2) + | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength + in + find_image_aux (what,with_what) + in + let add_ctx ctx n s = (n, NCic.Decl s)::ctx in + let add_ctx1 ctx n s ty = (n, NCic.Def (s,ty))::ctx in + let rec substaux k ctx what t = + try + NCicSubstitution.lift (k-1) (find_image ctx what t) + with Not_found -> + match t with + NCic.Rel _ as t -> t + | NCic.Meta (i, (shift,l)) -> + let l = NCicUtils.expand_local_context l in + let l' = + List.map (fun t -> substaux k ctx what (NCicSubstitution.lift shift t)) l + in + NCic.Meta(i,NCicMetaSubst.pack_lc (0, NCic.Ctx l')) + | NCic.Sort _ as t -> t + | NCic.Implicit _ as t -> t + | NCic.Prod (n,s,t) -> + NCic.Prod + (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (NCicSubstitution.lift 1) what) t) + | NCic.Lambda (n,s,t) -> + NCic.Lambda + (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (NCicSubstitution.lift 1) what) t) + | NCic.LetIn (n,s,ty,t) -> + NCic.LetIn + (n, substaux k ctx what s, substaux k ctx what ty, substaux (k + 1) (add_ctx1 ctx n s ty) (List.map (NCicSubstitution.lift 1) what) t) + | NCic.Appl (he::tl) -> + (* Invariant: no Appl applied to another Appl *) + let tl' = List.map (substaux k ctx what) tl in + begin + match substaux k ctx what he with + NCic.Appl l -> NCic.Appl (l@tl') + | _ as he' -> NCic.Appl (he'::tl') + end + | NCic.Appl _ -> assert false + | NCic.Const _ as t -> t + | NCic.Match (it,outt,t,pl) -> + NCic.Match (it,substaux k ctx what outt, substaux k ctx what t, + List.map (substaux k ctx what) pl) + in + prerr_endline "*** replace lifting -- what:"; + List.iter (fun x -> prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context x)) what; + prerr_endline "\n*** replace lifting -- with what:"; + List.iter (fun x -> prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context x)) with_what; + prerr_endline "\n*** replace lifting -- where:"; + prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context where); + + substaux 1 context what where +;; + + diff --git a/helm/software/components/ng_refiner/nCicRefineUtil.mli b/helm/software/components/ng_refiner/nCicRefineUtil.mli new file mode 100644 index 000000000..345b6bde2 --- /dev/null +++ b/helm/software/components/ng_refiner/nCicRefineUtil.mli @@ -0,0 +1,22 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *) + +val alpha_equivalence : NCic.term -> NCic.term -> bool + +val replace_lifting : + equality:((string * NCic.context_entry) list -> + NCic.term -> NCic.term -> bool) -> + context:(string * NCic.context_entry) list -> + what:NCic.term list -> + with_what:NCic.term list -> where:NCic.term -> NCic.term + diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 423c33d8e..8476119ad 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -421,9 +421,18 @@ and try_coercions rdb ~localise metasenv subst context t orig_t infty expty perform_unification exc = + let cs_subst = NCicSubstitution.subst ~avoid_beta_redexes:true in + try + pp (lazy "WWW: trying coercions -- preliminary unification"); + let metasenv, subst = + NCicUnification.unify rdb metasenv subst context infty expty + in metasenv, subst, t, expty + with + | exn -> (* we try with a coercion *) let rec first exc = function - | [] -> + | [] -> + pp (lazy "WWW: no more coercions!"); raise (wrap_exc (lazy (localise orig_t, Printf.sprintf "The term\n%s\nhas type\n%s\nbut is here used with type\n%s" (NCicPp.ppterm ~metasenv ~subst ~context t) @@ -458,7 +467,332 @@ and try_coercions rdb with | NCicUnification.UnificationFailure _ -> first exc tl | NCicUnification.Uncertain _ as exc -> first exc tl - in + 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)); -- 2.39.2