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 (* $Id$ *)
  27
  28 exception CannotSubstInMeta;;
  29 exception RelToHiddenHypothesis;;
  30 exception ReferenceToVariable;;
  31 exception ReferenceToConstant;;
  32 exception ReferenceToCurrentProof;;
  33 exception ReferenceToInductiveDefinition;;
  34
  35 let debug_print = fun _ -> ()
  36
  37 let lift_from k n =
  38  let rec liftaux k =
  39   let module C = Cic in
  40    function
  41       C.Rel m ->
  42        if m < k then
  43         C.Rel m
  44        else
  45         C.Rel (m + n)
  46     | C.Var (uri,exp_named_subst) ->
  47        let exp_named_subst' =
  48         List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
  49        in
  50         C.Var (uri,exp_named_subst')
  51     | C.Meta (i,l) ->
  52        let l' =
  53         List.map
  54          (function
  55              None -> None
  56            | Some t -> Some (liftaux k t)
  57          ) l
  58        in
  59         C.Meta(i,l')
  60     | C.Sort _ as t -> t
  61     | C.Implicit _ as t -> t
  62     | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty)
  63     | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
  64     | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
  65     | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t)
  66     | C.Appl l -> C.Appl (List.map (liftaux k) l)
  67     | C.Const (uri,exp_named_subst) ->
  68        let exp_named_subst' =
  69         List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
  70        in
  71         C.Const (uri,exp_named_subst')
  72     | C.MutInd (uri,tyno,exp_named_subst) ->
  73        let exp_named_subst' =
  74         List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
  75        in
  76         C.MutInd (uri,tyno,exp_named_subst')
  77     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
  78        let exp_named_subst' =
  79         List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
  80        in
  81         C.MutConstruct (uri,tyno,consno,exp_named_subst')
  82     | C.MutCase (sp,i,outty,t,pl) ->
  83        C.MutCase (sp, i, liftaux k outty, liftaux k t,
  84         List.map (liftaux k) pl)
  85     | C.Fix (i, fl) ->
  86        let len = List.length fl in
  87        let liftedfl =
  88         List.map
  89          (fun (name, i, ty, bo) -> (name, i, liftaux k ty, liftaux (k+len) bo))
  90           fl
  91        in
  92         C.Fix (i, liftedfl)
  93     | C.CoFix (i, fl) ->
  94        let len = List.length fl in
  95        let liftedfl =
  96         List.map
  97          (fun (name, ty, bo) -> (name, liftaux k ty, liftaux (k+len) bo))
  98           fl
  99        in
 100         C.CoFix (i, liftedfl)
 101  in
 102  liftaux k
 103
 104 let lift n t =
 105   if n = 0 then
 106    t
 107   else
 108    lift_from 1 n t
 109 ;;
 110
 111 let subst arg =
 112  let rec substaux k =
 113   let module C = Cic in
 114    function
 115       C.Rel n as t ->
 116        (match n with
 117            n when n = k -> lift (k - 1) arg
 118          | n when n < k -> t
 119          | _            -> C.Rel (n - 1)
 120        )
 121     | C.Var (uri,exp_named_subst) ->
 122        let exp_named_subst' =
 123         List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
 124        in
 125         C.Var (uri,exp_named_subst')
 126     | C.Meta (i, l) ->
 127        let l' =
 128         List.map
 129          (function
 130              None -> None
 131            | Some t -> Some (substaux k t)
 132          ) l
 133        in
 134         C.Meta(i,l')
 135     | C.Sort _ as t -> t
 136     | C.Implicit _ as t -> t
 137     | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
 138     | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
 139     | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
 140     | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
 141     | C.Appl (he::tl) ->
 142        (* Invariant: no Appl applied to another Appl *)
 143        let tl' = List.map (substaux k) tl in
 144         begin
 145          match substaux k he with
 146             C.Appl l -> C.Appl (l@tl')
 147           | _ as he' -> C.Appl (he'::tl')
 148         end
 149     | C.Appl _ -> assert false
 150     | C.Const (uri,exp_named_subst)  ->
 151        let exp_named_subst' =
 152         List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
 153        in
 154         C.Const (uri,exp_named_subst')
 155     | C.MutInd (uri,typeno,exp_named_subst) ->
 156        let exp_named_subst' =
 157         List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
 158        in
 159         C.MutInd (uri,typeno,exp_named_subst')
 160     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
 161        let exp_named_subst' =
 162         List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
 163        in
 164         C.MutConstruct (uri,typeno,consno,exp_named_subst')
 165     | C.MutCase (sp,i,outt,t,pl) ->
 166        C.MutCase (sp,i,substaux k outt, substaux k t,
 167         List.map (substaux k) pl)
 168     | C.Fix (i,fl) ->
 169        let len = List.length fl in
 170        let substitutedfl =
 171         List.map
 172          (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
 173           fl
 174        in
 175         C.Fix (i, substitutedfl)
 176     | C.CoFix (i,fl) ->
 177        let len = List.length fl in
 178        let substitutedfl =
 179         List.map
 180          (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
 181           fl
 182        in
 183         C.CoFix (i, substitutedfl)
 184  in
 185   substaux 1
 186 ;;
 187
 188 (*CSC: i controlli di tipo debbono essere svolti da destra a             *)
 189 (*CSC: sinistra: i{B/A;b/a} ==> a{B/A;b/a} ==> a{b/a{B/A}} ==> b         *)
 190 (*CSC: la sostituzione ora e' implementata in maniera simultanea, ma     *)
 191 (*CSC: dovrebbe diventare da sinistra verso destra:                      *)
 192 (*CSC: t{a=a/A;b/a} ==> \H:a=a.H{b/a} ==> \H:b=b.H                       *)
 193 (*CSC: per la roba che proviene da Coq questo non serve!                 *)
 194 let subst_vars exp_named_subst =
 195 (*
 196 debug_print (lazy ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS")) ;
 197 *)
 198  let rec substaux k =
 199   let module C = Cic in
 200    function
 201       C.Rel _ as t -> t
 202     | C.Var (uri,exp_named_subst') ->
 203        (try
 204          let (_,arg) =
 205           List.find
 206            (function (varuri,_) -> UriManager.eq uri varuri) exp_named_subst
 207          in
 208           lift (k -1) arg
 209         with
 210          Not_found ->
 211           let params =
 212            let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 213            (match obj with
 214                C.Constant _ -> raise ReferenceToConstant
 215              | C.Variable (_,_,_,params,_) -> params
 216              | C.CurrentProof _ -> raise ReferenceToCurrentProof
 217              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 218            )
 219           in
 220 (*
 221 debug_print (lazy "\n\n---- BEGIN ") ;
 222 debug_print (lazy ("----params: " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ;
 223 debug_print (lazy ("----S(" ^ UriManager.string_of_uri uri ^ "): " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst))) ;
 224 debug_print (lazy ("----P: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst'))) ;
 225 *)
 226            let exp_named_subst'' =
 227             substaux_in_exp_named_subst uri k exp_named_subst' params
 228            in
 229 (*
 230 debug_print (lazy ("----D: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst''))) ;
 231 debug_print (lazy "---- END\n\n ") ;
 232 *)
 233             C.Var (uri,exp_named_subst'')
 234        )
 235     | C.Meta (i, l) ->
 236        let l' =
 237         List.map
 238          (function
 239              None -> None
 240            | Some t -> Some (substaux k t)
 241          ) l
 242        in
 243         C.Meta(i,l')
 244     | C.Sort _ as t -> t
 245     | C.Implicit _ as t -> t
 246     | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
 247     | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
 248     | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
 249     | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
 250     | C.Appl (he::tl) ->
 251        (* Invariant: no Appl applied to another Appl *)
 252        let tl' = List.map (substaux k) tl in
 253         begin
 254          match substaux k he with
 255             C.Appl l -> C.Appl (l@tl')
 256           | _ as he' -> C.Appl (he'::tl')
 257         end
 258     | C.Appl _ -> assert false
 259     | C.Const (uri,exp_named_subst')  ->
 260        let params =
 261         let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 262         (match obj with
 263             C.Constant (_,_,_,params,_) -> params
 264           | C.Variable _ -> raise ReferenceToVariable
 265           | C.CurrentProof (_,_,_,_,params,_) -> params
 266           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 267         )
 268        in
 269         let exp_named_subst'' =
 270          substaux_in_exp_named_subst uri k exp_named_subst' params
 271         in
 272          C.Const (uri,exp_named_subst'')
 273     | C.MutInd (uri,typeno,exp_named_subst') ->
 274        let params =
 275         let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 276         (match obj with
 277             C.Constant _ -> raise ReferenceToConstant
 278           | C.Variable _ -> raise ReferenceToVariable
 279           | C.CurrentProof _ -> raise ReferenceToCurrentProof
 280           | C.InductiveDefinition (_,params,_,_) -> params
 281         )
 282        in
 283         let exp_named_subst'' =
 284          substaux_in_exp_named_subst uri k exp_named_subst' params
 285         in
 286          C.MutInd (uri,typeno,exp_named_subst'')
 287     | C.MutConstruct (uri,typeno,consno,exp_named_subst') ->
 288        let params =
 289         let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 290         (match obj with
 291             C.Constant _ -> raise ReferenceToConstant
 292           | C.Variable _ -> raise ReferenceToVariable
 293           | C.CurrentProof _ -> raise ReferenceToCurrentProof
 294           | C.InductiveDefinition (_,params,_,_) -> params
 295         )
 296        in
 297         let exp_named_subst'' =
 298          substaux_in_exp_named_subst uri k exp_named_subst' params
 299         in
 300          C.MutConstruct (uri,typeno,consno,exp_named_subst'')
 301     | C.MutCase (sp,i,outt,t,pl) ->
 302        C.MutCase (sp,i,substaux k outt, substaux k t,
 303         List.map (substaux k) pl)
 304     | C.Fix (i,fl) ->
 305        let len = List.length fl in
 306        let substitutedfl =
 307         List.map
 308          (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo))
 309           fl
 310        in
 311         C.Fix (i, substitutedfl)
 312     | C.CoFix (i,fl) ->
 313        let len = List.length fl in
 314        let substitutedfl =
 315         List.map
 316          (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
 317           fl
 318        in
 319         C.CoFix (i, substitutedfl)
 320  and substaux_in_exp_named_subst uri k exp_named_subst' params =
 321 (*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *)
 322 (*CSC: e' vero???? una veloce prova non sembra confermare la teoria        *)
 323   let rec filter_and_lift =
 324    function
 325       [] -> []
 326     | (uri,t)::tl when
 327         List.for_all
 328          (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst'
 329         &&
 330          List.mem uri params
 331        ->
 332         (uri,lift (k-1) t)::(filter_and_lift tl)
 333     | _::tl -> filter_and_lift tl
 334 (*
 335     | (uri,_)::tl ->
 336 debug_print (lazy ("---- SKIPPO " ^ UriManager.string_of_uri uri)) ;
 337 if List.for_all (function (uri',_) -> not (UriManager.eq uri uri'))
 338 exp_named_subst' then debug_print (lazy "---- OK1") ;
 339 debug_print (lazy ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ;
 340 if List.mem uri params then debug_print (lazy "---- OK2") ;
 341         filter_and_lift tl
 342 *)
 343   in
 344    List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst' @
 345     (filter_and_lift exp_named_subst)
 346  in
 347   substaux 1
 348 ;;
 349
 350 (* subst_meta [t_1 ; ... ; t_n] t                                *)
 351 (* returns the term [t] where [Rel i] is substituted with [t_i] *)
 352 (* [t_i] is lifted as usual when it crosses an abstraction      *)
 353 let subst_meta l t =
 354  let module C = Cic in
 355   if l = [] then t else
 356    let rec aux k = function
 357       C.Rel n as t ->
 358         if n <= k then t else
 359          (try
 360            match List.nth l (n-k-1) with
 361               None -> raise RelToHiddenHypothesis
 362             | Some t -> lift k t
 363           with
 364            (Failure _) -> assert false
 365          )
 366     | C.Var (uri,exp_named_subst) ->
 367        let exp_named_subst' =
 368         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
 369        in
 370         C.Var (uri,exp_named_subst')
 371     | C.Meta (i,l) ->
 372        let l' =
 373         List.map
 374          (function
 375              None -> None
 376            | Some t ->
 377               try
 378                Some (aux k t)
 379               with
 380                RelToHiddenHypothesis -> None
 381          ) l
 382        in
 383         C.Meta(i,l')
 384     | C.Sort _ as t -> t
 385     | C.Implicit _ as t -> t
 386     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) (*CSC ??? *)
 387     | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t)
 388     | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t)
 389     | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k + 1) t)
 390     | C.Appl l -> C.Appl (List.map (aux k) l)
 391     | C.Const (uri,exp_named_subst) ->
 392        let exp_named_subst' =
 393         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
 394        in
 395         C.Const (uri,exp_named_subst')
 396     | C.MutInd (uri,typeno,exp_named_subst) ->
 397        let exp_named_subst' =
 398         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
 399        in
 400         C.MutInd (uri,typeno,exp_named_subst')
 401     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
 402        let exp_named_subst' =
 403         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
 404        in
 405         C.MutConstruct (uri,typeno,consno,exp_named_subst')
 406     | C.MutCase (sp,i,outt,t,pl) ->
 407        C.MutCase (sp,i,aux k outt, aux k t, List.map (aux k) pl)
 408     | C.Fix (i,fl) ->
 409        let len = List.length fl in
 410        let substitutedfl =
 411         List.map
 412          (fun (name,i,ty,bo) -> (name, i, aux k ty, aux (k+len) bo))
 413           fl
 414        in
 415         C.Fix (i, substitutedfl)
 416     | C.CoFix (i,fl) ->
 417        let len = List.length fl in
 418        let substitutedfl =
 419         List.map
 420          (fun (name,ty,bo) -> (name, aux k ty, aux (k+len) bo))
 421           fl
 422        in
 423         C.CoFix (i, substitutedfl)
 424  in
 425   aux 0 t
 426 ;;
 427