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