helm/ocaml/cic_unification/coercGraph.ml

   1 (* Copyright (C) 2000, 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 open Printf;;
  27
  28 ignore(Helm_registry.load_from "/home/tassi/helm/gTopLevel/gTopLevel.conf.xml")
  29
  30 (* the list of known coercions (MUST be transitively closed) *)
  31 let coercions = ref [
  32   (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)",
  33    UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con",
  34    UriManager.uri_of_string "cic://Coq/Reals/Raxioms/INR.con") ;
  35
  36    (
  37      UriManager.uri_of_string "cic:/CoRN/algebra/CFields/CField.ind#xpointer(1/1)",
  38      UriManager.uri_of_string "cic:/CoRN/algebra/CRings/CRing.ind#xpointer(1/1)",
  39      UriManager.uri_of_string "cic:/CoRN/algebra/CFields/cf_crr.con"
  40
  41     );
  42     (
  43      UriManager.uri_of_string "cic:/CoRN/algebra/CAbGroups/CAbGroup.ind#xpointer(1/1)",
  44      UriManager.uri_of_string "cic:/CoRN/algebra/CGroups/CGroup.ind#xpointer(1/1)",
  45      UriManager.uri_of_string "cic:/CoRN/algebra/CAbGroups/cag_crr.con"
  46
  47     );
  48
  49 ]
  50 ;;
  51
  52 (* searches a coercion fron src to tgt in the !coercions list *)
  53 let look_for_coercion src tgt =
  54   try
  55     let s,t,u =
  56       List.find (fun (s,t,_) ->
  57         UriManager.eq s src &&
  58         UriManager.eq t tgt)
  59       !coercions
  60     in
  61     prerr_endline (sprintf ":) TROVATA la coercion %s %s"
  62       (UriManager.name_of_uri src)
  63       (UriManager.name_of_uri tgt));
  64     Some (CicUtil.term_of_uri (UriManager.string_of_uri u))
  65   with
  66     Not_found ->
  67       prerr_endline (sprintf ":( NON TROVATA la coercion %s %s"
  68         (UriManager.name_of_uri src) (UriManager.name_of_uri tgt));
  69       None
  70 ;;
  71
  72 (* given the new coercion uri from src to tgt returns the list
  73  * of new coercions to create. hte list elements are
  74  * (source, list of coercions to follow, target)
  75  *)
  76 let get_closure_coercions src tgt uri =
  77   let c_from_tgt =
  78     List.filter (fun (f,_,_) ->
  79       UriManager.eq f tgt)
  80     !coercions
  81   in
  82   let c_to_src =
  83     List.filter (fun (_,t,_) ->
  84       UriManager.eq t src)
  85     !coercions
  86   in
  87     (List.map (fun (_,t,u) -> src,[uri; u],t) c_from_tgt) @
  88     (List.map (fun (s,_,u) -> s,[u; uri],tgt) c_to_src) @
  89     (List.fold_left (
  90       fun l (s,_,u1) ->
  91         ((List.map (fun (_,t,u2) ->
  92           (s,[u1;uri;u2],t)
  93         )c_from_tgt)@l) )
  94     [] c_to_src)
  95 ;;
  96
  97
  98
  99 (* generate_composite_closure (c2 (c1 s)) in the universe graph univ *)
 100 let generate_composite_closure c1 c2 univ =
 101   let c1_ty,univ = CicTypeChecker.type_of_aux' [] [] c1 univ in
 102   let rec mk_rels n =
 103     match n with
 104     | 0 -> []
 105     | _ -> (Cic.Rel n) :: (mk_rels (n-1))
 106   in
 107   let rec compose k =
 108     function
 109     | Cic.Prod (name,src,tgt) ->
 110         let name =
 111           match name with
 112           | Cic.Anonymous -> Cic.Name "x"
 113           | _ -> name
 114         in
 115           Cic.Lambda (name,src,compose (k+1) tgt)
 116     | Cic.Appl (he::tl) ->
 117         Cic.Appl (c2 :: tl @ [Cic.Appl (c1 :: (mk_rels k)) ])
 118     | _ -> Cic.Appl (c2 :: [Cic.Appl (c1 :: (mk_rels k)) ])
 119   in
 120   let c = compose 0 c1_ty in
 121   let c_ty,univ =
 122     try
 123       CicTypeChecker.type_of_aux' [] [] c univ
 124     with CicTypeChecker.TypeCheckerFailure s as exn ->
 125       prerr_endline (sprintf "Generated composite coercion:\n%s\n%s"
 126         (CicPp.ppterm c) s);
 127       raise exn
 128   in
 129   let cleaned_ty =
 130     FreshNamesGenerator.clean_dummy_dependent_types c_ty
 131   in
 132   let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[]) in
 133     obj,univ
 134 ;;
 135
 136 (* removes from l the coercions that are in !coercions *)
 137 let filter_duplicates l =
 138   List.filter (
 139       fun (src,_,tgt) ->
 140         not (List.exists (fun (s,t,u) ->
 141           UriManager.eq s src &&
 142           UriManager.eq t tgt)
 143         !coercions))
 144   l
 145
 146 (* given a new coercion uri from src to tgt returns
 147  * a list of (new coercion uri, coercion obj, universe graph)
 148  *)
 149 let close_coercion_graph src tgt uri =
 150   (* check if the coercion already exists *)
 151   let todo_list = get_closure_coercions src tgt uri in
 152   let todo_list = filter_duplicates todo_list in
 153   let new_coercions, new_coercions_obj =
 154     List.split (
 155       List.map (
 156         fun (src, l , tgt) ->
 157           match l with
 158           | [] -> assert false
 159           | he :: tl ->
 160               let term_of_uri' uri =
 161                 CicUtil.term_of_uri (UriManager.string_of_uri uri)
 162               in
 163               let first_step =
 164                 (Cic.Constant ("",Some (term_of_uri' he),Cic.Sort Cic.Prop,[]))
 165               in
 166               let o,u =
 167                 List.fold_left (fun (o,u) coer ->
 168                   match o with
 169                   |  Cic.Constant (_,Some c,_,[]) ->
 170                     generate_composite_closure c (term_of_uri' coer) u
 171                   | _ -> assert false
 172                 ) (first_step, CicUniv.empty_ugraph) tl
 173               in
 174               let name_src = UriManager.name_of_uri src in
 175               let name_tgt = UriManager.name_of_uri tgt in
 176               let name = name_tgt ^ "_of_" ^ name_src in
 177               let buri = UriManager.buri_of_uri uri in
 178               let c_uri =
 179                 UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con")
 180               in
 181               let named_obj =
 182                 match o with
 183                 | Cic.Constant (_,bo,ty,vl) -> Cic.Constant (name,bo,ty,vl)
 184                 | _ -> assert false
 185               in
 186                 ((src,tgt,c_uri),(c_uri,named_obj,u))
 187       ) todo_list)
 188   in
 189   coercions := !coercions @ new_coercions;
 190   new_coercions_obj
 191 ;;
 192
 193
 194
 195
 196 (* stupid case *)
 197
 198 let l = close_coercion_graph
 199  (UriManager.uri_of_string
 200  "cic:/CoRN/algebra/CRings/CRing.ind#xpointer(1/1)")
 201  (UriManager.uri_of_string
 202  "cic:/CoRN/algebra/CAbGroups/CAbGroup.ind#xpointer(1/1)")
 203  (UriManager.uri_of_string
 204  "cic:/CoRN/algebra/CRings/cr_crr.con")
 205 in
 206  List.iter (fun (u,o,g) ->
 207    prerr_endline (CicPp.ppobj o);
 208    prerr_endline (UriManager.string_of_uri u);
 209    prerr_endline "")
 210  l
 211
 212
 213
 214 (* EOF *)