diff options
| author | Kathy Gray | 2014-05-14 13:26:33 +0100 |
|---|---|---|
| committer | Kathy Gray | 2014-05-14 13:26:33 +0100 |
| commit | 032f4937558c094c1878b1c1d467b4f630911450 (patch) | |
| tree | d71b77f1325e67ff7dbe8d5629855e9c5c3f2cef /src/pretty_print.ml | |
| parent | 314205cc12f9872b5c11ca76d4eb74a12d85cda7 (diff) | |
More interface update for connecting externally (interp_interface provides functions for connecting the interpreter to a memory model)
Also adding default values to index vectors for supporting sparse vectors/maps
Diffstat (limited to 'src/pretty_print.ml')
| -rw-r--r-- | src/pretty_print.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/pretty_print.ml b/src/pretty_print.ml index ecafc5f2..759e2f4a 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -236,7 +236,7 @@ and pp_exp ppf (E_aux(e,(_,annot))) = fprintf ppf "@[<0> %a %a (%a %a %a %a %a %a %a %a)@ @[<1>%a@]@]" kwd "foreach " pp_id id kwd "from " pp_exp exp1 kwd " to " pp_exp exp2 kwd "by " pp_exp exp3 kwd "in" pp_ord order pp_exp exp4 | E_vector(exps) -> fprintf ppf "@[<0>%a%a%a@]" kwd "[" (list_pp pp_comma_exp pp_exp) exps kwd "]" - | E_vector_indexed(iexps) -> + | E_vector_indexed(iexps,default) -> let iformat ppf (i,e) = fprintf ppf "@[<1>%i%a %a%a@]" i kwd " = " pp_exp e kwd "," in let lformat ppf (i,e) = fprintf ppf "@[<1>%i%a %a@]" i kwd " = " pp_exp e in fprintf ppf "@[<0> %a%a%a@]" kwd "[" (list_pp iformat lformat) iexps kwd "]" @@ -666,7 +666,7 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) = fprintf ppf "@[<0>(E_aux (%a %a %a %a %a %a @ @[<1> %a @]) (%a, %a))@]" kwd "E_for" 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_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_indexed(iexps) -> + | E_vector_indexed(iexps,default) -> (*TODO print out default when it is an nonempty*) let iformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) %a@]" i kwd ", " pp_lem_exp e kwd ";" in let lformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) @]" i kwd ", " pp_lem_exp e in fprintf ppf "@[<0>(E_aux (%a [%a]) (%a, %a))@]" kwd "E_vector_indexed" (list_pp iformat lformat) iexps pp_lem_l l pp_annot annot |