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