helm/software/components/ng_tactics/nTactics.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
  13
  14 open Printf
  15
  16 let debug = true
  17 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
  18
  19 open Continuationals.Stack
  20 open NTacStatus
  21 module Ast = CicNotationPt
  22
  23 let id_tac status = status ;;
  24 let print_tac message status = prerr_endline message; status ;;
  25
  26 let dot_tac status =
  27   let new_gstatus =
  28     match status.gstatus with
  29     | [] -> assert false
  30     | ([], _, [], _) :: _ as stack ->
  31         (* backward compatibility: do-nothing-dot *)
  32         stack
  33     | (g, t, k, tag) :: s ->
  34         match filter_open g, k with
  35         | loc :: loc_tl, _ ->
  36              (([ loc ], t, loc_tl @+ k, tag) :: s)
  37         | [], loc :: k ->
  38             assert (is_open loc);
  39             (([ loc ], t, k, tag) :: s)
  40         | _ -> fail (lazy "can't use \".\" here")
  41   in
  42    { status with gstatus = new_gstatus }
  43 ;;
  44
  45 let branch_tac status =
  46   let new_gstatus =
  47     match status.gstatus with
  48     | [] -> assert false
  49     | (g, t, k, tag) :: s ->
  50           match init_pos g with (* TODO *)
  51           | [] | [ _ ] -> fail (lazy "too few goals to branch");
  52           | loc :: loc_tl ->
  53                ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
  54   in
  55    { status with gstatus = new_gstatus }
  56 ;;
  57
  58 let shift_tac status =
  59   let new_gstatus =
  60     match status.gstatus with
  61     | (g, t, k, `BranchTag) :: (g', t', k', tag) :: s ->
  62           (match g' with
  63           | [] -> fail (lazy "no more goals to shift")
  64           | loc :: loc_tl ->
  65                 (([ loc ], t @+ filter_open g @+ k, [],`BranchTag)
  66                 :: (loc_tl, t', k', tag) :: s))
  67      | _ -> fail (lazy "can't shift goals here")
  68   in
  69    { status with gstatus = new_gstatus }
  70 ;;
  71
  72 let pos_tac i_s status =
  73   let new_gstatus =
  74     match status.gstatus with
  75     | [] -> assert false
  76     | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
  77       when is_fresh loc ->
  78         let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in
  79           ((l_js, t , [],`BranchTag)
  80            :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
  81     | _ -> fail (lazy "can't use relative positioning here")
  82   in
  83    { status with gstatus = new_gstatus }
  84 ;;
  85
  86 let wildcard_tac status =
  87   let new_gstatus =
  88     match status.gstatus with
  89     | [] -> assert false
  90     | ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s
  91        when is_fresh loc ->
  92             (([loc] @+ g', t, [], `BranchTag) :: ([], t', k', tag) :: s)
  93     | _ -> fail (lazy "can't use wildcard here")
  94   in
  95    { status with gstatus = new_gstatus }
  96 ;;
  97
  98 let merge_tac status =
  99   let new_gstatus =
 100     match status.gstatus with
 101     | [] -> assert false
 102     | (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
 103         ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s)
 104     | _ -> fail (lazy "can't merge goals here")
 105   in
 106    { status with gstatus = new_gstatus }
 107 ;;
 108
 109 let focus_tac gs status =
 110   let new_gstatus =
 111     match status.gstatus with
 112     | [] -> assert false
 113     | s -> assert(gs <> []);
 114           let stack_locs =
 115             let add_l acc _ _ l = if is_open l then l :: acc else acc in
 116             fold ~env:add_l ~cont:add_l ~todo:add_l [] s
 117           in
 118           List.iter
 119             (fun g ->
 120               if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
 121                 fail (lazy (sprintf "goal %d not found (or closed)" g)))
 122             gs;
 123           (zero_pos gs, [], [], `FocusTag) :: deep_close gs s
 124   in
 125    { status with gstatus = new_gstatus }
 126 ;;
 127
 128 let unfocus_tac status =
 129   let new_gstatus =
 130     match status.gstatus with
 131     | [] -> assert false
 132     | ([], [], [], `FocusTag) :: s -> s
 133     | _ -> fail (lazy "can't unfocus, some goals are still open")
 134   in
 135    { status with gstatus = new_gstatus }
 136 ;;
 137
 138 let skip_tac status =
 139   let new_gstatus =
 140     match status.gstatus with
 141     | [] -> assert false
 142     | (gl, t, k, tag) :: s ->
 143         let gl = List.map switch_of_loc gl in
 144         if List.exists (function Open _ -> true | Closed _ -> false) gl then
 145           fail (lazy "cannot skip an open goal")
 146         else
 147           ([],t,k,tag) :: s
 148   in
 149    { status with gstatus = new_gstatus }
 150 ;;
 151
 152 let block_tac l status =
 153   List.fold_left (fun status tac -> tac status) status l
 154 ;;
 155
 156 let compare_statuses ~past ~present =
 157  let _,_,past,_,_ = past.pstatus in
 158  let _,_,present,_,_ = present.pstatus in
 159  let closed =
 160   List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
 161  in
 162  let opened =
 163    List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present)
 164  in
 165  opened, closed
 166 ;;
 167
 168
 169
 170 (* Exec and distribute_tac form a retraction pair:
 171     1) exec (distribute_tac low_tac) (s,i) = low_tac (s,i)
 172     2) tac [s]::G = G1::...::Gn::G' && G' is G with some goals closed =>
 173          distribute_tac (exec tac) [s]::G = (G1@...Gn)::G'
 174     3) tac G = distribute_tac (exec tac) G if
 175        tac = distribute_tac lowtac
 176     4) atomic_tac t === distribute_tac (exec t)
 177
 178    Note that executing an high tactic on a set of goals may be stronger
 179    than executing the same tactic on those goals, but once at a time
 180    (e.g. the tactic could perform a global analysis of the set of goals)
 181 *)
 182
 183 let exec tac low_status g =
 184   let stack = [ [0,Open g], [], [], `NoTag ] in
 185   let status = tac { gstatus = stack ; istatus = low_status } in
 186    status.istatus
 187 ;;
 188
 189 let distribute_tac tac status =
 190   match status.gstatus with
 191   | [] -> assert false
 192   | (g, t, k, tag) :: s ->
 193       debug_print (lazy ("context length " ^string_of_int (List.length g)));
 194       let rec aux s go gc =
 195         function
 196         | [] ->
 197             debug_print (lazy "no selected goals");
 198             s, go, gc
 199         | loc :: loc_tl ->
 200             debug_print (lazy "inner eval tactical");
 201             let s, go, gc =
 202               if List.exists ((=) (goal_of_loc loc)) gc then
 203                 s, go, gc
 204               else
 205                 match switch_of_loc loc with
 206                 | Closed _ -> fail (lazy "cannot apply to a Closed goal")
 207                 | Open n ->
 208                    let sn = tac s n in
 209                    let go', gc' = compare_statuses ~past:s ~present:sn in
 210                    sn, ((go @+ [n]) @- gc') @+ go', gc @+ gc'
 211             in
 212             aux s go gc loc_tl
 213       in
 214       let s0, go0, gc0 = status.istatus, [], [] in
 215       let sn, gon, gcn = aux s0 go0 gc0 g in
 216       debug_print (lazy ("opened: "
 217         ^ String.concat " " (List.map string_of_int gon)));
 218       debug_print (lazy ("closed: "
 219         ^ String.concat " " (List.map string_of_int gcn)));
 220       let stack =
 221         (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
 222       in
 223        { gstatus = stack; istatus = sn }
 224 ;;
 225
 226 let atomic_tac htac = distribute_tac (exec htac) ;;
 227
 228 let exact_tac t = distribute_tac (fun status goal ->
 229  let goalty = get_goalty status goal in
 230  let status, t = disambiguate status t (Some goalty) (ctx_of goalty) in
 231  instantiate status goal t)
 232 ;;
 233
 234 let find_in_context name context =
 235   let rec aux acc = function
 236     | [] -> raise Not_found
 237     | (hd,_) :: tl when hd = name -> acc
 238     | _ :: tl ->  aux (acc + 1) tl
 239   in
 240   aux 1 context
 241 ;;
 242
 243 let clear_tac names =
 244  if names = [] then id_tac
 245  else
 246   distribute_tac (fun status goal ->
 247    let goalty = get_goalty status goal in
 248    let js =
 249      List.map
 250      (fun name ->
 251         try find_in_context name (ctx_of goalty)
 252         with Not_found ->
 253           fail (lazy ("hypothesis '" ^ name ^ "' not found")))
 254      names
 255    in
 256    let n,h,metasenv,subst,o = status.pstatus in
 257    let metasenv,subst,_ = NCicMetaSubst.restrict metasenv subst goal js in
 258     { status with pstatus = n,h,metasenv,subst,o })
 259 ;;
 260
 261 let force f s = Lazy.force f s;;
 262
 263 let generalize0_tac args =
 264  if args = [] then id_tac
 265  else exact_tac ("",0,Ast.Appl (Ast.Implicit :: args))
 266 ;;
 267
 268 let select0_tac ~where:(wanted,_,where) ~job  =
 269  let found, postprocess =
 270    match job with
 271    | `Substexpand argsno -> mk_in_scope, mk_out_scope argsno
 272    | `Collect l -> (fun s t -> l := t::!l; mk_in_scope s t), mk_out_scope 1
 273  in
 274  distribute_tac (fun status goal ->
 275    let goalty = get_goalty status goal in
 276    let path =
 277      match where with None -> NCic.Implicit `Term | Some where -> where
 278    in
 279    let status, newgoalty =
 280      select_term status ~found ~postprocess goalty (wanted,path)
 281    in
 282    let status, instance =
 283      mk_meta status (ctx_of newgoalty) (`Decl newgoalty)
 284    in
 285    instantiate status goal instance)
 286 ;;
 287
 288 let select_tac ~where ~job move_down_hyps =
 289  let (wanted,hyps,where) = GrafiteDisambiguate.disambiguate_npattern where in
 290  let path =
 291   match where with None -> NCic.Implicit `Term | Some where -> where in
 292  if not move_down_hyps then
 293   select0_tac ~where:(wanted,hyps,Some path) ~job
 294  else
 295   let path =
 296    List.fold_left
 297      (fun path (name,path_name) -> NCic.Prod ("_",path_name,path))
 298      path (List.rev hyps)
 299   in
 300    block_tac [
 301      generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyps);
 302      select0_tac ~where:(wanted,[],Some path) ~job;
 303      clear_tac (List.map fst hyps) ]
 304 ;;
 305
 306 let generalize_tac ~where =
 307  let l = ref [] in
 308  block_tac [
 309    select_tac ~where ~job:(`Collect l) true;
 310    force (lazy (distribute_tac (fun status goal ->
 311      let goalty = get_goalty status goal in
 312      (* unift (ctx_of goal) t s *)
 313      instantiate status goal
 314        (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ;
 315          term_of_cic_term (List.hd !l) (ctx_of goalty) ]))
 316    ))) ]
 317 ;;
 318
 319
 320 let reopen status =
 321  let n,h,metasenv,subst,o = status.pstatus in
 322  let subst, newm =
 323    List.partition
 324     (function (_,(Some tag,_,_,_)) ->
 325             tag <> NCicMetaSubst.in_scope_tag &&
 326             not (NCicMetaSubst.is_out_scope_tag tag)
 327     | _ -> true)
 328     subst
 329  in
 330  let in_m, out_m =
 331    List.partition
 332      (function (_,(Some tag,_,_,_)) ->
 333          tag = NCicMetaSubst.in_scope_tag | _ -> assert false)
 334      newm
 335  in
 336  let metasenv = List.map (fun (i,(_,c,_,t)) -> i,(None,c,t)) in_m @ metasenv in
 337  let in_m = List.map fst in_m in
 338  let out_m = match out_m with [i] -> i | _ -> assert false in
 339  { status with pstatus = n,h,metasenv,subst,o }, in_m, out_m
 340 ;;
 341
 342 let change ~where ~with_what status goal =
 343 assert false; (*
 344  let goalty = get_goalty status goal in
 345  let (wanted,_,where) = GrafiteDisambiguate.disambiguate_npattern where in
 346  let path =
 347    match where with None -> NCic.Implicit `Term | Some where -> where
 348  in
 349  let status, newgoalty = assert false (*
 350    select_term status 1 goalty (wanted,path)*) in
 351  let status, in_scope, out_scope = reopen status in
 352  let status =  List.fold_left (exact with_what) status in_scope in
 353
 354  let j,(n,cctx,bo,_) = out_scope in
 355  let _ = typeof status (ctx_of goalty) (Obj.magic (n,cctx,bo))  in
 356
 357  let n,h,metasenv,subst,o = status.pstatus in
 358  let subst = out_scope :: subst in
 359  let status = { status with pstatus = n,h,metasenv,subst,o } in
 360
 361  let status, instance =
 362    mk_meta status (ctx_of newgoalty) (`Decl newgoalty)
 363  in
 364  instantiate status goal instance
 365 *)
 366 ;;
 367 let change_tac ~where ~with_what = distribute_tac (change ~where ~with_what) ;;
 368
 369 let apply_tac = exact_tac;;
 370
 371 type indtyinfo = {
 372         rightno: int;
 373         leftno: int;
 374         consno: int;
 375         lefts: NCic.term list;
 376         rights: NCic.term list;
 377         reference: NReference.reference;
 378  }
 379 ;;
 380
 381 let analyze_indty_tac ~what indtyref = distribute_tac (fun status goal ->
 382   let goalty = get_goalty status goal in
 383   let status, what = disambiguate status what None (ctx_of goalty) in
 384   let ty_what = typeof status (ctx_of what) what in
 385   let r,consno,lefts,rights = analyse_indty status ty_what in
 386   let leftno = List.length rights in
 387   let rightno = List.length rights in
 388   indtyref := Some {
 389     rightno = rightno; leftno = leftno; consno = consno;
 390     lefts = lefts; rights = rights; reference = r;
 391   };
 392   exec id_tac status goal)
 393 ;;
 394
 395 let elim_tac ~what ~where =
 396   let indtyinfo = ref None in
 397   let sort = ref None in
 398   let compute_goal_sort_tac = distribute_tac (fun status goal ->
 399     let goalty = get_goalty status goal in
 400     let goalsort = typeof status (ctx_of goalty) goalty in
 401     sort := Some goalsort;
 402     exec id_tac status goal)
 403   in
 404   atomic_tac (block_tac [
 405     analyze_indty_tac ~what indtyinfo;
 406     force (lazy (select_tac
 407       ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true));
 408     compute_goal_sort_tac;
 409     force (lazy (
 410      let sort = HExtlib.unopt !sort in
 411      let ity = HExtlib.unopt !indtyinfo in
 412      let NReference.Ref (uri, _) = ity.reference in
 413      let name = NUri.name_of_uri uri ^
 414       match term_of_cic_term sort (ctx_of sort) with
 415        | NCic.Sort NCic.Prop -> "_ind"
 416        | NCic.Sort _ -> "_rect"
 417        | _ -> assert false
 418      in
 419      let holes =
 420        HExtlib.mk_list Ast.Implicit (ity.leftno+1+ ity.consno + ity.rightno) in
 421      let eliminator =
 422        let _,_,w = what in
 423        Ast.Appl(Ast.Ident(name,None)::holes @ [ w ])
 424      in
 425      exact_tac ("",0,eliminator))) ])
 426 ;;
 427
 428 let rewrite_tac ~dir ~what:(_,_,what) ~where =
 429  let name =
 430   match dir with `LeftToRight -> "eq_elim_r" | `RightToLeft -> "eq_ind"
 431  in
 432   block_tac
 433    [ select_tac ~where ~job:(`Substexpand 1) true;
 434      exact_tac
 435       ("",0,
 436        Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list Ast.Implicit 5 @
 437         [what]))]
 438 ;;
 439
 440 let intro_tac name =
 441  block_tac
 442   [ exact_tac
 443      ("",0,(Ast.Binder (`Lambda,
 444       (Ast.Ident (name,None),None),Ast.Implicit)));
 445     if name = "_" then clear_tac [name] else id_tac ]
 446 ;;
 447
 448 let cases ~what status goal =
 449  let gty = get_goalty status goal in
 450  let status, what = disambiguate status what None (ctx_of gty) in
 451  let ty = typeof status (ctx_of what) what in
 452  let ref, consno, _, _ = analyse_indty status ty in
 453  let t =
 454   NCic.Match (ref,NCic.Implicit `Term, term_of_cic_term what (ctx_of gty),
 455     HExtlib.mk_list (NCic.Implicit `Term) consno)
 456  in
 457  let ctx = ctx_of gty in
 458  let status,t,ty = refine status ctx (mk_cic_term ctx t) (Some gty) in
 459  instantiate status goal t
 460 ;;
 461
 462 let cases_tac ~what ~where =
 463   let indtyinfo = ref None in
 464   atomic_tac
 465    (block_tac [
 466       analyze_indty_tac ~what indtyinfo;
 467       force (lazy (select_tac
 468         ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1))true));
 469       distribute_tac (cases ~what) ])
 470 ;;
 471
 472 let case1_tac name =
 473  let name = if name = "_" then "_clearme" else name in
 474  block_tac [ intro_tac name;
 475              cases_tac
 476               ~where:("",0,(None,[],None))
 477               ~what:("",0,Ast.Ident (name,None));
 478               if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
 479 ;;