matita/components/ng_refiner/nCicRefineUtil.ml

   1 (* Copyright (C) 2004, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 (* $Id: cicUtil.ml 10153 2009-07-28 15:17:51Z sacerdot $ *)
  27
  28 exception Meta_not_found of int
  29 exception Subst_not_found of int
  30
  31 (* syntactic_equality up to the                 *)
  32 (* distinction between fake dependent products  *)
  33 (* and non-dependent products, alfa-conversion  *)
  34 let alpha_equivalence status =
  35   let rec aux t t' =
  36    if t = t' then true
  37    else
  38     match t,t' with
  39      | NCic.Prod (_,s,t), NCic.Prod (_,s',t') ->
  40         aux s s' && aux t t'
  41      | NCic.Lambda (_,s,t), NCic.Lambda (_,s',t') ->
  42         aux s s' && aux t t'
  43      | NCic.LetIn (_,s,ty,t), NCic.LetIn(_,s',ty',t') ->
  44         aux s s' && aux ty ty' && aux t t'
  45      | NCic.Appl l, NCic.Appl l' when List.length l = List.length l' ->
  46         (try
  47           List.fold_left2
  48            (fun b t1 t2 -> b && aux t1 t2) true l l'
  49          with
  50           Invalid_argument _ -> false)
  51      | NCic.Const _, NCic.Const _ -> t == t'
  52      | NCic.Match (it,outt,t,pl), NCic.Match (it',outt',t',pl') ->
  53         it == it' &&
  54          aux outt outt' && aux t t' &&
  55           (try
  56             List.fold_left2
  57              (fun b t1 t2 -> b && aux t1 t2) true pl pl'
  58            with
  59             Invalid_argument _ -> false)
  60      | NCic.Meta (n1,(s1, NCic.Irl _)), NCic.Meta (n2,(s2, NCic.Irl _))
  61         when n1 = n2 && s1 = s2 -> true
  62      | NCic.Meta (i, (s,lc)), NCic.Meta (i', (s',lc')) ->
  63         let lc = NCicUtils.expand_local_context lc in
  64         let lc' = NCicUtils.expand_local_context lc' in
  65         i = i' &&
  66         (try
  67           List.fold_left2
  68            (fun b xt xt' -> b && aux (NCicSubstitution.lift status s xt) (NCicSubstitution.lift status s' xt'))
  69            true lc lc'
  70          with
  71           Invalid_argument _ -> false)
  72      | NCic.Appl [_], _ | _, NCic.Appl [_] -> assert false
  73      | NCic.Sort s, NCic.Sort s' -> s == s'
  74      | _,_ -> false (* we already know that t != t' *)
  75   in
  76    aux
  77 ;;
  78
  79 exception WhatAndWithWhatDoNotHaveTheSameLength;;
  80
  81 let replace_lifting status ~equality ~context ~what ~with_what ~where =
  82   let find_image ctx what t =
  83    let rec find_image_aux =
  84     function
  85        [],[] -> raise Not_found
  86      | what::tl1,with_what::tl2 ->
  87         if equality ctx what t then with_what else find_image_aux (tl1,tl2)
  88      | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
  89    in
  90     find_image_aux (what,with_what)
  91   in
  92   let add_ctx ctx n s = (n, NCic.Decl s)::ctx in
  93   let add_ctx1 ctx n s ty = (n, NCic.Def (s,ty))::ctx in
  94   let rec substaux k ctx what t =
  95    try
  96     NCicSubstitution.lift status (k-1) (find_image ctx what t)
  97    with Not_found ->
  98     match t with
  99       NCic.Rel _ as t -> t
 100     | NCic.Meta (i, (shift,l)) ->
 101        let l = NCicUtils.expand_local_context l in
 102        let l' =
 103         List.map (fun t -> substaux k ctx what (NCicSubstitution.lift status shift t)) l
 104        in
 105         NCic.Meta(i,NCicMetaSubst.pack_lc (0, NCic.Ctx l'))
 106     | NCic.Sort _ as t -> t
 107     | NCic.Implicit _ as t -> t
 108     | NCic.Prod (n,s,t) ->
 109        NCic.Prod
 110         (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (NCicSubstitution.lift status 1) what) t)
 111     | NCic.Lambda (n,s,t) ->
 112        NCic.Lambda
 113         (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (NCicSubstitution.lift status 1) what) t)
 114     | NCic.LetIn (n,s,ty,t) ->
 115        NCic.LetIn
 116         (n, substaux k ctx what s, substaux k ctx what ty, substaux (k + 1) (add_ctx1 ctx n s ty) (List.map (NCicSubstitution.lift status 1) what) t)
 117     | NCic.Appl (he::tl) ->
 118        (* Invariant: no Appl applied to another Appl *)
 119        let tl' = List.map (substaux k ctx what) tl in
 120         begin
 121          match substaux k ctx what he with
 122             NCic.Appl l -> NCic.Appl (l@tl')
 123           | _ as he' -> NCic.Appl (he'::tl')
 124         end
 125     | NCic.Appl _ -> assert false
 126     | NCic.Const _ as t -> t
 127     | NCic.Match (it,outt,t,pl) ->
 128        NCic.Match (it,substaux k ctx what outt, substaux k ctx what t,
 129         List.map (substaux k ctx what) pl)
 130  in
 131 (*
 132   prerr_endline "*** replace lifting -- what:";
 133   List.iter (fun x -> prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context x)) what;
 134   prerr_endline "\n*** replace lifting -- with what:";
 135   List.iter (fun x -> prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context x)) with_what;
 136   prerr_endline "\n*** replace lifting -- where:";
 137   prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context where);
 138 *)
 139
 140   substaux 1 context what where
 141 ;;
 142
 143