(*
 JungTaek Kim

 Copyright(c) 2000-2004 KAIST/SNU Research On Program Analysis System
 (National Creative Research Initiative Center 1998-2003)
 http://ropas.snu.ac.kr/n

 All rights reserved. This file is distributed under the terms of
 an Open Source License.
*)

open String_ast.Ast
open Format
open Location
open List
open Nsyntaxerr

let duptyid(loc,loc',name) = raise(Error(Duptyid(loc,loc',name)))

let dupdatacon(loc,loc',name) = raise(Error(Dupdatacon(loc,loc',name)))

let duppatvar(loc,loc',name) = raise(Error(Duppatvar(loc,loc',name)))

let orpaterr(loc) = raise(Error(Orpaterr(loc)))

let other(loc,msg) = raise(Error(Other(loc,msg)))

let eq_tyid (x,y) = x = y

let eq_conid (x,y) = x = y

let eq_varid (x,y) = x = y

let check_tyvar v = 
  match v with
    (s,loc) -> () (*print_string s*)

let check_tyvars l =
  match l with
    [] -> ()
  | [ty] -> check_tyvar ty
  | l -> iter check_tyvar l

let check_varid (v,loc) = () 
let check_tyid (v,loc) = () 
let check_conid (v,loc) = () 
let check_strid (v,loc) = () 
let check_sigid (v,loc) = () 
let check_fctid (v,loc) = () 

