open Gui

let input_str = ref ""
let input_dialog () = ()
let create_bbox _ = true
exception Cannot_take
exception Unify_Error of string

(********** definition of two level types **********)
(********** ファンクターの引数の型 **********)
module type STRUCTURE_SIG =
sig
  (* ユーザ定義の型 *)
  type 'a t
    (* map 関数 *)
  val map : ('a -> 'b) -> 'a t -> 'b t
    (* acc 関数 : 中身を展開し、集める関数 *)
    (*  val acc : 'a t -> ('a -> 'a -> 'a) -> 'a ->'a (* 引数, 関数, 初期値 *) *)
    (* 単一化関数 *)
  val unify : ('a -> 'a -> unit) -> 'a t -> 'a t -> unit
    (* 描画関数 *)
  val draw : id_t t -> id_t
    (* search関数 *)
  val search : bool t -> bool
end

(********** ファンクターの定義 **********)
module F (S : STRUCTURE_SIG) : 
  sig
   type fix_t = 
       Fix of fix_t S.t
     | Meta of string	                (* メタ変数名 *)
	     * fix_t option ref		(* 実体へのポインタ *)
     | Code of (unit -> id_t)		(* コードの描画法 *)
	     * (unit -> fix_t)		(* コード本体 *)
	     * fix_t option ref		(* 実体へのポインタ *)

   (* val resubst : fix_t -> fix_t -> bool *)
   val take : fix_t -> fix_t S.t
   val occur : string -> fix_t -> bool
   val unify : fix_t -> fix_t -> unit
   val draw : fix_t -> id_t (* id_t を返すように変更 *)
   (* val clear : fix_t -> bool *)
   val make_meta : string -> fix_t
   val make_fix : fix_t S.t -> fix_t
   val make_code : (unit -> id_t) -> (unit -> fix_t) -> fix_t
   val init : unit -> unit
   val deref : fix_t -> fix_t
   val search : fix_t -> bool
     (* parser登録 *)
   val parse : (string -> fix_t) ref
end
= 
struct
  (* 型定義 *)
  type fix_t = 
      Fix of fix_t S.t
    | Meta of string
	    * fix_t option ref
     | Code of (unit -> id_t)
	     * (unit -> fix_t)
	     * fix_t option ref

  (* parser を持たせる *)
  let parse = ref (fun str -> raise Not_found)

  (* メタ変数を生成する *)
  let num = ref 0
  let make_meta str = 
    num := !num + 1;
    Meta (str ^ string_of_int !num, ref None)

  (* Fix を生成する *)
  let make_fix elt = Fix (elt)

  (* Codeを生成する *)
  let make_code draw_fun code_fun = Code(draw_fun, code_fun, ref None) 

 (* ref の一番先を取ってくる : fix_t -> fix_t
     この時、Codeは実行しておく*)
  let rec deref t = match t with
      Fix _ -> t
    | Meta (_, p) ->
	(match !p with
	    Some (t') -> let res = deref t' in
			 p := Some (res); res
	  | None -> t)
    | Code (_, code_fun, p) ->
	(match !p with
	    Some (t') -> let res = deref t' in
			 p := Some (res); res
	  | None ->
	      let res = code_fun () in
	      let res' = deref res in
	      p := Some (res');
	      res')

(*
  (* resubst : Undo の時に使おうと思っている *)
  let rec resubst fix1 fix2 = (*match deref fix1 with
      Meta(_, ({contents = None} as op), _) ->
	op := Some(fix2); true
    | Fix(tm, _) -> S.search (S.map (fun fix1 -> resubst fix1 fix2) tm)
    | _ -> false*) false (* あとで *)
*)

    (*
  let subst fix =
    let rec subst fix = match fix with
	(* 自分がオリジナルのケース *)
	Meta(_, ({contents = None} as op), _) -> 
	  op := Some(!parse (!input_str^";;"))
(*      | (* 自分はコピーのケース *)
	  Meta(_, {contents = Some (fix')}, _, _) -> subst fix' *)
      | _ -> assert false
    in input_dialog(); subst fix
    *)

(* id_t list を全て空リストにする *)
(*
  let rec clear fix = match fix with
     Fix (tm, ids) ->
       ids := [];
       let tm' = S.map clear tm in
	 S.search tm'
    | Meta (_, {contents = None}, ids) ->
	(ids := []; false)
    | Meta (_, {contents = Some (fix')}, ids) ->
	ids := [];
	clear fix';
    | Code (draw_fun, code, ids) ->
	ids := [];
	(match !code with
	     C _ -> false
	   | V(f) -> clear f)
*)

  (* 置換関数 *)
  let search fix = false (* not yet *)
(*
  let rec search fix = 
    match !mode with
	SUB -> (
	  match fix with
	      Meta(_, {contents = None}, ids) ->
		if create_bbox !ids
		then (subst fix; true)
		else false
	    | Meta(_, {contents = Some(fix2)}, ids) -> search fix2
	    | Fix(tm, id) -> S.search (S.map (fun t -> search t) tm)
	    | Code(_, c, _) -> (match !c with
				    C _ -> false
				  | V(v) -> search v))
      | OCC -> false
      | CLEAR -> clear fix
      *)

  (* Fixの中身を取ってくる *)
  let rec take fix = match deref fix with
      Fix (tm) -> tm
    | _ -> raise Cannot_take 

  let rec occur str fix = match deref fix with
       Fix (term) -> S.search (S.map (occur str) term)
     | Meta (str', _) -> str = str' (* 本当にＯＫ？ *)
     | Code (_, _, _) -> true

  (* unification : fix_t -> fix_t -> unit *)
  let rec unify fix1 fix2 = match (deref fix1, deref fix2) with
    | (Meta (_, op1), (Meta (_, op2) as fix2')) ->
	if op1 != op2 
	then op1 := Some (fix2')
    | (Meta (str, op), ((Fix _) as v))
    | (((Fix _) as v), Meta (str, op)) ->
	if occur str v
	then raise (Unify_Error str)
	else op := Some (v)
    | (Fix (t1), Fix (t2)) -> S.unify unify t1 t2
    | (Meta _, Code _)
    | (Code _, Meta _) -> raise (Unify_Error ("of_meta_and_code"))
    | (Code _, Code _) -> raise (Unify_Error("of_code_and_code"))
    | (Code _, Fix _)
    | (Fix _, Code _) -> raise (Unify_Error("of_fix_and_code"))

  (* 描画関数 : fix_t -> id_t *)
  (* 実際には id を正しく配置するだけ *)
  let rec draw fix = match fix with
      Fix (tm) ->
	let tm' = S.map draw tm in
	let id = S.draw tm' in
	id
    | Meta (str, {contents = None}) -> create_str str
    | Meta (str, {contents = Some (fix')}) -> draw fix'
    | Code (draw_fun, _, {contents = None}) -> draw_fun ()
    | Code (draw_fun, _, {contents = Some (fix')}) -> draw fix'

  (* 初期化関数 *)
  let init () = num := 0
end