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   if n = 0 then
  69    (function t -> t)
  70   else
  71    liftaux 1
  72 ;;
  73
  74 let subst arg =
  75  let rec substaux k =
  76   let module C = Cic in
  77    function
  78       C.Rel n as t ->
  79        (match n with
  80            n when n = k -> lift (k - 1) arg
  81          | n when n < k -> t
  82          | _            -> C.Rel (n - 1)
  83        )
  84     | C.Var _ as t  -> t
  85     | C.Meta _ as t -> t
  86     | C.Sort _ as t -> t
  87     | C.Implicit as t -> t
  88     | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
  89     | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
  90     | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
  91     | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
  92     | C.Appl (he::tl) ->
  93        (* Invariant: no Appl applied to another Appl *)
  94        let tl' = List.map (substaux k) tl in
  95         begin
  96          match substaux k he with
  97             C.Appl l -> C.Appl (l@tl')
  98           | _ as he' -> C.Appl (he'::tl')
  99         end
 100     | C.Appl _ -> assert false
 101     | C.Const _ as t -> t
 102     | C.Abst _ as t -> t
 103     | C.MutInd _ as t -> t
 104     | C.MutConstruct _ as t -> t
 105     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
 106        C.MutCase (sp,cookingsno,i,substaux k outt, substaux k t,
 107         List.map (substaux k) pl)
 108     | C.Fix (i,fl) ->
 109        let len = List.length fl in
 110        let substitutedfl =
 111         List.map
 112          (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
 113           fl
 114        in
 115         C.Fix (i, substitutedfl)
 116     | C.CoFix (i,fl) ->
 117        let len = List.length fl in
 118        let substitutedfl =
 119         List.map
 120          (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
 121           fl
 122        in
 123         C.CoFix (i, substitutedfl)
 124  in
 125   substaux 1
 126 ;;
 127
 128 let undebrujin_inductive_def uri =
 129  function
 130     Cic.InductiveDefinition (dl,params,n_ind_params) ->
 131      let dl' =
 132       List.map
 133        (fun (name,inductive,arity,constructors) ->
 134          let constructors' =
 135           List.map
 136            (fun (name,ty,r) ->
 137              let ty' =
 138               let counter = ref (List.length dl) in
 139                List.fold_right
 140                 (fun _ ->
 141                   decr counter ;
 142                   subst (Cic.MutInd (uri,0,!counter))
 143                 ) dl ty
 144              in
 145               (name,ty',r)
 146            ) constructors
 147          in
 148           (name,inductive,arity,constructors')
 149        ) dl
 150       in
 151        Cic.InductiveDefinition (dl', params, n_ind_params)
 152   | obj -> obj
 153 ;;