From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sun, 11 Oct 2009 13:54:47 +0000 (+0000)
Subject: auto with intro
X-Git-Tag: make_still_working~3345
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2f67829c12dea538114bb848e0275d220dba601b;p=helm.git

auto with intro
---

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index 896403d94..c2ee6a776 100644
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -140,11 +140,13 @@ let rec pp_term ?(pp_parens = true) t =
     | Ast.Ident (name, Some []) | Ast.Ident (name, None)
     | Ast.Uri (name, Some []) | Ast.Uri (name, None) -> name
     | Ast.NRef nref -> NReference.string_of_reference nref
+    | Ast.NCic cic -> NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[] cic
     | Ast.Ident (name, Some substs)
     | Ast.Uri (name, Some substs) ->
         sprintf "%s \\subst [%s]" name (pp_substs substs)
     | Ast.Implicit `Vector -> "?"
     | Ast.Implicit `JustOne -> "…"
+    | Ast.Implicit (`Tagged name) -> "?"^name
     | Ast.Meta (index, substs) ->
         sprintf "%d[%s]" index
           (String.concat "; "
diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml
index 4e9da0424..731a2ba74 100644
--- a/helm/software/components/acic_content/cicNotationPt.ml
+++ b/helm/software/components/acic_content/cicNotationPt.ml
@@ -94,6 +94,8 @@ type term =
   | Uri of string * subst list option (* as Ident, for long names *)
   | NRef of NReference.reference
 
+  | NCic of NCic.term
+
   (* Syntax pattern extensions *)
 
   | Literal of literal
diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml
index 0c8abce50..7eccd7901 100644
--- a/helm/software/components/acic_content/cicNotationUtil.ml
+++ b/helm/software/components/acic_content/cicNotationUtil.ml
@@ -63,6 +63,7 @@ let visit_ast ?(special_k = fun _ -> assert false)
       | Ast.Variable _) as t -> special_k t
     | (Ast.Ident _
       | Ast.NRef _
+      | Ast.NCic _
       | Ast.Implicit _
       | Ast.Num _
       | Ast.Sort _
diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
index 91839e209..853c38e4b 100644
--- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml
+++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
@@ -398,6 +398,7 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
     | CicNotationPt.Ident _
     | CicNotationPt.Uri _
     | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
+    | CicNotationPt.NCic _ -> assert false
     | CicNotationPt.NRef _ -> assert false
     | CicNotationPt.Ident (name,subst)
     | CicNotationPt.Uri (name, subst) as ast ->
diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml
index 52411d6ed..f3ba95765 100644
--- a/helm/software/components/disambiguation/disambiguate.ml
+++ b/helm/software/components/disambiguation/disambiguate.ml
@@ -311,6 +311,7 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
             [ Node ([loc], Id name, terms) ]))
   | Ast.Uri _ -> []
   | Ast.NRef _ -> []
+  | Ast.NCic _ -> []
   | Ast.Implicit _ -> []
   | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
   | Ast.Meta (index, local_context) ->
diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index d50eec796..f221a2b05 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -332,6 +332,10 @@ let interpretate_term_and_interpretate_term_option
         with NRef.IllFormedReference _ ->
          CicNotationPt.fail loc "Ill formed reference")
     | CicNotationPt.NRef nref -> NCic.Const nref
+    | CicNotationPt.NCic t -> 
+           let context = (* to make metas_of_term happy *)
+             List.map (fun x -> x,NCic.Decl (NCic.Implicit `Type)) context in
+           assert(NCicUntrusted.metas_of_term [] context t = []); t
     | CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector
     | CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term
     | CicNotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index 37ac72eb9..4193d41da 100644
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -912,19 +912,72 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa
 ;;
 *)
 
-module CacheElem : Set.OrderedType =
- struct
-  type t = 
-   | Failed_in of int * NCic.term     (* depth, goal type *)
-   | Succeded of Cic.term * Cic.term  (* proof, proof type *)
-   | UnderInspection of Cic.term      (* avoid looping *)
 
