summaryrefslogtreecommitdiff
path: root/src/ast_util.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/ast_util.ml')
-rw-r--r--src/ast_util.ml122
1 files changed, 115 insertions, 7 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml
index d0efc0de..33af1be7 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -519,7 +519,7 @@ and map_exp_annot_aux f = function
| E_tuple xs -> E_tuple (List.map (map_exp_annot f) xs)
| E_if (cond, t, e) -> E_if (map_exp_annot f cond, map_exp_annot f t, map_exp_annot f e)
| E_for (v, e1, e2, e3, o, e4) -> E_for (v, map_exp_annot f e1, map_exp_annot f e2, map_exp_annot f e3, o, map_exp_annot f e4)
- | E_loop (loop_type, e1, e2) -> E_loop (loop_type, map_exp_annot f e1, map_exp_annot f e2)
+ | E_loop (loop_type, measure, e1, e2) -> E_loop (loop_type, map_measure_annot f measure, map_exp_annot f e1, map_exp_annot f e2)
| E_vector exps -> E_vector (List.map (map_exp_annot f) exps)
| E_vector_access (exp1, exp2) -> E_vector_access (map_exp_annot f exp1, map_exp_annot f exp2)
| E_vector_subrange (exp1, exp2, exp3) -> E_vector_subrange (map_exp_annot f exp1, map_exp_annot f exp2, map_exp_annot f exp3)
@@ -546,6 +546,10 @@ and map_exp_annot_aux f = function
| E_var (lexp, exp1, exp2) -> E_var (map_lexp_annot f lexp, map_exp_annot f exp1, map_exp_annot f exp2)
| E_internal_plet (pat, exp1, exp2) -> E_internal_plet (map_pat_annot f pat, map_exp_annot f exp1, map_exp_annot f exp2)
| E_internal_return exp -> E_internal_return (map_exp_annot f exp)
+and map_measure_annot f (Measure_aux (m, l)) = Measure_aux (map_measure_annot_aux f m, l)
+and map_measure_annot_aux f = function
+ | Measure_none -> Measure_none
+ | Measure_some exp -> Measure_some (map_exp_annot f exp)
and map_opt_default_annot f (Def_val_aux (df, annot)) = Def_val_aux (map_opt_default_annot_aux f df, f annot)
and map_opt_default_annot_aux f = function
| Def_val_empty -> Def_val_empty
@@ -619,6 +623,84 @@ and map_lexp_annot_aux f = function
| LEXP_vector_range (lexp, exp1, exp2) -> LEXP_vector_range (map_lexp_annot f lexp, map_exp_annot f exp1, map_exp_annot f exp2)
| LEXP_field (lexp, id) -> LEXP_field (map_lexp_annot f lexp, id)
+and map_typedef_annot f = function
+ | TD_aux (td_aux, annot) -> TD_aux (td_aux, f annot)
+
+and map_fundef_annot f = function
+ | FD_aux (fd_aux, annot) -> FD_aux (map_fundef_annot_aux f fd_aux, f annot)
+and map_fundef_annot_aux f = function
+ | FD_function (rec_opt, tannot_opt, eff_opt, funcls) -> FD_function (map_recopt_annot f rec_opt, tannot_opt, eff_opt,
+ List.map (map_funcl_annot f) funcls)
+and map_funcl_annot f = function
+ | FCL_aux (fcl, annot) -> FCL_aux (map_funcl_annot_aux f fcl, f annot)
+and map_funcl_annot_aux f = function
+ | FCL_Funcl (id, pexp) -> FCL_Funcl (id, map_pexp_annot f pexp)
+and map_recopt_annot f = function
+ | Rec_aux (rec_aux, l) -> Rec_aux (map_recopt_annot_aux f rec_aux, l)
+and map_recopt_annot_aux f = function
+ | Rec_nonrec -> Rec_nonrec
+ | Rec_rec -> Rec_rec
+ | Rec_measure (pat, exp) -> Rec_measure (map_pat_annot f pat, map_exp_annot f exp)
+
+and map_mapdef_annot f = function
+ | MD_aux (md_aux, annot) -> MD_aux (map_mapdef_annot_aux f md_aux, f annot)
+and map_mapdef_annot_aux f = function
+ | MD_mapping (id, tannot_opt, mapcls) -> MD_mapping (id, tannot_opt, List.map (map_mapcl_annot f) mapcls)
+
+and map_valspec_annot f = function
+ | VS_aux (vs_aux, annot) -> VS_aux (vs_aux, f annot)
+
+and map_scattered_annot f = function
+ | SD_aux (sd_aux, annot) -> SD_aux (map_scattered_annot_aux f sd_aux, f annot)
+and map_scattered_annot_aux f = function
+ | SD_function (rec_opt, tannot_opt, eff_opt, name) -> SD_function (map_recopt_annot f rec_opt, tannot_opt, eff_opt, name)
+ | SD_funcl fcl -> SD_funcl (map_funcl_annot f fcl)
+ | SD_variant (id, typq) -> SD_variant (id, typq)
+ | SD_unioncl (id, tu) -> SD_unioncl (id, tu)
+ | SD_mapping (id, tannot_opt) -> SD_mapping (id, tannot_opt)
+ | SD_mapcl (id, mcl) -> SD_mapcl (id, map_mapcl_annot f mcl)
+ | SD_end id -> SD_end id
+
+and map_decspec_annot f = function
+ | DEC_aux (dec_aux, annot) -> DEC_aux (map_decspec_annot_aux f dec_aux, f annot)
+and map_decspec_annot_aux f = function
+ | DEC_reg (eff1, eff2, typ, id) -> DEC_reg (eff1, eff2, typ, id)
+ | DEC_config (id, typ, exp) -> DEC_config (id, typ, map_exp_annot f exp)
+ | DEC_alias (id, als) -> DEC_alias (id, map_aliasspec_annot f als)
+ | DEC_typ_alias (typ, id, als) -> DEC_typ_alias (typ, id, map_aliasspec_annot f als)
+and map_aliasspec_annot f = function
+ | AL_aux (al_aux, annot) -> AL_aux (map_aliasspec_annot_aux f al_aux, f annot)
+and map_aliasspec_annot_aux f = function
+ | AL_subreg (reg_id, id) -> AL_subreg (map_regid_annot f reg_id, id)
+ | AL_bit (reg_id, exp) -> AL_bit (map_regid_annot f reg_id, map_exp_annot f exp)
+ | AL_slice (reg_id, exp1, exp2) -> AL_slice (map_regid_annot f reg_id, map_exp_annot f exp1, map_exp_annot f exp2)
+ | AL_concat (reg_id1, reg_id2) -> AL_concat (map_regid_annot f reg_id1, map_regid_annot f reg_id2)
+and map_regid_annot f = function
+ | RI_aux (ri_aux, annot) -> RI_aux (map_regid_annot_aux f ri_aux, f annot)
+and map_regid_annot_aux f = function
+ | RI_id id -> RI_id id
+
+and map_def_annot f = function
+ | DEF_type td -> DEF_type (map_typedef_annot f td)
+ | DEF_fundef fd -> DEF_fundef (map_fundef_annot f fd)
+ | DEF_mapdef md -> DEF_mapdef (map_mapdef_annot f md)
+ | DEF_val lb -> DEF_val (map_letbind_annot f lb)
+ | DEF_spec vs -> DEF_spec (map_valspec_annot f vs)
+ | DEF_fixity (prec, n, id) -> DEF_fixity (prec, n, id)
+ | DEF_overload (name, overloads) -> DEF_overload (name, overloads)
+ | DEF_default ds -> DEF_default ds
+ | DEF_scattered sd -> DEF_scattered (map_scattered_annot f sd)
+ | DEF_measure (id, pat, exp) -> DEF_measure (id, map_pat_annot f pat, map_exp_annot f exp)
+ | DEF_loop_measures (id, measures) -> DEF_loop_measures (id, List.map (map_loop_measure_annot f) measures)
+ | DEF_reg_dec ds -> DEF_reg_dec (map_decspec_annot f ds)
+ | DEF_internal_mutrec fds -> DEF_internal_mutrec (List.map (map_fundef_annot f) fds)
+ | DEF_pragma (name, arg, l) -> DEF_pragma (name, arg, l)
+and map_defs_annot f = function
+ | Defs defs -> Defs (List.map (map_def_annot f) defs)
+
+and map_loop_measure_annot f = function
+ | Loop (loop, exp) -> Loop (loop, map_exp_annot f exp)
+
let id_loc = function
| Id_aux (_, l) -> l
@@ -648,6 +730,7 @@ let def_loc = function
| DEF_internal_mutrec _ -> Parse_ast.Unknown
| DEF_pragma (_, _, l) -> l
| DEF_measure (id, _, _) -> id_loc id
+ | DEF_loop_measures (id, _) -> id_loc id
let string_of_id = function
| Id_aux (Id v, _) -> v
@@ -838,8 +921,8 @@ let rec string_of_exp (E_aux (exp, _)) =
^ " by " ^ string_of_exp u ^ " order " ^ string_of_order ord
^ ") { "
^ string_of_exp body
- | E_loop (While, cond, body) -> "while " ^ string_of_exp cond ^ " do " ^ string_of_exp body
- | E_loop (Until, cond, body) -> "repeat " ^ string_of_exp body ^ " until " ^ string_of_exp cond
+ | E_loop (While, measure, cond, body) -> "while " ^ string_of_measure measure ^ string_of_exp cond ^ " do " ^ string_of_exp body
+ | E_loop (Until, measure, cond, body) -> "repeat " ^ string_of_measure measure ^ string_of_exp body ^ " until " ^ string_of_exp cond
| E_assert (test, msg) -> "assert(" ^ string_of_exp test ^ ", " ^ string_of_exp msg ^ ")"
| E_exit exp -> "exit " ^ string_of_exp exp
| E_throw exp -> "throw " ^ string_of_exp exp
@@ -853,7 +936,12 @@ let rec string_of_exp (E_aux (exp, _)) =
| E_internal_return exp -> "internal_return (" ^ string_of_exp exp ^ ")"
| E_internal_plet (pat, exp, body) -> "internal_plet " ^ string_of_pat pat ^ " = " ^ string_of_exp exp ^ " in " ^ string_of_exp body
| E_nondet _ -> "NONDET"
- | E_internal_value _ -> "INTERNAL VALUE"
+ | E_internal_value v -> "INTERNAL_VALUE(" ^ Value.string_of_value v ^ ")"
+
+and string_of_measure (Measure_aux (m,_)) =
+ match m with
+ | Measure_none -> ""
+ | Measure_some exp -> "termination_measure { " ^ string_of_exp exp ^ "}"
and string_of_fexp (FE_aux (FE_Fexp (field, exp), _)) =
string_of_id field ^ " = " ^ string_of_exp exp
@@ -1448,8 +1536,8 @@ let rec subst id value (E_aux (e_aux, annot) as exp) =
| E_if (cond, then_exp, else_exp) ->
E_if (subst id value cond, subst id value then_exp, subst id value else_exp)
- | E_loop (loop, cond, body) ->
- E_loop (loop, subst id value cond, subst id value body)
+ | E_loop (loop, measure, cond, body) ->
+ E_loop (loop, subst_measure id value measure, subst id value cond, subst id value body)
| E_for (id', exp1, exp2, exp3, order, body) when Id.compare id id' = 0 ->
E_for (id', exp1, exp2, exp3, order, body)
| E_for (id', exp1, exp2, exp3, order, body) ->
@@ -1503,6 +1591,11 @@ let rec subst id value (E_aux (e_aux, annot) as exp) =
in
wrap e_aux
+and subst_measure id value (Measure_aux (m_aux, l)) =
+ match m_aux with
+ | Measure_none -> Measure_aux (Measure_none, l)
+ | Measure_some exp -> Measure_aux (Measure_some (subst id value exp), l)
+
and subst_pexp id value (Pat_aux (pexp_aux, annot)) =
let pexp_aux = match pexp_aux with
| Pat_exp (pat, exp) when IdSet.mem id (pat_ids pat) -> Pat_exp (pat, exp)
@@ -1660,7 +1753,7 @@ let rec locate : 'a. (l -> l) -> 'a exp -> 'a exp = fun f (E_aux (e_aux, (l, ann
| E_app_infix (exp1, op, exp2) -> E_app_infix (locate f exp1, locate_id f op, locate f exp2)
| E_tuple exps -> E_tuple (List.map (locate f) exps)
| E_if (cond_exp, then_exp, else_exp) -> E_if (locate f cond_exp, locate f then_exp, locate f else_exp)
- | E_loop (loop, cond, body) -> E_loop (loop, locate f cond, locate f body)
+ | E_loop (loop, measure, cond, body) -> E_loop (loop, locate_measure f measure, locate f cond, locate f body)
| E_for (id, exp1, exp2, exp3, ord, exp4) ->
E_for (locate_id f id, locate f exp1, locate f exp2, locate f exp3, ord, locate f exp4)
| E_vector exps -> E_vector (List.map (locate f) exps)
@@ -1694,6 +1787,12 @@ let rec locate : 'a. (l -> l) -> 'a exp -> 'a exp = fun f (E_aux (e_aux, (l, ann
in
E_aux (e_aux, (f l, annot))
+and locate_measure : 'a. (l -> l) -> 'a internal_loop_measure -> 'a internal_loop_measure = fun f (Measure_aux (m, l)) ->
+ let m = match m with
+ | Measure_none -> Measure_none
+ | Measure_some exp -> Measure_some (locate f exp)
+ in Measure_aux (m, f l)
+
and locate_letbind : 'a. (l -> l) -> 'a letbind -> 'a letbind = fun f (LB_aux (LB_val (pat, exp), (l, annot))) ->
LB_aux (LB_val (locate_pat f pat, locate f exp), (f l, annot))
@@ -1728,6 +1827,15 @@ let unique l =
incr unique_ref;
l
+let extern_assoc backend exts =
+ try
+ try
+ Some (List.assoc backend exts)
+ with Not_found ->
+ Some (List.assoc "_" exts)
+ with Not_found ->
+ None
+
(**************************************************************************)
(* 1. Substitutions *)
(**************************************************************************)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 16:07:31 +0000