X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fcontinuationals.ml;h=fd965dddd62a6b7886a092ba8c63431c3d89819c;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=f4f9e34f665be5d106c4b2f68031fa18f23223fe;hpb=8b55faddb06e3c4b0a13839210bb49170939b33e;p=helm.git diff --git a/helm/ocaml/tactics/continuationals.ml b/helm/ocaml/tactics/continuationals.ml index f4f9e34f6..fd965dddd 100644 --- a/helm/ocaml/tactics/continuationals.ml +++ b/helm/ocaml/tactics/continuationals.ml @@ -25,42 +25,174 @@ open Printf -exception Error of string Lazy.t +let debug = false +let debug_print s = if debug then prerr_endline (Lazy.force s) else () -module type Engine = +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 goal - type proof + type input_status + type output_status + type tactic - val is_goal_closed: goal -> proof -> bool - val goals_of_proof: proof -> goal list + val id_tactic : tactic + val mk_tactic : (input_status -> output_status) -> tactic + val apply_tactic : tactic -> input_status -> output_status - val apply_tactic: - tactic -> proof -> goal -> - proof * goal list * goal list -end + 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 -(** like List.assoc returning a pair: binding matching the given key, - * associative list without the returned binding - * @raise Not_found *) -let list_assoc_extract key = - let rec aux acc = - function - | [] -> raise Not_found - | (key', _) as hd :: tl when key = key' -> hd, (List.rev acc @ tl) - | hd :: tl -> aux (hd :: acc) tl - in - aux [] + val inject : input_status -> output_status + val focus : goal -> output_status -> input_status +end module type C = sig - type goal - type proof + type input_status + type output_status type tactic - type status - type tactical = | Tactic of tactic | Skip @@ -70,43 +202,25 @@ sig | Semicolon | Branch - | Shift of int option - | Select of goal list - | End + | Shift + | Pos of int + | Merge - | Tactical of tactical - - val eval: t -> status -> status - val init: proof -> status - - val get_proof: status -> proof - val set_proof: proof -> status -> status + | Focus of goal list + | Unfocus - type goal_switch = Open of goal | Closed of goal - val get_goals: status -> goal_switch list + | Tactical of tactical - val is_completed: status -> bool + val eval: t -> input_status -> output_status end -module Make (E:Engine) = +module Make (S: Status) = struct - type goal = E.goal - type proof = E.proof - type tactic = E.tactic - - type goal_switch = Open of goal | Closed of goal - type 'a stack = 'a list - type stack_tag = BranchTag | SelectTag | NoTag - type stack_entry = - (int * goal_switch) list * goal list * goal list * stack_tag - type status = proof * stack_entry stack - - let get_proof = fst - let set_proof p (_, s) = p, s - let get_goals (_, stack) = - match stack with - | (goals, _, _, _) :: _ -> List.map snd goals - | [] -> assert false + open Stack + + type input_status = S.input_status + type output_status = S.output_status + type tactic = S.tactic type tactical = | Tactic of tactic @@ -116,130 +230,126 @@ struct | Dot | Semicolon | Branch - | Shift of int option - | Select of goal list - | End + | Shift + | Pos of int + | Merge + | Focus of goal list + | Unfocus | Tactical of tactical - let goal_of = function _, Open g -> g | _, Closed g -> g - let is_open = function _, Open _ -> true | _, Closed _ -> false - let open_all = List.map (fun p, g -> p, Open g) - - let union a b = a @ b - - let complementary part full = (* not really efficient *) - List.fold_left (fun acc g -> if List.mem g part then acc else g::acc) - full [] - - let close to_close = - List.map - (function - | p, Open g when List.mem g to_close -> p, Closed g - | g -> g) - - let map_stack f g h = List.map (fun (a,b,c,tag) -> f a, g b, h c, tag) - - let dummy_pos = ~-1 - let add_dummy_pos g = dummy_pos, g - let map_dummy_pos = List.map add_dummy_pos - - let map_open_pos = - let rec aux pos = - function - | [] -> [] - | g :: tl -> (pos, Open g) :: aux (pos + 1) tl - in - aux 1 + 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 " - let eval_tactical tactical proof switch = + let eval_tactical tactical ostatus switch = match tactical, switch with - | Tactic tac, Open n -> E.apply_tactic tac proof n - | Skip, Closed n -> proof, [], [n] - | Tactic _, Closed _ -> raise (Error (lazy "can't apply tactic to a closed goal")) - | Skip, Open _ -> raise (Error (lazy "can't skip an open goal")) - - let eval continuational status = - match continuational, status with - | _, (_, []) -> assert false - | Tactical t, (proof, (env, todo, left,tag)::tail) -> - assert (List.length env > 1); - let proof, opened, closed = - List.fold_left - (fun (proof, opened, closed) cur_goal -> - if List.exists ((=) (goal_of cur_goal)) closed then - proof, opened, closed - else - let proof, newopened, newclosed = - eval_tactical t proof (snd cur_goal) + | 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 - proof, - union (complementary newclosed opened) newopened, - union closed newclosed - ) (proof, [],[]) env - in - let pos = ref 0 in - let stack_opened = List.map (fun g -> incr pos; !pos, g) opened in - proof, - (open_all stack_opened, - complementary closed todo, - complementary opened left, tag) - :: map_stack - (close closed) (complementary closed) (complementary opened) tail - | Semicolon, (proof, stack) -> proof, stack - | Dot, (proof, (env, todo, left, tag)::tail) -> - let env, left = - match List.filter is_open env, left with - | [], [] -> raise (Error (lazy "There is nothig to do for '.'")) - | g::env,left -> [g], union (List.map goal_of env) left - | [], g::left -> [dummy_pos, Open g], left - in - proof, (env, todo, left, tag)::tail - | Branch, (proof, (g1::tl, todo, left, tag)::tail) -> - assert (List.length tl >= 1); - proof, ([g1], [], [], BranchTag)::(tl, todo, left, tag)::tail - | Branch, (_, _) -> raise (Error (lazy "can't branch on a singleton context")) - | Shift opt_pos, (proof, (leftopen, t, l,BranchTag):: - (goals, todo, left,tag)::tail) -> - let next_goal, rem_goals = - match opt_pos, goals with - | None, g1 :: tl -> g1, tl - | Some pos, _ -> - (try - list_assoc_extract pos goals - with Not_found -> raise (Error (lazy (sprintf "position %d not found" pos)))) - | None, [] -> raise (Error (lazy "no more goals to shift")) - in - let t = - union t (union (List.map goal_of (List.filter is_open leftopen)) l) - in - proof, ([next_goal], t, [], BranchTag)::(rem_goals, todo,left,tag)::tail - | Shift _, (_, _) -> raise (Error (lazy "no more goals to shift")) - | Select gl, (proof, stack) -> - List.iter - (fun g -> - if E.is_goal_closed g proof then - raise (Error (lazy "you can't select a closed goal"))) - gl; - (proof, (open_all (map_dummy_pos gl),[],[],SelectTag)::stack) - | End, (proof, stack) -> - (match stack with - | ([], [], [], SelectTag)::tail -> proof, tail - | (leftopen,t,l,BranchTag)::(not_processed,todo,left,tag)::tail -> - let env = - (union (open_all (map_dummy_pos t)) - (union (open_all (map_dummy_pos l)) - (union not_processed (List.filter is_open leftopen)))) - in - proof, (env,todo,left,tag)::tail - | _ -> raise (Error (lazy "can't end here"))) - - let init proof = - proof, - [ map_open_pos (E.goals_of_proof proof), [], [], NoTag ] - - let is_completed = - function - | (_, [[],[],[],NoTag]) -> true - | _ -> false + 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