diff options
| author | Kathy Gray | 2014-04-15 11:36:37 +0100 |
|---|---|---|
| committer | Kathy Gray | 2014-04-15 11:36:37 +0100 |
| commit | b6c01ea4e538cdd3d92f6ca2543e8ea95d542344 (patch) | |
| tree | a0dc818de6bd470ca0b3741c7d9fedf40da645a9 /src/pretty_print.ml | |
| parent | 5e9f4c46b55c527fe639ae88a78fd6386c31756b (diff) | |
Put conditional path information into constraint gathering so that checking uses appropriate information gleaned from pattern matching
Diffstat (limited to 'src/pretty_print.ml')
| -rw-r--r-- | src/pretty_print.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/pretty_print.ml b/src/pretty_print.ml index cfefd4d0..f0dea03f 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -357,7 +357,7 @@ let pp_def ppf d = | DEF_fundef(f_def) -> pp_fundef ppf f_def | DEF_val(lbind) -> fprintf ppf "@[<0>%a@]@\n" pp_let lbind | DEF_reg_dec(dec) -> pp_dec ppf dec - | _ -> raise (Reporting_basic.err_unreachable Unknown "initial_check didn't remove all scattered Defs") + | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "initial_check didn't remove all scattered Defs") let pp_defs ppf (Defs(defs)) = fprintf ppf "@[%a@]@\n" (list_pp pp_def pp_def) defs @@ -592,9 +592,9 @@ let pp_format_nes nes = | LtEq(_,n1,n2) -> "(Nec_lteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")" | Eq(_,n1,n2) -> "(Nec_eq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")" | GtEq(_,n1,n2) -> "(Nec_gteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")" - | In(_,i,ns) | InS(_,{nexp=Nvar i},ns) |InOpen(_,{nexp=Nvar i},ns)-> + | In(_,i,ns) | InS(_,{nexp=Nvar i},ns) -> "(Nec_in \"" ^ i ^ "\" [" ^ (list_format "; " string_of_int ns)^ "])" - | InS(_,{nexp = Nuvar _},ns) | InOpen(_,{nexp = Nuvar _},ns) -> + | InS(_,{nexp = Nuvar _},ns) -> "(Nec_in \"fresh\" [" ^ (list_format "; " string_of_int ns)^ "])" ) nes) ^*) "]" @@ -810,7 +810,7 @@ let pp_lem_def ppf d = | DEF_fundef(f_def) -> fprintf ppf "(DEF_fundef %a);" pp_lem_fundef f_def | DEF_val(lbind) -> fprintf ppf "(DEF_val %a);" pp_lem_let lbind | DEF_reg_dec(dec) -> fprintf ppf "(DEF_reg_dec %a);" pp_lem_dec dec - | _ -> raise (Reporting_basic.err_unreachable Unknown "initial_check didn't remove all scattered Defs") + | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "initial_check didn't remove all scattered Defs") let pp_lem_defs ppf (Defs(defs)) = fprintf ppf "Defs [@[%a@]]@\n" (list_pp pp_lem_def pp_lem_def) defs |