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 exception CannotSubstInMeta;;
  27 exception RelToHiddenHypothesis;;
  28
  29 let lift n =
  30  let rec liftaux k =
  31   let module C = Cic in
  32    function
  33       C.Rel m ->
  34        if m < k then
  35         C.Rel m
  36        else
  37         C.Rel (m + n)
  38     | C.Var _  as t -> t
  39     | C.Meta (i,l) ->
  40        let l' =
  41         List.map
  42          (function
  43              None -> None
  44            | Some t -> Some (liftaux k t)
  45          ) l
  46        in
  47         C.Meta(i,l')
  48     | C.Sort _ as t -> t
  49     | C.Implicit as t -> t
  50     | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty)
  51     | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
  52     | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
  53     | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t)
  54     | C.Appl l -> C.Appl (List.map (liftaux k) l)
  55     | C.Const _ as t -> t
  56     | C.MutInd _ as t -> t
  57     | C.MutConstruct _ as t -> t
  58     | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
  59        C.MutCase (sp, cookingsno, i, liftaux k outty, liftaux k t,
  60         List.map (liftaux k) pl)
  61     | C.Fix (i, fl) ->
  62        let len = List.length fl in
  63        let liftedfl =
  64         List.map
  65          (fun (name, i, ty, bo) -> (name, i, liftaux k ty, liftaux (k+len) bo))
  66           fl
  67        in
  68         C.Fix (i, liftedfl)
  69     | C.CoFix (i, fl) ->
  70        let len = List.length fl in
  71        let liftedfl =
  72         List.map
  73          (fun (name, ty, bo) -> (name, liftaux k ty, liftaux (k+len) bo))
  74           fl
  75        in
  76         C.CoFix (i, liftedfl)
  77  in
  78   if n = 0 then
  79    (function t -> t)
  80   else
  81    liftaux 1
  82 ;;
  83
  84 let subst arg =
  85  let rec substaux k =
  86   let module C = Cic in
  87    function
  88       C.Rel n as t ->
  89        (match n with
  90            n when n = k -> lift (k - 1) arg
  91          | n when n < k -> t
  92          | _            -> C.Rel (n - 1)
  93        )
  94     | C.Var _ as t  -> t
  95     | C.Meta (i, l) as t ->
  96        let l' =
  97         List.map
  98          (function
  99              None -> None
 100            | Some t -> Some (substaux k t)
 101          ) l
 102        in
 103         C.Meta(i,l')
 104     | C.Sort _ as t -> t
 105     | C.Implicit as t -> t
 106     | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
 107     | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
 108     | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
 109     | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
 110     | C.Appl (he::tl) ->
 111        (* Invariant: no Appl applied to another Appl *)
 112        let tl' = List.map (substaux k) tl in
 113         begin
 114          match substaux k he with
 115             C.Appl l -> C.Appl (l@tl')
 116           | _ as he' -> C.Appl (he'::tl')
 117         end
 118     | C.Appl _ -> assert false
 119     | C.Const _ as t -> t
 120     | C.MutInd _ as t -> t
 121     | C.MutConstruct _ as t -> t
 122     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
 123        C.MutCase (sp,cookingsno,i,substaux k outt, substaux k t,
 124         List.map (substaux k) pl)
 125     | C.Fix (i,fl) ->
 126        let len = List.length fl in
 127        let substitutedfl =
 128         List.map
 129          (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
 130           fl
 131        in
 132         C.Fix (i, substitutedfl)
 133     | C.CoFix (i,fl) ->
 134        let len = List.length fl in
 135        let substitutedfl =
 136         List.map
 137          (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
 138           fl
 139        in
 140         C.CoFix (i, substitutedfl)
 141  in
 142   substaux 1
 143 ;;
 144
 145 let undebrujin_inductive_def uri =
 146  function
 147     Cic.InductiveDefinition (dl,params,n_ind_params) ->
 148      let dl' =
 149       List.map
 150        (fun (name,inductive,arity,constructors) ->
 151          let constructors' =
 152           List.map
 153            (fun (name,ty,r) ->
 154              let ty' =
 155               let counter = ref (List.length dl) in
 156                List.fold_right
 157                 (fun _ ->
 158                   decr counter ;
 159                   subst (Cic.MutInd (uri,0,!counter))
 160                 ) dl ty
 161              in
 162               (name,ty',r)
 163            ) constructors
 164          in
 165           (name,inductive,arity,constructors')
 166        ) dl
 167       in
 168        Cic.InductiveDefinition (dl', params, n_ind_params)
 169   | obj -> obj
 170 ;;
 171
 172 (* l is the relocation list *)
 173
 174 let lift_meta l t =
 175     let module C = Cic in
 176     if l = [] then t else
 177     let rec aux k = function
 178       C.Rel n as t ->
 179         if n <= k then t else
 180          (try
 181            match List.nth l (n-k-1) with
 182               None -> raise RelToHiddenHypothesis
 183             | Some t -> lift k t
 184           with
 185            (Failure _) -> assert false
 186          )
 187     | C.Var _ as t  -> t
 188     | C.Meta (i,l) ->
 189        let l' =
 190         List.map
 191          (function
 192              None -> None
 193            | Some t ->
 194               try
 195                Some (aux k t)
 196               with
 197                RelToHiddenHypothesis -> None
 198          ) l
 199        in
 200         C.Meta(i,l')
 201     | C.Sort _ as t -> t
 202     | C.Implicit as t -> t
 203     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) (*CSC ??? *)
 204     | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t)
 205     | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t)
 206     | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k + 1) t)
 207     | C.Appl l -> C.Appl (List.map (aux k) l)
 208     | C.Const _ as t -> t
 209     | C.MutInd _ as t -> t
 210     | C.MutConstruct _ as t -> t
 211     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
 212        C.MutCase (sp,cookingsno,i,aux k outt, aux k t,
 213         List.map (aux k) pl)
 214     | C.Fix (i,fl) ->
 215        let len = List.length fl in
 216        let substitutedfl =
 217         List.map
 218          (fun (name,i,ty,bo) -> (name, i, aux k ty, aux (k+len) bo))
 219           fl
 220        in
 221         C.Fix (i, substitutedfl)
 222     | C.CoFix (i,fl) ->
 223        let len = List.length fl in
 224        let substitutedfl =
 225         List.map
 226          (fun (name,ty,bo) -> (name, aux k ty, aux (k+len) bo))
 227           fl
 228        in
 229         C.CoFix (i, substitutedfl)
 230  in
 231   aux 0 t
 232 ;;