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