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