tactic cases works! delift clears tags

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 2deacf2ac48bf5cde54bb68b3075889371a08788..512f5ede40c8643b21415f1ee3ceeaeb4bde1786 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -51,6 +51,7 @@ type 'term just =
 
 type ntactic =
    | NApply of loc * CicNotationPt.term
+   | NCases of loc * CicNotationPt.term * npattern  
    | NCase1 of loc * string
    | NChange of loc * npattern * CicNotationPt.term
    | NElim of loc * CicNotationPt.term * npattern  

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 347eab2dabee8871f938172b44b6da856fc3ef3b..22e4cbe09e19348aab695521a9947693bcfdaf4a 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -91,6 +91,8 @@ let pp_just ~term_pp =
 
 let pp_ntactic ~map_unicode_to_tex = function
   | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
+  | NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^
+      assert false ^ " " ^ assert false
   | NCase1 (_,n) -> "*" ^ n ^ ":"
   | NChange (_,what,wwhat) -> "nchange " ^ assert false ^ 
       " with " ^ CicNotationPp.pp_term wwhat

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 09eb2d34514011de6e606ca1c57d9adbd3021868..af8b086bfb58a256999d28a49fbe34cc72990f44 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -586,6 +586,10 @@ let eval_ng_punct (_text, _prefix_len, punct) =
 let eval_ng_tac (text, prefix_len, tac) =
   match tac with
   | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) 
+  | GrafiteAst.NCases (_loc, what, where) ->
+      NTactics.cases_tac 
+        ~what:(text,prefix_len,what)
+        ~where:(text,prefix_len,where)
   | GrafiteAst.NCase1 (_loc,n) -> NTactics.case1_tac n
   | GrafiteAst.NChange (_loc, pat, ww) -> 
       NTactics.change_tac 

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index fa2680811c38e7bfebeb014a80cb4d028189dc26..b20ca85baa3c0e48fb7e04d2c0055590a610e510 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -182,6 +182,8 @@ EXTEND
   using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
   ntactic: [
     [ IDENT "napply"; t = tactic_term -> GrafiteAst.NApply (loc, t)
+    | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
+        GrafiteAst.NCases (loc, what, where)
     | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term -> 
         GrafiteAst.NChange (loc, what, with_what)
     | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index 1a2b5471b0cf76910eb0666c1cba0fb96a59b7bb..adc1ac6202ef21c302026c88d9b1305aa3d67fbd 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -266,12 +266,18 @@ let delift ~unify metasenv subst context n l t =
             (NCicPp.ppterm ~context ~metasenv ~subst t))))
     | NCic.Meta (i,l1) as orig ->
         (try
-           let tag,_,t,_ = NCicUtils.lookup_subst i subst in
-           let in_scope = 
+           let tag,c,t,ty = NCicUtils.lookup_subst i subst in
+           let in_scope, clear = 
              match tag with 
-             | Some tag when tag = in_scope_tag -> 0
-             | Some tag when is_out_scope_tag tag -> int_of_out_scope_tag tag
-             | _ -> in_scope
+             | Some tag when tag = in_scope_tag -> 0, true
+             | Some tag when is_out_scope_tag tag->int_of_out_scope_tag tag,true
+             | _ -> in_scope, false
+           in
+           let ms = 
+             if not clear then ms
+             else 
+               metasenv, 
+               (i,(None,c,t,ty)) :: List.filter (fun j,_ -> i <> j) subst
            in
            aux (context,k,in_scope) ms (NCicSubstitution.subst_meta l1 t)
          with NCicUtils.Subst_not_found _ ->

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 8c5dcae76d0d700e5a93156faa32bdb5eae66ba0..f79b458419a9728421c21e814adf4054eade5cf0 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -27,7 +27,7 @@ let pp s =
   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
 ;;  
 
-let pp _ = ();;
+(* let pp _ = ();; *)
 
 let wrap_exc msg = function
   | NCicUnification.Uncertain _ -> Uncertain msg

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 006fcafe144f61d48c8c1713b4876c8d24420669..22f896f21e12c13fa26fe2cb5d6133911385481a 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -86,7 +86,7 @@ let pp s =
   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
 ;;  
 
-let pp _ = ();;
+(* let pp _ = ();; *)
 
 let fix_sorts swap metasenv subst context meta t =
   let rec aux () = function
@@ -302,23 +302,24 @@ and unify hdb test_eq_only metasenv subst context t1 t2 =
                   unify hdb test_eq_only metasenv subst context term1 term2
               with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
        
-       | NCic.Appl (NCic.Meta (i,l)::args), NCic.Meta (n, _) when 
-         not (NCicMetaSubst.flexible subst args) &&
-         is_locked n subst &&
-         not (List.mem_assoc i subst) 
-         ->
-           (* we verify that none of the args is a Meta, 
-              since beta expanding w.r.t a metavariable makes no sense  *)
-              let metasenv, lambda_Mj =
-                lambda_intros metasenv subst context t1 args
-              in
-              let metasenv, subst = 
-                unify hdb test_eq_only metasenv subst context 
-                  (C.Meta (i,l)) lambda_Mj
-              in
+       | _, NCic.Meta (n, _) when is_locked n subst ->
+           (let (metasenv, subst), i = 
+              match NCicReduction.whd ~subst context t1 with
+              | NCic.Appl (NCic.Meta (i,l)::args) when
+                  not (NCicMetaSubst.flexible subst args) 
+                ->
+                 let metasenv, lambda_Mj =
+                   lambda_intros metasenv subst context t1 args
+                 in
+                   unify hdb test_eq_only metasenv subst context 
+                    (C.Meta (i,l)) lambda_Mj,
+                   i
+              | NCic.Meta (i,_) -> (metasenv, subst), i
+              | _ -> assert false
+             in
               let t1 = NCicReduction.whd ~subst context t1 in
               let j, lj = 
-                match t1 with NCic.Meta (i,l) -> i, l | _ -> assert false
+                match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false
               in
               let metasenv, subst = 
                 instantiate hdb test_eq_only metasenv subst context j lj t2 true
@@ -328,7 +329,7 @@ and unify hdb test_eq_only metasenv subst context t1 t2 =
                 let term = eta_reduce subst term in
                 let subst = List.filter (fun (j,_) -> j <> i) subst in
                 metasenv, ((i, (name, ctx, term, ty)) :: subst)
-              with Not_found -> assert false)
+              with Not_found -> assert false))
 
        | C.Meta (n,lc), t -> 
            (try 

diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index f0d12aa8e6b25e1e837247b409bae46bece1ec00..1c7029f4ab038e8fb7e4f9fa6e06c043e9732ea1 100644 (file)
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -61,6 +61,10 @@ let relocate context (name,ctx,t as term) =
     assert false
 ;;
 
+let term_of_cic_term t c = 
+  let _,_,t = relocate c t in
+  t
+;;
 
 type ast_term = string * int * CicNotationPt.term
 

diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index ce3fd33b03c39da2b2a57f11d7da65c3e6e1a7b3..6c7d698239f96fa5ac7efba9e11f8053254cc214 100644 (file)
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -33,6 +33,7 @@ type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input
 
 type cic_term 
 val ctx_of : cic_term -> NCic.context
+val term_of_cic_term : cic_term -> NCic.context -> NCic.term
 
 val mk_cic_term : NCic.context -> NCic.term -> cic_term
 type ast_term = string * int * CicNotationPt.term

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index f45aa656b5136ce182460ca856526390668129c3..52a82af699febc4bdf9de0f50a03c6835cbba9e1 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -311,23 +311,27 @@ let intro_tac name =
    (CicNotationPt.Ident (name,None),None),CicNotationPt.Implicit)))
 ;;
 
