From b82e303159a8f1a96c80de9ca8f88363c81c9dc6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 14 Mar 2003 18:53:03 +0000 Subject: [PATCH] First committed version of the textual parser able to parse TeX syntax. (This should be the second release of the parser, but the first one was never committed.) --- .../META.helm-tex_cic_textual_parser.src | 5 + helm/ocaml/Makefile.in | 5 +- helm/ocaml/tex_cic_textual_parser/Makefile | 14 + .../texCicTextualLexer.mll | 103 +++ .../texCicTextualParser.mly | 586 ++++++++++++++++++ .../texCicTextualParser0.ml | 27 + .../texCicTextualParserContext.ml | 36 ++ .../texCicTextualParserContext.mli | 31 + 8 files changed, 805 insertions(+), 2 deletions(-) create mode 100644 helm/ocaml/META.helm-tex_cic_textual_parser.src create mode 100644 helm/ocaml/tex_cic_textual_parser/Makefile create mode 100644 helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll create mode 100644 helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly create mode 100644 helm/ocaml/tex_cic_textual_parser/texCicTextualParser0.ml create mode 100644 helm/ocaml/tex_cic_textual_parser/texCicTextualParserContext.ml create mode 100644 helm/ocaml/tex_cic_textual_parser/texCicTextualParserContext.mli diff --git a/helm/ocaml/META.helm-tex_cic_textual_parser.src b/helm/ocaml/META.helm-tex_cic_textual_parser.src new file mode 100644 index 000000000..dec21eebd --- /dev/null +++ b/helm/ocaml/META.helm-tex_cic_textual_parser.src @@ -0,0 +1,5 @@ +requires="helm-cic" +version="0.0.1" +archive(byte)="tex_cic_textual_parser.cma" +archive(native)="tex_cic_textual_parser.cmxa" +linkopts="" diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index 0996f7497..d5917ee50 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -1,7 +1,8 @@ # Warning: the modules must be in compilation order MODULES = xml urimanager getter pxp cic cic_annotations cic_annotations_cache \ - cic_cache cic_proof_checking cic_textual_parser cic_unification \ - mathql mathql_interpreter mquery_generator tactics + cic_cache cic_proof_checking cic_textual_parser \ + tex_cic_textual_parser cic_unification mathql mathql_interpreter \ + mquery_generator tactics OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@ OCAMLFIND_META_DIR = @OCAMLFIND_META_DIR@ diff --git a/helm/ocaml/tex_cic_textual_parser/Makefile b/helm/ocaml/tex_cic_textual_parser/Makefile new file mode 100644 index 000000000..b57b3a8ba --- /dev/null +++ b/helm/ocaml/tex_cic_textual_parser/Makefile @@ -0,0 +1,14 @@ +PACKAGE = tex_cic_textual_parser +REQUIRES = helm-cic helm-cic_textual_parser +PREDICATES = + +INTERFACE_FILES = texCicTextualParser.mli texCicTextualParserContext.mli +IMPLEMENTATION_FILES = texCicTextualParser0.ml $(INTERFACE_FILES:%.mli=%.ml) \ + texCicTextualLexer.ml +EXTRA_OBJECTS_TO_INSTALL = texCicTextualParser0.ml texCicTextualParser0.cmi \ + texCicTextualLexer.mll texCicTextualParser.mly + +EXTRA_OBJECTS_TO_CLEAN = texCicTextualParser.ml texCicTextualParser.mli \ + texCicTextualLexer.ml + +include ../Makefile.common diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll new file mode 100644 index 000000000..d40f09fb2 --- /dev/null +++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll @@ -0,0 +1,103 @@ +(* Copyright (C) 2000, 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/. + *) + +{ + open TexCicTextualParser;; + module L = Lexing;; + module U = UriManager;; + + let indtyuri_of_uri uri = + let index_sharp = String.index uri '#' in + let index_num = index_sharp + 3 in + (UriManager.uri_of_string (String.sub uri 0 index_sharp), + int_of_string (String.sub uri index_num (String.length uri - index_num)) - 1 + ) + ;; + + let indconuri_of_uri uri = + let index_sharp = String.index uri '#' in + let index_div = String.rindex uri '/' in + let index_con = index_div + 1 in + (UriManager.uri_of_string (String.sub uri 0 index_sharp), + int_of_string + (String.sub uri (index_sharp + 3) (index_div - index_sharp - 3)) - 1, + int_of_string + (String.sub uri index_con (String.length uri - index_con)) + ) + ;; +} +let dollar = '$' +let num = ['1'-'9']['0'-'9']* | '0' +let alfa = ['A'-'Z' 'a'-'z' '_' ''' '-'] | "\\_" +let ident = alfa (alfa | num)* +let baseuri = '/'(ident '/')* ident '.' +let conuri = baseuri "con" +let varuri = baseuri "var" +let indtyuri = baseuri "ind#1/" num +let indconuri = baseuri "ind#1/" num "/" num +let blanks = [' ' '\t' '\n' '~'] | "\\;" +rule token = + parse + blanks { token lexbuf } (* skip blanks *) + | "\\Case" { CASE } + | "\\Fix" { FIX } + | "\\CoFix" { COFIX } + | "\\Set" { SET } + | "\\Prop" { PROP } + | "\\Type" { TYPE } + | ident { ID (L.lexeme lexbuf) } + | conuri { CONURI (U.uri_of_string ("cic:" ^ L.lexeme lexbuf)) } + | varuri { VARURI (U.uri_of_string ("cic:" ^ L.lexeme lexbuf)) } + | indtyuri { INDTYURI (indtyuri_of_uri ("cic:" ^ L.lexeme lexbuf)) } + | indconuri { INDCONURI (indconuri_of_uri("cic:" ^ L.lexeme lexbuf)) } + | num { NUM (int_of_string (L.lexeme lexbuf)) } + | '?' num { let lexeme = L.lexeme lexbuf in + META + (int_of_string + (String.sub lexeme 1 (String.length lexeme - 1))) } + | ":>" { CAST } + | ":=" { LETIN } + | '?' { IMPLICIT } + | '(' { LPAREN } + | ')' { RPAREN } + | "\\[" { LBRACKET } + | "\\]" { RBRACKET } + | "\\{" { LCURLY } + | "\\}" { RCURLY } + | ';' { SEMICOLON } + | "\\lambda" { LAMBDA } + | "\\pi" { PROD } + | "\\forall" { PROD } + | ':' { COLON } + | '.' { DOT } + | "\\to" { ARROW } + | '_' { NONE } + | dollar { DOLLAR } + | eof { EOF } + (* Arithmetical operators *) + | '+' { PLUS } + | '*' { TIMES } + | '=' { EQ } +{} diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly new file mode 100644 index 000000000..245485922 --- /dev/null +++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly @@ -0,0 +1,586 @@ +/* Copyright (C) 2000, 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/. + */ + +%{ + open Cic;; + module U = UriManager;; + + exception InvalidSuffix of string;; + exception InductiveTypeURIExpected;; + exception UnknownIdentifier of string;; + exception ExplicitNamedSubstitutionAppliedToRel;; + exception TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable;; + + (* merge removing duplicates of two lists free of duplicates *) + let union dom1 dom2 = + let rec filter = + function + [] -> [] + | he::tl -> + if List.mem he dom1 then filter tl else he::(filter tl) + in + dom1 @ (filter dom2) + ;; + + let get_index_in_list e = + let rec aux i = + function + [] -> raise Not_found + | (Some he)::_ when he = e -> i + | _::tl -> aux (i+1) tl + in + aux 1 + ;; + + (* Returns the first meta whose number is above the *) + (* number of the higher meta. *) + (*CSC: cut&pasted from proofEngine.ml *) + let new_meta () = + let rec aux = + function + None,[] -> 1 + | Some n,[] -> n + | None,(n,_,_)::tl -> aux (Some n,tl) + | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl) + in + 1 + aux (None,!TexCicTextualParser0.metasenv) + ;; + + (* identity_relocation_list_for_metavariable i canonical_context *) + (* returns the identity relocation list, which is the list [1 ; ... ; n] *) + (* where n = List.length [canonical_context] *) + (*CSC: ma mi basta la lunghezza del contesto canonico!!!*) + (*CSC: cut&pasted from proofEngine.ml *) + let identity_relocation_list_for_metavariable canonical_context = + let canonical_context_length = List.length canonical_context in + let rec aux = + function + (_,[]) -> [] + | (n,None::tl) -> None::(aux ((n+1),tl)) + | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl)) + in + aux (1,canonical_context) + ;; + + let deoptionize_exp_named_subst = + function + None -> [], (function _ -> []) + | Some (dom,mk_exp_named_subst) -> dom,mk_exp_named_subst + ;; + + let term_of_con_uri uri exp_named_subst = + Const (uri,exp_named_subst) + ;; + + let term_of_var_uri uri exp_named_subst = + Var (uri,exp_named_subst) + ;; + + let term_of_indty_uri (uri,tyno) exp_named_subst = + MutInd (uri, tyno, exp_named_subst) + ;; + + let term_of_indcon_uri (uri,tyno,consno) exp_named_subst = + MutConstruct (uri, tyno, consno, exp_named_subst) + ;; + + let term_of_uri uri = + match uri with + CicTextualParser0.ConUri uri -> + term_of_con_uri uri + | CicTextualParser0.VarUri uri -> + term_of_var_uri uri + | CicTextualParser0.IndTyUri (uri,tyno) -> + term_of_indty_uri (uri,tyno) + | CicTextualParser0.IndConUri (uri,tyno,consno) -> + term_of_indcon_uri (uri,tyno,consno) + ;; + + let var_uri_of_id id interp = + let module CTP0 = CicTextualParser0 in + match interp (CicTextualParser0.Id id) with + None -> raise (UnknownIdentifier id) + | Some (CTP0.Uri (CTP0.VarUri uri)) -> uri + | Some _ -> raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable + ;; + + let indty_uri_of_id id interp = + let module CTP0 = CicTextualParser0 in + match interp (CicTextualParser0.Id id) with + None -> raise (UnknownIdentifier id) + | Some (CTP0.Uri (CTP0.IndTyUri (uri,tyno))) -> (uri,tyno) + | Some _ -> raise InductiveTypeURIExpected + ;; + + let mk_implicit () = + let newmeta = new_meta () in + let new_canonical_context = [] in + let irl = + identity_relocation_list_for_metavariable new_canonical_context + in + TexCicTextualParser0.metasenv := + [newmeta, new_canonical_context, Sort Type ; + newmeta+1, new_canonical_context, Meta (newmeta,irl); + newmeta+2, new_canonical_context, Meta (newmeta+1,irl) + ] @ !TexCicTextualParser0.metasenv ; + [], function _ -> Meta (newmeta+2,irl) + ;; +%} +%token ID +%token META +%token NUM +%token CONURI +%token VARURI +%token INDTYURI +%token INDCONURI +%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT NONE +%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF +%token DOLLAR +%token PLUS TIMES EQ +%right ARROW +%right EQ +%right PLUS +%right TIMES +%start main +%type Cic.term)> main +%% +main: + | EOF { raise CicTextualParser0.Eof } /* FG: was never raised */ + | DOLLAR DOLLAR EOF {raise CicTextualParser0.Eof } + | DOLLAR DOLLAR DOLLAR DOLLAR EOF {raise CicTextualParser0.Eof } + | expr EOF { $1 } + | DOLLAR expr DOLLAR EOF { $2 } + | DOLLAR DOLLAR expr DOLLAR DOLLAR EOF { $3 } + | expr SEMICOLON { $1 } /* FG: to read several terms in a row + * Do we need to clear some static variables? + */ +; +expr2: + NUM + { [], function interp -> + let rec cic_int_of_int = + function + 0 -> + Cic.MutConstruct + (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind", + 0,1,[]) + | n -> + Cic.Appl + [ Cic.MutConstruct + (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind", + 0,2,[]) ; + cic_int_of_int (n - 1) + ] + in + cic_int_of_int $1 + } + | expr2 PLUS expr2 + { let dom1,mk_expr1 = $1 in + let dom2,mk_expr2 = $3 in + let dom = union dom1 dom2 in + dom, function interp -> + Cic.Appl + [Cic.Const + (UriManager.uri_of_string "cic:/Coq/Init/Peano/plus.con",[]) ; + (mk_expr1 interp) ; + (mk_expr2 interp) + ] + } + | expr2 TIMES expr2 + { let dom1,mk_expr1 = $1 in + let dom2,mk_expr2 = $3 in + let dom = union dom1 dom2 in + dom, function interp -> + Cic.Appl + [Cic.Const + (UriManager.uri_of_string "cic:/Coq/Init/Peano/mult.con",[]) ; + (mk_expr1 interp) ; + (mk_expr2 interp) + ] + } + | expr2 EQ expr2 + { let dom1,mk_expr1 = $1 in + let dom2,mk_expr2 = $3 in + let dom3,mk_expr3 = mk_implicit () in + let dom = union dom1 (union dom2 dom3) in + dom, function interp -> + Cic.Appl + [Cic.MutInd + (UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind",0,[]) ; + (mk_expr3 interp) ; + (mk_expr1 interp) ; + (mk_expr2 interp) + ] + } + | CONURI exp_named_subst + { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in + dom, function interp -> term_of_con_uri $1 (mk_exp_named_subst interp) + } + | VARURI exp_named_subst + { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in + dom, function interp -> term_of_var_uri $1 (mk_exp_named_subst interp) + } + | INDTYURI exp_named_subst + { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in + dom, function interp -> term_of_indty_uri $1 (mk_exp_named_subst interp) + } + | INDCONURI exp_named_subst + { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in + dom, function interp -> term_of_indcon_uri $1 (mk_exp_named_subst interp) + } + | ID exp_named_subst + { try + let res = + Rel (get_index_in_list (Name $1) !TexCicTextualParser0.binders) + in + (match $2 with + None -> ([], function _ -> res) + | Some _ -> raise (ExplicitNamedSubstitutionAppliedToRel) + ) + with + Not_found -> + let dom1,mk_exp_named_subst = deoptionize_exp_named_subst $2 in + let dom = union dom1 [CicTextualParser0.Id $1] in + dom, + function interp -> + match interp (CicTextualParser0.Id $1) with + None -> raise (UnknownIdentifier $1) + | Some (CicTextualParser0.Uri uri) -> + term_of_uri uri (mk_exp_named_subst interp) + | Some CicTextualParser0.Implicit -> + (*CSC: not very clean; to maximize code reusage *) + snd (mk_implicit ()) "" + | Some (CicTextualParser0.Term mk_term) -> + (mk_term interp) + } + | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY + { let dom1,mk_expr1 = $3 in + let dom2,mk_expr2 = $7 in + let dom3,mk_expr3 = $10 in + let dom = union dom1 (union dom2 dom3) in + dom, + function interp -> + MutCase + (fst $5,snd $5,(mk_expr2 interp),(mk_expr1 interp),(mk_expr3 interp)) + } + | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY + { let dom1,mk_expr1 = $3 in + let dom2,mk_expr2 = $7 in + let dom3,mk_expr3 = $10 in + let dom = + union [CicTextualParser0.Id $5] (union dom1 (union dom2 dom3)) + in + dom, + function interp -> + let uri,typeno = indty_uri_of_id $5 interp in + MutCase + (uri,typeno,(mk_expr2 interp),(mk_expr1 interp), + (mk_expr3 interp)) + } + | fixheader LCURLY exprseplist RCURLY + { let dom1,foo,ids_and_indexes,mk_types = $1 in + let dom2,mk_exprseplist = $3 in + let dom = union dom1 dom2 in + for i = 1 to List.length ids_and_indexes do + TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders + done ; + dom, + function interp -> + let types = mk_types interp in + let fixfunsbodies = (mk_exprseplist interp) in + let idx = + let rec find idx = + function + [] -> raise Not_found + | (name,_)::_ when name = foo -> idx + | _::tl -> find (idx+1) tl + in + find 0 ids_and_indexes + in + let fixfuns = + List.map2 (fun ((name,recindex),ty) bo -> (name,recindex,ty,bo)) + (List.combine ids_and_indexes types) fixfunsbodies + in + Fix (idx,fixfuns) + } + | cofixheader LCURLY exprseplist RCURLY + { let dom1,foo,ids,mk_types = $1 in + let dom2,mk_exprseplist = $3 in + let dom = union dom1 dom2 in + dom, + function interp -> + let types = mk_types interp in + let fixfunsbodies = (mk_exprseplist interp) in + let idx = + let rec find idx = + function + [] -> raise Not_found + | name::_ when name = foo -> idx + | _::tl -> find (idx+1) tl + in + find 0 ids + in + let fixfuns = + List.map2 (fun (name,ty) bo -> (name,ty,bo)) + (List.combine ids types) fixfunsbodies + in + for i = 1 to List.length fixfuns do + TexCicTextualParser0.binders := + List.tl !TexCicTextualParser0.binders + done ; + CoFix (idx,fixfuns) + } + | IMPLICIT + { mk_implicit () } + | SET { [], function _ -> Sort Set } + | PROP { [], function _ -> Sort Prop } + | TYPE { [], function _ -> Sort Type } + | LPAREN expr CAST expr RPAREN + { let dom1,mk_expr1 = $2 in + let dom2,mk_expr2 = $4 in + let dom = union dom1 dom2 in + dom, function interp -> Cast ((mk_expr1 interp),(mk_expr2 interp)) + } + | META LBRACKET substitutionlist RBRACKET + { let dom,mk_substitutionlist = $3 in + dom, function interp -> Meta ($1, mk_substitutionlist interp) + } + | LPAREN expr exprlist RPAREN + { let length,dom2,mk_exprlist = $3 in + match length with + 0 -> $2 + | _ -> + let dom1,mk_expr1 = $2 in + let dom = union dom1 dom2 in + dom, + function interp -> + Appl ((mk_expr1 interp)::(mk_exprlist interp)) + } +; +exp_named_subst : + { None } + | LCURLY named_substs RCURLY + { Some $2 } +; +named_substs : + VARURI LETIN expr2 + { let dom,mk_expr = $3 in + dom, function interp -> [$1, mk_expr interp] } + | ID LETIN expr2 + { let dom1,mk_expr = $3 in + let dom = union [CicTextualParser0.Id $1] dom1 in + dom, function interp -> [var_uri_of_id $1 interp, mk_expr interp] } + | VARURI LETIN expr2 SEMICOLON named_substs + { let dom1,mk_expr = $3 in + let dom2,mk_named_substs = $5 in + let dom = union dom1 dom2 in + dom, function interp -> ($1, mk_expr interp)::(mk_named_substs interp) + } + | ID LETIN expr2 SEMICOLON named_substs + { let dom1,mk_expr = $3 in + let dom2,mk_named_substs = $5 in + let dom = union [CicTextualParser0.Id $1] (union dom1 dom2) in + dom, + function interp -> + (var_uri_of_id $1 interp, mk_expr interp)::(mk_named_substs interp) + } +; +expr : + pihead expr + { TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders ; + let dom1,mk_expr1 = snd $1 in + let dom2,mk_expr2 = $2 in + let dom = union dom1 dom2 in + dom, function interp -> Prod (fst $1, mk_expr1 interp, mk_expr2 interp) + } + | lambdahead expr + { TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders ; + let dom1,mk_expr1 = snd $1 in + let dom2,mk_expr2 = $2 in + let dom = union dom1 dom2 in + dom,function interp -> Lambda (fst $1, mk_expr1 interp, mk_expr2 interp) + } + | letinhead expr + { TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders ; + let dom1,mk_expr1 = snd $1 in + let dom2,mk_expr2 = $2 in + let dom = union dom1 dom2 in + dom, function interp -> LetIn (fst $1, mk_expr1 interp, mk_expr2 interp) + } + | expr2 + { $1 } +; +fixheader: + FIX ID LCURLY fixfunsdecl RCURLY + { let dom,ids_and_indexes,mk_types = $4 in + let bs = + List.rev_map (function (name,_) -> Some (Name name)) ids_and_indexes + in + TexCicTextualParser0.binders := bs@(!TexCicTextualParser0.binders) ; + dom, $2, ids_and_indexes, mk_types + } +; +fixfunsdecl: + ID LPAREN NUM RPAREN COLON expr + { let dom,mk_expr = $6 in + dom, [$1,$3], function interp -> [mk_expr interp] + } + | ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl + { let dom1,mk_expr = $6 in + let dom2,ids_and_indexes,mk_types = $8 in + let dom = union dom1 dom2 in + dom, ($1,$3)::ids_and_indexes, + function interp -> (mk_expr interp)::(mk_types interp) + } +; +cofixheader: + COFIX ID LCURLY cofixfunsdecl RCURLY + { let dom,ids,mk_types = $4 in + let bs = + List.rev_map (function name -> Some (Name name)) ids + in + TexCicTextualParser0.binders := bs@(!TexCicTextualParser0.binders) ; + dom, $2, ids, mk_types + } +; +cofixfunsdecl: + ID COLON expr + { let dom,mk_expr = $3 in + dom, [$1], function interp -> [mk_expr interp] + } + | ID COLON expr SEMICOLON cofixfunsdecl + { let dom1,mk_expr = $3 in + let dom2,ids,mk_types = $5 in + let dom = union dom1 dom2 in + dom, $1::ids, + function interp -> (mk_expr interp)::(mk_types interp) + } +; +pihead: + PROD ID COLON expr DOT + { TexCicTextualParser0.binders := + (Some (Name $2))::!TexCicTextualParser0.binders; + let dom,mk_expr = $4 in + Cic.Name $2, (dom, function interp -> mk_expr interp) + } + | expr2 ARROW + { TexCicTextualParser0.binders := + (Some Anonymous)::!TexCicTextualParser0.binders ; + let dom,mk_expr = $1 in + Anonymous, (dom, function interp -> mk_expr interp) + } + | PROD ID DOT + { TexCicTextualParser0.binders := + (Some (Name $2))::!TexCicTextualParser0.binders; + let newmeta = new_meta () in + let new_canonical_context = [] in + let irl = + identity_relocation_list_for_metavariable new_canonical_context + in + TexCicTextualParser0.metasenv := + [newmeta, new_canonical_context, Sort Type ; + newmeta+1, new_canonical_context, Meta (newmeta,irl) + ] @ !TexCicTextualParser0.metasenv ; + Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl)) + } +; +lambdahead: + LAMBDA ID COLON expr DOT + { TexCicTextualParser0.binders := + (Some (Name $2))::!TexCicTextualParser0.binders; + let dom,mk_expr = $4 in + Cic.Name $2, (dom, function interp -> mk_expr interp) + } + | LAMBDA ID DOT + { TexCicTextualParser0.binders := + (Some (Name $2))::!TexCicTextualParser0.binders; + let newmeta = new_meta () in + let new_canonical_context = [] in + let irl = + identity_relocation_list_for_metavariable new_canonical_context + in + TexCicTextualParser0.metasenv := + [newmeta, new_canonical_context, Sort Type ; + newmeta+1, new_canonical_context, Meta (newmeta,irl) + ] @ !TexCicTextualParser0.metasenv ; + Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl)) + } +; +letinhead: + LAMBDA ID LETIN expr DOT + { TexCicTextualParser0.binders := + (Some (Name $2))::!TexCicTextualParser0.binders ; + let dom,mk_expr = $4 in + Cic.Name $2, (dom, function interp -> mk_expr interp) + } +; +branches: + { [], function _ -> [] } + | expr SEMICOLON branches + { let dom1,mk_expr = $1 in + let dom2,mk_branches = $3 in + let dom = union dom1 dom2 in + dom, function interp -> (mk_expr interp)::(mk_branches interp) + } + | expr + { let dom,mk_expr = $1 in + dom, function interp -> [mk_expr interp] + } +; +exprlist: + + { 0, [], function _ -> [] } + | expr exprlist + { let dom1,mk_expr = $1 in + let length,dom2,mk_exprlist = $2 in + let dom = union dom1 dom2 in + length+1, dom, function interp -> (mk_expr interp)::(mk_exprlist interp) + } +; +exprseplist: + expr + { let dom,mk_expr = $1 in + dom, function interp -> [mk_expr interp] + } + | expr SEMICOLON exprseplist + { let dom1,mk_expr = $1 in + let dom2,mk_exprseplist = $3 in + let dom = union dom1 dom2 in + dom, function interp -> (mk_expr interp)::(mk_exprseplist interp) + } +; +substitutionlist: + { [], function _ -> [] } + | expr SEMICOLON substitutionlist + { let dom1,mk_expr = $1 in + let dom2,mk_substitutionlist = $3 in + let dom = union dom1 dom2 in + dom, + function interp ->(Some (mk_expr interp))::(mk_substitutionlist interp) + } + | NONE SEMICOLON substitutionlist + { let dom,mk_exprsubstitutionlist = $3 in + dom, function interp -> None::(mk_exprsubstitutionlist interp) + } diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser0.ml b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser0.ml new file mode 100644 index 000000000..133f2e0bb --- /dev/null +++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser0.ml @@ -0,0 +1,27 @@ +(* Copyright (C) 2000, 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/. + *) + +let binders = ref ([] : (Cic.name option) list);; +let metasenv = ref ([] : Cic.metasenv);; diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualParserContext.ml b/helm/ocaml/tex_cic_textual_parser/texCicTextualParserContext.ml new file mode 100644 index 000000000..28581bc58 --- /dev/null +++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualParserContext.ml @@ -0,0 +1,36 @@ +(* Copyright (C) 2000, 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/. + *) + +let main ~context ~metasenv lexer lexbuf = + (* Warning: higly non-reentrant code!!! *) + TexCicTextualParser0.binders := context ; + TexCicTextualParser0.metasenv := metasenv ; + let dom,mk_term = TexCicTextualParser.main lexer lexbuf in + dom, + function interp -> + let term = mk_term interp in + let metasenv = !TexCicTextualParser0.metasenv in + metasenv,term +;; diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualParserContext.mli b/helm/ocaml/tex_cic_textual_parser/texCicTextualParserContext.mli new file mode 100644 index 000000000..492b52d09 --- /dev/null +++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualParserContext.mli @@ -0,0 +1,31 @@ +(* Copyright (C) 2000, 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/. + *) + +val main : + context:((Cic.name option) list) -> + metasenv:Cic.metasenv -> + (Lexing.lexbuf -> TexCicTextualParser.token) -> Lexing.lexbuf -> + CicTextualParser0.interpretation_domain_item list * + (CicTextualParser0.interpretation -> (Cic.metasenv * Cic.term)) -- 2.39.2