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 ;;
 236
 237 (************************************************************************)
 238 (*CSC: spostare in cic_unification *)
 239
 240 (* the delift function takes in input an ordered list of integers [n1,...,nk]
 241    and a term t, and relocates rel(nk) to k. Typically, the list of integers
 242    is a parameter of a metavariable occurrence. *)
 243
 244 exception NotInTheList;;
 245
 246 let position n =
 247   let rec aux k =
 248    function
 249        [] -> raise NotInTheList
 250      | (Some (Cic.Rel m))::_ when m=n -> k
 251      | _::tl -> aux (k+1) tl in
 252   aux 1
 253 ;;
 254
 255 let restrict to_be_restricted =
 256   let rec erase i n =
 257     function
 258         [] -> []
 259       | _::tl when List.mem (n,i) to_be_restricted ->
 260           None::(erase (i+1) n tl)
 261       | he::tl -> he::(erase (i+1) n tl) in
 262   let rec aux =
 263     function
 264         [] -> []
 265       | (n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in
 266   aux
 267 ;;
 268
 269
 270 let delift context metasenv l t =
 271  let to_be_restricted = ref [] in
 272  let rec deliftaux k =
 273   let module C = Cic in
 274    function
 275       C.Rel m ->
 276         if m <=k then
 277          C.Rel m   (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *)
 278                    (*CSC: deliftato la regola per il LetIn                 *)
 279         else
 280          (match List.nth context (m-k-1) with
 281            Some (_,C.Def t) -> deliftaux k (lift m t)
 282          | Some (_,C.Decl t) ->
 283             (* It may augment to_be_restricted *)
 284             ignore (deliftaux k (lift m t)) ;
 285             C.Rel ((position (m-k) l) + k)
 286          | None -> raise RelToHiddenHypothesis)
 287     | C.Var _  as t -> t
 288     | C.Meta (i, l1) as t ->
 289        let rec deliftl j =
 290         function
 291            [] -> []
 292          | None::tl -> None::(deliftl (j+1) tl)
 293          | (Some t)::tl ->
 294             let l1' = (deliftl (j+1) tl) in
 295              try
 296               Some (deliftaux k t)::l1'
 297              with
 298                 RelToHiddenHypothesis
 299               | NotInTheList ->
 300                  to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
 301        in
 302         let l' = deliftl 1 l1 in
 303          C.Meta(i,l')
 304     | C.Sort _ as t -> t
 305     | C.Implicit as t -> t
 306     | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
 307     | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
 308     | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
 309     | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
 310     | C.Appl l -> C.Appl (List.map (deliftaux k) l)
 311     | C.Const _ as t -> t
 312     | C.Abst _  as t -> t
 313     | C.MutInd _ as t -> t
 314     | C.MutConstruct _ as t -> t
 315     | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
 316        C.MutCase (sp, cookingsno, i, deliftaux k outty, deliftaux k t,
 317         List.map (deliftaux k) pl)
 318     | C.Fix (i, fl) ->
 319        let len = List.length fl in
 320        let liftedfl =
 321         List.map
 322          (fun (name, i, ty, bo) -> (name, i, deliftaux k ty, deliftaux (k+len) bo))
 323           fl
 324        in
 325         C.Fix (i, liftedfl)
 326     | C.CoFix (i, fl) ->
 327        let len = List.length fl in
 328        let liftedfl =
 329         List.map
 330          (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo))
 331           fl
 332        in
 333         C.CoFix (i, liftedfl)
 334  in
 335    let res = deliftaux 0 t in
 336    res, restrict !to_be_restricted metasenv
 337 ;;