(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

open Util
open Format
open Pp
open Ptree
open Ident
open Ty
open Term
open Decl
open Theory
open Env
open Denv

(** errors *)

exception Message of string
exception DuplicateTypeVar of string
exception TypeArity of qualid * int * int
exception Clash of string
exception PredicateExpected
exception TermExpected
exception BadNumberOfArguments of Ident.ident * int * int
exception ClashTheory of string
exception UnboundTheory of qualid
exception CyclicTypeDef
exception UnboundTypeVar of string
exception UnboundType of string list
exception UnboundSymbol of string list

let error ?loc e = match loc with
  | None -> raise e
  | Some loc -> raise (Loc.Located (loc,e))

let errorm ?loc f =
  let buf = Buffer.create 512 in
  let fmt = Format.formatter_of_buffer buf in
  Format.kfprintf
    (fun _ ->
       Format.pp_print_flush fmt ();
       let s = Buffer.contents buf in
       Buffer.clear buf;
       error ?loc (Message s))
    fmt f

let rec print_qualid fmt = function
  | Qident s -> fprintf fmt "%s" s.id
  | Qdot (m, s) -> fprintf fmt "%a.%s" print_qualid m s.id

let () = Exn_printer.register (fun fmt e -> match e with
  | Message s ->
      fprintf fmt "%s" s
  | DuplicateTypeVar s ->
      fprintf fmt "duplicate type parameter %s" s
  | TypeArity (id, a, n) ->
      fprintf fmt "@[The type %a expects %d argument(s),@ " print_qualid id a;
      fprintf fmt "but is applied to %d argument(s)@]" n
  | Clash id ->
      fprintf fmt "Clash with previous symbol %s" id
  | PredicateExpected ->
      fprintf fmt "syntax error: predicate expected"
  | TermExpected ->
      fprintf fmt "syntax error: term expected"
  | BadNumberOfArguments (s, n, m) ->
      fprintf fmt "@[Symbol `%s' is applied to %d terms,@ " s.id_string n;
      fprintf fmt "but is expecting %d arguments@]" m
  | ClashTheory s ->
      fprintf fmt "clash with previous theory %s" s
  | UnboundTheory q ->
      fprintf fmt "unbound theory %a" print_qualid q
  | CyclicTypeDef ->
      fprintf fmt "cyclic type definition"
  | UnboundTypeVar s ->
      fprintf fmt "unbound type variable '%s" s
  | UnboundType sl ->
       fprintf fmt "Unbound type '%a'" (print_list dot pp_print_string) sl
  | UnboundSymbol sl ->
       fprintf fmt "Unbound symbol '%a'" (print_list dot pp_print_string) sl
  | _ -> raise e)

let debug_parse_only = Debug.register_flag "parse_only"
let debug_type_only  = Debug.register_flag "type_only"

(** Environments *)

(** typing using destructive type variables

    parsed trees        intermediate trees       typed trees
      (Ptree)               (D below)               (Term)
   -----------------------------------------------------------
     ppure_type  ---dty--->   dty       ---ty--->    ty
      lexpr      --dterm-->   dterm     --term-->    term
      lexpr      --dfmla-->   dfmla     --fmla-->    fmla

*)

let term_expected_type ~loc ty1 ty2 =
  errorm ~loc
    "@[This term has type %a@ but is expected to have type@ %a@]"
    print_dty ty1 print_dty ty2

let unify_raise ~loc ty1 ty2 =
  if not (unify ty1 ty2) then term_expected_type ~loc ty1 ty2

(** Destructive typing environment, that is
    environment + local variables.
    It is only local to this module and created with [create_denv] below. *)

type denv = {
  uc : theory_uc; (* the theory under construction *)
  utyvars : (string, type_var) Hashtbl.t; (* user type variables *)
  dvars : dty Mstr.t; (* local variables, to be bound later *)
}

let create_denv uc = {
  uc = uc;
  utyvars = Hashtbl.create 17;
  dvars = Mstr.empty;
}

let find_user_type_var x env =
  try
    Hashtbl.find env.utyvars x
  with Not_found ->
    (* TODO: shouldn't we localize this ident? *)
    let v = create_tvsymbol (id_fresh x) in
    let v = create_ty_decl_var ~user:true v in
    Hashtbl.add env.utyvars x v;
    v

let mem_var x denv = Mstr.mem x denv.dvars
let find_var x denv = Mstr.find x denv.dvars
let add_var x ty denv = { denv with dvars = Mstr.add x ty denv.dvars }

let print_denv fmt denv =
  Mstr.iter (fun x ty -> fprintf fmt "%s:%a,@ " x print_dty ty) denv.dvars

(* parsed types -> intermediate types *)

let rec qloc = function
  | Qident x -> x.id_loc
  | Qdot (m, x) -> Loc.join (qloc m) x.id_loc

let rec string_list_of_qualid acc = function
  | Qident id -> id.id :: acc
  | Qdot (p, id) -> string_list_of_qualid (id.id :: acc) p

let specialize_tysymbol loc p uc =
  let sl = string_list_of_qualid [] p in
  let ts =
    try ns_find_ts (get_namespace uc) sl
    with Not_found -> error ~loc (UnboundType sl)
  in
  ts, List.length ts.ts_args

(* lazy declaration of tuples *)

let tuples_needed = Hashtbl.create 17

let ts_tuple n = Hashtbl.replace tuples_needed n (); ts_tuple n
let fs_tuple n = Hashtbl.replace tuples_needed n (); fs_tuple n

let add_tuple_decls uc =
  Hashtbl.fold (fun n _ uc -> Theory.use_export uc (tuple_theory n))
    tuples_needed uc

let with_tuples ?(reset=false) f uc x =
  let uc = f (add_tuple_decls uc) x in
  if reset then Hashtbl.clear tuples_needed;
  uc

let add_ty_decl  = with_tuples add_ty_decl
let add_ty_decls = with_tuples ~reset:true add_ty_decl

let add_logic_decl  = with_tuples add_logic_decl
let add_logic_decls = with_tuples ~reset:true add_logic_decl

let add_ind_decl  = with_tuples add_ind_decl
let add_ind_decls = with_tuples ~reset:true add_ind_decl

let add_prop_decl = with_tuples ~reset:true add_prop_decl

let rec type_inst s ty = match ty.ty_node with
  | Ty.Tyvar n -> Mtv.find n s
  | Ty.Tyapp (ts, tyl) -> tyapp (ts, List.map (type_inst s) tyl)

let rec dty env = function
  | PPTtyvar {id=x} ->
      tyvar (find_user_type_var x env)
  | PPTtyapp (p, x) ->
      let loc = qloc x in
      let ts, a = specialize_tysymbol loc x env.uc in
      let np = List.length p in
      if np <> a then error ~loc (TypeArity (x, a, np));
      let tyl = List.map (dty env) p in
      begin match ts.ts_def with
	| None ->
	    tyapp (ts, tyl)
	| Some ty ->
	    let add m v t = Mtv.add v t m in
            let s = List.fold_left2 add Mtv.empty ts.ts_args tyl in
	    type_inst s ty
      end
  | PPTtuple tyl ->
      let ts = ts_tuple (List.length tyl) in
      tyapp (ts, List.map (dty env) tyl)

let find_ns find p ns =
  let loc = qloc p in
  let sl = string_list_of_qualid [] p in
  try find ns sl
  with Not_found -> error ~loc (UnboundSymbol sl)

let find_prop_ns = find_ns ns_find_pr
let find_prop p uc = find_prop_ns p (get_namespace uc)

let find_tysymbol_ns = find_ns ns_find_ts
let find_tysymbol q uc = find_tysymbol_ns q (get_namespace uc)

let find_lsymbol_ns = find_ns ns_find_ls
let find_lsymbol q uc = find_lsymbol_ns q (get_namespace uc)

let find_namespace_ns = find_ns ns_find_ns
let find_namespace q uc = find_namespace_ns q (get_namespace uc)

let specialize_lsymbol p uc =
  let s = find_lsymbol p uc in
  let tl,ty = specialize_lsymbol ~loc:(qloc p) s in
  s,tl,ty

let specialize_fsymbol p uc =
  let s,tl,ty = specialize_lsymbol p uc in
  match ty with
    | None -> let loc = qloc p in error ~loc TermExpected
    | Some ty -> s, tl, ty

let specialize_psymbol p uc =
  let s,tl,ty = specialize_lsymbol p uc in
  match ty with
    | None -> s, tl
    | Some _ -> let loc = qloc p in error ~loc PredicateExpected

let is_psymbol p uc =
  let s = find_lsymbol p uc in
  s.ls_value = None

(* [is_projection uc ls] returns
   - [Some (ts, lsc, i)] if [ls] is the i-th projection of an
     algebraic datatype [ts] with only one constructor [lcs]
   - [None] otherwise
 *)
let is_projection uc ls =
  try
    let ts,tl = match ls.ls_args, ls.ls_value with
      | [{ty_node = Ty.Tyapp (ts, tl)}], Some _ -> ts,tl
      | _ -> (* not a function with 1 argument *) raise Exit
    in
    ignore (List.fold_left (fun tvs t -> match t.ty_node with
      | Ty.Tyvar tv -> Stv.add_new tv Exit tvs
      | _ -> (* not a generic type *) raise Exit) Stv.empty tl);
    let kn = get_known uc in
    let lsc = match Decl.find_constructors kn ts with
      | [lsc] -> lsc
      | _ -> (* 0 or several constructors *) raise Exit
    in
    let def = match Decl.find_logic_definition kn ls with
      | Some def -> def
      | None -> (* no definition *) raise Exit
    in
    let v, t = match Decl.open_fs_defn def with
      | [v], t -> v, t
      | _ -> assert false
    in
    let b = match t.t_node with
      | Tcase ({t_node=Term.Tvar v'}, [b]) when vs_equal v' v -> b
      | _ -> raise Exit
    in
    let p, t = t_open_branch b in
    let pl = match p with
      | { pat_node = Term.Papp (lsc', pl) } when ls_equal lsc lsc' -> pl
      | _ -> raise Exit
    in
    let i = match t.t_node with
      | Term.Tvar xi ->
	  let rec index i = function
	    | [] -> raise Exit
	    | { pat_node = Term.Pvar v} :: _ when vs_equal v xi -> i
	    | _ :: l -> index (i+1) l
	  in
	  index 0 pl
      | _ ->
	  raise Exit
    in
    Some (ts, lsc, i)
  with Exit ->
    None

let list_fields uc fl =
  let type_field (q, e) =
    let loc = qloc q in
    let ls = find_lsymbol q uc in
    match is_projection uc ls with
      | None -> errorm ~loc "this is not a record field"
      | Some pr -> pr, loc, e
  in
  let fl = List.map type_field fl in
  let (ts,cs,_),_,_ = List.hd fl in
  let n = List.length cs.ls_args in
  let args = Array.create n None in
  let check_field ((ts',_,i),loc,e) =
    if not (ts_equal ts' ts) then
      errorm ~loc "this should be a field for type %a" Pretty.print_ts ts;
    assert (0 <= i && i < n);
    if args.(i) <> None then
      errorm ~loc "this record field is defined several times";
    args.(i) <- Some (loc,e);
  in
  List.iter check_field fl;
  ts,cs,Array.to_list args


(** Typing types *)

let split_qualid = function
  | Qident id -> [], id.id
  | Qdot (p, id) -> string_list_of_qualid [] p, id.id

(** Typing terms and formulas *)

let binop = function
  | PPand -> Fand
  | PPor -> For
  | PPimplies -> Fimplies
  | PPiff -> Fiff

let check_pat_linearity p =
  let s = ref Sstr.empty in
  let add id =
    if Sstr.mem id.id !s then
      errorm ~loc:id.id_loc "duplicate variable %s" id.id;
    s := Sstr.add id.id !s
  in
  let rec check p = match p.pat_desc with
    | PPpwild -> ()
    | PPpvar id -> add id
    | PPpapp (_, pl) | PPptuple pl -> List.iter check pl
    | PPprec pfl -> List.iter (fun (_,p) -> check p) pfl
    | PPpas (p, id) -> check p; add id
    | PPpor (p, _) -> check p
  in
  check p

let fresh_type_var loc =
  let tv = create_tvsymbol (id_user "a" loc) in
  tyvar (create_ty_decl_var ~loc ~user:false tv)

let rec dpat env pat =
  let env, n, ty = dpat_node pat.pat_loc env pat.pat_desc in
  env, { dp_node = n; dp_ty = ty }

and dpat_node loc env = function
  | PPpwild ->
      let ty = fresh_type_var loc in
      env, Pwild, ty
  | PPpvar x ->
      let ty = fresh_type_var loc in
      let env = { env with dvars = Mstr.add x.id ty env.dvars } in
      env, Pvar x, ty
  | PPpapp (x, pl) ->
      let s, tyl, ty = specialize_fsymbol x env.uc in
      let env, pl = dpat_args s.ls_name loc env tyl pl in
      env, Papp (s, pl), ty
  | PPprec fl ->
      let renv = ref env in
      let _,cs,fl = list_fields env.uc fl in
      let tyl,ty = Denv.specialize_lsymbol ~loc cs in
      let al = List.map2 (fun f ty -> match f with
        | Some (_,e) ->
            let loc = e.pat_loc in
            let env,e = dpat !renv e in
            unify_raise ~loc e.dp_ty ty;
            renv := env;
            e
        | None -> { dp_node = Pwild; dp_ty = ty }) fl tyl
      in
      !renv, Papp (cs,al), Util.of_option ty
  | PPptuple pl ->
      let n = List.length pl in
      let s = fs_tuple n in
      let tyl = List.map (fun _ -> fresh_type_var loc) pl in
      let env, pl = dpat_args s.ls_name loc env tyl pl in
      let ty = tyapp (ts_tuple n, tyl) in
      env, Papp (s, pl), ty
  | PPpas (p, x) ->
      let env, p = dpat env p in
      let env = { env with dvars = Mstr.add x.id p.dp_ty env.dvars } in
      env, Pas (p,x), p.dp_ty
  | PPpor (p, q) ->
      let env, p = dpat env p in
      let env, q = dpat env q in
      unify_raise ~loc p.dp_ty q.dp_ty;
      env, Por (p,q), p.dp_ty

and dpat_args s loc env el pl =
  let n = List.length el and m = List.length pl in
  if n <> m then error ~loc (BadNumberOfArguments (s, m, n));
  let rec check_arg env = function
    | [], [] ->
	env, []
    | a :: al, p :: pl ->
	let loc = p.pat_loc in
	let env, p = dpat env p in
	unify_raise ~loc p.dp_ty a;
	let env, pl = check_arg env (al, pl) in
	env, p :: pl
    | _ ->
	assert false
  in
  check_arg env (el, pl)

let rec trigger_not_a_term_exn = function
  | TermExpected -> true
  | Loc.Located (_, exn) -> trigger_not_a_term_exn exn
  | _ -> false

let check_quant_linearity uqu =
  let s = ref Sstr.empty in
  let check id =
    if Sstr.mem id.id !s then errorm ~loc:id.id_loc "duplicate variable %s" id.id;
    s := Sstr.add id.id !s
  in
  List.iter (fun (idl, _) -> Util.option_iter check idl) uqu

let check_highord env x tl = match x with
  | Qident { id = x } when Mstr.mem x env.dvars -> true
  | _ -> List.length tl > List.length ((find_lsymbol x env.uc).ls_args)

let apply_highord loc x tl = match List.rev tl with
  | a::[] -> [{pp_loc = loc; pp_desc = PPvar x}; a]
  | a::tl -> [{pp_loc = loc; pp_desc = PPapp (x, List.rev tl)}; a]
  | [] -> assert false

let rec dterm ?(localize=false) env { pp_loc = loc; pp_desc = t } =
  let n, ty = dterm_node ~localize loc env t in
  let t = { dt_node = n; dt_ty = ty } in
  if localize then
    let n = Tnamed (Ident.label ~loc "", t) in
    { dt_node = n; dt_ty = ty }
  else
    t

and dterm_node ~localize loc env = function
  | PPvar (Qident {id=x}) when Mstr.mem x env.dvars ->
      (* local variable *)
      let ty = Mstr.find x env.dvars in
      Tvar x, ty
  | PPvar x ->
      (* 0-arity symbol (constant) *)
      let s, tyl, ty = specialize_fsymbol x env.uc in
      let n = List.length tyl in
      if n > 0 then error ~loc (BadNumberOfArguments (s.ls_name, 0, n));
      Tapp (s, []), ty
  | PPapp (x, tl) when check_highord env x tl ->
      let tl = apply_highord loc x tl in
      let atyl, aty = Denv.specialize_lsymbol ~loc fs_func_app in
      let tl = dtype_args fs_func_app.ls_name loc env atyl tl in
      Tapp (fs_func_app, tl), Util.of_option aty
  | PPapp (x, tl) ->
      let s, tyl, ty = specialize_fsymbol x env.uc in
      let tl = dtype_args s.ls_name loc env tyl tl in
      Tapp (s, tl), ty
  | PPtuple tl ->
      let n = List.length tl in
      let s = fs_tuple n in
      let tyl = List.map (fun _ -> fresh_type_var loc) tl in
      let tl = dtype_args s.ls_name loc env tyl tl in
      let ty = tyapp (ts_tuple n, tyl) in
      Tapp (s, tl), ty
  | PPinfix (e1, x, e2) ->
      let s, tyl, ty = specialize_fsymbol (Qident x) env.uc in
      let tl = dtype_args s.ls_name loc env tyl [e1; e2] in
      Tapp (s, tl), ty
  | PPconst (ConstInt _ as c) ->
      Tconst c, tyapp (Ty.ts_int, [])
  | PPconst (ConstReal _ as c) ->
      Tconst c, tyapp (Ty.ts_real, [])
  | PPlet (x, e1, e2) ->
      let e1 = dterm ~localize env e1 in
      let ty = e1.dt_ty in
      let env = { env with dvars = Mstr.add x.id ty env.dvars } in
      let e2 = dterm ~localize env e2 in
      Tlet (e1, x, e2), e2.dt_ty
  | PPmatch (e1, bl) ->
      let t1 = dterm ~localize env e1 in
      let ty1 = t1.dt_ty in
      let tb = fresh_type_var loc in (* the type of all branches *)
      let branch (p, e) =
        let env, p = dpat_list env ty1 p in
        let loc = e.pp_loc in
	let e = dterm ~localize env e in
	unify_raise ~loc e.dt_ty tb;
        p, e
      in
      let bl = List.map branch bl in
      Tmatch (t1, bl), tb
  | PPnamed (x, e1) ->
      let e1 = dterm ~localize env e1 in
      Tnamed (x, e1), e1.dt_ty
  | PPcast (e1, ty) ->
      let loc = e1.pp_loc in
      let e1 = dterm ~localize env e1 in
      let ty = dty env ty in
      unify_raise ~loc e1.dt_ty ty;
      e1.dt_node, ty
  | PPif (e1, e2, e3) ->
      let loc = e3.pp_loc in
      let e2 = dterm ~localize env e2 in
      let e3 = dterm ~localize env e3 in
      unify_raise ~loc e3.dt_ty e2.dt_ty;
      Tif (dfmla ~localize env e1, e2, e3), e2.dt_ty
  | PPeps (x, ty, e1) ->
      let ty = dty env ty in
      let env = { env with dvars = Mstr.add x.id ty env.dvars } in
      let e1 = dfmla ~localize env e1 in
      Teps (x, ty, e1), ty
  | PPquant ((PPlambda|PPfunc|PPpred) as q, uqu, trl, a) ->
      check_quant_linearity uqu;
      let uquant env (idl,ty) =
        let ty = dty env ty in
        let id = match idl with
          | Some id -> id
          | None -> assert false
        in
        { env with dvars = Mstr.add id.id ty env.dvars }, (id,ty)
      in
      let env, uqu = map_fold_left uquant env uqu in
      let trigger e =
	try
	  TRterm (dterm ~localize env e)
	with exn when trigger_not_a_term_exn exn ->
	  TRfmla (dfmla ~localize env e)
      in
      let trl = List.map (List.map trigger) trl in
      let e = match q with
        | PPfunc -> TRterm (dterm ~localize env a)
        | PPpred -> TRfmla (dfmla ~localize env a)
        | PPlambda -> trigger a
        | _ -> assert false
      in
      let id, ty, f = match e with
        | TRterm t ->
            let id = { id = "fc"; id_lab = []; id_loc = loc } in
            let tyl,ty = List.fold_right (fun (_,uty) (tyl,ty) ->
              let nty = tyapp (ts_func, [uty;ty]) in ty :: tyl, nty)
              uqu ([],t.dt_ty)
            in
            let h = { dt_node = Tvar id.id ; dt_ty = ty } in
            let h = List.fold_left2 (fun h (uid,uty) ty ->
              let u = { dt_node = Tvar uid.id ; dt_ty = uty } in
              { dt_node = Tapp (fs_func_app, [h;u]) ; dt_ty = ty })
              h uqu tyl
            in
            id, ty, Fapp (ps_equ, [h;t])
        | TRfmla f ->
            let id = { id = "pc"; id_lab = []; id_loc = loc } in
            let (uid,uty),uqu = match List.rev uqu with
              | uq :: uqu -> uq, List.rev uqu
              | [] -> assert false
            in
            let tyl,ty = List.fold_right (fun (_,uty) (tyl,ty) ->
              let nty = tyapp (ts_func, [uty;ty]) in ty :: tyl, nty)
              uqu ([],tyapp (ts_pred, [uty]))
            in
            let h = { dt_node = Tvar id.id ; dt_ty = ty } in
            let h = List.fold_left2 (fun h (uid,uty) ty ->
              let u = { dt_node = Tvar uid.id ; dt_ty = uty } in
              { dt_node = Tapp (fs_func_app, [h;u]) ; dt_ty = ty })
              h uqu tyl
            in
            let u = { dt_node = Tvar uid.id ; dt_ty = uty } in
            id, ty, Fbinop (Fiff, Fapp (ps_pred_app, [h;u]), f)
      in
      Teps (id, ty, Fquant (Fforall, uqu, trl, f)), ty
  | PPrecord fl ->
      let _,cs,fl = list_fields env.uc fl in
      let tyl,ty = Denv.specialize_lsymbol ~loc cs in
      let al = List.map2 (fun f ty -> match f with
        | Some (_,e) ->
            let loc = e.pp_loc in
            let e = dterm ~localize env e in
            unify_raise ~loc e.dt_ty ty;
            e
        | None -> errorm ~loc "some record fields are missing") fl tyl
      in
      Tapp (cs,al), Util.of_option ty
  | PPupdate (e,fl) ->
      let n = ref (-1) in
      let q = Queue.create () in
      let e = dterm ~localize env e in
      let _,cs,fl = list_fields env.uc fl in
      (* prepare the pattern *)
      let tyl,ty = Denv.specialize_lsymbol ~loc cs in
      unify_raise ~loc e.dt_ty (Util.of_option ty);
      let pl = List.map2 (fun f ty -> match f with
        | Some _ ->
            { dp_node = Pwild ; dp_ty = ty }
        | None ->
            let x = (incr n; "x:" ^ string_of_int !n) in
            let i = { id = x ; id_lab = []; id_loc = loc } in
            Queue.add (x,ty) q;
            { dp_node = Pvar i ; dp_ty = ty }) fl tyl
      in
      let p = { dp_node = Papp (cs,pl) ; dp_ty = e.dt_ty } in
      (* prepare the result *)
      let tyl,ty = Denv.specialize_lsymbol ~loc cs in
      let al = List.map2 (fun f ty -> match f with
        | Some (_,e) ->
            let loc = e.pp_loc in
            let e = dterm ~localize env e in
            unify_raise ~loc:loc e.dt_ty ty;
            e
        | None ->
            let (x,xty) = Queue.take q in
            unify_raise ~loc xty ty;
            { dt_node = Tvar x ; dt_ty = ty }) fl tyl
      in
      let t = { dt_node = Tapp (cs,al) ; dt_ty = Util.of_option ty } in
      Tmatch (e,[p,t]), t.dt_ty
  | PPquant _ | PPbinop _ | PPunop _ | PPfalse | PPtrue ->
      error ~loc TermExpected

and dfmla ?(localize=false) env { pp_loc = loc; pp_desc = f } =
  let n = dfmla_node ~localize loc env f in
  if localize then Fnamed (Ident.label ~loc "", n) else n

and dfmla_node ~localize loc env = function
  | PPtrue ->
      Ftrue
  | PPfalse ->
      Ffalse
  | PPunop (PPnot, a) ->
      Fnot (dfmla ~localize env a)
  | PPbinop (a, (PPand | PPor | PPimplies | PPiff as op), b) ->
      Fbinop (binop op, dfmla ~localize env a, dfmla ~localize env b)
  | PPif (a, b, c) ->
      Fif (dfmla ~localize env a, dfmla ~localize env b, dfmla ~localize env c)
  | PPquant (q, uqu, trl, a) ->
      check_quant_linearity uqu;
      let uquant env (idl,ty) =
        let ty = dty env ty in
        let id = match idl with
          | Some id -> id
          | None -> assert false
        in
        { env with dvars = Mstr.add id.id ty env.dvars }, (id,ty)
      in
      let env, uqu = map_fold_left uquant env uqu in
      let trigger e =
	try
	  TRterm (dterm ~localize env e)
	with exn when trigger_not_a_term_exn exn ->
	  TRfmla (dfmla ~localize env e)
      in
      let trl = List.map (List.map trigger) trl in
      let q = match q with
        | PPforall -> Fforall
        | PPexists -> Fexists
        | _ -> error ~loc PredicateExpected
      in
      Fquant (q, uqu, trl, dfmla ~localize env a)
  | PPapp (x, tl) when check_highord env x tl ->
      let tl = apply_highord loc x tl in
      let atyl, _ = Denv.specialize_lsymbol ~loc ps_pred_app in
      let tl = dtype_args ps_pred_app.ls_name loc env atyl tl in
      Fapp (ps_pred_app, tl)
  | PPapp (x, tl) ->
      let s, tyl = specialize_psymbol x env.uc in
      let tl = dtype_args s.ls_name loc env tyl tl in
      Fapp (s, tl)
  | PPinfix (e12, op2, e3) ->
      begin match e12.pp_desc with
	| PPinfix (_, op1, e2) when is_psymbol (Qident op1) env.uc ->
	    let e23 = { pp_desc = PPinfix (e2, op2, e3); pp_loc = loc } in
	    Fbinop (Fand, dfmla ~localize env e12, dfmla ~localize env e23)
	| _ ->
	    let s, tyl = specialize_psymbol (Qident op2) env.uc in
	    let tl = dtype_args s.ls_name loc env tyl [e12; e3] in
	    Fapp (s, tl)
      end
  | PPlet (x, e1, e2) ->
      let e1 = dterm ~localize env e1 in
      let ty = e1.dt_ty in
      let env = { env with dvars = Mstr.add x.id ty env.dvars } in
      let e2 = dfmla ~localize env e2 in
      Flet (e1, x, e2)
  | PPmatch (e1, bl) ->
      let t1 = dterm ~localize env e1 in
      let ty1 = t1.dt_ty in
      let branch (p, e) =
        let env, p = dpat_list env ty1 p in
        p, dfmla ~localize env e
      in
      Fmatch (t1, List.map branch bl)
  | PPnamed (x, f1) ->
      let f1 = dfmla ~localize env f1 in
      Fnamed (x, f1)
  | PPvar (Qident s | Qdot (_,s) as x) when is_uppercase s.id.[0] ->
      let pr = find_prop x env.uc in
      Fvar (Decl.find_prop (Theory.get_known env.uc) pr)
  | PPvar x ->
      let s, tyl = specialize_psymbol x env.uc in
      let tl = dtype_args s.ls_name loc env tyl [] in
      Fapp (s, tl)
  | PPeps _ | PPconst _ | PPcast _ | PPtuple _ | PPrecord _ | PPupdate _ ->
      error ~loc PredicateExpected

and dpat_list env ty p =
  check_pat_linearity p;
  let loc = p.pat_loc in
  let env, p = dpat env p in
  unify_raise ~loc p.dp_ty ty;
  env, p

and dtype_args s loc env el tl =
  let n = List.length el and m = List.length tl in
  if n <> m then error ~loc (BadNumberOfArguments (s, m, n));
  let rec check_arg = function
    | [], [] ->
	[]
    | a :: al, t :: bl ->
	let loc = t.pp_loc in
	let t = dterm env t in
	unify_raise ~loc t.dt_ty a;
	t :: check_arg (al, bl)
    | _ ->
	assert false
  in
  check_arg (el, tl)

(** Add projection functions for the algebraic types *)

let add_projection cl p (fs,tyarg,tyval) th =
  let vs = create_vsymbol (id_fresh p) tyval in
  let per_cs (_,id,pl) =
    let cs = find_lsymbol (Qident id) th in
    let tc = match cs.ls_value with
      | None -> assert false
      | Some t -> t
    in
    let m = ty_match Mtv.empty tc tyarg in
    let per_param ty (n,_) = match n with
      | Some id when id.id = p -> pat_var vs
      | _ -> pat_wild (ty_inst m ty)
    in
    let al = List.map2 per_param cs.ls_args pl in
    t_close_branch (pat_app cs al tyarg) (t_var vs)
  in
  let vs = create_vsymbol (id_fresh "u") tyarg in
  let t = t_case (t_var vs) (List.map per_cs cl) in
  let d = make_fs_defn fs [vs] t in
  add_logic_decl th [d]

let add_projections th d = match d.td_def with
  | TDabstract | TDalias _ -> th
  | TDrecord _ -> assert false
  | TDalgebraic cl ->
      let per_cs acc (_,id,pl) =
        let cs = find_lsymbol (Qident id) th in
        let tc = match cs.ls_value with
          | None -> assert false
          | Some t -> t
        in
        let per_param acc ty (n,_) = match n with
          | Some { id = id ; id_lab = labels ; id_loc = loc }
            when not (Mstr.mem id acc) ->
              let fn = id_user ~labels id loc in
              let fs = create_fsymbol fn [tc] ty in
              Mstr.add id (fs,tc,ty) acc
          | _ -> acc
        in
        List.fold_left2 per_param acc cs.ls_args pl
      in
      let ps = List.fold_left per_cs Mstr.empty cl in
      try Mstr.fold (add_projection cl) ps th
      with e -> raise (Loc.Located (d.td_loc, e))

(** Typing declarations, that is building environments. *)

open Ptree

let add_types dl th =
  let def = List.fold_left
    (fun def d ->
      let id = d.td_ident.id in
      if Mstr.mem id def then error ~loc:d.td_loc (Clash id);
      Mstr.add id d def)
    Mstr.empty dl
  in
  let tysymbols = Hashtbl.create 17 in
  let rec visit x =
    try
      match Hashtbl.find tysymbols x with
	| None -> error CyclicTypeDef
	| Some ts -> ts
    with Not_found ->
      Hashtbl.add tysymbols x None;
      let d = Mstr.find x def in
      let id = d.td_ident.id in
      let vars = Hashtbl.create 17 in
      let vl =
	List.map
	  (fun { id = v ; id_lab = labels ; id_loc = loc } ->
	     if Hashtbl.mem vars v then error ~loc (DuplicateTypeVar v);
	     let i = create_tvsymbol (id_user ~labels v loc) in
	     Hashtbl.add vars v i;
	     i)
	  d.td_params
      in
      let id = id_user id ~labels:d.td_ident.id_lab d.td_loc in
      let ts = match d.td_def with
	| TDalias ty ->
	    let rec apply = function
	      | PPTtyvar v ->
		  begin
		    try ty_var (Hashtbl.find vars v.id)
		    with Not_found -> error ~loc:v.id_loc (UnboundTypeVar v.id)
		  end
	      | PPTtyapp (tyl, q) ->
		  let ts = match q with
		    | Qident x when Mstr.mem x.id def ->
			visit x.id
		    | Qident _ | Qdot _ ->
			find_tysymbol q th
		  in
		  begin try
		    ty_app ts (List.map apply tyl)
		  with Ty.BadTypeArity (_, tsal, tyll) ->
		    error ~loc:(qloc q) (TypeArity (q, tsal, tyll))
		  end
	      | PPTtuple tyl ->
		  let ts = ts_tuple (List.length tyl) in
		  ty_app ts (List.map apply tyl)
	    in
	    create_tysymbol id vl (Some (apply ty))
	| TDabstract | TDalgebraic _ ->
	    create_tysymbol id vl None
	| TDrecord _ ->
	    assert false
      in
      Hashtbl.add tysymbols x (Some ts);
      ts
  in
  let tsl = List.rev_map (fun d -> visit d.td_ident.id, Tabstract) dl in
  let th' = try add_ty_decl th tsl
    with ClashSymbol s -> error ~loc:(Mstr.find s def).td_loc (Clash s)
  in
  let csymbols = Hashtbl.create 17 in
  let decl d =
    let ts, th' = match Hashtbl.find tysymbols d.td_ident.id with
      | None ->
	  assert false
      | Some ts ->
	  let th' = create_denv th' in
	  let vars = th'.utyvars in
	  List.iter
	    (fun v ->
	       Hashtbl.add vars v.tv_name.id_string
                  (create_ty_decl_var ~user:true v))
	    ts.ts_args;
	  ts, th'
    in
    let d = match d.td_def with
      | TDabstract | TDalias _ ->
	  Tabstract
      | TDalgebraic cl ->
	  let ty = ty_app ts (List.map ty_var ts.ts_args) in
	  let constructor (loc, { id = id ; id_lab = labels }, pl) =
	    let param (_,t) = ty_of_dty (dty th' t) in
	    let tyl = List.map param pl in
	    Hashtbl.replace csymbols id loc;
	    create_fsymbol (id_user ~labels id loc) tyl ty
	  in
	  Talgebraic (List.map constructor cl)
      | TDrecord _ ->
	  assert false
    in
    ts, d
  in
  let th = try add_ty_decls th (List.map decl dl)
    with ClashSymbol s -> error ~loc:(Hashtbl.find csymbols s) (Clash s)
  in
  List.fold_left add_projections th dl

let record_typedef td = match td.td_def with
  | TDabstract | TDalgebraic _ | TDalias _ ->
      td
  | TDrecord fl ->
      let field (loc, mut, id, ty) =
	if mut then errorm ~loc "a logic record field cannot be mutable";
	Some id, ty
      in
      (* constructor for type t is "mk t" (and not String.capitalize t) *)
      let id = { td.td_ident with id = "mk " ^ td.td_ident.id } in
      { td with td_def = TDalgebraic [td.td_loc, id, List.map field fl] }

let add_types dl th =
  add_types (List.map record_typedef dl) th

let env_of_vsymbol_list vl =
  List.fold_left (fun env v -> Mstr.add v.vs_name.id_string v env) Mstr.empty vl

let add_logics dl th =
  let fsymbols = Hashtbl.create 17 in
  let psymbols = Hashtbl.create 17 in
  let denvs = Hashtbl.create 17 in
  (* 1. create all symbols and make an environment with these symbols *)
  let create_symbol th d =
    let id = d.ld_ident.id in
    let v = id_user ~labels:d.ld_ident.id_lab id d.ld_loc in
    let denv = create_denv th in
    Hashtbl.add denvs id denv;
    let type_ty (_,t) = ty_of_dty (dty denv t) in
    let pl = List.map type_ty d.ld_params in
    try match d.ld_type with
      | None -> (* predicate *)
	  let ps = create_psymbol v pl in
	  Hashtbl.add psymbols id ps;
	  add_logic_decl th [ps, None]
      | Some t -> (* function *)
	  let t = type_ty (None, t) in
	  let fs = create_fsymbol v pl t in
	  Hashtbl.add fsymbols id fs;
	  add_logic_decl th [fs, None]
    with ClashSymbol s -> error ~loc:d.ld_loc (Clash s)
  in
  let th' = List.fold_left create_symbol th dl in
  (* 2. then type-check all definitions *)
  let type_decl d =
    let id = d.ld_ident.id in
    let dadd_var denv (x, ty) = match x with
      | None -> denv
      | Some id -> { denv with dvars = Mstr.add id.id (dty denv ty) denv.dvars }
    in
    let denv = Hashtbl.find denvs id in
    let denv = { denv with uc = th' } in
    let denv = List.fold_left dadd_var denv d.ld_params in
    let create_var (x, _) ty =
      let id = match x with
	| None -> id_fresh "%x"
	| Some id -> id_user ~labels:id.id_lab id.id id.id_loc
      in
      create_vsymbol id ty
    in
    let mk_vlist = List.map2 create_var d.ld_params in
    match d.ld_type with
    | None -> (* predicate *)
	let ps = Hashtbl.find psymbols id in
        begin match d.ld_def with
	  | None -> ps,None
	  | Some f ->
	      let f = dfmla denv f in
              let vl = match ps.ls_value with
                | None -> mk_vlist ps.ls_args
                | _ -> assert false
              in
	      let env = env_of_vsymbol_list vl in
              make_ps_defn ps vl (fmla env f)
        end
    | Some ty -> (* function *)
	let fs = Hashtbl.find fsymbols id in
        begin match d.ld_def with
	  | None -> fs,None
	  | Some t ->
	      let loc = t.pp_loc in
	      let ty = dty denv ty in
	      let t = dterm denv t in
	      unify_raise ~loc t.dt_ty ty;
              let vl = match fs.ls_value with
                | Some _ -> mk_vlist fs.ls_args
                | _ -> assert false
              in
	      let env = env_of_vsymbol_list vl in
	      make_fs_defn fs vl (term env t)
        end
  in
  add_logic_decls th (List.map type_decl dl)

let type_term denv env t =
  let t = dterm denv t in
  term env t

let type_fmla denv env f =
  let f = dfmla denv f in
  fmla env f

let add_prop k loc s f th =
  let pr = create_prsymbol (id_user ~labels:s.id_lab s.id loc) in
  try add_prop_decl th k pr (type_fmla (create_denv th) Mstr.empty f)
  with ClashSymbol s -> error ~loc (Clash s)

let loc_of_id id = match id.id_origin with
  | User loc -> loc
  | _ -> assert false

let add_inductives dl th =
  (* 1. create all symbols and make an environment with these symbols *)
  let denv = create_denv th in
  let psymbols = Hashtbl.create 17 in
  let create_symbol th d =
    let id = d.in_ident.id in
    let v = id_user ~labels:d.in_ident.id_lab id d.in_loc in
    let type_ty (_,t) = ty_of_dty (dty denv t) in
    let pl = List.map type_ty d.in_params in
    let ps = create_psymbol v pl in
    Hashtbl.add psymbols id ps;
    try add_logic_decl th [ps, None]
    with ClashSymbol s -> error ~loc:d.in_loc (Clash s)
  in
  let th' = List.fold_left create_symbol th dl in
  let denv = { denv with uc = th' } in
  (* 2. then type-check all definitions *)
  let propsyms = Hashtbl.create 17 in
  let type_decl d =
    let id = d.in_ident.id in
    let ps = Hashtbl.find psymbols id in
    let clause (loc, { id = id ; id_lab = labels }, f) =
      Hashtbl.replace propsyms id loc;
      let f = type_fmla denv Mstr.empty f in
      create_prsymbol (id_user ~labels id loc), f
    in
    ps, List.map clause d.in_def
  in
  try add_ind_decls th (List.map type_decl dl)
  with
  | ClashSymbol s -> error ~loc:(Hashtbl.find propsyms s) (Clash s)
  | InvalidIndDecl (_,pr) -> errorm ~loc:(loc_of_id pr.pr_name)
      "not a clausal form"
  | NonPositiveIndDecl (_,pr,s) -> errorm ~loc:(loc_of_id pr.pr_name)
      "non-positive occurrence of %a" Pretty.print_ls s

(* parse declarations *)

let prop_kind = function
  | Kaxiom -> Paxiom
  | Kgoal -> Pgoal
  | Klemma -> Plemma

let find_theory env lenv q id = match q with
  | [] ->
      (* local theory *)
      begin try Mnm.find id lenv
      with Not_found -> find_theory env [] id end
  | _ :: _ ->
      (* theory in file f *)
      find_theory env q id

let rec clone_ns loc sl ns2 ns1 s =
  let clash id = error ~loc (Clash id.id_string) in
  let s = Mnm.fold (fun nm ns1 acc ->
    if not (Mnm.mem nm ns2.ns_ns) then acc else
    let ns2 = Mnm.find nm ns2.ns_ns in
    clone_ns loc sl ns2 ns1 acc) ns1.ns_ns s
  in
  let inst_ts = Mnm.fold (fun nm ts1 acc ->
    if not (Mnm.mem nm ns2.ns_ts) then acc else
    if not (Sid.mem ts1.ts_name sl) then acc else
    if Mts.mem ts1 acc then clash ts1.ts_name else
    let ts2 = Mnm.find nm ns2.ns_ts in
    Mts.add ts1 ts2 acc) ns1.ns_ts s.inst_ts
  in
  let inst_ls = Mnm.fold (fun nm ls1 acc ->
    if not (Mnm.mem nm ns2.ns_ls) then acc else
    if not (Sid.mem ls1.ls_name sl) then acc else
    if Mls.mem ls1 acc then clash ls1.ls_name else
    let ls2 = Mnm.find nm ns2.ns_ls in
    Mls.add ls1 ls2 acc) ns1.ns_ls s.inst_ls
  in
  { s with inst_ts = inst_ts; inst_ls = inst_ls }

let add_decl env lenv th = function
  | TypeDecl dl ->
      add_types dl th
  | LogicDecl dl ->
      add_logics dl th
  | IndDecl dl ->
      add_inductives dl th
  | PropDecl (loc, k, s, f) ->
      add_prop (prop_kind k) loc s f th
  | UseClone (loc, use, subst) ->
      let q, id = split_qualid use.use_theory in
      let t =
	try
	  find_theory env lenv q id
	with
	  | TheoryNotFound _ -> error ~loc (UnboundTheory use.use_theory)
      in
      let use_or_clone th = match subst with
	| None ->
	    use_export th t
	| Some s ->
            let add_inst s = function
              | CSns (p,q) ->
                  let find ns x = find_namespace_ns x ns in
                  let ns1 = option_fold find t.th_export p in
                  let ns2 = option_fold find (get_namespace th) q in
                  clone_ns loc t.th_local ns2 ns1 s
              | CStsym (p,q) ->
                  let ts1 = find_tysymbol_ns p t.th_export in
                  let ts2 = find_tysymbol q th in
                  if Mts.mem ts1 s.inst_ts
                  then error ~loc (Clash ts1.ts_name.id_string);
                  { s with inst_ts = Mts.add ts1 ts2 s.inst_ts }
              | CSlsym (p,q) ->
                  let ls1 = find_lsymbol_ns p t.th_export in
                  let ls2 = find_lsymbol q th in
                  if Mls.mem ls1 s.inst_ls
                  then error ~loc (Clash ls1.ls_name.id_string);
                  { s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
              | CSlemma p ->
                  let pr = find_prop_ns p t.th_export in
                  if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
                  then error ~loc (Clash pr.pr_name.id_string);
                  { s with inst_lemma = Spr.add pr s.inst_lemma }
              | CSgoal p ->
                  let pr = find_prop_ns p t.th_export in
                  if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
                  then error ~loc (Clash pr.pr_name.id_string);
                  { s with inst_goal = Spr.add pr s.inst_goal }
	    in
            let s = List.fold_left add_inst empty_inst s in
	    clone_export th t s
      in
      let n = match use.use_as with
	| None -> Some t.th_name.id_string
	| Some (Some x) -> Some x.id
	| Some None -> None
      in
      begin try match use.use_imp_exp with
	| Nothing ->
	    (* use T = namespace T use_export T end *)
	    let th = open_namespace th in
	    let th = use_or_clone th in
	    close_namespace th false n
	| Import ->
	    (* use import T = namespace T use_export T end import T *)
	    let th = open_namespace th in
	    let th = use_or_clone th in
	    close_namespace th true n
	| Export ->
	    use_or_clone th
      with ClashSymbol s -> error ~loc (Clash s)
      end
  | Meta (loc, id, al) ->
      let s = id.id in
      let convert = function
        | PMAts q  -> MAts (find_tysymbol q th)
        | PMAls q  -> MAls (find_lsymbol q th)
        | PMApr q  -> MApr (find_prop q th)
        | PMAstr s -> MAstr s
        | PMAint i -> MAint (int_of_string i)
      in
      let al = List.map convert al in
      begin try add_meta th (lookup_meta s) al
      with e -> raise (Loc.Located (loc,e)) end

let add_decl env lenv th d =
  if Debug.test_flag debug_parse_only then th else
  add_decl env lenv th d

let close_theory lenv { id = id ; id_loc = loc } th =
  if Mnm.mem id lenv then error ~loc (ClashTheory id);
  if Debug.test_flag debug_parse_only then lenv else
  Mnm.add id (close_theory th) lenv

let close_namespace loc import name th =
  let id = option_map (fun id -> id.id) name in
  try close_namespace th import id
  with ClashSymbol s -> error ~loc (Clash s)

(*
Local Variables:
compile-command: "unset LANG; make -C ../.. test"
End:
*)