module Goals where

import Unparse

import X_interface

import Edlib

import Core_datatype

import Vtslib

import Tree

import Globals

import Lookup -- stub

import Parse

import Kernel

import Sub_Core1

import Sub_Core2

import Sub_Core3

import Sub_Core4

import Type_defs

import Tags

{-
(******************************************************************************)
(*   A goal consists of: a tactic name, a list of arguments, a comment, a     *)
(*   unique identifier and a specification.                                   *)
(******************************************************************************)
-}

data GOAL = Goal ( Option String )   
	         ( Option [String] ) -- arguments if any  
	         ( Option String )   -- comment if any
	         String	             -- unique identifier 
	         Obj       	     -- spec (goal)	    
	         Bool                -- read only?      
	         Sgn		     -- its signature  
	         Lookup_table	     -- its lookup table




data Obj  = TrmSpec ITrm |
            ThmSpec ITrm |	
            SgnSpec ISgn |
            DecSpec IDec 




data Done = TrmDone Trm |
            ThmDone Thm |
            SgnDone Sgn |
            DecDone Dec





show_option :: (String -> a) -> (b -> String) -> (Option b) -> a

show_option xfn gfn NONE = xfn "None"

show_option xfn gfn (SOME x) = xfn (gfn x)



summary_depth :: Int

summary_depth = 4



is_done :: (Option a) -> String

is_done NONE = ""

is_done (SOME _) = "Done"




short :: Int -> String -> String

short = short' -- Check that they are the same



short' :: Int -> String -> String

short' _ [] = []

short' 0 _ = "..."

short' i ('\n' : l) = ' ' : remove_spaces (i-1) l

short' i (c : l) = c : short' (i-1) l





remove_spaces :: Int -> String -> String

remove_spaces i ( ' ' : l) = remove_spaces i l

remove_spaces i ( '\n' : l) = remove_spaces i l

remove_spaces i l = short' i l





depth_print_tm i l sg tm = short 50 (unparse_trm sg l tm) 

depth_print_sg i l sg isg = short 50 (unparse_sgn sg l isg)

depth_print_dc i l sg dc = short 50 (unparse_dec sg l dc)




{-
show_parent gst [] 
	= x_unset_parent 

show_parent gst ((_,t):_) 
	= x_set_parent done summary 
	  where
	  (done,summary) = show_summary (get_attributes gst) t
-}



show_summary attL (Tree (Goal _ _ _ _ (TrmSpec tm) _ sg _) _ dn _ _) 
	= (is_done dn, depth_print_tm summary_depth attL sg tm)

show_summary attL (Tree (Goal _ _ _ _ (ThmSpec tm) _ sg _) _ dn _ _) 
	= (is_done dn, depth_print_tm summary_depth attL sg tm)

show_summary attL (Tree (Goal _ _ _ _ (SgnSpec isg) _ sg _) _ dn _ _) 
	= (is_done dn, depth_print_sg summary_depth attL sg isg)

show_summary attL (Tree (Goal _ _ _ _ (DecSpec dc) _ sg _) _ dn _ _) 
	= (is_done dn, depth_print_dc summary_depth attL sg dc)






show_goal :: Global_state -> (TREE GOAL b c) -> Xio_fn

show_goal  gst t@(Tree (Goal tac args com uid obj rw _ lt) _ _ _ _) 
	= show_node uid obj				     ...
	  show_option x_set_tactic id tac                    ...
	  show_option x_set_argument head args		     ...
	  show_option x_set_comment (short 50) com           ...
	  x_set_rw (if rw then "Editable" else "Read Only")  ...
	  x_set_goal done summary 
	  where
	  (done,summary) = show_summary (get_attributes gst) t
--	  (done,summary) = show_summary []  t




show_node uid (TrmSpec tm)
        = x_set_node ("Trm Node: " ++ uid)

show_node uid (ThmSpec tm)
        = x_set_node ("Thm Node: " ++ uid)

show_node uid (DecSpec dc)
        = x_set_node ("Dec Node: " ++ uid)

show_node uid (SgnSpec sg)
        = x_set_node ("Sgn Node: " ++ uid)





show_subgoals gst goalL 
	= x_set_subgoals (map (show_summary (get_attributes gst)) goalL)



show_done NONE     = x_set_done "Incomplete"

show_done (SOME _) = x_set_done "Complete"





{- old initialize
initialize (TreeSt t@(Tree goal goalL dn _ _ ) spine gst ) 
	= show_parent gst spine   ...
	  show_done dn            ...
	  show_goal gst t         ...
	  show_subgoals gst goalL
-}

