diff options
| author | Jon French | 2018-10-16 16:25:39 +0100 |
|---|---|---|
| committer | Jon French | 2018-10-16 17:03:30 +0100 |
| commit | 315fccb1b063f5ffa131b5a761fa1b2d33fa130f (patch) | |
| tree | eed4db4a25e3c1c44d7394f4749ef1612c7af105 /src/pretty_print_lem.ml | |
| parent | 45ce9105ce90efeccb9d0a183390027cdb1536af (diff) | |
| parent | 58c1292f2f5a54f069e00e4065c00936963db8cd (diff) | |
Merge branch 'sail2' into rmem_interpreter
Diffstat (limited to 'src/pretty_print_lem.ml')
| -rw-r--r-- | src/pretty_print_lem.ml | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index d7f403a4..232c3aee 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -219,7 +219,7 @@ let rec lem_nexps_of_typ (Typ_aux (t,l)) = match t with | Typ_id _ -> NexpSet.empty | Typ_var kid -> NexpSet.singleton (orig_nexp (nvar kid)) - | Typ_fn (t1,t2,_) -> NexpSet.union (trec t1) (trec t2) + | Typ_fn (t1,t2,_) -> List.fold_left NexpSet.union (trec t2) (List.map trec t1) | Typ_tup ts -> List.fold_left (fun s t -> NexpSet.union s (trec t)) NexpSet.empty ts @@ -258,15 +258,12 @@ let doc_typ_lem, doc_atomic_typ_lem = let rec typ ty = fn_typ true ty and typ' ty = fn_typ false ty and fn_typ atyp_needed ((Typ_aux (t, _)) as ty) = match t with - | Typ_fn(arg,ret,efct) -> + | Typ_fn(args,ret,efct) -> let ret_typ = if effectful efct then separate space [string "M"; fn_typ true ret] else separate space [fn_typ false ret] in - let arg_typs = match arg with - | Typ_aux (Typ_tup typs, _) -> - List.map (app_typ false) typs - | _ -> [tup_typ false arg] in + let arg_typs = List.map (app_typ false) args in let tpp = separate (space ^^ arrow ^^ space) (arg_typs @ [ret_typ]) in (* once we have proper excetions we need to know what the exceptions type is *) if atyp_needed then parens tpp else tpp @@ -443,7 +440,7 @@ let rec typeclass_nexps (Typ_aux(t,l)) = | Typ_id _ | Typ_var _ -> NexpSet.empty - | Typ_fn (t1,t2,_) -> NexpSet.union (typeclass_nexps t1) (typeclass_nexps t2) + | Typ_fn (ts,t,_) -> List.fold_left NexpSet.union (typeclass_nexps t) (List.map typeclass_nexps ts) | Typ_tup ts -> List.fold_left NexpSet.union NexpSet.empty (List.map typeclass_nexps ts) | Typ_app (Id_aux (Id "vector",_), [Typ_arg_aux (Typ_arg_nexp size_nexp,_); @@ -531,7 +528,7 @@ let rec typ_needs_printed (Typ_aux (t,_) as typ) = match t with | Typ_tup ts -> List.exists typ_needs_printed ts | Typ_app (Id_aux (Id "itself",_),_) -> true | Typ_app (_, targs) -> is_bitvector_typ typ || List.exists typ_needs_printed_arg targs - | Typ_fn (t1,t2,_) -> typ_needs_printed t1 || typ_needs_printed t2 + | Typ_fn (ts,t,_) -> List.exists typ_needs_printed ts || typ_needs_printed t | Typ_exist (kids,_,t) -> let visible_kids = KidSet.inter (KidSet.of_list kids) (lem_tyvars_of_typ t) in typ_needs_printed t && KidSet.is_empty visible_kids |