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