helm/software/components/cic_proof_checking/freshNamesGenerator.ml

   1 (* Copyright (C) 2004, 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 (* $Id$ *)
  27
  28 let debug_print = fun _ -> ()
  29
  30 let rec higher_name arity =
  31   function
  32       Cic.Sort Cic.Prop
  33     | Cic.Sort Cic.CProp ->
  34         if arity = 0 then "A" (* propositions *)
  35         else if arity = 1 then "P" (* predicates *)
  36         else "R" (*relations *)
  37     | Cic.Sort Cic.Set
  38         -> if arity = 0 then "S" else "F"
  39     | Cic.Sort (Cic.Type _ ) ->
  40         if arity = 0 then "T" else "F"
  41     | Cic.Prod (_,_,t) -> higher_name (arity+1) t
  42     | _ -> "f"
  43
  44 let get_initial s =
  45    if String.length s = 0 then "_"
  46    else
  47      let head = String.sub s 0 1 in
  48      String.lowercase head
  49
  50 (* only used when the sort is not Prop or CProp *)
  51 let rec guess_a_name context ty =
  52   match ty with
  53     Cic.Rel n ->
  54       (match List.nth context (n-1) with
  55         None -> assert false
  56       | Some (Cic.Anonymous,_) -> "eccomi_qua"
  57       | Some (Cic.Name s,_) -> get_initial s)
  58   | Cic.Var (uri,_) -> get_initial (UriManager.name_of_uri uri)
  59   | Cic.Sort _ -> higher_name 0 ty
  60   | Cic.Implicit _ -> assert false
  61   | Cic.Cast (t1,t2) -> guess_a_name context t1
  62   | Cic.Prod (na_,_,t) -> higher_name 1 t
  63   | Cic.Lambda _ -> assert false
  64   | Cic.LetIn (_,s,t) -> guess_a_name context (CicSubstitution.subst ~avoid_beta_redexes:true s t)
  65   | Cic.Appl [] -> assert false
  66   | Cic.Appl (he::_) -> guess_a_name context he
  67   | Cic.Const (uri,_)
  68   | Cic.MutInd (uri,_,_)
  69   | Cic.MutConstruct (uri,_,_,_) -> get_initial (UriManager.name_of_uri uri)
  70   | _ -> "x"
  71
  72 (* mk_fresh_name context name typ                      *)
  73 (* returns an identifier which is fresh in the context *)
  74 (* and that resembles [name] as much as possible.      *)
  75 (* [typ] will be the type of the variable              *)
  76 let mk_fresh_name ~subst metasenv context name ~typ =
  77  let module C = Cic in
  78   let basename =
  79    match name with
  80       C.Anonymous ->
  81        (try
  82         let ty,_ =
  83           CicTypeChecker.type_of_aux' ~subst metasenv context typ
  84             CicUniv.empty_ugraph in
  85          (match ty with
  86              C.Sort C.Prop
  87            | C.Sort C.CProp -> "H"
  88            | _ -> guess_a_name context typ
  89          )
  90         with CicTypeChecker.TypeCheckerFailure _ -> "H"
  91        )
  92     | C.Name name ->
  93        Str.global_replace (Str.regexp "[0-9]*$") "" name
  94   in
  95    let already_used name =
  96     List.exists (function Some (n,_) -> n=name | _ -> false) context
  97    in
  98     if name <> C.Anonymous && not (already_used name) then
  99      name
 100     else if not (already_used (C.Name basename)) then
 101      C.Name basename
 102     else
 103      let rec try_next n =
 104       let name' = C.Name (basename ^ string_of_int n) in
 105        if already_used name' then
 106         try_next (n+1)
 107        else
 108         name'
 109      in
 110       try_next 1
 111 ;;
 112
 113 (* let mk_fresh_names ~subst metasenv context t *)
 114 let rec mk_fresh_names ~subst metasenv context t =
 115   match t with
 116     Cic.Rel _ -> t
 117   | Cic.Var (uri,exp_named_subst) ->
 118       let ens =
 119         List.map
 120           (fun (uri,t) ->
 121             (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
 122       Cic.Var (uri,ens)
 123   | Cic.Meta (i,l) ->
 124        let l' =
 125         List.map
 126          (fun t ->
 127            match t with
 128              None -> None
 129            | Some t -> Some (mk_fresh_names ~subst metasenv context t)) l in
 130        Cic.Meta(i,l')
 131     | Cic.Sort _
 132     | Cic.Implicit _ -> t
 133     | Cic.Cast (te,ty) ->
 134        let te' = mk_fresh_names ~subst metasenv context te in
 135        let ty' = mk_fresh_names ~subst metasenv context ty in
 136        Cic.Cast (te', ty')
 137     | Cic.Prod (n,s,t) ->
 138         let s' = mk_fresh_names ~subst metasenv context s in
 139         let n' =
 140           match n with
 141             Cic.Anonymous -> Cic.Anonymous
 142           | Cic.Name "matita_dummy" ->
 143               mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s'
 144           | _ -> n in
 145         let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Decl s')::context) t in
 146         Cic.Prod (n',s',t')
 147     | Cic.Lambda (n,s,t) ->
 148         let s' = mk_fresh_names ~subst metasenv context s in
 149         let n' =
 150           match n with
 151             Cic.Anonymous -> Cic.Anonymous
 152           | Cic.Name "matita_dummy" ->
 153               mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s'
 154           | _ -> n in
 155         let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Decl s')::context) t in
 156         Cic.Lambda (n',s',t')
 157     | Cic.LetIn (n,s,t) ->
 158         let s' = mk_fresh_names ~subst metasenv context s in
 159         let n' =
 160           match n with
 161             Cic.Anonymous -> Cic.Anonymous
 162           | Cic.Name "matita_dummy" ->
 163               mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s'
 164           | _ -> n in
 165         let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Def (s',None))::context) t in
 166         Cic.LetIn (n',s',t')
 167     | Cic.Appl l ->
 168         Cic.Appl (List.map (mk_fresh_names ~subst metasenv context) l)
 169     | Cic.Const (uri,exp_named_subst) ->
 170         let ens =
 171           List.map
 172             (fun (uri,t) ->
 173               (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
 174         Cic.Const(uri,ens)
 175     | Cic.MutInd (uri,tyno,exp_named_subst) ->
 176         let ens =
 177           List.map
 178             (fun (uri,t) ->
 179               (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
 180         Cic.MutInd (uri,tyno,ens)
 181     | Cic.MutConstruct (uri,tyno,consno,exp_named_subst) ->
 182         let ens =
 183           List.map
 184             (fun (uri,t) ->
 185               (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
 186         Cic.MutConstruct (uri,tyno,consno, ens)
 187     | Cic.MutCase (sp,i,outty,t,pl) ->
 188        let outty' = mk_fresh_names ~subst metasenv context outty in
 189        let t' = mk_fresh_names ~subst metasenv context t in
 190        let pl' = List.map (mk_fresh_names ~subst metasenv context) pl in
 191        Cic.MutCase (sp, i, outty', t', pl')
 192     | Cic.Fix (i, fl) ->
 193         let tys = List.map
 194             (fun (n,_,ty,_) ->
 195               Some (Cic.Name n,(Cic.Decl ty))) fl in
 196         let fl' = List.map
 197             (fun (n,i,ty,bo) ->
 198               let ty' = mk_fresh_names ~subst metasenv context ty in
 199               let bo' = mk_fresh_names ~subst metasenv (tys@context) bo in
 200               (n,i,ty',bo')) fl in
 201         Cic.Fix (i, fl')
 202     | Cic.CoFix (i, fl) ->
 203         let tys = List.map
 204             (fun (n,_,ty) ->
 205               Some (Cic.Name n,(Cic.Decl ty))) fl in
 206         let fl' = List.map
 207             (fun (n,ty,bo) ->
 208               let ty' = mk_fresh_names ~subst metasenv context ty in
 209               let bo' = mk_fresh_names ~subst metasenv (tys@context) bo in
 210               (n,ty',bo')) fl in
 211         Cic.CoFix (i, fl')
 212 ;;
 213
 214 (* clean_dummy_dependent_types term                             *)
 215 (* returns a copy of [term] where every dummy dependent product *)
 216 (* have been replaced with a non-dependent product and where    *)
 217 (* dummy let-ins have been removed.                             *)
 218 let clean_dummy_dependent_types t =
 219  let module C = Cic in
 220   let rec aux k =
 221    function
 222       C.Rel m as t -> t,[k - m]
 223     | C.Var (uri,exp_named_subst) ->
 224        let exp_named_subst',rels =
 225         List.fold_right
 226          (fun (uri,t) (exp_named_subst,rels) ->
 227            let t',rels' = aux k t in
 228             (uri,t')::exp_named_subst, rels' @ rels
 229          ) exp_named_subst ([],[])
 230        in
 231         C.Var (uri,exp_named_subst'),rels
 232     | C.Meta (i,l) ->
 233        let l',rels =
 234         List.fold_right
 235          (fun t (l,rels) ->
 236            let t',rels' =
 237             match t with
 238                None -> None,[]
 239              | Some t ->
 240                 let t',rels' = aux k t in
 241                  Some t', rels'
 242            in
 243             t'::l, rels' @ rels
 244          ) l ([],[])
 245        in
 246         C.Meta(i,l'),rels
 247     | C.Sort _ as t -> t,[]
 248     | C.Implicit _ as t -> t,[]
 249     | C.Cast (te,ty) ->
 250        let te',rels1 = aux k te in
 251        let ty',rels2 = aux k ty in
 252         C.Cast (te', ty'), rels1@rels2
 253     | C.Prod (n,s,t) ->
 254        let s',rels1 = aux k s in
 255        let t',rels2 = aux (k+1) t in
 256         let n' =
 257          match n with
 258             C.Anonymous ->
 259              if List.mem k rels2 then
 260 (
 261               debug_print (lazy "If this happens often, we can do something about it (i.e. we can generate a new fresh name; problem: we need the metasenv and context ;-(. Alternative solution: mk_implicit does not generate entries for the elements in the context that have no name") ;
 262               C.Anonymous
 263 )
 264              else
 265               C.Anonymous
 266           | C.Name _ as n ->
 267              if List.mem k rels2 then n else C.Anonymous
 268         in
 269          C.Prod (n', s', t'), rels1@rels2
 270     | C.Lambda (n,s,t) ->
 271        let s',rels1 = aux k s in
 272        let t',rels2 = aux (k+1) t in
 273         C.Lambda (n, s', t'), rels1@rels2
 274     | C.LetIn (n,s,t) ->
 275        let s',rels1 = aux k s in
 276        let t',rels2 = aux (k+1) t in
 277        let rels = rels1 @ rels2 in
 278         if List.mem k rels2 then
 279          C.LetIn (n, s', t'), rels
 280         else
 281          (* (C.Rel 1) is just a dummy term; any term would fit *)
 282          CicSubstitution.subst (C.Rel 1) t', rels
 283     | C.Appl l ->
 284        let l',rels =
 285         List.fold_right
 286          (fun t (exp_named_subst,rels) ->
 287            let t',rels' = aux k t in
 288             t'::exp_named_subst, rels' @ rels
 289          ) l ([],[])
 290        in
 291         C.Appl l', rels
 292     | C.Const (uri,exp_named_subst) ->
 293        let exp_named_subst',rels =
 294         List.fold_right
 295          (fun (uri,t) (exp_named_subst,rels) ->
 296            let t',rels' = aux k t in
 297             (uri,t')::exp_named_subst, rels' @ rels
 298          ) exp_named_subst ([],[])
 299        in
 300         C.Const (uri,exp_named_subst'),rels
 301     | C.MutInd (uri,tyno,exp_named_subst) ->
 302        let exp_named_subst',rels =
 303         List.fold_right
 304          (fun (uri,t) (exp_named_subst,rels) ->
 305            let t',rels' = aux k t in
 306             (uri,t')::exp_named_subst, rels' @ rels
 307          ) exp_named_subst ([],[])
 308        in
 309         C.MutInd (uri,tyno,exp_named_subst'),rels
 310     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
 311        let exp_named_subst',rels =
 312         List.fold_right
 313          (fun (uri,t) (exp_named_subst,rels) ->
 314            let t',rels' = aux k t in
 315             (uri,t')::exp_named_subst, rels' @ rels
 316          ) exp_named_subst ([],[])
 317        in
 318         C.MutConstruct (uri,tyno,consno,exp_named_subst'),rels
 319     | C.MutCase (sp,i,outty,t,pl) ->
 320        let outty',rels1 = aux k outty in
 321        let t',rels2 = aux k t in
 322        let pl',rels3 =
 323         List.fold_right
 324          (fun t (exp_named_subst,rels) ->
 325            let t',rels' = aux k t in
 326             t'::exp_named_subst, rels' @ rels
 327          ) pl ([],[])
 328        in
 329         C.MutCase (sp, i, outty', t', pl'), rels1 @ rels2 @rels3
 330     | C.Fix (i, fl) ->
 331        let len = List.length fl in
 332        let fl',rels =
 333         List.fold_right
 334          (fun (name,i,ty,bo) (fl,rels) ->
 335            let ty',rels1 = aux k ty in
 336            let bo',rels2 = aux (k + len) bo in
 337             (name,i,ty',bo')::fl, rels1 @ rels2 @ rels
 338          ) fl ([],[])
 339        in
 340         C.Fix (i, fl'),rels
 341     | C.CoFix (i, fl) ->
 342        let len = List.length fl in
 343        let fl',rels =
 344         List.fold_right
 345          (fun (name,ty,bo) (fl,rels) ->
 346            let ty',rels1 = aux k ty in
 347            let bo',rels2 = aux (k + len) bo in
 348             (name,ty',bo')::fl, rels1 @ rels2 @ rels
 349          ) fl ([],[])
 350        in
 351         C.CoFix (i, fl'),rels
 352   in
 353    fst (aux 0 t)
 354 ;;