include "vect.idr";
include "env.idr";
include "listmem.idr";
include "handle.idr";

data Filepath = F String;

getPath : Filepath -> String;
getPath (F p) = p;

data Perm = Read | Write | Execute;
data Purpose = Reading | Writing;
data FileState = Open Purpose | Closed;

pMode : Purpose -> String;
pMode Reading = "r";
pMode Writing = "w";

reqPerm : Purpose -> Perm;
reqPerm Reading = Read;
reqPerm Writing = Write;

data FileHandle : FileState -> # where
   OpenFile : (h:File) -> -- actual file
	      (FileHandle (Open p))
 | ClosedFile : FileHandle Closed;


data FH : # where mkFH : (FileHandle f) -> FH;

getFileState : FH -> FileState;
getFileState (mkFH {f} fh) = f;

HEnv : (Vect FileState n) -> #;
HEnv xs = Env FileState FileHandle xs;

using (ts:Vect FileState n, ts':Vect FileState n', tI:Vect FileState nI)
{

data OpenH : (Fin n) -> Purpose -> (Vect FileState n) -> # where
   openFirst : OpenH fO p (Open p :: ts)
 | openLater : (OpenH i p ts) -> (OpenH (fS i) p (x :: ts));

data ClosedH : (Fin n) -> (Vect FileState n) -> # where
   closedFirst : ClosedH fO (Closed :: ts)
 | closedLater : (ClosedH i ts) -> (ClosedH (fS i) (x :: ts));

data AllClosed : (Vect FileState n) -> # where
   acNil : AllClosed VNil
 | acCons : AllClosed ts -> AllClosed (Closed :: ts);

getFile : {i:Fin n} -> (OpenH i p ts) -> (env:HEnv ts) -> File;
getFile openFirst (Extend (OpenFile h) _) = h;
getFile (openLater p) (Extend x env) = getFile p env;

getPurpose : (i:Fin n) -> (Vect FileState n) -> Purpose;
getPurpose fO (Open p :: _) = p;
getPurpose (fS i) (x :: xs) = getPurpose i xs;

data Ty = TyNat | TyHandle Nat | TyUnit | TyLift #;

interpTy : Ty -> #;
interpTy TyNat = Nat;
interpTy (TyHandle n) = Fin n;
interpTy TyUnit = ();
interpTy (TyLift A) = A;

data [noElim] 
     Lang : (Vect FileState n) -> (Vect FileState n') -> Ty -># where
   ACTION : |(act:IO A) -> (Lang ts ts (TyLift A))
 | RETURN : (val:A) -> (Lang ts ts (TyLift A))
 | NOP : Lang ts ts TyUnit
 | FORGET : (Lang ts (snoc ts' Closed) t) -> (Lang ts ts' t)
 | CALL : (Lang VNil VNil t) -> (Lang ts ts t)
 | WHILE : (Lang ts ts (TyLift Bool)) -> (Lang ts ts TyUnit) -> 
	   (Lang ts ts TyUnit)
 | IF : (a:Bool) -> (Lang ts ts b) -> (Lang ts ts b) ->
        (Lang ts ts b)
 | BIND : (code:Lang ts tI ty)->
	  (k:(interpTy ty)->(Lang tI ts' tyout))->
	  (Lang ts ts' tyout)
 | OPEN : (p:Purpose) -> (fd:Filepath) -> 
	  (Lang ts (snoc ts (Open p)) (TyHandle (S n)))
 | CLOSE : (i : Fin n) -> (OpenH i (getPurpose i ts) ts) ->
	   (Lang ts (update i Closed ts) TyUnit) 
 | GETLINE : (i:Fin n) -> (p:OpenH i Reading ts) ->
             (Lang ts ts (TyLift String))
 | EOF : (i:Fin n) -> (p:OpenH i Reading ts) ->
         (Lang ts ts (TyLift Bool))
 | PUTLINE : (i:Fin n) -> (str:String) -> (p:OpenH i Writing ts) ->
             (Lang ts ts (TyUnit));

maybe : (x:Maybe a) -> |(default:b) -> (a->b) -> b;
maybe Nothing def f = def;
maybe (Just a) def f = f a;

nClosed : (n:Nat) -> (Vect FileState n);
nClosed O = VNil;
nClosed (S k) = Closed :: (nClosed k);

dumpVect : (Vect A n) -> String;
dumpVect VNil = "[]";
dumpVect (x :: xs) = "[*," ++ dumpVect xs ++ "]";

noFiles : Vect FileState O;
noFiles = VNil;

--- Some test data

dropLast : (HEnv (snoc ts x) & interpTy t) -> 
	   (HEnv ts & interpTy t);
dropLast (env, val) = (dropEnd env, val);

anyEnv : (HEnv ts) -> (HEnv VNil & interpTy t) -> 
	 (HEnv ts & interpTy t);
anyEnv env evP = (env, snd evP);

-- Binds which lift the IO operation so we can continue evaluation
-- under IODo


ibind : (IO ()) -> (() -> (IO b)) -> (IO b);
ibind f k = IODo (IOLift f) (\x => k II);

ibinda : (IO a) -> (a -> (IO b)) -> (IO b);
ibinda f k = IODo (IOLift f) k;

interp : (HEnv ts) -> (Lang ts ts' T) -> 
	 (IO (HEnv ts' & interpTy T));

interpBind : (HEnv ts & A) -> (A -> (Lang ts ts' B)) ->
	     (IO (HEnv ts' & interpTy B));
interpBind c k = interp (fst c) (k (snd c));

ioSnd : IO (a & b) -> IO b;
ioSnd p = do { p' <- p;
      	       return (snd p'); };

runInterp : IO (a & b) -> IO b;
runInterp p = ioSnd p;

interp env (ACTION io) = -- do { x <- io;
       	   	       	 --     return (env, x); };
                         ibinda io (\x => return (env, x));
interp env (RETURN val) = return (env, val);
interp env NOP = return (env, II);
interp env (WHILE test body) =
     ibinda (while (ioSnd (interp env test)) (ioSnd (interp env body)))
            (\k => return (env,II));
interp env (IF v thenp elsep) =
     ibinda (if v then (ioSnd (interp env thenp)) else (ioSnd (interp env elsep)))
            (\k => return (env, k));
interp env (FORGET p) = do { runp <- interp env p;
		             return (dropLast runp); }; 
interp env (CALL p) = ibinda (runInterp (interp Empty p))
		             (\callp => return (env, callp));
interp env (BIND code k) = bind (interp env code)
		                (\coderes => interpBind coderes k);

-- File operations

interp env (OPEN p fpath) 
   = do { fh <- fopen (getPath fpath) (pMode p);
	  return (addEnd env (OpenFile fh), bound); };
interp env (CLOSE i p)
   = do { fclose (getFile p env);
	  return (updateEnv env i ClosedFile, II); }; 
interp env (GETLINE i p)
   = do { str <- fread (getFile p env);
	  return (env, str); };
interp env (EOF i p)
   = do { e <- feof (getFile p env);
	  return (env, e); };
interp env (PUTLINE i str p)
   = do { fwrite (getFile p env) str;
     	  fwrite (getFile p env) "\n";
	  return (env, II); };

Uses : Nat -> Ty -> #;
Uses n t = Lang noFiles (nClosed n) t; 

freedSnoc : (Closed :: (nClosed n) = (snoc (nClosed n) Closed));
freedSnoc = ?freedSnocPrf;

UsesClosed : AllClosed (nClosed n);
UsesClosed {n=O} = acNil;
UsesClosed {n=S k} = acCons UsesClosed;

programA : (Uses n t) -> (Lang ts' ts' t);
programA {n=O} prog = CALL prog;
programA {n=S k} prog = ?doProgramS;

program : (x:Int) -> (Uses (intToNat x) t) -> (Lang ts' ts' t);
program x p = programA {n=intToNat x} p;

call : (Uses O t) -> (Lang ts' ts' t);
call prog = programA {n=O} prog;

FileSafe : Ty -> #;
FileSafe T = Lang noFiles noFiles T;

-- test programs

do using (BIND, RETURN) {

  copy : Filepath -> Filepath -> FileSafe TyUnit;
  copy infile outfile = program 2
           do { fh1 <- OPEN Reading infile;
	        fh2 <- OPEN Writing outfile;
		WHILE (do { e <- EOF (handle fh1) ?;
		      	    return (not e); })
		      (do { str <- GETLINE (handle fh1) ?;
--		      	    ACTION (putStrLn ("Writing " ++ str));
                            PUTLINE (handle fh2) str ?; 
                          });
                CLOSE (handle fh1) ?;
                CLOSE (handle fh2) ?;
	      };

  copyLine : Filepath -> Filepath -> FileSafe TyUnit;
  copyLine infile outfile = program 2
           do { 
	      	fh1 <- OPEN Reading infile;
	        fh2 <- OPEN Writing outfile;
		str <- GETLINE fO openFirst;
                PUTLINE (fS fO) str (openLater openFirst); 
                CLOSE (fS fO) ?;
                CLOSE (fO) ?;
	      };
}

}

-- test it


doProgramS proof {
        %intro T,k;
        %rewrite <- freedSnoc {n=k};
        %intro prog, n, xs;
        %fill programA (FORGET prog);
        %qed;
};

freedSnocPrf proof {
        %intro n;
        %induction n;
        %refl;
        %intro k;
        %intro k_IH;
        %compute;
        %rewrite k_IH;
        %refl;
        %qed;
};


copy_1 proof {
	%intro;
	%refine openFirst;
	%qed;
};
copy_2 proof {
	%intro;
	%refine openFirst;
	%qed;
};
copy_3 proof {
	%intro;
	%refine openLater;
	%refine openFirst;
	%qed;
};
copy_4 proof {
	%intro;
	%refine openFirst;
	%qed;
};
copy_5 proof {
	%intro;
	%refine openLater;
	%refine openFirst;
	%qed;
};

copyLine_1 proof {
	%intro;
	%refine openLater;
	%refine openFirst;
	%qed;
};

copyLine_2 proof {
	%intro;
	%refine openFirst;
	%qed;
};


run : FileSafe t -> IO (HEnv VNil & interpTy t);
run prog = interp Empty prog;

copyInt = \inf, outf => ioSnd (interp Empty (copy inf outf))
  %spec;
  %freeze copy;
  %transform runInterp (interp Empty (copy ?inf ?outf)) => copyInt ?inf ?outf;

do using (BIND, RETURN) {
  copyDyn : Filepath -> FileSafe TyUnit;
  copyDyn dfile = program 1
       do { fh1 <- OPEN Reading dfile;
       	    dat1 <- GETLINE (handle fh1) openFirst;
	    dat2 <- GETLINE (handle fh1) openFirst;
	    call (copy (F dat1) (F dat2));
	    CLOSE (handle fh1) openFirst;
	  };

  copyRec' : FileSafe TyUnit;

  copyRec : FileSafe TyUnit;
  copyRec = do { ACTION (putStr "File [END to end]: ");
  	       	 fname <- ACTION getStr;
		 IF (__strEq fname "END")  
		      NOP
		      (do { ACTION (putStrLn "Copying");
		      	    call (copyDyn (F fname));
	               	    call copyRec'; });
	       };

  copyRec' = copyRec;


}



copyDynInt = \df => ioSnd (interp Empty (copyDyn df))
  %spec;
  %freeze copyDyn;
  %transform runInterp (interp Empty (copyDyn ?df)) => copyDynInt ?df;

copyRecInt = ioSnd (interp Empty copyRec)
  %spec(copyRec');
  %freeze copyRec;
  %transform runInterp (interp Empty copyRec') => copyRecInt;

backup : List Filepath -> IO ();
backup Nil = return II;
backup (Cons (F x) xs) = do { copyInt (F x) (F (x++".bak"));
       	       	              backup xs; };


maincopy : Nat -> IO ();
maincopy O = return II;
maincopy (S k) = do { ans <- interp Empty (copyDyn (F "bigdatafile"));
	  	      putStrLn "Copied";
		      maincopy k;
        	      };

maincopyd : Nat -> IO ();
maincopyd O = return II;
maincopyd (S k) = do { ans <- copyDynInt (F "bigdatafile");
	  	       putStrLn "Copied";
		       maincopyd k;
        	       };


mainall : IO ();
mainall
     = do { ans <- interp Empty (copyLine (F "infile") (F "outfile"));
       	    putStrLn "Done test 1";
       	    backup (Cons (F "infile") (Cons (F "infile2") Nil));
	    putStrLn "Done test 2"; 
	    copyDynInt (F "datafile");
	    putStrLn "Done test 3"; 
	    copyRecInt;
	    putStrLn "Done test 4";
          };

main : IO ();
main = maincopyd (intToNat 10);