open Gui

(* functorに渡す引数の型: ユーザが定義したモジュール *)
module type NODE_SIG =
sig
  type fix_t
  val draw : fix_t -> id_t
  (* val clear : fix_t -> bool *)
  val unify : fix_t -> fix_t -> unit
  (* val search : fix_t -> bool  *)
  (* val resubst : fix_t -> fix_t -> bool *)
end

module F (Node : NODE_SIG) = struct 

(* 内部で保持している証明木の型 *)
type tree_t =
    Axiom of Node.fix_t		(* 結論部 *)
	   * id_t		(* この推論規則に対応する GUI object *)
  | Infer of Node.fix_t		(* 結論部 *)
	   * tree_t list	(* 前提部のリスト *)
	   * id_t		(* この推論規則に対応する GUI object *)

let get_id tree = match tree with
    Axiom (_, id) | Infer (_, _, id) -> id

let display_tree tree = Gui.display (get_id tree)

let rec move (x, y) tree = match tree with
    Axiom (fix, id) -> Axiom (fix, Gui.move (x, y) id)
  | Infer (fix, fixes, id) ->
      Infer (fix, List.map (move (x, y)) fixes, Gui.move (x, y) id)

(* tree を作っている最中に on the fly で id を作るのは無理 *)
(* 規則を適用して unification が起きると、そこら中で書き変わるから *)
(* よって一度 unification をして木を更新してから draw し直す必要あり *)

let axiom fix = Axiom (fix, Node.draw fix)

(* re-arrange items horizontally *)
let rec combine_list x fixes gap max_y = match fixes with
    [] -> []
  | fix :: rest ->
      let (x0, y0, x1, y1) = get_coord (get_id fix) in
      move (x - x0, max_y - (y1 - y0)) fix
      :: combine_list (x + (x1 - x0) + gap) rest gap max_y

let rec get_max_x fixes = match fixes with
    [] -> 0
  | [fix] ->
      let (_, _, x1, _) = get_coord (get_id fix) in
      x1
  | fix :: rest -> get_max_x rest

let rec get_max_y fixes max_y = match fixes with
    [] -> max_y
  | fix :: rest ->
      let (_, y0, _, y1) = get_coord (get_id fix) in
      get_max_y rest (max max_y (y1 - y0))

(*
let combine_des ids gap =
  let max_y = get_max_y ids 1 in
  let lst = combine_list 0 ids gap max_y in
  let max_x = get_max_x lst in
  H (lst, (0, 0, max_x, max_y))

let combineH ids = combine_des ids 0
*)

let infer fix premises =
  let max_y = get_max_y premises 1 in
  let lst = combine_list 0 premises 1 max_y in
  let max_x = get_max_x lst in
  let premises_id = H (List.map get_id lst, (0, 0, max_x, max_y)) in
  let id = combineV premises_id (Node.draw fix) in
  Infer (fix, lst, id)
