From: Simon Huber Date: Tue, 11 Aug 2015 11:36:10 +0000 (+0200) Subject: Fix squeezes X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=b8df2049c498d2a009fce8c10cd6a785399fc7ea;p=cubicaltt.git Fix squeezes --- diff --git a/Eval.hs b/Eval.hs index 9a4c760..772ec0a 100644 --- a/Eval.hs +++ b/Eval.hs @@ -361,27 +361,14 @@ transFillNeg i a u = (transFill i (a `sym` i) u) `sym` i -- Given u of type a "squeeze i a u" connects in the direction i -- trans i a u(i=0) to u(i=1) squeeze :: Name -> Val -> Val -> Val -squeeze i a u = comp i (a `disj` (i,j)) u $ mkSystem [ (j ~> 1, ui1) ] - where j = fresh (Atom i,a,u) - ui1 = u `face` (i ~> 1) - -squeezeFill :: Name -> Val -> Val -> Val -squeezeFill i a u = fill i (a `disj` (i,j)) u $ mkSystem [ (j ~> 1, ui1) ] +squeeze i a u = comp j (a `disj` (i,j)) u $ mkSystem [ (i ~> 1, ui1) ] where j = fresh (Atom i,a,u) ui1 = u `face` (i ~> 1) squeezes :: Name -> [(Ident,Ter)] -> Env -> [Val] -> [Val] -squeezes i [] _ [] = [] -squeezes i ((x,a):as) e (u:us) = - let v = squeezeFill i (eval e a) u - vi1 = squeeze i (eval e a) u - vs = squeezes i as (upd (x,v) e) us - in vi1 : vs -squeezes _ _ _ _ = error "squeezes: different lengths of types and values" - --- squeezeNeg :: Name -> Val -> Val -> Val --- squeezeNeg i a u = transNeg j (a `conj` (i,j)) u --- where j = fresh (Atom i,a,u) +squeezes i xas e us = comps j xas (e `disj` (i,j)) us' + where j = fresh (us,e) + us' = [ (mkSystem [(i ~> 1, u `face` (i ~> 1))],u) | u <- us ] -------------------------------------------------------------------------------