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 exception Error of string lazy_t
  20 let fail msg = raise (Error msg)
  21
  22 type lowtac_status = {
  23         pstatus : NCic.obj;
  24         lstatus : LexiconEngine.status
  25 }
  26
  27 type lowtactic = lowtac_status * int -> lowtac_status * int list * int list
  28
  29 type tac_status = {
  30         gstatus : Continuationals.Stack.t;
  31         istatus : lowtac_status;
  32 }
  33
  34 type tactic = tac_status -> tac_status
  35
  36 type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
  37
  38 let pp_tac_status status =
  39   prerr_endline (NCicPp.ppobj status.istatus.pstatus)
  40 ;;
  41
  42 open Continuationals.Stack
  43
  44 let dot_tac status =
  45   let new_gstatus =
  46     match status.gstatus with
  47     | [] -> assert false
  48     | ([], _, [], _) :: _ as stack ->
  49         (* backward compatibility: do-nothing-dot *)
  50         stack
  51     | (g, t, k, tag) :: s ->
  52         match filter_open g, k with
  53         | loc :: loc_tl, _ ->
  54              (([ loc ], t, loc_tl @+ k, tag) :: s)
  55         | [], loc :: k ->
  56             assert (is_open loc);
  57             (([ loc ], t, k, tag) :: s)
  58         | _ -> fail (lazy "can't use \".\" here")
  59   in
  60    { status with gstatus = new_gstatus }
  61 ;;
  62
  63 let branch_tac status =
  64   let new_gstatus =
  65     match status.gstatus with
  66     | [] -> assert false
  67     | (g, t, k, tag) :: s ->
  68           match init_pos g with (* TODO *)
  69           | [] | [ _ ] -> fail (lazy "too few goals to branch");
  70           | loc :: loc_tl ->
  71                ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
  72   in
  73    { status with gstatus = new_gstatus }
  74 ;;
  75
  76 let shift_tac status =
  77   let new_gstatus =
  78     match status.gstatus with
  79     | (g, t, k, `BranchTag) :: (g', t', k', tag) :: s ->
  80           (match g' with
  81           | [] -> fail (lazy "no more goals to shift")
  82           | loc :: loc_tl ->
  83                 (([ loc ], t @+ filter_open g @+ k, [],`BranchTag)
  84                 :: (loc_tl, t', k', tag) :: s))
  85      | _ -> fail (lazy "can't shift goals here")
  86   in
  87    { status with gstatus = new_gstatus }
  88 ;;
  89
  90 let pos_tac i_s 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         let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in
  97           ((l_js, t , [],`BranchTag)
  98            :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
  99     | _ -> fail (lazy "can't use relative positioning here")
 100   in
 101    { status with gstatus = new_gstatus }
 102 ;;
 103
 104 let wildcard_tac status =
 105   let new_gstatus =
 106     match status.gstatus with
 107     | [] -> assert false
 108     | ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s
 109        when is_fresh loc ->
 110             (([loc] @+ g', t, [], `BranchTag) :: ([], t', k', tag) :: s)
 111     | _ -> fail (lazy "can't use wildcard here")
 112   in
 113    { status with gstatus = new_gstatus }
 114 ;;
 115
 116 let merge_tac status =
 117   let new_gstatus =
 118     match status.gstatus with
 119     | [] -> assert false
 120     | (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
 121         ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s)
 122     | _ -> fail (lazy "can't merge goals here")
 123   in
 124    { status with gstatus = new_gstatus }
 125 ;;
 126
 127 let focus_tac gs status =
 128   let new_gstatus =
 129     match status.gstatus with
 130     | [] -> assert false
 131     | s -> assert(gs <> []);
 132           let stack_locs =
 133             let add_l acc _ _ l = if is_open l then l :: acc else acc in
 134             fold ~env:add_l ~cont:add_l ~todo:add_l [] s
 135           in
 136           List.iter
 137             (fun g ->
 138               if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
 139                 fail (lazy (sprintf "goal %d not found (or closed)" g)))
 140             gs;
 141           (zero_pos gs, [], [], `FocusTag) :: deep_close gs s
 142   in
 143    { status with gstatus = new_gstatus }
 144 ;;
 145
 146 let unfocus_tac status =
 147   let new_gstatus =
 148     match status.gstatus with
 149     | [] -> assert false
 150     | ([], [], [], `FocusTag) :: s -> s
 151     | _ -> fail (lazy "can't unfocus, some goals are still open")
 152   in
 153    { status with gstatus = new_gstatus }
 154 ;;
 155
 156 let skip_tac status =
 157   let new_gstatus =
 158     match status.gstatus with
 159     | [] -> assert false
 160     | (gl, t, k, tag) :: s ->
 161         let gl = List.map switch_of_loc gl in
 162         if List.exists (function Open _ -> true | Closed _ -> false) gl then
 163           fail (lazy "cannot skip an open goal")
 164         else
 165           ([],t,k,tag) :: s
 166   in
 167    { status with gstatus = new_gstatus }
 168 ;;
 169
 170 let fold_tactic tac status =
 171   match status.gstatus with
 172   | [] -> assert false
 173   | (g, t, k, tag) :: s ->
 174       debug_print (lazy ("context length " ^string_of_int (List.length g)));
 175       let rec aux s go gc =
 176         function
 177         | [] -> s, go, gc
 178         | loc :: loc_tl ->
 179             debug_print (lazy "inner eval tactical");
 180             let s, go, gc =
 181               if List.exists ((=) (goal_of_loc loc)) gc then
 182                 s, go, gc
 183               else
 184                 match switch_of_loc loc with
 185                 | Closed _ -> fail (lazy "cannot apply to a Closed goal")
 186                 | Open n ->
 187                    let s, go', gc' = tac (s,n) in
 188                    s, (go @- gc') @+ go', gc @+ gc'
 189             in
 190             aux s go gc loc_tl
 191       in
 192       let s0, go0, gc0 = status.istatus, [], [] in
 193       let sn, gon, gcn = aux s0 go0 gc0 g in
 194       debug_print (lazy ("opened: "
 195         ^ String.concat " " (List.map string_of_int gon)));
 196       debug_print (lazy ("closed: "
 197         ^ String.concat " " (List.map string_of_int gcn)));
 198       let stack =
 199         (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
 200       in
 201        { gstatus = stack; istatus = sn }
 202 ;;
 203
 204 let compare_menv ~past ~present =
 205   List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i past)) present),
 206   List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
 207 ;;
 208
 209 let apply t (status,goal) =
 210  let uri,height,(metasenv as old_metasenv), subst,obj = status.pstatus in
 211  let name,context,gty = List.assoc goal metasenv in
 212  let metasenv, subst, lexicon_status, t =
 213    GrafiteDisambiguate.disambiguate_nterm (Some gty) status.lstatus context metasenv subst t
 214  in
 215  let subst, metasenv =
 216    (goal, (name, context, t, gty)):: subst,
 217    List.filter(fun (x,_) -> x <> goal) metasenv
 218  in
 219  let open_goals, closed_goals = compare_menv ~past:old_metasenv ~present:metasenv in
 220  let new_pstatus = uri,height,metasenv,subst,obj in
 221
 222    prerr_endline ("termine disambiguato: " ^ NCicPp.ppterm ~context ~metasenv ~subst t);
 223    prerr_endline ("menv:" ^ NCicPp.ppmetasenv ~subst metasenv);
 224    prerr_endline ("subst:" ^ NCicPp.ppsubst subst ~metasenv);
 225    prerr_endline "fine napply";
 226
 227   { lstatus = lexicon_status; pstatus = new_pstatus }, open_goals, closed_goals
 228 ;;
 229
 230 let apply_tac t = fold_tactic (apply t) ;;
 231