new discrimination tree instantiation with

[helm.git] / helm / software / components / ng_tactics / nTacStatus.ml

diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index 41319b4739d6c44f08f75fa39e70dc201debd9fc..d55f7439f385c847370433ed570e594c7b6dc3cf 100644 (file)
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -16,14 +16,14 @@ let fail ?exn msg = raise (Error (msg,exn))
 
 module NRef = NReference
 
-let wrap f x =
+let wrap fname f x =
   try f x 
   with 
   | MultiPassDisambiguator.DisambiguationError _ 
   | NCicRefiner.RefineFailure _ 
   | NCicUnification.UnificationFailure _ 
   | NCicTypeChecker.TypeCheckerFailure _ 
-  | NCicMetaSubst.MetaSubstFailure _ as exn -> fail ~exn (lazy "")
+  | NCicMetaSubst.MetaSubstFailure _ as exn -> fail ~exn (lazy fname)
 ;;
 
 class pstatus =
@@ -94,7 +94,7 @@ let relocate status destination (source,t as orig) =
   let status = status#set_obj (u, d, metasenv, subst, o) in
   status, (destination, t)
 ;;
-let relocate a b c = wrap (relocate a b) c;;
+let relocate a b c = wrap "relocate" (relocate a b) c;;
 
 let term_of_cic_term s t c = 
   let s, (_,t) = relocate s c t in
@@ -121,7 +121,7 @@ let disambiguate status t ty context =
  let new_pstatus = uri,height,metasenv,subst,obj in
   status#set_obj new_pstatus, (context, t) 
 ;;
-let disambiguate a b c d = wrap (disambiguate a b c) d;;
+let disambiguate a b c d = wrap "disambiguate" (disambiguate a b c) d;;
 
 let typeof status ctx t =
   let status, (_,t) = relocate status ctx t in
@@ -129,7 +129,7 @@ let typeof status ctx t =
   let ty = NCicTypeChecker.typeof ~subst ~metasenv ctx t in
   status, (ctx, ty)
 ;;
-let typeof a b c = wrap (typeof a b) c;;
+let typeof a b c = wrap "typeof" (typeof a b) c;;
   
 let whd status ?delta ctx t =
   let status, (_,t) = relocate status ctx t in
@@ -152,14 +152,14 @@ let unify status ctx a b =
   let metasenv, subst = NCicUnification.unify status metasenv subst ctx a b in
    status#set_obj (n,h,metasenv,subst,o)
 ;;
-let unify a b c d = wrap (unify a b c) d;;
+let unify a b c d = wrap "unify" (unify a b c) d;;
 
 let fix_sorts (ctx,t) =
  let f () =
   let t = NCicUnification.fix_sorts t in
    ctx,t
  in
-  wrap f ()
+  wrap "fix_sorts" f ()
 ;;
 
 let refine status ctx term expty =
@@ -176,12 +176,14 @@ let refine status ctx term expty =
   in
    status#set_obj (name,height,metasenv,subst,obj), (ctx,t), (ctx,ty)
 ;;
-let refine a b c d = wrap (refine a b c) d;;
+let refine a b c d = wrap "refine" (refine a b c) d;;
 
 let get_goalty status g =
  let _,_,metasenv,_,_ = status#obj in
- let _, a, b = List.assoc g metasenv in
- a, b
+ try
+   let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
+   ctx, ty
+ with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_goalty")
 ;;
 
 let instantiate status i t =
@@ -373,3 +375,66 @@ class type tac_status = [Continuationals.Stack.t] status
 
 type 'status tactic = #tac_status as 'status -> 'status
 
+module NCicInverseRelIndexable : Discrimination_tree.Indexable
+with type input = cic_term and type constant_name = NUri.uri = struct
+
+open Discrimination_tree
+
+type input = cic_term
+type constant_name = NUri.uri
+
+let ppelem = function
+  | Constant (uri,arity) -> 
+      "("^NUri.name_of_uri uri ^ "," ^ string_of_int arity^")"
+  | Bound (i,arity) -> 
+      "("^string_of_int i ^ "," ^ string_of_int arity^")"
+  | Variable -> "?"
+  | Proposition -> "Prop"
+  | Datatype -> "Type"
+  | Dead -> "Dead"
+;;
+
+let path_string_of (ctx,t) =
+  let len_ctx = List.length ctx in
+  let rec aux arity = function
+    | NCic.Appl ((NCic.Meta _|NCic.Implicit _)::_) -> [Variable]
+    | NCic.Appl (NCic.Lambda _ :: _) -> [Variable] (* maybe we should b-reduce *)
+    | NCic.Appl [] -> assert false
+    | NCic.Appl (hd::tl) ->
+        aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl) 
+    | NCic.Lambda _ | NCic.Prod _ -> [Variable]
+        (* I think we should CicSubstitution.subst Implicit t *)
+    | NCic.LetIn _ -> [Variable] (* z-reduce? *)
+    | NCic.Meta _ | NCic.Implicit _ -> assert (arity = 0); [Variable]
+    | NCic.Rel i -> [Bound (len_ctx - i, arity)]
+    | NCic.Sort (NCic.Prop) -> assert (arity=0); [Proposition]
+    | NCic.Sort _ -> assert (arity=0); [Datatype]
+    | NCic.Const (NReference.Ref (u,_)) -> [Constant (u, arity)]
+    | NCic.Match _ -> [Dead]
+  in 
+    aux 0 t
+;;
+
+let compare e1 e2 =
+  match e1,e2 with
+  | Constant (u1,a1),Constant (u2,a2) -> 
+       let x = NUri.compare u1 u2 in
+       if x = 0 then Pervasives.compare a1 a2 else x
+  | e1,e2 -> Pervasives.compare e1 e2
+;;
+
+let string_of_path l = String.concat "." (List.map ppelem l) ;;
+
+end
+
+module Ncic_termOT : Set.OrderedType with type t = cic_term =
+ struct
+   type t = cic_term
+   let compare = Pervasives.compare
+ end
+
+module Ncic_termSet : Set.S with type elt = cic_term = Set.Make(Ncic_termOT)
+
+module InvRelDiscriminationTree = 
+   Discrimination_tree.Make(NCicInverseRelIndexable)(Ncic_termSet)
+