diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print.ml | 29 |
1 files changed, 15 insertions, 14 deletions
diff --git a/src/pretty_print.ml b/src/pretty_print.ml index b31838d9..2fbd81e2 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -2127,8 +2127,8 @@ let doc_typ_lem, doc_atomic_typ_lem = (* doc_lit_lem gets as an additional parameter the type information from the * expression around it: that's a hack, but how else can we distinguish between * undefined values of different types ? *) -let doc_lit_lem in_pat (L_aux(l,_)) a = - utf8string (match l with +let doc_lit_lem in_pat (L_aux(lit,l)) a = + utf8string (match lit with | L_unit -> "()" | L_zero -> "O" | L_one -> "I" @@ -2146,7 +2146,8 @@ let doc_lit_lem in_pat (L_aux(l,_)) a = | Tid "bit" | Tabbrev ({t = Tid "bit"},_) -> "Undef" | Tapp ("register",_) - | Tabbrev ({t = Tapp ("register",_)},_) -> "UndefinedReg 0") + | Tabbrev ({t = Tapp ("register",_)},_) -> "UndefinedReg 0" + | _ -> raise (Reporting_basic.err_unreachable l "undefined value of unsupported type")) | L_string s -> "\"" ^ s ^ "\"") (* typ_doc is the doc for the type being quantified *) @@ -2187,18 +2188,18 @@ let rec doc_pat_lem apat_needed regtypes (P_aux (p,(l,annot)) as pa) = match p w | _ -> parens (separate_map comma_sp (doc_pat_lem false regtypes) pats)) | P_list pats -> brackets (separate_map semi (doc_pat_lem false regtypes) pats) (*Never seen but easy in lem*) -let rec getregtyp_annot (Base ((_,t),_,_,_,_,_)) = +let rec getregtyp (LEXP_aux (le,(l,Base ((_,{t=t}),_,_,_,_,_)))) = match t with - | {t = Tabbrev ({t = Tid name},_)} -> name - -let rec getregtyp (LEXP_aux (le,(_,annot))) = match le with - | LEXP_id _ - | LEXP_cast _ -> getregtyp_annot annot - | LEXP_memory _ -> failwith "This lexp writes memory" - | LEXP_vector (le,_) - | LEXP_vector_range (le,_,_) - | LEXP_field (le,_) -> - getregtyp le + | Tabbrev ({t = Tid name},{t= Tapp ("register",_)}) -> name + | _ -> + match le with + | LEXP_id _ + | LEXP_cast _ -> raise (Reporting_basic.err_unreachable l "unsupported reg type") + | LEXP_memory _ -> failwith "This lexp writes memory" + | LEXP_vector (le,_) + | LEXP_vector_range (le,_,_) + | LEXP_field (le,_) -> + getregtyp le let doc_exp_lem, doc_let_lem = let rec top_exp (regs,(regtypes : string list)) (aexp_needed : bool) (E_aux (e, (_,annot))) = |