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