diff options
author | 2007-05-28 20:14:48 +0000 | |
---|---|---|
committer | 2007-05-28 20:14:48 +0000 | |
commit | 9443fe76a5e368257a88e49839505a395a4ed768 (patch) | |
tree | cefc755a18e6e4be1405a037a2b204bf112f9f65 /parsing/prettyp.ml | |
parent | 25ebbaf1f325cf4e3694ab379f48a269d1d83d25 (diff) |
Réaffichage des Structure/Record sous la forme Record
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9864 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/prettyp.ml')
-rw-r--r-- | parsing/prettyp.ml | 36 |
1 files changed, 35 insertions, 1 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 4d311b177..9acf697e3 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -320,11 +320,45 @@ let pr_mutual_inductive finite indl = prlist_with_sep (fun () -> fnl () ++ str" with ") print_one_inductive indl) +let get_fields = + let rec prodec_rec l subst c = + match kind_of_term c with + | Prod (na,t,c) -> + let id = match na with Name id -> id | Anonymous -> id_of_string "_" in + prodec_rec ((id,true,substl subst t)::l) (mkVar id::subst) c + | LetIn (na,b,_,c) -> + let id = match na with Name id -> id | Anonymous -> id_of_string "_" in + prodec_rec ((id,false,substl subst b)::l) (mkVar id::subst) c + | _ -> l + in + prodec_rec [] [] + +let pr_record (sp,tyi) = + let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in + let env = Global.env () in + let envpar = push_rel_context params env in + let fields = get_fields cstrtypes.(0) in + hov 0 ( + hov 0 ( + str "Record " ++ pr_global (IndRef (sp,tyi)) ++ brk(1,4) ++ + print_params env params ++ + str ": " ++ pr_lconstr_env envpar arity ++ brk(1,2) ++ + str ":= " ++ pr_id cstrnames.(0)) ++ + brk(1,2) ++ + hv 2 (str "{ " ++ + prlist_with_sep (fun () -> str "; " ++ brk(1,0)) + (fun (id,b,c) -> + pr_id id ++ str (if b then " : " else " := ") ++ + pr_lconstr_env envpar c) fields) ++ str" }") + let gallina_print_inductive sp = let (mib,mip) = Global.lookup_inductive (sp,0) in let mipv = mib.mind_packets in let names = list_tabulate (fun x -> (sp,x)) (Array.length mipv) in - pr_mutual_inductive mib.mind_finite names ++ fnl () ++ fnl () ++ + (if mib.mind_record & not !Options.raw_print then + pr_record (List.hd names) + else + pr_mutual_inductive mib.mind_finite names) ++ fnl () ++ fnl () ++ print_inductive_implicit_args sp mipv ++ print_inductive_argument_scopes sp mipv |