Skip to content

Commit

Permalink
Fix typos in DESIGN.md
Browse files Browse the repository at this point in the history
  • Loading branch information
msprotz committed Nov 3, 2016
1 parent 2c43fac commit c3f5579
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions DESIGN.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,12 +4,12 @@ Overview of KreMLin
From a high-level perspective, KreMLin takes an input AST, translates it into a
typed internal AST, then massages the program by performing repeated
transformations until the program fits within a simple enough subset dubbed
Low*. Once a program is valid Low*, it translates almost trivially into C*, an
Low\*. Once a program is valid Low\*, it translates almost trivially into C\*, an
idealized dialect of C. Then, the program is translated to an abstract C AST,
and finally pretty-printed.

The detailed steps are as follows. KreMLin:
- loads an AST written by F* or Dafny (see `InputAst.ml`)
- loads an AST written by F\* or Dafny (see `InputAst.ml`)
- translates it into an AST where expressions and patterns are annotated with
their types (see `InputAstToAst.ml`, `Ast.ml`)
- re-checks the program to see that it makes sense; possibly drops some
Expand Down Expand Up @@ -44,7 +44,7 @@ The detailed steps are as follows. KreMLin:
- performs part of the "round of transformations" again.

At this stage, the (unverified) invariant is that the any program fits the
definition of Low* and can be trivially translated to C*; KreMLin then:
definition of Low\* and can be trivially translated to C\*; KreMLin then:
- translates the program to C* (see `CStar.ml`, `AstToCStar.ml`); this involves
* going from a lexical scope to a block scope while preserving names insofar
as possible;
Expand Down

0 comments on commit c3f5579

Please sign in to comment.