diff options
| -rw-r--r-- | src/pretty_print_coq.ml | 26 | ||||
| -rw-r--r-- | src/type_check.ml | 3 | ||||
| -rw-r--r-- | src/type_check.mli | 3 |
3 files changed, 29 insertions, 3 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 8d9dd881..6d9cbfc1 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1048,13 +1048,33 @@ let doc_exp_lem, doc_let_lem = (doc_fexp ctxt recordtyp) fexps)) in if aexp_needed then parens epp else epp | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) -> - let recordtyp = match annot with + let recordtyp, env = match annot with | Some (env, Typ_aux (Typ_id tid,_), _) | Some (env, Typ_aux (Typ_app (tid, _), _), _) when Env.is_record tid env -> - tid + tid, env | _ -> raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in - enclose_record_update (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp ctxt recordtyp) fexps)) + if List.length fexps > 1 then + let _,fields = Env.get_record recordtyp env in + let var, let_pp = + match e with + | E_aux (E_id id,_) -> id, empty + | _ -> let v = mk_id "_record" in (* TODO: collision avoid *) + v, separate space [string "let "; doc_id v; coloneq; top_exp ctxt true e; string "in"] ^^ break 1 + in + let doc_field (_,id) = + match List.find (fun (FE_aux (FE_Fexp (id',_),_)) -> Id.compare id id' == 0) fexps with + | fexp -> doc_fexp ctxt recordtyp fexp + | exception Not_found -> + let fname = + if prefix_recordtype && string_of_id recordtyp <> "regstate" + then (string (string_of_id recordtyp ^ "_")) ^^ doc_id id + else doc_id id in + doc_op coloneq fname (doc_id var ^^ dot ^^ parens fname) + in let_pp ^^ enclose_record (align (separate_map (semi_sp ^^ break 1) + doc_field fields)) + else + enclose_record_update (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp ctxt recordtyp) fexps)) | E_vector exps -> let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in let start, (len, order, etyp) = diff --git a/src/type_check.ml b/src/type_check.ml index afdf41c9..db85bf33 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -355,6 +355,7 @@ module Env : sig val is_mapping : id -> t -> bool val add_record : id -> typquant -> (typ * id) list -> t -> t val is_record : id -> t -> bool + val get_record : id -> t -> typquant * (typ * id) list val get_accessor_fn : id -> id -> t -> typquant * typ val get_accessor : id -> id -> t -> typquant * typ * typ * effect val add_local : id -> mut * typ -> t -> t @@ -917,6 +918,8 @@ end = struct let is_record id env = Bindings.mem id env.records + let get_record id env = Bindings.find id env.records + let add_record id typq fields env = if bound_typ_id env id then typ_error (id_loc id) ("Cannot create record " ^ string_of_id id ^ ", type name is already bound") diff --git a/src/type_check.mli b/src/type_check.mli index 4f87e4e6..fd1ddb92 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -136,6 +136,9 @@ module Env : sig val is_record : id -> t -> bool + (** Returns record quantifiers and fields *) + val get_record : id -> t -> typquant * (typ * id) list + (** Return type is: quantifier, argument type, return type, effect *) val get_accessor : id -> id -> t -> typquant * typ * typ * effect |