--- /dev/null
+(* 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
+;;
+
+
~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)
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));
projects / helm.git / commitdiff