module StringMap = Map.Make (String)
open Big_int

type term = { 
  t_id : int;
  t_shape : shape;
  t_max_var_level : int;
  mutable t_nf : term option;
}

and shape =
  | Var of int
  | App of string * term list
  | Lam of term

type rule =
  {
    r_arg_count : int;
    r_source : term;
    r_target : term;
  }

let smt = ref false
let verbose = ref false
let term_log = ref false
let dump_coq = ref false
let dump_maude = ref false
let reductions = ref 0
let topnames = Hashtbl.create 10000
let trusted_mode = ref false
let query = ref None

(* r_source name -> rule list *)
let rules = Hashtbl.create 123 

let get_id t = t.t_id

let t2s ?(collapse = false) t = 
  let b = Buffer.create 100 in
  let say = Buffer.add_string b in
  let gen_name vars =
    let len = List.length vars in
    let name = 
      if len < 25 then String.make 1 (char_of_int (int_of_char 'A' + len))
      else Printf.sprintf "X%d" len
    in
    (name :: vars, name)
  in
  let rec f vars t = 
    if collapse && Hashtbl.mem topnames (get_id t) then
      say (Hashtbl.find topnames (get_id t))
    else
      match t.t_shape with
      | Var x -> 
        (try say (List.nth vars x)
         with Invalid_argument _ | Failure _ -> Printf.bprintf b "x%d" x)
      | App (name, []) -> say name
      | App (name, args) -> 
        say "("; say name;
        List.iter (fun a -> say " "; f vars a) args;
        say ")"
      | Lam n -> 
          say "(\\ ";
          let (vars', name) = gen_name vars in
          say name; say " "; f vars' n; say ")"
  in f [] t; Buffer.contents b

let maude_defined = Hashtbl.create 13
let maude_buffer = Buffer.create 100
let maude_commands = Buffer.create 100
let sf = Printf.sprintf
let var_names = Hashtbl.create 10

let maude_quote = function
  | "+" -> "%add"
  | "-" -> "%sub"
  | "~" -> "%neg"
  | "<=" -> "%le"
  | "=" -> "%eq"
  | s ->
    let res = Buffer.create (String.length s) in
    String.iter (function
      | '_' | '.' -> Buffer.add_char res '-'
      | c -> Buffer.add_char res c) s;
    Buffer.contents res

let maude_define name =
  match name with
    | _ when Hashtbl.mem maude_defined name -> ()
    | "+" | "-" | "<=" | "~"
    | "%BETA" | "%CONS" | "%NIL" | "%SKOL" | "%CONSTANT_FOLD" ->
      Hashtbl.add maude_defined name true
    | _ ->
      Buffer.add_string maude_buffer (sf "  op %s : -> C .\n" (maude_quote name));
      Hashtbl.add maude_defined name true

let is_number name =
  let rec loop i =
    if i >= String.length name then true
    else
      match name.[i] with
        | '-'
        | '0' .. '9' -> loop (i + 1)
        | _ -> false
  in loop 0
;;

let t2m t =
  let b = Buffer.create 100 in
  let say = Buffer.add_string b in
  let rec f d t =
    match t.t_shape with
    | Var x ->
      (try
        let name = Hashtbl.find var_names (x - d) in
        say (if d == 0 then sf " %s:T" name else sf " %%lift(%d, 0, %s:T)" d name)
      with Not_found -> say (sf " (%% %d)" x))

    | App ("", _) ->
      prerr_endline "empty term name";
      exit 1

    | App (name, []) when is_number name ->
      say " (%c "; say name; say ")"

    | App (name, args) ->
      maude_define name;
      let qname = maude_quote name in
      (match args with
       | [] -> say " "; say qname
       | _ -> 
         say " ("; say qname;
         List.iter (f d) args;
         say ")")
    | Lam n ->
      say " (\\"; f (d + 1) n; say ")"
  in f 0 t; Buffer.contents b
;;

let hash_consed_maude = Hashtbl.create 123
;;

let rec t2hcm t =
  try
    Hashtbl.find hash_consed_maude t.t_id
  with Not_found ->
    let build name args =
      let sname = sf " %%t%d" t.t_id in
      Buffer.add_string maude_buffer (sf "  op%s : -> C [memo] .\n" sname);
      Hashtbl.add hash_consed_maude t.t_id sname;
      let buf = Buffer.create 100 in
      let say = Buffer.add_string buf in
      say (maude_quote name);
      List.iter (fun t -> say (t2hcm t)) args;
      Buffer.add_string maude_buffer (sf "  eq%s = %s .\n" sname (Buffer.contents buf));
      sname
    in

    let s =
      match t.t_shape with
      | Var x -> sf " (%% %d)" x

      | App ("", _) ->
        prerr_endline "empty term name";
        exit 1

      | App (name, []) ->
        if is_number name then sf " (%%c %s)" name
        else 
          (maude_define name;
           " " ^ maude_quote name)

      | App (name, args) ->
        maude_define name;
        build name args
        
      | Lam n -> build "\\" [n]
    in
    Hashtbl.replace hash_consed_maude t.t_id s;
    s
;;

let hashed_id = ref 0
let previous_print = ref 0.0
let previous_print_reds = ref 0
let previous_hashed_id = ref 0

let print_status msg =
  let time = 
    if !previous_print = 0.0 then 
      let _ = previous_print := Unix.gettimeofday () in
      0.0 
    else
      let time = Unix.gettimeofday () in
      let res = time -. !previous_print in
      let _ = previous_print := time in
      res in
  let delta now prev =
    let res = !now - !prev in
    let _ = prev := !now in
    res in
  let reds = delta reductions previous_print_reds in
  let terms = delta hashed_id previous_hashed_id in
  if not !dump_coq  && not !dump_maude then (
    Printf.printf "%0.3f %8d %8d %s" time reds terms msg;
    print_newline ())

let hashed hash mk =
  let cache = Hashtbl.create 200003 in 
  fun n ->
    let _ = incr reductions in
    try Hashtbl.find cache (hash n)
    with Not_found ->
      incr hashed_id;
      let (var, shape) = mk n in
      let v = { t_id = !hashed_id; t_shape = shape; t_max_var_level = var; t_nf = None } in
      if !dump_maude then
        v.t_nf <- Some v;
      if !term_log then
        Printf.printf "create: %s\n" (t2s ~collapse:true v);
      Hashtbl.add cache (hash n) v;
      v

let var = hashed (fun x -> x) (fun x -> assert (x >= 0); (x, Var x))
let app = hashed (fun (n, a) -> (n, List.map get_id a)) 
  (fun (name, args) -> (List.fold_left (fun a t -> max a t.t_max_var_level) (-1) args, App (name, args)))
let lam = hashed get_id (fun n -> (n.t_max_var_level - 1, Lam n))

let err s = raise (Failure s)

let offset n t =
  let cache = Hashtbl.create 13 in
  let rec off_aux d t = 
    if t.t_max_var_level < 0 then t
    else 
      try Hashtbl.find cache (get_id t, d)
      with Not_found ->
        let res =
          match t.t_shape with
            | Lam m ->
              lam (off_aux (d + 1) m)
            | App (name, terms) ->
              app (name, List.map (off_aux d) terms)
            | Var k ->
              if k >= d then var (k + n)
              else t
        in Hashtbl.add cache (get_id t, d) res; res
  in if n == 0 then t else off_aux 0 t

let unsome = function
  | Some t -> t
  | None -> failwith "unsome"

let sharing_map f l = 
  let same = ref true in
  let rec sm_aux = function
    | x :: xs ->
      let x' = f x in
      if !same && x' != x then same := false;
      x' :: sm_aux xs
    | [] -> []
  in
  let res = sm_aux l in
  (!same, res)


let parse_number s = function
  | [] ->
    (try Some (big_int_of_string s)
     with _ -> None)
  | _ -> None

let number_term n =
  app (string_of_big_int n, [])

let rec try_apply term rule =
  let vars = Array.make rule.r_arg_count None in
  let rec compare t1 t2 = 
    match t1.t_shape, t2.t_shape with
      | (App (name, args), App (name', args')) 
          when name = name' && List.length args = List.length args' ->
        List.for_all2 compare args args' 
      | (Var v, _) ->
        (match vars.(v) with
          | Some t' -> t' == t2
          | None -> vars.(v) <- Some t2; true)
    | _ -> false
  in

  let rec subst x t =
    match t.t_shape with
      | _ when t.t_max_var_level < 0 -> nf t
      | Var y ->
        if y >= x then
          let off = y - x in
          if off < rule.r_arg_count then
            offset x (unsome vars.(off))
          else assert false (* var (y - rule.r_arg_count) *)
        else t
      | App (name, terms) ->
        let (same, terms) = sharing_map (subst x) terms in
        (match t.t_nf with
          | Some t when same -> t
          | _ -> rule_app (name, terms))

      | Lam m ->
        lam (subst (x + 1) m)
  in

  if compare rule.r_source term then
    (* let _ = Printf.printf "got hit, term: %s, rule: %s ==> %s\n" (t2s term) (t2s rule.r_source) (t2s rule.r_target) in *)
    let res = subst 0 rule.r_target in
    let _ = 
      if !verbose then
        Printf.printf "end hit, res: %s ===> %s by rule: %s ==> %s\n" 
          (t2s term) (t2s res) (t2s rule.r_source) (t2s rule.r_target) in
    Some res
  else None

and rule_app = function
  | ("%BETA", [{ t_shape = Lam m }; n]) ->
    beta m n

  | ("%CONSTANT_FOLD", ([{ t_shape = App (op, [{t_shape = App (n1, [])}] )}] as top_args)) ->
    (match op, parse_number n1 [] with
      | "~", Some x1 ->
        number_term (minus_big_int x1)
      | _ -> app ("%CONSTANT_FOLD", top_args))

  | ("%CONSTANT_FOLD", ([{ t_shape = App (op, [{t_shape = App (n1, a1)} as t1; 
                                               {t_shape = App (n2, a2)} as t2] )}] as top_args)) ->
    (match op, parse_number n1 a1, parse_number n2 a2 with
      | "+", Some x1, Some x2 -> number_term (add_big_int x1 x2)
      | "+", Some _, None when n1 = "0" -> t2
      | "+", None, Some _ when n2 = "0" -> t1
      | "-", Some x1, Some x2 -> number_term (sub_big_int x1 x2)
      | "-", None, Some _ when n2 = "0" -> t1
      | "-", Some _, None when n1 = "0" ->
        (match n2, a2 with
          | ("~", [t]) -> t
          | _ -> app ("~", [t2]))
      | "%div", Some x1, Some x2 ->
        number_term (div_big_int x1 x2)
      | "<=", Some x1, Some x2 ->
        if le_big_int x1 x2 then app ("true", []) else app ("false", [])
      | _ -> app ("%CONSTANT_FOLD", top_args))

  | ("%SKOL", ([{ t_shape = App (name, []) }; args] as top_args)) ->
    (try
      let rec mkargs t = 
        match t.t_shape with
          | App ("%CONS", [hd; tl]) -> hd :: mkargs tl
          | App ("%NIL", []) -> []
          | _ -> raise Not_found
      in app (name, mkargs args)
    with Not_found -> app ("%SKOL", top_args))

  | (name, args) ->
    let term = app (name, args) in
    match term.t_nf with
      | Some t -> t
      | None ->
        let res =
          if Hashtbl.mem rules name then
            let apply_rule acc rule =
              match acc with
                | Some _ -> acc
                | None -> try_apply term rule
            in
            match List.fold_left apply_rule None (Hashtbl.find rules name) with
              | Some t -> t
              | None -> term
          else term
        in
        term.t_nf <- Some res;
        res

(* m[x := n] where m is in \x.m, ensures result = nf result  *)
and beta m n = 
  let cache = Hashtbl.create 13 in
  let rec beta_aux donf x t = 
    try Hashtbl.find cache (x, get_id t)
    with Not_found ->
      let res =
        match t.t_shape with
          | _ when t.t_max_var_level < 0 ->
            if donf then nf t else t
          | Var y when x = y -> if donf then nf (offset x n) else offset x n
          | Var y when x < y -> var (y - 1)
          | Var _ -> t
          | App (name, terms) ->
            let (same, terms) = sharing_map (beta_aux donf x) terms in
            if donf then
              match t.t_nf with
                | Some t when same -> t
                | _ -> rule_app (name, terms)
            else
              if same then t else app (name, terms)

          | Lam m ->
            lam (beta_aux donf (x + 1) m)
      in Hashtbl.add cache (x, get_id t) res; res
  in beta_aux true 0 m

and nf t =
  match t with
    | { t_nf = Some t } -> t
    | _ ->
      if !term_log  then
        Printf.printf "(nf: %s \n" (t2s ~collapse:true t);
      let res =
        match t.t_shape with
          | App (name, args) ->
            rule_app (name, List.map nf args)
          | Lam t -> 
            lam (nf t)
          | Var _ -> t
      in
      if !term_log  then
        Printf.printf " ---> %s \n" (t2s ~collapse:true res);
      t.t_nf <- Some res;
      res

type sexpr =
  | Appl of string * sexpr list
  | Atom of string

let rec s2s = function
  | Atom n -> n
  | Appl (n, lst) ->
    "(" ^ n ^ " " ^ (String.concat " " (List.map s2s lst)) ^ ")"

let sexpr_to_term env s = 
  let rec self depth env s =
    let get s = 
      try 
        match StringMap.find s env with
          | (-1, t) -> t
          | (depth', t) -> offset (depth - depth') t
      with Not_found -> app (s, [])
    in
    match s with
      | Atom s ->
        if not !trusted_mode && s.[0] == '%' then
          err ("attempt to use restricted identifier in non trusted mode " ^ s);
        get s
      | Appl ("let", [Atom (name); m; n]) ->
        let m = self depth env m in
        self depth (StringMap.add name (depth, m) env) n
      | Appl ("let", _) ->
        err ("malformed let " ^ s2s s)
      | Appl ("\\", [Atom (name); body]) ->
        let depth = depth + 1 in
        let env = StringMap.add name (depth, var 0) env in
        lam (self depth env body)
      | Appl (name, args) ->
        if not !trusted_mode && name.[0] == '%' then
          err ("attempt to use restricted identifier in non trusted mode " ^ name);
        app (name, List.map (self depth env) args)
  in self 0 env s
  

type my_file = { handle : in_channel; mutable peeked : int; }

let rec peek f =
  if f.peeked >= 0 then char_of_int f.peeked
  else ( f.peeked <- input_byte f.handle; peek f )

let read f = let c = peek f in f.peeked <- -1; c
let putback f c = f.peeked <- int_of_char c

let rec non_ws f =
  match read f with
    | ' ' | '\t' | '\n' -> non_ws f
    | ';' -> let rec loop () = if read f = '\n' then non_ws f else loop () in loop ()
    | c -> c

let read_word f =
  let b = Buffer.create 10 in
  match peek f with
    | '"' ->
      let rec loop2 () =
        match read f with
          | '"' -> Buffer.contents b
          | c -> Buffer.add_char b c; loop2 ()
      in
      let _ = read f in loop2 ()

    | '{' ->
      let rec loop3 lev =
        match read f with
          | '}' when lev = 1 -> Buffer.contents b
          | '}' ->
            Buffer.add_char b '}'; loop3 (lev - 1)
          | '{' ->
            Buffer.add_char b '{'; loop3 (lev + 1)
          | c ->
            Buffer.add_char b c; loop3 lev
      in
      let _ = read f in loop3 1

    | _ ->
      let rec loop () =
        match peek f with
          | ' ' | '\t' | '\n' | '(' | ')' | ';' -> Buffer.contents b
          | _ -> Buffer.add_char b (read f); loop ()
      in loop ()

let rec read_sexpr f =
  match peek f with
    | '(' ->
      let _ = read f in
      let hd = read_word f in
      let rec loop acc = function
        | ')' -> Appl (hd, List.rev acc)
        | c ->
          putback f c; 
          let inner = read_sexpr f in loop (inner :: acc) (non_ws f)
      in loop [] (non_ws f)
    | _ -> Atom (read_word f)
;;

let smt_to_term env s = 
  let rec kill_annotations acc = function
    | Atom (name) :: _ :: rest when name.[0] = ':' -> kill_annotations acc rest
    | x :: xs -> kill_annotations (x :: acc) xs
    | [] -> acc
  in
  let rec self depth env s =
    let get s = 
      try 
        match StringMap.find s env with
          | (-1, t) -> t
          | (depth', t) -> offset (depth - depth') t
      with Not_found -> app (s, [])
    in
    match s with
      | Atom s -> get s
      (*
      | Appl ("flet", [Atom (name); m; n]) ->
        let m = self depth env m in
        self depth (StringMap.add name (depth, m) env) n
      | Appl ("flet", _) ->
        err ("malformed let " ^ s2s s) *)
      | Appl ("exists" as qname, args) 
      | Appl ("forall" as qname, args) ->
        (match kill_annotations [] args with
          | body :: vars ->
            let rec build depth env = function
              | Appl (name, [Atom (_)]) :: rest when name.[0] = '?' ->
                let depth = depth + 1 in
                let env = StringMap.add name (depth, var 0) env in
                app (qname, [lam (build depth env rest)])
              | [] -> self depth env body
              | x :: _ -> err ("evil forall 2 " ^ s2s x)
            in build depth env (List.rev vars)
          | _ -> err "evil forall")
      | Appl (name, args) ->
        let args = List.map (self depth env) args in
        (match name with
          | "distinct" | "and" | "or" ->
            let rec build = function
              | [x] -> x
              | x :: xs -> app (name, [x; build xs])
              | [] -> err ("evil " ^ name)
            in build args
          | _ -> app (name, args))
  in self 0 env s
;;

let read_benchmark f =
  let skip_ws f =
    let c = non_ws f in
    putback f c
  in
  match non_ws f with
    | '(' ->
      skip_ws f;
      (match read_word f with
        | "benchmark" ->
          skip_ws f;
          let name = read_word f in
          print_status ("reading SMT " ^ name);
          let rec loop acc = 
            let c = non_ws f in
            if c = ')' then 
              acc
            else
              let _ = putback f c in
              match read_word f with
                | ":formula"
                | ":assumption" ->
                  skip_ws f;
                  loop (read_sexpr f :: acc)
                | _ ->
                  skip_ws f;
                  let _ = read_sexpr f in loop acc
          in 
            let res = smt_to_term StringMap.empty (Appl ("and", List.rev (loop []))) in
            (try 
              let c = non_ws f in
              err (Printf.sprintf "junk after benchmark file, %c" c)
            with End_of_file ->
              print_status ("SMT read");
              res)

        | _ -> err "wrong benchmark (no 'benchmark')")
    | _ -> err "wrong benchmark (no '(')"

let top_read f =
  let has_more =
    try let c = non_ws f in putback f c; true with End_of_file -> false
  in if has_more then read_sexpr f else Atom ("quit")
let bad_term t = err ("bad term " ^ t2s t)
let var_trans n = Hashtbl.find var_names n
let to_coq ?(err = bad_term) ?(var_trans = var_trans) t =
  let rec f t =
    match t.t_shape with
      | App ("implies", [a; b]) ->
        Printf.sprintf "(%s -> %s)" (f a) (f b)
      | App ("iff", [a; b]) ->
        Printf.sprintf "(%s <-> %s)" (f a) (f b)
      | App ("and", [a; b]) ->
        Printf.sprintf "(%s /\\ %s)" (f a) (f b)
      | App ("or", [a; b]) ->
        Printf.sprintf "(%s \\/ %s)" (f a) (f b)
      | App ("not", [a]) ->
        Printf.sprintf "~%s" (f a)
      | App ("%div", [a;b]) ->
        Printf.sprintf "(%s / %s)" (f a) (f b)
      | App ("-", [a]) | App ("~", [a]) -> "-" ^ f a
      | App (("<="|">="|"<"|">"|"="|"+"|"-"|"*") as name, [a;b]) ->
        Printf.sprintf "(%s %s %s)" (f a) name (f b)
      | App (("0"|"1"|"2") as n, []) -> n
      | App ("%CONSTANT_FOLD", [a]) -> f a
      | App ("false", []) ->
        "False"
      | App ("true", []) ->
        "True"
      | Var n -> var_trans n
      | _ ->
        err t
  in f t

let k_rules = Hashtbl.create 13

let dump_coq_krule ?(is_arith = false) ?(is_eq = false) r =
  let dump_known t =
    match t.t_shape with
      | App ("%known", [formula]) -> Some (to_coq formula)
      | _ -> None
  in
  match r.r_source.t_shape with
    | App (name, args) ->
      let name =
        if not (Hashtbl.mem k_rules name) then (Hashtbl.add k_rules name name; name)
        else (Hashtbl.add k_rules (name^"__2") name; name ^ "__2")
      in
      Printf.printf "Lemma k_%s : forall" name;
      if is_eq then Printf.printf " T : Type, forall ";
      let rec quant n =
        if n >= 0 then
          (Printf.printf " %s" (var_trans n); quant (n - 1))
      in quant (r.r_arg_count - 1);
      if is_eq then Printf.printf " : T, "
      else if is_arith then Printf.printf " : Z, "
      else Printf.printf " : Prop, ";
      List.iter (fun a -> 
        match dump_known a with 
          | None -> () 
          | Some s -> Printf.printf "%s -> " s) args;
      (match dump_known r.r_target with
        | Some s -> Printf.printf "%s.\n" s
        | None -> err "result is supposed to be (known ...)");
      if is_eq then Printf.printf "congruence. Qed.\n\n"
      else if is_arith  then Printf.printf "intros. omega. Qed.\n\n"
      else Printf.printf "intros. apply NNPP. tauto. Qed.\n\n";
    | _ -> assert false

let iter_term f t =
  let rec aux t = 
    f t;
    match t.t_shape with
      | App (_, ts) -> List.iter aux ts
      | Lam (t) -> aux t
      | Var _ -> ()
  in aux t

let dump_coq_srule r =
  let var_trans n = (var_trans n) ^ " t" in
  let to_coq = to_coq ~var_trans:var_trans in
  let skol t = match t.t_shape with
    | App ("%skol", [{ t_shape = Var 0 }; _; t]) -> Some t
    | _ -> None
  in
  match skol r.r_source with
    | Some t -> 
      let name = match r.r_source.t_shape with 
        | App (_, [_; { t_shape = App (name, _) }; _]) -> name
        | _ -> assert false
      in
      Printf.printf "Lemma s_%s : forall T : Type,\n" name;

      let skols = Hashtbl.create 10 in
      let skol_list = ref [] in
      let find_skol t =
        match skol t with
          | Some t when not (Hashtbl.mem skols (get_id t)) ->
            let id = Hashtbl.length skols in
            Printf.printf "\tforall T%d : Type, forall P%d : T -> T%d -> Prop,\n" id id id;
            skol_list := (t, id) :: !skol_list;
            Hashtbl.add skols (get_id t) (t, id)
          | _ -> ()
      in iter_term find_skol r.r_target;

      Printf.printf "\tforall";
      let vars = Hashtbl.create 10 in
      let add t = match t.t_shape with
        | Var n when not (Hashtbl.mem vars n) ->
          Printf.printf " %s" (Hashtbl.find var_names n);
          Hashtbl.add vars n n
        | _ -> ()
      in iter_term add t;
      Printf.printf " : T -> Prop,\n";
      
      let print_skol t =
        match skol t with
          | Some t -> 
            let _, id = Hashtbl.find skols (get_id t) in
            Printf.sprintf "P%d t f%d" id id
          | _ -> assert false
      in
      let print_premise (t, id) =
        Printf.printf "\t(exists f%d : T%d, forall t : T, %s -> P%d t f%d) ->\n" id id (to_coq ~err:print_skol t) id id
      in List.iter print_premise !skol_list;

      Printf.printf "\t";
      for i = 0 to Hashtbl.length skols - 1 do
        Printf.printf "exists f%d : T%d, " i i;
      done;

      Printf.printf "forall t : T,\n\t%s -> %s.\n" (to_coq t) (to_coq ~err:print_skol r.r_target);
      (* Printf.printf "Proof. Admitted.\n\n"; *)

    | None -> err "bad srule source"
 
let read_rule t =
  if not !trusted_mode then
    err "rules allowed only in trusted mode, use -trusted";

  let vars = Hashtbl.create 10 in
  let rec aux depth t = match t.t_shape with
    | App (name, []) when name <> "" ->
      (match name.[0] with
        | 'A' .. 'Z' ->
          (try
             var (Hashtbl.find vars name + depth)
           with Not_found ->
             let id = Hashtbl.length vars in
             Hashtbl.add vars name id;
             var (depth + id))
        | _ -> t)
    | App (name, args) ->
      app (name, List.map (aux depth) args)
    | Lam t -> lam (aux (depth + 1) t)
    | Var _ -> t
  in
    let save_rule name s t =
      let len = Hashtbl.length vars in
      let rule = { r_source = s; r_target = t; r_arg_count = len } in
      if !verbose then Printf.printf "rule  %s  ==>  %s\n" (t2s s) (t2s t);
      Hashtbl.clear var_names;
      Hashtbl.iter (fun n i -> Hashtbl.add var_names i n) vars;
      (try
         Hashtbl.add rules name (rule :: Hashtbl.find rules name)
       with Not_found -> Hashtbl.add rules name [rule]);
      if !dump_maude then (
        Buffer.add_string maude_buffer (sf "  eq%s =%s .\n" (t2m s) (t2m t))
      );
      rule
    in
    match (aux 0 t).t_shape with
      | App (cmd, [{ t_shape = App (name, _) } as s; t]) ->
        let rule = save_rule name s t in
        if !dump_coq then
          (match cmd with
            | "eq_rule" -> dump_coq_krule ~is_eq:true rule
            | "arith_rule" -> dump_coq_krule ~is_arith:true rule
            | "bool_rule" -> dump_coq_krule rule
            | "skol_rule" -> dump_coq_srule rule
            | "trusted_rule"
            | "rule" -> ()
            | _ -> assert false)
      | App ("raw_coq_rule", [{ t_shape = App (coq, []) }; { t_shape = App (name, _) } as s; t]) ->
        let _rule = save_rule name s t in
        if !dump_coq then Printf.printf "%s\n" coq;
      | _ -> assert false

let check_unique sk form =
  let used = Hashtbl.create 12342 in
  let skcon = ref 0 in
  let rec add insk t =
    match t.t_shape with 
      | App ("skolemize", t) when insk ->
        (match t with
          | [{ t_shape = App (name, []) }] ->
            if Hashtbl.mem used name then
              err ("attempt to reuse skolem constant " ^ name);
            incr skcon;
            Hashtbl.add used name true
          | _ -> err "ill formed skolemize(...)")
      | App (name, children) ->
        if not insk && not (Hashtbl.mem used name) then Hashtbl.add used name false;
        List.iter (add insk) children
      | Var _ -> ()
      | Lam t -> add insk t
  in 
  add false form;
  add true sk;
  print_status (Printf.sprintf "sk-unique OK, %d fun, %d sk-fun" (Hashtbl.length used) !skcon)
  
let top_loop f =
  let rec eval_loop numbers = 
    match top_read f with
      | Atom ("quit") ->
        if !trusted_mode then ()
        else err "wanted to escape, huh?!"

      | Appl ("coq", [Atom (s)]) ->
        if !dump_coq then Printf.printf "%s\n\n" s;
        eval_loop numbers

      | Appl ("eq_rule", [_; _])
      | Appl ("bool_rule", [_; _])
      | Appl ("skol_rule", [_; _])
      | Appl ("arith_rule", [_; _])
      | Appl ("trusted_rule", [_; _])
      | Appl ("raw_coq_rule", [_; _; _])
      | Appl ("rule", [_; _]) as body ->
        read_rule (sexpr_to_term numbers body);
        eval_loop numbers

      | Appl ("initial", [t1; t2]) ->
        if StringMap.mem "initial" numbers then
          err "attempt to initiate twice";
        let t1 = sexpr_to_term numbers t1 in
        let t2 = sexpr_to_term numbers t2 in
        (match !query with
          | Some q ->
            if q != t2 then (
              Printf.printf "%s\n%s\n" (t2s q) (t2s t2);
              err "term passed to initial doesn't match the query")
          | None ->
            if not !trusted_mode then
              err "no query specified, either specify query with -q, or use trusted mode (-t)");
        check_unique t1 t2;
        let body = nf (app ("%initial", [t1; t2])) in
        eval_loop (StringMap.add "initial" (-1, body) numbers)

      | Appl ("final", [t]) ->
        let t = sexpr_to_term numbers t in
        let ok = app ("%final_ok", []) in
        let t = nf (app ("%final", [t])) in
        if !dump_maude then
          Buffer.add_string maude_commands (sf "red %%assert-eq(%s, %%final-ok) .\n" (t2hcm t))
        else
          if t == ok then
            print_status "proof OK"
          else err ("final check failed for " ^ (t2s t))

      | Appl ("let", [Atom (name); body]) ->
        let body = sexpr_to_term numbers body in
        if !verbose then
          Printf.printf "let %s\n\t%s =>\n\t" name (t2s body);
        flush stdout;
        let body = nf body in
        if !verbose then
          Printf.printf "\t%s\n" (t2s body);
        flush stdout;
        Hashtbl.add topnames (get_id body) name;
        eval_loop (StringMap.add name (-1, body) numbers)

      | Appl ("print", [body]) ->
        let body = sexpr_to_term numbers body in
        print_status ((if !trusted_mode then "Trusted: " else "Proof: ") ^ t2s body);
        eval_loop numbers

      | Appl ("assert_ok", [t]) ->
        let ok = app ("%ok", []) in
        let t = nf (sexpr_to_term numbers t) in
        (*if !dump_maude then
          Buffer.add_string maude_commands (sf "red %%assert-eq(%s, %%ok) .\n" (t2hcm t));*)
        if not !dump_maude && t != ok then
          err (Printf.sprintf "assert OK FAILED: %s\n" (t2s t));
        eval_loop numbers

      | Appl ("assert_eq", [t1; t2]) ->
        let t1 = sexpr_to_term numbers t1 in
        let t2 = sexpr_to_term numbers t2 in
        if !dump_maude then
          Buffer.add_string maude_commands (sf "red %%assert-eq(%s, %s) .\n" (t2hcm t1) (t2hcm t2));
        if not !dump_maude && t1 != t2 then
          err (Printf.sprintf "assert FAILED: %s %s\n" (t2s t1) (t2s t2));
        eval_loop numbers

      | Appl ("rem", _) ->
        eval_loop numbers

      | Appl ("term_log_on", []) ->
        term_log := true;
        eval_loop numbers

      | Appl ("term_log_off", []) ->
        term_log := false;
        eval_loop numbers

      | t ->
        err ("bad magic word " ^ s2s t)
  in 
    try eval_loop StringMap.empty
    with Failure s ->
      Printf.eprintf "FATAL: %s\n" s;
      exit 1
;;

Gc.set { (Gc.get()) with Gc.space_overhead = 300; Gc.minor_heap_size = 300000 }


let fopen name = { handle = open_in name; peeked = -1 }

let read_trusted name =
  trusted_mode := true;
  try
    top_loop (fopen name);
    trusted_mode := false;
    print_status ("trusted file `" ^ name ^ "' read")
  with e ->
    trusted_mode := false;
    raise e
;;

let read_query name =
  assert (!query = None);
  let q = read_benchmark (fopen name) in
  query := Some q;
  if !smt then
    Printf.printf "%s\n" (t2s q)

let read_proof name =
  top_loop (fopen name)
;;

let options =
  [
    ( "-v", Arg.Set verbose, "Be noisy" );
    ( "-coq", Arg.Set dump_coq, "Dump Coq proof" );
    ( "-maude", Arg.Set dump_maude, "Dump Maude proof" );
    ( "-smt", Arg.Set smt, "Dump SMT query" );

    ( "-trusted", Arg.String read_trusted, "Read a logic description (rewrite rules)");
    ( "-t", Arg.String read_trusted, "As -trusted");

    ( "-query", Arg.String read_query, "Read a SMT-LIB format query");
    ( "-q", Arg.String read_query, "As -query");

    ( "-proof", Arg.String read_proof, "Read, and evaluate a proof");
    ( "-p", Arg.String read_proof, "As -proof; In fact -p can be omitted altogether");
  ]
in
Arg.parse options read_proof "Check the proof.";

if !dump_maude then (
  print_endline (Buffer.contents maude_buffer);
  print_endline "endfm\n";
  print_endline (Buffer.contents maude_commands);
)