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