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 = false
  29 let debug_print = if debug then prerr_endline else ignore
  30
  31 (* searches a coercion fron src to tgt in the !coercions list *)
  32 let look_for_coercion src tgt =
  33     try
  34       let src = UriManager.uri_of_string (CicUtil.uri_of_term src) in
  35       let tgt = UriManager.uri_of_string (CicUtil.uri_of_term tgt) in
  36       let l =
  37         CoercDb.find_coercion
  38           (fun (s,t) -> UriManager.eq s src && UriManager.eq t tgt)
  39       in
  40       match l with
  41       | [] -> prerr_endline ":( coercion non trovata"; None
  42       | u::_ ->
  43           debug_print (
  44             sprintf ":) TROVATE %d coercion(s) da %s a %s, prendo la prima: %s"
  45               (List.length l)
  46               (UriManager.name_of_uri src)
  47               (UriManager.name_of_uri tgt)
  48               (UriManager.name_of_uri u));
  49               Some (CicUtil.term_of_uri (UriManager.string_of_uri u))
  50     with Invalid_argument s ->
  51       debug_print (":( coercion non trovata (fallita la uri_of_term): " ^ s);
  52       None
  53 ;;
  54
  55 (* given the new coercion uri from src to tgt returns the list
  56  * of new coercions to create. hte list elements are
  57  * (source, list of coercions to follow, target)
  58  *)
  59 let get_closure_coercions src tgt uri coercions =
  60   let c_from_tgt = List.filter (fun (f,_,_) -> UriManager.eq f tgt) coercions in
  61   let c_to_src = List.filter (fun (_,t,_) -> UriManager.eq t src) coercions in
  62     (List.map (fun (_,t,u) -> src,[uri; u],t) c_from_tgt) @
  63     (List.map (fun (s,_,u) -> s,[u; uri],tgt) c_to_src) @
  64     (List.fold_left (
  65       fun l (s,_,u1) ->
  66         ((List.map (fun (_,t,u2) ->
  67           (s,[u1;uri;u2],t)
  68         )c_from_tgt)@l) )
  69     [] c_to_src)
  70 ;;
  71
  72 let obj_attrs = [`Class `Coercion; `Generated]
  73
  74 (* generate_composite_closure (c2 (c1 s)) in the universe graph univ *)
  75 let generate_composite_closure c1 c2 univ =
  76   let c1_ty,univ = CicTypeChecker.type_of_aux' [] [] c1 univ in
  77   let rec mk_rels n =
  78     match n with
  79     | 0 -> []
  80     | _ -> (Cic.Rel n) :: (mk_rels (n-1))
  81   in
  82   let rec compose k =
  83     function
  84     | Cic.Prod (name,src,tgt) ->
  85         let name =
  86           match name with
  87           | Cic.Anonymous -> Cic.Name "x"
  88           | _ -> name
  89         in
  90           Cic.Lambda (name,src,compose (k+1) tgt)
  91     | Cic.Appl (he::tl) ->
  92         Cic.Appl (c2 :: tl @ [Cic.Appl (c1 :: (mk_rels k)) ])
  93     | _ -> Cic.Appl (c2 :: [Cic.Appl (c1 :: (mk_rels k)) ])
  94   in
  95   let c = compose 0 c1_ty in
  96   let c_ty,univ =
  97     try
  98       CicTypeChecker.type_of_aux' [] [] c univ
  99     with CicTypeChecker.TypeCheckerFailure s as exn ->
 100       debug_print (sprintf "Generated composite coercion:\n%s\n%s"
 101         (CicPp.ppterm c) s);
 102       raise exn
 103   in
 104   let cleaned_ty =
 105     FreshNamesGenerator.clean_dummy_dependent_types c_ty
 106   in
 107   let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs) in
 108     obj,univ
 109 ;;
 110
 111 (* removes from l the coercions that are in !coercions *)
 112 let filter_duplicates l coercions =
 113   List.filter (
 114       fun (src,_,tgt) ->
 115         not (List.exists (fun (s,t,u) ->
 116           UriManager.eq s src &&
 117           UriManager.eq t tgt)
 118         coercions))
 119   l
 120
 121 (* given a new coercion uri from src to tgt returns
 122  * a list of (new coercion uri, coercion obj, universe graph)
 123  *)
 124 let close_coercion_graph src tgt uri =
 125   (* check if the coercion already exists *)
 126   let coercions = CoercDb.to_list () in
 127   let todo_list = get_closure_coercions src tgt uri coercions in
 128   let todo_list = filter_duplicates todo_list coercions in
 129   let new_coercions, new_coercions_obj =
 130     List.split (
 131       List.map (
 132         fun (src, l , tgt) ->
 133           match l with
 134           | [] -> assert false
 135           | he :: tl ->
 136               let term_of_uri' uri =
 137                 CicUtil.term_of_uri (UriManager.string_of_uri uri)
 138               in
 139               let first_step =
 140                 Cic.Constant ("", Some (term_of_uri' he), Cic.Sort Cic.Prop, [],
 141                   obj_attrs)
 142               in
 143               let o,u =
 144                 List.fold_left (fun (o,u) coer ->
 145                   match o with
 146                   | Cic.Constant (_,Some c,_,[],_) ->
 147                       generate_composite_closure c (term_of_uri' coer) u
 148                   | _ -> assert false
 149                 ) (first_step, CicUniv.empty_ugraph) tl
 150               in
 151               let name_src = UriManager.name_of_uri src in
 152               let name_tgt = UriManager.name_of_uri tgt in
 153               let name = name_tgt ^ "_of_" ^ name_src in
 154               let buri = UriManager.buri_of_uri uri in
 155               let c_uri =
 156                 UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con")
 157               in
 158               let named_obj =
 159                 match o with
 160                 | Cic.Constant (_,bo,ty,vl,attrs) ->
 161                     Cic.Constant (name,bo,ty,vl,attrs)
 162                 | _ -> assert false
 163               in
 164                 ((src,tgt,c_uri),(c_uri,named_obj,u))
 165       ) todo_list)
 166   in
 167   List.iter CoercDb.add_coercion (new_coercions @ [src,tgt,uri]);
 168   new_coercions_obj
 169 ;;
 170
 171 (* EOF *)