<commit_before>include "vect.idr";

data Ty = TyNat | TyFun Ty Ty | TyBool;

interpTy : Ty -> #;
interpTy TyNat = Nat;
interpTy (TyFun s t) = (interpTy s)->(interpTy t);
interpTy TyBool = Bool;

data Term : (Vect Ty n) -> Ty -> # where
   Var : {G:Vect Ty n} -> (i:Fin n) -> (Term G (vlookup i G))
 | Lam : {G:Vect Ty n} ->  
	 (Term (VCons s G) t) -> (Term G (TyFun s t))
 | App : {G:Vect Ty n} -> (Term G (TyFun s t)) -> (Term G s) -> (Term G t)
 | NatVal : {G:Vect Ty n} -> Nat -> (Term G TyNat)
 | BoolVal : {G:Vect Ty n} -> Bool -> (Term G TyBool)
 | Op : {G:Vect Ty n} -> 
	(op : (interpTy a) -> (interpTy b) -> (interpTy c)) ->
	(Term G a) -> (Term G b) -> (Term G c);

data Env : (xs:Vect Ty n) -> # where
   Empty : Env VNil
 | Extend : {xs:Vect Ty n} -> (interpTy t) -> (Env xs) -> 
	    (Env (VCons t xs));

envLookup : {xs:Vect Ty n} -> 
	    (i:Fin n) -> (Env xs) -> (interpTy (vlookup i xs));
envLookup fO (Extend t env) = t;
envLookup (fS i) (Extend t env) = envLookup i env;

interp : {G:Vect Ty n} -> 
         (Env G) -> (Term G t) -> (interpTy t);
interp env (Var i) = envLookup i env;
interp env (Lam {s} sc) = \ v:(interpTy s) . (interp (Extend v env) sc);
interp env (App f a) = (interp env f) (interp env a);
interp env (NatVal n) = n;
interp env (BoolVal b) = b;
interp env (Op f l r) = f (interp env l) (interp env r);

plusOp = Op {a=TyNat} {b=TyNat} {c=TyNat};

fPlus = Lam  
        (Lam  
	 (plusOp
             plus (Var {G=VCons TyNat (VCons TyNat VNil)} fO) 
		  (Var {G=VCons TyNat (VCons TyNat VNil)} (fS fO))));

test = interp Empty fPlus;<commit_msg>Take advantage of better ivor inference<commit_after>include "vect.idr";

data Ty = TyNat | TyFun Ty Ty | TyBool;

interpTy : Ty -> #;
interpTy TyNat = Nat;
interpTy (TyFun s t) = (interpTy s)->(interpTy t);
interpTy TyBool = Bool;

data Term : (Vect Ty n) -> Ty -> # where
   Var : {G:Vect Ty n} -> (i:Fin n) -> (Term G (vlookup i G))
 | Lam : {G:Vect Ty n} ->  
	 (Term (VCons s G) t) -> (Term G (TyFun s t))
 | App : {G:Vect Ty n} -> (Term G (TyFun s t)) -> (Term G s) -> (Term G t)
 | NatVal : {G:Vect Ty n} -> Nat -> (Term G TyNat)
 | BoolVal : {G:Vect Ty n} -> Bool -> (Term G TyBool)
 | Op : {G:Vect Ty n} -> 
	(op : (interpTy a) -> (interpTy b) -> (interpTy c)) ->
	(Term G a) -> (Term G b) -> (Term G c);

data Env : (xs:Vect Ty n) -> # where
   Empty : Env VNil
 | Extend : {xs:Vect Ty n} -> (interpTy t) -> (Env xs) -> 
	    (Env (VCons t xs));

envLookup : {xs:Vect Ty n} -> 
	    (i:Fin n) -> (Env xs) -> (interpTy (vlookup i xs));
envLookup fO (Extend t env) = t;
envLookup (fS i) (Extend t env) = envLookup i env;

interp : {G:Vect Ty n} -> 
         (Env G) -> (Term G t) -> (interpTy t);
interp env (Var i) = envLookup i env;
interp env (Lam {s} sc) = \ v:(interpTy s) . (interp (Extend v env) sc);
interp env (App f a) = (interp env f) (interp env a);
interp env (NatVal n) = n;
interp env (BoolVal b) = b;
interp env (Op f l r) = f (interp env l) (interp env r);

plusOp : {G:Vect Ty n} -> 
         (Term G TyNat) -> (Term G TyNat) -> (Term G TyNat);
plusOp = Op {a=TyNat} {b=TyNat} {c=TyNat} plus;

thing : Term VNil (TyFun TyNat TyNat);
thing = Lam (Var fO);

fPlus2 : Term VNil TyNat;
fPlus2 = (plusOp
             (NatVal (S (S O)))
		(NatVal (S (S O))));

fSnd : Term VNil (TyFun TyNat (TyFun TyNat TyNat));
fSnd = Lam (Lam (Var fO));

fPlus : Term VNil (TyFun TyNat (TyFun TyNat TyNat));
fPlus = Lam (Lam (plusOp (Var fO) (Var (fS fO))));

test = interp Empty fPlus;
{'fraction_non_alphanumeric': 0.18545140885566416, 'fraction_numerical': 0.0005750431282346176, 'mean_word_length': 2.7248394004282654, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 68, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5587186', 'n_tokens_mistral': 1560, 'n_tokens_neox': 1481, 'n_words': 548}