summaryrefslogtreecommitdiff
path: root/src/ast_util.mli
diff options
context:
space:
mode:
authorBrian Campbell2017-08-28 11:29:37 +0100
committerBrian Campbell2017-08-28 11:29:37 +0100
commitb0dbd56a224497d91bc2f1950b2f3246247b02b3 (patch)
treefdfd3009958ea22a4693b7f52fcb43af3a17a8e7 /src/ast_util.mli
parent0025734876be60e2de6fba935cb507a6158d870a (diff)
parentbeb2279dcab654d6e7c6ff16247dd93c743a27ba (diff)
Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into mono-experiments
# Conflicts: # src/gen_lib/sail_values.lem
Diffstat (limited to 'src/ast_util.mli')
-rw-r--r--src/ast_util.mli10
1 files changed, 10 insertions, 0 deletions
diff --git a/src/ast_util.mli b/src/ast_util.mli
index b0ccb7b8..7580404d 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -47,10 +47,18 @@ open Ast
val mk_nc : n_constraint_aux -> n_constraint
val mk_nexp : nexp_aux -> nexp
val mk_exp : unit exp_aux -> unit exp
+val mk_pat : unit pat_aux -> unit pat
val mk_lit : lit_aux -> lit
+val mk_lit_exp : lit_aux -> unit exp
+val mk_funcl : id -> unit pat -> unit exp -> unit funcl
+val mk_fundef : (unit funcl) list -> unit def
+val mk_val_spec : val_spec_aux -> unit def
val unaux_exp : 'a exp -> 'a exp_aux
+val inc_ord : order
+val dec_ord : order
+
(* Functions to map over the annotations in sub-expressions *)
val map_exp_annot : ('a annot -> 'b annot) -> 'a exp -> 'b exp
val map_pat_annot : ('a annot -> 'b annot) -> 'a pat -> 'b pat
@@ -92,6 +100,8 @@ val id_of_fundef : 'a fundef -> id
val id_of_kid : kid -> id
+val prepend_id : string -> id -> id
+
module Id : sig
type t = id
val compare : id -> id -> int