diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 120 |
1 files changed, 74 insertions, 46 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 0608a75b..0b52155d 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -590,19 +590,6 @@ let rec doc_pat ctxt apat_needed (P_aux (p,(l,annot))) = match p with | P_cons (p,p') -> doc_op (string "::") (doc_pat ctxt true p) (doc_pat ctxt true p') | P_record (_,_) -> empty (* TODO *) -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_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 - | _ -> false -and typ_needs_printed_arg (Typ_arg_aux (targ, _)) = match targ with - | Typ_arg_typ t -> typ_needs_printed t - | _ -> false - let contains_early_return exp = let e_app (f, args) = let rets, args = List.split args in @@ -823,31 +810,40 @@ let doc_exp_lem, doc_let_lem = "Unexpected number of arguments for early_return builtin") end | _ -> - begin match annot with - | Some (env, _, _) when Env.is_union_constructor f env -> - let epp = - match args with - | [] -> doc_id_ctor f - | [arg] -> doc_id_ctor f ^^ space ^^ expV true arg - | _ -> - doc_id_ctor f ^^ space ^^ - parens (separate_map comma (expV false) args) in - if aexp_needed then parens (align epp) else epp - | _ -> - let call, is_extern = match annot with - | Some (env, _, _) when Env.is_extern f env "coq" -> - string (Env.get_extern f env "coq"), true - | _ -> doc_id f, false in - let epp = hang 2 (flow (break 1) (call :: List.map expY args)) in - let (taepp,aexp_needed) = - let env = env_of full_exp in - let t = Env.expand_synonyms env (typ_of full_exp) in - let eff = effect_of full_exp in - if typ_needs_printed t - then (align (group (prefix 0 1 epp (doc_tannot_lem ctxt env (effectful eff) t))), true) - else (epp, aexp_needed) in - liftR (if aexp_needed then parens (align taepp) else taepp) - end + let env = env_of_annot (l,annot) in + if Env.is_union_constructor f env then + let epp = + match args with + | [] -> doc_id_ctor f + | [arg] -> doc_id_ctor f ^^ space ^^ expV true arg + | _ -> + doc_id_ctor f ^^ space ^^ + parens (separate_map comma (expV false) args) in + if aexp_needed then parens (align epp) else epp + else + let call, is_extern = + if Env.is_extern f env "coq" + then string (Env.get_extern f env "coq"), true + else doc_id f, false in + let (tqs,fn_ty) = Env.get_val_spec_orig f env in + let arg_typs = match fn_ty with + | Typ_aux (Typ_fn (arg_typ,_,_),_) -> + (match arg_typ with + | Typ_aux (Typ_tup typs,_) -> typs + | _ -> [arg_typ]) + | _ -> failwith "Function not a function type" + in + (* Insert existential unpacking where necessary *) + let doc_arg arg typ_from_fn = + let arg_pp = expY arg in + (* TODO: more sophisticated check *) + match destruct_exist env (typ_of arg), destruct_exist env typ_from_fn with + | Some _, None -> parens (string "projT1 " ^^ arg_pp) + | _, _ -> arg_pp + in + (* TODO: automatically build existentials *) + let epp = hang 2 (flow (break 1) (call :: List.map2 doc_arg args arg_typs)) in + liftR (if aexp_needed then parens (align epp) else epp) end | E_vector_access (v,e) -> raise (Reporting_basic.err_unreachable l @@ -1468,6 +1464,7 @@ let doc_regtype_fields (tname, (n1, n2, fields)) = (* Remove some type variables in a similar fashion to merge_kids_atoms *) let doc_axiom_typschm typ_env (TypSchm_aux (TypSchm_ts (tqs,typ),l) as ts) = + let typ_env = add_typquant tqs typ_env in match typ with | Typ_aux (Typ_fn (args_ty, ret_ty, eff),l') -> let check_typ (args,used) typ = @@ -1508,6 +1505,37 @@ let doc_val_spec unimplemented (VS_aux (VS_val_spec(tys,id,_,_),ann)) = [string "Axiom"; doc_id id; colon; doc_axiom_typschm typ_env tys] ^^ dot) ^/^ hardline else empty (* Type signatures appear in definitions *) +(* If a top-level value is an existential type, we define the dependent pair of + the value and the proof, then just the value with Let so that it appears in + the local context when constraint solving and the ltac can find the proof. *) +let doc_val pat exp = + let (id,typpp) = match pat with + | P_aux (P_typ (typ, P_aux (P_id id,_)),_) -> id, space ^^ colon ^^ space ^^ doc_typ empty_ctxt typ + | P_aux (P_id id, _) -> id, empty + | _ -> failwith "Top-level value definition with complex pattern not supported for Coq yet" + in + let id, opt_unpack = + match destruct_exist (env_of exp) (typ_of exp) with + | None -> id, None + | Some (kids,nc,typ) -> + match drop_duplicate_atoms kids typ, nc with + | None, NC_aux (NC_true,_) -> id, None + | _ -> + (* TODO: name collisions *) + mk_id (string_of_id id ^ "_spec"), + Some (id, string_of_id id ^ "_prop") + in + let idpp = doc_id id in + let basepp = + group (string "Definition" ^^ space ^^ idpp ^^ typpp ^^ space ^^ coloneq ^^ + space ^^ doc_exp_lem empty_ctxt false exp ^^ dot) ^^ hardline + in + match opt_unpack with + | None -> basepp ^^ hardline + | Some (orig_id, hyp_id) -> + basepp ^^ + group (separate space [string "Let"; doc_id orig_id; coloneq; string "projT1"; idpp; dot]) ^^ hardline ^^ hardline + let rec doc_def unimplemented def = (* let _ = Pretty_print_sail.pp_defs stderr (Defs [def]) in *) match def with @@ -1520,14 +1548,7 @@ let rec doc_def unimplemented def = | DEF_default df -> empty | DEF_fundef fdef -> group (doc_fundef fdef) ^/^ hardline | DEF_internal_mutrec fundefs -> doc_mutrec_lem fundefs ^/^ hardline - | DEF_val (LB_aux (LB_val (pat, exp), _)) -> - let (id,typpp) = match pat with - | P_aux (P_typ (typ, P_aux (P_id id,_)),_) -> id, space ^^ colon ^^ space ^^ doc_typ empty_ctxt typ - | P_aux (P_id id, _) -> id, empty - | _ -> failwith "Top-level value definition with complex pattern not supported for Coq yet" - in - group (string "Definition" ^^ space ^^ doc_id id ^^ typpp ^^ space ^^ coloneq ^^ - doc_exp_lem empty_ctxt false exp ^^ dot) ^/^ hardline + | DEF_val (LB_aux (LB_val (pat, exp), _)) -> doc_val pat exp | DEF_scattered sdef -> failwith "doc_def: shoulnd't have DEF_scattered at this point" | DEF_kind _ -> empty @@ -1607,5 +1628,12 @@ string "Require Import String."; hardline; (fun lib -> separate space [string "Require Import";string lib] ^^ dot) defs_modules;hardline; string "Require Import List. Import ListNotations. Require Import Sumbool."; hardline; + (* Put the body into a Section so that we can define some values with + Let to put them into the local context, where tactics can see them *) + string "Section Content."; + hardline; + hardline; separate empty (List.map (doc_def unimplemented) defs); + hardline; + string "End Content."; hardline]); |