Experimental support for Russell (coercions moving inside lambda & pattern

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

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 9834cce8a943e1377ecd0b6728e5dca46506847c..f3d74050f9247cb07cc14d231428c5108ba683da 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -22,7 +22,7 @@ module Ast = CicNotationPt
 
 let id_tac status = status ;;
 let print_tac print_status message status = 
-  if print_status then pp_status status;
+  if print_status then pp_tac_status status;
   prerr_endline message; 
   status
 ;;
@@ -46,13 +46,14 @@ let dot_tac status =
    status#set_stack gstatus
 ;;
 
-let branch_tac status =
+let branch_tac ?(force=false) status =
   let gstatus = 
     match status#stack with
     | [] -> assert false
     | (g, t, k, tag) :: s ->
           match init_pos g with (* TODO *)
-          | [] | [ _ ] -> fail (lazy "too few goals to branch");
+          | [] -> fail (lazy "empty goals")
+         | [_] when (not force) -> fail (lazy "too few goals to branch")
           | loc :: loc_tl ->
                ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
   in
@@ -314,7 +315,7 @@ let clear_tac names =
      names
    in
    let n,h,metasenv,subst,o = status#obj in
-   let metasenv,subst,_ = NCicMetaSubst.restrict metasenv subst goal js in
+   let metasenv,subst,_,_ = NCicMetaSubst.restrict metasenv subst goal js in
     status#set_obj (n,h,metasenv,subst,o))
 ;;
 
@@ -368,7 +369,7 @@ let select0_tac ~where:(wanted,hyps,where) ~job  =
    let newgoalty = mk_cic_term newgoalctx newgoalty in
 
    let status, instance = 
-     mk_meta status newgoalctx (`Decl newgoalty) 
+     mk_meta status newgoalctx (`Decl newgoalty) `IsTerm
    in
    instantiate status goal instance)
 ;;
@@ -395,7 +396,6 @@ let generalize_tac ~where =
  let l = ref [] in
  block_tac [ 
    select_tac ~where ~job:(`Collect l) true; 
-   print_tac true "ha selezionato?";
    (fun s -> distribute_tac (fun status goal ->
       let goalty = get_goalty status goal in
       let status,canon,rest =
@@ -423,8 +423,8 @@ let cut_tac t =
  block_tac [ 
   exact_tac ("",0, Ast.Appl [Ast.Implicit `JustOne; Ast.Implicit `JustOne]);
   branch_tac;
-   pos_tac [2]; exact_tac t;
-   shift_tac; pos_tac [1]; skip_tac;
+   pos_tac [3]; exact_tac t;
+   shift_tac; pos_tac [2]; skip_tac;
   merge_tac ]
 ;;
 
@@ -479,6 +479,8 @@ type indtyinfo = {
  }
 ;;
 
+let ref_of_indtyinfo iti = iti.reference;;
+
 let analyze_indty_tac ~what indtyref =
  distribute_tac (fun status goal ->
   let goalty = get_goalty status goal in
@@ -497,7 +499,7 @@ let analyze_indty_tac ~what indtyref =
 let sort_of_goal_tac sortref = distribute_tac (fun status goal ->
   let goalty = get_goalty status goal in
   let status,sort = typeof status (ctx_of goalty) goalty in
-  let sort = fix_sorts sort in
+  let status, sort = fix_sorts status sort in
   let status, sort = term_of_cic_term status sort (ctx_of goalty) in
    sortref := sort;
    status)
@@ -539,7 +541,7 @@ let rewrite_tac ~dir ~what:(_,_,what) ~where status =
    | `RightToLeft -> "eq" ^ suffix
  in
   block_tac
-   [ select_tac ~where ~job:(`Substexpand 1) true;
+   [ select_tac ~where ~job:(`Substexpand 2) true;
      exact_tac
       ("",0,
        Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list (Ast.Implicit `JustOne) 5@
@@ -554,6 +556,25 @@ let intro_tac name =
     if name = "_" then clear_tac [name] else id_tac ]
 ;;
 
+let name_counter = ref 0;;
+let intros_tac ?names_ref names s =
+  let names_ref, prefix = 
+    match names_ref with | None -> ref [], "__" | Some r -> r, "H" 
+  in
+  if names = [] then
+   repeat_tac 
+     (fun s ->
+        incr name_counter;
+        (* TODO: generate better names *)
+        let name = prefix ^ string_of_int !name_counter in
+        let s = intro_tac name s in 
+        names_ref := !names_ref @ [name];
+        s)
+     s
+   else
+     block_tac (List.map intro_tac names) s
+;;
+
 let cases ~what status goal =
  let gty = get_goalty status goal in
  let status, what = disambiguate status (ctx_of gty) what None in
@@ -587,7 +608,7 @@ let case1_tac name =
              if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
 ;;
 
-let constructor ?(num=1) ~args status goal = 
+let constructor_tac ?(num=1) ~args = distribute_tac (fun status goal ->
   if num < 1 then fail (lazy "constructor numbers begin with 1");
   let gty = get_goalty status goal in
   let status, (r,_,_,_) = analyse_indty status gty in
@@ -597,11 +618,9 @@ let constructor ?(num=1) ~args status goal =
     Ast.Appl (HExtlib.list_concat ~sep:[Ast.Implicit `Vector]
       ([Ast.NRef ref] :: List.map (fun _,_,x -> [x]) args))
   in
-  exec (apply_tac ("",0,t)) status goal
+  exec (apply_tac ("",0,t)) status goal)
 ;;
 
-let constructor_tac ?num ~args = distribute_tac (constructor ?num ~args);;
-
 let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
  let gty = get_goalty status goal in
  let eq status ctx t1 t2 =
@@ -645,10 +664,33 @@ let assert_tac seqs status =
        | [seq] -> assert0_tac seq
        | _ ->
          block_tac
-          (branch_tac::
+          ((branch_tac ~force:false)::
           HExtlib.list_concat ~sep:[shift_tac]
             (List.map (fun seq -> [assert0_tac seq]) seqs)@
           [merge_tac])
      ) status
 ;;
 
+let inversion_tac ~what:(txt,len,what) ~where = 
+  let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
+  let indtyinfo = ref None in
+  let sort = ref (NCic.Rel 1) in
+  atomic_tac (block_tac [
+    analyze_indty_tac ~what indtyinfo;    
+    (fun s -> select_tac 
+      ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true s);
+    sort_of_goal_tac sort;
+    (fun status ->
+     let ity = HExtlib.unopt !indtyinfo in
+     let NReference.Ref (uri, _) = ity.reference in
+     let name = 
+       NUri.name_of_uri uri ^ "_inv_" ^
+        snd (NCicElim.ast_of_sort 
+          (match !sort with NCic.Sort x -> x | _ -> assert false))
+     in
+     let eliminator = 
+       let _,_,w = what in
+       Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
+     in
+     exact_tac ("",0,eliminator) status) ]) 
+;;