Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse code

Added linlang

  • Loading branch information...
commit 78ee1f1f7683e64c352380ac9ea322e4e84ff227 1 parent 5f43a17
Edwin Brady authored

Showing 1 changed file with 125 additions and 0 deletions. Show diff stats Hide diff stats

  1. +125 0 linlang.idr
125 linlang.idr
... ... @@ -0,0 +1,125 @@
  1 +{-- Whether a variable must be used or not.
  2 + Only primitives are allowed to say a variable is unused in its scope
  3 + (e.g. reading from a file handle. --}
  4 +
  5 +data IsUsed = Used | Unused;
  6 +
  7 +infixr 5 :->;
  8 +
  9 +data LTy = TyVal Set
  10 + | TyRes Set
  11 + | TyReadRes Set
  12 + | TyIO LTy
  13 + | (:->) LTy LTy;
  14 +
  15 +data Resource a = MkRes a;
  16 +
  17 +using (gam : Vect LTy n) {
  18 +
  19 + data Res : Vect LTy n -> LTy -> Set;
  20 +
  21 + interpTy : LTy -> Set;
  22 + interpTy (TyVal T) = T;
  23 + interpTy (TyRes T) = T;
  24 + interpTy (TyReadRes T) = T;
  25 + interpTy (TyIO T) = IO (interpTy T);
  26 + interpTy (A :-> T) = interpTy A -> interpTy T;
  27 +
  28 + interpIO : LTy -> Set;
  29 + interpIO (TyVal T) = IO T;
  30 + interpIO (TyRes T) = IO T;
  31 + interpIO (TyReadRes T) = IO T;
  32 + interpIO (A :-> T) = interpTy A -> interpIO T;
  33 +
  34 + data AEnv : Vect LTy n -> List LTy -> Set where
  35 + ANil : AEnv gam Nil
  36 + | ACons : {as:List LTy} -> {A:LTy} ->
  37 + Res gam A -> AEnv gam as -> AEnv gam (Cons A as);
  38 +
  39 + mkFun : List LTy -> LTy -> Set;
  40 + mkFun Nil T = interpTy T;
  41 + mkFun (Cons a as) T = interpTy a -> mkFun as T;
  42 +
  43 + mkTyFun : List LTy -> LTy -> LTy;
  44 + mkTyFun Nil T = T;
  45 + mkTyFun (Cons a as) T = a :-> mkTyFun as T;
  46 +
  47 + data [noElim] Res : Vect LTy n -> LTy -> Set where
  48 + V : (i:Fin n) -> Res gam (vlookup i gam)
  49 + | I : a -> Res gam (TyVal a)
  50 + | Lam : Res (A :: gam) T -> Res gam (A :-> T)
  51 + | Bind : Res gam (TyIO A) -> Res gam (A :-> (TyIO T)) -> Res gam (TyIO T)
  52 + | App : Res gam (A :-> T) -> Res gam A -> Res gam T
  53 + | Read : Res gam (TyRes A) -> Res gam (TyReadRes A)
  54 + | Prim : (argTys : List LTy) ->
  55 + (interpTy (mkTyFun argTys T)) ->
  56 + Res gam (mkTyFun argTys T);
  57 +
  58 +
  59 + data Env : Vect LTy n -> Set where
  60 + Empty : Env VNil
  61 + | Extend : interpTy a -> Env gam -> Env (a :: gam);
  62 +
  63 + envLookup : (i:Fin n) -> Env gam -> interpTy (vlookup i gam);
  64 + envLookup fO (Extend x xs) = x;
  65 + envLookup (fS k) (Extend x xs) = envLookup k xs;
  66 +
  67 + interp : Env gam -> Res gam T -> interpTy T;
  68 + interp env (V i) = envLookup i env;
  69 + interp env (I a) = a;
  70 + interp env (Lam e) = \x => interp (Extend x env) e;
  71 + interp env (Lam e) = \x => interp (Extend x env) e;
  72 + interp env (Bind val e) = do {
  73 + val' <- interp env val;
  74 + interp env e val';
  75 + };
  76 + interp env (App f a) = interp env f (interp env a);
  77 + interp env (Read a) = let a' = interp env a in a'; -- ????
  78 + interp env (Prim args fn) = fn;
  79 +
  80 + run : Res VNil (TyIO T) -> IO (interpTy T);
  81 + run prog = interp Empty prog;
  82 +
  83 +}
  84 +
  85 +syntax RIO x = #({gam:Vect LTy n} -> Res gam (TyIO (TyVal x)));
  86 +syntax RIOres x = #({gam:Vect LTy n} -> Res gam (TyIO (TyRes x)));
  87 +syntax RVal x = #({gam:Vect LTy n} -> Res gam x);
  88 +syntax RArg x = Res gam x;
  89 +
  90 +lopen' : RVal (TyVal String :-> TyVal String :-> TyIO (TyRes File));
  91 +lopen' = Prim [TyVal String, TyVal String] fopen;
  92 +
  93 +lopen : RArg (TyVal String) -> RArg (TyVal String) -> RIOres File;
  94 +lopen fn mode = App (App lopen' fn) mode;
  95 +
  96 +lread' : RVal (TyReadRes File :-> TyIO (TyVal String));
  97 +lread' = Prim [TyReadRes File] fread;
  98 +
  99 +lread : RArg (TyRes File) -> RIO String;
  100 +lread h = App lread' (Read h);
  101 +
  102 +lclose' : RVal (TyRes File :-> TyIO (TyVal ()));
  103 +lclose' = Prim [TyRes File] fclose;
  104 +
  105 +lclose : RArg (TyRes File) -> RIO ();
  106 +lclose h = App lclose' h;
  107 +
  108 +print : RArg (TyVal String) -> RIO ();
  109 +print str = App (Prim [TyVal String] putStrLn) str;
  110 +
  111 +dsl (V, Lam) {
  112 + do using (Bind, I) {
  113 +
  114 + prog : RIO ();
  115 + prog = do { h <- lopen (I "Test") (I "r");
  116 + str <- lread h;
  117 + print str;
  118 + lclose h;
  119 + };
  120 +
  121 + }
  122 +}
  123 +
  124 +main = run prog;
  125 +

0 comments on commit 78ee1f1

Please sign in to comment.
Something went wrong with that request. Please try again.