module Lookup where

import Vtslib

import Core_datatype

{-
(******************************************************************************)
(*  memoised lookup table of signatures.                                      *)
(******************************************************************************)
-}

{-
(******************************************************************************)
(*   A lookup table is an list of association lists.                          *)
(*   Each element of an association list consists of                          *)
(*         string                  - The name of a symbol  (or constructor)   *)
(*         int * bool              - The j index of a symbol, or              *)
(*         int * int * int list    - The j,k indexes for of a constructor     *)
(*         (int * opr) option      - The precedence and type of operator      *)
(*   The boolean in the symbol part indicates wheather the symbol is          *)
(*   accessabe by a rec expression.                                           *)
(*   in                                                                       *)
(******************************************************************************)
-}

type Index = Sum (Int , Bool) ( Int , Int , [(Int , Int)] )

type Entry = [(String , Option (Index , (Int , String) ))] 

type Lookup_table = [Entry]

{-

    local

(******************************************************************************)
(*   Turn a name into a lookup table                                          *)
(******************************************************************************)

    fun  get_nms jf (Name s) =
	    [(s, (jf, NONE))]
      | get_nms jf (Operator (s,p,opr)) =
      	    [(s,(jf,SOME (p,opr)))]

(******************************************************************************)
(*   Turn a list of names and a list of list of terms (taken from a           *)
(*   datatype declaration) and turn them into a lookup table                  *)
(******************************************************************************)

    and get_nmsL jf k [] [] =
    	    []
      | get_nmsL jf k (nm :: nmL) (tmL :: tmLL) =
      	    get_nms (inr (jf,k,(length tmL, rec_pars 0 tmL))) nm @ 
	    get_nmsL jf (k+1) nmL tmLL
      | get_nmsL jf k _ _ =
	    []

    and rec_pars _ [] = []
      | rec_pars i (tm :: tmL) = 
	    (if is_00_sm tm then [i] else []) @ rec_pars (i+1) tmL

    and is_00_sm (Sym (0,0,_,_)) = true 
      | is_00_sm _ = false

    
(******************************************************************************)
(*   Return the lookup table for a declaration                                *)
(******************************************************************************)

    fun get_dec_nms rec_flag j (Symbol_dec (_,attL)) =
	    (case get_att Name_Style attL
	       of SOME (Symbol_Name nm) => (get_nms (inl (j,rec_flag)) nm, j)
	        | _ => ([], j))
      | get_dec_nms rec_flag j (Axiom_dec (_,attL)) =
            (case get_att Name_Style attL
	       of SOME (Symbol_Name nm) => (get_nms (inl (j,rec_flag)) nm, j)
	        | _ => ([], j))
      | get_dec_nms rec_flag j (Def (_,_,attL)) =
      	    (case get_att Name_Style attL
	       of SOME (Symbol_Name nm) => (get_nms (inl (j,rec_flag)) nm, j)
	        | _ => ([], j))
      | get_dec_nms rec_flag j (Data (_,tmLL,attL)) =
            (case get_att Name_Style attL
	       of SOME (Datatype_Name (nm::nmL)) => 
		      (get_nms (inr (j,0,(0,[]))) nm @
			       get_nmsL j 1 nmL tmLL, j)
	        | _ => ([], j))
      | get_dec_nms rec_flag j (Decpair (dc1,dc2,_)) =
      	    let val (nms1,j1) = get_dec_nms rec_flag (j+1) dc1
	    	val (nms2,j2) = get_dec_nms rec_flag (j1+1) dc2
	    in (nms1@nms2, j2) end
		
(******************************************************************************)
(*   Return the lookup table for a pass1 decaration                           *)
(******************************************************************************)

    fun get_pdec_nms rec_flag j (P1_Dec (nmL, _)) = get_p1_nmsL rec_flag j nmL
      | get_pdec_nms rec_flag j (P1_Def (P1_Lhs (_,nm,_),_)) =
	    get_p1_nmsL rec_flag j [nm]
      | get_pdec_nms rec_flag j (P1_Define (nm,_,_)) =
	    get_p1_nmsL rec_flag j [nm]
      | get_pdec_nms rec_flag j (P1_Data (P1_Lhs (_,nm,_), conL,_)) =
      	    (get_nms (inr (j,0,(0,[]))) nm @ get_con_nms j 1 conL, j)
      | get_pdec_nms rec_flag j (P1_Decp (dc1,dc2)) =
      	    let val (nms1,j1) = get_pdec_nms rec_flag (j+1) dc1
	    	val (nms2,j2) = get_pdec_nms rec_flag (j1+1) dc2
	    in (nms1@nms2, j2) end
      | get_pdec_nms rec_flag j (P1_BDec dc) =
	    get_p1bdc rec_flag j dc
      | get_pdec_nms rec_flag j (P1_Database_dec dc) =
            let val (dc1, _) = internal_Dec dc
            in  get_dec_nms rec_flag j dc1 end

(******************************************************************************)
(*   Return the lookup table for a pass1 binding declaration                  *)
(******************************************************************************)

    and get_p1bdc rec_flag j (P1_Bdec (nmL, _)) =
            get_p1_nmsL rec_flag j nmL
      | get_p1bdc rec_flag j (P1_Bdecp (dc1,dc2)) =
            let val (nms1, j1) = get_p1bdc rec_flag (j+1) dc1
                val (nms2, j2) = get_p1bdc rec_flag (j1+1) dc2
            in (nms1@nms2, j2) end

(******************************************************************************)
(*   Return the llokup table for a list of names, that representing           *)
(*   sequence of paired declarations                                          *)
(******************************************************************************)

    and get_p1_nmsL rec_flag j [nm] = (get_nms (inl (j,rec_flag)) nm, j)
      | get_p1_nmsL rec_flag j (nm :: nmL) =
            let val nms1 = get_nms (inl (j+1,rec_flag)) nm
                val (nms2,j1) = get_p1_nmsL rec_flag (j+2) nmL
            in (nms1@nms2, j1) end
      | get_p1_nmsL rec_flag j [] = ([], j)

(******************************************************************************)
(*   Return the lookup table for the constuctors of a pass1 datatype          *)
(*   declaration                                                              *)
(******************************************************************************)

    and get_con_nms j k [] = []
      | get_con_nms j k (P1_Rhs (nm,tmL) :: nmL) =
            get_nms (inr (j,k,(length tmL,get_pvars 0 tmL))) nm @
	    get_con_nms j (k+1) nmL

    and get_pvars _ [] = []
      | get_pvars i (tm :: tmL) = 
	    (if is_00_psm tm then [i] else []) @ get_pvars (i+1) tmL

    and is_00_psm (P1_Sym (0,0,_)) = true
      | is_00_psm _ = false

    in (* local *)

(******************************************************************************)
(*   Take a signature and return its lookup table                             *)
(******************************************************************************)

    fun create_lookup_table (sg : sgn) : lookup_table =
	    case sg
	      of Empty _ =>
	             []
	       | Extend (dc,sg,_) =>
		     extend_lookup_table true dc (create_lookup_table sg)
	       | Combine (sg1,sg2,_,_,_) => 
		     let val tbl1 = create_lookup_table sg2
			 and tbl2 = create_lookup_table sg1
		     in [] :: tbl1 @ tbl2 end
	       | Share (sg,_,_,_,_,_) =>
		     [] :: create_lookup_table sg

(******************************************************************************)
(*   Extend a lookup table with a new declaration                             *)
(******************************************************************************)

    and extend_lookup_table rec_flag dc tbl : lookup_table =
	    let val (nms, _) = get_dec_nms rec_flag 0 dc
	    in nms :: tbl end

    fun combine_lookup_table tbl1 tbl2 : lookup_table =
	    tbl2 @ [[]] @ tbl1

    fun share_lookup_table tbl (i : int) (j : int)  : lookup_table =
	    [] :: tbl

    fun create_tbl (sg : pass1_sgn) : lookup_table =
	    case sg
	      of P1_Empty =>
	             []
	       | P1_Signature (dc) =>
		     extend_tbl true dc []
	       | P1_Extend (dc,sg) =>
		     extend_tbl true dc (create_tbl sg)
	       | P1_Combine (sg1,sg2) => 
		     let val tbl1 = create_tbl sg2
			 and tbl2 = create_tbl sg1
		     in [] :: tbl1 @ tbl2 end
	       | P1_Sharing (sg,_) =>
		     [] :: create_tbl sg
	       | P1_Database_sgn sg =>
		     create_lookup_table (internal_Sgn sg)
	       | P1_Named_sgn (_,sg) =>
		    create_tbl sg
	       | P1_plus_plus (sg1,sg2) =>
		     let val tbl1 = create_tbl sg2
			 and tbl2 = create_tbl sg1
		     in [] :: tbl1 @ tbl2 end

    and extend_tbl rec_flag pdc tbl  : lookup_table =
	    let val (nms,_) = get_pdec_nms rec_flag 0 pdc
	    in nms :: tbl end

(******************************************************************************)
(*   Lookup a string in the lookup table and return the pass1 symbol (or      *)
(*   constructor) and its optional operator status                            *)
(******************************************************************************)

    fun lookup_name (tbl : lookup_table) (str : string) =
	    let fun lookup i [] = 
			NONE
		  | lookup i (entry :: tbl) =
			case assoc str entry
			  of SOME (inl (j,true),opr_op) => 
				SOME (P1_Sym (i,j,true), opr_op)
			   | SOME (inr (j,k,_),opr_op) => 
				SOME (P1_Const (i,j,k,true), opr_op)
			   | _ => lookup (i+1) tbl
	    in lookup 0 tbl end

    fun lookup_rec_name (tbl : lookup_table) (str : string) =
	    let fun lookup i [] = 
			NONE
		  | lookup i (entry :: tbl) =
			case assoc str entry
			  of SOME (inl (j, false),opr_op) => 
				SOME (P1_Sym (i,j,true), opr_op)
			   | _ => lookup (i+1) tbl
	    in lookup 0 tbl end

    exception BadIndex

    fun lookup_sm_index (tbl : lookup_table) (i,j) =
	    let val entry = tbl !! i
		fun is_sm (_,(inl (j',_),_)) = j = j'
		  | is_sm _ = false
	    in case filter is_sm entry
		 of ((s,(inl (_,f),NONE)) :: _) => SOME (s, f, NONE) 
		  | ( (s,(inl (_,f),SOME (i, opr))) :: _) => 
			SOME (s, f, SOME (i,opr))
		  | _ => NONE
	    end

    fun lookup_cn_index (tbl : lookup_table) (i,j,k) =
	    let val entry = tbl !! i
		fun is_sm (_,(inr (j',k',_),_)) = (j',k') = (j,k)
		  | is_sm _ = false
	    in case filter is_sm entry
		 of ( (s,(inr (_,_,_),SOME (i, opr))) :: _) => 
			SOME (s, SOME (i,opr))
		  | ((s,(inr (_,_,_),_)) :: _) => SOME (s, NONE)
		  | _ => NONE
	    end
    end (* of local *)

    fun rec_parameters (tbl : lookup_table) (i,j,k) =
	    let val entry = tbl !! i
		fun is_sm (_,(inr (j',k',_),_)) = (j',k') = (j,k)
		  | is_sm _ = false
	    in case filter is_sm entry
		 of ((_,(inr (_,_,iL),_)) :: _) => iL
		  | _ => raise BadIndex
	    end

    fun operators ([] : lookup_table) = []
      | operators (ent :: tbl) =
	    foldr (curry op@) (operators tbl) (map get_ops ent)

    and get_ops (id, (inr _, SOME (i, opr))) =
	    [(id, Operator (id,i,opr))]
      | get_ops (id, (inr _, NONE)) =
	    [(id, Name id)]
      | get_ops _ =
	    []
end
-}