rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

remove Eval.idr which is no good

Browse source
This commit is contained in:
rhiannon morris 2021-11-29 14:50:53 +01:00
parent fce293caa7
commit d5530f9884
1 changed files with 0 additions and 130 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

130
src/Quox/Eval.idr
View file

@ -1,130 +0,0 @@
module Quox.Eval
-- todo list:
-- - understand nbe and use it
-- - take a proof of well-typedness as an argument,
-- to reduce the number of eithers
-- - remove the either if possible (should be???)
import Quox.Syntax
import Quox.Context
import Data.DPair
import Data.SortedMap
%default total
public export
record Global where
constructor G
val : forall d, n. NotCloElim d n
public export Globals : Type
Globals = SortedMap Name Global
export (!!) : Globals -> Name -> Maybe (Elim d n)
gs !! x = map (\g => g.val.fst) $ lookup x gs
-- just `map (fst . val)` fails?
mutual
public export isValue : Term d n -> Bool
isValue (TYPE {}) = True
isValue (Pi {arg, res, _}) = isValue arg && isValue res
isValue (Lam {body, _}) = isValue body
isValue (E e) = isNeutral e
isValue (CloT {}) = False
isValue (DCloT {}) = False
public export isNeutral : Elim d n -> Bool
isNeutral (F {}) = False
isNeutral (B {}) = True
isNeutral (fun :@ arg) = isNeutral fun && isValue arg
isNeutral (_ :# _) = False
isNeutral (CloE {}) = False
isNeutral (DCloE {}) = False
public export IsValue : Term d n -> Type
IsValue = So . isValue
public export IsNeutral : Elim d n -> Type
IsNeutral = So . isNeutral
public export Value : Nat -> Nat -> Type
Value d n = Subset (Term d n) IsValue
public export Neutral : Nat -> Nat -> Type
Neutral d n = Subset (Elim d n) IsNeutral
public export valT : (t : Term d n) -> (0 _ : IsValue t) => Value d n
valT t = Element t %search
public export neuE : (e : Elim d n) -> (0 _ : IsNeutral e) => Neutral d n
neuE e = Element e %search
data EvalError =
NotInScope Name
| NonFunction SomeElim
parameters (globals : Globals)
mutual
export covering %inline
evalT : Term d n -> Either EvalError (Value d n)
evalT = uncurry evalT' . pushSubstsT
export covering %inline
evalE : Elim d n -> Either EvalError (Neutral d n)
evalE = uncurry evalE' . pushSubstsE
export covering
evalT' : (t : Term d n) -> (0 prf : IsNotCloT t) ->
Either EvalError (Value d n)
export covering
evalE' : (e : Elim d n) -> (0 prf : IsNotCloE e) ->
Either EvalError (Neutral d n)
public export
data AlphaResult =
Ok
| Clash SomeTerm SomeTerm
| DClash SomeDim SomeDim
| QClash Qty Qty
export
Semigroup AlphaResult where
Ok <+> res = res
res <+> _ = res
export Monoid AlphaResult where neutral = Ok
private %inline clash : Term d1 n1 -> Term d2 n2 -> AlphaResult
clash s t = Clash (some2 s) (some2 t)
||| check two quantities are exactly equal and fail if not
export %inline
alphaQ : (pi, rh : Qty) -> AlphaResult
alphaQ pi rh = if pi == rh then Ok else QClash pi rh
export %inline
alphaD : (al, be : Dim d) -> AlphaResult
alphaD al be = if al == be then Ok else DClash (some al) (some be)
mutual
private
alphaT : (s, t : Term d n) -> AlphaResult
private
alphaE : (e, f : Elim d n) -> AlphaResult
export %inline alphaV : (u, v : Value d n) -> AlphaResult
alphaV u v = alphaT u.fst v.fst
export %inline alphaN : (p, q : Neutral d n) -> AlphaResult
alphaN p q = alphaE p.fst q.fst