let exclude_varid ve (v,loc) = 
  try
    let (x,loc') = List.find (fun (x,loc) -> eq_varid (x,v)) ve in
      duppatvar (loc',loc,v)
  with Not_found -> ()

let exclude_conid ve (v,loc) = 
  try
    let (x,loc') = List.find (fun (x,loc) -> eq_conid (x,v)) ve in
      dupdatacon (loc',loc,v)
  with Not_found -> ()

let exclude_tyid ve (v,loc) = 
  try
    let (x,loc') = List.find (fun (x,loc) -> eq_tyid (x,v)) ve in
      duptyid (loc',loc,v)
  with Not_found -> ()

let check_label (v,loc) = () 

let check_varlongid (l,v,loc) = 
  match l with
    [] -> check_varid v
  | l  -> iter check_strid l; check_varid v

let check_tylongid (l,v,loc) = 
  match l with
    [] -> check_tyid v
  | l  -> iter check_strid l; check_tyid v

let check_conlongid (l,v,loc) = 
  match l with
    [] -> check_conid v
  | l  -> iter check_strid l; check_conid v

let check_strlongid (l,v,loc) = 
  match l with
    [] -> check_strid v
  | l  -> iter check_strid l; check_strid v

let rec check_ty t = 
  match t with
    VarTy (tyv,loc) -> check_tyvar tyv
  | ConstTy ([],lid,loc) -> check_tylongid lid
  | ConstTy ([hd],lid,loc) -> check_ty hd; check_tylongid lid
  | ConstTy (l,lid,loc) -> iter check_ty l; check_tylongid lid
  | RecordTy ([],loc) -> prerr_string "ty error\n"
  | RecordTy (l,loc) ->
      begin
        let check_tyrow (l,t,loc) = check_label l; check_ty t
        in iter check_tyrow l 
      end
  | TupleTy ([],loc) -> prerr_string "ty error\n"
  | TupleTy (l,loc) -> iter check_ty l
  | FunTy (t1,t2,loc) -> check_ty t1; check_ty t2
          
let check_con ve (id,tyop,loc) =
  exclude_conid ve id; 
  (match tyop with
    None -> () | Some(ty) -> check_ty ty); id::ve
   
let rec check_patrow ve (l,p,loc) = check_label l; check_pat ve p

and check_pat ve p =
  match p with
    WildPat(loc) -> ve
  | UnitPat(loc) -> ve
  | IntPat (i,loc) -> ve
  | StringPat (s,loc) -> ve
  | CharPat (c,loc) -> ve
  | RecordPat (l,loc) -> fold_left check_patrow ve l
  | SubRecordPat (l,loc) -> fold_left check_patrow ve l
  | RefPat (p,loc) -> check_pat ve p
  | VarPat ((id,info) as v,loc) -> 
  	  if id = "true" or id = "false" 
	  then ve
	  else (exclude_varid ve v; v::ve)
  | ConPat (l,loc) -> check_conlongid l; ve
  | AppPat (l,p,loc) -> check_conlongid l; check_pat ve p
  | ConstraintPat (p,t,loc) -> let ve' = check_pat ve p in check_ty t; ve'
  | AsPat (id,top,p,loc) ->
      exclude_varid ve id;
      begin
        match top with
	  None -> ()
	| Some (t) -> check_ty t
      end;
      check_pat (id::ve) p
  | TuplePat (l,loc) -> fold_left check_pat ve l
  | ListPat ([],loc) -> ve
  | ListPat (l,loc) -> fold_left check_pat ve l
  | ArrayPat (l,loc) -> fold_left check_pat ve l
  | OrPat (l,loc) -> check_orpat ve (l,loc)

and check_orpat ve (pl,loc) =
  match pl with
    [] -> ve
  | (hd::tl) as l -> 
    let nv = check_pat [] hd in
    let ve' = check_pat ve hd in
    let nvl = map (check_pat []) l in
    let eq_varenv l l' = 
      if (length l) = (length l') then
        let rec member l ((v,loc') as id) =
	  (match l with
	    [] -> orpaterr(loc)
	  | (v',_)::tl -> if v = v' then () else member tl id) in
	iter (member l) l'
      else orpaterr(loc)
    in iter (eq_varenv nv) nvl; ve'

       
let rec check_exprow (l, e,loc) = check_label l; check_exp e

and check_rule (p,e,loc) = ignore(check_pat [] p); check_exp e

and check_fnrule (pl,e,loc) = ignore(fold_left check_pat [] pl); check_exp e

and check_exp p =
  match p with
    UnitExp (loc) -> ()
  | IntExp (i,loc) -> ()
  | RealExp (f,loc) -> ()
  | StringExp (s,loc) -> ()
  | CharExp (c,loc) -> ()
  | VarExp (l,loc) -> check_varlongid l
  | ConExp (l,loc) -> check_conlongid l
  | AppExp (e,a,loc) -> check_exp e; check_exp a
  | RecordExp (l,loc) -> iter check_exprow l
  | RecordFieldExp (e,l,loc) -> check_exp e; check_label l
  | ArrayFieldExp (e,e',loc) -> check_exp e; check_exp e'
  | UpdateArrayExp (e,e',e'',loc) -> check_exp e; check_exp e'; check_exp e''
  | SubstRecordExp (e,l,e',loc) -> check_exp e; check_exp e'; check_label l
  | TupleExp (l,loc) -> iter check_exp l
  | ListExp ([],loc) -> ()
  | ListExp (l,loc) -> iter check_exp l
  | ArrayExp (l,loc) -> iter check_exp l
  | LetExp (d,e,loc) -> check_dec d; check_exp e
  | HandleExp (e,l,loc) -> check_exp e; iter check_rule l
  | RaiseExp (e,loc) -> check_exp e
  | FnExp (l,loc) -> iter check_fnrule l
  | AssignExp (e, e',loc) -> check_exp e; check_exp e'
  | RefExp (e,loc) -> check_exp e
  | DeRefExp (e,loc) -> check_exp e
  | SeqExp (l,loc) -> iter check_exp l
  | CaseExp (e,l,loc) -> check_exp e; iter check_rule l
  | IfExp (e,e',e'',loc) -> check_exp e; check_exp e'; check_exp e''
  | WhileExp (e,e',loc) -> check_exp e; check_exp e'
  | ForExp (id,e,e',e'',e''',loc) ->
      check_varid id; check_exp e; check_exp e'; check_exp e''; check_exp e'''
  | ConstraintExp (e,t,loc) -> check_exp e; check_ty t

and check_valbind (p,e,loc) = ignore(check_pat [] p); check_exp e

and check_recvalbind (p,e,loc) = 
  match e with
    FnExp(_,_) -> ignore(check_pat [] p); check_exp e
  | SeqExp([e'],_) -> check_recvalbind(p,e',loc)
  | _ -> other(loc, IllegalRecBind)

and check_funbind (l,loc) =
  begin
    let check_body (id,pl,e,loc) =
      check_varid id; ignore(fold_left check_pat [] pl); check_exp e
    in 
      iter check_body l
  end


and check_typebind ve tb =
  match tb with
    TypeBind (tyvs,id,ty,loc) ->
      check_tyvars tyvs; exclude_tyid ve id; check_ty ty; id::ve
  | DataBind (tyvs,id,cl,loc) ->
      check_tyvars tyvs; exclude_tyid ve id; 
      ignore(fold_left check_con [] cl); id::ve

and check_exnbind ve (c) = check_con ve c

and check_dec p =
  match p with
    ValDec (tyvs,l,loc) -> check_tyvars tyvs; iter check_valbind l
  | RecValDec (tyvs,l,loc) -> check_tyvars tyvs; iter check_recvalbind l
  | FunDec (tyvs,l,loc) -> check_tyvars tyvs; iter check_funbind l
  | TypeDec (l,loc) -> ignore(fold_left check_typebind [] l)
  | AbstypeDec (l,d,loc) -> ignore(fold_left check_typebind [] l); check_dec d
  | ExceptionDec (l,loc) -> ignore(fold_left check_exnbind [] l)
  | LocalDec (d,d',loc) -> check_dec d; check_dec d'
  | OpenDec (l,loc) -> iter check_strlongid l
  | SeqDec (l,loc) -> iter check_dec l

let check_longtypebind (tyvs,l,ty,loc) =
  check_tyvars tyvs; check_tylongid l; check_ty ty

let check_where (l,loc) = iter check_longtypebind l

let check_valdesc (id,t,loc) = check_varid id; check_ty t

let check_typedesc ve td =
  match td with
    TypeDesc (tyvs,id,loc) -> 
      check_tyvars tyvs; exclude_tyid ve id; id::ve
  | TypeBindDesc (tyvs,id,ty,loc) ->
      check_tyvars tyvs; exclude_tyid ve id; check_ty ty; id::ve
  | DataDesc (tyvs,id,cl,loc) -> 
      check_tyvars tyvs; exclude_tyid ve id; 
      ignore(fold_left check_con [] cl); id::ve

let check_exndesc ve (c) = check_con ve c

let rec check_strdesc (id,se,loc) = check_strid id; check_sigexp se

and check_spec p =
  match p with
    ValSpec (l,loc) -> iter check_valdesc l
  | TypeSpec (l,loc) -> ignore(fold_left check_typedesc [] l)
  | ExnSpec (l,loc) -> ignore(fold_left check_exndesc [] l)
  | IncludeSpec (s,loc) -> check_sigexp s
  | StrSpec (l,loc) -> iter check_strdesc l
  | SeqSpec (l,loc) -> iter check_spec l

and check_sigexp p =
  match p with
    VarSig (s,loc) -> check_sigid s
  | SigSig (s,loc) -> check_spec s
  | ConstraintSig (se,wh,loc) -> check_sigexp se; check_where wh

let check_sigexpop p =
  match p with
    None -> ()
  | Some(s) -> check_sigexp s

let check_sigbind (id,s,loc) = check_sigid id; check_sigexp s

let check_sigdec (l,loc) = iter check_sigbind l

let rec check_strexp p = 
  match p with
    VarStr (l,loc) -> check_strlongid l
  | StrStr (d,loc) -> check_strdec d
  | SigStr (ste, sie,loc) -> check_strexp ste; check_sigexp sie
  | FctAppStr (id, sl,loc) -> check_fctid id; iter check_strexp sl

and check_strbind (id, sgop, se,loc) =
  check_strid id; check_sigexpop sgop; check_strexp se


and check_strdec p = 
  match p with
    SimpleDec (d,loc) -> check_dec d
  | StrDec (l,loc) -> iter check_strbind l
  | SeqStrDec (l,loc) -> iter check_strdec l

let check_fctarg (id, se, loc) = check_strid id; check_sigexp se

let check_whereop p =
  match p with
    None -> ()
  | Some(w) -> check_where w

let check_fctdec p =
  match p with
    (id, al, sgop, se, loc) ->
      check_fctid id;
      iter check_fctarg al;
      check_sigexpop sgop;
      check_strexp se

let rec check_topdec p =
  match p with
    Sig (d,loc) -> check_sigdec d
  | Fct (d,loc) -> check_fctdec d
  | Str (d,loc) -> check_strdec d
  | SeqTopDec (dl,loc) -> 
      begin
        let check_one d = check_topdec d
        in List.iter check_one dl
      end

(***** poisson *****)

let check_toplevel p =
  match p with
    TopDef (d) -> check_topdec d
  | TopExp (el,loc) -> List.iter check_exp el
  | topdir -> ()

(*******************)

let check_error ast = check_topdec ast

(*
 Modification history.

 2000/03/27 By Judaigi

 - Remove print_databind and print_datadesc functions.
 - Change according to changes in ast.
*)