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   | SomeCoercionToTgt of (Cic.metasenv * Cic.term * Cic.term) list
  36   | NoCoercion
  37   | NotMetaClosed
  38   | NotHandled of string Lazy.t
  39
  40 let debug = false
  41 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
  42
  43 let saturate_coercion ul metasenv subst context =
  44   let cl =
  45    List.map (fun u,saturations -> CicUtil.term_of_uri u,saturations) ul in
  46   let funclass_arityl =
  47     let _,tgtcarl = List.split (List.map (fun u,_ -> CoercDb.get_carr u) ul) in
  48     List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl
  49   in
  50   let freshmeta = CicMkImplicit.new_meta metasenv subst in
  51    List.map2
  52     (fun arity (c,saturations) ->
  53       let ty,_ =
  54        CicTypeChecker.type_of_aux' ~subst metasenv context c
  55         CicUniv.oblivion_ugraph in
  56       let _,metasenv,args,lastmeta =
  57        TermUtil.saturate_term ~delta:false freshmeta metasenv context ty arity in
  58       let irl =
  59        CicMkImplicit.identity_relocation_list_for_metavariable context
  60       in
  61        metasenv, Cic.Meta (lastmeta - saturations - 1,irl),
  62         match args with
  63            [] -> c
  64          | _ -> Cic.Appl (c::args)
  65     ) funclass_arityl cl
  66 ;;
  67
  68 (* searches a coercion fron src to tgt in the !coercions list *)
  69 let look_for_coercion' metasenv subst context src tgt =
  70   let pp_l s l =
  71    match l with
  72    | [] ->
  73        debug_print
  74          (lazy
  75          (sprintf ":-( coercion non trovata[%s] da %s a %s" s
  76              (CoercDb.name_of_carr src)
  77              (CoercDb.name_of_carr tgt)));
  78    | _::_ ->
  79        debug_print (lazy (
  80                sprintf ":-) TROVATE[%s] %d coercion(s) da %s a %s" s
  81            (List.length l)
  82            (CoercDb.name_of_carr src)
  83            (CoercDb.name_of_carr tgt)));
  84   in
  85   try
  86     let l =
  87       CoercDb.find_coercion
  88         (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt)
  89     in
  90     pp_l "precise" l;
  91      (match l with
  92      | [] ->
  93          let l =
  94            CoercDb.find_coercion
  95              (fun (_,t) -> CoercDb.eq_carr t tgt)
  96          in
  97          pp_l "approx" l;
  98          (match l with
  99          | [] -> NoCoercion
 100          | ul -> SomeCoercionToTgt (saturate_coercion ul metasenv subst context))
 101      | ul -> SomeCoercion (saturate_coercion ul metasenv subst context))
 102   with
 103     | CoercDb.EqCarrNotImplemented s -> NotHandled s
 104     | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
 105 ;;
 106
 107 let look_for_coercion metasenv subst context src tgt =
 108   let src_uri = CoercDb.coerc_carr_of_term src in
 109   let tgt_uri = CoercDb.coerc_carr_of_term tgt in
 110   look_for_coercion' metasenv subst context src_uri tgt_uri
 111
 112 let source_of t =
 113   try
 114     let uri = CicUtil.uri_of_term t in
 115     CoercDb.term_of_carr (fst (CoercDb.get_carr uri))
 116   with Invalid_argument _ -> assert false (* t must be a coercion *)
 117
 118 let generate_dot_file () =
 119   let module Pp = GraphvizPp.Dot in
 120   let buf = Buffer.create 10240 in
 121   let fmt = Format.formatter_of_buffer buf in
 122   Pp.header ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
 123     ~edge_attrs:["fontsize", "10"] fmt;
 124   let l = CoercDb.to_list () in
 125   let pp_description carr =
 126     match CoercDb.uri_of_carr carr with
 127     | None -> ()
 128     | Some uri ->
 129         Pp.node (CoercDb.name_of_carr carr)
 130           ~attrs:["href", UriManager.string_of_uri uri] fmt in
 131   List.iter
 132     (fun (src, tgt, ul) ->
 133       let src_name = CoercDb.name_of_carr src in
 134       let tgt_name = CoercDb.name_of_carr tgt in
 135       pp_description src;
 136       pp_description tgt;
 137       List.iter
 138         (fun (u,saturations) ->
 139           Pp.edge src_name tgt_name
 140             ~attrs:[ "label",
 141                      (UriManager.name_of_uri u ^
 142                       if saturations = 0 then
 143                        ""
 144                       else
 145                        "(" ^ string_of_int saturations ^ ")");
 146               "href", UriManager.string_of_uri u ]
 147             fmt)
 148         ul)
 149     l;
 150   Pp.trailer fmt;
 151   Buffer.contents buf
 152 ;;
 153
 154 let is_composite t =
 155   try
 156     let uri =
 157       match t with
 158       | Cic.Appl (he::_) -> CicUtil.uri_of_term he
 159       | _ -> CicUtil.uri_of_term t
 160     in
 161     match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with
 162     | Cic.Constant (_,_, _, _, attrs),_  ->
 163         List.exists (function `Class (`Coercion _) -> true | _ -> false) attrs
 164     | _ -> false
 165   with Invalid_argument _ -> false
 166 ;;
 167
 168 let coerced_arg l =
 169   match l with
 170   | [] | [_] -> assert false
 171   | c::_ when not (CoercDb.is_a_coercion' c) -> assert false
 172   | c::tl ->
 173      let arity =
 174        match CoercDb.is_a_coercion_to_funclass c with None -> 0 | Some a -> a
 175     in
 176     (* decide a decent structure for coercion carriers so that all this stuff is
 177      * useless *)
 178     let pi =
 179       (* this calculation is not complete, since we have strange carriers *)
 180       let rec count_pi = function
 181         | Cic.Prod(_,_,t) -> 1+ (count_pi t)
 182         | _ -> 0
 183       in
 184       let uri = CicUtil.uri_of_term c in
 185       match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 186       | Cic.Constant (_, _, ty, _, _) -> count_pi ty
 187       | _ -> assert false
 188     in
 189     try Some (List.nth tl (pi - arity)) with Invalid_argument _ -> None
 190 ;;
 191
 192 (************************* meet calculation stuff ********************)
 193 let eq_uri_opt u1 u2 =
 194   match u1,u2 with
 195   | Some (u1,_), Some (u2,_) -> UriManager.eq u1 u2
 196   | None,Some _ | Some _, None -> false
 197   | None, None -> true
 198 ;;
 199
 200 let eq_carr_uri (c1,u1) (c2,u2) = CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2;;
 201
 202 let eq_carr_uri_uri (c1,u1,u11) (c2,u2,u22) =
 203   CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2 && eq_uri_opt u11 u22
 204 ;;
 205
 206 let uniq = HExtlib.list_uniq ~eq:eq_carr_uri;;
 207
 208 let uniq2 = HExtlib.list_uniq ~eq:eq_carr_uri_uri;;
 209
 210 let splat e l = List.map (fun x -> e, Some x) l;;
 211
 212 (* : carr -> (carr * uri option) where the option is always Some *)
 213 let get_coercions_to carr =
 214   let l = CoercDb.to_list () in
 215   let splat_coercion_to carr (src,tgt,cl) =
 216     if CoercDb.eq_carr tgt carr then Some (splat src cl) else None
 217   in
 218   let l = List.flatten (HExtlib.filter_map (splat_coercion_to carr) l) in
 219   l
 220 ;;
 221
 222 (* : carr -> (carr * uri option) where the option is always Some *)
 223 let get_coercions_from carr =
 224   let l = CoercDb.to_list () in
 225   let splat_coercion_from carr (src,tgt,cl) =
 226     if CoercDb.eq_carr src carr then Some (splat tgt cl) else None
 227   in
 228   List.flatten (HExtlib.filter_map (splat_coercion_from carr) l)
 229 ;;
 230
 231 (* intersect { (s1,u1) | u1:s1->t1 } { (s2,u2) | u2:s2->t2 }
 232  * gives the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } *)
 233 let intersect l1 l2 =
 234   let is_in_l1 (x,u2) =
 235     HExtlib.filter_map
 236       (fun (src,u1) ->
 237          if CoercDb.eq_carr x src then Some (src,u1,u2) else None)
 238     l1
 239   in
 240   uniq2 (List.flatten (List.map is_in_l1 l2))
 241 ;;
 242
 243 (* grow tgt gives all the (src,u) such that u:tgt->src *)
 244 let grow tgt =
 245   uniq ((tgt,None)::(get_coercions_to tgt))
 246 ;;
 247
 248 let lb (c,_,_) =
 249   let l = get_coercions_from c in
 250   fun (x,_,_) -> List.exists (fun (y,_) -> CoercDb.eq_carr x y) l
 251 ;;
 252
 253 (* given the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } removes the elements
 254  * (s,_,_) such that (s',_,_) is in the set and there exists a coercion s->s' *)
 255 let rec min acc = function
 256   | c::tl ->
 257     if List.exists (lb c) (tl@acc) then min acc tl else min (c::acc) tl
 258   | [] -> acc
 259 ;;
 260
 261 let meets metasenv subst context left right =
 262   let saturate metasenv uo =
 263     match uo with
 264     | None -> metasenv, None
 265     | Some u ->
 266         match saturate_coercion [u] metasenv subst context with
 267         | [metasenv, sat, last] -> metasenv, Some (sat, last)
 268         | _ -> assert false
 269   in
 270   List.map
 271     (fun (c,uo1,uo2) ->
 272       let metasenv, uo1 = saturate metasenv uo1 in
 273       let metasenv, uo2 = saturate metasenv uo2 in
 274       c,metasenv, uo1, uo2)
 275     (min [] (intersect (grow left) (grow right)))
 276 ;;
 277
 278 (* EOF *)