-  let compare = Pervasives.compare
- end
+type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
 
-module CacheSet = Set.Make(CacheElem)
-module Cache = 
-  Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(CacheSet)
+let mk_th_cache status gl = 
+  List.fold_left 
+    (fun (status, acc) g ->
+       let gty = get_goalty status g in
+       let ctx = ctx_of gty in
+       if List.mem_assq ctx acc then status, acc else
+         let idx = InvRelDiscriminationTree.empty in
+         let status,_,idx = 
+           List.fold_left (fun (status, i, idx) _ -> 
+              let t = mk_cic_term ctx (NCic.Rel i) in
+              let status, ty = typeof status ctx t in
+              let _, ty, _ = saturate status ty in
+              let idx = InvRelDiscriminationTree.index idx ty t in
+              status, i+1, idx)
+             (status, 1, idx) ctx
+          in
+         status, (ctx, idx) :: acc)
+    (status,[]) gl
+;;
+
+let add_to_th t ty c = 
+  let key_c = ctx_of t in
+  if not (List.mem_assq key_c c) then
+      (key_c ,InvRelDiscriminationTree.index 
+               InvRelDiscriminationTree.empty ty t ) :: c 
+  else
+    let rec replace = function
+      | [] -> []
+      | (x, idx) :: tl when x == key_c -> 
+          (x, InvRelDiscriminationTree.index idx ty t) :: tl
+      | x :: tl -> x :: replace tl
+    in 
+      replace c
+;;
+
+let search_in_th gty th = 
+  let c = ctx_of gty in
+  let rec aux acc = function
+   | [] -> Ncic_termSet.elements acc
+   | (_::tl) as k ->
+       try 
+         let idx = List.assq k th in
+         let acc = Ncic_termSet.union acc 
+           (InvRelDiscriminationTree.retrieve_unifiables idx gty)
+         in
+         aux acc tl
+       with Not_found -> aux acc tl
+  in
+    aux Ncic_termSet.empty c
+;;
+
+let pp_th status = 
+  List.iter 
+    (fun ctx, idx ->
+       prerr_endline "-----------------------------------------------";
+       prerr_endline (NCicPp.ppcontext ~metasenv:[] ~subst:[] ctx);
+       prerr_endline "||====>  ";
+       InvRelDiscriminationTree.iter idx
+          (fun k set ->
+             prerr_endline ("K: " ^ NCicInverseRelIndexable.string_of_path k);
+             Ncic_termSet.iter 
+             (fun t -> prerr_endline ("\t"^ppterm status t)) set))
+;;
 
 type cache_examination_result =
   [ `Failed_in of int
@@ -952,7 +1005,7 @@ type 'a elem =
 type 'a auto_status = 
   (* list of computations that may lead to the solution: all op list will
    * end with the same (S(g,_)) *)
-  'a elem list * Cache.t
+  'a elem list * th_cache
 
 type 'a auto_result = 
   | Gaveup 
@@ -995,26 +1048,26 @@ let rec mk_irl n = function
   | _ :: tl -> NCic.Rel n :: mk_irl (n+1) tl
 ;;
 
-let get_candidates status signature gty =
+let get_candidates status cache_th signature gty =
   let universe = status#auto_cache in
   let context = ctx_of gty in
-  let _, gty = term_of_cic_term status gty context in
+  let _, raw_gty = term_of_cic_term status gty context in
   let cands = 
-    NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe gty
+    NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe raw_gty
   in
   let cands = 
     List.filter (only signature context) 
       (NDiscriminationTree.TermSet.elements cands)
   in
-  (* XXX we have to use the trie for the context *)
-  HExtlib.filter_map (fun name,_ -> 
-    if name <> "_" then Some (Ast.Ident (name,None)) else None) context 
+  List.map (fun t -> 
+     let _status, t = term_of_cic_term status t context in Ast.NCic t) 
+     (search_in_th gty cache_th)
   @ 
   List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands
 ;;
 
 let applicative_case signature status flags g gty cache = 
-  let candidates = get_candidates status signature gty in
+  let candidates = get_candidates status cache signature gty in
   debug_print (lazy ("candidates: " ^ string_of_int (List.length candidates)));
   let elems = 
     List.fold_left 
@@ -1058,7 +1111,7 @@ let equational_and_applicative_case
    List.map (fun c,s,gl -> c,s,List.map (fun i -> i,depth-1,P) gl) elems 
  in
  let elems = sort_new_elems elems in
- elems
+ elems, cache
 ;;
 
 let calculate_goal_ty (goalno,_,_) status = 
@@ -1085,6 +1138,42 @@ let remove_s_from_fl (id,_,_) (fl : fail list) =
     aux fl
 ;;
 
+let rec guess_name name ctx = 
+  if name = "_" then guess_name "auto" ctx else
+  if not (List.mem_assoc name ctx) then name else
+  guess_name (name^"'") ctx
+;;
+
+let intro_case status gno gty depth cache name =
+   let status = NTactics.focus_tac [gno] status in
+   let status = NTactics.intro_tac (guess_name name (ctx_of gty)) status in
+   let open_goals = head_goals status#stack in
+   assert (List.length open_goals  = 1);
+   let open_goal = List.hd open_goals in
+   let status, cache =
+     let ngty = get_goalty status open_goal in
+     let ctx = ctx_of ngty in
+     let t = mk_cic_term ctx (NCic.Rel 1) in
+     let status, ty = typeof status ctx t in
+     let _status, ty, _args = saturate status ty in
+     status, add_to_th t ty cache 
+   in
+   debug_print (lazy (" intro: "^ string_of_int open_goal));
+(*    pp_th status cache; *)
+   incr candidate_no;
+    (* XXX calculate the sort *)
+   [(!candidate_no,Ast.Implicit `JustOne),status,[open_goal,depth,P]],
+   cache
+;;
+                      
+let do_something signature flags s gno depth gty cache =
+  let _s, raw_gty = term_of_cic_term s gty (ctx_of gty) in
+  match raw_gty with
+  | NCic.Prod (name,_,_) -> intro_case s gno gty depth cache name
+  | _ -> 
+      equational_and_applicative_case signature flags s gno depth gty cache
+;;
+
 let auto_main flags signature elems cache =
   let rec aux (elems, cache : 'a auto_status) =
 (* processa le hint dell'utente *)
@@ -1137,6 +1226,7 @@ let auto_main flags signature elems cache =
             debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno));
             aux ((s,size,don,todo, fl)::orlist, cache)
         | Some gty ->
