Added translation from the CST to AST - #2
Closed
ychtao wants to merge 18 commits into
Closed
Conversation
… for the low-level CST nodes. Temp commit before rewriting
There was a problem hiding this comment.
Pull request overview
This PR introduces a CST→AST translation layer in CstToAst.lean and updates CST evaluation semantics in CstSemantics.lean, notably around like pattern handling.
Changes:
- Added
CstToAst.leanimplementing (partial) translation fromCedar.Spec.Cst.ExprintoCedar.Spec.Expr. - Added string unescaping and wildcard-pattern parsing utilities to support translation of string/pattern constructs.
- Updated
CstSemantics.leanto parselikepatterns more strictly (with Unicode escape support) and fail on invalid pattern escapes.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 8 comments.
| File | Description |
|---|---|
| cedar-lean/Cedar/Spec/CstToAst.lean | Adds CST→AST translation logic, including escape handling, attribute/member translation, and operator lowering. |
| cedar-lean/Cedar/Spec/CstSemantics.lean | Replaces permissive like pattern parsing with an Option-based parser (Unicode escape support) and propagates failures as .typeError. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+8
to
+9
| /- Begin code by Claude -/ | ||
| /- Check correctness later -/ |
Comment on lines
+159
to
+160
| let unescapted ← s.unescape? | ||
| some (.lit (.string unescapted)) |
Comment on lines
+213
to
+216
| | .index e => do | ||
| let s ← e.toStringLiteral? | ||
| some (.index s) | ||
|
|
Comment on lines
+16
to
+31
| private def parseUnicodeEscape (cs : List Char) : Option (Char × List Char) := do | ||
| match cs with | ||
| | '{' :: rest => | ||
| let digits := rest.takeWhile (· ≠ '}') | ||
| let afterBrace := rest.drop digits.length | ||
| match afterBrace with | ||
| | '}' :: remaining => | ||
| if digits.isEmpty ∨ digits.length > 6 then none else do | ||
| let codepoint ← digits.foldlM (fun acc d => do | ||
| let v ← hexDigitToNat? d | ||
| some (acc * 16 + v)) 0 | ||
| if codepoint > 0x10FFFF then none | ||
| else some (Char.ofNat codepoint, remaining) | ||
| | _ => none | ||
| | _ => none | ||
|
|
Comment on lines
+189
to
+193
| -- Unescape `eid` not done | ||
| | .uid path eid => do | ||
| let ty ← path.toAName? | ||
| match eid with | ||
| | .string s => some (.expr (.lit (.entityUID {ty := ty, eid := s}))) |
Comment on lines
+365
to
+368
| let y := (Int64.ofUInt64 x) | ||
| match compare y (Int64.MAX+1).toInt64 with | ||
| | .eq => some (.expr ((Expr.lit (.int (Int64.MIN).toInt64)).dashN (n-1).toNat)) | ||
| | .lt => some (.expr ((Expr.lit (.int (-y))).dashN (n-1).toNat)) |
Comment on lines
+281
to
+307
| private def toPatternAux (input : List Char) : Option Pattern := | ||
| match input with | ||
| | [] => some [] | ||
| | '\\' :: '*' :: cs => do let tail ← toPatternAux cs; some (.justChar '*' :: tail) | ||
| | '\\' :: '\\' :: cs => do let tail ← toPatternAux cs; some (.justChar '\\' :: tail) | ||
| | '\\' :: 'n' :: cs => do let tail ← toPatternAux cs; some (.justChar '\n' :: tail) | ||
| | '\\' :: 'r' :: cs => do let tail ← toPatternAux cs; some (.justChar '\r' :: tail) | ||
| | '\\' :: 't' :: cs => do let tail ← toPatternAux cs; some (.justChar '\t' :: tail) | ||
| | '\\' :: '0' :: cs => do let tail ← toPatternAux cs; some (.justChar '\x00' :: tail) | ||
| | '\\' :: '"' :: cs => do let tail ← toPatternAux cs; some (.justChar '"' :: tail) | ||
| | '\\' :: '\'' :: cs => do let tail ← toPatternAux cs; some (.justChar '\'' :: tail) | ||
| | '\\' :: 'u' :: '{' :: cs => | ||
| let digits := cs.takeWhile (· ≠ '}') | ||
| let afterBrace := cs.drop digits.length | ||
| match h : afterBrace with | ||
| | '}' :: remaining => do | ||
| if digits.isEmpty ∨ digits.length > 6 then none else do | ||
| let codepoint ← digits.foldlM (fun acc d => do | ||
| let v ← hexDigitToNat? d | ||
| some (acc * 16 + v)) 0 | ||
| if codepoint > 0x10FFFF then none | ||
| let tail ← toPatternAux remaining | ||
| some (.justChar (Char.ofNat codepoint) :: tail) | ||
| | _ => none | ||
| | '\\' :: _ => none | ||
| | '*' :: cs => do let tail ← toPatternAux cs; some (.star :: tail) | ||
| | c :: cs => do let tail ← toPatternAux cs; some (.justChar c :: tail) |
Comment on lines
+257
to
+261
| private def hexDigitToNat? (c : Char) : Option Nat := | ||
| if '0' ≤ c ∧ c ≤ '9' then some (c.toNat - '0'.toNat) | ||
| else if 'a' ≤ c ∧ c ≤ 'f' then some (c.toNat - 'a'.toNat + 10) | ||
| else if 'A' ≤ c ∧ c ≤ 'F' then some (c.toNat - 'A'.toNat + 10) | ||
| else none |
ychtao
marked this pull request as draft
May 27, 2026 14:44
ychtao
marked this pull request as ready for review
May 27, 2026 20:54
ychtao
marked this pull request as draft
May 27, 2026 20:54
ychtao
marked this pull request as ready for review
May 27, 2026 20:57
Comment on lines
+272
to
+283
| | some (.nDash n) => | ||
| match e.item.toLit? with | ||
| | some (.liNum x) => | ||
| let y := (Int64.ofUInt64 x) | ||
| match compare y (Int64.MAX+1).toInt64 with | ||
| | .eq => some (.expr ((Expr.lit (.int (Int64.MIN).toInt64)).dashN (n-1).toNat)) | ||
| | .lt => some (.expr ((Expr.lit (.int (-y))).dashN (n-1).toNat)) | ||
| | .gt => none | ||
| | _ => do | ||
| let eos ← e.item.toExprOrSpecial? | ||
| let expr ← eos.toExpr? | ||
| some (ExprOrSpecial.expr (expr.dashN n.toNat)) |
Comment on lines
+152
to
+159
| | .edOr e => match e.initial.initial with | ||
| | .rHas _ _ => none | ||
| | .rLike _ _ => none | ||
| | .rCommon i _ => match i.initial.initial.item.item with | ||
| | .literal l => match l with | ||
| | .liStr s => some s | ||
| | _ => none | ||
| | _ => none |
Comment on lines
+142
to
+146
| -- Unescape `eid` not done | ||
| | .uid path eid => do | ||
| let ty ← path.toAName? | ||
| match eid with | ||
| | .string s => some (.expr (.lit (.entityUID {ty := ty, eid := s}))) |
| | .expr e => some e | ||
| | .var v => some (.var v) | ||
| | .strLit s => do | ||
| let unescapted ← Cedar.Spec.CstCommon.unescape? s |
Comment on lines
+36
to
+58
| match s with | ||
| | "principal" => false | ||
| | "action" => false | ||
| | "resource" => false | ||
| | "context" => false | ||
| | "true" => false | ||
| | "false" => false | ||
| | "permit" => false | ||
| | "forbid" => false | ||
| | "when" => false | ||
| | "unless" => false | ||
| | "in" => false | ||
| | "has" => false | ||
| | "like" => false | ||
| | "is" => false | ||
| | "if" => false | ||
| | "then" => false | ||
| | "else" => false | ||
| | "__cedar" => false | ||
| | _ => true | ||
|
|
||
| private def Cst.Ident.toUnreservedId? : Cst.Ident → Option String | ||
| | .idIdent s => if Unreserved? s then some s else none |
Comment on lines
+484
to
+486
| public def Cst.Expr.toAExpr? (e : Cst.Expr) : Option AExpr := do | ||
| let ret ← e.toExprOrSpecial? | ||
| ret.toExpr? |
Comment on lines
+672
to
+684
| -- `id` to be filled in later | ||
| public def Cst.PolicyImpl.toPolicy? (p : Cst.PolicyImpl) : Option Cedar.Spec.Policy := do | ||
| let effect ← p.effect.toEffect? | ||
| let (ps, as, rs) ← extractScope? p.vars | ||
| let conds ← toConditions? p.conds | ||
| some {id := "", effect := effect, principalScope := ps, actionScope := as, resourceScope := rs, condition := conds} | ||
|
|
||
| public def Cst.Policy.toPolicy? : Cst.Policy → Option Cedar.Spec.Policy | ||
| | .policy p => p.toPolicy? | ||
|
|
||
| public def Cst.Policies.toPolicies? (ps : List Cst.Policy) : Option Cedar.Spec.Policies := do | ||
| let rets ← ps.mapM Cst.Policy.toPolicy? | ||
| some (rets.mapIdx (fun i p => {p with id := s!"policy{i}"})) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The translation of CST expressions to AST expressions is implemented in CstToAst.lean
The semantics of CST is implemented in CstSemantics.lean