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