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