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