initialize dset thy styp spec NONE 
        = get_tree dset thy styp spec NONE /./
	  exp
	  where
          exp ( SOME (tr@(TreeSt t@(Tree goal goalL dn _ _) spine gst)))
		= show_goal gst t          ...
                  show_subgoals gst goalL  ./.
                  reTurn tr 
          exp NONE 
		= end_x 	./.
		  return_err "no state" 


get_tree :: (Option String) -> (Option String) -> (Option String) ->
		(Option String) -> (Option String) -> Xin -> 
	 	 Xst ( MayBe (Option (Tree_state GOAL b Global_state )) String )

get_tree dset thy styp spec errmesg
	= x_form True (input_form dset thy styp spec errmesg) /./
	  exp
	  where
	  exp NONE = reTurn NONE 

          exp ( SOME [OutText ds, OutText ty, OutText sp, OutRadio st] )
		= parse_fn /.>/
		  genuid   /./
		  exp2 
		  where
                  parse_fn = case st of
                                   "Thm" -> mkspec ThmSpec parse_trm sp
                                   "Trm" -> mkspec TrmSpec parse_trm sp
--                                   "Dec" -> mkspec DecSpec parse_dec sp
--                                   "Sgn" -> mkspec SgnSpec parse_sgn sp
--                                   _     -> return_err "Bad Type" 
		  mkspec ctr p_fn sp
			= case p_fn sg ps sp of
				Ok res   -> reTurn ( ctr res )
				Bad mesg -> return_err mesg 
			  where
			  ps = default_tag_tbl

		  exp2 ( obj , uid )
			= reTurn ( SOME tst )
			  where
                          tst = TreeSt tr [] gst
                  	  tr  = Tree gl [] NONE ( \ x y -> y ) NONE
                  	  gl  = Goal NONE NONE NONE uid obj True sg lt
                  	  lt = [] --create_lookup_table isg
                  	  at = [] --defaults
                  	  gst = ( 0 , [] , default_tag_tbl ) 

	  exp _ = error "unimplemented in get_tree"
          sg  = empty --erestore_Sgn (ds,ty)
	  isg = internal_Sgn sg

{-
                    handle
                        Syntax (e,inp) =>
                            let val err = unerr e
                                val where = under_line_input inp
                            in get_tree (SOME ds) (SOME ty) (SOME st) (SOME sp)
                                        (SOME (err  ^ "\n" ^ where)) xio
                            end
                      | Expect (t1,t2,inp) =>
                            let val err = eexperr t1 t2
                                val where = under_line_input inp
                            in get_tree (SOME ds) (SOME ty) (SOME st) (SOME sp)
                                        (SOME (err  ^ "\n" ^ where)) xio
                            end
                      | Fail s =>
                            let val err = "Error: "^ s
                            in get_tree (SOME ds) (SOME ty) (SOME st) (SOME sp)
                                        (SOME err) xio
                            end
                      | _ =>

                           let val err = "Error in specification"
                            in get_tree (SOME ds) (SOME ty) (SOME st) (SOME sp)
                                        (SOME err) xio
                            end
                    )
-}


input_form dset thy styp spec errmesg 
	= [ InComment "XVTSEDIT VERSION 1.1",
            InSingleText "Dataset" ( case dset of 
				  	SOME ds -> ds 
				  	_       -> default_ds ),
            InSingleText "Theory " ( case thy  of 
				  	SOME ty -> ty 
				  	_       -> default_ty ),
            InMultiText  "Spec   " ( case spec of 
				  	SOME sp -> sp 
				  	_       -> "" ),
            InRadio "Type   " 
		    ( case styp of 
		  	SOME st -> my_index st types 
		  	_       -> 0 )
                    types ] ++
            (case errmesg of
                  SOME err -> [ InComment err ]
                  NONE     -> [] )


types = ["Thm","Trm","Sgn","Dec"]



my_index :: Eq b => b -> [b] -> Int

my_index s (s' : l) = if s == s' then 0 else 1 + my_index s l

my_index s []        = 0


default_ty = "empty"

default_ds = "default_ds not passed in yet"






{-
(******************************************************************************)
(*   When sorted out equalities, should check differences and only update     *)
(*   those fields which differ                                                *)
(******************************************************************************)
-}

update_state (TreeSt   ( Tree goal1 goalL1 dn1 _ _ ) spine1 gst1 )
       (TreeSt t@( Tree goal2 goalL2 dn2 _ _ ) spine2 gst2 ) 
	= ((show_goal gst2 t)          ...
	  (show_subgoals gst2 goalL2))



my_quit current 
	= x_form True form /./ exp
	  where
	  exp NONE       = reTurn False 
	  exp ( SOME _ ) = reTurn True 
	  form = [InComment "\n\nSelect ok to Quit\n\n"]



finish = end_x ./. reTurn (error "Finish state evaluated")