Skip to content

Commit b0c6bf4

Browse files
FrederickPuFrederickPu
committed
switched SSAExpr.loop to CPS form
1 parent 0f138bd commit b0c6bf4

1 file changed

Lines changed: 56 additions & 58 deletions

File tree

‎Pullback/UnquoteTy/SSA.lean‎

Lines changed: 56 additions & 58 deletions
Original file line numberDiff line numberDiff line change
@@ -80,7 +80,11 @@ def SSAConst.inferType : SSAConst → SSAType
8080
| ofFloat _ => .ofBase .float
8181
| ofInt _ => .ofBase .int
8282
| ofUnit _ => .ofBase .unit
83-
| loop ty => .fun (.ofBase ty) (.fun (.fun (.ofBase ty) (.prod (.ofBase ty) (.ofBase .int))) (.ofBase ty))-- ((x, 1) denotes break anything else denotes continue) todo :: adapt loop to use ForInStep and be inline with Lean.Loop
83+
| loop ty => .fun (.ofBase ty) <|
84+
.fun (.fun (.ofBase ty) (.fun (.fun (.ofBase ty) (.ofBase ty)) (.ofBase ty)))
85+
(.ofBase ty)
86+
87+
-- the step function takes in a kcontinue continuation and returns ty (loop in CPS form)
8488
| prod α β => .fun α (.fun β (.prod α β))
8589
| prod₁ α β => .fun (.prod α β) α
8690
| prod₂ α β => .fun (.prod α β) β
@@ -146,15 +150,9 @@ theorem Array.find?_eq_getElem_findFinIdx? {α : Type u} (xs : Array α) (p : α
146150
· rintro ⟨_, _, _, rfl, _⟩; grind
147151
· grind
148152

153+
#check ForIn
149154
-- (a : α, true) means break (a : α, false) means continue
150-
def SSA.loop {α : Type u} [Inhabited α] (init : α) (step : α → α × Bool) : α := Id.run do
151-
let mut state := init
152-
while true do
153-
let temp := step state
154-
if temp.2 then
155-
break
156-
state := temp.1
157-
return state
155+
def SSA.loop {α : Type u} [Inhabited α] (init : α) (step : α → (α → α) → α) : α := sorry
158156

159157
private def SSABaseType.decEq : (ty : SSABaseType) → DecidableEq ty.type
160158
| float => by
@@ -185,7 +183,7 @@ def SSAConst.interp : (e : SSAConst) → (e.inferType).type
185183
| ofInt i => i
186184
| ofUnit () => ()
187185
| ifthenelse ty => fun c t e => if (cast (by simp [SSAType.type, SSABaseType.type]) c : Int) != 0 then t else e
188-
| loop ty => fun init => fun step => SSA.loop (α := (SSAType.ofBase ty).type) init (fun x => let (a, b) := step x; (a, cast (β := Int) (by simp [SSAType.type, SSABaseType.type]) b == 1))
186+
| loop ty => SSA.loop (α := (SSAType.ofBase ty).type)
189187
| prod α β => (@Prod.mk α.type β.type)
190188
| prod₁ α β => fun ab => ab.1
191189
| prod₂ α β => fun ab => ab.2
@@ -330,51 +328,51 @@ inductive SSADo where
330328
| return (out : SSAExpr) : SSADo
331329
| ifthenelse (cond : SSAExpr) (t e : SSADo) (rest : SSADo) : SSADo
332330

333-
-- partial def SSADo.toSSAExpr (mutVars : VarMap) (kbreak kcontinue : Option Name) : SSADo → SSAExpr
334-
-- | expr (.const (.ofUnit ())) =>
335-
-- match kcontinue with
336-
-- | some kcontinue => SSAExpr.app (SSAExpr.var kcontinue) (mkMutTuple mutVars).1
337-
-- | none => (.const (.ofUnit ()))
338-
-- -- note: only trailing exprs are interpreted as return types
339-
-- -- ie: `do if cond then 10 else 10` is invalid but `do if cond then return 10 else (); 10` is valid
340-
-- | expr e =>
341-
-- match kcontinue with
342-
-- | some kcontinue => e
343-
-- | none => sorry -- loop body should not end in non unit type
344-
-- | seq s₁ s₂ => SSAExpr.letE `x (s₁.toSSAExpr mutVars kbreak kcontinue) (s₂.toSSAExpr mutVars kbreak kcontinue)
345-
-- | letE var val rest => SSAExpr.letE var val (rest.toSSAExpr mutVars kbreak kcontinue)
346-
-- | letM var val rest => SSAExpr.letE var val (rest.toSSAExpr (mutVars.push (var, val.inferType)) kbreak kcontinue)
347-
-- | assign var val rest => SSAExpr.letE var val (rest.toSSAExpr mutVars kbreak kcontinue)
348-
-- | loop body rest =>
349-
-- let (mutTuple, mutTupleType) := (mkMutTuple mutVars)
350-
-- let bodyMutVars : VarMap := sorry
351-
-- let nS : Name := freshName (Array.append mutVars bodyMutVars) `s
352-
-- let breakNew : SSAExpr := SSAExpr.lam nS mutTupleType <| (destructMutTuple mutVars (rest.toSSAExpr mutVars kbreak kcontinue))
353-
-- let nKBreak : Name := freshName mutVars `kbreak
354-
-- let nKContinue : Name := freshName mutVars `kcontinue
355-
-- -- todo :: modify mutvars passed into toSSAExpr for body
356-
-- let body' : SSAExpr := destructMutTuple mutVars (body.toSSAExpr mutVars nKBreak nKContinue)
357-
-- SSAExpr.letE nKBreak breakNew <|
358-
-- SSAExpr.app (SSAExpr.app (SSAExpr.const (SSAConst.loop mutTupleType)) (SSAExpr.lam nKContinue (SSAType.fun mutTupleType (SSAType.ofBase .unit)) (SSAExpr.lam nS mutTupleType body'))) mutTuple
359-
-- | .break =>
360-
-- match kbreak with
361-
-- | some kbreak =>
362-
-- let mutTuple : SSAExpr := (mkMutTuple mutVars).1
363-
-- SSAExpr.app (SSAExpr.var kbreak) mutTuple
364-
-- | none => sorry -- violates grammer
365-
-- | .continue =>
366-
-- match kcontinue with
367-
-- | some kcontinue =>
368-
-- let mutTuple : SSAExpr := (mkMutTuple mutVars).1
369-
-- SSAExpr.app (SSAExpr.var kcontinue) mutTuple
370-
-- | none => sorry -- violates grammer
371-
-- | .return out => out
372-
-- | ifthenelse cond t e rest =>
373-
-- let (mutTuple, mutTupleType) := (mkMutTuple mutVars)
374-
-- let nKContinue : Name := freshName mutVars `kcontinue
375-
-- let restMutVars : VarMap := sorry
376-
-- let nS : Name := freshName (Array.append mutVars restMutVars) `s
377-
-- -- todo :: pass expanded mutvars into toSSAExpr
378-
-- let continue' := SSAExpr.lam nS mutTupleType <| rest.toSSAExpr mutVars kbreak kcontinue
379-
-- SSAExpr.letE nKContinue continue' <|
380-
-- SSAExpr.ifthenelse cond (t.toSSAExpr mutVars kbreak nKContinue) (e.toSSAExpr mutVars kbreak nKContinue)
331+
partial def SSADo.toSSAExpr (vars : VarMap) (mutVars : VarMap) (kbreak kcontinue : Option Name) : SSADo → Option SSAExpr
332+
| expr (.const (.ofUnit ())) =>
333+
match kcontinue with
334+
| some kcontinue => SSAExpr.app (SSAExpr.var kcontinue) (mkMutTuple mutVars).1
335+
| none => (.const (.ofUnit ()))
336+
-- note: only trailing exprs are interpreted as return types
337+
-- ie: `do if cond then 10 else 10` is invalid but `do if cond then return 10 else (); 10` is valid
338+
| expr e =>
339+
match kcontinue with
340+
| some kcontinue => e
341+
| none => sorry -- loop body should not end in non unit type
342+
| seq s₁ s₂ => SSAExpr.letE `x (s₁.toSSAExpr vars mutVars kbreak kcontinue) (s₂.toSSAExpr vars mutVars kbreak kcontinue)
343+
| letE var val rest => SSAExpr.letE var val (rest.toSSAExpr vars mutVars kbreak kcontinue)
344+
| letM var val rest => SSAExpr.letE var val (rest.toSSAExpr (mutVars.push (var, val.inferType vars)) kbreak kcontinue)
345+
| assign var val rest => SSAExpr.letE var val (rest.toSSAExpr mutVars kbreak kcontinue)
346+
| loop body rest =>
347+
let (mutTuple, mutTupleType) := (mkMutTuple mutVars)
348+
let bodyMutVars : VarMap := sorry
349+
let nS : Name := freshName (Array.append mutVars bodyMutVars) `s
350+
let breakNew : SSAExpr := SSAExpr.lam nS mutTupleType <| (destructMutTuple mutVars (rest.toSSAExpr mutVars kbreak kcontinue))
351+
let nKBreak : Name := freshName mutVars `kbreak
352+
let nKContinue : Name := freshName mutVars `kcontinue
353+
-- todo :: modify mutvars passed into toSSAExpr for body
354+
let body' : SSAExpr := destructMutTuple mutVars (body.toSSAExpr mutVars nKBreak nKContinue)
355+
SSAExpr.letE nKBreak breakNew <|
356+
SSAExpr.app (SSAExpr.app (SSAExpr.const (SSAConst.loop mutTupleType)) (SSAExpr.lam nKContinue (SSAType.fun mutTupleType (SSAType.ofBase .unit)) (SSAExpr.lam nS mutTupleType body'))) mutTuple
357+
| .break =>
358+
match kbreak with
359+
| some kbreak =>
360+
let mutTuple : SSAExpr := (mkMutTuple mutVars).1
361+
SSAExpr.app (SSAExpr.var kbreak) mutTuple
362+
| none => sorry -- violates grammer
363+
| .continue =>
364+
match kcontinue with
365+
| some kcontinue =>
366+
let mutTuple : SSAExpr := (mkMutTuple mutVars).1
367+
SSAExpr.app (SSAExpr.var kcontinue) mutTuple
368+
| none => sorry -- violates grammer
369+
| .return out => out
370+
| ifthenelse cond t e rest =>
371+
let (mutTuple, mutTupleType) := (mkMutTuple mutVars)
372+
let nKContinue : Name := freshName mutVars `kcontinue
373+
let restMutVars : VarMap := sorry
374+
let nS : Name := freshName (Array.append mutVars restMutVars) `s
375+
-- todo :: pass expanded mutvars into toSSAExpr
376+
let continue' := SSAExpr.lam nS mutTupleType <| rest.toSSAExpr mutVars kbreak kcontinue
377+
SSAExpr.letE nKContinue continue' <|
378+
SSAExpr.ifthenelse cond (t.toSSAExpr mutVars kbreak nKContinue) (e.toSSAExpr mutVars kbreak nKContinue)

0 commit comments

Comments
 (0)