diff options
| author | Kathy Gray | 2015-02-13 15:50:51 +0000 |
|---|---|---|
| committer | Kathy Gray | 2015-02-13 15:50:51 +0000 |
| commit | f0bc412fa3b9f3f2b6131fe5322d4916730efac1 (patch) | |
| tree | 31ab6d211354d8850526166a1f0ff612c05e0e51 /src/pretty_print.ml | |
| parent | 7531d3dec300e9251f3abd6d57fc3a3464edf1c1 (diff) | |
Actually use new dependency information in generation of lem/etc.
Also stop rewriting code in the pretty printer, instead move it all into a new general rewriting pass
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 cd754786..a622cd3a 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -416,7 +416,7 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) = | E_let(leb,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_let" pp_lem_let leb pp_lem_exp exp pp_lem_l l pp_annot annot | E_assign(lexp,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_assign" pp_lem_lexp lexp pp_lem_exp exp pp_lem_l l pp_annot annot | E_exit exp -> fprintf ppf "@[<0>(E_aux (E_exit %a) (%a, %a))@]" pp_lem_exp exp pp_lem_l l pp_annot annot - | E_internal_exp (l, Base((_,t),_,_,_,bindings)) -> + | E_internal_exp ((l, Base((_,t),_,_,_,bindings))) -> (*TODO use bindings where appropriate*) (match t.t with | Tapp("register",[TA_typ {t=Tapp("vector",[TA_nexp _;TA_nexp r;_;_])}]) @@ -975,7 +975,7 @@ let doc_exp, doc_let = | E_app_infix(l,op,r) -> failwith ("unexpected app_infix operator " ^ (pp_format_id op)) (* doc_op (doc_id op) (exp l) (exp r) *) - | E_internal_exp (l, Base((_,t),_,_,_,bindings)) -> (*TODO use bindings*) + | E_internal_exp((l, Base((_,t),_,_,_,bindings))) -> (*TODO use bindings, and other params*) (match t.t with | Tapp("register",[TA_typ {t=Tapp("vector",[TA_nexp _;TA_nexp r;_;_])}]) | Tapp("vector",[TA_nexp _;TA_nexp r;_;_]) -> |