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