ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-21 22:17:19 +03:00
Code Issues Projects Releases Wiki Activity

Fiddle with elaborator; update interp sample and test

Browse Source
This commit is contained in:
Edwin Brady 2011-12-02 16:50:05 +00:00
parent 4ceba27c96
commit 73846830fb
7 changed files with 115 additions and 61 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

45
samples/interp.idr
View File

@ -13,18 +13,20 @@ using (G : Vect Ty n) {
Nil : Env Nil
| (::) : interpTy a -> Env G -> Env (a :: G);
lookup : (i : Fin n) -> Env G -> interpTy (lookup i G);
lookup fO (x :: xs) = x;
lookup (fS i) (x :: xs) = lookup i xs;
data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
stop : HasType fO (t :: G) t
| pop : HasType k G t -> HasType (fS k) (u :: G) t;
lookup : HasType i G t -> Env G -> interpTy t;
lookup stop (x :: xs) = x;
lookup (pop k) (x :: xs) = lookup k xs;
data Expr : Vect Ty n -> Ty -> Set where
Var : (i : Fin n) -> Expr G (lookup i G)
Var : HasType i G t -> Expr G t
| Val : (x : Int) -> Expr G TyInt
| Lam : Expr (a :: G) t -> Expr G (TyFun a t)
| App : Expr G (TyFun a t) -> Expr G a -> Expr G t
| Op : (Int -> Int -> interpTy c) ->
Expr G TyInt -> Expr G TyInt -> Expr G c
| Op' : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
| Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
Expr G c
| If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
| Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;
@ -35,45 +37,50 @@ using (G : Vect Ty n) {
interp env (Lam sc) = \x => interp (x :: env) sc;
interp env (App f s) = (interp env f) (interp env s);
interp env (Op op x y) = op (interp env x) (interp env y);
interp env (Op' op x y) = op (interp env x) (interp env y);
interp env (If x t e) = if (interp env x) then (interp env t) else (interp env e);
interp env (Bind v f) = interp env (f (interp env v));
eId : Expr G (TyFun TyInt TyInt);
eId = Lam (Var fO);
eId = Lam (Var stop);
eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt));
eTEST = Lam (Lam (Var (pop stop)));
eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt));
eAdd = Lam (Lam (Op (+) (Var fO) (Var (fS fO))));
eAdd = Lam (Lam (Op prim__addInt (Var stop) (Var (pop stop))));
-- eDouble : Expr G (TyFun TyInt TyInt);
-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO));
eDouble : Expr G (TyFun TyInt TyInt);
eDouble = Lam (App (App eAdd (Var fO)) (Var fO));
eDouble = Lam (App (App eAdd (Var stop)) (Var stop));
app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t;
app = \f, a => App f a;
eFac : Expr G (TyFun TyInt TyInt);
eFac = Lam (If (Op (==) (Var fO) (Val 0))
(Val 1) (Op (*) (app eFac (Op (-) (Var fO) (Val 1))) (Var fO)));
eFac = Lam (If (Op (==) (Var stop) (Val 0))
(Val 1) (Op (*) (app eFac (Op (-) (Var stop) (Val 1))) (Var stop)));
-- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2
eProg : Expr G (TyFun TyInt (TyFun TyInt TyInt));
eProg = Lam (Lam
(Bind (App eDouble (Var (fS fO)))
(\x => Bind (App eDouble (Var fO))
(Bind (App eDouble (Var (pop stop)))
(\x => Bind (App eDouble (Var stop))
(\y => Bind (App eDouble (Val x))
(\z => App (App eAdd (Val y)) (Val z))))));
}
test : Int;
test = interp Nil eProg 2 2;
test = interp [] eProg 2 2;
testFac : Int;
testFac = interp Nil eFac 4;
testFac = interp [] eFac 4;
main : IO ();
main = print testFac;
main = do { print testFac;
print test; };

30
src/Core/Elaborate.hs
View File

@ -223,6 +223,9 @@ instanceArg n = processTactic' (Instance n)
proofstate :: Elab ()
proofstate = processTactic' ProofState
reorder_claims :: Name -> Elab ()
reorder_claims n = processTactic' (Reorder n)
qed :: Elab Term
qed = do processTactic' QED
ES p _ _ <- get
@ -231,35 +234,41 @@ qed = do processTactic' QED
undo :: Elab ()
undo = processTactic' Undo
prepare_apply :: Raw -> [Bool] -> Elab [Name]
prepare_apply :: Raw -> [(Bool, Int)] -> Elab [Name]
prepare_apply fn imps =
do ty <- get_type fn
ctxt <- get_context
env <- get_env
-- let claims = getArgs ty imps
claims <- doClaims (normalise ctxt env ty) imps []
claims <- mkClaims (normalise ctxt env ty) imps []
ES p s prev <- get
-- reverse the claims we made so that args go left to right
let n = length (filter not imps)
let n = length (filter not (map fst imps))
let (h : hs) = holes p
put (ES (p { holes = h : (reverse (take n hs) ++ drop n hs) }) s prev)
-- case claims of
-- [] -> return ()
-- (h : _) -> reorder_claims h
return claims
where
doClaims (Bind n' (Pi t) sc) (i : is) claims =
mkClaims (Bind n' (Pi t) sc) (i : is) claims =
do n <- unique_hole (mkMN n')
when (null claims) (start_unify n)
-- when (null claims) (start_unify n)
let sc' = instantiate (P Bound n t) sc
claim n (forget t)
when i (movelast n)
doClaims sc' is (n : claims)
doClaims t [] claims = return (reverse claims)
doClaims _ _ _ = fail $ "Wrong number of arguments for " ++ show fn
when (fst i) (movelast n)
mkClaims sc' is (n : claims)
mkClaims t [] claims = return (reverse claims)
mkClaims _ _ _ = fail $ "Wrong number of arguments for " ++ show fn
doClaim ((i, _), n, t) = do claim n t
when i (movelast n)
mkMN n@(MN _ _) = n
mkMN n@(UN x) = MN 0 x
mkMN (NS n xs) = NS (mkMN n) xs
apply :: Raw -> [Bool] -> Elab [Name]
apply :: Raw -> [(Bool, Int)] -> Elab [Name]
apply fn imps =
do args <- prepare_apply fn imps
fill (raw_apply fn (map Var args))
@ -267,6 +276,7 @@ apply fn imps =
-- (remove from unified list before calling end_unify)
-- HMMM: Actually, if we get it wrong, the typechecker will complain!
-- so do nothing
ptm <- get_term
let dontunify = [] -- map fst (filter (not.snd) (zip args imps))
ES p s prev <- get
let (n, hs) = unified p

36
src/Core/ProofState.hs
View File

@ -37,6 +37,7 @@ data Goal = GD { premises :: Env,
data Tactic = Attack
| Claim Name Raw
| Reorder Name
| Exact Raw
| Fill Raw
| PrepFill Name [Name]
@ -181,6 +182,29 @@ claim n ty ctxt env t =
ps { holes = g : n : gs } )
return $ Bind n (Hole tyv) t -- (weakenTm 1 t)
reorder_claims :: RunTactic
reorder_claims ctxt env t
= -- trace (showSep "\n" (map show (scvs t))) $
let (bs, sc) = scvs t []
newbs = reverse (sortB (reverse bs)) in
traceWhen (bs /= newbs) (show bs ++ "\n ==> \n" ++ show newbs) $
return (bindAll newbs sc)
where scvs (Bind n b@(Hole _) sc) acc = scvs sc ((n, b):acc)
scvs sc acc = (reverse acc, sc)
sortB :: [(Name, Binder (TT Name))] -> [(Name, Binder (TT Name))]
sortB [] = []
sortB (x:xs) | all (noOcc x) xs = x : sortB xs
| otherwise = sortB (insertB x xs)
insertB x [] = [x]
insertB x (y:ys) | all (noOcc x) (y:ys) = x : y : ys
| otherwise = y : insertB x ys
noOcc (n, _) (_, Let t v) = noOccurrence n t && noOccurrence n v
noOcc (n, _) (_, Guess t v) = noOccurrence n t && noOccurrence n v
noOcc (n, _) (_, b) = noOccurrence n (binderTy b)
focus :: Name -> RunTactic
focus n ctxt env t = do action (\ps -> let hs = holes ps in
if n `elem` hs
@ -231,6 +255,7 @@ exact _ _ _ _ = fail "Can't fill here."
fill :: Raw -> RunTactic
fill guess ctxt env (Bind x (Hole ty) sc) =
do (val, valty) <- lift $ check ctxt env guess
s <- get
ns <- lift $ unify ctxt env valty ty
ps <- get
let (uh, uns) = unified ps
@ -259,7 +284,9 @@ complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
solve :: RunTactic
solve ctxt env (Bind x (Guess ty val) sc)
| pureTerm val = do ps <- get
let (uh, uns) = unified ps
action (\ps -> ps { holes = holes ps \\ [x],
-- unified = (uh, uns ++ [(x, val)]),
instances = instances ps \\ [x] })
return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)
| otherwise = fail $ "I see a hole in your solution. " ++ showEnv env val
@ -383,7 +410,7 @@ solve_unified ctxt env tm =
do ps <- get
let (_, ns) = unified ps
action (\ps -> ps { holes = holes ps \\ map fst ns })
-- action (\ps -> ps { pterm = updateSolved ns (pterm ps) })
action (\ps -> ps { pterm = updateSolved ns (pterm ps) })
return (updateSolved ns tm)
updateSolved xs (Bind n (Hole ty) t)
@ -411,12 +438,13 @@ processTactic EndUnify ps = let (h, ns) = unified ps
return (ps { pterm = tm',
unified = (h, []),
holes = holes ps \\ map fst ns }, "")
where
processTactic (Reorder n) ps
= do ps' <- execStateT (tactic (Just n) reorder_claims) ps
return (ps' { previous = Just ps, plog = "" }, plog ps')
processTactic t ps
= case holes ps of
[] -> fail "Nothing to fill in."
(h:_) -> do let n = nextname ps
ps' <- execStateT (process t h) ps
(h:_) -> do ps' <- execStateT (process t h) ps
return (ps' { previous = Just ps, plog = "" }, plog ps')
process :: Tactic -> Name -> StateT TState TC ()

2
src/Core/ShellParser.hs
View File

@ -51,7 +51,7 @@ pTactic = do reserved "attack"; return attack
<|> do reserved "exact"; tm <- pTerm; return (exact tm)
<|> do reserved "fill"; tm <- pTerm; return (fill tm)
<|> do reserved "apply"; tm <- pTerm; args <- many pArgType;
return (discard (apply tm args))
return (discard (apply tm (map (\x -> (x,0)) args)))
<|> do reserved "solve"; return solve
<|> do reserved "compute"; return compute
<|> do reserved "intro"; n <- iName []; return (intro (Just n))

14
src/Idris/ElabTerm.hs
View File

@ -42,8 +42,8 @@ elab ist info pattern tm
mkPat
where
isph arg = case getTm arg of
Placeholder -> True
_ -> False
Placeholder -> (True, priority arg)
_ -> (False, priority arg)
toElab arg = case getTm arg of
Placeholder -> Nothing
@ -283,10 +283,10 @@ resolveTC depth ist
args <- apply (Var n) imps
mapM_ (\ (_,n) -> do focus n
resolveTC (depth - 1) ist)
(filter (\ (x, y) -> not x) (zip imps args))
(filter (\ (x, y) -> not x) (zip (map fst imps) args))
solve
where isImp (PImp _ _ _ _) = True
isImp _ = False
where isImp (PImp p _ _ _) = (True, p)
isImp arg = (False, priority arg)
collectDeferred :: Term -> State [(Name, Type)] Term
collectDeferred (Bind n (GHole t) app) =
@ -322,7 +322,7 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where
return (fn, a)
-- FIXME: resolve ambiguities
[(n, args)] -> return $ (n, map isImp args)
ns <- apply (Var fn') imps
ns <- apply (Var fn') (map (\x -> (x,0)) imps)
when autoSolve solveAll
where isImp (PImp _ _ _ _) = True
isImp _ = False
@ -331,7 +331,7 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where
Just t -> return $ map (const False)
(getArgTys (binderTy t))
_ -> return []
runT (Refine fn imps) = do ns <- apply (Var fn) imps
runT (Refine fn imps) = do ns <- apply (Var fn) (map (\x -> (x,0)) imps)
when autoSolve solveAll
runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that
= do attack; -- (h:_) <- get_holes

1
test/test001/expected
View File

@ -1 +1,2 @@
24
12

48
test/test001/test001.idr
View File

@ -13,19 +13,21 @@ using (G : Vect Ty n) {
Nil : Env Nil
| (::) : interpTy a -> Env G -> Env (a :: G);
lookup : (i : Fin n) -> Env G -> interpTy (lookup i G);
lookup fO (x :: xs) = x;
lookup (fS i) (x :: xs) = lookup i xs;
data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
stop : HasType fO (t :: G) t
| pop : HasType k G t -> HasType (fS k) (u :: G) t;
lookup : HasType i G t -> Env G -> interpTy t;
lookup stop (x :: xs) = x;
lookup (pop k) (x :: xs) = lookup k xs;
data Expr : Vect Ty n -> Ty -> Set where
Var : (i : Fin n) -> Expr G (lookup i G)
Var : HasType i G t -> Expr G t
| Val : (x : Int) -> Expr G TyInt
| Lam : Expr (a :: G) t -> Expr G (TyFun a t)
| App : Expr G (TyFun a t) -> Expr G a -> Expr G t
| Op : (Int -> Int -> interpTy c) ->
Expr G TyInt -> Expr G TyInt -> Expr G c
| Op' : (interpTy a -> interpTy b -> interpTy c) ->
Expr G a -> Expr G b -> Expr G c
| Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->
Expr G c
| If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
| Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;
@ -35,45 +37,51 @@ using (G : Vect Ty n) {
interp env (Lam sc) = \x => interp (x :: env) sc;
interp env (App f s) = (interp env f) (interp env s);
interp env (Op op x y) = op (interp env x) (interp env y);
interp env (Op' op x y) = op (interp env x) (interp env y);
interp env (If x t e) = if (interp env x) then (interp env t) else (interp env e);
interp env (Bind v f) = interp env (f (interp env v));
eId : Expr G (TyFun TyInt TyInt);
eId = Lam (Var fO);
eId = Lam (Var stop);
eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt));
eTEST = Lam (Lam (Var (pop stop)));
eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt));
eAdd = Lam (Lam (Op (+) (Var fO) (Var (fS fO))));
eAdd = Lam (Lam (Op prim__addInt (Var stop) (Var (pop stop))));
-- eDouble : Expr G (TyFun TyInt TyInt);
-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO));
eDouble : Expr G (TyFun TyInt TyInt);
eDouble = Lam (App (App eAdd (Var fO)) (Var fO));
eDouble = Lam (App (App eAdd (Var stop)) (Var stop));
app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t;
app = \f, a => App f a;
eFac : Expr G (TyFun TyInt TyInt);
eFac = Lam (If (Op (==) (Var fO) (Val 0))
(Val 1) (Op (*) (app eFac (Op (-) (Var fO) (Val 1))) (Var fO)));
eFac = Lam (If (Op (==) (Var stop) (Val 0))
(Val 1) (Op (*) (app eFac (Op (-) (Var stop) (Val 1))) (Var stop)));
-- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2
eProg : Expr G (TyFun TyInt (TyFun TyInt TyInt));
eProg = Lam (Lam
(Bind (App eDouble (Var (fS fO)))
(\x => Bind (App eDouble (Var fO))
(Bind (App eDouble (Var (pop stop)))
(\x => Bind (App eDouble (Var stop))
(\y => Bind (App eDouble (Val x))
(\z => App (App eAdd (Val y)) (Val z))))));
}
test : Int;
test = interp Nil eProg 2 2;
test = interp [] eProg 2 2;
testFac : Int;
testFac = interp Nil eFac 4;
testFac = interp [] eFac 4;
main : IO ();
main = print testFac;
main = do { print testFac;
print test; };