helm/ocaml/cic_unification/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 (* mk_fresh_name context name typ                      *)
  27 (* returns an identifier which is fresh in the context *)
  28 (* and that resembles [name] as much as possible.      *)
  29 (* [typ] will be the type of the variable              *)
  30 let mk_fresh_name ~subst metasenv context name ~typ =
  31  let module C = Cic in
  32   let basename =
  33    match name with
  34       C.Anonymous ->
  35        (*CSC: great space for improvements here *)
  36        (try
  37         let ty,_ =
  38           CicTypeChecker.type_of_aux' ~subst metasenv context typ
  39             CicUniv.empty_ugraph in
  40          (match ty with
  41              C.Sort C.Prop
  42            | C.Sort C.CProp -> "H"
  43            | C.Sort C.Set -> "x"
  44            | _ -> "H"
  45          )
  46         with CicTypeChecker.TypeCheckerFailure _ -> "H"
  47        )
  48     | C.Name name ->
  49        Str.global_replace (Str.regexp "[0-9]*$") "" name
  50   in
  51    let already_used name =
  52     List.exists (function Some (C.Name n,_) -> n=name | _ -> false) context
  53    in
  54     if not (already_used basename) then
  55      C.Name basename
  56     else
  57      let rec try_next n =
  58       let name' = basename ^ string_of_int n in
  59        if already_used name' then
  60         try_next (n+1)
  61        else
  62         C.Name name'
  63      in
  64       try_next 1
  65 ;;
  66
  67 (* clean_dummy_dependent_types term                             *)
  68 (* returns a copy of [term] where every dummy dependent product *)
  69 (* have been replaced with a non-dependent product and where    *)
  70 (* dummy let-ins have been removed.                             *)
  71 let clean_dummy_dependent_types t =
  72  let module C = Cic in
  73   let rec aux k =
  74    function
  75       C.Rel m as t -> t,[k - m]
  76     | C.Var (uri,exp_named_subst) ->
  77        let exp_named_subst',rels =
  78         List.fold_right
  79          (fun (uri,t) (exp_named_subst,rels) ->
  80            let t',rels' = aux k t in
  81             (uri,t')::exp_named_subst, rels' @ rels
  82          ) exp_named_subst ([],[])
  83        in
  84         C.Var (uri,exp_named_subst'),rels
  85     | C.Meta (i,l) ->
  86        let l',rels =
  87         List.fold_right
  88          (fun t (l,rels) ->
  89            let t',rels' =
  90             match t with
  91                None -> None,[]
  92              | Some t ->
  93                 let t',rels' = aux k t in
  94                  Some t', rels'
  95            in
  96             t'::l, rels' @ rels
  97          ) l ([],[])
  98        in
  99         C.Meta(i,l'),rels
 100     | C.Sort _ as t -> t,[]
 101     | C.Implicit _ as t -> t,[]
 102     | C.Cast (te,ty) ->
 103        let te',rels1 = aux k te in
 104        let ty',rels2 = aux k ty in
 105         C.Cast (te', ty'), rels1@rels2
 106     | C.Prod (n,s,t) ->
 107        let s',rels1 = aux k s in
 108        let t',rels2 = aux (k+1) t in
 109         let n' =
 110          match n with
 111             C.Anonymous ->
 112              if List.mem k rels2 then
 113 (
 114               prerr_endline "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" ;
 115               C.Anonymous
 116 )
 117              else
 118               C.Anonymous
 119           | C.Name _ as n ->
 120              if List.mem k rels2 then n else C.Anonymous
 121         in
 122          C.Prod (n', s', t'), rels1@rels2
 123     | C.Lambda (n,s,t) ->
 124        let s',rels1 = aux k s in
 125        let t',rels2 = aux (k+1) t in
 126         C.Lambda (n, s', t'), rels1@rels2
 127     | C.LetIn (n,s,t) ->
 128        let s',rels1 = aux k s in
 129        let t',rels2 = aux (k+1) t in
 130        let rels = rels1 @ rels2 in
 131         if List.mem k rels2 then
 132          C.LetIn (n, s', t'), rels
 133         else
 134          (* (C.Rel 1) is just a dummy term; any term would fit *)
 135          CicSubstitution.subst (C.Rel 1) t', rels
 136     | C.Appl l ->
 137        let l',rels =
 138         List.fold_right
 139          (fun t (exp_named_subst,rels) ->
 140            let t',rels' = aux k t in
 141             t'::exp_named_subst, rels' @ rels
 142          ) l ([],[])
 143        in
 144         C.Appl l', rels
 145     | C.Const (uri,exp_named_subst) ->
 146        let exp_named_subst',rels =
 147         List.fold_right
 148          (fun (uri,t) (exp_named_subst,rels) ->
 149            let t',rels' = aux k t in
 150             (uri,t')::exp_named_subst, rels' @ rels
 151          ) exp_named_subst ([],[])
 152        in
 153         C.Const (uri,exp_named_subst'),rels
 154     | C.MutInd (uri,tyno,exp_named_subst) ->
 155        let exp_named_subst',rels =
 156         List.fold_right
 157          (fun (uri,t) (exp_named_subst,rels) ->
 158            let t',rels' = aux k t in
 159             (uri,t')::exp_named_subst, rels' @ rels
 160          ) exp_named_subst ([],[])
 161        in
 162         C.MutInd (uri,tyno,exp_named_subst'),rels
 163     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
 164        let exp_named_subst',rels =
 165         List.fold_right
 166          (fun (uri,t) (exp_named_subst,rels) ->
 167            let t',rels' = aux k t in
 168             (uri,t')::exp_named_subst, rels' @ rels
 169          ) exp_named_subst ([],[])
 170        in
 171         C.MutConstruct (uri,tyno,consno,exp_named_subst'),rels
 172     | C.MutCase (sp,i,outty,t,pl) ->
 173        let outty',rels1 = aux k outty in
 174        let t',rels2 = aux k t in
 175        let pl',rels3 =
 176         List.fold_right
 177          (fun t (exp_named_subst,rels) ->
 178            let t',rels' = aux k t in
 179             t'::exp_named_subst, rels' @ rels
 180          ) pl ([],[])
 181        in
 182         C.MutCase (sp, i, outty', t', pl'), rels1 @ rels2 @rels3
 183     | C.Fix (i, fl) ->
 184        let len = List.length fl in
 185        let fl',rels =
 186         List.fold_right
 187          (fun (name,i,ty,bo) (fl,rels) ->
 188            let ty',rels1 = aux k ty in
 189            let bo',rels2 = aux (k + len) bo in
 190             (name,i,ty',bo')::fl, rels1 @ rels2 @ rels
 191          ) fl ([],[])
 192        in
 193         C.Fix (i, fl'),rels
 194     | C.CoFix (i, fl) ->
 195        let len = List.length fl in
 196        let fl',rels =
 197         List.fold_right
 198          (fun (name,ty,bo) (fl,rels) ->
 199            let ty',rels1 = aux k ty in
 200            let bo',rels2 = aux (k + len) bo in
 201             (name,ty',bo')::fl, rels1 @ rels2 @ rels
 202          ) fl ([],[])
 203        in
 204         C.CoFix (i, fl'),rels
 205   in
 206    fst (aux 0 t)
 207 ;;