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