+            let s, gty = apply_subst s (ctx_of gty) gty in
             debug_print (lazy ("EXAMINE: "^ ppterm s gty));
             match cache_examine cache gty with
             | `Failed_in d when d >= depth -> 
@@ -1164,9 +1254,8 @@ let auto_main flags signature elems cache =
                         string_of_int gno ^ "("^ string_of_int size ^ "): "^
                         ppterm s gty));
                     (* elems are possible computations for proving gty *)
-                    let elems =
-                      equational_and_applicative_case 
-                        signature flags s gno depth gty cache 
+                    let elems, cache = 
+                      do_something signature flags s gno depth gty cache
                     in
                     if elems = [] then
                       (* this goal has failed *)
@@ -1205,10 +1294,15 @@ let auto_main flags signature elems cache =
     (aux (elems, cache) : 'a auto_result)
 ;;
 
-let auto_tac ~params status =
-  let cache = Cache.empty in
+let int name l def = 
+  try int_of_string (List.assoc name l)
+  with Failure _ | Not_found -> def
+;;
+
+let auto_tac ~params:(_univ,flags) status =
   let goals = head_goals status#stack in
-  let depth = 3 in 
+  let status, cache = mk_th_cache status goals in
+  let depth = int "depth" flags 3 in 
   (* XXX fix sort *)
   let goals = List.map (fun i -> D(i,depth,P)) goals in
   let elems = [status,0,[],goals,[]] in
diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index d55f7439f..ce7ca8216 100644
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -130,6 +130,14 @@ let typeof status ctx t =
   status, (ctx, ty)
 ;;
 let typeof a b c = wrap "typeof" (typeof a b) c;;
+
+let saturate status (ctx,t) =
+  let n,h,metasenv,subst,k = status#obj in
+  let t, metasenv, args = NCicMetaSubst.saturate metasenv subst ctx t 0 in
+  let status = status#set_obj (n,h,metasenv,subst,k) in
+  status, (ctx,t), List.map (fun x -> ctx,x) args
+;;
+let saturate a b = wrap "saturate" (saturate a) b;;
   
 let whd status ?delta ctx t =
   let status, (_,t) = relocate status ctx t in
diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index 15a788669..0dd5acdc0 100644
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -56,6 +56,8 @@ val refine:
 val apply_subst:
  #pstatus as 'status -> NCic.context -> cic_term -> 'status * cic_term
 val fix_sorts: cic_term -> cic_term
+val saturate :
+ #pstatus as 'status -> cic_term -> 'status * cic_term * cic_term list
 
 val get_goalty: #pstatus -> int -> cic_term
 val mk_meta: 
diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends
index c5d90654b..9d21d9838 100644
--- a/helm/software/matita/nlibrary/depends
+++ b/helm/software/matita/nlibrary/depends
@@ -8,6 +8,7 @@ sets/setoids.ma logic/connectives.ma properties/relations.ma
 logic/connectives.ma logic/pts.ma
 datatypes/pairs.ma logic/pts.ma
 algebra/abelian_magmas.ma algebra/magmas.ma
+topology/igft-setoid.ma sets/sets.ma
 nat/plus.ma algebra/abelian_magmas.ma algebra/unital_magmas.ma nat/big_ops.ma
 nat/minus.ma nat/order.ma
 algebra/magmas.ma sets/sets.ma
diff --git a/helm/software/matita/nlibrary/depends.dot b/helm/software/matita/nlibrary/depends.dot
index b987610af..8af49c5d8 100644
--- a/helm/software/matita/nlibrary/depends.dot
+++ b/helm/software/matita/nlibrary/depends.dot
@@ -27,6 +27,8 @@ digraph g {
   "datatypes/pairs.ma" -> "logic/pts.ma" [];
   "algebra/abelian_magmas.ma" [];
   "algebra/abelian_magmas.ma" -> "algebra/magmas.ma" [];
+  "topology/igft-setoid.ma" [];
+  "topology/igft-setoid.ma" -> "sets/sets.ma" [];
   "nat/plus.ma" [];
   "nat/plus.ma" -> "algebra/abelian_magmas.ma" [];
   "nat/plus.ma" -> "algebra/unital_magmas.ma" [];
diff --git a/helm/software/matita/nlibrary/depends.png b/helm/software/matita/nlibrary/depends.png
index e3fb6c252..fc6f14ecd 100644
Binary files a/helm/software/matita/nlibrary/depends.png and b/helm/software/matita/nlibrary/depends.png differ
diff --git a/helm/software/matita/tests/ng_auto.ma b/helm/software/matita/tests/ng_auto.ma
index b2a420667..2438c5470 100644
--- a/helm/software/matita/tests/ng_auto.ma
+++ b/helm/software/matita/tests/ng_auto.ma
@@ -41,5 +41,12 @@ naxiom is_nat_0 : is_nat zero.
 naxiom is_nat_S : ∀x.is_nat x → is_nat (succ x).
 
 nlemma bar : ∀P:T → CProp[0].P (succ zero) → (λx.And (is_nat x) (P x)) ?.
-##[ #P; #H; nwhd; ##] nauto.  
+##[ #P; #H; nwhd; napply And_intro; ##] nauto.  
+nqed.
+
+naxiom A : CProp[0].
+naxiom pA : A.
+
+nlemma baz : ∀P,Q:CProp[0].(A → P) → (And A P → Q) → Q.
+nauto depth=4;
 nqed.  
\ No newline at end of file