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