-let case ~what status goal =
+let cases ~what status goal =
  let gty = get_goalty status goal in
  let status, what = disambiguate status what None (ctx_of gty) in
  let ty = typeof status (ctx_of what) what in
  let ref, consno, left, right = analyse_indty status ty in
  let t =
-  NCic.Match (ref,NCic.Implicit `Term,NCic.Rel 1,
+  NCic.Match (ref,NCic.Implicit `Term, term_of_cic_term what (ctx_of gty),
     HExtlib.mk_list (NCic.Implicit `Term) consno)
  in
  let ctx = ctx_of gty in
- let status,t,ty = refine status ctx (mk_cic_term ctx t) None in
+ let status,t,ty = refine status ctx (mk_cic_term ctx t) (Some gty) in
  instantiate status goal t
 ;;
 
-let case_tac ~what = distribute_tac (case ~what);;
+let cases_tac ~what ~where = 
+  block_tac [ select_tac ~where ; distribute_tac (cases ~what) ]
+;;
 
 let case1_tac name =
  block_tac [ intro_tac name; 
-             case_tac ~what:("",0,CicNotationPt.Ident (name,None)) ]
+             cases_tac 
+              ~where:("",0,(None,[],None)) 
+              ~what:("",0,CicNotationPt.Ident (name,None)) ]
 ;;

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index fffcad698339e0ebd885e52ddf312f92e69b54a3..a834c4e52a8439ac1fea0eda294ad9435c8c5fa2 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -32,5 +32,8 @@ val elim_tac:
    what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
      NTacStatus.tactic
 val intro_tac: string -> NTacStatus.tactic
+val cases_tac: 
+   what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
+     NTacStatus.tactic
 val case1_tac: string -> NTacStatus.tactic