helm/software/components/cic_unification/cicReplace.ml

   1 (* Copyright (C) 2000, 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://cs.unibo.it/helm/.
  24  *)
  25
  26 (* $Id: cicRefine.ml 7618 2007-09-05 10:07:39Z sacerdot $ *)
  27
  28 exception WhatAndWithWhatDoNotHaveTheSameLength;;
  29
  30 module C = Cic
  31 module S = CicSubstitution
  32
  33 let replace_lifting ~equality ~context ~what ~with_what ~where =
  34   let find_image ctx what t =
  35    let rec find_image_aux =
  36     function
  37        [],[] -> raise Not_found
  38      | what::tl1,with_what::tl2 ->
  39         if equality ctx what t then with_what else find_image_aux (tl1,tl2)
  40      | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
  41    in
  42     find_image_aux (what,with_what)
  43   in
  44   let add_ctx ctx n s = (Some (n, Cic.Decl s))::ctx in
  45   let add_ctx1 ctx n s ty = (Some (n, Cic.Def (s,ty)))::ctx in
  46   let rec substaux k ctx what t =
  47    try
  48     S.lift (k-1) (find_image ctx what t)
  49    with Not_found ->
  50     match t with
  51       C.Rel n as t -> t
  52     | C.Var (uri,exp_named_subst) ->
  53        let exp_named_subst' =
  54         List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst
  55        in
  56         C.Var (uri,exp_named_subst')
  57     | C.Meta (i, l) ->
  58        let l' =
  59         List.map
  60          (function
  61              None -> None
  62            | Some t -> Some (substaux k ctx what t)
  63          ) l
  64        in
  65         C.Meta(i,l')
  66     | C.Sort _ as t -> t
  67     | C.Implicit _ as t -> t
  68     | C.Cast (te,ty) -> C.Cast (substaux k ctx what te, substaux k ctx what ty)
  69     | C.Prod (n,s,t) ->
  70        C.Prod
  71         (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t)
  72     | C.Lambda (n,s,t) ->
  73        C.Lambda
  74         (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t)
  75     | C.LetIn (n,s,ty,t) ->
  76        C.LetIn
  77         (n, substaux k ctx what s, substaux k ctx what ty, substaux (k + 1) (add_ctx1 ctx n s ty) (List.map (S.lift 1) what) t)
  78     | C.Appl (he::tl) ->
  79        (* Invariant: no Appl applied to another Appl *)
  80        let tl' = List.map (substaux k ctx what) tl in
  81         begin
  82          match substaux k ctx what he with
  83             C.Appl l -> C.Appl (l@tl')
  84           | _ as he' -> C.Appl (he'::tl')
  85         end
  86     | C.Appl _ -> assert false
  87     | C.Const (uri,exp_named_subst) ->
  88        let exp_named_subst' =
  89         List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst
  90        in
  91        C.Const (uri,exp_named_subst')
  92     | C.MutInd (uri,i,exp_named_subst) ->
  93        let exp_named_subst' =
  94         List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst
  95        in
  96         C.MutInd (uri,i,exp_named_subst')
  97     | C.MutConstruct (uri,i,j,exp_named_subst) ->
  98        let exp_named_subst' =
  99         List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst
 100        in
 101         C.MutConstruct (uri,i,j,exp_named_subst')
 102     | C.MutCase (sp,i,outt,t,pl) ->
 103        C.MutCase (sp,i,substaux k ctx what outt, substaux k ctx what t,
 104         List.map (substaux k ctx what) pl)
 105     | C.Fix (i,fl) ->
 106        let len = List.length fl in
 107        let substitutedfl =
 108         List.map
 109          (fun (name,i,ty,bo) -> (* WRONG CTX *)
 110            (name, i, substaux k ctx what ty,
 111              substaux (k+len) ctx (List.map (S.lift len) what) bo)
 112          ) fl
 113        in
 114         C.Fix (i, substitutedfl)
 115     | C.CoFix (i,fl) ->
 116        let len = List.length fl in
 117        let substitutedfl =
 118         List.map
 119          (fun (name,ty,bo) -> (* WRONG CTX *)
 120            (name, substaux k ctx what ty,
 121              substaux (k+len) ctx (List.map (S.lift len) what) bo)
 122          ) fl
 123        in
 124         C.CoFix (i, substitutedfl)
 125  in
 126   substaux 1 context what where
 127 ;;
 128
 129