From 9468e4b49bd2f397b5e1bd2b7994cc84929fb6ac Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 27 Apr 2017 20:16:35 +0200 Subject: Fix bugs and add an option for cumulativity --- ide/texmacspp.ml | 769 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 769 insertions(+) create mode 100644 ide/texmacspp.ml (limited to 'ide') diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml new file mode 100644 index 0000000000..8409c75218 --- /dev/null +++ b/ide/texmacspp.ml @@ -0,0 +1,769 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (List.filter (fun (a,_) -> a = attr) attrs) + | _ -> []) + xml_list in + match List.flatten attrs_list with + | [] -> (attr, "") + | l -> (List.hd l) + +let backstep_loc xmllist = + let start_att = get_fst_attr_in_xml_list "begin" xmllist in + let stop_att = get_fst_attr_in_xml_list "end" (List.rev xmllist) in + [start_att ; stop_att] + +let compare_begin_att xml1 xml2 = + let att1 = get_fst_attr_in_xml_list "begin" [xml1] in + let att2 = get_fst_attr_in_xml_list "begin" [xml2] in + match att1, att2 with + | (_, s1), (_, s2) when s1 == "" || s2 == "" -> 0 + | (_, s1), (_, s2) when int_of_string s1 > int_of_string s2 -> 1 + | (_, s1), (_, s2) when int_of_string s1 < int_of_string s2 -> -1 + | _ -> 0 + +let xmlBeginSection ?loc name = xmlWithLoc ?loc "beginsection" ["name", name] [] + +let xmlEndSegment ?loc name = xmlWithLoc ?loc "endsegment" ["name", name] [] + +let xmlThm ?loc typ name xml = + xmlWithLoc ?loc "theorem" ["type", typ; "name", name] xml + +let xmlDef ?loc typ name xml = + xmlWithLoc ?loc "definition" ["type", typ; "name", name] xml + +let xmlNotation ?loc attr name xml = + xmlWithLoc ?loc "notation" (("name", name) :: attr) xml + +let xmlReservedNotation ?loc attr name = + xmlWithLoc ?loc "reservednotation" (("name", name) :: attr) [] + +let xmlCst ?loc ?(attr=[]) name = + xmlWithLoc ?loc "constant" (("name", name) :: attr) [] + +let xmlOperator ?loc ?(attr=[]) ?(pprules=[]) name = + xmlWithLoc ?loc "operator" + (("name", name) :: List.map (fun (a,b) -> "format"^a,b) pprules @ attr) [] + +let xmlApply ?loc ?(attr=[]) xml = xmlWithLoc ?loc "apply" attr xml + +let xmlToken ?loc ?(attr=[]) xml = xmlWithLoc ?loc "token" attr xml + +let xmlTyped xml = Element("typed", (backstep_loc xml), xml) + +let xmlReturn ?(attr=[]) xml = Element("return", attr, xml) + +let xmlCase xml = Element("case", [], xml) + +let xmlScrutinee ?(attr=[]) xml = Element("scrutinee", attr, xml) + +let xmlWith xml = Element("with", [], xml) + +let xmlAssign id xml = Element("assign", ["target",string_of_id id], [xml]) + +let xmlInductive ?loc kind xml = xmlWithLoc ?loc "inductive" ["kind",kind] xml + +let xmlCoFixpoint xml = Element("cofixpoint", [], xml) + +let xmlFixpoint xml = Element("fixpoint", [], xml) + +let xmlCheck ?loc xml = xmlWithLoc ?loc "check" [] xml + +let xmlAssumption ?loc kind xml = xmlWithLoc ?loc "assumption" ["kind",kind] xml + +let xmlComment ?loc xml = xmlWithLoc ?loc "comment" [] xml + +let xmlCanonicalStructure ?loc attr = xmlWithLoc ?loc "canonicalstructure" attr [] + +let xmlQed ?loc ?(attr=[]) = xmlWithLoc ?loc "qed" attr [] + +let xmlPatvar ?loc id = xmlWithLoc ?loc "patvar" ["id", id] [] + +let xmlReference ref = + let name = Libnames.string_of_reference ref in + let i, j = Option.cata Loc.unloc (0,0) (Libnames.loc_of_reference ref) in + let b, e = string_of_int i, string_of_int j in + Element("reference",["name", name; "begin", b; "end", e] ,[]) + +let xmlRequire ?loc ?(attr=[]) xml = xmlWithLoc ?loc "require" attr xml +let xmlImport ?loc ?(attr=[]) xml = xmlWithLoc ?loc "import" attr xml + +let xmlAddLoadPath ?loc ?(attr=[]) xml = xmlWithLoc ?loc "addloadpath" attr xml +let xmlRemoveLoadPath ?loc ?(attr=[]) = xmlWithLoc ?loc "removeloadpath" attr +let xmlAddMLPath ?loc ?(attr=[]) = xmlWithLoc ?loc "addmlpath" attr + +let xmlExtend ?loc xml = xmlWithLoc ?loc "extend" [] xml + +let xmlScope ?loc ?(attr=[]) action name xml = + xmlWithLoc ?loc "scope" (["name",name;"action",action] @ attr) xml + +let xmlProofMode ?loc name = xmlWithLoc ?loc "proofmode" ["name",name] [] + +let xmlProof ?loc xml = xmlWithLoc ?loc "proof" [] xml + +let xmlSectionSubsetDescr name ssd = + Element("sectionsubsetdescr",["name",name], + [PCData (Proof_using.to_string ssd)]) + +let xmlDeclareMLModule ?loc s = + xmlWithLoc ?loc "declarexmlmodule" [] + (List.map (fun x -> Element("path",["value",x],[])) s) + +(* tactics *) +let xmlLtac ?loc xml = xmlWithLoc ?loc "ltac" [] xml + +(* toplevel commands *) +let xmlGallina ?loc xml = xmlWithLoc ?loc "gallina" [] xml + +let xmlTODO ?loc x = + xmlWithLoc ?loc "todo" [] [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] + +let string_of_name n = + match n with + | Anonymous -> "_" + | Name id -> Id.to_string id + +let string_of_glob_sort s = + match s with + | GProp -> "Prop" + | GSet -> "Set" + | GType _ -> "Type" + +let string_of_cast_sort c = + match c with + | CastConv _ -> "CastConv" + | CastVM _ -> "CastVM" + | CastNative _ -> "CastNative" + | CastCoerce -> "CastCoerce" + +let string_of_case_style s = + match s with + | LetStyle -> "Let" + | IfStyle -> "If" + | LetPatternStyle -> "LetPattern" + | MatchStyle -> "Match" + | RegularStyle -> "Regular" + +let attribute_of_syntax_modifier sm = +match sm with + | SetItemLevel (sl, NumLevel n) -> + List.map (fun s -> ("itemlevel", s)) sl @ ["level", string_of_int n] + | SetItemLevel (sl, NextLevel) -> + List.map (fun s -> ("itemlevel", s)) sl @ ["level", "next"] + | SetLevel i -> ["level", string_of_int i] + | SetAssoc a -> + begin match a with + | NonA -> ["",""] + | RightA -> ["associativity", "right"] + | LeftA -> ["associativity", "left"] + end + | SetEntryType (s, _) -> ["entrytype", s] + | SetOnlyPrinting -> ["onlyprinting", ""] + | SetOnlyParsing -> ["onlyparsing", ""] + | SetCompatVersion v -> ["compat", Flags.pr_version v] + | SetFormat (system, (loc, s)) -> + let start, stop = unlock ?loc in + ["format-"^system, s; "begin", start; "end", stop] + +let string_of_assumption_kind l a many = + match l, a, many with + | (Discharge, Logical, true) -> "Hypotheses" + | (Discharge, Logical, false) -> "Hypothesis" + | (Discharge, Definitional, true) -> "Variables" + | (Discharge, Definitional, false) -> "Variable" + | (Global, Logical, true) -> "Axioms" + | (Global, Logical, false) -> "Axiom" + | (Global, Definitional, true) -> "Parameters" + | (Global, Definitional, false) -> "Parameter" + | (Local, Logical, true) -> "Local Axioms" + | (Local, Logical, false) -> "Local Axiom" + | (Local, Definitional, true) -> "Local Parameters" + | (Local, Definitional, false) -> "Local Parameter" + | (Global, Conjectural, _) -> "Conjecture" + | ((Discharge | Local), Conjectural, _) -> assert false + +let rec pp_bindlist bl = + let tlist = + List.flatten + (List.map + (fun (loc_names, _, e) -> + let names = + (List.map + (fun (loc, name) -> + xmlCst ?loc (string_of_name name)) loc_names) in + match e.CAst.v with + | CHole _ -> names + | _ -> names @ [pp_expr e]) + bl) in + match tlist with + | [e] -> e + | l -> xmlTyped l +and pp_decl_notation ((_, s), ce, sc) = (* don't know what it is for now *) + Element ("decl_notation", ["name", s], [pp_expr ce]) +and pp_local_binder lb = (* don't know what it is for now *) + match lb with + | CLocalDef ((loc, nam), ce, ty) -> + let attrs = ["name", string_of_name nam] in + let value = match ty with + Some t -> CAst.make ?loc:(Loc.merge_opt (constr_loc ce) (constr_loc t)) @@ CCast (ce, CastConv t) + | None -> ce in + pp_expr ~attr:attrs value + | CLocalAssum (namll, _, ce) -> + let ppl = + List.map (fun (loc, nam) -> (xmlCst ?loc (string_of_name nam))) namll in + xmlTyped (ppl @ [pp_expr ce]) + | CLocalPattern _ -> + assert false +and pp_local_decl_expr lde = (* don't know what it is for now *) + match lde with + | AssumExpr (_, ce) -> pp_expr ce + | DefExpr (_, ce, _) -> pp_expr ce +and pp_inductive_expr ((_, ((l, id),_)), lbl, ceo, _, cl_or_rdexpr) = + (* inductive_expr *) + let b,e = Option.cata Loc.unloc (0,0) l in + let location = ["begin", string_of_int b; "end", string_of_int e] in + [Element ("lident", ["name", Id.to_string id] @ location, [])] @ (* inductive name *) + begin match cl_or_rdexpr with + | Constructors coel -> List.map (fun (_, (_, ce)) -> pp_expr ce) coel + | RecordDecl (_, ldewwwl) -> + List.map (fun (((_, x), _), _) -> pp_local_decl_expr x) ldewwwl + end @ + begin match ceo with (* don't know what it is for now *) + | Some ce -> [pp_expr ce] + | None -> [] + end @ + (List.map pp_local_binder lbl) +and pp_recursion_order_expr optid roe = (* don't know what it is for now *) + let attrs = + match optid with + | None -> [] + | Some (loc, id) -> + let start, stop = unlock ?loc in + ["begin", start; "end", stop ; "name", Id.to_string id] in + let kind, expr = + match roe with + | CStructRec -> "struct", [] + | CWfRec e -> "rec", [pp_expr e] + | CMeasureRec (e, None) -> "mesrec", [pp_expr e] + | CMeasureRec (e, Some rel) -> "mesrec", [pp_expr e] @ [pp_expr rel] in + Element ("recursion_order", ["kind", kind] @ attrs, expr) +and pp_fixpoint_expr (((loc, id), pl), (optid, roe), lbl, ce, ceo) = + (* fixpoint_expr *) + let start, stop = unlock ?loc in + let id = Id.to_string id in + [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @ + (* fixpoint name *) + [pp_recursion_order_expr optid roe] @ + (List.map pp_local_binder lbl) @ + [pp_expr ce] @ + begin match ceo with (* don't know what it is for now *) + | Some ce -> [pp_expr ce] + | None -> [] + end +and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *) + (* Nota: it is like fixpoint_expr without (optid, roe) + * so could be merged if there is no more differences *) + let start, stop = unlock ?loc in + let id = Id.to_string id in + [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @ + (* cofixpoint name *) + (List.map pp_local_binder lbl) @ + [pp_expr ce] @ + begin match ceo with (* don't know what it is for now *) + | Some ce -> [pp_expr ce] + | None -> [] + end +and pp_lident (loc, id) = xmlCst ?loc (Id.to_string id) +and pp_simple_binder (idl, ce) = List.map pp_lident idl @ [pp_expr ce] +and pp_cases_pattern_expr {loc ; CAst.v = cpe} = + match cpe with + | CPatAlias (cpe, id) -> + xmlApply ?loc + (xmlOperator ?loc ~attr:["name", string_of_id id] "alias" :: + [pp_cases_pattern_expr cpe]) + | CPatCstr (ref, None, cpel2) -> + xmlApply ?loc + (xmlOperator ?loc "reference" + ~attr:["name", Libnames.string_of_reference ref] :: + [Element ("impargs", [], []); + Element ("args", [], (List.map pp_cases_pattern_expr cpel2))]) + | CPatCstr (ref, Some cpel1, cpel2) -> + xmlApply ?loc + (xmlOperator ?loc "reference" + ~attr:["name", Libnames.string_of_reference ref] :: + [Element ("impargs", [], (List.map pp_cases_pattern_expr cpel1)); + Element ("args", [], (List.map pp_cases_pattern_expr cpel2))]) + | CPatAtom optr -> + let attrs = match optr with + | None -> [] + | Some r -> ["name", Libnames.string_of_reference r] in + xmlApply ?loc (xmlOperator ?loc "atom" ~attr:attrs :: []) + | CPatOr cpel -> + xmlApply ?loc (xmlOperator ?loc "or" :: List.map pp_cases_pattern_expr cpel) + | CPatNotation (n, (subst_constr, subst_rec), cpel) -> + xmlApply ?loc + (xmlOperator ?loc "notation" :: + [xmlOperator ?loc n; + Element ("subst", [], + [Element ("subterms", [], + List.map pp_cases_pattern_expr subst_constr); + Element ("recsubterms", [], + List.map + (fun (cpel) -> + Element ("recsubterm", [], + List.map pp_cases_pattern_expr cpel)) + subst_rec)]); + Element ("args", [], (List.map pp_cases_pattern_expr cpel))]) + | CPatPrim tok -> pp_token ?loc tok + | CPatRecord rcl -> + xmlApply ?loc + (xmlOperator ?loc "record" :: + List.map (fun (r, cpe) -> + Element ("field", + ["reference", Libnames.string_of_reference r], + [pp_cases_pattern_expr cpe])) + rcl) + | CPatDelimiters (delim, cpe) -> + xmlApply ?loc + (xmlOperator ?loc "delimiter" ~attr:["name", delim] :: + [pp_cases_pattern_expr cpe]) + | CPatCast _ -> assert false +and pp_case_expr (e, name, pat) = + match name, pat with + | None, None -> xmlScrutinee [pp_expr e] + | Some (loc, name), None -> + let start, stop= unlock ?loc in + xmlScrutinee ~attr:["name", string_of_name name; + "begin", start; "end", stop] [pp_expr e] + | Some (loc, name), Some p -> + let start, stop= unlock ?loc in + xmlScrutinee ~attr:["name", string_of_name name; + "begin", start; "end", stop] + [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e] + | None, Some p -> + xmlScrutinee [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e] +and pp_branch_expr_list bel = + xmlWith + (List.map + (fun (_, (cpel, e)) -> + let ppcepl = + List.map pp_cases_pattern_expr (List.flatten (List.map snd cpel)) in + let ppe = [pp_expr e] in + xmlCase (ppcepl @ ppe)) + bel) +and pp_token ?loc tok = + let tokstr = + match tok with + | String s -> PCData s + | Numeral n -> PCData (to_string n) in + xmlToken ?loc [tokstr] +and pp_local_binder_list lbl = + let l = (List.map pp_local_binder lbl) in + Element ("recurse", (backstep_loc l), l) +and pp_const_expr_list cel = + let l = List.map pp_expr cel in + Element ("recurse", (backstep_loc l), l) +and pp_expr ?(attr=[]) { loc; CAst.v = e } = + match e with + | CRef (r, _) -> + xmlCst ?loc:(Libnames.loc_of_reference r) ~attr (Libnames.string_of_reference r) + | CProdN (bl, e) -> + xmlApply ?loc + (xmlOperator ?loc "forall" :: [pp_bindlist bl] @ [pp_expr e]) + | CApp ((_, hd), args) -> + xmlApply ?loc ~attr (pp_expr hd :: List.map (fun (e,_) -> pp_expr e) args) + | CAppExpl ((_, r, _), args) -> + xmlApply ?loc ~attr + (xmlCst ?loc:(Libnames.loc_of_reference r) (Libnames.string_of_reference r) + :: List.map pp_expr args) + | CNotation (notation, ([],[],[])) -> + xmlOperator ?loc notation + | CNotation (notation, (args, cell, lbll)) -> + let fmts = Notation.find_notation_extra_printing_rules notation in + let oper = xmlOperator ?loc notation ~pprules:fmts in + let cels = List.map pp_const_expr_list cell in + let lbls = List.map pp_local_binder_list lbll in + let args = List.map pp_expr args in + xmlApply ?loc (oper :: (List.sort compare_begin_att (args @ cels @ lbls))) + | CSort(s) -> + xmlOperator ?loc (string_of_glob_sort s) + | CDelimiters (scope, ce) -> + xmlApply ?loc (xmlOperator ?loc "delimiter" ~attr:["name", scope] :: + [pp_expr ce]) + | CPrim tok -> pp_token ?loc tok + | CGeneralization (kind, _, e) -> + let kind= match kind with + | Explicit -> "explicit" + | Implicit -> "implicit" in + xmlApply ?loc + (xmlOperator ?loc ~attr:["kind", kind] "generalization" :: [pp_expr e]) + | CCast (e, tc) -> + begin match tc with + | CastConv t | CastVM t |CastNative t -> + xmlApply ?loc + (xmlOperator ?loc ":" ~attr:["kind", (string_of_cast_sort tc)] :: + [pp_expr e; pp_expr t]) + | CastCoerce -> + xmlApply ?loc + (xmlOperator ?loc ":" ~attr:["kind", "CastCoerce"] :: + [pp_expr e]) + end + | CEvar (ek, cel) -> + let ppcel = List.map (fun (id,e) -> xmlAssign id (pp_expr e)) cel in + xmlApply ?loc + (xmlOperator ?loc "evar" ~attr:["id", string_of_id ek] :: + ppcel) + | CPatVar id -> xmlPatvar ?loc (string_of_id id) + | CHole (_, _, _) -> xmlCst ?loc ~attr "_" + | CIf (test, (_, ret), th, el) -> + let return = match ret with + | None -> [] + | Some r -> [xmlReturn [pp_expr r]] in + xmlApply ?loc + (xmlOperator ?loc "if" :: + return @ [pp_expr th] @ [pp_expr el]) + | CLetTuple (names, (_, ret), value, body) -> + let return = match ret with + | None -> [] + | Some r -> [xmlReturn [pp_expr r]] in + xmlApply ?loc + (xmlOperator ?loc "lettuple" :: + return @ + (List.map (fun (loc, var) -> xmlCst ?loc (string_of_name var)) names) @ + [pp_expr value; pp_expr body]) + | CCases (sty, ret, cel, bel) -> + let return = match ret with + | None -> [] + | Some r -> [xmlReturn [pp_expr r]] in + xmlApply ?loc + (xmlOperator ?loc ~attr:["style", (string_of_case_style sty)] "match" :: + (return @ + [Element ("scrutinees", [], List.map pp_case_expr cel)] @ + [pp_branch_expr_list bel])) + | CRecord _ -> assert false + | CLetIn ((varloc, var), value, typ, body) -> + let value = match typ with + | Some t -> + CAst.make ?loc:(Loc.merge_opt (constr_loc value) (constr_loc t)) (CCast (value, CastConv t)) + | None -> value in + xmlApply ?loc + (xmlOperator ?loc "let" :: + [xmlCst ?loc:varloc (string_of_name var) ; pp_expr value; pp_expr body]) + | CLambdaN (bl, e) -> + xmlApply ?loc + (xmlOperator ?loc "lambda" :: [pp_bindlist bl] @ [pp_expr e]) + | CCoFix (_, _) -> assert false + | CFix (lid, fel) -> + xmlApply ?loc + (xmlOperator ?loc "fix" :: + List.flatten (List.map + (fun (a,b,cl,c,d) -> pp_fixpoint_expr ((a,None),b,cl,c,Some d)) + fel)) + +let pp_comment c = + match c with + | CommentConstr e -> [pp_expr e] + | CommentString s -> [Element ("string", [], [PCData s])] + | CommentInt i -> [PCData (string_of_int i)] + +let rec tmpp ?loc v = + match v with + (* Control *) + | VernacLoad (verbose,f) -> + xmlWithLoc ?loc "load" ["verbose",string_of_bool verbose;"file",f] [] + | VernacTime (loc,e) -> + xmlApply ?loc (Element("time",[],[]) :: + [tmpp ?loc e]) + | VernacRedirect (s, (loc,e)) -> + xmlApply ?loc (Element("redirect",["path", s],[]) :: + [tmpp ?loc e]) + | VernacTimeout (s,e) -> + xmlApply ?loc (Element("timeout",["val",string_of_int s],[]) :: + [tmpp ?loc e]) + | VernacFail e -> xmlApply ?loc (Element("fail",[],[]) :: [tmpp ?loc e]) + + (* Syntax *) + | VernacSyntaxExtension (_, ((_, name), sml)) -> + let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in + xmlReservedNotation ?loc attrs name + + | VernacOpenCloseScope (_,(true,name)) -> xmlScope ?loc "open" name [] + | VernacOpenCloseScope (_,(false,name)) -> xmlScope ?loc "close" name [] + | VernacDelimiters (name,Some tag) -> + xmlScope ?loc "delimit" name ~attr:["delimiter",tag] [] + | VernacDelimiters (name,None) -> + xmlScope ?loc "undelimit" name ~attr:[] [] + | VernacInfix (_,((_,name),sml),ce,sn) -> + let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in + let sc_attr = + match sn with + | Some scope -> ["scope", scope] + | None -> [] in + xmlNotation ?loc (sc_attr @ attrs) name [pp_expr ce] + | VernacNotation (_, ce, (lstr, sml), sn) -> + let name = snd lstr in + let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in + let sc_attr = + match sn with + | Some scope -> ["scope", scope] + | None -> [] in + xmlNotation ?loc (sc_attr @ attrs) name [pp_expr ce] + | VernacBindScope _ as x -> xmlTODO ?loc x + | VernacNotationAddFormat _ as x -> xmlTODO ?loc x + | VernacUniverse _ + | VernacConstraint _ + | VernacPolymorphic (_, _) as x -> xmlTODO ?loc x + (* Gallina *) + | VernacDefinition (ldk, ((_,id),_), de) -> + let l, dk = + match ldk with + | Some l, dk -> (l, dk) + | None, dk -> (Global, dk) in (* Like in ppvernac.ml, l 585 *) + let e = + match de with + | ProveBody (_, ce) -> ce + | DefineBody (_, Some _, ce, None) -> ce + | DefineBody (_, None , ce, None) -> ce + | DefineBody (_, Some _, ce, Some _) -> ce + | DefineBody (_, None , ce, Some _) -> ce in + let str_dk = Kindops.string_of_definition_kind (l, false, dk) in + let str_id = Id.to_string id in + (xmlDef ?loc str_dk str_id [pp_expr e]) + | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) -> + let str_tk = Kindops.string_of_theorem_kind tk in + let str_id = Id.to_string id in + (xmlThm ?loc str_tk str_id [pp_expr statement]) + | VernacStartTheoremProof _ as x -> xmlTODO ?loc x + | VernacEndProof pe -> + begin + match pe with + | Admitted -> xmlQed ?loc ?attr:None + | Proved (_, Some ((_, id), Some tk)) -> + let nam = Id.to_string id in + let typ = Kindops.string_of_theorem_kind tk in + xmlQed ?loc ~attr:["name", nam; "type", typ] + | Proved (_, Some ((_, id), None)) -> + let nam = Id.to_string id in + xmlQed ?loc ~attr:["name", nam] + | Proved _ -> xmlQed ?loc ?attr:None + end + | VernacExactProof _ as x -> xmlTODO ?loc x + | VernacAssumption ((l, a), _, sbwcl) -> + let binders = List.map (fun (_, (id, c)) -> (List.map fst id, c)) sbwcl in + let many = + List.length (List.flatten (List.map fst binders)) > 1 in + let exprs = + List.flatten (List.map pp_simple_binder binders) in + let l = match l with Some x -> x | None -> Decl_kinds.Global in + let kind = string_of_assumption_kind l a many in + xmlAssumption ?loc kind exprs + | VernacInductive (_, _, _, iednll) -> + let kind = + let (_, _, _, k, _), _ = List.hd iednll in + begin + match k with + | Record -> "Record" + | Structure -> "Structure" + | Inductive_kw -> "Inductive" + | CoInductive -> "CoInductive" + | Class _ -> "Class" + | Variant -> "Variant" + end in + let exprs = + List.flatten (* should probably not be flattened *) + (List.map + (fun (ie, dnl) -> (pp_inductive_expr ie) @ + (List.map pp_decl_notation dnl)) iednll) in + xmlInductive ?loc kind exprs + | VernacFixpoint (_, fednll) -> + let exprs = + List.flatten (* should probably not be flattened *) + (List.map + (fun (fe, dnl) -> (pp_fixpoint_expr fe) @ + (List.map pp_decl_notation dnl)) fednll) in + xmlFixpoint exprs + | VernacCoFixpoint (_, cfednll) -> + (* Nota: it is like VernacFixpoint without so could be merged *) + let exprs = + List.flatten (* should probably not be flattened *) + (List.map + (fun (cfe, dnl) -> (pp_cofixpoint_expr cfe) @ + (List.map pp_decl_notation dnl)) cfednll) in + xmlCoFixpoint exprs + | VernacScheme _ as x -> xmlTODO ?loc x + | VernacCombinedScheme _ as x -> xmlTODO ?loc x + + (* Gallina extensions *) + | VernacBeginSection (_, id) -> xmlBeginSection ?loc (Id.to_string id) + | VernacEndSegment (_, id) -> xmlEndSegment ?loc (Id.to_string id) + | VernacNameSectionHypSet _ as x -> xmlTODO ?loc x + | VernacRequire (from, import, l) -> + let import = match import with + | None -> [] + | Some true -> ["export","true"] + | Some false -> ["import","true"] + in + let from = match from with + | None -> [] + | Some r -> ["from", Libnames.string_of_reference r] + in + xmlRequire ?loc ~attr:(from @ import) (List.map (fun ref -> + xmlReference ref) l) + | VernacImport (true,l) -> + xmlImport ?loc ~attr:["export","true"] (List.map (fun ref -> + xmlReference ref) l) + | VernacImport (false,l) -> + xmlImport ?loc (List.map (fun ref -> xmlReference ref) l) + | VernacCanonical r -> + let attr = + match r with + | AN (Qualid (_, q)) -> ["qualid", string_of_qualid q] + | AN (Ident (_, id)) -> ["id", Id.to_string id] + | ByNotation (_, (s, _)) -> ["notation", s] in + xmlCanonicalStructure ?loc attr + | VernacCoercion _ as x -> xmlTODO ?loc x + | VernacIdentityCoercion _ as x -> xmlTODO ?loc x + + (* Type classes *) + | VernacInstance _ as x -> xmlTODO ?loc x + + | VernacContext _ as x -> xmlTODO ?loc x + + | VernacDeclareInstances _ as x -> xmlTODO ?loc x + + | VernacDeclareClass _ as x -> xmlTODO ?loc x + + (* Modules and Module Types *) + | VernacDeclareModule _ as x -> xmlTODO ?loc x + | VernacDefineModule _ as x -> xmlTODO ?loc x + | VernacDeclareModuleType _ as x -> xmlTODO ?loc x + | VernacInclude _ as x -> xmlTODO ?loc x + + (* Solving *) + + | (VernacSolveExistential _) as x -> + xmlLtac ?loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] + + (* Auxiliary file and library management *) + | VernacAddLoadPath (recf,name,None) -> + xmlAddLoadPath ?loc ~attr:["rec",string_of_bool recf;"path",name] [] + | VernacAddLoadPath (recf,name,Some dp) -> + xmlAddLoadPath ?loc ~attr:["rec",string_of_bool recf;"path",name] + [PCData (Names.DirPath.to_string dp)] + | VernacRemoveLoadPath name -> xmlRemoveLoadPath ?loc ~attr:["path",name] [] + | VernacAddMLPath (recf,name) -> + xmlAddMLPath ?loc ~attr:["rec",string_of_bool recf;"path",name] [] + | VernacDeclareMLModule sl -> xmlDeclareMLModule ?loc sl + | VernacChdir _ as x -> xmlTODO ?loc x + + (* State management *) + | VernacWriteState _ as x -> xmlTODO ?loc x + | VernacRestoreState _ as x -> xmlTODO ?loc x + + (* Resetting *) + | VernacResetName _ as x -> xmlTODO ?loc x + | VernacResetInitial as x -> xmlTODO ?loc x + | VernacBack _ as x -> xmlTODO ?loc x + | VernacBackTo _ -> PCData "VernacBackTo" + + (* Commands *) + | VernacCreateHintDb _ as x -> xmlTODO ?loc x + | VernacRemoveHints _ as x -> xmlTODO ?loc x + | VernacHints _ as x -> xmlTODO ?loc x + | VernacSyntacticDefinition ((_, name), (idl, ce), _, _) -> + let name = Id.to_string name in + let attrs = List.map (fun id -> ("id", Id.to_string id)) idl in + xmlNotation ?loc attrs name [pp_expr ce] + | VernacDeclareImplicits _ as x -> xmlTODO ?loc x + | VernacArguments _ as x -> xmlTODO ?loc x + | VernacArgumentsScope _ as x -> xmlTODO ?loc x + | VernacReserve _ as x -> xmlTODO ?loc x + | VernacGeneralizable _ as x -> xmlTODO ?loc x + | VernacSetOpacity _ as x -> xmlTODO ?loc x + | VernacSetStrategy _ as x -> xmlTODO ?loc x + | VernacUnsetOption _ as x -> xmlTODO ?loc x + | VernacSetOption _ as x -> xmlTODO ?loc x + | VernacSetAppendOption _ as x -> xmlTODO ?loc x + | VernacAddOption _ as x -> xmlTODO ?loc x + | VernacRemoveOption _ as x -> xmlTODO ?loc x + | VernacMemOption _ as x -> xmlTODO ?loc x + | VernacPrintOption _ as x -> xmlTODO ?loc x + | VernacCheckMayEval (_,_,e) -> xmlCheck ?loc [pp_expr e] + | VernacGlobalCheck _ as x -> xmlTODO ?loc x + | VernacDeclareReduction _ as x -> xmlTODO ?loc x + | VernacPrint _ as x -> xmlTODO ?loc x + | VernacSearch _ as x -> xmlTODO ?loc x + | VernacLocate _ as x -> xmlTODO ?loc x + | VernacRegister _ as x -> xmlTODO ?loc x + | VernacComments (cl) -> + xmlComment ?loc (List.flatten (List.map pp_comment cl)) + + (* Stm backdoor *) + | VernacStm _ as x -> xmlTODO ?loc x + + (* Proof management *) + | VernacGoal _ as x -> xmlTODO ?loc x + | VernacAbort _ as x -> xmlTODO ?loc x + | VernacAbortAll -> PCData "VernacAbortAll" + | VernacRestart as x -> xmlTODO ?loc x + | VernacUndo _ as x -> xmlTODO ?loc x + | VernacUndoTo _ as x -> xmlTODO ?loc x + | VernacBacktrack _ as x -> xmlTODO ?loc x + | VernacFocus _ as x -> xmlTODO ?loc x + | VernacUnfocus as x -> xmlTODO ?loc x + | VernacUnfocused as x -> xmlTODO ?loc x + | VernacBullet _ as x -> xmlTODO ?loc x + | VernacSubproof _ as x -> xmlTODO ?loc x + | VernacEndSubproof as x -> xmlTODO ?loc x + | VernacShow _ as x -> xmlTODO ?loc x + | VernacCheckGuard as x -> xmlTODO ?loc x + | VernacProof (tac,using) -> + let tac = None (** FIXME *) in + let using = Option.map (xmlSectionSubsetDescr "using") using in + xmlProof ?loc (Option.List.(cons tac (cons using []))) + | VernacProofMode name -> xmlProofMode ?loc name + + (* Toplevel control *) + | VernacToplevelControl _ as x -> xmlTODO ?loc x + + (* For extension *) + | VernacExtend _ as x -> + xmlExtend ?loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] + + (* Flags *) + | VernacProgram e -> xmlApply ?loc (Element("program",[],[]) :: [tmpp ?loc e]) + | VernacLocal (b,e) -> + xmlApply ?loc (Element("local",["flag",string_of_bool b],[]) :: + [tmpp ?loc e]) + +let tmpp ?loc v = + match tmpp ?loc v with + | Element("ltac",_,_) as x -> x + | xml -> xmlGallina ?loc [xml] -- cgit v1.2.3 From 11c52f0882b39afe853473f7a9289e62d1ca843a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 15 Jun 2017 12:36:54 +0200 Subject: [ide] Better exn printing. [fixes BZ#5524] Due to the situation explained in bug 5360, error printing in ide_slave results in an anomaly. We fix that by properly processing the error. This fixes BZ#5524, however BZ#5525 , still applies. --- ide/ide_slave.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'ide') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 9c771cbef1..6298d9f093 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -341,6 +341,7 @@ let about () = { } let handle_exn (e, info) = + let (e, info) = ExplainErr.process_vernac_interp_error (e, info) in let dummy = Stateid.dummy in let loc_of e = match Loc.get_loc e with | Some loc -> Some (Loc.unloc loc) -- cgit v1.2.3 From d8874dd855d748aaaf504890487ab15ffd7a677d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 12 Jun 2017 11:41:40 +0200 Subject: [ide] Add route_id parameter to query call. This is necessary in order for clients to identify the results of queries. This is a minor breaking change of the protocol, affecting only this particular call. This change is necessary in order to fix bug ####. --- ide/coqOps.ml | 10 +++++----- ide/ide_slave.ml | 4 ++-- ide/interface.mli | 5 +++-- ide/xmlprotocol.ml | 20 +++++++++++++++++--- 4 files changed, 27 insertions(+), 12 deletions(-) (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index d30d7ab5e0..3a869f69af 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -373,7 +373,8 @@ object(self) else messages#add s; in let query = - Coq.query (phrase,sid) in + let route_id = 0 in + Coq.query (route_id,(phrase,sid)) in let next = function | Fail (_, _, err) -> display_error err; Coq.return () | Good msg -> Coq.return () @@ -841,15 +842,14 @@ object(self) in let try_phrase phrase stop more = let action = log "Sending to coq now" in - let query = Coq.query (phrase,Stateid.dummy) in + let route_id = 0 in + let query = Coq.query (route_id,(phrase,Stateid.dummy)) in let next = function | Fail (_, l, str) -> (* FIXME: check *) display_error (l, str); messages#add (Pp.str ("Unsuccessfully tried: "^phrase)); more - | Good msg -> - messages#add_string msg; - stop Tags.Script.processed + | Good () -> stop Tags.Script.processed in Coq.bind (Coq.seq action query) next in diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 9c771cbef1..7cb22aa33f 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -109,9 +109,9 @@ let edit_at id = * as not to break the core protocol for this minor change, but it should * be removed in the next version of the protocol. *) -let query (s,id) = +let query (route, (s,id)) = let pa = Pcoq.Gram.parsable (Stream.of_string s) in - Stm.query ~at:id pa; "" + Stm.query ~at:id ~route pa let annotate phrase = let (loc, ast) = diff --git a/ide/interface.mli b/ide/interface.mli index 62f63aefb9..1a4d6c0ecb 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -112,6 +112,7 @@ type coq_info = { type location = (int * int) option (* start and end of the error *) type state_id = Stateid.t +type route_id = Feedback.route_id (* Obsolete *) type edit_id = int @@ -154,8 +155,8 @@ type edit_at_rty = (unit, state_id * (state_id * state_id)) union has been deprecated in favor of sending the query answers as feedback. It will be removed in a future version of the protocol. *) -type query_sty = string * state_id -type query_rty = string +type query_sty = route_id * (string * state_id) +type query_rty = unit (** Fetching the list of current goals. Return [None] if no proof is in progress, [Some gl] otherwise. *) diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 53eb1a95ff..d42bfe43dd 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -10,7 +10,7 @@ (** WARNING: TO BE UPDATED WHEN MODIFIED! *) -let protocol_version = "20150913" +let protocol_version = "20170413" type msg_format = Richpp of int | Ppcmds let msg_format = ref (Richpp 72) @@ -95,6 +95,13 @@ let to_stateid = function let of_stateid i = Element ("state_id",["val",string_of_int (Stateid.to_int i)],[]) +let to_routeid = function + | Element ("route_id",["val",i],[]) -> + let id = int_of_string i in id + | _ -> raise (Invalid_argument "to_route_id") + +let of_routeid i = Element ("route_id",["val",string_of_int i],[]) + let of_box (ppb : Pp.block_type) = let open Pp in match ppb with | Pp_hbox i -> constructor "ppbox" "hbox" [of_int i] | Pp_vbox i -> constructor "ppbox" "vbox" [of_int i] @@ -269,6 +276,7 @@ module ReifType : sig val coq_info_t : coq_info val_t val coq_object_t : 'a val_t -> 'a coq_object val_t val state_id_t : state_id val_t + val route_id_t : route_id val_t val search_cst_t : search_constraint val_t val of_value_type : 'a val_t -> 'a -> xml @@ -304,6 +312,7 @@ end = struct | Coq_info : coq_info val_t | Coq_object : 'a val_t -> 'a coq_object val_t | State_id : state_id val_t + | Route_id : route_id val_t | Search_cst : search_constraint val_t type value_type = Value_type : 'a val_t -> value_type @@ -329,6 +338,7 @@ end = struct let coq_info_t = Coq_info let coq_object_t x = Coq_object x let state_id_t = State_id + let route_id_t = Route_id let search_cst_t = Search_cst let of_value_type (ty : 'a val_t) : 'a -> xml = @@ -350,6 +360,7 @@ end = struct | Pair (t1,t2) -> (of_pair (convert t1) (convert t2)) | Union (t1,t2) -> (of_union (convert t1) (convert t2)) | State_id -> of_stateid + | Route_id -> of_routeid | Search_cst -> of_search_cst in convert ty @@ -373,6 +384,7 @@ end = struct | Pair (t1,t2) -> (to_pair (convert t1) (convert t2)) | Union (t1,t2) -> (to_union (convert t1) (convert t2)) | State_id -> to_stateid + | Route_id -> to_routeid | Search_cst -> to_search_cst in convert ty @@ -450,6 +462,7 @@ end = struct | Pair (t1,t2) -> (pr_pair (print t1) (print t2)) | Union (t1,t2) -> (pr_union (print t1) (print t2)) | State_id -> pr_state_id + | Route_id -> pr_int (* This is to break if a rename/refactoring makes the strings below outdated *) type 'a exists = bool @@ -475,6 +488,7 @@ end = struct | Union (t1,t2) -> assert(true : ('a,'b) CSig.union exists); Printf.sprintf "((%s, %s) CSig.union)" (print_val_t t1) (print_val_t t2) | State_id -> assert(true : Stateid.t exists); "Stateid.t" + | Route_id -> assert(true : route_id exists); "route_id" let print_type = function Value_type ty -> print_val_t ty @@ -506,7 +520,7 @@ open ReifType let add_sty_t : add_sty val_t = pair_t (pair_t string_t int_t) (pair_t state_id_t bool_t) let edit_at_sty_t : edit_at_sty val_t = state_id_t -let query_sty_t : query_sty val_t = pair_t string_t state_id_t +let query_sty_t : query_sty val_t = pair_t route_id_t (pair_t string_t state_id_t) let goals_sty_t : goals_sty val_t = unit_t let evars_sty_t : evars_sty val_t = unit_t let hints_sty_t : hints_sty val_t = unit_t @@ -528,7 +542,7 @@ let add_rty_t : add_rty val_t = pair_t state_id_t (pair_t (union_t unit_t state_id_t) string_t) let edit_at_rty_t : edit_at_rty val_t = union_t unit_t (pair_t state_id_t (pair_t state_id_t state_id_t)) -let query_rty_t : query_rty val_t = string_t +let query_rty_t : query_rty val_t = unit_t let goals_rty_t : goals_rty val_t = option_t goals_t let evars_rty_t : evars_rty val_t = option_t (list_t evar_t) let hints_rty_t : hints_rty val_t = -- cgit v1.2.3 From fb09983542295dc31122fbad5e01799c1f48e498 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 21 Jun 2017 15:07:26 +0200 Subject: [ide] Correct more merging errors. This file doesn't want to leave us. --- ide/texmacspp.ml | 769 ------------------------------------------------------- 1 file changed, 769 deletions(-) delete mode 100644 ide/texmacspp.ml (limited to 'ide') diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml deleted file mode 100644 index 8409c75218..0000000000 --- a/ide/texmacspp.ml +++ /dev/null @@ -1,769 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* (List.filter (fun (a,_) -> a = attr) attrs) - | _ -> []) - xml_list in - match List.flatten attrs_list with - | [] -> (attr, "") - | l -> (List.hd l) - -let backstep_loc xmllist = - let start_att = get_fst_attr_in_xml_list "begin" xmllist in - let stop_att = get_fst_attr_in_xml_list "end" (List.rev xmllist) in - [start_att ; stop_att] - -let compare_begin_att xml1 xml2 = - let att1 = get_fst_attr_in_xml_list "begin" [xml1] in - let att2 = get_fst_attr_in_xml_list "begin" [xml2] in - match att1, att2 with - | (_, s1), (_, s2) when s1 == "" || s2 == "" -> 0 - | (_, s1), (_, s2) when int_of_string s1 > int_of_string s2 -> 1 - | (_, s1), (_, s2) when int_of_string s1 < int_of_string s2 -> -1 - | _ -> 0 - -let xmlBeginSection ?loc name = xmlWithLoc ?loc "beginsection" ["name", name] [] - -let xmlEndSegment ?loc name = xmlWithLoc ?loc "endsegment" ["name", name] [] - -let xmlThm ?loc typ name xml = - xmlWithLoc ?loc "theorem" ["type", typ; "name", name] xml - -let xmlDef ?loc typ name xml = - xmlWithLoc ?loc "definition" ["type", typ; "name", name] xml - -let xmlNotation ?loc attr name xml = - xmlWithLoc ?loc "notation" (("name", name) :: attr) xml - -let xmlReservedNotation ?loc attr name = - xmlWithLoc ?loc "reservednotation" (("name", name) :: attr) [] - -let xmlCst ?loc ?(attr=[]) name = - xmlWithLoc ?loc "constant" (("name", name) :: attr) [] - -let xmlOperator ?loc ?(attr=[]) ?(pprules=[]) name = - xmlWithLoc ?loc "operator" - (("name", name) :: List.map (fun (a,b) -> "format"^a,b) pprules @ attr) [] - -let xmlApply ?loc ?(attr=[]) xml = xmlWithLoc ?loc "apply" attr xml - -let xmlToken ?loc ?(attr=[]) xml = xmlWithLoc ?loc "token" attr xml - -let xmlTyped xml = Element("typed", (backstep_loc xml), xml) - -let xmlReturn ?(attr=[]) xml = Element("return", attr, xml) - -let xmlCase xml = Element("case", [], xml) - -let xmlScrutinee ?(attr=[]) xml = Element("scrutinee", attr, xml) - -let xmlWith xml = Element("with", [], xml) - -let xmlAssign id xml = Element("assign", ["target",string_of_id id], [xml]) - -let xmlInductive ?loc kind xml = xmlWithLoc ?loc "inductive" ["kind",kind] xml - -let xmlCoFixpoint xml = Element("cofixpoint", [], xml) - -let xmlFixpoint xml = Element("fixpoint", [], xml) - -let xmlCheck ?loc xml = xmlWithLoc ?loc "check" [] xml - -let xmlAssumption ?loc kind xml = xmlWithLoc ?loc "assumption" ["kind",kind] xml - -let xmlComment ?loc xml = xmlWithLoc ?loc "comment" [] xml - -let xmlCanonicalStructure ?loc attr = xmlWithLoc ?loc "canonicalstructure" attr [] - -let xmlQed ?loc ?(attr=[]) = xmlWithLoc ?loc "qed" attr [] - -let xmlPatvar ?loc id = xmlWithLoc ?loc "patvar" ["id", id] [] - -let xmlReference ref = - let name = Libnames.string_of_reference ref in - let i, j = Option.cata Loc.unloc (0,0) (Libnames.loc_of_reference ref) in - let b, e = string_of_int i, string_of_int j in - Element("reference",["name", name; "begin", b; "end", e] ,[]) - -let xmlRequire ?loc ?(attr=[]) xml = xmlWithLoc ?loc "require" attr xml -let xmlImport ?loc ?(attr=[]) xml = xmlWithLoc ?loc "import" attr xml - -let xmlAddLoadPath ?loc ?(attr=[]) xml = xmlWithLoc ?loc "addloadpath" attr xml -let xmlRemoveLoadPath ?loc ?(attr=[]) = xmlWithLoc ?loc "removeloadpath" attr -let xmlAddMLPath ?loc ?(attr=[]) = xmlWithLoc ?loc "addmlpath" attr - -let xmlExtend ?loc xml = xmlWithLoc ?loc "extend" [] xml - -let xmlScope ?loc ?(attr=[]) action name xml = - xmlWithLoc ?loc "scope" (["name",name;"action",action] @ attr) xml - -let xmlProofMode ?loc name = xmlWithLoc ?loc "proofmode" ["name",name] [] - -let xmlProof ?loc xml = xmlWithLoc ?loc "proof" [] xml - -let xmlSectionSubsetDescr name ssd = - Element("sectionsubsetdescr",["name",name], - [PCData (Proof_using.to_string ssd)]) - -let xmlDeclareMLModule ?loc s = - xmlWithLoc ?loc "declarexmlmodule" [] - (List.map (fun x -> Element("path",["value",x],[])) s) - -(* tactics *) -let xmlLtac ?loc xml = xmlWithLoc ?loc "ltac" [] xml - -(* toplevel commands *) -let xmlGallina ?loc xml = xmlWithLoc ?loc "gallina" [] xml - -let xmlTODO ?loc x = - xmlWithLoc ?loc "todo" [] [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] - -let string_of_name n = - match n with - | Anonymous -> "_" - | Name id -> Id.to_string id - -let string_of_glob_sort s = - match s with - | GProp -> "Prop" - | GSet -> "Set" - | GType _ -> "Type" - -let string_of_cast_sort c = - match c with - | CastConv _ -> "CastConv" - | CastVM _ -> "CastVM" - | CastNative _ -> "CastNative" - | CastCoerce -> "CastCoerce" - -let string_of_case_style s = - match s with - | LetStyle -> "Let" - | IfStyle -> "If" - | LetPatternStyle -> "LetPattern" - | MatchStyle -> "Match" - | RegularStyle -> "Regular" - -let attribute_of_syntax_modifier sm = -match sm with - | SetItemLevel (sl, NumLevel n) -> - List.map (fun s -> ("itemlevel", s)) sl @ ["level", string_of_int n] - | SetItemLevel (sl, NextLevel) -> - List.map (fun s -> ("itemlevel", s)) sl @ ["level", "next"] - | SetLevel i -> ["level", string_of_int i] - | SetAssoc a -> - begin match a with - | NonA -> ["",""] - | RightA -> ["associativity", "right"] - | LeftA -> ["associativity", "left"] - end - | SetEntryType (s, _) -> ["entrytype", s] - | SetOnlyPrinting -> ["onlyprinting", ""] - | SetOnlyParsing -> ["onlyparsing", ""] - | SetCompatVersion v -> ["compat", Flags.pr_version v] - | SetFormat (system, (loc, s)) -> - let start, stop = unlock ?loc in - ["format-"^system, s; "begin", start; "end", stop] - -let string_of_assumption_kind l a many = - match l, a, many with - | (Discharge, Logical, true) -> "Hypotheses" - | (Discharge, Logical, false) -> "Hypothesis" - | (Discharge, Definitional, true) -> "Variables" - | (Discharge, Definitional, false) -> "Variable" - | (Global, Logical, true) -> "Axioms" - | (Global, Logical, false) -> "Axiom" - | (Global, Definitional, true) -> "Parameters" - | (Global, Definitional, false) -> "Parameter" - | (Local, Logical, true) -> "Local Axioms" - | (Local, Logical, false) -> "Local Axiom" - | (Local, Definitional, true) -> "Local Parameters" - | (Local, Definitional, false) -> "Local Parameter" - | (Global, Conjectural, _) -> "Conjecture" - | ((Discharge | Local), Conjectural, _) -> assert false - -let rec pp_bindlist bl = - let tlist = - List.flatten - (List.map - (fun (loc_names, _, e) -> - let names = - (List.map - (fun (loc, name) -> - xmlCst ?loc (string_of_name name)) loc_names) in - match e.CAst.v with - | CHole _ -> names - | _ -> names @ [pp_expr e]) - bl) in - match tlist with - | [e] -> e - | l -> xmlTyped l -and pp_decl_notation ((_, s), ce, sc) = (* don't know what it is for now *) - Element ("decl_notation", ["name", s], [pp_expr ce]) -and pp_local_binder lb = (* don't know what it is for now *) - match lb with - | CLocalDef ((loc, nam), ce, ty) -> - let attrs = ["name", string_of_name nam] in - let value = match ty with - Some t -> CAst.make ?loc:(Loc.merge_opt (constr_loc ce) (constr_loc t)) @@ CCast (ce, CastConv t) - | None -> ce in - pp_expr ~attr:attrs value - | CLocalAssum (namll, _, ce) -> - let ppl = - List.map (fun (loc, nam) -> (xmlCst ?loc (string_of_name nam))) namll in - xmlTyped (ppl @ [pp_expr ce]) - | CLocalPattern _ -> - assert false -and pp_local_decl_expr lde = (* don't know what it is for now *) - match lde with - | AssumExpr (_, ce) -> pp_expr ce - | DefExpr (_, ce, _) -> pp_expr ce -and pp_inductive_expr ((_, ((l, id),_)), lbl, ceo, _, cl_or_rdexpr) = - (* inductive_expr *) - let b,e = Option.cata Loc.unloc (0,0) l in - let location = ["begin", string_of_int b; "end", string_of_int e] in - [Element ("lident", ["name", Id.to_string id] @ location, [])] @ (* inductive name *) - begin match cl_or_rdexpr with - | Constructors coel -> List.map (fun (_, (_, ce)) -> pp_expr ce) coel - | RecordDecl (_, ldewwwl) -> - List.map (fun (((_, x), _), _) -> pp_local_decl_expr x) ldewwwl - end @ - begin match ceo with (* don't know what it is for now *) - | Some ce -> [pp_expr ce] - | None -> [] - end @ - (List.map pp_local_binder lbl) -and pp_recursion_order_expr optid roe = (* don't know what it is for now *) - let attrs = - match optid with - | None -> [] - | Some (loc, id) -> - let start, stop = unlock ?loc in - ["begin", start; "end", stop ; "name", Id.to_string id] in - let kind, expr = - match roe with - | CStructRec -> "struct", [] - | CWfRec e -> "rec", [pp_expr e] - | CMeasureRec (e, None) -> "mesrec", [pp_expr e] - | CMeasureRec (e, Some rel) -> "mesrec", [pp_expr e] @ [pp_expr rel] in - Element ("recursion_order", ["kind", kind] @ attrs, expr) -and pp_fixpoint_expr (((loc, id), pl), (optid, roe), lbl, ce, ceo) = - (* fixpoint_expr *) - let start, stop = unlock ?loc in - let id = Id.to_string id in - [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @ - (* fixpoint name *) - [pp_recursion_order_expr optid roe] @ - (List.map pp_local_binder lbl) @ - [pp_expr ce] @ - begin match ceo with (* don't know what it is for now *) - | Some ce -> [pp_expr ce] - | None -> [] - end -and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *) - (* Nota: it is like fixpoint_expr without (optid, roe) - * so could be merged if there is no more differences *) - let start, stop = unlock ?loc in - let id = Id.to_string id in - [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @ - (* cofixpoint name *) - (List.map pp_local_binder lbl) @ - [pp_expr ce] @ - begin match ceo with (* don't know what it is for now *) - | Some ce -> [pp_expr ce] - | None -> [] - end -and pp_lident (loc, id) = xmlCst ?loc (Id.to_string id) -and pp_simple_binder (idl, ce) = List.map pp_lident idl @ [pp_expr ce] -and pp_cases_pattern_expr {loc ; CAst.v = cpe} = - match cpe with - | CPatAlias (cpe, id) -> - xmlApply ?loc - (xmlOperator ?loc ~attr:["name", string_of_id id] "alias" :: - [pp_cases_pattern_expr cpe]) - | CPatCstr (ref, None, cpel2) -> - xmlApply ?loc - (xmlOperator ?loc "reference" - ~attr:["name", Libnames.string_of_reference ref] :: - [Element ("impargs", [], []); - Element ("args", [], (List.map pp_cases_pattern_expr cpel2))]) - | CPatCstr (ref, Some cpel1, cpel2) -> - xmlApply ?loc - (xmlOperator ?loc "reference" - ~attr:["name", Libnames.string_of_reference ref] :: - [Element ("impargs", [], (List.map pp_cases_pattern_expr cpel1)); - Element ("args", [], (List.map pp_cases_pattern_expr cpel2))]) - | CPatAtom optr -> - let attrs = match optr with - | None -> [] - | Some r -> ["name", Libnames.string_of_reference r] in - xmlApply ?loc (xmlOperator ?loc "atom" ~attr:attrs :: []) - | CPatOr cpel -> - xmlApply ?loc (xmlOperator ?loc "or" :: List.map pp_cases_pattern_expr cpel) - | CPatNotation (n, (subst_constr, subst_rec), cpel) -> - xmlApply ?loc - (xmlOperator ?loc "notation" :: - [xmlOperator ?loc n; - Element ("subst", [], - [Element ("subterms", [], - List.map pp_cases_pattern_expr subst_constr); - Element ("recsubterms", [], - List.map - (fun (cpel) -> - Element ("recsubterm", [], - List.map pp_cases_pattern_expr cpel)) - subst_rec)]); - Element ("args", [], (List.map pp_cases_pattern_expr cpel))]) - | CPatPrim tok -> pp_token ?loc tok - | CPatRecord rcl -> - xmlApply ?loc - (xmlOperator ?loc "record" :: - List.map (fun (r, cpe) -> - Element ("field", - ["reference", Libnames.string_of_reference r], - [pp_cases_pattern_expr cpe])) - rcl) - | CPatDelimiters (delim, cpe) -> - xmlApply ?loc - (xmlOperator ?loc "delimiter" ~attr:["name", delim] :: - [pp_cases_pattern_expr cpe]) - | CPatCast _ -> assert false -and pp_case_expr (e, name, pat) = - match name, pat with - | None, None -> xmlScrutinee [pp_expr e] - | Some (loc, name), None -> - let start, stop= unlock ?loc in - xmlScrutinee ~attr:["name", string_of_name name; - "begin", start; "end", stop] [pp_expr e] - | Some (loc, name), Some p -> - let start, stop= unlock ?loc in - xmlScrutinee ~attr:["name", string_of_name name; - "begin", start; "end", stop] - [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e] - | None, Some p -> - xmlScrutinee [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e] -and pp_branch_expr_list bel = - xmlWith - (List.map - (fun (_, (cpel, e)) -> - let ppcepl = - List.map pp_cases_pattern_expr (List.flatten (List.map snd cpel)) in - let ppe = [pp_expr e] in - xmlCase (ppcepl @ ppe)) - bel) -and pp_token ?loc tok = - let tokstr = - match tok with - | String s -> PCData s - | Numeral n -> PCData (to_string n) in - xmlToken ?loc [tokstr] -and pp_local_binder_list lbl = - let l = (List.map pp_local_binder lbl) in - Element ("recurse", (backstep_loc l), l) -and pp_const_expr_list cel = - let l = List.map pp_expr cel in - Element ("recurse", (backstep_loc l), l) -and pp_expr ?(attr=[]) { loc; CAst.v = e } = - match e with - | CRef (r, _) -> - xmlCst ?loc:(Libnames.loc_of_reference r) ~attr (Libnames.string_of_reference r) - | CProdN (bl, e) -> - xmlApply ?loc - (xmlOperator ?loc "forall" :: [pp_bindlist bl] @ [pp_expr e]) - | CApp ((_, hd), args) -> - xmlApply ?loc ~attr (pp_expr hd :: List.map (fun (e,_) -> pp_expr e) args) - | CAppExpl ((_, r, _), args) -> - xmlApply ?loc ~attr - (xmlCst ?loc:(Libnames.loc_of_reference r) (Libnames.string_of_reference r) - :: List.map pp_expr args) - | CNotation (notation, ([],[],[])) -> - xmlOperator ?loc notation - | CNotation (notation, (args, cell, lbll)) -> - let fmts = Notation.find_notation_extra_printing_rules notation in - let oper = xmlOperator ?loc notation ~pprules:fmts in - let cels = List.map pp_const_expr_list cell in - let lbls = List.map pp_local_binder_list lbll in - let args = List.map pp_expr args in - xmlApply ?loc (oper :: (List.sort compare_begin_att (args @ cels @ lbls))) - | CSort(s) -> - xmlOperator ?loc (string_of_glob_sort s) - | CDelimiters (scope, ce) -> - xmlApply ?loc (xmlOperator ?loc "delimiter" ~attr:["name", scope] :: - [pp_expr ce]) - | CPrim tok -> pp_token ?loc tok - | CGeneralization (kind, _, e) -> - let kind= match kind with - | Explicit -> "explicit" - | Implicit -> "implicit" in - xmlApply ?loc - (xmlOperator ?loc ~attr:["kind", kind] "generalization" :: [pp_expr e]) - | CCast (e, tc) -> - begin match tc with - | CastConv t | CastVM t |CastNative t -> - xmlApply ?loc - (xmlOperator ?loc ":" ~attr:["kind", (string_of_cast_sort tc)] :: - [pp_expr e; pp_expr t]) - | CastCoerce -> - xmlApply ?loc - (xmlOperator ?loc ":" ~attr:["kind", "CastCoerce"] :: - [pp_expr e]) - end - | CEvar (ek, cel) -> - let ppcel = List.map (fun (id,e) -> xmlAssign id (pp_expr e)) cel in - xmlApply ?loc - (xmlOperator ?loc "evar" ~attr:["id", string_of_id ek] :: - ppcel) - | CPatVar id -> xmlPatvar ?loc (string_of_id id) - | CHole (_, _, _) -> xmlCst ?loc ~attr "_" - | CIf (test, (_, ret), th, el) -> - let return = match ret with - | None -> [] - | Some r -> [xmlReturn [pp_expr r]] in - xmlApply ?loc - (xmlOperator ?loc "if" :: - return @ [pp_expr th] @ [pp_expr el]) - | CLetTuple (names, (_, ret), value, body) -> - let return = match ret with - | None -> [] - | Some r -> [xmlReturn [pp_expr r]] in - xmlApply ?loc - (xmlOperator ?loc "lettuple" :: - return @ - (List.map (fun (loc, var) -> xmlCst ?loc (string_of_name var)) names) @ - [pp_expr value; pp_expr body]) - | CCases (sty, ret, cel, bel) -> - let return = match ret with - | None -> [] - | Some r -> [xmlReturn [pp_expr r]] in - xmlApply ?loc - (xmlOperator ?loc ~attr:["style", (string_of_case_style sty)] "match" :: - (return @ - [Element ("scrutinees", [], List.map pp_case_expr cel)] @ - [pp_branch_expr_list bel])) - | CRecord _ -> assert false - | CLetIn ((varloc, var), value, typ, body) -> - let value = match typ with - | Some t -> - CAst.make ?loc:(Loc.merge_opt (constr_loc value) (constr_loc t)) (CCast (value, CastConv t)) - | None -> value in - xmlApply ?loc - (xmlOperator ?loc "let" :: - [xmlCst ?loc:varloc (string_of_name var) ; pp_expr value; pp_expr body]) - | CLambdaN (bl, e) -> - xmlApply ?loc - (xmlOperator ?loc "lambda" :: [pp_bindlist bl] @ [pp_expr e]) - | CCoFix (_, _) -> assert false - | CFix (lid, fel) -> - xmlApply ?loc - (xmlOperator ?loc "fix" :: - List.flatten (List.map - (fun (a,b,cl,c,d) -> pp_fixpoint_expr ((a,None),b,cl,c,Some d)) - fel)) - -let pp_comment c = - match c with - | CommentConstr e -> [pp_expr e] - | CommentString s -> [Element ("string", [], [PCData s])] - | CommentInt i -> [PCData (string_of_int i)] - -let rec tmpp ?loc v = - match v with - (* Control *) - | VernacLoad (verbose,f) -> - xmlWithLoc ?loc "load" ["verbose",string_of_bool verbose;"file",f] [] - | VernacTime (loc,e) -> - xmlApply ?loc (Element("time",[],[]) :: - [tmpp ?loc e]) - | VernacRedirect (s, (loc,e)) -> - xmlApply ?loc (Element("redirect",["path", s],[]) :: - [tmpp ?loc e]) - | VernacTimeout (s,e) -> - xmlApply ?loc (Element("timeout",["val",string_of_int s],[]) :: - [tmpp ?loc e]) - | VernacFail e -> xmlApply ?loc (Element("fail",[],[]) :: [tmpp ?loc e]) - - (* Syntax *) - | VernacSyntaxExtension (_, ((_, name), sml)) -> - let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in - xmlReservedNotation ?loc attrs name - - | VernacOpenCloseScope (_,(true,name)) -> xmlScope ?loc "open" name [] - | VernacOpenCloseScope (_,(false,name)) -> xmlScope ?loc "close" name [] - | VernacDelimiters (name,Some tag) -> - xmlScope ?loc "delimit" name ~attr:["delimiter",tag] [] - | VernacDelimiters (name,None) -> - xmlScope ?loc "undelimit" name ~attr:[] [] - | VernacInfix (_,((_,name),sml),ce,sn) -> - let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in - let sc_attr = - match sn with - | Some scope -> ["scope", scope] - | None -> [] in - xmlNotation ?loc (sc_attr @ attrs) name [pp_expr ce] - | VernacNotation (_, ce, (lstr, sml), sn) -> - let name = snd lstr in - let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in - let sc_attr = - match sn with - | Some scope -> ["scope", scope] - | None -> [] in - xmlNotation ?loc (sc_attr @ attrs) name [pp_expr ce] - | VernacBindScope _ as x -> xmlTODO ?loc x - | VernacNotationAddFormat _ as x -> xmlTODO ?loc x - | VernacUniverse _ - | VernacConstraint _ - | VernacPolymorphic (_, _) as x -> xmlTODO ?loc x - (* Gallina *) - | VernacDefinition (ldk, ((_,id),_), de) -> - let l, dk = - match ldk with - | Some l, dk -> (l, dk) - | None, dk -> (Global, dk) in (* Like in ppvernac.ml, l 585 *) - let e = - match de with - | ProveBody (_, ce) -> ce - | DefineBody (_, Some _, ce, None) -> ce - | DefineBody (_, None , ce, None) -> ce - | DefineBody (_, Some _, ce, Some _) -> ce - | DefineBody (_, None , ce, Some _) -> ce in - let str_dk = Kindops.string_of_definition_kind (l, false, dk) in - let str_id = Id.to_string id in - (xmlDef ?loc str_dk str_id [pp_expr e]) - | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) -> - let str_tk = Kindops.string_of_theorem_kind tk in - let str_id = Id.to_string id in - (xmlThm ?loc str_tk str_id [pp_expr statement]) - | VernacStartTheoremProof _ as x -> xmlTODO ?loc x - | VernacEndProof pe -> - begin - match pe with - | Admitted -> xmlQed ?loc ?attr:None - | Proved (_, Some ((_, id), Some tk)) -> - let nam = Id.to_string id in - let typ = Kindops.string_of_theorem_kind tk in - xmlQed ?loc ~attr:["name", nam; "type", typ] - | Proved (_, Some ((_, id), None)) -> - let nam = Id.to_string id in - xmlQed ?loc ~attr:["name", nam] - | Proved _ -> xmlQed ?loc ?attr:None - end - | VernacExactProof _ as x -> xmlTODO ?loc x - | VernacAssumption ((l, a), _, sbwcl) -> - let binders = List.map (fun (_, (id, c)) -> (List.map fst id, c)) sbwcl in - let many = - List.length (List.flatten (List.map fst binders)) > 1 in - let exprs = - List.flatten (List.map pp_simple_binder binders) in - let l = match l with Some x -> x | None -> Decl_kinds.Global in - let kind = string_of_assumption_kind l a many in - xmlAssumption ?loc kind exprs - | VernacInductive (_, _, _, iednll) -> - let kind = - let (_, _, _, k, _), _ = List.hd iednll in - begin - match k with - | Record -> "Record" - | Structure -> "Structure" - | Inductive_kw -> "Inductive" - | CoInductive -> "CoInductive" - | Class _ -> "Class" - | Variant -> "Variant" - end in - let exprs = - List.flatten (* should probably not be flattened *) - (List.map - (fun (ie, dnl) -> (pp_inductive_expr ie) @ - (List.map pp_decl_notation dnl)) iednll) in - xmlInductive ?loc kind exprs - | VernacFixpoint (_, fednll) -> - let exprs = - List.flatten (* should probably not be flattened *) - (List.map - (fun (fe, dnl) -> (pp_fixpoint_expr fe) @ - (List.map pp_decl_notation dnl)) fednll) in - xmlFixpoint exprs - | VernacCoFixpoint (_, cfednll) -> - (* Nota: it is like VernacFixpoint without so could be merged *) - let exprs = - List.flatten (* should probably not be flattened *) - (List.map - (fun (cfe, dnl) -> (pp_cofixpoint_expr cfe) @ - (List.map pp_decl_notation dnl)) cfednll) in - xmlCoFixpoint exprs - | VernacScheme _ as x -> xmlTODO ?loc x - | VernacCombinedScheme _ as x -> xmlTODO ?loc x - - (* Gallina extensions *) - | VernacBeginSection (_, id) -> xmlBeginSection ?loc (Id.to_string id) - | VernacEndSegment (_, id) -> xmlEndSegment ?loc (Id.to_string id) - | VernacNameSectionHypSet _ as x -> xmlTODO ?loc x - | VernacRequire (from, import, l) -> - let import = match import with - | None -> [] - | Some true -> ["export","true"] - | Some false -> ["import","true"] - in - let from = match from with - | None -> [] - | Some r -> ["from", Libnames.string_of_reference r] - in - xmlRequire ?loc ~attr:(from @ import) (List.map (fun ref -> - xmlReference ref) l) - | VernacImport (true,l) -> - xmlImport ?loc ~attr:["export","true"] (List.map (fun ref -> - xmlReference ref) l) - | VernacImport (false,l) -> - xmlImport ?loc (List.map (fun ref -> xmlReference ref) l) - | VernacCanonical r -> - let attr = - match r with - | AN (Qualid (_, q)) -> ["qualid", string_of_qualid q] - | AN (Ident (_, id)) -> ["id", Id.to_string id] - | ByNotation (_, (s, _)) -> ["notation", s] in - xmlCanonicalStructure ?loc attr - | VernacCoercion _ as x -> xmlTODO ?loc x - | VernacIdentityCoercion _ as x -> xmlTODO ?loc x - - (* Type classes *) - | VernacInstance _ as x -> xmlTODO ?loc x - - | VernacContext _ as x -> xmlTODO ?loc x - - | VernacDeclareInstances _ as x -> xmlTODO ?loc x - - | VernacDeclareClass _ as x -> xmlTODO ?loc x - - (* Modules and Module Types *) - | VernacDeclareModule _ as x -> xmlTODO ?loc x - | VernacDefineModule _ as x -> xmlTODO ?loc x - | VernacDeclareModuleType _ as x -> xmlTODO ?loc x - | VernacInclude _ as x -> xmlTODO ?loc x - - (* Solving *) - - | (VernacSolveExistential _) as x -> - xmlLtac ?loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] - - (* Auxiliary file and library management *) - | VernacAddLoadPath (recf,name,None) -> - xmlAddLoadPath ?loc ~attr:["rec",string_of_bool recf;"path",name] [] - | VernacAddLoadPath (recf,name,Some dp) -> - xmlAddLoadPath ?loc ~attr:["rec",string_of_bool recf;"path",name] - [PCData (Names.DirPath.to_string dp)] - | VernacRemoveLoadPath name -> xmlRemoveLoadPath ?loc ~attr:["path",name] [] - | VernacAddMLPath (recf,name) -> - xmlAddMLPath ?loc ~attr:["rec",string_of_bool recf;"path",name] [] - | VernacDeclareMLModule sl -> xmlDeclareMLModule ?loc sl - | VernacChdir _ as x -> xmlTODO ?loc x - - (* State management *) - | VernacWriteState _ as x -> xmlTODO ?loc x - | VernacRestoreState _ as x -> xmlTODO ?loc x - - (* Resetting *) - | VernacResetName _ as x -> xmlTODO ?loc x - | VernacResetInitial as x -> xmlTODO ?loc x - | VernacBack _ as x -> xmlTODO ?loc x - | VernacBackTo _ -> PCData "VernacBackTo" - - (* Commands *) - | VernacCreateHintDb _ as x -> xmlTODO ?loc x - | VernacRemoveHints _ as x -> xmlTODO ?loc x - | VernacHints _ as x -> xmlTODO ?loc x - | VernacSyntacticDefinition ((_, name), (idl, ce), _, _) -> - let name = Id.to_string name in - let attrs = List.map (fun id -> ("id", Id.to_string id)) idl in - xmlNotation ?loc attrs name [pp_expr ce] - | VernacDeclareImplicits _ as x -> xmlTODO ?loc x - | VernacArguments _ as x -> xmlTODO ?loc x - | VernacArgumentsScope _ as x -> xmlTODO ?loc x - | VernacReserve _ as x -> xmlTODO ?loc x - | VernacGeneralizable _ as x -> xmlTODO ?loc x - | VernacSetOpacity _ as x -> xmlTODO ?loc x - | VernacSetStrategy _ as x -> xmlTODO ?loc x - | VernacUnsetOption _ as x -> xmlTODO ?loc x - | VernacSetOption _ as x -> xmlTODO ?loc x - | VernacSetAppendOption _ as x -> xmlTODO ?loc x - | VernacAddOption _ as x -> xmlTODO ?loc x - | VernacRemoveOption _ as x -> xmlTODO ?loc x - | VernacMemOption _ as x -> xmlTODO ?loc x - | VernacPrintOption _ as x -> xmlTODO ?loc x - | VernacCheckMayEval (_,_,e) -> xmlCheck ?loc [pp_expr e] - | VernacGlobalCheck _ as x -> xmlTODO ?loc x - | VernacDeclareReduction _ as x -> xmlTODO ?loc x - | VernacPrint _ as x -> xmlTODO ?loc x - | VernacSearch _ as x -> xmlTODO ?loc x - | VernacLocate _ as x -> xmlTODO ?loc x - | VernacRegister _ as x -> xmlTODO ?loc x - | VernacComments (cl) -> - xmlComment ?loc (List.flatten (List.map pp_comment cl)) - - (* Stm backdoor *) - | VernacStm _ as x -> xmlTODO ?loc x - - (* Proof management *) - | VernacGoal _ as x -> xmlTODO ?loc x - | VernacAbort _ as x -> xmlTODO ?loc x - | VernacAbortAll -> PCData "VernacAbortAll" - | VernacRestart as x -> xmlTODO ?loc x - | VernacUndo _ as x -> xmlTODO ?loc x - | VernacUndoTo _ as x -> xmlTODO ?loc x - | VernacBacktrack _ as x -> xmlTODO ?loc x - | VernacFocus _ as x -> xmlTODO ?loc x - | VernacUnfocus as x -> xmlTODO ?loc x - | VernacUnfocused as x -> xmlTODO ?loc x - | VernacBullet _ as x -> xmlTODO ?loc x - | VernacSubproof _ as x -> xmlTODO ?loc x - | VernacEndSubproof as x -> xmlTODO ?loc x - | VernacShow _ as x -> xmlTODO ?loc x - | VernacCheckGuard as x -> xmlTODO ?loc x - | VernacProof (tac,using) -> - let tac = None (** FIXME *) in - let using = Option.map (xmlSectionSubsetDescr "using") using in - xmlProof ?loc (Option.List.(cons tac (cons using []))) - | VernacProofMode name -> xmlProofMode ?loc name - - (* Toplevel control *) - | VernacToplevelControl _ as x -> xmlTODO ?loc x - - (* For extension *) - | VernacExtend _ as x -> - xmlExtend ?loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] - - (* Flags *) - | VernacProgram e -> xmlApply ?loc (Element("program",[],[]) :: [tmpp ?loc e]) - | VernacLocal (b,e) -> - xmlApply ?loc (Element("local",["flag",string_of_bool b],[]) :: - [tmpp ?loc e]) - -let tmpp ?loc v = - match tmpp ?loc v with - | Element("ltac",_,_) as x -> x - | xml -> xmlGallina ?loc [xml] -- cgit v1.2.3