]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/library/cicFix.ml
...
[helm.git] / helm / software / components / library / cicFix.ml
1 (* Copyright (C) 2004-2005, 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://helm.cs.unibo.it/
24  *)
25
26 (* $Id: librarySync.ml 9482 2009-01-08 18:12:28Z tassi $ *)
27
28 let generate_sibling_mutual_definitions ~add_obj ~add_coercion uri obj =
29  match obj with
30  | Cic.Constant (name_to_avoid,Some bo,_,_,attrs) when
31    List.mem (`Flavour `MutualDefinition) attrs ->
32     (match bo with
33       Cic.Fix (_,funs) ->
34        snd (
35         List.fold_right
36          (fun (name,idx,ty,bo) (n,uris) ->
37            if name = name_to_avoid then
38             (n-1,uris)
39            else
40             let uri =
41              UriManager.uri_of_string
42               (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
43                 let bo = Cic.Fix (n-1,funs) in 
44             let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
45             let lemmas = add_obj uri obj in
46             (n-1,lemmas @ uri::uris))
47          (List.tl funs) (List.length funs,[]))
48     | Cic.CoFix (_,funs) ->
49        snd (
50         List.fold_right
51          (fun (name,ty,bo) (n,uris) ->
52            if name = name_to_avoid then
53             (n-1,uris)
54            else
55             let uri =
56              UriManager.uri_of_string
57               (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
58             let bo = Cic.CoFix (n-1,funs) in 
59             let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
60             let lemmas = add_obj uri obj in
61              (n-1,lemmas @ uri::uris)) 
62           (List.tl funs) (List.length funs,[]))
63     | _ -> assert false)
64   | _ -> []
65 ;;
66
67
68 let init () = 
69   LibrarySync.add_object_declaration_hook generate_sibling_mutual_definitions;;