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 (n,_) -> n=name | _ -> false) context
  55    in
  56     if name <> C.Anonymous && not (already_used name) then
  57      name
  58     else if not (already_used (C.Name basename)) then
  59      C.Name basename
  60     else
  61      let rec try_next n =
  62       let name' = C.Name (basename ^ string_of_int n) in
  63        if already_used name' then
  64         try_next (n+1)
  65        else
  66         name'
  67      in
  68       try_next 1
  69 ;;
  70
  71 (* clean_dummy_dependent_types term                             *)
  72 (* returns a copy of [term] where every dummy dependent product *)
  73 (* have been replaced with a non-dependent product and where    *)
  74 (* dummy let-ins have been removed.                             *)
  75 let clean_dummy_dependent_types t =
  76  let module C = Cic in
  77   let rec aux k =
  78    function
  79       C.Rel m as t -> t,[k - m]
  80     | C.Var (uri,exp_named_subst) ->
  81        let exp_named_subst',rels =
  82         List.fold_right
  83          (fun (uri,t) (exp_named_subst,rels) ->
  84            let t',rels' = aux k t in
  85             (uri,t')::exp_named_subst, rels' @ rels
  86          ) exp_named_subst ([],[])
  87        in
  88         C.Var (uri,exp_named_subst'),rels
  89     | C.Meta (i,l) ->
  90        let l',rels =
  91         List.fold_right
  92          (fun t (l,rels) ->
  93            let t',rels' =
  94             match t with
  95                None -> None,[]
  96              | Some t ->
  97                 let t',rels' = aux k t in
  98                  Some t', rels'
  99            in
 100             t'::l, rels' @ rels
 101          ) l ([],[])
 102        in
 103         C.Meta(i,l'),rels
 104     | C.Sort _ as t -> t,[]
 105     | C.Implicit _ as t -> t,[]
 106     | C.Cast (te,ty) ->
 107        let te',rels1 = aux k te in
 108        let ty',rels2 = aux k ty in
 109         C.Cast (te', ty'), rels1@rels2
 110     | C.Prod (n,s,t) ->
 111        let s',rels1 = aux k s in
 112        let t',rels2 = aux (k+1) t in
 113         let n' =
 114          match n with
 115             C.Anonymous ->
 116              if List.mem k rels2 then
 117 (
 118               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" ;
 119               C.Anonymous
 120 )
 121              else
 122               C.Anonymous
 123           | C.Name _ as n ->
 124              if List.mem k rels2 then n else C.Anonymous
 125         in
 126          C.Prod (n', s', t'), rels1@rels2
 127     | C.Lambda (n,s,t) ->
 128        let s',rels1 = aux k s in
 129        let t',rels2 = aux (k+1) t in
 130         C.Lambda (n, s', t'), rels1@rels2
 131     | C.LetIn (n,s,t) ->
 132        let s',rels1 = aux k s in
 133        let t',rels2 = aux (k+1) t in
 134        let rels = rels1 @ rels2 in
 135         if List.mem k rels2 then
 136          C.LetIn (n, s', t'), rels
 137         else
 138          (* (C.Rel 1) is just a dummy term; any term would fit *)
 139          CicSubstitution.subst (C.Rel 1) t', rels
 140     | C.Appl l ->
 141        let l',rels =
 142         List.fold_right
 143          (fun t (exp_named_subst,rels) ->
 144            let t',rels' = aux k t in
 145             t'::exp_named_subst, rels' @ rels
 146          ) l ([],[])
 147        in
 148         C.Appl l', rels
 149     | C.Const (uri,exp_named_subst) ->
 150        let exp_named_subst',rels =
 151         List.fold_right
 152          (fun (uri,t) (exp_named_subst,rels) ->
 153            let t',rels' = aux k t in
 154             (uri,t')::exp_named_subst, rels' @ rels
 155          ) exp_named_subst ([],[])
 156        in
 157         C.Const (uri,exp_named_subst'),rels
 158     | C.MutInd (uri,tyno,exp_named_subst) ->
 159        let exp_named_subst',rels =
 160         List.fold_right
 161          (fun (uri,t) (exp_named_subst,rels) ->
 162            let t',rels' = aux k t in
 163             (uri,t')::exp_named_subst, rels' @ rels
 164          ) exp_named_subst ([],[])
 165        in
 166         C.MutInd (uri,tyno,exp_named_subst'),rels
 167     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
 168        let exp_named_subst',rels =
 169         List.fold_right
 170          (fun (uri,t) (exp_named_subst,rels) ->
 171            let t',rels' = aux k t in
 172             (uri,t')::exp_named_subst, rels' @ rels
 173          ) exp_named_subst ([],[])
 174        in
 175         C.MutConstruct (uri,tyno,consno,exp_named_subst'),rels
 176     | C.MutCase (sp,i,outty,t,pl) ->
 177        let outty',rels1 = aux k outty in
 178        let t',rels2 = aux k t in
 179        let pl',rels3 =
 180         List.fold_right
 181          (fun t (exp_named_subst,rels) ->
 182            let t',rels' = aux k t in
 183             t'::exp_named_subst, rels' @ rels
 184          ) pl ([],[])
 185        in
 186         C.MutCase (sp, i, outty', t', pl'), rels1 @ rels2 @rels3
 187     | C.Fix (i, fl) ->
 188        let len = List.length fl in
 189        let fl',rels =
 190         List.fold_right
 191          (fun (name,i,ty,bo) (fl,rels) ->
 192            let ty',rels1 = aux k ty in
 193            let bo',rels2 = aux (k + len) bo in
 194             (name,i,ty',bo')::fl, rels1 @ rels2 @ rels
 195          ) fl ([],[])
 196        in
 197         C.Fix (i, fl'),rels
 198     | C.CoFix (i, fl) ->
 199        let len = List.length fl in
 200        let fl',rels =
 201         List.fold_right
 202          (fun (name,ty,bo) (fl,rels) ->
 203            let ty',rels1 = aux k ty in
 204            let bo',rels2 = aux (k + len) bo in
 205             (name,ty',bo')::fl, rels1 @ rels2 @ rels
 206          ) fl ([],[])
 207        in
 208         C.CoFix (i, fl'),rels
 209   in
 210    fst (aux 0 t)
 211 ;;