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