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,_ =
 197           List.fold_left
 198             (fun (types,len) (n,_,ty,_) ->
 199                (Some (Cic.Name n,(Cic.Decl (CicSubstitution.lift len ty)))::types,
 200                 len+1)
 201             ) ([],0) fl
 202         in
 203         let fl' = List.map
 204             (fun (n,i,ty,bo) ->
 205               let ty' = mk_fresh_names ~subst metasenv context ty in
 206               let bo' = mk_fresh_names ~subst metasenv (tys@context) bo in
 207               (n,i,ty',bo')) fl in
 208         Cic.Fix (i, fl')
 209     | Cic.CoFix (i, fl) ->
 210         let tys,_ =
 211           List.fold_left
 212             (fun (types,len) (n,ty,_) ->
 213                (Some (Cic.Name n,(Cic.Decl (CicSubstitution.lift len ty)))::types,
 214                 len+1)
 215             ) ([],0) fl
 216         in
 217         let fl' = List.map
 218             (fun (n,ty,bo) ->
 219               let ty' = mk_fresh_names ~subst metasenv context ty in
 220               let bo' = mk_fresh_names ~subst metasenv (tys@context) bo in
 221               (n,ty',bo')) fl in
 222         Cic.CoFix (i, fl')
 223 ;;
 224
 225 (* clean_dummy_dependent_types term                             *)
 226 (* returns a copy of [term] where every dummy dependent product *)
 227 (* have been replaced with a non-dependent product and where    *)
 228 (* dummy let-ins have been removed.                             *)
 229 let clean_dummy_dependent_types t =
 230  let module C = Cic in
 231   let rec aux k =
 232    function
 233       C.Rel m as t -> t,[k - m]
 234     | C.Var (uri,exp_named_subst) ->
 235        let exp_named_subst',rels =
 236         List.fold_right
 237          (fun (uri,t) (exp_named_subst,rels) ->
 238            let t',rels' = aux k t in
 239             (uri,t')::exp_named_subst, rels' @ rels
 240          ) exp_named_subst ([],[])
 241        in
 242         C.Var (uri,exp_named_subst'),rels
 243     | C.Meta (i,l) ->
 244        let l',rels =
 245         List.fold_right
 246          (fun t (l,rels) ->
 247            let t',rels' =
 248             match t with
 249                None -> None,[]
 250              | Some t ->
 251                 let t',rels' = aux k t in
 252                  Some t', rels'
 253            in
 254             t'::l, rels' @ rels
 255          ) l ([],[])
 256        in
 257         C.Meta(i,l'),rels
 258     | C.Sort _ as t -> t,[]
 259     | C.Implicit _ as t -> t,[]
 260     | C.Cast (te,ty) ->
 261        let te',rels1 = aux k te in
 262        let ty',rels2 = aux k ty in
 263         C.Cast (te', ty'), rels1@rels2
 264     | C.Prod (n,s,t) ->
 265        let s',rels1 = aux k s in
 266        let t',rels2 = aux (k+1) t in
 267         let n' =
 268          match n with
 269             C.Anonymous ->
 270              if List.mem k rels2 then
 271 (
 272               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") ;
 273               C.Anonymous
 274 )
 275              else
 276               C.Anonymous
 277           | C.Name _ as n ->
 278              if List.mem k rels2 then n else C.Anonymous
 279         in
 280          C.Prod (n', s', t'), rels1@rels2
 281     | C.Lambda (n,s,t) ->
 282        let s',rels1 = aux k s in
 283        let t',rels2 = aux (k+1) t in
 284         C.Lambda (n, s', t'), rels1@rels2
 285     | C.LetIn (n,s,t) ->
 286        let s',rels1 = aux k s in
 287        let t',rels2 = aux (k+1) t in
 288        let rels = rels1 @ rels2 in
 289         if List.mem k rels2 then
 290          C.LetIn (n, s', t'), rels
 291         else
 292          (* (C.Rel 1) is just a dummy term; any term would fit *)
 293          CicSubstitution.subst (C.Rel 1) t', rels
 294     | C.Appl l ->
 295        let l',rels =
 296         List.fold_right
 297          (fun t (exp_named_subst,rels) ->
 298            let t',rels' = aux k t in
 299             t'::exp_named_subst, rels' @ rels
 300          ) l ([],[])
 301        in
 302         C.Appl l', rels
 303     | C.Const (uri,exp_named_subst) ->
 304        let exp_named_subst',rels =
 305         List.fold_right
 306          (fun (uri,t) (exp_named_subst,rels) ->
 307            let t',rels' = aux k t in
 308             (uri,t')::exp_named_subst, rels' @ rels
 309          ) exp_named_subst ([],[])
 310        in
 311         C.Const (uri,exp_named_subst'),rels
 312     | C.MutInd (uri,tyno,exp_named_subst) ->
 313        let exp_named_subst',rels =
 314         List.fold_right
 315          (fun (uri,t) (exp_named_subst,rels) ->
 316            let t',rels' = aux k t in
 317             (uri,t')::exp_named_subst, rels' @ rels
 318          ) exp_named_subst ([],[])
 319        in
 320         C.MutInd (uri,tyno,exp_named_subst'),rels
 321     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
 322        let exp_named_subst',rels =
 323         List.fold_right
 324          (fun (uri,t) (exp_named_subst,rels) ->
 325            let t',rels' = aux k t in
 326             (uri,t')::exp_named_subst, rels' @ rels
 327          ) exp_named_subst ([],[])
 328        in
 329         C.MutConstruct (uri,tyno,consno,exp_named_subst'),rels
 330     | C.MutCase (sp,i,outty,t,pl) ->
 331        let outty',rels1 = aux k outty in
 332        let t',rels2 = aux k t in
 333        let pl',rels3 =
 334         List.fold_right
 335          (fun t (exp_named_subst,rels) ->
 336            let t',rels' = aux k t in
 337             t'::exp_named_subst, rels' @ rels
 338          ) pl ([],[])
 339        in
 340         C.MutCase (sp, i, outty', t', pl'), rels1 @ rels2 @rels3
 341     | C.Fix (i, fl) ->
 342        let len = List.length fl in
 343        let fl',rels =
 344         List.fold_right
 345          (fun (name,i,ty,bo) (fl,rels) ->
 346            let ty',rels1 = aux k ty in
 347            let bo',rels2 = aux (k + len) bo in
 348             (name,i,ty',bo')::fl, rels1 @ rels2 @ rels
 349          ) fl ([],[])
 350        in
 351         C.Fix (i, fl'),rels
 352     | C.CoFix (i, fl) ->
 353        let len = List.length fl in
 354        let fl',rels =
 355         List.fold_right
 356          (fun (name,ty,bo) (fl,rels) ->
 357            let ty',rels1 = aux k ty in
 358            let bo',rels2 = aux (k + len) bo in
 359             (name,ty',bo')::fl, rels1 @ rels2 @ rels
 360          ) fl ([],[])
 361        in
 362         C.CoFix (i, fl'),rels
 363   in
 364    fst (aux 0 t)
 365 ;;