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