Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Changed way of building pattern match terms

  • Loading branch information...
commit 3501adbbcc4bcf569e5042eec71cbdde6742668d 1 parent c966457
Edwin Brady authored
View
1  miniidris.cabal
@@ -26,3 +26,4 @@ Executable miniidris
Extensions: MultiParamTypeClasses, FunctionalDependencies,
FlexibleInstances
ghc-prof-options: -auto-all
+ ghc-options: -rtsopts
View
31 src/Elaborate.hs
@@ -51,6 +51,10 @@ get_env :: Elab Env
get_env = do (p, _) <- get
lift $ envAtFocus p
+get_holes :: Elab [Name]
+get_holes = do (p, _) <- get
+ return (holes p)
+
-- get the current goal type
goal :: Elab Type
goal = do (p, _) <- get
@@ -65,8 +69,9 @@ get_type tm = do ctxt <- get_context
-- given a desired hole name, return a unique hole name
unique_hole :: Name -> Elab Name
-unique_hole n = do env <- get_env
- return (uniq n (map fst env))
+unique_hole n = do (p, _) <- get
+ env <- get_env
+ return (uniq n (holes p ++ map fst env))
where
uniq n hs | n `elem` hs = uniq (next n) hs
| otherwise = n
@@ -125,8 +130,8 @@ intro n = processTactic' (Intro n)
forall :: Name -> Raw -> Elab ()
forall n t = processTactic' (Forall n t)
-patvar :: Name -> Raw -> Elab ()
-patvar n t = processTactic' (PatVar n t)
+patvar :: Name -> Elab ()
+patvar n = processTactic' (PatVar n)
focus :: Name -> Elab ()
focus n = processTactic' (Focus n)
@@ -148,7 +153,13 @@ prepare_apply :: Raw -> [Bool] -> Elab [Name]
prepare_apply fn imps =
do ty <- get_type fn
-- let claims = getArgs ty imps
- doClaims ty imps []
+ claims <- doClaims ty imps []
+ (p, s) <- get
+ -- reverse the claims we made so that args go left to right
+ let n = length (filter not imps)
+ let (h : hs) = holes p
+ put (p { holes = h : (reverse (take n hs) ++ drop n hs) }, s)
+ return claims
where
doClaims (Bind n' (Pi t) sc) (i : is) claims =
do n <- unique_hole n'
@@ -164,7 +175,7 @@ apply :: Raw -> [Bool] -> Elab ()
apply fn imps =
do args <- prepare_apply fn imps
fill (raw_apply fn (map Var args))
- when (not (null args)) end_unify
+ end_unify
-- Abstract over an argument of unknown type, giving a name for the hole
-- which we'll fill with the argument type too.
@@ -173,10 +184,10 @@ arg n tyhole = do ty <- unique_hole tyhole
claim ty (RSet 0)
forall n (Var ty)
-patarg :: Name -> Name -> Elab ()
-patarg n tyhole = do ty <- unique_hole tyhole
- claim ty (RSet 0)
- patvar n (Var ty)
+-- patarg :: Name -> Name -> Elab ()
+-- patarg n tyhole = do ty <- unique_hole tyhole
+-- claim ty (RSet 0)
+-- patvar n (Var ty)
-- Some combinators on elaborations
View
55 src/ProofState.hs
@@ -47,21 +47,13 @@ data Tactic = Attack
| CheckIn Raw
| Intro Name
| Forall Name Raw
- | PatVar Name Raw
+ | PatVar Name
| Focus Name
| MoveLast Name
| ProofState
| Undo
| QED
-data TacticAction = AddGoal Name -- add a new goal, solve immediately
- | NextGoal Name -- add a new goal, solve it after current one
- | FocusGoal Name -- focus on this goal next
- | MoveGoal Name -- move this goal to the end of the hole queue
- | Solved Name
- | AlsoSolved [(Name, Term)] -- variables solved by unification
- | Log String
-
-- Some utilites on proof and tactic states
instance Show ProofState where
@@ -69,21 +61,22 @@ instance Show ProofState where
show (PS nm (h:hs) _ tm _ _ i _ ctxt _ _)
= let OK g = goal (Just h) tm
wkenv = premises g in
+ "Other goals: " ++ show hs ++ "\n" ++
showPs wkenv (reverse wkenv) ++ "\n" ++
"-------------------------------- (" ++ show nm ++
- ") -------\n" ++
+ ") -------\n " ++
show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
where showPs env [] = ""
showPs env ((n, Let t v):bs)
= " " ++ show n ++ " : " ++
- showEnv env (normalise ctxt env t) ++ " = " ++
- showEnv env (normalise ctxt env v) ++
+ showEnv env ({- normalise ctxt env -} t) ++ " = " ++
+ showEnv env ({- normalise ctxt env -} v) ++
"\n" ++ showPs env bs
showPs env ((n, b):bs)
= " " ++ show n ++ " : " ++
- showEnv env (normalise ctxt env (binderTy b)) ++
+ showEnv env ({- normalise ctxt env -} (binderTy b)) ++
"\n" ++ showPs env bs
- showG ps (Guess t v) = showEnv ps (normalise ctxt ps t) ++
+ showG ps (Guess t v) = showEnv ps ({- normalise ctxt ps -} t) ++
" =?= " ++ showEnv ps v
showG ps b = showEnv ps (binderTy b)
@@ -211,14 +204,14 @@ fill guess ctxt env (Bind x (Hole ty) sc) =
ps <- get
let (uh, uns) = unified ps
put (ps { unified = (uh, uns ++ ns) })
- addLog (show (uh, uns ++ ns))
+-- addLog (show (uh, uns ++ ns))
return $ Bind x (Guess ty val) sc
fill _ _ _ _ = fail "Can't fill here."
solve :: RunTactic
solve ctxt env (Bind x (Guess ty val) sc)
| pureTerm val = do action (\ps -> ps { holes = holes ps \\ [x] })
- return $ Bind x (Let ty val) sc -- instantiate val (pToV x sc)
+ return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)
| otherwise = fail "I see a hole in your solution."
solve _ _ _ = fail "Not a guess."
@@ -238,11 +231,10 @@ forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
lift $ isSet ctxt env t
return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))
-patvar :: Name -> Raw -> RunTactic
-patvar n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
- do (tyv, tyt) <- lift $ check ctxt env ty
- lift $ isSet ctxt env tyt
- return $ Bind n (PVar tyv) (Bind x (Hole t) (P Bound x t))
+patvar :: Name -> RunTactic
+patvar n ctxt env (Bind x (Hole t) sc) =
+ do action (\ps -> ps { holes = holes ps \\ [x] })
+ return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))
compute :: RunTactic
compute ctxt env (Bind x (Hole ty) sc) =
@@ -276,9 +268,10 @@ 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) })
return (updateSolved ns tm)
where
- updateSolved xs (Bind n b@(Hole _) t)
+ updateSolved xs (Bind n (Hole ty) t)
| Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))
updateSolved xs (Bind n b t)
| otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)
@@ -295,7 +288,7 @@ solve_unified ctxt env tm =
processTactic :: Tactic -> ProofState -> TC (ProofState, String)
processTactic QED ps = case holes ps of
- [] -> do let tm = pterm ps
+ [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)
(tm', ty') <- recheck (context ps) [] tm
return (ps { done = True, pterm = tm' },
"Proof complete: " ++ showEnv [] tm')
@@ -304,6 +297,20 @@ processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
processTactic Undo ps = case previous ps of
Nothing -> Error "Nothing to undo."
Just pold -> return (pold, "")
+processTactic EndUnify ps = let (h, ns) = unified ps
+ tm' = updateSolved ns (pterm ps) in
+ return (ps { pterm = tm',
+ unified = (h, []),
+ holes = holes ps \\ map fst ns }, "")
+ where
+ updateSolved xs (Bind n (Hole ty) t)
+ | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))
+ updateSolved xs (Bind n b t)
+ | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)
+ updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)
+ updateSolved xs (P _ n _)
+ | Just v <- lookup n xs = v
+ updateSolved xs t = t
processTactic t ps
= case holes ps of
[] -> Error "Nothing to fill in."
@@ -327,7 +334,7 @@ process t h = tactic (Just h) (mktac t)
mktac Compute = compute
mktac (Intro n) = intro n
mktac (Forall n t) = forall n t
- mktac (PatVar n t) = patvar n t
+ mktac (PatVar n) = patvar n
mktac (CheckIn r) = check_in r
mktac (EvalIn r) = eval_in r
mktac (Focus n) = focus n
View
7 src/ShellParser.hs
@@ -57,10 +57,9 @@ pTactic = do reserved "attack"; return attack
<|> do reserved "intro"; n <- iName; return (intro n)
<|> do reserved "forall"; n <- iName; lchar ':'; ty <- pTerm
return (forall n ty)
- <|> do reserved "arg"; n <- iName; t <- iName; return (arg n t)
- <|> do reserved "patvar"; n <- iName; lchar ':'; ty <- pTerm
- return (patvar n ty)
- <|> do reserved "patarg"; n <- iName; t <- iName; return (patarg n t)
+-- <|> do reserved "arg"; n <- iName; t <- iName; return (arg n t)
+ <|> do reserved "patvar"; n <- iName; return (patvar n)
+-- <|> do reserved "patarg"; n <- iName; t <- iName; return (patarg n t)
<|> do reserved "eval"; t <- pTerm; return (eval_in t)
<|> do reserved "check"; t <- pTerm; return (check_in t)
<|> do reserved "focus"; n <- iName; return (focus n)
View
2  src/Typecheck.hs
@@ -34,7 +34,7 @@ check :: Context -> Env -> Raw -> TC (Term, Type)
check ctxt env (Var n)
| Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)
| Just (P nt n' ty) <- lookupP n ctxt = return (P nt n' ty, ty)
- | otherwise = do fail $ "No such variable " ++ show n
+ | otherwise = do fail $ "No such variable " ++ show n ++ " in " ++ show (map fst env)
check ctxt env (RApp f a)
= do (fv, fty) <- check ctxt env f
(av, aty) <- check ctxt env a
Please sign in to comment.
Something went wrong with that request. Please try again.