summaryrefslogtreecommitdiff
path: root/src/GF/Grammar/AbsCompute.hs
blob: b2139f90a733511a453eaa5ebb6e1909d7dfd87f (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
----------------------------------------------------------------------
-- |
-- Module      : AbsCompute
-- Maintainer  : AR
-- Stability   : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/10/02 20:50:19 $ 
-- > CVS $Author: aarne $
-- > CVS $Revision: 1.8 $
--
-- computation in abstract syntax w.r.t. explicit definitions.
--
-- old GF computation; to be updated
-----------------------------------------------------------------------------

module GF.Grammar.AbsCompute (LookDef,
		   compute, 
		   computeAbsTerm, 
		   computeAbsTermIn, 
		   beta
		  ) where

import GF.Data.Operations

import GF.Grammar.Abstract
import GF.Grammar.PrGrammar
import GF.Grammar.LookAbs
import GF.Grammar.PatternMatch
import GF.Grammar.Compute

import Control.Monad (liftM, liftM2)

compute :: GFCGrammar -> Exp -> Err Exp
compute = computeAbsTerm

computeAbsTerm :: GFCGrammar -> Exp -> Err Exp
computeAbsTerm gr = computeAbsTermIn (lookupAbsDef gr) []

-- | a hack to make compute work on source grammar as well
type LookDef = Ident -> Ident -> Err (Maybe Term)

computeAbsTermIn :: LookDef -> [Ident] -> Exp -> Err Exp
computeAbsTermIn lookd xs e = errIn ("computing" +++ prt e) $ compt xs e where
  compt vv t = case t of
    Prod x a b  -> liftM2 (Prod x) (compt vv a) (compt (x:vv) b)
    Abs x b     -> liftM  (Abs  x)              (compt (x:vv) b)
    _ -> do
      let t' = beta vv t
      (yy,f,aa) <- termForm t'
      let vv' = yy ++ vv
      aa'    <- mapM (compt vv') aa
      case look f of
        Just (Eqs eqs) -> case findMatch eqs aa' of
          Ok (d,g) -> do
            let (xs,ts) = unzip g
            ts' <- alphaFreshAll vv' ts ---
            let g' = zip xs ts'
            d' <- compt vv' $ substTerm vv' g' d
            return $ mkAbs yy $ d'
          _ -> do
            return $ mkAbs yy $ mkApp f aa'
        Just d -> do
          d' <- compt vv' d
          da <- ifNull (return d') (compt vv' . mkApp d') aa' 
          return $ mkAbs yy $ da
        _ -> do
          return $ mkAbs yy $ mkApp f aa'

  look t = case t of
     (Q m f) -> case lookd m f of
       Ok (Just EData) -> Nothing  -- canonical --- should always be QC
       Ok md -> md
       _ -> Nothing
     Eqs _ -> return t ---- for nested fn
     _ -> Nothing

beta :: [Ident] -> Exp -> Exp
beta vv c = case c of
  App (Abs x b) a -> beta vv $ substTerm vv [xvv] (beta (x:vv) b) 
                                                    where xvv = (x,beta vv a) 
  Let (x,(_,a)) b -> beta vv $ substTerm vv [xvv] (beta (x:vv) b) 
                                                    where xvv = (x,beta vv a) 
  App f         a -> let (a',f') = (beta vv a, beta vv f) in 
                     (if a'==a && f'==f then id else beta vv) $ App f' a'
  Prod x a b      -> Prod x (beta vv a) (beta (x:vv) b)
  Abs x b         -> Abs x (beta (x:vv) b)
  _               -> c