helm/ocaml/cic_proof_checking/cicSubstitution.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 let lift n =
  27  let rec liftaux k =
  28   let module C = Cic in
  29    function
  30       C.Rel m ->
  31        if m < k then
  32         C.Rel m
  33        else
  34         C.Rel (m + n)
  35     | C.Var _  as t -> t
  36     | C.Meta _ as t -> t
  37     | C.Sort _ as t -> t
  38     | C.Implicit as t -> t
  39     | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty)
  40     | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
  41     | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
  42     | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t)
  43     | C.Appl l -> C.Appl (List.map (liftaux k) l)
  44     | C.Const _ as t -> t
  45     | C.Abst _  as t -> t
  46     | C.MutInd _ as t -> t
  47     | C.MutConstruct _ as t -> t
  48     | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
  49        C.MutCase (sp, cookingsno, i, liftaux k outty, liftaux k t,
  50         List.map (liftaux k) pl)
  51     | C.Fix (i, fl) ->
  52        let len = List.length fl in
  53        let liftedfl =
  54         List.map
  55          (fun (name, i, ty, bo) -> (name, i, liftaux k ty, liftaux (k+len) bo))
  56           fl
  57        in
  58         C.Fix (i, liftedfl)
  59     | C.CoFix (i, fl) ->
  60        let len = List.length fl in
  61        let liftedfl =
  62         List.map
  63          (fun (name, ty, bo) -> (name, liftaux k ty, liftaux (k+len) bo))
  64           fl
  65        in
  66         C.CoFix (i, liftedfl)
  67  in
  68   liftaux 1
  69 ;;
  70
  71 let subst arg =
  72  let rec substaux k =
  73   let module C = Cic in
  74    function
  75       C.Rel n as t ->
  76        (match n with
  77            n when n = k -> lift (k - 1) arg
  78          | n when n < k -> t
  79          | _            -> C.Rel (n - 1)
  80        )
  81     | C.Var _ as t  -> t
  82     | C.Meta _ as t -> t
  83     | C.Sort _ as t -> t
  84     | C.Implicit as t -> t
  85     | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty) (*CSC ??? *)
  86     | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
  87     | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
  88     | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
  89     | C.Appl l -> C.Appl (List.map (substaux k) l)
  90     | C.Const _ as t -> t
  91     | C.Abst _ as t -> t
  92     | C.MutInd _ as t -> t
  93     | C.MutConstruct _ as t -> t
  94     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
  95        C.MutCase (sp,cookingsno,i,substaux k outt, substaux k t,
  96         List.map (substaux k) pl)
  97     | C.Fix (i,fl) ->
  98        let len = List.length fl in
  99        let substitutedfl =
 100         List.map
 101          (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
 102           fl
 103        in
 104         C.Fix (i, substitutedfl)
 105     | C.CoFix (i,fl) ->
 106        let len = List.length fl in
 107        let substitutedfl =
 108         List.map
 109          (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
 110           fl
 111        in
 112         C.CoFix (i, substitutedfl)
 113  in
 114   substaux 1
 115 ;;
 116
 117 let undebrujin_inductive_def uri =
 118  function
 119     Cic.InductiveDefinition (dl,params,n_ind_params) ->
 120      let dl' =
 121       List.map
 122        (fun (name,inductive,arity,constructors) ->
 123          let constructors' =
 124           List.map
 125            (fun (name,ty,r) ->
 126              let ty' =
 127               let counter = ref (List.length dl) in
 128                List.fold_right
 129                 (fun _ ->
 130                   decr counter ;
 131                   subst (Cic.MutInd (uri,0,!counter))
 132                 ) dl ty
 133              in
 134               (name,ty',r)
 135            ) constructors
 136          in
 137           (name,inductive,arity,constructors')
 138        ) dl
 139       in
 140        Cic.InductiveDefinition (dl', params, n_ind_params)
 141   | obj -> obj
 142 ;;