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;;