helm/software/components/ng_refiner/nCicUnifHint.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 module COT : Set.OrderedType with type t = NCic.term =
  15   struct
  16         type t = NCic.term
  17         let compare = Pervasives.compare
  18   end
  19
  20 module HintSet = Set.Make(COT)
  21
  22 module DB =
  23   Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(HintSet)
  24
  25 type db = DB.t
  26
  27 let dummy = NCic.Const (NReference.reference_of_string "cic:/dummy_conv.dec");;
  28 let pair t1 t2 = (NCic.Appl [dummy;t1;t2]) ;;
  29
  30 let index_hint hdb context t1 t2 =
  31   let pair' = pair t1 t2 in
  32   let data =
  33     List.fold_left
  34      (fun t (n,e) ->
  35         match e with
  36         | NCic.Decl ty -> NCic.Prod (n,ty,t)
  37         | _ -> assert false)
  38       pair' context in
  39   let src =
  40     List.fold_left
  41      (fun t (_,e) ->
  42         match e with
  43         | NCic.Decl _ -> NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) t
  44         | _ -> assert false)
  45      pair' context in
  46   let _ = prerr_endline ("SONO PASSATO DI QUI") in
  47
  48 (*
  49   prerr_endline ("INDEX:" ^
  50     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
  51     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ "  :=  " ^
  52     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c);
  53 *)
  54   DB.index hdb src data
  55 ;;
  56
  57 let empty_db = DB.empty ;;
  58
  59 let db () =
  60   try let _,_,_,x,_,_ = NCicEnvironment.get_checked_def
  61     (NReference.reference_of_string "cic:/matita/tests/pullback/xxx.def(0)")
  62   in
  63     prerr_endline "iiiiiiiiiiiiiiiiii";
  64   let rec decontextualize ctx = function
  65     | NCic.Prod (n,s,t) -> decontextualize ((n,NCic.Decl s)::ctx) t
  66     | t -> ctx, t
  67   in
  68     match (decontextualize [] x) with
  69     | ctx, NCic.Appl [_;_;a;b] -> index_hint empty_db ctx a b
  70     | _ -> assert false
  71   with exn -> prerr_endline ("PIPPO" ^ Printexc.to_string exn); empty_db
  72
  73 (*  List.fold_left
  74     (fun db (_,tgt,clist) ->
  75        List.fold_left
  76          (fun db (uri,_,arg) ->
  77             let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in
  78             let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in
  79             let src, tgt =
  80               let cty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] c in
  81               let scty, metasenv,_ =
  82                 NCicMetaSubst.saturate ~delta:max_int [] [] [] cty (arity+1)
  83               in
  84               match scty with
  85               | NCic.Prod (_, src, tgt) ->
  86                  let tgt =
  87                    NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt
  88                  in
  89 (*
  90             prerr_endline (Printf.sprintf "indicizzo %s (%d) : %s ===> %s"
  91               (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] scty) (arity+1)
  92               (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] src)
  93               (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] tgt));
  94 *)
  95                 src, tgt
  96               | t ->
  97                   prerr_endline (
  98                     NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t);
  99                   assert false
 100             in
 101             index_coercion db c src tgt arity arg)
 102          db clist)
 103     (DB.empty,DB.empty) (CoercDb.to_list ())
 104  *)
 105 ;;
 106
 107
 108 let look_for_hint hdb metasenv subst context t1 t2 =
 109
 110   let candidates = DB.retrieve_unifiables hdb (pair t1 t2) in
 111   let res = List.map
 112       (fun ty ->
 113           let ty, metasenv, _ =
 114            NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty 0
 115           in
 116           match ty with
 117           | NCic.Appl [_; t1; t2] ->
 118           prerr_endline ("candidate1: " ^ NCicPp.ppterm ~metasenv ~subst ~context t1);
 119           prerr_endline ("candidate2: " ^ NCicPp.ppterm ~metasenv ~subst ~context t2);
 120
 121               metasenv, t1, t2
 122           | _ -> assert false)
 123       (HintSet.elements candidates)
 124   in
 125   let _ = prerr_endline ("DENTRO RICERCA: " ^ (string_of_int (List.length res))) in
 126   res
 127 ;;