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