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_carr 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) ->
  95           CoercDb.eq_carr s src &&
  96           match t, tgt with
  97           | CoercDb.Sort Cic.Prop, CoercDb.Sort Cic.Prop
  98           | CoercDb.Sort Cic.Set, CoercDb.Sort Cic.Set
  99           | CoercDb.Sort _, CoercDb.Sort (Cic.Type _|Cic.CProp _) -> true
 100           | _ -> CoercDb.eq_carr t tgt)
 101     in
 102     pp_l "precise" l;
 103      (match l with
 104      | [] ->
 105          let l =
 106            CoercDb.find_coercion
 107              (fun (_,t) -> CoercDb.eq_carr t tgt)
 108          in
 109          pp_l "approx" l;
 110          (match l with
 111          | [] -> NoCoercion
 112          | ul ->
 113             SomeCoercionToTgt (saturate_coercion ul metasenv subst context))
 114      | ul -> SomeCoercion (saturate_coercion ul metasenv subst context))
 115 ;;
 116
 117 let rec count_pi c s t =
 118   match CicReduction.whd ~delta:false ~subst:s c t with
 119   | Cic.Prod (_,_,t) -> 1 + count_pi c s t
 120   | _ -> 0
 121 ;;
 122
 123 let look_for_coercion metasenv subst context src tgt =
 124   let src_arity = count_pi context subst src in
 125   let tgt_arity = count_pi context subst tgt in
 126   let src_carr = CoercDb.coerc_carr_of_term src src_arity in
 127   let tgt_carr = CoercDb.coerc_carr_of_term tgt tgt_arity in
 128   look_for_coercion_carr metasenv subst context src_carr tgt_carr
 129
 130 let source_of t =
 131   match CoercDb.is_a_coercion t with
 132   | None -> assert false
 133   | Some (CoercDb.Sort s,_,_,_,_) -> Cic.Sort s
 134   | Some (CoercDb.Uri u,_,_,_,_) -> CicUtil.term_of_uri u
 135   | Some _ -> assert false (* t must be a coercion not to funclass *)
 136 ;;
 137
 138 let generate_dot_file fmt =
 139   let l = CoercDb.to_list (CoercDb.dump ()) in
 140   let module Pp = GraphvizPp.Dot in
 141   if List.exists (fun (_,t,_) -> CoercDb.string_of_carr t = "Type") l then
 142     Format.fprintf fmt "subgraph cluster_rest { style=\"filled\";
 143     color=\"white\"; label=<%s>; labelloc=\"b\"; %s; }\n"
 144        ("<FONT POINT-SIZE=\"10.0\"><TABLE BORDER=\"1\" CELLBORDER=\"1\" >
 145          <TR><TD BGCOLOR=\"gray95\">Source</TD>
 146          <TD BGCOLOR=\"gray95\">Target</TD>
 147          <TD BGCOLOR=\"gray95\">Arrows</TD></TR>"^
 148        String.concat "</TR>"
 149          (List.map
 150            (fun (src,tgt,ul) ->
 151             let src_name = CoercDb.string_of_carr src in
 152             let tgt_name = CoercDb.string_of_carr tgt in
 153             let names =
 154               List.map (fun (u,_,_) ->
 155                 UriManager.name_of_uri u ^
 156                   (match CicEnvironment.get_obj CicUniv.empty_ugraph u with
 157                   | Cic.Constant (_,Some (Cic.Const (u',_)),_,_,attrs), _
 158                     when List.exists ((=) (`Flavour `Variant)) attrs -> "*"
 159                   | _ -> "")
 160               ) ul
 161             in
 162             "<TR><TD>"  ^ src_name ^ "</TD><TD>" ^ tgt_name ^ "</TD><TD>" ^
 163             String.concat ",&nbsp;" names ^ "</TD>")
 164          (List.sort (fun (x,y,_) (x1,y1,_) ->
 165              let rc = compare x x1 in
 166              if rc = 0 then compare y y1 else rc) l))
 167        ^ "</TR></TABLE></FONT>")
 168        (String.concat ";" ["Type"]);
 169   let type_uri u =
 170     let ty, _ =
 171       CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri u)
 172       CicUniv.oblivion_ugraph
 173     in
 174       ty
 175   in
 176   let deref_coercion u =
 177    match CicEnvironment.get_obj CicUniv.empty_ugraph u with
 178    | Cic.Constant (_,Some (Cic.Const (u',_)),_,_,attrs), _
 179      when List.exists ((=) (`Flavour `Variant)) attrs ->
 180        UriManager.name_of_uri u'
 181    | Cic.Constant (_,Some t,_,_,_), _ when
 182        let rec is_id = function
 183          | Cic.Lambda (_,_,t) -> is_id t
 184          | Cic.Rel _ -> true
 185          | _ -> false
 186          in is_id t -> "ID"
 187    | _ -> UriManager.name_of_uri u
 188   in
 189   List.iter
 190     (fun (src, tgt, ul) ->
 191       List.iter
 192         (fun (u,saturations,cpos) ->
 193           let ty = type_uri u in
 194           let src_name, tgt_name =
 195             let rec aux ctx cpos t =
 196               match cpos, t with
 197               | 0,Cic.Prod (_,src,tgt) ->
 198                   CicPp.pp src ctx, tgt, (Some (Cic.Name "_")::ctx)
 199               | 0,t -> CicPp.pp t ctx, Cic.Implicit None, []
 200               | n,Cic.Prod (_,_,tgt) -> aux (Some (Cic.Name "_")::ctx) (n-1) tgt
 201               | _ -> assert false
 202             in
 203             let ssrc, rest, ctx = aux [] cpos ty in
 204             let stgt, rest, _ = aux ctx saturations rest in
 205             let stgt =
 206               if rest <> Cic.Implicit None then
 207                 match tgt with
 208                 | CoercDb.Fun _ -> CoercDb.string_of_carr tgt
 209                 | _ -> assert false
 210               else
 211                 stgt
 212             in
 213             ssrc, stgt
 214           in
 215           Pp.node src_name fmt;
 216           Pp.node tgt_name fmt;
 217           Pp.edge src_name tgt_name
 218             ~attrs:[ "label",
 219                  (deref_coercion u ^
 220                   if saturations = 0 then ""
 221                   else "(" ^ string_of_int saturations ^ ")");
 222               "href", UriManager.string_of_uri u ]
 223             fmt)
 224         ul)
 225     l;
 226 ;;
 227
 228 let coerced_arg l =
 229   match l with
 230   | [] | [_] -> None
 231   | c::tl ->
 232      match CoercDb.is_a_coercion c with
 233      | None -> None
 234      | Some (_,_,_,_,cpos) ->
 235         if List.length tl > cpos then Some (List.nth tl cpos, cpos) else None
 236 ;;
 237
 238 (************************* meet calculation stuff ********************)
 239 let eq_uri_opt u1 u2 =
 240   match u1,u2 with
 241   | Some (u1,_), Some (u2,_) -> UriManager.eq u1 u2
 242   | None,Some _ | Some _, None -> false
 243   | None, None -> true
 244 ;;
 245
 246 let eq_carr_uri (c1,u1) (c2,u2) = CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2;;
 247
 248 let eq_carr_uri_uri (c1,u1,u11) (c2,u2,u22) =
 249   CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2 && eq_uri_opt u11 u22
 250 ;;
 251
 252 let uniq = HExtlib.list_uniq ~eq:eq_carr_uri;;
 253
 254 let uniq2 = HExtlib.list_uniq ~eq:eq_carr_uri_uri;;
 255
 256 let splat e l = List.map (fun (x1,x2,_) -> e, Some (x1,x2)) l;;
 257
 258 (* : carr -> (carr * uri option) where the option is always Some *)
 259 let get_coercions_to carr =
 260   let l = CoercDb.to_list (CoercDb.dump ()) in
 261   let splat_coercion_to carr (src,tgt,cl) =
 262     if CoercDb.eq_carr tgt carr then Some (splat src cl) else None
 263   in
 264   let l = List.flatten (HExtlib.filter_map (splat_coercion_to carr) l) in
 265   l
 266 ;;
 267
 268 (* : carr -> (carr * uri option) where the option is always Some *)
 269 let get_coercions_from carr =
 270   let l = CoercDb.to_list (CoercDb.dump ()) in
 271   let splat_coercion_from carr (src,tgt,cl) =
 272     if CoercDb.eq_carr src carr then Some (splat tgt cl) else None
 273   in
 274   List.flatten (HExtlib.filter_map (splat_coercion_from carr) l)
 275 ;;
 276
 277 (* intersect { (s1,u1) | u1:s1->t1 } { (s2,u2) | u2:s2->t2 }
 278  * gives the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } *)
 279 let intersect l1 l2 =
 280   let is_in_l1 (x,u2) =
 281     HExtlib.filter_map
 282       (fun (src,u1) ->
 283          if CoercDb.eq_carr x src then Some (src,u1,u2) else None)
 284     l1
 285   in
 286   uniq2 (List.flatten (List.map is_in_l1 l2))
 287 ;;
 288
 289 (* grow tgt gives all the (src,u) such that u:tgt->src *)
 290 let grow tgt =
 291   uniq ((tgt,None)::(get_coercions_to tgt))
 292 ;;
 293
 294 let lb (c,_,_) =
 295   let l = get_coercions_from c in
 296   fun (x,_,_) -> List.exists (fun (y,_) -> CoercDb.eq_carr x y) l
 297 ;;
 298
 299 (* given the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } removes the elements
 300  * (s,_,_) such that (s',_,_) is in the set and there exists a coercion s->s' *)
 301 let rec min acc skipped = function
 302   | c::tl ->
 303     if List.exists (lb c) (tl@acc)
 304     then min acc (c::skipped) tl else min (c::acc) skipped tl
 305   | [] -> acc, skipped
 306 ;;
 307
 308
 309 let sort l =
 310   let low, high = min [] [] l in low @ high
 311 ;;
 312
 313 let meets metasenv subst context (grow_left,left) (grow_right,right) =
 314   let saturate metasenv uo =
 315     match uo with
 316     | None -> metasenv, None
 317     | Some u ->
 318         match saturate_coercion [u] metasenv subst context with
 319         | [metasenv, sat, last] -> metasenv, Some (sat, last)
 320         | _ -> assert false
 321   in
 322   List.map
 323     (fun (c,uo1,uo2) ->
 324       let metasenv, uo1 = saturate metasenv uo1 in
 325       let metasenv, uo2 = saturate metasenv uo2 in
 326       c,metasenv, uo1, uo2)
 327     (sort (intersect
 328       (if grow_left then grow left else [left,None])
 329       (if grow_right then grow right else [right,None])))
 330 ;;
 331
 332 (* EOF *)