+++ /dev/null
-(* Copyright (C) 2005, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-(* $Id$ *)
-
-open Printf
-
-let debug = false
-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 goal = ProofEngineTypes.goal
-
-module Stack =
-struct
- type switch = Open of goal | Closed of goal
- type locator = int * switch
- type tag = [ `BranchTag | `FocusTag | `NoTag ]
- type entry = locator list * locator list * locator list * tag
- type t = entry list
-
- let empty = [ [], [], [], `NoTag ]
-
- let fold ~env ~cont ~todo init stack =
- let rec aux acc depth =
- function
- | [] -> acc
- | (locs, todos, conts, tag) :: tl ->
- let acc = List.fold_left (fun acc -> env acc depth tag) acc locs in
- let acc = List.fold_left (fun acc -> cont acc depth tag) acc conts in
- let acc = List.fold_left (fun acc -> todo acc depth tag) acc todos in
- aux acc (depth + 1) tl
- in
- assert (stack <> []);
- aux init 0 stack
-
- let iter ~env ~cont ~todo =
- fold ~env:(fun _ -> env) ~cont:(fun _ -> cont) ~todo:(fun _ -> todo) ()
-
- let map ~env ~cont ~todo =
- let depth = ref ~-1 in
- List.map
- (fun (s, t, c, tag) ->
- incr depth;
- let d = !depth in
- env d tag s, todo d tag t, cont d tag c, tag)
-
- let is_open = function _, Open _ -> true | _ -> false
- let close = function n, Open g -> n, Closed g | l -> l
- let filter_open = List.filter is_open
- let is_fresh = function n, Open _ when n > 0 -> true | _ -> false
- let goal_of_loc = function _, Open g | _, Closed g -> g
- let goal_of_switch = function Open g | Closed g -> g
- let switch_of_loc = snd
-
- let zero_pos = List.map (fun g -> 0, Open g)
-
- let init_pos locs =
- let pos = ref 0 in (* positions are 1-based *)
- List.map (function _, sw -> incr pos; !pos, sw) locs
-
- let extract_pos i =
- let rec aux acc =
- function
- | [] -> fail (lazy (sprintf "relative position %d not found" i))
- | (i', _) as loc :: tl when i = i' -> loc, (List.rev acc) @ tl
- | hd :: tl -> aux (hd :: acc) tl
- in
- aux []
-
- let deep_close gs =
- let close _ _ =
- List.map (fun l -> if List.mem (goal_of_loc l) gs then close l else l)
- in
- let rm _ _ = List.filter (fun l -> not (List.mem (goal_of_loc l) gs)) in
- map ~env:close ~cont:rm ~todo:rm
-
- let rec find_goal =
- function
- | [] -> raise (Failure "Continuationals.find_goal")
- | (l :: _, _ , _ , _) :: _ -> goal_of_loc l
- | ( _ , _ , l :: _, _) :: _ -> goal_of_loc l
- | ( _ , l :: _, _ , _) :: _ -> goal_of_loc l
- | _ :: tl -> find_goal tl
-
- let is_empty =
- function
- | [] -> assert false
- | [ [], [], [], `NoTag ] -> true
- | _ -> false
-
- let of_metasenv metasenv =
- let goals = List.map (fun (g, _, _) -> g) metasenv in
- [ zero_pos goals, [], [], `NoTag ]
-
- let head_switches =
- function
- | (locs, _, _, _) :: _ -> List.map switch_of_loc locs
- | [] -> assert false
-
- let head_goals =
- function
- | (locs, _, _, _) :: _ -> List.map goal_of_loc locs
- | [] -> assert false
-
- let head_tag =
- function
- | (_, _, _, tag) :: _ -> tag
- | [] -> assert false
-
- let shift_goals =
- function
- | _ :: (locs, _, _, _) :: _ -> List.map goal_of_loc locs
- | [] -> assert false
- | _ -> []
-
- let open_goals stack =
- let add_open acc _ _ l = if is_open l then goal_of_loc l :: acc else acc in
- List.rev (fold ~env:add_open ~cont:add_open ~todo:add_open [] stack)
-
- let (@+) = (@) (* union *)
-
- let (@-) s1 s2 = (* difference *)
- List.fold_right
- (fun e acc -> if List.mem e s2 then acc else e :: acc)
- s1 []
-
- let (@~-) locs gs = (* remove some goals from a locators list *)
- List.fold_right
- (fun loc acc -> if List.mem (goal_of_loc loc) gs then acc else loc :: acc)
- locs []
-
- let pp stack =
- let pp_goal = string_of_int in
- let pp_switch =
- function Open g -> "o" ^ pp_goal g | Closed g -> "c" ^ pp_goal g
- in
- let pp_loc (i, s) = string_of_int i ^ pp_switch s in
- let pp_env env = sprintf "[%s]" (String.concat ";" (List.map pp_loc env)) in
- let pp_tag = function `BranchTag -> "B" | `FocusTag -> "F" | `NoTag -> "N" in
- let pp_stack_entry (env, todo, cont, tag) =
- sprintf "(%s, %s, %s, %s)" (pp_env env) (pp_env todo) (pp_env cont)
- (pp_tag tag)
- in
- String.concat " :: " (List.map pp_stack_entry stack)
-end
-
-module type Status =
-sig
- type input_status
- type output_status
-
- type tactic
-
- val id_tactic : tactic
- val mk_tactic : (input_status -> output_status) -> tactic
- val apply_tactic : tactic -> input_status -> output_status
-
- val goals : output_status -> goal list * goal list (** opened, closed goals *)
- val set_goals: goal list * goal list -> output_status -> output_status
- val get_stack : input_status -> Stack.t
- val set_stack : Stack.t -> output_status -> output_status
-
- val inject : input_status -> output_status
- val focus : goal -> output_status -> input_status
-end
-
-module type C =
-sig
- type input_status
- type output_status
- type tactic
-
- type tactical =
- | Tactic of tactic
- | Skip
-
- type t =
- | Dot
- | Semicolon
-
- | Branch
- | Shift
- | Pos of int
- | Merge
-
- | Focus of goal list
- | Unfocus
-
- | Tactical of tactical
-
- val eval: t -> input_status -> output_status
-end
-
-module Make (S: Status) =
-struct
- open Stack
-
- type input_status = S.input_status
- type output_status = S.output_status
- type tactic = S.tactic
-
- type tactical =
- | Tactic of tactic
- | Skip
-
- type t =
- | Dot
- | Semicolon
- | Branch
- | Shift
- | Pos of int
- | Merge
- | Focus of goal list
- | Unfocus
- | Tactical of tactical
-
- let pp_t =
- function
- | Dot -> "Dot"
- | Semicolon -> "Semicolon"
- | Branch -> "Branch"
- | Shift -> "Shift"
- | Pos i -> "Pos " ^ string_of_int i
- | Merge -> "Merge"
- | Focus gs ->
- sprintf "Focus [%s]" (String.concat "; " (List.map string_of_int gs))
- | Unfocus -> "Unfocus"
- | Tactical _ -> "Tactical <abs>"
-
- let eval_tactical tactical ostatus switch =
- match tactical, switch with
- | Tactic tac, Open n ->
- let ostatus = S.apply_tactic tac (S.focus n ostatus) in
- let opened, closed = S.goals ostatus in
- ostatus, opened, closed
- | Skip, Closed n -> ostatus, [], [n]
- | Tactic _, Closed _ -> fail (lazy "can't apply tactic to a closed goal")
- | Skip, Open _ -> fail (lazy "can't skip an open goal")
-
- let eval cmd istatus =
- let stack = S.get_stack istatus in
- debug_print (lazy (sprintf "EVAL CONT %s <- %s" (pp_t cmd) (pp stack)));
- let new_stack stack = S.inject istatus, stack in
- let ostatus, stack =
- match cmd, stack with
- | _, [] -> assert false
- | Tactical tac, (g, t, k, tag) :: s ->
- if g = [] then fail (lazy "can't apply a tactic to zero goals");
- 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
- let s, go', gc' = eval_tactical tac s (switch_of_loc loc) in
- s, (go @- gc') @+ go', gc @+ gc'
- in
- aux s go gc loc_tl
- in
- let s0, go0, gc0 = S.inject 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 @~- gon, tag) :: deep_close gcn s
- in
- sn, stack
- | Dot, ([], _, [], _) :: _ ->
- (* backward compatibility: do-nothing-dot *)
- new_stack stack
- | Dot, (g, t, k, tag) :: s ->
- (match filter_open g, k with
- | loc :: loc_tl, _ -> new_stack (([ loc ], t, loc_tl @+ k, tag) :: s)
- | [], loc :: k ->
- assert (is_open loc);
- new_stack (([ loc ], t, k, tag) :: s)
- | _ -> fail (lazy "can't use \".\" here"))
- | Semicolon, _ -> new_stack stack
- | Branch, (g, t, k, tag) :: s ->
- (match init_pos g with
- | [] | [ _ ] -> fail (lazy "too few goals to branch");
- | loc :: loc_tl ->
- new_stack
- (([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s))
- | Shift, (g, t, k, `BranchTag) :: (g', t', k', tag) :: s ->
- (match g' with
- | [] -> fail (lazy "no more goals to shift")
- | loc :: loc_tl ->
- new_stack
- (([ loc ], t @+ filter_open g, [],`BranchTag)
- :: (loc_tl, t', k', tag) :: s))
- | Shift, _ -> fail (lazy "can't shift goals here")
- | Pos i, ([ loc ], [], [],`BranchTag) :: (g', t', k', tag) :: s
- when is_fresh loc ->
- let loc_i, g' = extract_pos i g' in
- new_stack
- (([ loc_i ], [], [],`BranchTag)
- :: ([ loc ] @+ g', t', k', tag) :: s)
- | Pos i, (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
- let loc_i, g' = extract_pos i g' in
- new_stack
- (([ loc_i ], [], [],`BranchTag)
- :: (g', t' @+ filter_open g, k', tag) :: s)
- | Pos _, _ -> fail (lazy "can't use relative positioning here")
- | Merge, (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
- new_stack ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s)
- | Merge, _ -> fail (lazy "can't merge goals here")
- | Focus [], _ -> assert false
- | Focus gs, s ->
- let stack_locs =
- let add_l acc _ _ l = if is_open l then l :: acc else acc in
- Stack.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;
- new_stack ((zero_pos gs, [], [], `FocusTag) :: deep_close gs s)
- | Unfocus, ([], [], [], `FocusTag) :: s -> new_stack s
- | Unfocus, _ -> fail (lazy "can't unfocus, some goals are still open")
- in
- debug_print (lazy (sprintf "EVAL CONT %s -> %s" (pp_t cmd) (pp stack)));
- S.set_stack stack ostatus
-end
-
projects / helm.git / blobdiff