components/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 (* $Id$ *)
  27
  28 open Printf;;
  29
  30 type coercion_search_result =
  31      (* metasenv, last coercion argument, fully saturated coercion *)
  32      (* to apply the coercion it is sufficient to unify the last coercion
  33         argument (that is a Meta) with the term to be coerced *)
  34   | SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list
  35   | NoCoercion
  36   | NotMetaClosed
  37   | NotHandled of string Lazy.t
  38
  39 let debug = false
  40 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
  41
  42 (* searches a coercion fron src to tgt in the !coercions list *)
  43 let look_for_coercion' metasenv subst context src tgt =
  44   try
  45     let l =
  46       CoercDb.find_coercion
  47         (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) in
  48     let uri =
  49      match l with
  50      | [] ->
  51          debug_print
  52            (lazy
  53              (sprintf ":-( coercion non trovata da %s a %s"
  54                (CoercDb.name_of_carr src)
  55                (CoercDb.name_of_carr tgt)));
  56          None
  57      | _::_ ->
  58          debug_print (lazy (
  59            sprintf ":-) TROVATE %d coercion(s) da %s a %s"
  60              (List.length l)
  61              (CoercDb.name_of_carr src)
  62              (CoercDb.name_of_carr tgt)));
  63          Some l
  64     in
  65      (match uri with
  66          None -> NoCoercion
  67        | Some ul ->
  68           let cl = List.map CicUtil.term_of_uri ul in
  69           let funclass_arityl =
  70             let _,tgtcarl = List.split (List.map CoercDb.get_carr ul) in
  71             List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl
  72           in
  73           let freshmeta = CicMkImplicit.new_meta metasenv subst in
  74           let newtl =
  75            List.map2
  76             (fun arity c ->
  77               let ty,_ =
  78                CicTypeChecker.type_of_aux' ~subst metasenv context c
  79                 CicUniv.empty_ugraph in
  80               let _,metasenv,args,lastmeta =
  81                TermUtil.saturate_term freshmeta metasenv context ty arity in
  82               let irl =
  83                CicMkImplicit.identity_relocation_list_for_metavariable context
  84               in
  85                metasenv, Cic.Meta (lastmeta-1,irl),
  86                 match args with
  87                    [] -> c
  88                  | _ -> Cic.Appl (c::args)
  89             ) funclass_arityl cl
  90           in
  91            SomeCoercion newtl)
  92   with
  93     | CoercDb.EqCarrNotImplemented s -> NotHandled s
  94     | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
  95 ;;
  96
  97 let look_for_coercion metasenv subst context src tgt =
  98   let src_uri = CoercDb.coerc_carr_of_term src in
  99   let tgt_uri = CoercDb.coerc_carr_of_term tgt in
 100   look_for_coercion' metasenv subst context src_uri tgt_uri
 101
 102 let source_of t =
 103   try
 104     let uri = CicUtil.uri_of_term t in
 105     CoercDb.term_of_carr (fst (CoercDb.get_carr uri))
 106   with Invalid_argument _ -> assert false (* t must be a coercion *)
 107
 108 let generate_dot_file () =
 109   let module Pp = GraphvizPp.Dot in
 110   let buf = Buffer.create 10240 in
 111   let fmt = Format.formatter_of_buffer buf in
 112   Pp.header ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
 113     ~edge_attrs:["fontsize", "10"] fmt;
 114   let l = CoercDb.to_list () in
 115   let pp_description carr =
 116     match CoercDb.uri_of_carr carr with
 117     | None -> ()
 118     | Some uri ->
 119         Pp.node (CoercDb.name_of_carr carr)
 120           ~attrs:["href", UriManager.string_of_uri uri] fmt in
 121   List.iter
 122     (fun (src, tgt, cl) ->
 123       let src_name = CoercDb.name_of_carr src in
 124       let tgt_name = CoercDb.name_of_carr tgt in
 125       pp_description src;
 126       pp_description tgt;
 127       List.iter
 128         (fun c ->
 129           Pp.edge src_name tgt_name
 130             ~attrs:[ "label", UriManager.name_of_uri c;
 131               "href", UriManager.string_of_uri c ]
 132             fmt)
 133         cl)
 134     l;
 135   Pp.trailer fmt;
 136   Buffer.contents buf
 137 ;;
 138
 139 let is_composite t =
 140   try
 141     let uri =
 142       match t with
 143       | Cic.Appl (he::_) -> CicUtil.uri_of_term he
 144       | _ -> CicUtil.uri_of_term t
 145     in
 146     match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
 147     | Cic.Constant (_,_, _, _, attrs),_  ->
 148         List.exists (function `Class (`Coercion _) -> true | _ -> false) attrs
 149     | _ -> false
 150   with Invalid_argument _ -> false
 151 ;;
 152
 153 let uniq = HExtlib.list_uniq ~eq:(fun (a,_) (b,_) -> CoercDb.eq_carr a b);;
 154
 155 let splat e l = List.map (fun x -> e, x) l;;
 156
 157 let get_coercions_to carr =
 158   let l = CoercDb.to_list () in
 159   List.flatten
 160     (HExtlib.filter_map
 161       (fun (src,tgt,cl) ->
 162         if CoercDb.eq_carr tgt carr then Some (splat src cl) else None)
 163       l)
 164 ;;
 165
 166 let get_coercions_from carr =
 167   let l = CoercDb.to_list () in
 168   List.flatten
 169     (HExtlib.filter_map
 170       (fun (src,tgt,cl) ->
 171         if CoercDb.eq_carr src carr then Some (splat tgt cl) else None)
 172       l)
 173 ;;
 174
 175 let intersect l1 l2 =
 176   let is_in_l1 (x,_) = List.exists (fun (src,_) -> CoercDb.eq_carr x src) l1 in
 177   uniq (List.filter is_in_l1 l2)
 178 ;;
 179
 180 let grow s =
 181   uniq (List.flatten (List.map (fun (x,_) -> get_coercions_to x) s) @ s)
 182 ;;
 183
 184 let lb c =
 185   let l = get_coercions_from c in
 186   function x -> List.exists (fun (y,_) -> CoercDb.eq_carr x y) l
 187 ;;
 188
 189 let rec min acc = function
 190   | c::tl ->
 191     if List.exists (lb c) (tl@acc) then min acc tl else min (c::acc) tl
 192   | [] -> acc
 193 ;;
 194
 195 let meets left right =
 196   let u = UriManager.uri_of_string "cic:/foo.con" in
 197   min [] (List.map fst (intersect (grow [left,u]) (grow [right,u])))
 198 ;;
 199
 200 (* EOF *)