From dd00feacb373defbcfd8c50b9a8381c4a7db7cba Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 30 Nov 2017 19:35:35 +0000
Subject: Improvements to enable parsing and checking intermediate rewriting
 steps

Parser now has syntax for mutual recusion blocks

mutual {
  ... fundefs ...
}

which is used for parsing and pretty printing
DEF_internal_mutrec. It's stripped away by the initial_check, so the
typechecker never sees DEF_internal_mutrec. Maybe this could change,
as forcing mutual recursion to be explicit would probably be a good
thing.

Added record syntax to the new parser

New option -dmagic_hash is similar to GHC's -XMagicHash in that it
allows for identifiers to contain the special hash character, which is
used to introduce new autogenerated variables in a way that doesn't
clash with existing names.

Option -sil compiles sail down to the intermediate language defined in
sil.ott (not complete yet).
---
 src/process_file.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src/process_file.mli')

diff --git a/src/process_file.mli b/src/process_file.mli
index b575bd14..116df06e 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -48,6 +48,7 @@ val rewrite_ast: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
 val rewrite_undefined: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
 val rewrite_ast_lem : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
 val rewrite_ast_ocaml : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_ast_sil : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
 val rewrite_ast_check : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
 
 val load_file_no_check : Ast.order -> string -> unit Ast.defs
-- 
cgit v1.2.3