diff options
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 61 |
1 files changed, 42 insertions, 19 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 89ffae4b..72b9cafe 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -43,6 +43,12 @@ module Make else pr_id id + let pr_plident (lid, l) = + pr_lident lid ++ + (match l with + | Some l -> prlist_with_sep spc pr_lident l + | None -> mt()) + let string_of_fqid fqid = String.concat "." (List.map Id.to_string fqid) @@ -160,6 +166,8 @@ module Make (* This should not happen because of the grammar *) | IntValue (Some n) -> spc() ++ int n | StringValue s -> spc() ++ str s + | StringOptValue None -> mt() + | StringOptValue (Some s) -> spc() ++ str s | BoolValue b -> mt() in pr_printoption a None ++ pr_opt_value b @@ -348,6 +356,7 @@ module Make | l -> prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params pr_c p ++ str ")")) l + (* prlist_with_sep pr_semicolon (pr_params pr_c) *) @@ -387,10 +396,16 @@ module Make hov 0 (prlist_with_sep sep pr_production_item pil ++ spc() ++ str":=" ++ spc() ++ pr_raw_tactic t)) - let pr_statement head (id,(bl,c,guard)) = - assert (not (Option.is_empty id)); + let pr_univs pl = + match pl with + | None -> mt () + | Some pl -> str"@{" ++ prlist_with_sep spc pr_lident pl ++ str"}" + + let pr_statement head (idpl,(bl,c,guard)) = + assert (not (Option.is_empty idpl)); + let id, pl = Option.get idpl in hov 2 - (head ++ spc() ++ pr_lident (Option.get id) ++ spc() ++ + (head ++ spc() ++ pr_lident id ++ pr_univs pl ++ spc() ++ (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++ pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++ str":" ++ pr_spc_lconstr c) @@ -579,7 +594,8 @@ module Make let pr_goal_reference = function | OpenSubgoals -> mt () | NthGoal n -> spc () ++ int n - | GoalId n -> spc () ++ str n in + | GoalId id -> spc () ++ pr_id id + | GoalUid n -> spc () ++ str n in let pr_showable = function | ShowGoal n -> keyword "Show" ++ pr_goal_reference n | ShowGoalImplicitly n -> keyword "Show Implicit Arguments" ++ pr_opt int n @@ -627,6 +643,8 @@ module Make ) | VernacTime v -> return (keyword "Time" ++ spc() ++ pr_vernac_list v) + | VernacRedirect (s, v) -> + return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_list v) | VernacTimeout(n,v) -> return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac v) | VernacFail v -> @@ -642,11 +660,15 @@ module Make keyword (if opening then "Open " else "Close ") ++ keyword "Scope" ++ spc() ++ str sc ) - | VernacDelimiters (sc,key) -> + | VernacDelimiters (sc,Some key) -> return ( keyword "Delimit Scope" ++ spc () ++ str sc ++ spc() ++ keyword "with" ++ spc () ++ str key ) + | VernacDelimiters (sc, None) -> + return ( + keyword "Undelimit Scope" ++ spc () ++ str sc + ) | VernacBindScope (sc,cll) -> return ( keyword "Bind Scope" ++ spc () ++ str sc ++ @@ -723,7 +745,7 @@ module Make return ( hov 2 ( pr_def_token d ++ spc() - ++ pr_lident id ++ binds ++ typ + ++ pr_plident id ++ binds ++ typ ++ (match c with | None -> mt() | Some cc -> str" :=" ++ spc() ++ cc)) @@ -754,11 +776,12 @@ module Make return (hov 2 (keyword "Proof" ++ pr_lconstrarg c)) | VernacAssumption (stre,_,l) -> let n = List.length (List.flatten (List.map fst (List.map snd l))) in - return ( - hov 2 - (pr_assumption_token (n > 1) stre ++ spc() ++ - pr_ne_params_list pr_lconstr_expr l) - ) + let pr_params (c, (xl, t)) = + hov 2 (prlist_with_sep sep pr_plident xl ++ spc() ++ + (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr t)) + in + let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in + return (hov 2 (pr_assumption_token (n > 1) stre ++ spc() ++ assumptions)) | VernacInductive (p,f,l) -> let pr_constructor (coe,(id,c)) = hov 2 (pr_lident id ++ str" " ++ @@ -775,10 +798,10 @@ module Make | RecordDecl (c,fs) -> pr_record_decl b c fs in - let pr_oneind key (((coe,id),indpar,s,k,lc),ntn) = + let pr_oneind key (((coe,(id,pl)),indpar,s,k,lc),ntn) = hov 0 ( str key ++ spc() ++ - (if coe then str"> " else str"") ++ pr_lident id ++ + (if coe then str"> " else str"") ++ pr_lident id ++ pr_univs pl ++ pr_and_type_binders_arg indpar ++ spc() ++ Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++ str" :=") ++ pr_constructor_list k lc ++ @@ -802,9 +825,9 @@ module Make | None | Some Global -> "" in let pr_onerec = function - | ((loc,id),ro,bl,type_,def),ntn -> + | (((loc,id),pl),ro,bl,type_,def),ntn -> let annot = pr_guard_annot pr_lconstr_expr bl ro in - pr_id id ++ pr_binders_arg bl ++ annot + pr_id id ++ pr_univs pl ++ pr_binders_arg bl ++ annot ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_ ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++ prlist (pr_decl_notation pr_constr) ntn @@ -820,8 +843,8 @@ module Make | Some Local -> keyword "Local" ++ spc () | None | Some Global -> str "" in - let pr_onecorec (((loc,id),bl,c,def),ntn) = - pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++ + let pr_onecorec ((((loc,id),pl),bl,c,def),ntn) = + pr_id id ++ pr_univs pl ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++ spc() ++ pr_lconstr_expr c ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++ prlist (pr_decl_notation pr_constr) ntn @@ -1253,7 +1276,7 @@ module Make and pr_extend s cl = let pr_arg a = try pr_gen a - with Failure _ -> str ("<error in "^fst s^">") in + with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in try let rl = Egramml.get_extend_vernac_rule s in let start,rl,cl = @@ -1271,7 +1294,7 @@ module Make (start,cl) rl in hov 1 pp with Not_found -> - hov 1 (str ("TODO("^fst s) ++ prlist_with_sep sep pr_arg cl ++ str ")") + hov 1 (str "TODO(" ++ str (fst s) ++ prlist_with_sep sep pr_arg cl ++ str ")") in pr_vernac |