helm/software/components/ng_refiner/nCicCoercion.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *)
  13
  14 let debug s = prerr_endline (Lazy.force s);;
  15 let debug _ = ();;
  16
  17 module COT : Set.OrderedType with type t = NCic.term * int * int  * NCic.term *
  18 NCic.term =
  19   struct
  20         type t = NCic.term * int * int * NCic.term * NCic.term
  21         let compare = Pervasives.compare
  22   end
  23
  24 module CoercionSet = Set.Make(COT)
  25
  26 module DB =
  27   Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(CoercionSet)
  28
  29 type db = DB.t * DB.t
  30
  31 let empty_db = DB.empty,DB.empty
  32
  33 class status =
  34  object
  35   inherit NCicUnifHint.status
  36   val db = empty_db
  37   method coerc_db = db
  38   method set_coerc_db v = {< db = v >}
  39   method set_coercion_status
  40   : 'status. < coerc_db : db; uhint_db: NCicUnifHint.db; .. > as 'status ->
  41           'self
  42           = fun o -> {< db = o#coerc_db >}#set_unifhint_status o
  43  end
  44
  45 let index_coercion status c src tgt arity arg =
  46   let db_src,db_tgt = status#coerc_db in
  47   let data = (c,arity,arg,src,tgt) in
  48
  49   let debug s = prerr_endline (Lazy.force s) in
  50   debug (lazy ("INDEX:" ^
  51     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
  52     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ "  :=  " ^
  53     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c ^ " " ^
  54     string_of_int arg ^ " " ^ string_of_int arity));
  55
  56   let db_src = DB.index db_src src data in
  57   let db_tgt = DB.index db_tgt tgt data in
  58   status#set_coerc_db (db_src, db_tgt)
  59 ;;
  60
  61 let index_old_db odb (status : #status) =
  62   List.fold_left
  63     (fun status (_,tgt,clist) ->
  64        List.fold_left
  65          (fun status (uri,_,arg) ->
  66            try
  67             let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in
  68             let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in
  69             let src, tgt =
  70               let cty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] c in
  71               let scty, metasenv,_ =
  72                 NCicMetaSubst.saturate ~delta:max_int [] [] [] cty (arity+1)
  73               in
  74               match scty with
  75               | NCic.Prod (_, src, tgt) ->
  76                  let tgt =
  77                    NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt
  78                  in
  79 (*
  80             debug (lazy (Printf.sprintf "indicizzo %s (%d)) : %s ===> %s"
  81               (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] scty) (arity+1)
  82               (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] src)
  83               (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] tgt));
  84 *)
  85                 src, tgt
  86               | t ->
  87                   debug (lazy (
  88                     NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t));
  89                   assert false
  90             in
  91             index_coercion status c src tgt arity arg
  92            with
  93            | NCicEnvironment.BadDependency _
  94            | NCicTypeChecker.TypeCheckerFailure _ -> status)
  95          status clist)
  96     status (CoercDb.to_list odb)
  97 ;;
  98
  99 let look_for_coercion status metasenv subst context infty expty =
 100  let db_src,db_tgt = status#coerc_db in
 101   match infty, expty with
 102   | (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)),
 103     (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> []
 104   | _ ->
 105
 106     debug (lazy ("LOOK FOR COERCIONS: " ^
 107       NCicPp.ppterm ~metasenv ~subst ~context infty ^ "  |===> " ^
 108       NCicPp.ppterm ~metasenv ~subst ~context expty));
 109
 110     let src_class = infty :: NCicUnifHint.eq_class_of status infty in
 111     let tgt_class = expty :: NCicUnifHint.eq_class_of status expty in
 112
 113     let set_src =
 114       List.fold_left
 115         (fun set infty ->
 116           CoercionSet.union (DB.retrieve_unifiables db_src infty) set)
 117         CoercionSet.empty src_class
 118     in
 119     let set_tgt =
 120       List.fold_left
 121         (fun set expty ->
 122           CoercionSet.union (DB.retrieve_unifiables db_tgt expty) set)
 123         CoercionSet.empty tgt_class
 124     in
 125     let candidates = CoercionSet.inter set_src set_tgt in
 126
 127     debug (lazy ("CANDIDATES: " ^
 128       String.concat "," (List.map (fun (t,_,_,_,_) ->
 129         NCicPp.ppterm ~metasenv ~subst ~context t)
 130       (CoercionSet.elements candidates))));
 131
 132     List.map
 133       (fun (t,arity,arg,_,_) ->
 134           let ty =
 135             try NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t
 136             with NCicTypeChecker.TypeCheckerFailure s ->
 137              prerr_endline ("illtyped coercion: "^Lazy.force s);
 138              prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
 139              assert false
 140           in
 141           let ty, metasenv, args =
 142            NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity
 143           in
 144
 145           debug (lazy (
 146             NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^
 147             NCicPp.ppterm ~metasenv ~subst ~context
 148             (NCicUntrusted.mk_appl t args) ^ " --- " ^
 149               string_of_int (List.length args) ^ " == " ^ string_of_int arg));
 150
 151           metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
 152       (CoercionSet.elements candidates)
 153 ;;
 154
 155 (* CSC: very inefficient implementation!
 156    Enrico, can we use a discrimination tree here? *)
 157 let match_coercion status ~metasenv ~subst ~context t =
 158  let db =
 159   DB.fold (fst (status#coerc_db)) (fun _ v l -> (CoercionSet.elements v)@l) []
 160  in
 161     (HExtlib.list_findopt
 162       (fun (p,arity,cpos,_,_) _ ->
 163         try
 164          let t =
 165           match p,t with
 166              NCic.Appl lp, NCic.Appl lt ->
 167               (match fst (HExtlib.split_nth (List.length lp) lt) with
 168                   [t] -> t
 169                 | l -> NCic.Appl l)
 170            | _,NCic.Appl (he::_) -> he
 171            | _,_ -> t
 172          in
 173          let b = NCicReduction.alpha_eq metasenv subst context p t in
 174          if not b then None else
 175          let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] p in
 176          let pis =
 177            let rec aux = function NCic.Prod (_,_,t) -> 1+aux t | _ -> 0 in
 178            aux ty
 179          in
 180          Some (p,pis - arity - cpos - 1,cpos)
 181         with
 182          Failure _ -> None (* raised by split_nth *)
 183       ) db)
 184 ;;
 185
 186 let generate_dot_file status =
 187   let module Pp = GraphvizPp.Dot in
 188   let buf = Buffer.create 10240 in
 189   let fmt = Format.formatter_of_buffer buf in
 190   Pp.header ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
 191     ~edge_attrs:["fontsize", "10"] fmt;
 192   let src_db, _ = status#coerc_db in
 193   let edges = ref [] in
 194   DB.iter src_db (fun _ dataset ->
 195      edges := !edges @
 196       List.map
 197         (fun (t,a,g,sk,dk) ->
 198                 prerr_endline (let p = NCicPp.ppterm ~metasenv:[] ~context:[]
 199                 ~subst:[] in p t ^ " ::: " ^ p sk ^ " |--> " ^ p dk);
 200           let eq_s=List.sort compare (sk::NCicUnifHint.eq_class_of status sk) in
 201           let eq_t=List.sort compare (dk::NCicUnifHint.eq_class_of status dk) in
 202           (t,a,g),eq_s,eq_t
 203           )
 204         (CoercionSet.elements dataset);
 205     );
 206   let nodes =
 207     HExtlib.list_uniq
 208      (List.sort compare
 209        (List.flatten
 210          (List.map
 211            (fun (_,a,b) ->
 212              [a;b]
 213             )
 214            !edges)))
 215   in
 216   let names = ref [] in
 217   let id = ref 0 in
 218   let mangle l =
 219     try List.assoc l !names
 220     with Not_found ->
 221       incr id;
 222       names := (l,"node"^string_of_int!id) :: !names;
 223       List.assoc l !names
 224   in
 225   List.iter
 226     (fun cl ->
 227       Pp.node (mangle cl)
 228       ~attrs:["label",String.concat "\\n"
 229         (List.map (fun t->
 230           NCicPp.ppterm ~metasenv:[] ~subst:[]
 231            ~context:[] t ~margin:max_int
 232         ) cl)]
 233       fmt)
 234     nodes;
 235   List.iter
 236     (fun ((t,a,b),src,tgt) ->
 237        Pp.edge (mangle src) (mangle tgt)
 238          ~attrs:["label",
 239            NCicPp.ppterm ~metasenv:[]
 240            ~subst:[] ~context:[] t] fmt)
 241     !edges;
 242   Pp.trailer fmt;
 243   Buffer.contents buf
 244 ;;