Permalink
Browse files

Move pi's from synthesis to checking.

  • Loading branch information...
1 parent d442bda commit e1e026145353c58ea01550398fbb4b63710e5591 @mboes committed Apr 4, 2012
Showing with 1 addition and 1 deletion.
  1. +1 −1 Dedukti/Runtime.hs
View
@@ -118,13 +118,13 @@ mkpair n ty = Pair (Box ty (Var n)) (Var n)
check :: Int -> Term -> Code -> ()
check n (TLam _ f) (Pi a f') = check (n + 1) (f (mkpair n a)) (f' (Var n))
+check n (TPi (Box Type tya) f) ty = check (n + 1) (f (mkpair n tya)) ty
check n (TLet (Pair t tc) f) ty
| tyt <- synth n t = check (n + 1) (f (Pair (Box tyt tc) tc)) ty
check n t ty = convertible n (synth n t) ty
synth :: Int -> Term -> Code
synth n (Box ty _) = ty
-synth n (TPi (Box Type tya) f) = synth (n + 1) (f (mkpair n tya))
synth n (TApp t1 (Pair t2 c2))
| Pi tya f <- synth n t1
, () <- check n t2 tya = f c2

0 comments on commit e1e0261

Please sign in to comment.