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