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

data Filepath = F String;
data Username = U String;
data Group = G String;

data Perm = Read | Write | Execute;

eqPerm : (x:Perm) -> (y:Perm) -> (Maybe (x=y));
eqPerm Read Read = Just (refl _);
eqPerm Write Write = Just (refl _);
eqPerm Execute Execute = Just (refl _);
eqPerm _ _ = Nothing;

isPermitted : (x:Perm) -> (ps:List Perm) -> (Maybe (Elem x ps));
isPermitted x ps = isLElem eqPerm x ps;

data GroupData = GD Group (List Username);
data FileData 
   = FS Filepath Username GroupData (List Perm) (List Perm) (List Perm);

using (op:List Perm, grp:List Perm, glp:List Perm,
       gusers:List Username, g:Group) {

data FileAccessible : Perm -> Username -> FileData -> # where
   GlobalAccess : 
      (Elem p glp) ->
      (FileAccessible p u (FS name owner group op grp glp))
 | UserAccess : 
      (Elem p op) ->
      (FileAccessible p u (FS name u group op grp glp))
 | GroupAccess : 
      (Elem p grp) ->
      (Elem u gusers) ->
      (FileAccessible p u (FS name owner (GD g gusers) op grp glp));
}

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 : (acc:FileAccessible (reqPerm p) u fd) ->
	      (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;

getFile : {i:Fin n} -> {xs:Vect FileState n} ->
	  (ElemIs i (Open p) xs) -> (env:HEnv xs) -> File;
getFile first (Extend (OpenFile _ h) _) = h;
getFile (later p) (Extend x env) = getFile p env;

showNat : Nat -> String;
showNat O = "O";
showNat (S k) = "s" ++ (showNat k);

data IHandle : (Vect FileState nh) -> # where 
   mkIH : {hs:Vect FileState (S n)} ->
	  (p:ElemIs bound (vlookup bound hs) hs) -> (IHandle hs);

geth : {xs:Vect FileState (S n)} -> (IHandle xs) -> (Fin (S n));
geth p = bound;

pIH : {xs:Vect FileState (S n)} ->
      (h:IHandle xs) -> (ElemIs (geth h) (vlookup bound xs) xs);
pIH (mkIH p) = p;

-- wknH pulls a Fin out of the IHandle and either:
--   fails, if it is already weaker than n
--   weakens until it is an n
-- This is partial, so *must* be run at compile time only and *must* fail
-- with a type error if it can't weaken.

makeWeaker : (Compare n nh) -> (i:Fin nh) -> (Fin n);
-- makeWeaker (cmpLT y) i FAIL
makeWeaker cmpEQ i = i;
makeWeaker (cmpGT y) i ?= weaken (nweaken {k=y} i); [wkn]
wkn proof {
        %intro;
        %rewrite <- plus_nSm {n=X} {m=y};
        %rewrite <- plus_comm X y;
        %fill value;
        %qed;
};

wknH : {n:Nat} -> {nh:Nat} -> (Fin (S nh)) -> (Fin n);
wknH {n} {nh} p = makeWeaker (compare n (S nh)) (bound {n=nh});

-- TyHandle records how many things were around when it was created.

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

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

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

data [noElim] 
     Lang : Username -> 
	    (Vect FileState n)->(Vect FileState n')->Ty-># where
   ACTION : (IO ()) -> (Lang u ts ts TyUnit)
 | RETURN : (val:A) -> (Lang u ts ts (TyLift A))
 | BIND : (code:Lang u ts tI ty)->
	  (k:(interpTy ty)->(Lang u tI ts' tyout))->
	  (Lang u ts ts' tyout)
 | OPEN : (p:Purpose) -> (fd:FileData) -> (FileAccessible (reqPerm p) u fd) ->
	  (Lang u ts (snoc ts (Open p)) 
			      (TyHandle (S n)))
 | CLOSE : (i : Fin n) -> (ElemIs i (Open p) ts) ->
	   (Lang u ts (update i Closed ts) TyUnit) 
 | READ : (i:Fin n) -> (p:ElemIs i (Open Reading) ts) ->
          (Lang u ts ts (TyLift String))
 | WRITE : (i:Fin n) -> (str:String) -> (p:ElemIs i (Open Writing) ts) ->
           (Lang u ts ts (TyUnit));

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

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

noFiles : Vect FileState O;
noFiles = VNil;

--- Some test data

edwin = U "edwin";
kevin = U "kevin";
staff = G "staff";

staff_data = GD staff (Cons edwin (Cons kevin Nil));

RWX = Cons Read (Cons Write (Cons Execute Nil));
R = Cons Read Nil;

filesdata = FS (F "filesdata") edwin staff_data RWX Nil Nil;
infile = FS (F "infile") kevin staff_data R R Nil;
outfile = FS (F "outfile") edwin staff_data RWX Nil Nil;

data I A B = MkPair A B;

fst : (I A B) -> A;
fst (MkPair a b) = a;

snd : (I A B) -> B;
snd (MkPair a b) = b;

nthElem : {i:Fin n} -> {xs:Vect A n} ->
	  (ElemIs i (vlookup i xs) xs);
nthElem {i=fO} {xs=VCons x xs} = first;
nthElem {i=fS k} {xs=VCons x xs} = later nthElem;

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

interpBind : (I (HEnv ts) A) -> (A -> (Lang u ts ts' B)) ->
	     (IO (I (HEnv ts') (interpTy B)));
interpBind (MkPair env val) k = interp env (k val);

interp env (ACTION io) = do { io;
			      return (MkPair env II); };
interp env (RETURN val) = return (MkPair env val);
interp env (BIND code k) = do { coderes <- interp env code;
				interpBind coderes k; };

-- File operations

interp {ts} env (OPEN p (FS (F path) _ _ _ _ _) acc) 
   = do { fh <- fopen path (pMode p);
	  putStrLn "Opening";
	  putStrLn (dumpVect ts);
	  return (MkPair (addEnd env (OpenFile acc fh)) bound); };
interp env (CLOSE i p)
   = do { fclose (getFile p env);
	  return (MkPair (updateEnv env i ClosedFile) II); }; 
interp env (READ i p)
   = do { str <- fread (getFile p env);
	  return (MkPair env str); };
interp {ts} env (WRITE i str p)
   = do { putStrLn "Attempting write";
	  putStrLn (dumpVect ts);
	  fwrite (getFile p env) str;
	  putStrLn "Wrote";
	  return (MkPair env II); };

}

-- test programs

do using (BIND, RETURN) {

-- a program which finishes with two closed file handles.
testProg2 : Lang edwin noFiles (nClosed (S (S O))) TyUnit;
testProg2 = do { fh1 <- OPEN Reading infile ?;
	         fh2 <- OPEN Writing outfile ?;
		 str <- READ (wknH fh1) ?;
		 WRITE (wknH fh2) str ?;
		 CLOSE {p=Reading} (wknH fh1) ?;
		 CLOSE {p=Writing} (wknH fh2) ?;
		 };
}

-- TODO: autogenerate this. And need to deal with non-linear patterns!
ElemIs_build : (i:Fin n) -> (a:A) -> (xs:Vect A n) -> 
	       (ElemIs i a xs);
ElemIs_build fO x (VCons x xs) = first;
ElemIs_build (fS i) x (VCons y ys) = later (ElemIs_build i x ys);
ElemIs_build _ _ _ = __Prove_Anything;

-- testProg2 proofs
testProg2_1 proof {
  %refine GroupAccess;%refine lfirst;%refine lfirst;%qed;
};
testProg2_2 proof {
  %intro;%refine UserAccess;%refine llater;%refine lfirst;%qed;
};
testProg2_3 proof {
  %intro;%refine first;%qed;
};
testProg2_4 proof {
  %intro;%refine later;%refine first;%qed;
};
testProg2_5 proof {
  %intro;%refine first;%qed;
};
testProg2_6 proof {
  %intro;%refine later;%refine first;%qed;
};

-- test it

main : IO ();
main = do { ans <- interp Empty testProg2;
	    putStrLn "Done"; };


{-
testProg1 : Lang edwin noFiles (nClosed (S O)) (TyLift String);
testProg1 = BIND (OPEN Reading infile ?tp1)
     (\fh.  BIND (READ (geth fh) ?oreading)
     (\str. BIND (CLOSE {p=Reading} (geth fh) ?fhopen)
     (\u.   RETURN str)));
-}
{-
-- a program which tries to read after opening
testProg3 : Lang edwin noFiles (nClosed (S (S O))) TyUnit;
testProg3 = BIND (OPEN Reading infile ?perm1_3)
     (\fh1. BIND (OPEN Writing outfile ?perm2_3)
     (\fh2. BIND (READ (wknH fh1) ?op1_3)
     (\str. BIND (WRITE (wknH fh2) str ?op2_3)
     (\u.   BIND (CLOSE {p=Reading} (wknH fh1) ?fhc1_3)
     (\u.   BIND (READ (wknH fh1) ?rp_fail) -- rp_fail is unprovable.
     (\str. CLOSE {p=Writing} (wknH fh2) ?fhc2_3))))));

-}