| "_" -> Cic.Anonymous
| s -> Cic.Name s
+let string_of_name = function
+ | Cic.Anonymous -> "_"
+ | Cic.Name s -> s
+
let int_opt = function
| None -> None
| Some lexeme -> Some (int_of_string lexeme)
];
typed_name: [
[ PAREN "("; i = IDENT; SYMBOL ":"; typ = term; PAREN ")" ->
- (name_of_string i, Some typ)
- | i = IDENT -> (name_of_string i, None)
+ (Cic.Name i, Some typ)
+ | i = IDENT -> (Cic.Name i, None)
]
];
subst: [
(head, vars)
]
];
+ let_defs:[
+ [ defs = LIST1 [
+ var = typed_name;
+ args = LIST1 [
+ PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":";
+ ty = term; PAREN ")" ->
+ (names, ty)
+ ];
+ index_name = OPT [ IDENT "on"; idx = IDENT -> idx ];
+ SYMBOL <:unicode<def>> (* ≝ *);
+ t1 = term ->
+ let rec list_of_lambda ty final_term = function
+ | [] -> final_term
+ | name::tl ->
+ CicAst.Binder (`Lambda, (Cic.Name name, Some ty),
+ list_of_lambda ty final_term tl)
+ in
+ let rec lambda_of_arg_list final_term = function
+ | [] -> final_term
+ | (l,ty)::tl ->
+ list_of_lambda ty (lambda_of_arg_list final_term tl) l
+ in
+ let t1' = lambda_of_arg_list t1 args in
+ let rec get_position_of name n = function
+ | [] -> (None,n)
+ | nam::tl ->
+ if nam = name then
+ (Some n,n)
+ else
+ (get_position_of name (n+1) tl)
+ in
+ let rec find_arg name n = function
+ | [] -> (fail loc (sprintf "Argument %s not found" name))
+ | (l,_)::tl ->
+ let (got,len) = get_position_of name 0 l in
+ (match got with
+ | None -> (find_arg name (n+len) tl)
+ | Some where -> n + where)
+ in
+ let index =
+ (match index_name with
+ | None -> 0
+ | (Some name) -> find_arg name 0 args)
+ in
+ (var, t1', index)
+ ] SEP "and" -> defs
+ ]];
constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
term0: [ [ t = term; EOI -> return_term loc t ] ];
term:
[ "letin" NONA
[ "let"; var = typed_name;
- SYMBOL "="; (* SYMBOL <:unicode<def>> (* ≝ *); *)
+ SYMBOL <:unicode<def>> (* ≝ *);
t1 = term; "in"; t2 = term ->
return_term loc (CicAst.LetIn (var, t1, t2))
| "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
- defs = LIST1 [
- var = typed_name;
- index = OPT [ PAREN "("; index = NUM; PAREN ")" ->
- int_of_string index
- ];
- SYMBOL "="; (* SYMBOL <:unicode<def>> (* ≝ *); *)
- t1 = term ->
- (var, t1, (match index with None -> 0 | Some i -> i))
- ] SEP "and";
- "in"; body = term ->
+ defs = let_defs; "in"; body = term ->
return_term loc (CicAst.LetRec (ind_kind, defs, body))
]
| "binder" RIGHTA
"with";
PAREN "[";
patterns = LIST0 [
- lhs = pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *); rhs = term ->
+ lhs = pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *); rhs = term
+ ->
((lhs: CicAst.case_pattern), rhs)
] SEP SYMBOL "|";
PAREN "]" ->
let ind_types = fst_ind_type :: tl_ind_types in
(params, ind_types)
] ];
+ print_kind: [
+ [ [ IDENT "Env" | IDENT "env" | IDENT "Environment" | IDENT "environment" ]
+ -> `Env
+ ] ];
+
command: [
[ [ IDENT "abort" | IDENT "Abort" ] -> return_command loc TacticAst.Abort
| [ IDENT "proof" | IDENT "Proof" ] -> return_command loc TacticAst.Proof
| [ IDENT "quit" | IDENT "Quit" ] -> return_command loc TacticAst.Quit
| [ IDENT "qed" | IDENT "Qed" ] ->
return_command loc (TacticAst.Qed None)
+ | [ IDENT "print" | IDENT "Print" ];
+ print_kind = print_kind ->
+ return_command loc (TacticAst.Print print_kind)
| [ IDENT "save" | IDENT "Save" ]; name = IDENT ->
return_command loc (TacticAst.Qed (Some name))
| flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
return_command loc (TacticAst.Theorem (flavour, name, typ, body))
+ | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
+ defs = let_defs ->
+ let name,ty =
+ match defs with
+ | ((Cic.Name name,Some ty),_,_) :: _ -> name,ty
+ | ((Cic.Name name,None),_,_) :: _ ->
+ fail loc ("No type given for " ^ name)
+ | _ -> assert false
+ in
+ let body = CicAst.Ident (name,None) in
+ TacticAst.Theorem(`Definition, Some name, ty,
+ Some (CicAst.LetRec (ind_kind, defs, body)))
+
| [ IDENT "inductive" | IDENT "Inductive" ]; spec = inductive_spec ->
let (params, ind_types) = spec in
return_command loc (TacticAst.Inductive (params, ind_types))
exception Try_again
let debug = false
+let debug = true
let debug_print = if debug then prerr_endline else ignore
(*
let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
try
snd (Environment.find item env) env num args
- with Not_found -> assert false
+ with Not_found ->
+ failwith ("Domain item not found: " ^
+ (DisambiguateTypes.string_of_domain_item item))
(* TODO move it to Cic *)
let find_in_environment name context =
contentTable.cmi: cicAst.cmi
acic2Ast.cmi: cicAst.cmi
cicAstPp.cmi: cicAst.cmi
-ast2pres.cmi: mpresentation.cmi cicAst.cmi box.cmi
-content2pres.cmi: mpresentation.cmi box.cmi
-sequent2pres.cmi: mpresentation.cmi box.cmi
-tacticAstPp.cmi: tacticAst.cmo cicAst.cmi
-boxPp.cmi: cicAst.cmi box.cmi
-tacticAst2Box.cmi: tacticAst.cmo cicAst.cmi box.cmi
+ast2pres.cmi: box.cmi cicAst.cmi mpresentation.cmi
+content2pres.cmi: box.cmi mpresentation.cmi
+sequent2pres.cmi: box.cmi mpresentation.cmi
+tacticAstPp.cmi: cicAst.cmi tacticAst.cmo
+boxPp.cmi: box.cmi cicAst.cmi
+tacticAst2Box.cmi: box.cmi cicAst.cmi tacticAst.cmo
tacticAst.cmo: cicAst.cmi
tacticAst.cmx: cicAst.cmx
cicAst.cmo: cicAst.cmi
acic2Ast.cmx: cicAst.cmx acic2Ast.cmi
cicAstPp.cmo: cicAst.cmi cicAstPp.cmi
cicAstPp.cmx: cicAst.cmx cicAstPp.cmi
-ast2pres.cmo: mpresentation.cmi cicAst.cmi box.cmi ast2pres.cmi
-ast2pres.cmx: mpresentation.cmx cicAst.cmx box.cmx ast2pres.cmi
-content2pres.cmo: mpresentation.cmi box.cmi ast2pres.cmi acic2Ast.cmi \
+ast2pres.cmo: box.cmi cicAst.cmi mpresentation.cmi ast2pres.cmi
+ast2pres.cmx: box.cmx cicAst.cmx mpresentation.cmx ast2pres.cmi
+content2pres.cmo: acic2Ast.cmi ast2pres.cmi box.cmi mpresentation.cmi \
content2pres.cmi
-content2pres.cmx: mpresentation.cmx box.cmx ast2pres.cmx acic2Ast.cmx \
+content2pres.cmx: acic2Ast.cmx ast2pres.cmx box.cmx mpresentation.cmx \
content2pres.cmi
-sequent2pres.cmo: mpresentation.cmi box.cmi ast2pres.cmi acic2Ast.cmi \
+sequent2pres.cmo: acic2Ast.cmi ast2pres.cmi box.cmi mpresentation.cmi \
sequent2pres.cmi
-sequent2pres.cmx: mpresentation.cmx box.cmx ast2pres.cmx acic2Ast.cmx \
+sequent2pres.cmx: acic2Ast.cmx ast2pres.cmx box.cmx mpresentation.cmx \
sequent2pres.cmi
misc.cmo: misc.cmi
misc.cmx: misc.cmi
xml2Gdome.cmx: xml2Gdome.cmi
sequentPp.cmo: cic2Xml.cmi sequentPp.cmi
sequentPp.cmx: cic2Xml.cmx sequentPp.cmi
-applyStylesheets.cmo: xml2Gdome.cmi sequentPp.cmi misc.cmi cic2Xml.cmi \
- applyStylesheets.cmi
-applyStylesheets.cmx: xml2Gdome.cmx sequentPp.cmx misc.cmx cic2Xml.cmx \
- applyStylesheets.cmi
-applyTransformation.cmo: xml2Gdome.cmi sequent2pres.cmi mpresentation.cmi \
- misc.cmi content2pres.cmi box.cmi ast2pres.cmi applyTransformation.cmi
-applyTransformation.cmx: xml2Gdome.cmx sequent2pres.cmx mpresentation.cmx \
- misc.cmx content2pres.cmx box.cmx ast2pres.cmx applyTransformation.cmi
-tacticAstPp.cmo: tacticAst.cmo cicAstPp.cmi tacticAstPp.cmi
-tacticAstPp.cmx: tacticAst.cmx cicAstPp.cmx tacticAstPp.cmi
-boxPp.cmo: cicAstPp.cmi box.cmi ast2pres.cmi boxPp.cmi
-boxPp.cmx: cicAstPp.cmx box.cmx ast2pres.cmx boxPp.cmi
-tacticAst2Box.cmo: tacticAstPp.cmi tacticAst.cmo cicAstPp.cmi boxPp.cmi \
- box.cmi ast2pres.cmi tacticAst2Box.cmi
-tacticAst2Box.cmx: tacticAstPp.cmx tacticAst.cmx cicAstPp.cmx boxPp.cmx \
- box.cmx ast2pres.cmx tacticAst2Box.cmi
+applyTransformation.cmo: ast2pres.cmi box.cmi content2pres.cmi misc.cmi \
+ mpresentation.cmi sequent2pres.cmi xml2Gdome.cmi applyTransformation.cmi
+applyTransformation.cmx: ast2pres.cmx box.cmx content2pres.cmx misc.cmx \
+ mpresentation.cmx sequent2pres.cmx xml2Gdome.cmx applyTransformation.cmi
+tacticAstPp.cmo: cicAstPp.cmi tacticAst.cmo tacticAstPp.cmi
+tacticAstPp.cmx: cicAstPp.cmx tacticAst.cmx tacticAstPp.cmi
+boxPp.cmo: ast2pres.cmi box.cmi cicAstPp.cmi boxPp.cmi
+boxPp.cmx: ast2pres.cmx box.cmx cicAstPp.cmx boxPp.cmi
+tacticAst2Box.cmo: ast2pres.cmi box.cmi boxPp.cmi cicAstPp.cmi tacticAst.cmo \
+ tacticAstPp.cmi tacticAst2Box.cmi
+tacticAst2Box.cmx: ast2pres.cmx box.cmx boxPp.cmx cicAstPp.cmx tacticAst.cmx \
+ tacticAstPp.cmx tacticAst2Box.cmi
cicAstPp.mli ast2pres.mli content2pres.mli \
sequent2pres.mli \
misc.mli xml2Gdome.mli sequentPp.mli \
- applyStylesheets.mli applyTransformation.mli \
+ applyTransformation.mli \
tacticAstPp.mli boxPp.mli tacticAst2Box.mli
IMPLEMENTATION_FILES = \
tacticAst.ml \
+++ /dev/null
-(* Copyright (C) 2000-2002, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(******************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* 30/01/2002 *)
-(* *)
-(* *)
-(******************************************************************************)
-
-(** stylesheets and parameters list **)
-
-let parseStyle name =
- let style =
- Misc.domImpl#createDocumentFromURI
- (* ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None *)
- ~uri:("styles/" ^ name) ()
- in
- Gdome_xslt.processStylesheet style
-;;
-
-let parseStyles () =
- parseStyle "drop_coercions.xsl",
- parseStyle "objtheorycontent.xsl",
- parseStyle "content_to_html.xsl",
- parseStyle "link.xsl",
- parseStyle "rootcontent.xsl",
- parseStyle "genmmlid.xsl",
- parseStyle "annotatedpres.xsl"
-;;
-
-let (d_c,tc1,hc2,l,c1,g,c2) =
- let (d_c,tc1,hc2,l,c1,g,c2) = parseStyles () in
- ref d_c, ref tc1, ref hc2, ref l, ref c1, ref g, ref c2
-;;
-
-let reload_stylesheets () =
- let (d_c',tc1',hc2',l',c1',g',c2') = parseStyles () in
- d_c := d_c';
- tc1 := tc1';
- hc2 := hc2';
- l := l' ;
- c1 := c1' ;
- g := g' ;
- c2 := c2'
-;;
-
-
-let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
-let mml_args ~explode_all =
- ("explodeall",(if explode_all then "true()" else "false()"))::
- ["processorURL", "'" ^ Helm_registry.get "uwobo.url" ^ "'" ;
- "getterURL", "'" ^ Helm_registry.get "getter.url" ^ "'" ;
- "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
- "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
- "UNICODEvsSYMBOL", "'symbol'" ;
- "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
- "encoding", "'iso-8859-1'" ;
- "media-type", "'text/html'" ;
- "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
- "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
- "naturalLanguage", "'yes'" ;
- "annotations", "'no'" ;
- "URLs_or_URIs", "'URIs'" ;
- "topurl", "'http://phd.cs.unibo.it/helm'" ;
- "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
-;;
-
-let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
-let sequent_args () =
- ["processorURL", "'" ^ Helm_registry.get "uwobo.url" ^ "'" ;
- "getterURL", "'" ^ Helm_registry.get "getter.url" ^ "'" ;
- "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
- "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
- "UNICODEvsSYMBOL", "'symbol'" ;
- "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
- "encoding", "'iso-8859-1'" ;
- "media-type", "'text/html'" ;
- "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
- "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
- "naturalLanguage", "'no'" ;
- "annotations", "'no'" ;
- "explodeall", "true()" ;
- "URLs_or_URIs", "'URIs'" ;
- "topurl", "'http://phd.cs.unibo.it/helm'" ;
- "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
-;;
-
-(** Stylesheets application **)
-
-let apply_stylesheets input styles args =
- List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i !style args)
- input styles
-;;
-
-let apply_proof_stylesheets proof_doc ~explode_all =
- apply_stylesheets proof_doc mml_styles (mml_args ~explode_all)
-;;
-
-let apply_sequent_stylesheets sequent_doc =
- apply_stylesheets sequent_doc sequent_styles (sequent_args ())
-;;
-
-(** Utility functions to map objects to MathML Presentation **)
-
-(*CSC: the getter should handle the innertypes, not the FS *)
-
-let innertypesfile () = Helm_registry.get "gtoplevel.inner_types_file";;
-let constanttypefile () = Helm_registry.get "gtoplevel.constant_type_file";;
-
-let mml_of_cic_sequent metasenv sequent =
- let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
- SequentPp.XmlPp.print_sequent metasenv sequent in
- let sequent_doc =
- Xml2Gdome.document_of_xml Misc.domImpl sequent_gdome in
- let sequent_mml = apply_sequent_stylesheets sequent_doc in
- sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
-;;
-
-let
- mml_of_cic_object ~explode_all uri annobj ids_to_inner_sorts ids_to_inner_types
-=
-(*CSC: ????????????????? *)
- let xml, bodyxml =
- Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:true
- annobj
- in
- let xmlinnertypes =
- Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
- ~ask_dtd_to_the_getter:true
- in
- let input =
- match bodyxml with
- None -> Xml2Gdome.document_of_xml Misc.domImpl xml
- | Some bodyxml' ->
- Xml.pp xml (Some (constanttypefile ())) ;
- Xml2Gdome.document_of_xml Misc.domImpl bodyxml'
- in
-(*CSC: We save the innertypes to disk so that we can retrieve them in the *)
-(*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
-(*CSC: local. *)
- Xml.pp xmlinnertypes (Some (innertypesfile ())) ;
- let output = apply_proof_stylesheets input ~explode_all in
- output
-;;
-
-
-
-
-
+++ /dev/null
-(* Copyright (C) 2000-2002, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(******************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* 15/01/2003 *)
-(* *)
-(* *)
-(******************************************************************************)
-
-val reload_stylesheets : unit -> unit
-
-val mml_of_cic_sequent :
- Cic.metasenv ->
- int * Cic.context * Cic.term ->
- Gdome.document *
- ((Cic.id, Cic.term) Hashtbl.t *
- (Cic.id, Cic.id option) Hashtbl.t *
- (string, Cic.hypothesis) Hashtbl.t)
-
-val mml_of_cic_object :
- explode_all:bool ->
- UriManager.uri ->
- Cic.annobj ->
- (string, string) Hashtbl.t ->
- (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document
type search_kind = [ `Locate | `Hint | `Match | `Elim ]
+type print_kind = [ `Env ]
+
type 'term command =
| Abort
| Baseuri of string option (** get/set base uri *)
| Coercion of 'term
| Redo of int option
| Undo of int option
+ | Print of print_kind
type ('term, 'ident) tactical =
| LocatedTactical of CicAst.location * ('term, 'ident) tactical
(* stupid case *)
-
+(*
let l = close_coercion_graph
(UriManager.uri_of_string
"cic:/CoRN/algebra/CRings/CRing.ind#xpointer(1/1)")
prerr_endline (UriManager.string_of_uri u);
prerr_endline "")
l
-
+*)
(* EOF *)
projects / helm.git / commitdiff