diff options
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 82 |
1 files changed, 39 insertions, 43 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index e88284fb1c..950246c531 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -31,12 +31,6 @@ open Decl_kinds let pr_lconstr = pr_lconstr_expr let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr - let pr_lident (loc,id) = - match loc with - | None -> pr_id id - | Some loc -> let (b,_) = Loc.unloc loc in - pr_located pr_id @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (Id.to_string id))) id - let pr_uconstraint (l, d, r) = pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ pr_glob_level r @@ -77,9 +71,8 @@ open Decl_kinds | Some loc -> let (b,_) = Loc.unloc loc in pr_located pr_fqid @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (string_of_fqid fqid))) fqid - let pr_lname = function - | (loc,Name id) -> pr_lident (loc,id) - | lna -> pr_located Name.print lna + let pr_lname_decl (n, u) = + pr_lname n ++ pr_universe_decl u let pr_smart_global = Pputils.pr_or_by_notation pr_reference @@ -91,7 +84,7 @@ open Decl_kinds let sep_end = function | VernacBullet _ - | VernacSubproof None + | VernacSubproof _ | VernacEndSubproof -> str"" | _ -> str"." @@ -398,8 +391,6 @@ open Decl_kinds ++ prlist (pr_decl_notation pr_constr) ntn let pr_statement head (idpl,(bl,c)) = - assert (not (Option.is_empty idpl)); - let idpl = Option.get idpl in hov 2 (head ++ spc() ++ pr_ident_decl idpl ++ spc() ++ (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++ @@ -535,17 +526,25 @@ open Decl_kinds | SsFwdClose e -> "("^aux e^")*" in Pp.str (aux e) - let rec pr_vernac_expr v = + let pr_extend s cl = + let pr_arg a = + try pr_gen a + with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in + try + let rl = Egramml.get_extend_vernac_rule s in + let rec aux rl cl = + match rl, cl with + | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl + | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl + | [], [] -> [] + | _ -> assert false in + hov 1 (pr_sequence identity (aux rl cl)) + with Not_found -> + hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")") + + let pr_vernac_expr v = let return = tag_vernac v in match v with - | VernacPolymorphic (poly, v) -> - let s = if poly then keyword "Polymorphic" else keyword "Monomorphic" in - return (s ++ spc () ++ pr_vernac_expr v) - | VernacProgram v -> - return (keyword "Program" ++ spc() ++ pr_vernac_expr v) - | VernacLocal (local, v) -> - return (pr_locality local ++ spc() ++ pr_vernac_expr v) - | VernacLoad (f,s) -> return ( keyword "Load" @@ -564,8 +563,6 @@ open Decl_kinds return (keyword "Unfocus") | VernacUnfocused -> return (keyword "Unfocused") - | VernacGoal c -> - return (keyword "Goal" ++ pr_lconstrarg c) | VernacAbort id -> return (keyword "Abort" ++ pr_opt pr_lident id) | VernacUndo i -> @@ -676,7 +673,10 @@ open Decl_kinds (* Gallina *) | VernacDefinition ((discharge,kind),id,b) -> (* A verifier... *) let pr_def_token dk = - keyword (Kindops.string_of_definition_object_kind dk) + keyword ( + if Name.is_anonymous (snd (fst id)) + then "Goal" + else Kindops.string_of_definition_object_kind dk) in let pr_reduce = function | None -> mt() @@ -693,12 +693,13 @@ open Decl_kinds in (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body)) | ProveBody (bl,t) -> - (pr_binders_arg bl, str" :" ++ pr_spc_lconstr t, None) in + let typ u = if snd (fst id) = Anonymous then (assert (bl = []); u) else (str" :" ++ u) in + (pr_binders_arg bl, typ (pr_spc_lconstr t), None) in let (binds,typ,c) = pr_def_body b in return ( hov 2 ( pr_def_token kind ++ spc() - ++ pr_ident_decl id ++ binds ++ typ + ++ pr_lname_decl id ++ binds ++ typ ++ (match c with | None -> mt() | Some cc -> str" :=" ++ spc() ++ cc)) @@ -1199,30 +1200,25 @@ open Decl_kinds | VernacSubproof None -> return (str "{") | VernacSubproof (Some i) -> - return (keyword "BeginSubproof" ++ spc () ++ int i) + return (Proof_bullet.pr_goal_selector i ++ str ":" ++ spc () ++ str "{") | VernacEndSubproof -> return (str "}") - and pr_extend s cl = - let pr_arg a = - try pr_gen a - with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in - try - let rl = Egramml.get_extend_vernac_rule s in - let rec aux rl cl = - match rl, cl with - | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl - | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl - | [], [] -> [] - | _ -> assert false in - hov 1 (pr_sequence identity (aux rl cl)) - with Not_found -> - hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")") +let pr_vernac_flag = + function + | VernacPolymorphic true -> keyword "Polymorphic" + | VernacPolymorphic false -> keyword "Monomorphic" + | VernacProgram -> keyword "Program" + | VernacLocal local -> pr_locality local let rec pr_vernac_control v = let return = tag_vernac v in match v with - | VernacExpr v' -> pr_vernac_expr v' ++ sep_end v' + | VernacExpr (f, v') -> + List.fold_right + (fun f a -> pr_vernac_flag f ++ spc() ++ a) + f + (pr_vernac_expr v' ++ sep_end v') | VernacTime (_,(_,v)) -> return (keyword "Time" ++ spc() ++ pr_vernac_control v) | VernacRedirect (s, (_,v)) -> |