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 block_tac l status =
 171   List.fold_left (fun status tac -> tac status) status l
 172 ;;
 173
 174 let compare_menv ~past ~present =
 175   List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i past)) present),
 176   List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
 177 ;;
 178
 179 (* Exec and distribute_tac form a retraction pair:
 180     1) exec (distribute_tac low_tac) (s,i) = low_tac (s,i)
 181     2) tac [s]::G = G1::...::Gn::G' && G' is G with some goals closed =>
 182          distribute_tac (exec tac) [s]::G = (G1@...Gn)::G'
 183     3) tac G = distribute_tac (exec tac) G if
 184        tac = distribute_tac lowtac
 185
 186    Note that executing an high tactic on a set of goals may be stronger
 187    than executing the same tactic on those goals, but once at a time
 188    (e.g. the tactic could perform a global analysis of the set of goals)
 189 *)
 190
 191 let exec tac (low_status,g) =
 192   let stack = [ [0,Open g], [], [], `NoTag ] in
 193   let _,_,old_metasenv,_,_ = low_status.pstatus in
 194   let status = tac { gstatus = stack ; istatus = low_status } in
 195   let _,_,metasenv,_,_ = status.istatus.pstatus in
 196   let open_goals, closed_goals =
 197     compare_menv ~past:old_metasenv ~present:metasenv
 198   in
 199    status.istatus, open_goals, closed_goals
 200 ;;
 201
 202 let distribute_tac tac status =
 203   match status.gstatus with
 204   | [] -> assert false
 205   | (g, t, k, tag) :: s ->
 206       debug_print (lazy ("context length " ^string_of_int (List.length g)));
 207       let rec aux s go gc =
 208         function
 209         | [] -> s, go, gc
 210         | loc :: loc_tl ->
 211             debug_print (lazy "inner eval tactical");
 212             let s, go, gc =
 213               if List.exists ((=) (goal_of_loc loc)) gc then
 214                 s, go, gc
 215               else
 216                 match switch_of_loc loc with
 217                 | Closed _ -> fail (lazy "cannot apply to a Closed goal")
 218                 | Open n ->
 219                    let s, go', gc' = tac (s,n) in
 220                    s, (go @- gc') @+ go', gc @+ gc'
 221             in
 222             aux s go gc loc_tl
 223       in
 224       let s0, go0, gc0 = status.istatus, [], [] in
 225       let sn, gon, gcn = aux s0 go0 gc0 g in
 226       debug_print (lazy ("opened: "
 227         ^ String.concat " " (List.map string_of_int gon)));
 228       debug_print (lazy ("closed: "
 229         ^ String.concat " " (List.map string_of_int gcn)));
 230       let stack =
 231         (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
 232       in
 233        { gstatus = stack; istatus = sn }
 234 ;;
 235
 236 (* attempt....
 237 type cic_term = NCic.conjecture
 238 type ast_term = CicNotationPt.term
 239 type position = Ctx of NCic.context | Term of cic_term
 240
 241 let relocate (name,ctx,t as term) context =
 242   if ctx = context then term else assert false
 243 ;;
 244
 245 let disambiguate (status : lowtac_status) (t : ast_term)
 246                  (ty : cic_term option) (where : position) =
 247  let uri,height,metasenv,subst,obj = status.pstatus in
 248  let context = match where with Ctx c -> c | Term (_,c,_) -> c in
 249  let expty =
 250    match ty with
 251    | None -> None | Some ty -> let _,_,x = relocate ty context in Some x
 252  in
 253  let metasenv, subst, lexicon_status, t =
 254    GrafiteDisambiguate.disambiguate_nterm expty
 255     status.lstatus context metasenv subst t
 256  in
 257  let new_pstatus = uri,height,metasenv,subst,obj in
 258  { lstatus = lexicon_status; pstatus = new_pstatus }, (None, context, t)
 259 ;;
 260
 261 let get_goal (status : low_status) (g : int) =
 262  let _,_,metasenv,_,_ = status.pstatus in
 263  List.assoc goal metasenv
 264 ;;
 265
 266 let return ~orig status =
 267  let _,_,past,_,_ = orig.pstatus in
 268  let _,_,present,_,_ = status.pstatus in
 269  let open_goals, closed_goals = compare_menv ~past ~present in
 270  status, open_goals, closed_goals
 271 ;;
 272
 273 let apply t (status as orig,goal) =
 274  let goal = get_goal status goal in
 275  let status, t = disambiguate status t goal (Term goal) in
 276  let subst, metasenv =
 277    (goal, (name, context, t, gty)):: subst,
 278    List.filter(fun (x,_) -> x <> goal) metasenv
 279  in
 280  return ~orig status
 281 ;;
 282
 283 *)
 284
 285
 286 let apply t (status,goal) =
 287  let uri,height,(metasenv as old_metasenv), subst,obj = status.pstatus in
 288  let name,context,gty = List.assoc goal metasenv in
 289  let metasenv, subst, lexicon_status, t =
 290    GrafiteDisambiguate.disambiguate_nterm (Some gty)
 291     status.lstatus context metasenv subst t
 292  in
 293  let subst, metasenv =
 294    (goal, (name, context, t, gty)):: subst,
 295    List.filter(fun (x,_) -> x <> goal) metasenv
 296  in
 297  let open_goals, closed_goals =
 298    compare_menv ~past:old_metasenv ~present:metasenv in
 299  let new_pstatus = uri,height,metasenv,subst,obj in
 300
 301    prerr_endline ("termine disambiguato: " ^
 302      NCicPp.ppterm ~context ~metasenv ~subst t);
 303    prerr_endline ("menv:" ^ NCicPp.ppmetasenv ~subst metasenv);
 304    prerr_endline ("subst:" ^ NCicPp.ppsubst subst ~metasenv);
 305    prerr_endline "fine napply";
 306
 307   { lstatus = lexicon_status; pstatus = new_pstatus }, open_goals, closed_goals
 308 ;;
 309
 310 let apply_tac t = distribute_tac (apply t) ;;
 311