← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda/raring-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/Auto/SearchControl.hs

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2010-01-05 23:43:20 UTC
  • mfrom: (1.1.1 upstream)
  • Revision ID: james.westby@ubuntu.com-20100105234320-6ksc0sdsfhtweknu
Tags: 2.2.6-1
http://bugs.debian.org/559197
* New upstream release 2.2.6, for headlines please see:
  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-2-6
* debian/control
  + Bump standards-version to 3.8.3, no changes
  + Fix Vcs-Git to point to correct URL
  + Update build-depends for new upstream release
  + Undo arch/indep split per current pkg-haskell practice
  + Add Homepage field
* debian/copyright: Fix encoding to UTF-8 (thanks Lintian) 
* debian/README.source: Remove, no repacking so not necessary any more 
* debian/50agda.el:
  + Only load file if it exists, prevents a non-intrusive emacs warning
    where 50agda.el is left on system when package is removed. 
    (Closes: #559197). 
  + Do not load file on XEmacs — agda-mode is not compatible with XEmacs.

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/Auto/SearchControl.hs
 
1
{-# OPTIONS -fglasgow-exts -XUndecidableInstances #-}
 
2
 
 
3
module Agda.Auto.SearchControl where
 
4
 
 
5
import Control.Monad
 
6
import Data.IORef
 
7
import Control.Monad.State
 
8
 
 
9
import Agda.Auto.NarrowingSearch
 
10
import Agda.Auto.Syntax
 
11
import Agda.Auto.Print
 
12
 
 
13
 
 
14
instance Refinable (ArgList o) (RefInfo o) where
 
15
 refinements _ _ = return [
 
16
   (0, return ALNil),
 
17
   (0, cons NotHidden),
 
18
   (0, cons Hidden)
 
19
  ]
 
20
  where cons hid = do p1 <- newPlaceholder
 
21
                      p2 <- newPlaceholder
 
22
                      return $ ALCons hid p1 p2
 
23
 printref x = pargs [] (NotM x)
 
24
 
 
25
 
 
26
getinfo [] (Just x) us = (x, us)
 
27
getinfo (x@(RIMainInfo _ _) : xs) Nothing us = getinfo xs (Just x) us
 
28
getinfo (x@(RIUnifInfo _ _ _) : xs) m us = getinfo xs m (x : us)
 
29
getinfo _ _ _ = error "getinfo: case should not occur"
 
30
 
 
31
instance Refinable (Exp o) (RefInfo o) where
 
32
 refinements envinfo infos = do
 
33
  let RIEnv hints = envinfo
 
34
      (RIMainInfo n tt, unis) = getinfo infos Nothing []
 
35
  occs <- mapM (\(RIUnifInfo mm _ opphne) -> occursCheck mm opphne) unis
 
36
  cons <- case tt of
 
37
           HNApp (Const c) _ -> do
 
38
            cd <- readIORef c
 
39
            return $ case cdcont cd of
 
40
             Datatype cons -> cons
 
41
             _ -> []
 
42
           _ -> return []
 
43
  let up = case unis of
 
44
            [] -> False
 
45
            _ -> all not occs
 
46
      lam hid = (0,
 
47
                 do p <- newPlaceholder
 
48
                    return $ Lam hid (Abs NoId p)
 
49
                )
 
50
      apps = map app [0..n - 1]
 
51
      capps = case unis of
 
52
               [] -> map capp (hints ++ cons)
 
53
               _ -> []
 
54
      app v = (if up then 0 else 1,
 
55
               do p <- newPlaceholder
 
56
                  return $ App (Var v) p
 
57
              )
 
58
      capp c = (if up then 0 else 2,
 
59
                do p <- newPlaceholder
 
60
                   return $ App (Const c) p
 
61
               )
 
62
      set l = map (\l -> (0, return $ Sort (SortLevel l))) [0 .. l - 1]
 
63
      fun hid = (2,
 
64
                 do p1 <- newPlaceholder
 
65
                    p2 <- newPlaceholder
 
66
                    return $ Fun hid p1 p2)
 
67
      pi hid = (2,
 
68
                do p1 <- newPlaceholder
 
69
                   p2 <- newPlaceholder
 
70
                   return $ Pi hid True p1 (Abs NoId p2))
 
71
      mimic = case unis of
 
72
               [] -> []
 
73
               (RIUnifInfo _ cl hnopp : _) -> case hnopp of
 
74
                HNApp (Const c) _ -> [capp c]
 
75
                _ -> []
 
76
               _ -> error "refinements: mimic: not matched"
 
77
  case tt of
 
78
   HNFun hid _ _ -> return $ lam hid : apps ++ capps ++ mimic
 
79
   HNPi hid _ _ _ -> return $ lam hid : apps ++ capps ++ mimic
 
80
   HNSort (SortLevel l) -> return $ set l ++ [fun NotHidden, fun Hidden, pi NotHidden, pi Hidden] ++ apps ++ capps ++ mimic
 
81
   _ -> return $ apps ++ capps ++ mimic
 
82
 printref x = printExp [] (NotM x)
 
83
 
 
84
-- ---------------------------------
 
85
 
 
86
occursCheck :: forall a o . Metavar a (RefInfo o) -> HNExp o -> IO Bool
 
87
occursCheck m0 hn = liftM snd $ runStateT (
 
88
  let f :: forall b . Trav b (RefInfo o) => MM b (RefInfo o) -> StateT Bool IO ()
 
89
      f (NotM x) = traverse f x
 
90
      f (Meta m) = do
 
91
         bind <- lift $ readIORef $ mbind m
 
92
         case bind of
 
93
          Just x -> traverse f x
 
94
          Nothing -> when (hequalMetavar m m0) $ put True
 
95
  in  traverse f hn
 
96
 ) False
 
97
 
 
98
 
 
99
-- ---------------------------------
 
100
 
 
101
prioNo, prioTypeUnknown, prioTypecheckArgList, prioInferredTypeUnknown, prioPreCompare, prioCompare, prioCompareArgList, prioCompIota, prioCompChoice :: Int
 
102
prioNo = (-1)
 
103
prioTypeUnknown = 0
 
104
prioTypecheck False = 1
 
105
prioTypecheck True = 0
 
106
prioTypecheckArgList = 3
 
107
prioInferredTypeUnknown = 4
 
108
prioPreCompare = 4
 
109
prioCompChoice = 4
 
110
prioCompare = 2
 
111
prioCompareArgList = 2
 
112
prioCompIota = 4
 
113
 
 
114
-- ---------------------------------
 
115
 
 
116
instance Trav a blk => Trav [a] blk where
 
117
 traverse _ [] = return ()
 
118
 traverse f (x:xs) = traverse f x >> traverse f xs
 
119
 
 
120
instance Trav (MId, CExp o) (RefInfo o) where
 
121
 traverse f (_, ce) = traverse f ce
 
122
 
 
123
instance Trav a (RefInfo o) => Trav (Clos a o) (RefInfo o) where
 
124
 traverse f (Clos cl e) = traverse f cl >> traverse f e
 
125
 
 
126
instance Trav (CAction o) (RefInfo o) where
 
127
 traverse f (Sub ce) = traverse f ce
 
128
 traverse _ Skip = return ()
 
129
 traverse _ (Weak _) = return ()
 
130
 
 
131
instance Trav (Exp o) (RefInfo o) where
 
132
 traverse f e = case e of
 
133
  App _ args -> traverse f args
 
134
  Lam _ (Abs _ b) -> traverse f b
 
135
  Fun _ it ot -> traverse f it >> traverse f ot
 
136
  Pi _ _ it (Abs _ ot) -> traverse f it >> traverse f ot
 
137
  Sort _ -> return ()
 
138
 
 
139
instance Trav (ArgList o) (RefInfo o) where
 
140
 traverse _ ALNil = return ()
 
141
 traverse f (ALCons _ arg args) = traverse f arg >> traverse f args
 
142
 traverse f (ALConPar args) = traverse f args
 
143
 
 
144
instance Trav (HNExp o) (RefInfo o) where
 
145
 traverse f e = case e of
 
146
  HNApp _ args -> traverse f args
 
147
  HNLam (Abs _ b) -> traverse f b
 
148
  HNFun _ it ot -> traverse f it >> traverse f ot
 
149
  HNPi _ _ it (Abs _ ot) -> traverse f it >> traverse f ot
 
150
  HNSort _ -> return ()
 
151
 
 
152
instance Trav (CArgList o) (RefInfo o) where
 
153
 traverse _ CALNil = return ()
 
154
 traverse f (CALConcat arg args) = traverse f arg >> traverse f args
 
155
 
 
156