summaryrefslogtreecommitdiff
path: root/ide/texmacspp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/texmacspp.ml')
-rw-r--r--ide/texmacspp.ml768
1 files changed, 768 insertions, 0 deletions
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
new file mode 100644
index 00000000..680da7f5
--- /dev/null
+++ b/ide/texmacspp.ml
@@ -0,0 +1,768 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Xml_datatype
+open Vernacexpr
+open Constrexpr
+open Names
+open Misctypes
+open Bigint
+open Decl_kinds
+open Extend
+open Libnames
+
+let unlock loc =
+ let start, stop = Loc.unloc loc in
+ (string_of_int start, string_of_int stop)
+
+let xmlWithLoc loc ename attr xml =
+ let start, stop = unlock loc in
+ Element(ename, [ "begin", start; "end", stop ] @ attr, xml)
+
+let get_fst_attr_in_xml_list attr xml_list =
+ let attrs_list =
+ List.map (function
+ | Element (_, attrs, _) -> (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 typ name loc xml =
+ xmlWithLoc loc "theorem" ["type", typ; "name", name] xml
+
+let xmlDef typ name loc xml =
+ xmlWithLoc loc "definition" ["type", typ; "name", name] xml
+
+let xmlNotation attr name loc xml =
+ xmlWithLoc loc "notation" (("name", name) :: attr) xml
+
+let xmlReservedNotation attr name loc =
+ xmlWithLoc loc "reservednotation" (("name", name) :: attr) []
+
+let xmlCst name ?(attr=[]) loc =
+ xmlWithLoc loc "constant" (("name", name) :: attr) []
+
+let xmlOperator name ?(attr=[]) ?(pprules=[]) loc =
+ 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 kind loc 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 kind loc xml = xmlWithLoc loc "assumption" ["kind",kind] xml
+
+let xmlComment loc xml = xmlWithLoc loc "comment" [] xml
+
+let xmlCanonicalStructure attr loc = xmlWithLoc loc "canonicalstructure" attr []
+
+let xmlQed ?(attr=[]) loc = xmlWithLoc loc "qed" attr []
+
+let xmlPatvar id loc = xmlWithLoc loc "patvar" ["id", id] []
+
+let xmlReference ref =
+ let name = Libnames.string_of_reference ref in
+ let i, j = Loc.unloc (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 action ?(attr=[]) 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 xmlRawTactic name rtac =
+ Element("rawtactic", ["name",name],
+ [PCData (Pp.string_of_ppcmds (Pptactic.pr_raw_tactic rtac))])
+
+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 (string_of_name name) loc) loc_names) in
+ match e 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
+ | LocalRawDef ((_, nam), ce) ->
+ let attrs = ["name", string_of_name nam] in
+ pp_expr ~attr:attrs ce
+ | LocalRawAssum (namll, _, ce) ->
+ let ppl =
+ List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in
+ xmlTyped (ppl @ [pp_expr ce])
+ | LocalPattern _ ->
+ 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 = Loc.unloc 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 (Id.to_string id) loc
+and pp_simple_binder (idl, ce) = List.map pp_lident idl @ [pp_expr ce]
+and pp_cases_pattern_expr cpe =
+ match cpe with
+ | CPatAlias (loc, cpe, id) ->
+ xmlApply loc
+ (xmlOperator "alias" ~attr:["name", string_of_id id] loc ::
+ [pp_cases_pattern_expr cpe])
+ | CPatCstr (loc, ref, None, cpel2) ->
+ xmlApply loc
+ (xmlOperator "reference"
+ ~attr:["name", Libnames.string_of_reference ref] loc ::
+ [Element ("impargs", [], []);
+ Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
+ | CPatCstr (loc, ref, Some cpel1, cpel2) ->
+ xmlApply loc
+ (xmlOperator "reference"
+ ~attr:["name", Libnames.string_of_reference ref] loc ::
+ [Element ("impargs", [], (List.map pp_cases_pattern_expr cpel1));
+ Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
+ | CPatAtom (loc, optr) ->
+ let attrs = match optr with
+ | None -> []
+ | Some r -> ["name", Libnames.string_of_reference r] in
+ xmlApply loc (xmlOperator "atom" ~attr:attrs loc :: [])
+ | CPatOr (loc, cpel) ->
+ xmlApply loc (xmlOperator "or" loc :: List.map pp_cases_pattern_expr cpel)
+ | CPatNotation (loc, n, (subst_constr, subst_rec), cpel) ->
+ xmlApply loc
+ (xmlOperator "notation" loc ::
+ [xmlOperator n loc;
+ 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 (loc, tok) -> pp_token loc tok
+ | CPatRecord (loc, rcl) ->
+ xmlApply loc
+ (xmlOperator "record" loc ::
+ List.map (fun (r, cpe) ->
+ Element ("field",
+ ["reference", Libnames.string_of_reference r],
+ [pp_cases_pattern_expr cpe]))
+ rcl)
+ | CPatDelimiters (loc, delim, cpe) ->
+ xmlApply loc
+ (xmlOperator "delimiter" ~attr:["name", delim] loc ::
+ [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=[]) e =
+ match e with
+ | CRef (r, _) ->
+ xmlCst ~attr
+ (Libnames.string_of_reference r) (Libnames.loc_of_reference r)
+ | CProdN (loc, bl, e) ->
+ xmlApply loc
+ (xmlOperator "forall" loc :: [pp_bindlist bl] @ [pp_expr e])
+ | CApp (loc, (_, hd), args) ->
+ xmlApply ~attr loc (pp_expr hd :: List.map (fun (e,_) -> pp_expr e) args)
+ | CAppExpl (loc, (_, r, _), args) ->
+ xmlApply ~attr loc
+ (xmlCst (Libnames.string_of_reference r)
+ (Libnames.loc_of_reference r) :: List.map pp_expr args)
+ | CNotation (loc, notation, ([],[],[])) ->
+ xmlOperator notation loc
+ | CNotation (loc, notation, (args, cell, lbll)) ->
+ let fmts = Notation.find_notation_extra_printing_rules notation in
+ let oper = xmlOperator notation loc ~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(loc, s) ->
+ xmlOperator (string_of_glob_sort s) loc
+ | CDelimiters (loc, scope, ce) ->
+ xmlApply loc (xmlOperator "delimiter" ~attr:["name", scope] loc ::
+ [pp_expr ce])
+ | CPrim (loc, tok) -> pp_token loc tok
+ | CGeneralization (loc, kind, _, e) ->
+ let kind= match kind with
+ | Explicit -> "explicit"
+ | Implicit -> "implicit" in
+ xmlApply loc
+ (xmlOperator "generalization" ~attr:["kind", kind] loc :: [pp_expr e])
+ | CCast (loc, 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 (loc, ek, cel) ->
+ let ppcel = List.map (fun (id,e) -> xmlAssign id (pp_expr e)) cel in
+ xmlApply loc
+ (xmlOperator "evar" loc ~attr:["id", string_of_id ek] ::
+ ppcel)
+ | CPatVar (loc, id) -> xmlPatvar (string_of_id id) loc
+ | CHole (loc, _, _, _) -> xmlCst ~attr "_" loc
+ | CIf (loc, test, (_, ret), th, el) ->
+ let return = match ret with
+ | None -> []
+ | Some r -> [xmlReturn [pp_expr r]] in
+ xmlApply loc
+ (xmlOperator "if" loc ::
+ return @ [pp_expr th] @ [pp_expr el])
+ | CLetTuple (loc, names, (_, ret), value, body) ->
+ let return = match ret with
+ | None -> []
+ | Some r -> [xmlReturn [pp_expr r]] in
+ xmlApply loc
+ (xmlOperator "lettuple" loc ::
+ return @
+ (List.map (fun (loc, var) -> xmlCst (string_of_name var) loc) names) @
+ [pp_expr value; pp_expr body])
+ | CCases (loc, sty, ret, cel, bel) ->
+ let return = match ret with
+ | None -> []
+ | Some r -> [xmlReturn [pp_expr r]] in
+ xmlApply loc
+ (xmlOperator "match" loc ~attr:["style", (string_of_case_style sty)] ::
+ (return @
+ [Element ("scrutinees", [], List.map pp_case_expr cel)] @
+ [pp_branch_expr_list bel]))
+ | CRecord (_, _) -> assert false
+ | CLetIn (loc, (varloc, var), value, body) ->
+ xmlApply loc
+ (xmlOperator "let" loc ::
+ [xmlCst (string_of_name var) varloc; pp_expr value; pp_expr body])
+ | CLambdaN (loc, bl, e) ->
+ xmlApply loc
+ (xmlOperator "lambda" loc :: [pp_bindlist bl] @ [pp_expr e])
+ | CCoFix (_, _, _) -> assert false
+ | CFix (loc, lid, fel) ->
+ xmlApply loc
+ (xmlOperator "fix" loc ::
+ 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 v loc =
+ 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 e loc])
+ | VernacRedirect (s, (loc,e)) ->
+ xmlApply loc (Element("redirect",["path", s],[]) ::
+ [tmpp e loc])
+ | VernacTimeout (s,e) ->
+ xmlApply loc (Element("timeout",["val",string_of_int s],[]) ::
+ [tmpp e loc])
+ | VernacFail e -> xmlApply loc (Element("fail",[],[]) :: [tmpp e loc])
+ | VernacError _ -> xmlWithLoc loc "error" [] []
+
+ (* Syntax *)
+ | VernacSyntaxExtension (_, ((_, name), sml)) ->
+ let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
+ xmlReservedNotation attrs name loc
+
+ | 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 (sc_attr @ attrs) name loc [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 (sc_attr @ attrs) name loc [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 str_dk str_id loc [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 str_tk str_id loc [pp_expr statement])
+ | VernacStartTheoremProof _ as x -> xmlTODO loc x
+ | VernacEndProof pe ->
+ begin
+ match pe with
+ | Admitted -> xmlQed loc
+ | Proved (_, Some ((_, id), Some tk)) ->
+ let nam = Id.to_string id in
+ let typ = Kindops.string_of_theorem_kind tk in
+ xmlQed ~attr:["name", nam; "type", typ] loc
+ | Proved (_, Some ((_, id), None)) ->
+ let nam = Id.to_string id in
+ xmlQed ~attr:["name", nam] loc
+ | Proved _ -> xmlQed loc
+ 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 kind loc 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 kind loc 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 attr loc
+ | 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 attrs name loc [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 = Option.map (xmlRawTactic "closingtactic") tac 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 e loc])
+ | VernacLocal (b,e) ->
+ xmlApply loc (Element("local",["flag",string_of_bool b],[]) ::
+ [tmpp e loc])
+
+let tmpp v loc =
+ match tmpp v loc with
+ | Element("ltac",_,_) as x -> x
+ | xml -> xmlGallina loc [xml]
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-05 22:03:06 +0000