/* $Id: parser_typen.c,v 1.13 2001/07/28 11:15:56 cb Exp $ $Log: parser_typen.c,v $ Revision 1.13 2001/07/28 11:15:56 cb added --parse-only option Revision 1.12 2001/05/30 18:07:57 sbeyer * added array and ram support in types * BETA support for function lookup table Revision 1.11 2001/05/17 12:12:19 dirkl - added command-line option --no-translation Revision 1.10 2001/01/21 17:22:58 sbeyer added additional option '--hdl-comments' Revision 1.9 2001/01/18 16:07:47 sbeyer added strings for typenames "(un)bounded nat" and "record" Revision 1.8 2001/01/11 16:16:50 sbeyer added command line support for pvs_path Revision 1.7 2001/01/11 10:08:49 sbeyer added parameter parse_verbose */ #include "parser_typen.h" int parameter_gdlausgabe; int parameter_parsetreeausgabe; int parameter_verbose; int parameter_parse_only; int parameter_parse_verbose; int parameter_hdl_comment; int parameter_speicherausgabe; int parameter_no_translation; int freigegebener_speicher; int allokierter_speicher; char *pvs_path; const char * const boolstring[] = { "FALSE","TRUE" }; const char * const typname[] = {"Bitvector","Unbounded Nat","Bounded Nat" ,"Other","RAM"}; const char * const token_string[] = { "adt_or_theories","adt_or_theory","theory_or_datatype","theory", "datatype","adtcase_plus","adtcase","constructor","idopstype_expr_list", "theoryformals","theoryformal_list","theoryformal","theoryformaldecl", "exporting","exportings","expname_list","expname","exportingmods", "assumingpart","assumings","assuming","pdformals_stern","theory_part", "theory_elt","importing","modname_list","judgement","jdecl_list", "jdecl","ename","conversion","ename_list","adformals","adformal", "assuming_decl","theory_decl","lib_decl","mod_decl","type_decl", "type_keyword","type_def","var_decl","const_decl","const_value", "def_decl","ind_decl","assumption","formula_decl","type_expr", "type_expr_sans_name","comp_type_expr","dep_type_expr_list", "recordtype","field_decls_list","field_decls","fun_array","dep_type_expr", "funarg","expr","cond_case_list","selection_list","bind","bind_list", "elseif_plus","expr_leerlist","expr_list","assignment_list","set_expr", "cond_case","lambda_body","lambda_formals","lambda_formal","set_formals", "set_formal","selection","assignment","assign_arg_plus","assign_arg", "table_expr","col_heading","expr_else_plus","expr_else_plus2", "table_entries","table_entry","simplebind_list","simplebind", "pdformals_plus","modnames","modname","mappings","mapdecl_list","mapdecl", "typedecl_or_constdecl","idops","idop","ids","typeid","typeids","name_token", "opsym","actuals","actual_list","actual","formulaname","ID","NUMBER","STRING"}; const char * const subtyp_string[] = { "adt_or_theory", "adt_or_theories adt_or_theory", "ID ':' theory_or_datatype", "ID theoryformals ':' theory_or_datatype", "theory", "datatype", "THEORY BEGINN END ID", "THEORY BEGINN theory_part END ID", "THEORY BEGINN assumingpart END ID", "THEORY BEGINN assumingpart theory_part END ID", "THEORY exporting BEGINN END ID", "THEORY exporting BEGINN theory_part END ID", "THEORY exporting BEGINN assumingpart END ID", "THEORY exporting BEGINN assumingpart theory_part END ID", "DATATYPE BEGINN adtcase_plus END ID", "DATATYPE BEGINN assumingpart adtcase_plus END ID", "DATATYPE BEGINN importing adtcase_plus END ID", "DATATYPE BEGINN importing assumingpart adtcase_plus END ID", "DATATYPE BEGINN importing ';' adtcase_plus END ID", "DATATYPE BEGINN importing ';' assumingpart adtcase_plus END ID", "DATATYPE WITH SUBTYPES ids BEGINN adtcase_plus END ID", "DATATYPE WITH SUBTYPES ids BEGINN assumingpart adtcase_plus END ID", "DATATYPE WITH SUBTYPES ids BEGINN importing adtcase_plus END ID", "DATATYPE WITH SUBTYPES ids BEGINN importing assumingpart adtcase_plus END ID", "DATATYPE WITH SUBTYPES ids BEGINN importing ';' adtcase_plus END ID", "DATATYPE WITH SUBTYPES ids BEGINN importing ';' assumingpart adtcase_plus END ID", "adtcase", "adtcase_plus adtcase", "constructor ':' idop ':' ID", "constructor ':' idop", "idop", "idop '(' idopstype_expr_list ')'", "idops ':' type_expr", "idopstype_expr_list ',' idops ':' type_expr", "'[' theoryformal_list ']'", "theoryformal", "theoryformal_list ',' theoryformal", "'(' importing ')' idops ':' theoryformaldecl", "idops ':' theoryformaldecl", "type_keyword", "type_keyword FROM type_expr", "type_expr", "EXPORTING exportings", "EXPORTING exportings WITH exportingmods", "ALL", "ALL BUT expname_list", "expname_list", "expname", "expname ',' expname_list", "idop", "idop ':' type_expr", "idop ':' TYPE", "idop ':' FORMULA", "'|' idop '|'", "ALL", "CLOSURE", "modnames", "ASSUMING assumings ENDASSUMING", "assuming", "assuming assumings", "importing ';'", "importing", "judgement", "judgement ';'", "conversion", "conversion ';'", "idops pdformals_stern ':' assuming_decl ';'", "NULL", "pdformals_plus", "theory_elt", "theory_part theory_elt", "importing ';'", "importing", "judgement", "judgement ';'", "conversion", "conversion ';'", "idops pdformals_stern ':' theory_decl ';'", "IMPORTING modname_list", "modname", "modname_list ',' modname", "JUDGEMENT jdecl_list HAS_TYPE type_expr", "JUDGEMENT jdecl_list SUBTYPE_OF type_expr", "jdecl", "jdecl_list ',' jdecl", "type_expr_sans_name", "NUMBER", "name '(' adformals ')' pdformals_stern", "name", "name ':' type_expr", "CONVERSION ename_list", "ename", "ename_list ',' ename", "adformal", "adformal ',' adformals", "typeid", "'(' typeid ')'", "theory_decl", "assumption", "lib_decl", "mod_decl", "type_decl", "var_decl", "const_decl", "def_decl", "ind_decl", "formula_decl", "datatype", "judgement", "LIBRARY '=' STRING", "LIBRARY STRING", "THEORY '=' modname", "THEORY modname", "type_keyword", "type_keyword type_def", "type_keyword type_def CONTAINING expr", "TYPE", "NONEMPTY_TYPE", "TYPEPLUS", "'=' type_expr", "FROM type_expr", "VAR type_expr", "type_expr", "type_expr const_value", "'=' expr", "RECURSIVE type_expr '=' expr MEASURE expr", "RECURSIVE type_expr '=' expr MEASURE expr BY expr", "INDUCTIVE type_expr '=' expr", "ASSUMPTION expr", "formulaname expr", "name '(' expr_list ')'", "name", "type_expr_sans_name", "'(' expr ')'", "'{' set_formals '}'", "'{' set_formals '|' expr '}'", "comp_type_expr", "recordtype", "'[' dep_type_expr_list MINUS_GROESSER type_expr ']'", "'[' MINUS_GROESSER type_expr ']'", "fun_array '[' dep_type_expr_list MINUS_GROESSER type_expr ']'", "fun_array '[' MINUS_GROESSER type_expr ']'", "'[' dep_type_expr_list ']'", "'[' ']'", "fun_array '[' dep_type_expr_list ']'", "fun_array '[' ']'", "dep_type_expr", "dep_type_expr_list ',' dep_type_expr", "'[#' field_decls_list '#]'", "field_decls", "field_decls_list ',' field_decls", "ids ':' type_expr", "FUNCTION", "ARRAY", "type_expr", "idop ':' type_expr", "'(' expr_leerlist ')'", "NUMBER", "STRING", "name", "'(:' expr_leerlist ':)'", "'[|' expr_leerlist '|]'", "'(#' assignment_list '#)'", "'(' ')'", "'(' expr_list ')'", "expr '`' ID", "expr '`' NUMBER", "expr funarg", "expr O_OPERATOR expr", "expr IFF expr", "expr '<=>' expr", "expr IMPLIES expr", "expr '=>' expr", "expr WHEN expr", "expr OR expr", "expr '\\/' expr", "expr AND expr", "expr '/\\' expr", "expr '&' expr", "expr XOR expr", "expr ANDTHEN expr", "expr ORELSE expr", "expr '^' expr", "expr '+' expr", "expr '-' expr", "expr '*' expr", "expr '/' expr", "expr '++' expr", "expr '~' expr", "expr '**' expr", "expr '//' expr", "expr '^^' expr", "expr '|-' expr", "expr '|=' expr", "expr '<|' expr", "expr '|>' expr", "expr '=' expr", "expr '/=' expr", "expr '==' expr", "expr '<' expr", "expr '<=' expr", "expr '>' expr", "expr '>=' expr", "expr '<<' expr", "expr '>>' expr", "expr '<<=' expr", "expr '>>=' expr", "expr '#' expr", "expr '@@' expr", "expr '##' expr", "not expr", "'~' expr", "'[]' expr", "'<>' expr", "'-' expr", "expr '::' name", "expr '::' name '(' expr_list ')'", "expr '::' type_expr_sans_name", "IF expr THEN expr ELSE expr ENDIF", "IF expr THEN expr elseif_plus ELSE exr ENDIF", "LAMBDA lambda_body", "FORALL lambda_body", "EXISTS lambda_body", "ID '!' NUMBER", "ID '!' lambda_body", "set_expr", "expr WHERE bind_list", "LET bind_list IN expr", "expr WITH '[' assignment_list ']'", "CASES expr OF selection_list ENDCASES", "CASES expr OF selection_list ELSE expr ENDCASES", "COND cond_case_list ENDCOND", "table_expr", "cond_case", "cond_case ',' cond_case_list", "cond_case ',' ELSE '->' expr", "selection", "selection_list ',' selection", "'(' simplebind_list ')' '=' expr", "simplebind '=' expr", "bind", "bind_list ',' bind", "ELSEIF expr THEN expr", "ELSEIF expr THEN expr elseif_plus", "NULL", "expr_list", "expr", "expr ',' expr_list", "assignment", "assignment_list ',' assignment", "'{' set_formals '|' expr '}'", "expr '->' expr", "lambda_formals ':' expr", "lambda_formal", "lambda_formal lambda_formals", "lambda_formal ',' lambda_formals", "idop", "'(' adformals ')'", "set_formal", "set_formals set_formal", "set_formals ',' set_formal", "idop", "idop ':' name", "idop ':' name '(' expr_list ')'", "idop ':' type_expr_sans_name", "'(' adformals ')'", "idop ':' expr", "idop '(' idops ')' ':' expr", "assign_arg_plus ':=' expr", "assign_arg_plus '|->' expr", "assign_arg", "assign_arg assign_arg_plus", "'(' expr_leerlist ')'", "'`' ID", "'`' NUMBER", "ID", "ID '!' NUMBER", "NUMBER", "TABLE table_entries ENDTABLE", "TABLE col_heading table_entries ENDTABLE", "TABLE ',' expr table_entries ENDTABLE", "TABLE ',' expr col_heading table_entries ENDTABLE", "TABLE expr table_entries ENDTABLE", "TABLE expr col_heading table_entries ENDTABLE", "TABLE expr ',' expr table_entries ENDTABLE", "TABLE expr ',' expr col_heading table_entries ENDTABLE", "'|[' expr expr_else_plus ']|'", "'|' expr", "'|' ELSE", "'|' expr expr_else_plus", "'|' ELSE expr_else_plus", "'|'", "'|' expr", "'|' ELSE", "'|' expr_else_plus2", "'|' expr expr_else_plus2", "'|' ELSE expr_else_plus2", "table_entry", "table_entry table_entries", "expr_else_plus2 '||'", "simplebind", "simplebind_list ',' simplebind", "idop", "idop pdformals_plus", "idop ':' type_expr", "idop pdformals_plus ':' type_expr", "'(' adformals ')'", "pdformals_plus '(' adformals ')'", "modname", "modname ',' modnamess", "IDAT ID", "IDAT ID actuals", "IDAT ID mappings", "IDAT ID actuals mappings", "ID", "ID actuals", "ID mappings", "ID actuals mappings", "'{' mapdecl_list '}'", "mapdecl", "mapdecl_list ',' mapdecl", "idops ':' typedecl_or_constdecl", "idops ':' typedecl_or_constdecl ';'", "idops pdformals_plus ':' typedecl_or_constdecl", "idops pdformals_plus ':' typedecl_or_constdecl ';'", "idops theoryformals ':' typedecl_or_constdecl", "idops theoryformals ':' typedecl_or_constdecl ';'", "type_decl", "const_decl", "idop", "idops ',' idop", "ID", "opsym", "ID", "ID ',' ids", "idop", "idop '|' expr", "idop ':' type_expr", "idop ':' type_expr '|' expr", "idops", "idops '|' expr", "idops ':' type_expr", "idops ':' type_expr '|' expr", "IDAT idop", "IDAT idop actuals", "IDAT idop '.' idop", "IDAT idop actuals '.' idop", "idop", "idop actuals", "idop '.' idop", "idop actuals '.' idop", "'+'", "'-'", "'*'", "'/'", "'='", "'/='", "'=='", "'<'", "'<='", "'>'", "'>='", "IFF", "IMPLIES", "WHEN", "OR", "AND", "NOT", "'&'", "'/\\'", "'\\/'", "'^'", "'[]'", "'<>'", "'~'", "'=>'", "'<=>'", "TRUE", "FALSE", "'o'", "XOR", "ORELSE", "ANDTHEN", "'++'", "'**'", "'//'", "'^^'", "'<<'", "'>>'", "'<<='", "'>>='", "'#'", "'@@'", "'##'", "'|-'", "'|='", "'<|'", "'|>'", "'[||]'", "'[' actual_list ']'", "actual", "actual_list ',' actual", "expr", "comp_type_expr", "AXIOM", "CHALLENGE", "CLAIM", "CONJECTURE", "COROLLARY", "FACT", "FORMULA", "LAW", "LEMMA", "OBLIGATION", "POSTULATE", "PROPOSITION", "SUBLEMMA", "THEOREM", "no subtyp"};