From 44d302801af535a58c207b33960b7cfdb116a933 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 27 Apr 2005 13:45:11 +0000 Subject: [PATCH] removed ancient cic_textual_parser (last live version tagged "dead_dir_walking") --- helm/ocaml/cic_textual_parser/.cvsignore | 1 - helm/ocaml/cic_textual_parser/.depend | 10 - helm/ocaml/cic_textual_parser/Makefile | 14 - .../cic_textual_parser/cicTextualLexer.mll | 105 ---- .../cic_textual_parser/cicTextualParser.mly | 519 ------------------ .../cic_textual_parser/cicTextualParser0.ml | 48 -- .../cicTextualParserContext.ml | 38 -- .../cicTextualParserContext.mli | 31 -- 8 files changed, 766 deletions(-) delete mode 100644 helm/ocaml/cic_textual_parser/.cvsignore delete mode 100644 helm/ocaml/cic_textual_parser/.depend delete mode 100644 helm/ocaml/cic_textual_parser/Makefile delete mode 100644 helm/ocaml/cic_textual_parser/cicTextualLexer.mll delete mode 100644 helm/ocaml/cic_textual_parser/cicTextualParser.mly delete mode 100644 helm/ocaml/cic_textual_parser/cicTextualParser0.ml delete mode 100644 helm/ocaml/cic_textual_parser/cicTextualParserContext.ml delete mode 100644 helm/ocaml/cic_textual_parser/cicTextualParserContext.mli diff --git a/helm/ocaml/cic_textual_parser/.cvsignore b/helm/ocaml/cic_textual_parser/.cvsignore deleted file mode 100644 index b94a8197a..000000000 --- a/helm/ocaml/cic_textual_parser/.cvsignore +++ /dev/null @@ -1 +0,0 @@ -*.cm[iaox] *.cmxa cicTextualParser.ml cicTextualParser.mli cicTextualLexer.ml diff --git a/helm/ocaml/cic_textual_parser/.depend b/helm/ocaml/cic_textual_parser/.depend deleted file mode 100644 index f5ce25fb9..000000000 --- a/helm/ocaml/cic_textual_parser/.depend +++ /dev/null @@ -1,10 +0,0 @@ -cicTextualParser.cmi: cicTextualParser0.cmo -cicTextualParserContext.cmi: cicTextualParser.cmi cicTextualParser0.cmo -cicTextualParser.cmo: cicTextualParser0.cmo cicTextualParser.cmi -cicTextualParser.cmx: cicTextualParser0.cmx cicTextualParser.cmi -cicTextualParserContext.cmo: cicTextualParser.cmi cicTextualParser0.cmo \ - cicTextualParserContext.cmi -cicTextualParserContext.cmx: cicTextualParser.cmx cicTextualParser0.cmx \ - cicTextualParserContext.cmi -cicTextualLexer.cmo: cicTextualParser.cmi cicTextualParser0.cmo -cicTextualLexer.cmx: cicTextualParser.cmx cicTextualParser0.cmx diff --git a/helm/ocaml/cic_textual_parser/Makefile b/helm/ocaml/cic_textual_parser/Makefile deleted file mode 100644 index 8863155b0..000000000 --- a/helm/ocaml/cic_textual_parser/Makefile +++ /dev/null @@ -1,14 +0,0 @@ -PACKAGE = cic_textual_parser -REQUIRES = helm-cic -PREDICATES = - -INTERFACE_FILES = cicTextualParser.mli cicTextualParserContext.mli -IMPLEMENTATION_FILES = cicTextualParser0.ml $(INTERFACE_FILES:%.mli=%.ml) \ - cicTextualLexer.ml -EXTRA_OBJECTS_TO_INSTALL = cicTextualParser0.ml cicTextualParser0.cmi \ - cicTextualLexer.mll cicTextualParser.mly - -EXTRA_OBJECTS_TO_CLEAN = cicTextualParser.ml cicTextualParser.mli \ - cicTextualLexer.ml - -include ../Makefile.common diff --git a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll deleted file mode 100644 index 613645bc4..000000000 --- a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll +++ /dev/null @@ -1,105 +0,0 @@ -(* 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 CicTextualParser;; - 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 - try - (UriManager.uri_of_string (String.sub uri 0 index_sharp), - int_of_string(String.sub uri index_num (String.length uri - index_num)) - 1 - ) - with - Failure msg -> - raise (CicTextualParser0.LexerFailure "Not an inductive URI") - ;; - - 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 - try - (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)) - ) - with - Failure msg -> - raise (CicTextualParser0.LexerFailure "Not a constructor URI") - ;; -} -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 } - | "CProp" { CPROP } - | 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 } - | '!' { PROD } - | ':' { COLON } - | '.' { DOT } - | "->" { ARROW } - | "_" { NONE } - | eof { EOF } -{} diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly deleted file mode 100644 index a869bc068..000000000 --- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly +++ /dev/null @@ -1,519 +0,0 @@ -/* 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,!CicTextualParser0.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 newuniv = CicUniv.fresh () in - (* TASSI: what is an implicit? *) - let newmeta = new_meta () in - let new_canonical_context = [] in - let irl = - identity_relocation_list_for_metavariable new_canonical_context - in - CicTextualParser0.metasenv := - [newmeta, new_canonical_context, Sort (Type newuniv); - newmeta+1, new_canonical_context, Meta (newmeta,irl); - newmeta+2, new_canonical_context, Meta (newmeta+1,irl) - ] @ !CicTextualParser0.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 CPROP CAST IMPLICIT NONE -%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF -%right ARROW -%start main -%type Cic.term)> main -%% -main: - | EOF { raise CicTextualParser0.Eof } /* FG: was never raised */ - | expr EOF { $1 } - | expr SEMICOLON { $1 } /* FG: to read several terms in a row - * Do we need to clear some static variables? - */ -; -expr2: - 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) !CicTextualParser0.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 - CicTextualParser0.binders := List.tl !CicTextualParser0.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 - CicTextualParser0.binders := List.tl !CicTextualParser0.binders - done ; - CoFix (idx,fixfuns) - } - | IMPLICIT - { mk_implicit () } - | SET { [], function _ -> Sort Set } - | PROP { [], function _ -> Sort Prop } - | TYPE { [], function _ -> Sort (Type (CicUniv.fresh ())) (* TASSI: ?? *)} - | CPROP { [], function _ -> Sort CProp } - | 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 - { CicTextualParser0.binders := List.tl !CicTextualParser0.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 - { CicTextualParser0.binders := List.tl !CicTextualParser0.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 - { CicTextualParser0.binders := List.tl !CicTextualParser0.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 - CicTextualParser0.binders := bs@(!CicTextualParser0.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 - CicTextualParser0.binders := bs@(!CicTextualParser0.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 - { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders; - let dom,mk_expr = $4 in - Cic.Name $2, (dom, function interp -> mk_expr interp) - } - | expr2 ARROW - { CicTextualParser0.binders := (Some Anonymous)::!CicTextualParser0.binders ; - let dom,mk_expr = $1 in - Anonymous, (dom, function interp -> mk_expr interp) - } - | PROD ID DOT - { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders; - let newmeta = new_meta () in - let newuniv = CicUniv.fresh () in - let new_canonical_context = [] in - let irl = - identity_relocation_list_for_metavariable new_canonical_context - in - CicTextualParser0.metasenv := - [newmeta, new_canonical_context, Sort (Type newuniv); - (* TASSI: ?? *) - newmeta+1, new_canonical_context, Meta (newmeta,irl) - ] @ !CicTextualParser0.metasenv ; - Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl)) - } -; -lambdahead: - LAMBDA ID COLON expr DOT - { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders; - let dom,mk_expr = $4 in - Cic.Name $2, (dom, function interp -> mk_expr interp) - } - | LAMBDA ID DOT - { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders; - let newmeta = new_meta () in - let newuniv = CicUniv.fresh () in - let new_canonical_context = [] in - let irl = - identity_relocation_list_for_metavariable new_canonical_context - in - CicTextualParser0.metasenv := - [newmeta, new_canonical_context, Sort (Type newuniv); - (* TASSI: ?? *) - newmeta+1, new_canonical_context, Meta (newmeta,irl) - ] @ !CicTextualParser0.metasenv ; - Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl)) - } -; -letinhead: - LAMBDA ID LETIN expr DOT - { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.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/cic_textual_parser/cicTextualParser0.ml b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml deleted file mode 100644 index 7a53057e2..000000000 --- a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml +++ /dev/null @@ -1,48 +0,0 @@ -(* 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/. - *) - -exception Eof;; -exception LexerFailure of string;; - -type uri = - ConUri of UriManager.uri - | VarUri of UriManager.uri - | IndTyUri of UriManager.uri * int - | IndConUri of UriManager.uri * int * int -;; - -type interpretation_domain_item = - Id of string - | Symbol of string * (string * (interpretation -> Cic.term)) list -and interpretation_codomain_item = - Uri of uri - | Implicit - | Term of (interpretation -> Cic.term) -and interpretation = - interpretation_domain_item -> interpretation_codomain_item option -;; - -let binders = ref ([] : (Cic.name option) list);; -let metasenv = ref ([] : Cic.metasenv);; diff --git a/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml b/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml deleted file mode 100644 index c9dfe664b..000000000 --- a/helm/ocaml/cic_textual_parser/cicTextualParserContext.ml +++ /dev/null @@ -1,38 +0,0 @@ -(* 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!!! *) - CicTextualParser0.binders := context ; - CicTextualParser0.metasenv := metasenv ; - let dom,mk_term = CicTextualParser.main lexer lexbuf in - let metasenv' = !CicTextualParser0.metasenv in - dom, - function interp -> - CicTextualParser0.metasenv := metasenv' ; - let term = mk_term interp in - let metasenv = !CicTextualParser0.metasenv in - metasenv,term -;; diff --git a/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli b/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli deleted file mode 100644 index 0b8871ee8..000000000 --- a/helm/ocaml/cic_textual_parser/cicTextualParserContext.mli +++ /dev/null @@ -1,31 +0,0 @@ -(* 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 -> CicTextualParser.token) -> Lexing.lexbuf -> - CicTextualParser0.interpretation_domain_item list * - (CicTextualParser0.interpretation -> (Cic.metasenv * Cic.term)) -- 2.39.2