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