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