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