X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fcontinuationals.ml;h=fd965dddd62a6b7886a092ba8c63431c3d89819c;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=0dc1b75238366a2e8ebda0f6d2c0f768d3050e58;hpb=99db482ebae3e3e4dcc6c4df12027a81bb7a7f76;p=helm.git

diff --git a/helm/ocaml/tactics/continuationals.ml b/helm/ocaml/tactics/continuationals.ml
index 0dc1b7523..fd965dddd 100644
--- a/helm/ocaml/tactics/continuationals.ml
+++ b/helm/ocaml/tactics/continuationals.ml
@@ -23,169 +23,333 @@
  * http://helm.cs.unibo.it/
  *)
 
-exception Error of string 
+open Printf
 
-module L = List
+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 conjecture
-  type metasenv = conjecture list
+  type input_status
+  type output_status
+
   type tactic
 
-  val goal_of_conjecture: conjecture -> goal
-  val goal_mem: goal -> metasenv -> bool
+  val id_tactic : tactic
+  val mk_tactic : (input_status -> output_status) -> tactic
+  val apply_tactic : tactic -> input_status -> output_status
 
-  val apply_tactic:
-    tactic -> metasenv -> goal ->
-      metasenv * 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 Make (E:Engine) =
-struct
-  type goal_switch = Open of E.goal | Closed of E.goal
-  type 'a stack = 'a list
-  type status =
-    E.metasenv * ((int * goal_switch) list * E.goal list * E.goal list) stack
+module type C =
+sig
+  type input_status
+  type output_status
+  type tactic
 
   type tactical =
-    | Tactic of E.tactic
+    | Tactic of tactic
     | Skip
 
   type t =
     | Dot
     | Semicolon
+
     | Branch
-    | Shift of int option
+    | Shift
+    | Pos of int
     | Merge
-    | Select of E.goal list
-    | End_select
+
+    | Focus of goal list
+    | Unfocus
+
     | Tactical of tactical
-    | Qed
 
-  let goal_of = function _, Open g -> g | _, Closed g -> g 
-  let is_open = function _, Open _ -> true | _, Closed _ -> false 
-  let open_all = L.map (fun p, g -> p, Open g)
-    
-  let union a b = a @ b
-  
-  let complementary part full = (* not really efficient *)
-    L.fold_left (fun acc g -> if L.mem g part then acc else g::acc) full []
+  val eval: t -> input_status -> output_status
+end
 
-  let close to_close l =
-    L.map (function p, Open g when L.mem g to_close -> p, Closed g | g -> g) l
+module Make (S: Status) =
+struct
+  open Stack
 
-  let stack_map f g h stack =
-    L.map (fun (a,b,c) -> f a, g b, h c) stack
+  type input_status = S.input_status
+  type output_status = S.output_status
+  type tactic = S.tactic
 
-  let dummy_pos = ~-1
-  let add_dummy_pos g = dummy_pos, g
-  let map_dummy_pos = List.map add_dummy_pos
+  type tactical =
+    | Tactic of tactic
+    | Skip
 
-  let map_open_pos =
-    let rec aux pos =
-      function
-      | [] -> []
-      | g :: tl -> (pos, Open g) :: aux (pos + 1) tl
-    in
-    aux 1
+  type t =
+    | Dot
+    | Semicolon
+    | Branch
+    | Shift
+    | Pos of int
+    | Merge
+    | Focus of goal list
+    | Unfocus
+    | Tactical of tactical
 
-  let eval_tactical tactical metasenv switch =
+  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 -> E.apply_tactic tac metasenv n
-    | Skip, Closed n -> metasenv, [], [n]
-    | Tactic _, Closed _ -> raise (Error "can't apply tactic to a closed goal")
-    | Skip, Open _ -> raise (Error "can't skip an open goal")
-
-  let eval continuational status =
-    match continuational, status with
-    | _, (_, []) -> assert false
-    | Tactical t, (metasenv, (env, todo, left)::tail) ->
-        assert (L.length env > 1);
-        let metasenv, opened, closed =
-          L.fold_left 
-            (fun (metasenv, opened, closed) cur_goal ->
-              if L.exists ((=) (goal_of cur_goal)) closed then
-                metasenv, opened, closed 
-              else
-                let metasenv, newopened, newclosed = 
-                  eval_tactical t metasenv (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
-                metasenv, 
-                union (complementary newclosed opened) newopened,
-                union closed newclosed
-            ) (metasenv, [],[]) env
-        in
-        let pos = ref 0 in
-        let stack_opened = List.map (fun g -> incr pos; !pos, g) opened in
-        metasenv, 
-        (open_all stack_opened,
-         complementary closed todo,
-         complementary opened left)
-        :: stack_map
-            (close closed) (complementary closed) (complementary opened) tail 
-    | Semicolon, (metasenv, stack) -> metasenv, stack
-    | Dot, (metasenv, (env, todo, left)::tail) ->
-        let env, left = 
-          match L.filter is_open env, left with 
-          | [], [] -> raise (Error "There is nothig to do for '.'")
-          | g::env,left -> [g], union (L.map goal_of env) left
-          | [], g::left -> [dummy_pos, Open g], left
-        in
-        metasenv, (env, todo, left)::tail
-    | Branch, (metasenv, (g1::tl, todo, left)::tail) ->
-        assert (L.length tl >= 1);
-        metasenv, ([g1], [], [])::(tl, todo, left)::tail
-    | Branch, (_, _) -> raise (Error "can't branch on a singleton context")
-    | Shift opt_pos, (metasenv, (leftopen, t, l)::(goals, todo, left)::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 (Printf.sprintf "position %d not found" pos)))
-          | None, [] -> raise (Error "no more goals to shift")
-        in
-        let t = union t (union (L.map goal_of (L.filter is_open leftopen)) l) in
-        metasenv, ([next_goal], t, [])::(rem_goals, todo,left)::tail
-    | Shift _, (_, _) -> raise (Error "no more goals to shift")
-    | Merge, (metasenv, (leftopen,t,l)::(not_processed,todo,left)::tail) -> 
-        let env = 
-          (union (open_all (map_dummy_pos t))
-            (union (open_all (map_dummy_pos l))
-              (union not_processed (L.filter is_open leftopen ))))
-        in
-        metasenv, (env,todo,left)::tail
-    | Merge, (_, [_]) -> raise (Error "can't merge here")
-    | Select gl, (metasenv, stack) ->
-        List.iter
-          (fun g -> if not (E.goal_mem g metasenv) then 
-            raise (Error "you can't select a closed goal")) gl;
-        (metasenv, (open_all (map_dummy_pos gl),[],[])::stack)
-    | End_select, (metasenv, stack) ->
-        (match stack with 
-        | ([], [], [])::tail -> metasenv, tail
-        | _ -> raise (Error "select left some goals open"))
-    | Qed, (metasenv, [[], [], []]) -> status
-    | Qed, _ -> raise (Error "can't qed an unfinished proof")
-
-  let init metasenv =
-    metasenv,
-    [ map_open_pos (List.map E.goal_of_conjecture metasenv),  [], [] ]
+                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