+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
+
+open Printf
+
+let debug = true
+let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
+
+exception Error of string lazy_t
+let fail msg = raise (Error msg)
+
+type lowtac_status = {
+ pstatus : NCic.obj;
+ lstatus : LexiconEngine.status
+}
+
+type lowtactic = lowtac_status * int -> lowtac_status * int list * int list
+
+type tac_status = {
+ gstatus : Continuationals.Stack.t;
+ istatus : lowtac_status;
+}
+
+type tactic = tac_status -> tac_status
+
+type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
+
+let pp_tac_status status =
+ prerr_endline (NCicPp.ppobj status.istatus.pstatus)
+;;
+
+open Continuationals.Stack
+
+let dot_tac status =
+ let new_gstatus =
+ match status.gstatus with
+ | [] -> assert false
+ | ([], _, [], _) :: _ as stack ->
+ (* backward compatibility: do-nothing-dot *)
+ stack
+ | (g, t, k, tag) :: s ->
+ match filter_open g, k with
+ | loc :: loc_tl, _ ->
+ (([ loc ], t, loc_tl @+ k, tag) :: s)
+ | [], loc :: k ->
+ assert (is_open loc);
+ (([ loc ], t, k, tag) :: s)
+ | _ -> fail (lazy "can't use \".\" here")
+ in
+ { status with gstatus = new_gstatus }
+;;
+
+let branch_tac status =
+ let new_gstatus =
+ match status.gstatus with
+ | [] -> assert false
+ | (g, t, k, tag) :: s ->
+ match init_pos g with (* TODO *)
+ | [] | [ _ ] -> fail (lazy "too few goals to branch");
+ | loc :: loc_tl ->
+ ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
+ in
+ { status with gstatus = new_gstatus }
+;;
+
+let shift_tac status =
+ let new_gstatus =
+ match status.gstatus with
+ | (g, t, k, `BranchTag) :: (g', t', k', tag) :: s ->
+ (match g' with
+ | [] -> fail (lazy "no more goals to shift")
+ | loc :: loc_tl ->
+ (([ loc ], t @+ filter_open g @+ k, [],`BranchTag)
+ :: (loc_tl, t', k', tag) :: s))
+ | _ -> fail (lazy "can't shift goals here")
+ in
+ { status with gstatus = new_gstatus }
+;;
+
+let pos_tac i_s status =
+ let new_gstatus =
+ match status.gstatus with
+ | [] -> assert false
+ | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
+ when is_fresh loc ->
+ let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in
+ ((l_js, t , [],`BranchTag)
+ :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
+ | _ -> fail (lazy "can't use relative positioning here")
+ in
+ { status with gstatus = new_gstatus }
+;;
+
+let wildcard_tac status =
+ let new_gstatus =
+ match status.gstatus with
+ | [] -> assert false
+ | ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s
+ when is_fresh loc ->
+ (([loc] @+ g', t, [], `BranchTag) :: ([], t', k', tag) :: s)
+ | _ -> fail (lazy "can't use wildcard here")
+ in
+ { status with gstatus = new_gstatus }
+;;
+
+let merge_tac status =
+ let new_gstatus =
+ match status.gstatus with
+ | [] -> assert false
+ | (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
+ ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s)
+ | _ -> fail (lazy "can't merge goals here")
+ in
+ { status with gstatus = new_gstatus }
+;;
+
+let focus_tac gs status =
+ let new_gstatus =
+ match status.gstatus with
+ | [] -> assert false
+ | s -> assert(gs <> []);
+ let stack_locs =
+ let add_l acc _ _ l = if is_open l then l :: acc else acc in
+ fold ~env:add_l ~cont:add_l ~todo:add_l [] s
+ in
+ List.iter
+ (fun g ->
+ if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
+ fail (lazy (sprintf "goal %d not found (or closed)" g)))
+ gs;
+ (zero_pos gs, [], [], `FocusTag) :: deep_close gs s
+ in
+ { status with gstatus = new_gstatus }
+;;
+
+let unfocus_tac status =
+ let new_gstatus =
+ match status.gstatus with
+ | [] -> assert false
+ | ([], [], [], `FocusTag) :: s -> s
+ | _ -> fail (lazy "can't unfocus, some goals are still open")
+ in
+ { status with gstatus = new_gstatus }
+;;
+
+let skip_tac status =
+ let new_gstatus =
+ match status.gstatus with
+ | [] -> assert false
+ | (gl, t, k, tag) :: s ->
+ let gl = List.map switch_of_loc gl in
+ if List.exists (function Open _ -> true | Closed _ -> false) gl then
+ fail (lazy "cannot skip an open goal")
+ else
+ ([],t,k,tag) :: s
+ in
+ { status with gstatus = new_gstatus }
+;;
+
+let fold_tactic tac status =
+ match status.gstatus with
+ | [] -> assert false
+ | (g, t, k, tag) :: s ->
+ debug_print (lazy ("context length " ^string_of_int (List.length g)));
+ let rec aux s go gc =
+ function
+ | [] -> s, go, gc
+ | loc :: loc_tl ->
+ debug_print (lazy "inner eval tactical");
+ let s, go, gc =
+ if List.exists ((=) (goal_of_loc loc)) gc then
+ s, go, gc
+ else
+ match switch_of_loc loc with
+ | Closed _ -> fail (lazy "cannot apply to a Closed goal")
+ | Open n ->
+ let s, go', gc' = tac (s,n) in
+ s, (go @- gc') @+ go', gc @+ gc'
+ in
+ aux s go gc loc_tl
+ in
+ let s0, go0, gc0 = status.istatus, [], [] in
+ let sn, gon, gcn = aux s0 go0 gc0 g in
+ debug_print (lazy ("opened: "
+ ^ String.concat " " (List.map string_of_int gon)));
+ debug_print (lazy ("closed: "
+ ^ String.concat " " (List.map string_of_int gcn)));
+ let stack =
+ (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
+ in
+ { gstatus = stack; istatus = sn }
+;;
+
+
+let apply t (status,goal) =
+ let _,_,metasenv, subst,_ = status.pstatus in
+ let _,context,gty = List.assoc goal metasenv in
+ let metasenv, subst, lexicon_status, t =
+ GrafiteDisambiguate.disambiguate_nterm (Some gty) status.lstatus context metasenv subst t
+ in
+ prerr_endline ("termine disambiguato: " ^ NCicPp.ppterm ~context ~metasenv ~subst t);
+ prerr_endline ("menv:" ^ NCicPp.ppmetasenv ~subst metasenv);
+ prerr_endline ("subst:" ^ NCicPp.ppsubst subst ~metasenv);
+ prerr_endline "fine napply";
+ { status with lstatus = lexicon_status }, [goal], []
+;;
+
+let apply_tac t = fold_tactic (apply t) ;;
+