From: Enrico Tassi Date: Mon, 15 Dec 2008 22:49:47 +0000 (+0000) Subject: added unification hints X-Git-Tag: make_still_working~4390 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e6cfe36583259c1e3f6d91e66e50a647726c1716;p=helm.git added unification hints --- diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml new file mode 100644 index 000000000..01f9b594b --- /dev/null +++ b/helm/software/components/ng_refiner/nCicUnifHint.ml @@ -0,0 +1,127 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *) + +module COT : Set.OrderedType with type t = NCic.term = + struct + type t = NCic.term + let compare = Pervasives.compare + end + +module HintSet = Set.Make(COT) + +module DB = + Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(HintSet) + +type db = DB.t + +let dummy = NCic.Const (NReference.reference_of_string "cic:/dummy_conv.dec");; +let pair t1 t2 = (NCic.Appl [dummy;t1;t2]) ;; + +let index_hint hdb context t1 t2 = + let pair' = pair t1 t2 in + let data = + List.fold_left + (fun t (n,e) -> + match e with + | NCic.Decl ty -> NCic.Prod (n,ty,t) + | _ -> assert false) + pair' context in + let src = + List.fold_left + (fun t (_,e) -> + match e with + | NCic.Decl _ -> NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) t + | _ -> assert false) + pair' context in + let _ = prerr_endline ("SONO PASSATO DI QUI") in + +(* + prerr_endline ("INDEX:" ^ + NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^ + NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ " := " ^ + NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c); +*) + DB.index hdb src data +;; + +let empty_db = DB.empty ;; + +let db () = + try let _,_,_,x,_,_ = NCicEnvironment.get_checked_def + (NReference.reference_of_string "cic:/matita/tests/pullback/xxx.def(0)") + in + prerr_endline "iiiiiiiiiiiiiiiiii"; + let rec decontextualize ctx = function + | NCic.Prod (n,s,t) -> decontextualize ((n,NCic.Decl s)::ctx) t + | t -> ctx, t + in + match (decontextualize [] x) with + | ctx, NCic.Appl [_;_;a;b] -> index_hint empty_db ctx a b + | _ -> assert false + with exn -> prerr_endline ("PIPPO" ^ Printexc.to_string exn); empty_db + +(* List.fold_left + (fun db (_,tgt,clist) -> + List.fold_left + (fun db (uri,_,arg) -> + let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in + let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in + let src, tgt = + let cty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] c in + let scty, metasenv,_ = + NCicMetaSubst.saturate ~delta:max_int [] [] [] cty (arity+1) + in + match scty with + | NCic.Prod (_, src, tgt) -> + let tgt = + NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt + in +(* + prerr_endline (Printf.sprintf "indicizzo %s (%d) : %s ===> %s" + (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] scty) (arity+1) + (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] src) + (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] tgt)); +*) + src, tgt + | t -> + prerr_endline ( + NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t); + assert false + in + index_coercion db c src tgt arity arg) + db clist) + (DB.empty,DB.empty) (CoercDb.to_list ()) + *) +;; + + +let look_for_hint hdb metasenv subst context t1 t2 = + + let candidates = DB.retrieve_unifiables hdb (pair t1 t2) in + let res = List.map + (fun ty -> + let ty, metasenv, _ = + NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty 0 + in + match ty with + | NCic.Appl [_; t1; t2] -> + prerr_endline ("candidate1: " ^ NCicPp.ppterm ~metasenv ~subst ~context t1); + prerr_endline ("candidate2: " ^ NCicPp.ppterm ~metasenv ~subst ~context t2); + + metasenv, t1, t2 + | _ -> assert false) + (HintSet.elements candidates) + in + let _ = prerr_endline ("DENTRO RICERCA: " ^ (string_of_int (List.length res))) in + res +;; diff --git a/helm/software/components/ng_refiner/nCicUnifHint.mli b/helm/software/components/ng_refiner/nCicUnifHint.mli new file mode 100644 index 000000000..115ddfb15 --- /dev/null +++ b/helm/software/components/ng_refiner/nCicUnifHint.mli @@ -0,0 +1,28 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *) + +type db + +val index_hint: + db -> NCic.context -> NCic.term -> NCic.term -> db + + (* gets the old imperative coercion DB *) +val db : unit -> db + +val empty_db : db + +val look_for_hint: + db -> + NCic.metasenv -> NCic.substitution -> NCic.context -> + NCic.term -> NCic.term -> + (NCic.metasenv * NCic.term * NCic.term) list