(* lst: 中身を全て正しく move したもの *)
(* id : premises の ids を combineH して、fix' の id と combineV したもの *)

(********** ユーザ定義の規則を tree_t 型に変更する **********)
let rec change r = match r with
    Gui.Axiom (j) ->
      axiom j
      (* Axiom (j, Node.draw j) *)
  | Gui.Infer (j, lst) ->
      infer j (List.map change lst)
      (*
      let lst2 = List.map change lst in
      let ids = List.map get_id lst2 in
      Infer (j, lst2, combineV (combineH ids) (Node.draw j))
      *)

exception ApplyRule of string

let rec apply_rule tree (x, y) rule =
  if not (inside (x, y) (get_id tree)) then raise (ApplyRule "not inside") else
  match tree with
      Axiom (_, _) -> raise (ApplyRule "axiom")
    | Infer (fix, [], _) -> (* これが規則を適用する場所 *)
	(match rule with
	    Gui.Axiom (judge) ->
	      Node.unify fix judge;
	      change rule
	  | Gui.Infer (judge, premises) ->
	      Node.unify fix judge;
	      change rule)
    | Infer (fix, lst, _) -> (* lst の中から (x, y) を探す *)
	infer fix (find_apply lst (x, y) rule)
and find_apply lst (x, y) rule = match lst with
    [] -> []
  | tree :: rest ->
      if inside (x, y) (get_id tree)
      then apply_rule tree (x, y) rule :: rest
      else tree :: find_apply rest (x, y) rule

let rec reconstruct tree = match tree with
    Axiom (fix, _) -> axiom fix
  | Infer (fix, fixes, _) ->
      infer fix (List.map reconstruct fixes)

let launch_gui parse infer_rule_list =
  let fix = parse "fun x -> x" in
  let tree = infer fix [] in
  let tree = reconstruct tree in
  display_tree tree;
  let tree = apply_rule tree (1, 2) (List.assoc "TABS" infer_rule_list ()) in
  let tree = reconstruct tree in
  display_tree tree;
  let tree = apply_rule tree (1, 2) (List.assoc "TVAR" infer_rule_list ()) in
  let tree = reconstruct tree in
  display_tree tree;
  let tree = apply_rule tree (1, 2) (List.assoc "TEQUAL" infer_rule_list ()) in
  let tree = reconstruct tree in
  display_tree tree
(*
  display_tree tree;
  let tree = apply_rule tree (1, 2) (List.assoc "MP" infer_rule_list ()) in
  let tree = reconstruct tree in
  display_tree tree;
  let tree = apply_rule tree (7, 2) (List.assoc "MP" infer_rule_list ()) in
  let tree = reconstruct tree in
  display_tree tree;
  let tree = apply_rule tree (9, 2) (List.assoc "S" infer_rule_list ()) in
  let tree = reconstruct tree in
  display_tree tree;
  let tree = apply_rule tree (0, 4) (List.assoc "K" infer_rule_list ()) in
  let tree = reconstruct tree in
  display_tree tree;
  let tree = apply_rule tree (20, 2) (List.assoc "K" infer_rule_list ()) in
  let tree = reconstruct tree in
  display_tree tree
*)
   
(*
  let init_tree = Infer (parse "(A -> B) -> (B -> C) -> (A -> C)",
			 "", [], ref None) in
  ()
  *)

(*

  (********** 定義 **********)
  type rule_t =  
      MEmpty 
    | MAxiom of Node.fix_t * id_t
    | MInfer of Node.fix_t * rule_t list * id_t
  type trule_t = 
    | TInfer of (unit -> Node.fix_t prule_t) * (trule_t list)
    | TEmpty

  (* データ保存用 *)
  let save_rule = ref MEmpty
  let save_trule = ref [TEmpty]
  let init() = save_rule := MEmpty; save_trule := [TEmpty]
    (*let save_draw = ref MEmpty*)

  (********** idを取り出す **********)	
  let get_rule_id t = match t with
      MAxiom(_,id) | MInfer(_,_,id) -> id
    | MEmpty -> NEW

  (* treeの中で推論出来るものを集めてくる関数 tree_t -> id_t list *)
  let collect_tree () =
    let rec loop res tree = match tree with
	(* 一番上にあるjudgeの未適応部分を集めてくる *)
	MEmpty -> []
      | MInfer(_,[], id) -> id :: res
      | MInfer(_, lst, _) -> List.fold_left loop res lst
      | _ -> res
    in loop [] !save_rule (*!save_draw *)

(********** ユーザ定義から変更する **********)
let rec change r = match r with
    Infer(j, lst) -> MInfer(j, List.map change lst, NEW)
  | Axiom(j) -> MAxiom(j, NEW)

(********** 空の木を作成する **********)  
let make_empty tree = 
  let rec num_of_child tree = match tree with
      MInfer(_, child, _) -> List.length child
    | MAxiom(_, _) -> 0 
    | MEmpty -> assert false in
  let rec loop num res = 
      if num = 0
      then res
      else loop (num - 1) (TEmpty :: res)
  in loop (num_of_child tree) []

(********** unify **********)
let unify_rule rule_tree judge = match rule_tree with
    MInfer(rule_judge, _, _) | MAxiom(rule_judge, _) -> 
      Node.unify rule_judge judge;
      rule_tree
  | MEmpty -> MEmpty

let subst_rule tree fix1 fix2 = match tree with
    MInfer(j, lst, _) -> Node.resubst fix1 fix2
  | MAxiom(j, _) -> Node.resubst fix1 fix2
  | MEmpty -> true

(********** 規則を挿入する **********)
(* typing : ユーザがクリックした規則（多分）*)
let infer typing =
  mode := OCC;
  let rec loop save_rule save_trule = match (save_rule, save_trule) with
    | (MInfer(j, [], id), TEmpty) -> 
	if judge_inside id
	then 
	  let new_rule = unify_rule (change (typing())) j in
	    (new_rule, TInfer(typing, make_empty new_rule))
	else (save_rule, save_trule)
    | (MInfer(j, child_lst, id), TInfer(r, r_lst)) ->
	if judge_inside id
	then 
	  let (tree_lst, trule_lst) = 
	    List.split(List.map2 loop child_lst r_lst) in
	    (MInfer(j, tree_lst, NEW), TInfer(r, trule_lst))
	else (save_rule, save_trule)
    | _ -> (save_rule, save_trule)
	
  in let (new_rule, new_trule) =
      loop !save_rule (List.hd !save_trule) 
  in save_rule := new_rule ;
    save_trule := new_trule :: !save_trule

(********** 初めから証明木を組み直す **********)
let rec restruct tr =
  let rec loop tree trule = match (tree, trule) with
      (MInfer(judge, [], _), TInfer(r, _)) ->
	loop (unify_rule (change (r())) judge) trule
    | (MInfer(judge, [], _), TEmpty) -> tree
    | (MInfer(judge, child_lst, _), TInfer(r, r_lst)) ->
	MInfer(judge, 
	       List.map2 (fun tree trule -> loop tree trule) child_lst r_lst, NEW)
    | (MInfer _, TEmpty) -> assert false
    | (MAxiom(judge, _), _) -> tree
    | _ -> assert false
  in 
    save_rule := loop (tr) (List.hd !save_trule)

(********** tree_tの描画 **********)
let clear_tree () = 
  mode := CLEAR;
  let rec loop tree = match tree with
      MEmpty -> false
    | MInfer(j, [], _) -> Node.clear j
    | MInfer(j, lst, _) -> 
	let _ = Node.clear j  in
	let _ = List.map loop lst in false
    | MAxiom(j, _) -> 
	Node.clear j 
  in loop !save_rule

let draw_tree () = 
  let rec loop tree = match tree with
      MEmpty -> MEmpty
    | MInfer(j, [], _) -> 
	  let t = Node.draw j in
	    MInfer(j, [], t) 
    | MInfer(j, lst, _) -> 
	let down = Node.draw j in
	let lst' = List.map loop lst in 
	let up_lst = List.map get_rule_id lst' in
	let t = combineV down (combine_des up_lst 30) in
	  MInfer(j,lst', t) 
    | MAxiom(j, _) -> 
	let axm = Node.draw j in
	let t = combineV_axm axm in
	  MAxiom(j, t)
  in save_rule := loop !save_rule

(* 描く関数 *)
let draw () = 
  (* Canvas.delete Gui.canvas [`Tag("all")]; キャンバスのアイテムを全て消す *)
  init();
  let _ = clear_tree() in
  draw_tree();
  let un_lst = collect_tree () in
    if List.length un_lst = 0 
    then show_comp()

(* 置換箇所を見つけ、置換を行う *)
let search_elem () = 
  mode := SUB;
  let rec loop tree = match tree with
      MEmpty -> false
    | MInfer(j, lst, id) ->
	if (check id)
	then 
	  (if (Node.search j)
	   then true
	   else 
	     let rec loop2 lst = match lst with
		 [] -> false
	       | first :: rest -> if loop first then true else loop2 rest
	     in loop2 lst)
	else false
    | MAxiom(j, id) -> 
	if check id
	then Node.search j
	else false
  in delete_bbox (); 
    if !save_rule (*!save_draw*) <> MEmpty
    then loop !save_rule 
      (*if loop !save_rule (*!save_draw*)	
      then draw(); true *)
    else false 

(********** Undoを作成する **********)
let undo init = 
  if List.length !save_trule > 1
  then 
    (save_trule := (List.tl !save_trule); restruct init; draw())

(* マウスが動いた時の動作 *)
  let create_bbox_tree () =
    let rec loop tree = match tree with
	(* 一番上にあるjudgeの未適応部分を集めてくる *)
	MEmpty -> false
      | MInfer(_, [], id) -> create_bbox [id]
      | MInfer(_, lst, _) -> 
	  let rec loop2 lst = match lst with
	      [] -> false
	    | first :: rest -> if loop first then true else loop2 rest
	  in loop2 lst
      | _ -> false
    in delete_bbox (); 
      if !save_rule (*!save_draw*) <> MEmpty 
      then loop !save_rule (* !save_draw *)
      else false

  (* 登録関数を作成する *)
  let regist_infer_button rlist = 
    List.iter (fun (str, f) -> 
		 create_button str (fun _ -> infer f; draw())) rlist

  (******************* ここから、元 Miki.F *******************)
  exception Parse_Error
  exception Chosen_Some_Items

  (* 初期化関数 *)
  let init () = 
    (* Gui.init(); *)
    init()
    (*  Term.init(); *)
    (* Canvas.delete Gui.canvas [`Tag("all")] *)

  let init_string = ref ""

  (********** メイン関数 **********)
  let launch_gui parse ?(parse_list=[]) infer_rule_list =
    let parse j = Infer (parse j, []) in
    (* ボタン生成 *)
    regist_infer_button infer_rule_list;
    (* トップフレーム *)
    let frame_top = Frame.create Gui.top in
    let ent = Entry.create ~background:`White ~width:50 frame_top in
      Focus.set ent; 
      (* Goボタンの動作 *)
      let b_exe = Button.create ~padx:10 ~text:"Go" ~takefocus:false frame_top
	~command:(fun _ -> 
		    init();
		    let str = Entry.get ent in
		      init_string := str;
		      let loop() = 
			try
			  parse (str^";;")
			      (*
 				Parser.start Lexer.token (Lexing.from_string (str^";;")) 
			      *)
			with Failure(_) | Parsing.Parse_error -> 
			  ((ignore (messageBox ~default:"ok" ~icon:`Warning 
				      ~message:"False! \n Unknown token." 
				      ~parent:Gui.top ~title:"Warning" ~typ:`Ok ()));
			   raise Parse_Error)
		      in save_rule := change (loop ());
		    draw ()
		      
		 (*		  tm := Term.draw !tm*)
		 ) in

	(* undoボタン *)
	Gui.create_button_low "Undo" 
	  (fun _ -> 
	     (* Term.init(); *)
	     undo (change (parse (!init_string^";;"))));
	(* Parser.start Lexer.token 
	   (Lexing.from_string (!init_string^";;")) *)

	(* newボタン *)
	Gui.create_button_low "New" (fun _ -> init ()) ;
	
	let label = Label.create ~text:"Expression" frame_top in

	  (* クリックしてbboxを表示/非表示 *)
	  bind Gui.canvas 
	    (*~extend:true*) ~breakable:false ~events:[`ButtonPress](*[`Motion]*)
	    ~fields:[`MouseX; `MouseY]
	    ~action:(fun ev -> 
		       Gui.coord_x := int_of_float (Canvas.canvasx ~x:ev.ev_MouseX Gui.canvas);
		       Gui.coord_y := int_of_float(Canvas.canvasy ~y:ev.ev_MouseY Gui.canvas);
		       let _ = create_bbox_tree() in ());

	  (* スクロールバー *)
	  let xsbar = Scrollbar.create (Winfo.parent Gui.canvas) 
	    ~orient:`Horizontal ~takefocus:false 
	    ~command:(fun ~scroll:sv -> Canvas.xview Gui.canvas ~scroll:sv ) in
	    
	  let ysbar = Scrollbar.create (Winfo.parent Gui.canvas) ~orient:`Vertical 
	    ~takefocus:false
	    ~command:(Canvas.yview Gui.canvas) in 
     
	    Canvas.configure ~xscrollcommand:( Scrollbar.set xsbar ) 
	      ~yscrollcommand:(Scrollbar.set ysbar) Gui.canvas;

	(* 終了確認 *)
	    let quit() = 
	  let n = Dialog.create ~parent:Gui.top ~title:"confirmation"
	    ~message:"Finish Miki?" ~buttons:["Yes"; "No"] () in
	    if n = 0
	    then closeTk()
	    else ()
	    in

	    (* 環境設定 *)
	    let config() =
	      let top2 =Toplevel.create Gui.top ~width:240 ~height:400 in
		Wm.resizable_set top2 ~width:false ~height:false;

		(* 文字の大きさ *)
	 let font_frame = Frame.create ~relief:`Groove ~borderwidth:2 top2 in
	 let font_label = Label.create ~text:"Font" ~foreground:`Blue top2 in
	 let frame1 = Frame.create font_frame in
	 let label1 = Label.create ~text:"Size" frame1 in
	 let scale = Scale.create ~max:50. ~min:5. ~width:10 ~length:200
	   ~orient:`Horizontal ~relief:`Sunken
	   ~variable:(Textvariable.create ~on:font_frame ()) 
	   ~command:(fun num -> 
		       Gui.font := ("Century "^ (string_of_int (int_of_float num)));
		       if !save_rule <> MEmpty
		       then draw ())
	   frame1 in
	   Scale.set scale (float_of_int (Font.actual_size !Gui.font)); 
	   (* 文字の色 *)
	   let frame2 = Frame.create font_frame in
	   let label2 = Label.create ~text:"Color" frame2 in
	   let color = Textvariable.create () in	 
	   let color_string var = 
	     Textvariable.set var (match !Gui.font_color with
				       `Black -> "Black"
				     | `Blue -> "Blue"
				     | `Color(str) -> str
				     | `Green -> "Green"
				     | `Red -> "Red"
				     | `White -> "White"
				     | `Yellow -> "Yellow"); var in
	   let current_color = 
	     Label.create ~foreground:!Gui.font_color 
	       ~textvariable:(color_string color) frame2 in
	   let button1 = Button.create 
	     ~command:(fun () -> 
			 let font_color = chooseColor ~initialcolor:!Gui.font_color 
			   ~parent:frame2 ~title:"select a font_color" () in
			   Gui.font_color := font_color;
			   Label.configure ~foreground:!Gui.font_color current_color;
			   let _ = color_string color in 
			     if !save_rule <> MEmpty
			     then draw ()
		      ) ~text:"select color ..." frame2 in

	   let ok = Button.create ~text:"ok" ~command:(fun _ -> destroy top2)  top2 in
	     pack ~side:`Left  ~padx:5 [coe label1; coe scale];
	     pack ~side:`Left  ~padx:5 [coe label2; coe current_color; coe button1];
	     pack ~side:`Top ~anchor:`W [coe font_label; coe frame1; coe frame2];
	     pack ~side:`Top ~anchor:`W [coe font_frame; coe ok];
	     Tkwait.window top2 (* Gui.topを待機させる *) in

	(* ファイルを開く *)
	let op() = (* idをどうにかする必要がありそう...? *)
	  let file = 
	    getOpenFile ~filetypes:[
	      {typename="Miki Files"; extensions=[".miki"]; mactypes=["*.miki"]};		
	      {typename="All Files"; extensions=[".*"]; mactypes=["*.*"]}
	    ] () in 
	  let in_channel = open_in file in
	  let data = input_value in_channel in
	 save_rule := data;
	 draw ();
	 close_in in_channel in

     (* 保存をする *)
     let save () = 
       let file = 
	 getSaveFile ~filetypes:[
	   {typename="Miki Files"; extensions=[".miki"]; mactypes=["*.miki"]};		
	   {typename="All Files"; extensions=[".*"]; mactypes=["*.*"]}
	 ] () in 
       let out_channel = open_out file in
	 (*output_value out_channel !Rule.save_rule;*)
	 close_out out_channel in

     (* メニュー *)
     let menu = Menu.create ~takefocus:false ~typ:`Menubar Gui.top in

       (* Mikiのメニュー *)
     let miki = Menu.create ~tearoff:false menu in
       Menu.add_cascade ~label:"Miki" ~menu:miki ~underline:0 menu;
       Menu.add_command ~label:"About Miki"  ~underline:0 
	 ~command:(fun _ -> 
		     let _ = messageBox ~default:"ok" ~icon:`Info
			~message:"This is a Miki β. \n To write a beautiful prove-tree." 
			~parent:Gui.top ~title:"Warning" ~typ:`Ok () in
		     ()) miki;
       Menu.add_command ~label:"Preferences..."  ~underline:0 ~command:(fun _ -> config()) miki;
       Menu.add_command ~label:"Quit" ~underline:0 ~command:quit
	 ~accelerator:"Ctl-Q" miki;

       (* fileのメニュー *)
     let file = Menu.create ~tearoff:false menu in
       Menu.add_cascade ~label:"File" ~menu:file ~underline:0 menu;
       Menu.add_command ~label:"New"  ~underline:0 ~command: (fun _ -> init ()) 
	 ~accelerator:"Ctl-N" file;
       Menu.add_command ~label:"Open..."  ~underline:0 ~command:(fun _ -> op()) 
	 ~accelerator:"Ctl-O" file;
       Menu.add_command ~label:"Save..." ~underline:0 
	 ~command:(fun _ -> save()) 
	 ~accelerator:"Ctl-S" file;

       (* ショートカットの登録 *)
       bind ~events:[`Modified([`Control], `KeyPressDetail("q"))]
	 ~action:(fun _ -> quit()) Gui.top;
       bind ~events:[`Modified([`Control], `KeyPressDetail("n"))]
	 ~action:(fun _ -> init() ) Gui.top;
       bind ~events:[`Modified([`Control], `KeyPressDetail("s"))]
	 ~action:(fun _ -> save()) Gui.top;
       bind ~events:[`Modified([`Control], `KeyPressDetail("o"))]
	 ~action:(fun _ -> op()) Gui.top;

       (* 配置 *)
       Toplevel.configure ~menu:menu Gui.top; 
(*       let str = ref "" in *)

       (* 入力ダイアログ *)
  (*     let entry_dialog () = 
	 let top2 = Toplevel.create top in
	 let message = Label.create top2 
	   ~text:"Enter a substitution term." ~width:20 in
	 let ent = Entry.create top2 ~width:20 in
	 let qbutton = Button.create ~takefocus:false ~text:"OK" top2
	   ~command:(fun () -> str := Entry.get ent;
			destroy top2) in
	   pack [coe message; coe ent; coe qbutton];
	   Tkwait.window top2;
       in *)

       (* 右クリックをした時の動作 *)
      bind Gui.canvas ~extend:true 
	~events:[`Modified([`Control],`ButtonPress)]
	~fields:[`MouseX; `MouseY]
	~action:(fun ev ->
		   Gui.coord_x := int_of_float (Canvas.canvasx ~x:ev.ev_MouseX Gui.canvas) ;
		   Gui.coord_y := int_of_float(Canvas.canvasy ~y:ev.ev_MouseY Gui.canvas) ;
		   (*    entry_dialog(); *)
		   let _ =search_elem () in draw ()(*(!str ^ ";;")*)); 

    (* Gui.create_button "aaa" (fun _ -> ()); テスト...*)
    (* 配置する 初めに置いたものが残る *)
    pack ~expand:false ~fill:`X [coe frame_top]; 
    pack ~anchor:`W [Gui.user_frame];
    pack ~expand:true ~fill:`Both [Gui.frame_cv];
    pack ~expand:false ~fill:`X [coe Gui.frame_bottom];
    pack ~side:`Left [coe label; coe ent; coe b_exe];
    Grid.column_configure ~weight:1 ~minsize:100 Gui.frame_cv 0;
    Grid.row_configure ~weight:1 ~minsize:100 Gui.frame_cv 0;
    grid ~column:0 ~row:0 ~sticky:"nsew" [Gui.canvas];     (*row:行 column:列*)
    grid ~column:1 ~row:0 ~sticky:"ns" [ysbar];
    grid ~column:0 ~row:1 ~sticky:"ew" [xsbar]; 
    pack ~ipadx:10 ~padx:10 ~side:`Left [coe Gui.b_quit];      
    mainLoop ()

*)

end