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