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