diff options
| -rw-r--r-- | src/pretty_print_lem.ml | 1 | ||||
| -rw-r--r-- | src/pretty_print_lem_ast.ml | 15 | ||||
| -rw-r--r-- | src/spec_analysis.ml | 1 |
3 files changed, 17 insertions, 0 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 5ca0c1bc..dc51c819 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1544,6 +1544,7 @@ let rec doc_def_lem sequential mwords def = (* let _ = Pretty_print_sail.pp_defs stderr (Defs [def]) in *) match def with | DEF_spec v_spec -> (doc_spec_lem mwords v_spec,empty) + | DEF_fixity _ -> (empty,empty) | DEF_overload _ -> (empty,empty) | DEF_type t_def -> (group (doc_typdef_lem sequential mwords t_def) ^/^ hardline,empty) | DEF_reg_dec dec -> (group (doc_dec_lem sequential dec),empty) diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml index 2e464a08..2232b4de 100644 --- a/src/pretty_print_lem_ast.ml +++ b/src/pretty_print_lem_ast.ml @@ -234,6 +234,17 @@ let pp_lem_nexp ppf n = base ppf (pp_format_nexp_lem n) let pp_lem_ord ppf o = base ppf (pp_format_ord_lem o) let pp_lem_effects ppf e = base ppf (pp_format_effects_lem e) let pp_lem_beffect ppf be = base ppf (pp_format_base_effect_lem be) +let pp_lem_loop ppf l = + let l_str = match l with + | While -> "While" + | Until -> "Until" in + base ppf l_str +let pp_lem_prec ppf p = + let p_str = match p with + | Infix -> "Infix" + | InfixL -> "InfixL" + | InfixR -> "InfixR" in + base ppf p_str let pp_lem_nexp_constraint ppf nc = base ppf (pp_format_nexp_constraint_lem nc) @@ -380,6 +391,9 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) = fprintf ppf "@[<0>(E_aux (E_for %a %a %a %a %a @ @[<1> %a @]) (%a, %a))@]" pp_lem_id id pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_exp exp3 pp_lem_ord order pp_lem_exp exp4 pp_lem_l l pp_annot annot + | E_loop(loop,cond,body) -> + fprintf ppf "@[<0>(E_aux (E_loop %a %a @ @[<1> %a @]) (%a, %a))@]" + pp_lem_loop loop pp_lem_exp cond pp_lem_exp body pp_lem_l l pp_annot annot | E_vector(exps) -> fprintf ppf "@[<0>(E_aux (%a [%a]) (%a, %a))@]" kwd "E_vector" (list_pp pp_semi_lem_exp pp_lem_exp) exps pp_lem_l l pp_annot annot | E_vector_access(v,e) -> @@ -634,6 +648,7 @@ let pp_lem_def ppf d = | DEF_val(lbind) -> fprintf ppf "(DEF_val %a);@\n" pp_lem_let lbind | DEF_reg_dec(dec) -> fprintf ppf "(DEF_reg_dec %a);@\n" pp_lem_dec dec | DEF_comm d -> fprintf ppf "" + | DEF_fixity (prec, n, id) -> fprintf ppf "(DEF_fixity %a %s %a);@\n" pp_lem_prec prec (lemnum string_of_int n) pp_lem_id id | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "initial_check didn't remove all scattered Defs") let pp_lem_defs ppf (Defs(defs)) = diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index 2e368c53..c896f07a 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -534,6 +534,7 @@ let fv_of_def consider_var consider_scatter_as_one all_defs = function | DEF_fundef fdef -> fv_of_fun consider_var fdef | DEF_val lebind -> ((fun (b,u,_) -> (b,u)) (fv_of_let consider_var mt mt mt lebind)) | DEF_spec vspec -> fv_of_vspec consider_var vspec + | DEF_fixity _ -> mt,mt | DEF_overload (id,ids) -> init_env (string_of_id id), List.fold_left (fun ns id -> Nameset.add (string_of_id id) ns) mt ids | DEF_default def -> mt,mt | DEF_scattered sdef -> fv_of_scattered consider_var consider_scatter_as_one all_defs sdef |