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