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 type cic_term = NCic.conjecture
 237 type ast_term = string * int * CicNotationPt.term
 238 type position = Ctx of NCic.context | Term of cic_term
 239
 240
 241 let relocate (name,ctx,t as term) context =
 242   let is_prefix l1 l2 =
 243     let rec aux = function
 244       | [],[] -> true
 245       | x::xs, y::ys -> x=y && aux (xs,ys)
 246       | _ -> false
 247     in
 248       aux (List.rev l1, List.rev l2)
 249   in
 250   if ctx = context then term else
 251   if is_prefix ctx context then
 252     (name, context,
 253       NCicSubstitution.lift (List.length context - List.length ctx) t)
 254   else
 255     assert false
 256 ;;
 257
 258 let disambiguate (status : lowtac_status) (t : ast_term)
 259                  (ty : cic_term option) (where : position) =
 260  let uri,height,metasenv,subst,obj = status.pstatus in
 261  let context = match where with Ctx c -> c | Term (_,c,_) -> c in
 262  let expty =
 263    match ty with
 264    | None -> None | Some ty -> let _,_,x = relocate ty context in Some x
 265  in
 266  let metasenv, subst, lexicon_status, t =
 267    GrafiteDisambiguate.disambiguate_nterm expty
 268     status.lstatus context metasenv subst t
 269  in
 270  let new_pstatus = uri,height,metasenv,subst,obj in
 271  { lstatus = lexicon_status; pstatus = new_pstatus }, (None, context, t)
 272 ;;
 273
 274 let select_term low_status (name,context,term) (path, matched) =
 275   let eq context (status as old_status) t1 t2 =
 276     let _,_,t2 = relocate t2 context in
 277     if t2 = t1 then true, status else false, old_status
 278   in
 279   let match_term m =
 280     let rec aux ctx status t =
 281       let b, status = eq ctx status t m in
 282       if b then
 283         let n,h,metasenv,subst,o = status.pstatus in
 284         let ty = NCicTypeChecker.typeof ~subst ~metasenv ctx t in
 285         let metasenv, instance, ty =
 286           NCicMetaSubst.mk_meta ~name:"expanded" metasenv ctx (`WithType ty)
 287         in
 288         let metasenv, subst =
 289           NCicUnification.unify (NCicUnifHint.db ()) metasenv subst ctx
 290             t instance
 291         in
 292         let status = { status with pstatus = n,h,metasenv,subst,o } in
 293         status, instance
 294       else NCicUntrusted.map_term_fold_a (fun e c -> e::c) ctx aux status t
 295      in
 296        aux
 297   in
 298   let rec select status ctx pat cic =
 299     match pat, cic with
 300     | NCic.Prod (_,s1,t1), NCic.Prod (n,s2,t2) ->
 301         let status, s = select status ctx s1 s2 in
 302         let ctx = (n, NCic.Decl s2) :: ctx in
 303         let status, t = select status ctx t1 t2 in
 304         status, NCic.Prod (n,s,t)
 305     | NCic.Appl l1, NCic.Appl l2 ->
 306         let status, l =
 307            List.fold_left2
 308              (fun (status,l) x y ->
 309               let status, x = select status ctx x y in
 310               status, l @ [x])
 311              (status,[]) l1 l2
 312         in
 313         status, NCic.Appl l
 314     | NCic.Implicit `Hole, t -> status, t
 315     | NCic.Implicit `Term, t ->
 316         let status, matched = disambiguate status matched None (Ctx ctx) in
 317         match_term matched ctx status t
 318     | _,t -> status, t
 319   in
 320   let status, term = select low_status context path term in
 321   let _,_,_,subst,_ = status.pstatus in
 322   let selections =
 323     HExtlib.filter_map
 324       (function (i,(Some "expanded",c,_,_)) -> Some i | _ -> None)
 325       subst
 326   in
 327   status, (name, context, term), selections
 328 ;;
 329
 330 let get_goal (status : lowtac_status) (g : int) =
 331  let _,_,metasenv,_,_ = status.pstatus in
 332  List.assoc g metasenv
 333 ;;
 334
 335 let return ~orig status =
 336  let _,_,past,_,_ = orig.pstatus in
 337  let _,_,present,_,_ = status.pstatus in
 338  let open_goals, closed_goals = compare_menv ~past ~present in
 339  status, open_goals, closed_goals
 340 ;;
 341
 342 let instantiate status i t =
 343  let name,height,metasenv,subst,obj = status.pstatus in
 344  let _, context, ty = List.assoc i metasenv in
 345  let _,_,t = relocate t context in
 346  let m = NCic.Meta (i,(0,NCic.Irl (List.length context))) in
 347  let db = NCicUnifHint.db () in (* XXX fixme *)
 348  let metasenv, subst = NCicUnification.unify db metasenv subst context m t in
 349  { status with pstatus = (name,height,metasenv,subst,obj) }
 350 ;;
 351
 352 let mkmeta name status (_,ctx,ty) =
 353   let n,h,metasenv,s,o = status.pstatus in
 354   let metasenv, instance, _ =
 355     NCicMetaSubst.mk_meta ?name metasenv ctx (`WithType ty)
 356   in
 357   let status = { status with pstatus = n,h,metasenv,s,o } in
 358   status, (name,ctx,instance)
 359 ;;
 360
 361 let apply t (status as orig, goal) =
 362  let goalty = get_goal status goal in
 363  let status, t = disambiguate status t (Some goalty) (Term goalty) in
 364  let status = instantiate status goal t in
 365  return ~orig status
 366 ;;
 367
 368 let change what (*where*) with_what (status as orig, goal) =
 369  let (name,_,_ as goalty) = get_goal status goal in
 370  let status, newgoalty, selections =
 371    select_term status goalty
 372      (NCic.Prod ("_",NCic.Implicit `Hole,NCic.Implicit `Term), what)
 373  in
 374
 375  let n,h,metasenv,subst,o = status.pstatus in
 376  let subst, newm =
 377    List.partition (fun i,_ -> not (List.mem i selections)) subst
 378  in
 379  let metasenv = List.map (fun (i,(n,c,_,t)) -> i,(n,c,t)) newm @ metasenv in
 380  let status = { status with pstatus = n,h,metasenv,subst,o } in
 381
 382  let status =  (* queste sono apply, usa un tatticale! *)
 383    List.fold_left
 384      (fun status i ->
 385        let x = get_goal status i in
 386        let status, with_what =
 387          disambiguate status with_what (Some x) (Term x)
 388        in
 389        instantiate status i with_what)
 390      status selections
 391  in
 392  let status, m = mkmeta name status newgoalty in
 393  let status = instantiate status goal m in
 394  return ~orig status
 395 ;;
 396
 397 let apply t (status,goal) =
 398  let uri,height,(metasenv as old_metasenv), subst,obj = status.pstatus in
 399  let name,context,gty = List.assoc goal metasenv in
 400  let metasenv, subst, lexicon_status, t =
 401    GrafiteDisambiguate.disambiguate_nterm (Some gty)
 402     status.lstatus context metasenv subst t
 403  in
 404  let subst, metasenv =
 405    (goal, (name, context, t, gty)):: subst,
 406    List.filter(fun (x,_) -> x <> goal) metasenv
 407  in
 408  let open_goals, closed_goals =
 409    compare_menv ~past:old_metasenv ~present:metasenv in
 410  let new_pstatus = uri,height,metasenv,subst,obj in
 411
 412    prerr_endline ("termine disambiguato: " ^
 413      NCicPp.ppterm ~context ~metasenv ~subst t);
 414    prerr_endline ("menv:" ^ NCicPp.ppmetasenv ~subst metasenv);
 415    prerr_endline ("subst:" ^ NCicPp.ppsubst subst ~metasenv);
 416    prerr_endline "fine napply";
 417
 418   { lstatus = lexicon_status; pstatus = new_pstatus }, open_goals, closed_goals
 419 ;;
 420
 421 let apply_tac t = distribute_tac (apply t) ;;
 422 let change_tac w ww = distribute_tac (change w ww) ;;
 423