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