Last active
September 19, 2017 22:32
-
-
Save JasonGross/2c792768f8ca895351152b388f167440 to your computer and use it in GitHub Desktop.
Notations for compcert clight
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Require Import Clightdefs. | |
| Delimit Scope None_scope with None. | |
| Delimit Scope C_scope with C. | |
| Delimit Scope Z_scope with Z. | |
| Delimit Scope camlfloat_of_coqfloat_scope with camlfloat_of_coqfloat. | |
| Delimit Scope camlfloat_of_coqfloat32_scope with camlfloat_of_coqfloat32. | |
| Delimit Scope camlint64_of_coqint_scope with camlint64_of_coqint. | |
| Delimit Scope camlint_of_coqint_scope with camlint_of_coqint. | |
| Delimit Scope expr_scope with expr. | |
| Delimit Scope extern_atom_scope with extern_atom. | |
| Delimit Scope name_of_external_scope with name_of_external. | |
| Delimit Scope name_type_scope with name_type. | |
| Delimit Scope positive_scope with positive. | |
| Delimit Scope print_case_label_scope with print_case_label. | |
| Delimit Scope print_cases_scope with print_cases. | |
| Delimit Scope print_expr_list_true_scope with print_expr_list_true. | |
| Delimit Scope print_stmt_for_scope with print_stmt_for. | |
| Notation "x" := (Int.repr x%Z) (only printing, at level 10) : expr_scope. | |
| Notation "({ s_val })" := s_val%C (only printing, left associativity, at level 26, format "({ s_val })") : print_stmt_for_scope. | |
| Notation "id = 'builtin' ef ( el );" := (Sbuiltin (Some id%positive) ef%name_of_external _ el%print_expr_list_true) (only printing, ef at level 26, el at level 26, left associativity, at level 26, format "'[hv ' id = '/' 'builtin' ef '/' ( el ); ']'") : print_stmt_for_scope. | |
| Notation "'builtin' ef ( el );" := (Sbuiltin None ef%name_of_external _ el%print_expr_list_true) (only printing, ef at level 26, el at level 26, left associativity, at level 26, format "'[hv ' 'builtin' ef '/' ( el ); ']'") : print_stmt_for_scope. | |
| Notation "id = e1 ( el )" := (Scall (Some id%positive) e1%expr el%print_expr_list_true) (only printing, e1 at level 26, el at level 26, left associativity, at level 26, format "'[hv ' id = '/' e1 '/' ( el ) ']'") : print_stmt_for_scope. | |
| Notation "e1 ( el )" := (Scall None e1%expr el%print_expr_list_true) (only printing, el at level 26, left associativity, at level 26, format "'[hv ' e1 '/' ( el ) ']'") : print_stmt_for_scope. | |
| Notation "s1 , s2" := (Ssequence s1%print_stmt_for s2%print_stmt_for) (only printing, s2 at level 26, left associativity, at level 26, format "s1 , s2") : print_stmt_for_scope. | |
| Notation "id = e2" := (Sset id%positive e2%expr) (only printing, format "id = e2", at level 70) : print_stmt_for_scope. | |
| Notation "e1 = e2" := (Sassign e1%expr e2%expr) (only printing, format "e1 = e2", at level 70) : print_stmt_for_scope. | |
| Notation "/*nothing*/" := Sskip (only printing, format "/*nothing*/", at level 10) : print_stmt_for_scope. | |
| Notation "'goto' lbl ;" := (Sgoto lbl%extern_atom) (only printing, lbl at level 26, left associativity, at level 26, format "'goto' lbl ;") : C_scope. | |
| Notation "lbl : s1" := (Slabel lbl%extern_atom s1%C) (only printing, s1 at level 26, left associativity, at level 26, format "lbl : '/' s1") : C_scope. | |
| Notation "'return' e_val ;" := (Sreturn (Some e_val%expr)) (only printing, left associativity, at level 26, format "'return' e_val ;") : C_scope. | |
| Notation "return;" := (Sreturn None) (only printing, format "return;", at level 10) : C_scope. | |
| Notation "'switch' ( e_val ) { cases }" := (Sswitch e_val%expr cases%print_cases) (only printing, cases at level 26, left associativity, at level 26, format "'[v' 'switch' ( e_val ) { '/ ' cases '/' } ']'") : C_scope. | |
| Notation "continue;" := Scontinue (only printing, format "continue;", at level 10) : C_scope. | |
| Notation "break;" := Sbreak (only printing, format "break;", at level 10) : C_scope. | |
| Notation "'for' ( ; 1; s2 ) { s1 }" := (Sloop s1%C s2%print_stmt_for) (only printing, s2 at level 26, s1 at level 26, left associativity, at level 26, format "'[v' 'for' ( ; '/' 1; '/' s2 ) { '/ ' s1 '/' } ']'") : C_scope. | |
| Notation "'while' (1) { s1 }" := (Sloop s1%C Sskip) (only printing, s1 at level 26, left associativity, at level 26, format "'[v' 'while' (1) { '/ ' s1 '/' } ']'") : C_scope. | |
| Notation "'if' ( e_val ) { s1 } 'else' { s2 }" := (Sifthenelse e_val%expr s1%C s2%C) (only printing, s1 at level 26, s2 at level 26, left associativity, at level 26, format "'[v' 'if' ( e_val ) { '/ ' s1 '/' } 'else' { '/ ' s2 '/' } ']'") : C_scope. | |
| Notation "'if' (! e_val ) { s2 }" := (Sifthenelse e_val%expr Sskip s2%C) (only printing, s2 at level 26, left associativity, at level 26, format "'[v' 'if' (! e_val ) { '/ ' s2 '/' } ']'") : C_scope. | |
| Notation "'if' ( e_val ) { s1 }" := (Sifthenelse e_val%expr s1%C Sskip) (only printing, s1 at level 26, left associativity, at level 26, format "'[v' 'if' ( e_val ) { '/ ' s1 '/' } ']'") : C_scope. | |
| Notation "s1 s2" := (Ssequence s1%C s2%C) (only printing, s2 at level 26, left associativity, at level 26, format "s1 '//' s2") : C_scope. | |
| Notation "s1" := (Ssequence s1%C Sskip) (only printing, format "s1", at level 10) : C_scope. | |
| Notation "s2" := (Ssequence Sskip s2%C) (only printing, format "s2", at level 10) : C_scope. | |
| Notation "id = 'builtin' ef ( el );" := (Sbuiltin (Some id%positive) ef%name_of_external _ el%print_expr_list_true) (only printing, ef at level 26, el at level 26, left associativity, at level 26, format "'[hv ' id = '/' 'builtin' ef '/' ( el ); ']'") : C_scope. | |
| Notation "'builtin' ef ( el );" := (Sbuiltin None ef%name_of_external _ el%print_expr_list_true) (only printing, ef at level 26, el at level 26, left associativity, at level 26, format "'[hv ' 'builtin' ef '/' ( el ); ']'") : C_scope. | |
| Notation "id = e1 ( el );" := (Scall (Some id%positive) e1%expr el%print_expr_list_true) (only printing, e1 at level 26, el at level 26, left associativity, at level 26, format "'[hv ' id = '/' e1 '/' ( el ); ']'") : C_scope. | |
| Notation "e1 ( el );" := (Scall None e1%expr el%print_expr_list_true) (only printing, el at level 26, left associativity, at level 26, format "'[hv ' e1 '/' ( el ); ']'") : C_scope. | |
| Notation "id = e2 ;" := (Sset id%positive e2%expr) (only printing, e2 at level 26, left associativity, at level 26, format "'[hv ' id = '/' e2 ; ']'") : C_scope. | |
| Notation "e1 = e2 ;" := (Sassign e1%expr e2%expr) (only printing, e2 at level 26, left associativity, at level 26, format "'[hv ' e1 = '/' e2 ; ']'") : C_scope. | |
| Notation "/*skip*/;" := Sskip (only printing, format "/*skip*/;", at level 10) : C_scope. | |
| Notation "'__alignof__(' ty )" := (Ealignof ty%name_type _) (only printing, ty at level 11, right associativity (* XXX Is RtoL the same as right associativity in Coq? *), at level 11, format "'[hv ' '__alignof__(' ty ) ']'") : expr_scope. | |
| Notation "'sizeof(' ty )" := (Esizeof ty%name_type _) (only printing, ty at level 11, right associativity (* XXX Is RtoL the same as right associativity in Coq? *), at level 11, format "'[hv ' 'sizeof(' ty ) ']'") : expr_scope. | |
| Notation "( ty ) a1" := (Ecast a1%expr ty%name_type) (only printing, ty at level 12, a1 at level 12, right associativity (* XXX Is RtoL the same as right associativity in Coq? *), at level 12, format "'[hv ' ( ty ) a1 ']'") : expr_scope. | |
| Notation "a1 < a2" := (Ebinop Olt a1%expr a2%expr _) (only printing, format "'[hv ' a1 '/' < a2 ']'", at level 70) : expr_scope. | |
| Notation "a1 > a2" := (Ebinop Ogt a1%expr a2%expr _) (only printing, format "'[hv ' a1 '/' > a2 ']'", at level 70) : expr_scope. | |
| Notation "a1 >= a2" := (Ebinop Oge a1%expr a2%expr _) (only printing, format "'[hv ' a1 '/' >= a2 ']'", at level 70) : expr_scope. | |
| Notation "a1 % a2" := (Ebinop Omod a1%expr a2%expr _) (only printing, a2 at level 12, left associativity (* XXX Is LtoR the same as left associativity in Coq? *), at level 13, format "'[hv ' a1 '/' % a2 ']'") : expr_scope. | |
| Notation "a1 ^ a2" := (Ebinop Oxor a1%expr a2%expr _) (only printing, format "'[hv ' a1 '/' ^ a2 ']'", at level 30, right associativity) : expr_scope. | |
| Notation "a1 - a2" := (Ebinop Osub a1%expr a2%expr _) (only printing, format "'[hv ' a1 '/' - a2 ']'", at level 50, left associativity) : expr_scope. | |
| Notation "a1 >> a2" := (Ebinop Oshr a1%expr a2%expr _) (only printing, a2 at level 14, left associativity (* XXX Is LtoR the same as left associativity in Coq? *), at level 15, format "'[hv ' a1 '/' >> a2 ']'") : expr_scope. | |
| Notation "a1 <= a2" := (Ebinop Ole a1%expr a2%expr _) (only printing, format "'[hv ' a1 '/' <= a2 ']'", at level 70) : expr_scope. | |
| Notation "a1 | a2" := (Ebinop Oor a1%expr a2%expr _) (only printing, a2 at level 19, left associativity (* XXX Is LtoR the same as left associativity in Coq? *), at level 20, format "'[hv ' a1 '/' | a2 ']'") : expr_scope. | |
| Notation "a1 / a2" := (Ebinop Odiv a1%expr a2%expr _) (only printing, format "'[hv ' a1 '/' / a2 ']'", at level 40, left associativity) : expr_scope. | |
| Notation "a1 << a2" := (Ebinop Oshl a1%expr a2%expr _) (only printing, a2 at level 14, left associativity (* XXX Is LtoR the same as left associativity in Coq? *), at level 15, format "'[hv ' a1 '/' << a2 ']'") : expr_scope. | |
| Notation "a1 & a2" := (Ebinop Oand a1%expr a2%expr _) (only printing, a2 at level 17, left associativity (* XXX Is LtoR the same as left associativity in Coq? *), at level 18, format "'[hv ' a1 '/' & a2 ']'") : expr_scope. | |
| Notation "a1 != a2" := (Ebinop Cop.One a1%expr a2%expr _) (only printing, a2 at level 16, left associativity (* XXX Is LtoR the same as left associativity in Coq? *), at level 17, format "'[hv ' a1 '/' != a2 ']'") : expr_scope. | |
| Notation "a1 * a2" := (Ebinop Omul a1%expr a2%expr _) (only printing, format "'[hv ' a1 '/' * a2 ']'", at level 40, left associativity) : expr_scope. | |
| Notation "a1 == a2" := (Ebinop Oeq a1%expr a2%expr _) (only printing, a2 at level 16, left associativity (* XXX Is LtoR the same as left associativity in Coq? *), at level 17, format "'[hv ' a1 '/' == a2 ']'") : expr_scope. | |
| Notation "a1 + a2" := (Ebinop Oadd a1%expr a2%expr _) (only printing, format "'[hv ' a1 '/' + a2 ']'", at level 50, left associativity) : expr_scope. | |
| Notation "& a1" := (Eaddrof a1%expr _) (only printing, a1 at level 11, right associativity (* XXX Is RtoL the same as right associativity in Coq? *), at level 11, format "'[hv ' & a1 ']'") : expr_scope. | |
| Notation "'__builtin_fabs' a1" := (Eunop Oabsfloat a1%expr _) (only printing, a1 at level 11, right associativity (* XXX Is RtoL the same as right associativity in Coq? *), at level 11, format "'[hv ' '__builtin_fabs' a1 ']'") : expr_scope. | |
| Notation "~ a1" := (Eunop Onotint a1%expr _) (only printing, format "'[hv ' ~ a1 ']'", at level 75, right associativity) : expr_scope. | |
| Notation "! a1" := (Eunop Onotbool a1%expr _) (only printing, format "'[hv ' ! a1 ']'", at level 30, right associativity) : expr_scope. | |
| Notation "- a1" := (Eunop Oneg a1%expr _) (only printing, format "'[hv ' - a1 ']'", at level 35, right associativity) : expr_scope. | |
| Notation "'__builtin_fabs(' a1 )" := (Eunop Oabsfloat a1%expr _) (only printing, a1 at level 24, right associativity (* XXX Is RtoL the same as right associativity in Coq? *), at level 11, format "'[hv ' '__builtin_fabs(' a1 ) ']'") : expr_scope. | |
| Notation "n_val 'LL'" := (Econst_long n_val%camlint64_of_coqint _) (only printing, no associativity, at level 10, format "'[hv ' n_val 'LL' ']'") : expr_scope. | |
| Notation "n_val 'LLU'" := (Econst_long n_val%camlint64_of_coqint (Tlong Unsigned _)) (only printing, no associativity, at level 10, format "'[hv ' n_val 'LLU' ']'") : expr_scope. | |
| Notation "f_val 'f'" := (Econst_single f_val%camlfloat_of_coqfloat32 _) (only printing, no associativity, at level 10, format "'[hv ' f_val 'f' ']'") : expr_scope. | |
| Notation "f_val" := (Econst_float f_val%camlfloat_of_coqfloat _) (only printing, format "'[hv ' f_val ']'", at level 10) : expr_scope. | |
| Notation "n_val" := (Econst_int n_val%camlint_of_coqint _) (only printing, format "'[hv ' n_val ']'", at level 10) : expr_scope. | |
| Notation "n_val 'U'" := (Econst_int n_val%camlint_of_coqint (Tint I32 Unsigned _)) (only printing, no associativity, at level 10, format "'[hv ' n_val 'U' ']'") : expr_scope. | |
| Notation "a1 . f_val" := (Efield a1%expr f_val%extern_atom _) (only printing, left associativity (* XXX Is LtoR the same as left associativity in Coq? *), at level 10, format "'[hv ' a1 . f_val ']'") : expr_scope. | |
| Notation "* a1" := (Ederef a1%expr _) (only printing, a1 at level 11, right associativity (* XXX Is RtoL the same as right associativity in Coq? *), at level 11, format "'[hv ' * a1 ']'") : expr_scope. | |
| Notation "id" := (Etempvar id%positive _) (only printing, format "'[hv ' id ']'", at level 10) : expr_scope. | |
| Notation "id" := (Evar id%extern_atom _) (only printing, format "'[hv ' id ']'", at level 10) : expr_scope. | |
| Notation "lbl : s_val rem" := (LScons lbl%print_case_label s_val%C rem%print_cases) (only printing, rem at level 26, left associativity, at level 26, format "'[v ' lbl : '/' s_val ']' '/' rem") : print_cases_scope. | |
| Notation "lbl : rem" := (LScons lbl%print_case_label Sskip rem%print_cases) (only printing, rem at level 26, left associativity, at level 26, format "lbl : '/' rem") : print_cases_scope. | |
| Notation "" := LSnil (only printing, left associativity, at level 26, format "") : print_cases_scope. | |
| Notation "'case' lbl" := (Some lbl%Z) (only printing, lbl at level 26, left associativity, at level 26, format "'case' lbl") : print_case_label_scope. | |
| Notation "'default'" := None (only printing, format "'default'", at level 10) : print_case_label_scope. | |
| Notation "p_val -> f_val" := (Efield (Ederef p_val%expr _) f_val%extern_atom _) (only printing, right associativity, at level 99, f_val at level 200, format "p_val -> f_val") : expr_scope. | |
| Notation "p_val [ i_val ]" := (Ederef (Ebinop Oadd p_val%expr i_val%expr _) _) (only printing, left associativity, at level 26, format "p_val [ i_val ]") : expr_scope. | |
| Notation "x , .. , y" := (@cons expr x%expr .. (@cons expr y%expr (@nil expr)) .. ) (only printing, at level 26, x at level 24, y at level 24) : print_expr_list_true_scope. | |
| Notation "'while' ( e_val ) { s1 }" := (Swhile e_val%expr s1%C) (only printing, s1 at level 26, left associativity, at level 26, format "'[v' 'while' ( e_val ) { '/ ' s1 '/' } ']'") : C_scope. | |
| Global Open Scope expr_scope. | |
| Global Open Scope C_scope. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #!/usr/bin/env python | |
| from __future__ import with_statement | |
| import sys, re, os | |
| KNOWN_FUNCTIONS = {} | |
| KNOWN_RUNNABLE_FUNCTIONS = {} | |
| FUNCTIONS_AS_SCOPES = ('name_of_external', 'extern_atom', 'camlint_of_coqint', 'camlfloat_of_coqfloat', 'camlfloat_of_coqfloat32', 'camlint64_of_coqint', 'name_type') | |
| FUNCTION_WITH_STREAM_AND_ONE_ARG_AS_SCOPES = ('print_stmt', ) | |
| FUNCTIONS_WITH_PRECEDENCE = ('expr', ) | |
| FOR_COQ_8_6 = True | |
| SCOPE_MAP = {'print_expr':'expr', 'print_stmt':'C'} | |
| TEMP_NAME_REPLACEMENT = (r'"$" ^ ', '') | |
| EVERY_STATEMENT_ON_A_NEW_LINE = True | |
| var_replacements = dict((ch, ch + '_val') for ch in 'abcdefghijklmnopqrstuvwxyz') | |
| def ocaml_to_coq_precedence(prec): | |
| # PrintClight.ml parenthesizes things whenever a smaller precedence | |
| # falls inside a larger one; Coq parenthesizes things the other | |
| # way around, so we need to flip the sense of precedences. Note | |
| # that the .ml file has 16 as it's max precedence, and we probably | |
| # don't want anything below 10 (the level of Coq function | |
| # application | |
| return 26 - prec | |
| def get_new_function_name(line, cur_function): | |
| words = line.split(' ') | |
| if words[0] in ('let', 'and') and len(words) > 1: | |
| if words[0] == 'let' and words[1] == 'rec' and len(words) > 2: | |
| return True, words[2], ' '.join(words[3:]) | |
| else: | |
| return True, words[1], ' '.join(words[2:]) | |
| else: | |
| return False, cur_function, None | |
| def normalize(line): | |
| line = line.strip() | |
| if line[:2] == '(*' and line[-2:] == '*)' and '(*' not in line[2:-2]: | |
| return '' | |
| return line | |
| def lines_to_functions(lines): | |
| cur_function = None | |
| is_match = False | |
| ret = [] | |
| for line in lines: | |
| changed, cur_function, extra = get_new_function_name(line, cur_function) | |
| if changed: | |
| parts = extra.split('=') | |
| ret.append((cur_function, parts[0].strip(), [normalize('='.join(parts[1:]))])) | |
| elif len(ret) > 0: | |
| ret[-1][-1].append(normalize(line)) | |
| return tuple((name, args, tuple(line for line in body if len(line) > 0)) | |
| for name, args, body in ret) | |
| def lex_string(body, delim='"'): | |
| assert(len(delim) > 0) | |
| assert(body[:len(delim)] == delim) | |
| assert(delim in body[len(delim):]) | |
| body = body[len(delim):] | |
| idx = body.index(delim) + len(delim) | |
| return body[idx:], delim + body[:idx] | |
| TOKENS = tuple(reversed(sorted( | |
| list(r'~!@#$%^&*()+`-={}|[]\:;<>?,./') + | |
| ['->', '<-', ':=', '()', '[]', '::'] | |
| ))) | |
| def lex_token(body): | |
| body = body.strip(' \n\t') | |
| if len(body) == 0: return body, None | |
| if body[0] in "'\"": return lex_string(body, body[0]) | |
| if body[0].isalpha() or body[0] == '_' or (body[0] == "'" and (body[1].isalpha() or body[1] == '_')): | |
| if body[0] == "'": | |
| body, ident = lex_token(body[1:]) | |
| return body, "'" + ident | |
| match = re.match(r"^([A-Za-z_][A-Za-z0-9_'\.]*)", body) | |
| ident = match.groups()[0] | |
| body = body[len(ident):] | |
| if ident in var_replacements.keys(): | |
| # this is a kludge to get around the fact that we can't | |
| # use a variable called 'f' after reserving 'f' as a | |
| # keyword | |
| ident = var_replacements[ident] | |
| return body, ident | |
| if body[0].isdigit() or (body[0] in '+-' and len(body) > 1 and | |
| (body[1].isdigit() or (body[1] == '.' and len(body) > 2 and | |
| body[2].isdigit()))): | |
| match = re.match(r'^([+-]?[0-9][0-9\.]*[L]?)', body) | |
| ident = match.groups()[0] | |
| return body[len(ident):], ident | |
| else: | |
| for tok in TOKENS: | |
| if body[:len(tok)] == tok: | |
| return body[len(tok):], tok | |
| raw_input('ERROR: Unknown token: %s' % repr(body[20:])) | |
| DEFAULT_INVALID_TOKS = ('let', 'in', 'if', 'then', 'else', 'rec', 'begin', 'match', 'with', 'end', 'function') | |
| def parse_sexpr_gen(body, cur_sep=None, extra_toks=tuple(), inside_parens=False, max_app=None, top_invalid_toks=tuple(), invalid_toks=DEFAULT_INVALID_TOKS): | |
| body = body.strip(' \n\t') | |
| if len(body) == 0: return body, None, None | |
| orig_body = body | |
| def parse_again(body, tok): | |
| if max_app is None: | |
| new_max_app = None | |
| else: | |
| new_max_app = max_app - 1 | |
| if max_app == 0: | |
| rest_idents, ty = None, None | |
| else: | |
| body, rest_idents, ty = parse_sexpr_gen(body, cur_sep=' ', extra_toks=extra_toks, inside_parens=inside_parens, max_app=new_max_app, top_invalid_toks=top_invalid_toks, invalid_toks=invalid_toks) | |
| my_idents = [tok] | |
| if ty == 'atom': my_idents.append(rest_idents) | |
| elif ty is None: pass | |
| elif ty == 'app': my_idents += rest_idents | |
| else: assert(False) | |
| if cur_sep == ' ': | |
| return body, my_idents, 'app' | |
| elif cur_sep == ',': | |
| if len(my_idents) > 1: | |
| ident = ('app', tuple(my_idents)) | |
| else: | |
| ident = my_idents[0] | |
| if max_app is not None: | |
| return body, ident, 'atom' | |
| body, rest_elements, ty2 = parse_sexpr_gen(body, cur_sep=',', extra_toks=extra_toks, inside_parens=inside_parens, max_app=None, top_invalid_toks=top_invalid_toks, invalid_toks=invalid_toks) | |
| if ty2 is None: | |
| return body, [ident], 'tuple' | |
| elif ty2 == 'tuple': | |
| return body, [ident] + rest_elements, 'tuple' | |
| elif ty2 == 'atom': | |
| return body, [ident, rest_elements], 'tuple' | |
| else: | |
| assert(False) | |
| else: | |
| assert(False) | |
| body, tok = lex_token(body) | |
| if cur_sep is None: | |
| body, subexpr, ty = parse_sexpr_gen(orig_body, cur_sep=',', extra_toks=extra_toks, inside_parens=inside_parens, max_app=max_app, top_invalid_toks=top_invalid_toks, invalid_toks=invalid_toks) | |
| if ty == 'atom' or ty is None: | |
| return body, subexpr, ty | |
| elif ty == 'tuple': | |
| if len(subexpr) > 1: | |
| return body, ('tuple', tuple(subexpr)), 'atom' | |
| else: | |
| return body, subexpr[0], 'atom' | |
| else: | |
| print(ty) | |
| assert(False) | |
| elif tok == ')': | |
| return orig_body, None, None | |
| elif tok == '(': | |
| body, subexpr, ty = parse_sexpr_gen(body, cur_sep=None, extra_toks=extra_toks, inside_parens=True, max_app=None, top_invalid_toks=tuple(), invalid_toks=invalid_toks) | |
| body = body.strip(' \n\t') | |
| assert(body[:1] == ')') | |
| body = body[1:] | |
| if subexpr is None: | |
| subexpr, ty = '()', 'atom' | |
| elif ty == 'atom': | |
| pass | |
| elif ty in ('app', 'tuple'): | |
| if len(subexpr) > 1: | |
| subexpr, ty = (ty, tuple(subexpr)), 'atom' | |
| else: | |
| subexpr, ty = subexpr[0], 'atom' | |
| else: | |
| assert(False) | |
| assert(ty == 'atom') | |
| return parse_again(body, subexpr) | |
| elif tok == ',': | |
| if cur_sep == ' ': | |
| return orig_body, None, None | |
| elif cur_sep == ',': | |
| body, next_app_list, ty = parse_sexpr_gen(body, cur_sep=' ', extra_toks=extra_toks, inside_parens=inside_parens, max_app=max_app, top_invalid_toks=top_invalid_toks, invalid_toks=invalid_toks) | |
| if ty == 'app': | |
| if len(next_app_list) > 1: | |
| next_app_list = (ty, tuple(next_app_list)) | |
| else: | |
| next_app_list = next_app_list[0] | |
| ty = 'atom' | |
| else: | |
| assert(ty == 'atom') | |
| if max_app is not None: | |
| return orig_body, next_app_list, 'atom' | |
| body, rest_components, ty2 = parse_sexpr_gen(body, cur_sep=',', extra_toks=extra_toks, inside_parens=inside_parens, max_app=None, top_invalid_toks=top_invalid_toks, invalid_toks=invalid_toks) | |
| if ty2 == 'tuple': | |
| return body, [next_app_list] + rest_components, 'tuple' | |
| elif ty2 == 'app': | |
| return body, [next_app_list, (ty2, tuple(rest_components))], 'tuple' | |
| elif ty2 == 'atom': | |
| return body, [next_app_list, rest_components], 'tuple' | |
| elif ty2 is None: | |
| return body, [next_app_list], 'tuple' | |
| else: | |
| assert(False) | |
| else: | |
| assert(False) | |
| elif tok in top_invalid_toks or tok in invalid_toks: | |
| return orig_body, None, None | |
| elif tok[0].isalnum() or tok[0] in "'_\"" or tok in extra_toks or (inside_parens and tok in '|+<>'): | |
| return parse_again(body, tok) | |
| else: | |
| return orig_body, None, None | |
| def parse_sexpr(body, extra_toks=tuple(), max_app=None, top_invalid_toks=tuple(), invalid_toks=DEFAULT_INVALID_TOKS): | |
| body = body.strip(' \n\t') | |
| orig_body = body | |
| body, sexpr, ty = parse_sexpr_gen(body, extra_toks=extra_toks, max_app=None, top_invalid_toks=top_invalid_toks, invalid_toks=invalid_toks) | |
| if ty is None: | |
| return orig_body, None | |
| assert(ty == 'atom') | |
| body = body.strip(' \n\t') | |
| return body, sexpr | |
| def parse_begin_end(body): | |
| body = body.strip(' \n\t') | |
| expr = [] | |
| orig_body = body | |
| new_body, tok = lex_token(body) | |
| if tok != 'begin': return parse_sexpr(orig_body) | |
| new_body, main = parse_body(new_body) | |
| new_body, tok = lex_token(new_body) | |
| #print(tok) | |
| assert(tok == 'end') | |
| return new_body, ('begin_end', main) | |
| def parse_list_with_toks(body, tag, good_toks, end_toks, parse_next): | |
| body = body.strip(' \n\t') | |
| expr = [] | |
| orig_body = body | |
| new_body = body | |
| tok = '' | |
| while len(new_body) > 0 and tok not in end_toks: | |
| body = new_body | |
| new_body, pexpr = parse_next(body) | |
| if pexpr is not None: | |
| expr.append(pexpr) | |
| else: | |
| new_body, tok = lex_token(body) | |
| if tok in good_toks: | |
| expr.append(tok) | |
| elif tok not in end_toks: | |
| raw_input((tok, body)) | |
| if tok not in end_toks: body = new_body | |
| if len(expr) == 0: return orig_body, None | |
| if len(expr) == 1: return body, expr[0] | |
| if tag is not None: return body, (tag, tuple(expr)) | |
| return body, tuple(expr) | |
| def parse_unit(body): | |
| body = body.strip(' \n\t') | |
| new_body, tok = lex_token(body) | |
| if tok == '()': return new_body, ('()',) | |
| return parse_begin_end(body) | |
| def parse_strcat(body): | |
| body, expr \ | |
| = parse_list_with_toks(body, 'strcat', tuple('^'), tuple(list('+=-*<>;|') + list(DEFAULT_INVALID_TOKS)), parse_unit) | |
| if expr is None: return body, None | |
| if expr[0] == 'strcat': | |
| #print(expr) | |
| expr = expr[1] | |
| assert(all(expr[i] == '^' for i in range(len(expr)) if i % 2 == 1)) | |
| assert(len(expr) > 1) | |
| return body, ('strcat', tuple(i for i in expr if i != '^')) | |
| return body, expr | |
| def parse_infix(body): | |
| return parse_list_with_toks(body, 'infix', tuple('+=-*<>'), tuple(list(';|') + list(DEFAULT_INVALID_TOKS)), parse_strcat) | |
| def parse_if_then_else(body): | |
| body = body.strip(' \n\t') | |
| expr = [] | |
| orig_body = body | |
| new_body, tok = lex_token(body) | |
| if tok != 'if': return parse_infix(orig_body) | |
| new_body, cond = parse_infix(new_body) | |
| new_body, thens = lex_token(new_body) | |
| if thens != 'then': return parse_seq(orig_body) | |
| new_body, then_case = parse_infix(new_body) | |
| body = new_body | |
| new_body, elses = lex_token(new_body) | |
| if elses != 'else': | |
| return body, ('ifthenelse', {'test':cond, 'then':then_case, 'else':None}) | |
| new_body, else_case = parse_infix(new_body) | |
| return new_body, ('ifthenelse', {'test':cond, 'then':then_case, 'else':else_case}) | |
| def parse_seq(body): | |
| body, expr \ | |
| = parse_list_with_toks(body, 'seq', tuple(';'), tuple(list('|') + list(DEFAULT_INVALID_TOKS)), parse_if_then_else) | |
| if expr is None: return body, None | |
| if expr[0] == 'seq': | |
| #print(expr) | |
| expr = expr[1] | |
| assert(len(expr) > 1) | |
| return body, ('seq', tuple(i for i in expr if i != ';')) | |
| return body, expr | |
| def parse_let_in(body): | |
| body = body.strip(' \n\t') | |
| expr = [] | |
| orig_body = body | |
| new_body, tok = lex_token(body) | |
| if tok != 'let': return parse_seq(orig_body) | |
| #print('let') | |
| new_body, ident = parse_sexpr(new_body, max_app=1) | |
| new_body, eqs = lex_token(new_body) | |
| #print('=') | |
| if eqs != '=': return parse_seq(orig_body) | |
| new_body, val = parse_let_in(new_body) | |
| new_body, instr = lex_token(new_body) | |
| if instr != 'in': return parse_seq(orig_body) | |
| #print('in') | |
| new_body, rest = parse_let_in(new_body) | |
| #print(rest) | |
| #print(repr(new_body[:40])) | |
| if len(new_body.strip(' \n\t')) != 0: return parse_seq(orig_body) | |
| return new_body, ('letin', {'ident':ident,'val':val,'body':rest}) | |
| def parse_branch_cont(body): | |
| return parse_list_with_toks(body, None, tuple(), tuple(list('|') + list(DEFAULT_INVALID_TOKS)), parse_let_in) | |
| def parse_branch(body): | |
| assert(body[0] == '|') | |
| pats = [] | |
| while body[:1] == '|': | |
| body, pat = parse_sexpr(body[1:], extra_toks=('::', '[]')) | |
| pats.append(pat) | |
| body, sep = lex_token(body) | |
| assert(sep == '->') | |
| body, expr = parse_branch_cont(body) | |
| if isinstance(expr, str): expr = (expr,) | |
| return body.strip(' \n\t'), {'patterns':tuple(pats), 'body': tuple(expr)} | |
| def parse_match_branches(body): | |
| body = body.strip(' \n\t') | |
| ret = [] | |
| while True: | |
| if body[:1] != '|': return body, ret | |
| body, branch = parse_branch(body) | |
| if branch is not None: ret.append(branch) | |
| def parse_body(body): | |
| body = body.strip(' \n\t') | |
| if len(body) == 0: return '', [] | |
| orig_body = body | |
| body, tok = lex_token(body) | |
| if tok == 'match': | |
| body, discriminee = parse_body(body) | |
| if discriminee is None: return parse_let_in(orig_body) | |
| body, tok = lex_token(body) | |
| if tok != 'with': return parse_let_in(orig_body) | |
| body, branches = parse_match_branches(body) | |
| return body, [('match', {'discriminee':discriminee, 'branches':tuple(branches)})] | |
| elif tok == 'function': | |
| body, branches = parse_match_branches(body) | |
| return body, [('function', {'branches':tuple(branches)})] | |
| else: | |
| return parse_let_in(orig_body) | |
| def match_branch_body_to_notation(name, body, stream=None): | |
| stmt = body | |
| if len(stmt) == 1 and stmt[0] == '()': return '""', tuple() | |
| if len(stmt) == 2 and stmt[0] == 'app': | |
| funcall = stmt[1] | |
| if funcall[0] == 'fprintf': | |
| if stream is not None: assert(funcall[1] == stream) | |
| format_string, args = funcall[2], funcall[3:] | |
| args_types = re.findall('%(.)', format_string) | |
| if len(args) == 0: | |
| assert(len(args_types) == 0) | |
| return format_string, tuple() | |
| else: | |
| arg_info = [] | |
| for ty in args_types: | |
| if ty == 'a': | |
| arg_info.append((args[1], args[0])) | |
| args = args[2:] | |
| else: | |
| arg_info.append((args[0], None)) | |
| args = args[1:] | |
| return format_string, tuple(arg_info) | |
| elif funcall[0] in FUNCTION_WITH_STREAM_AND_ONE_ARG_AS_SCOPES: | |
| assert(len(funcall) == 3) | |
| if stream is not None: assert(funcall[1] == stream) | |
| return '"%a"', ((funcall[2], funcall[0]), ) | |
| else: | |
| raw_input(funcall) | |
| elif len(stmt) == 2 and stmt[0] == 'seq': | |
| stmt = stmt[1] | |
| assert(len(stmt) == 2) | |
| assert(stmt[0][0] == 'ifthenelse') | |
| assert(stmt[0][1]['test'] == ('app', ('not', 'first'))) | |
| raw_input(stmt) | |
| else: | |
| raw_input(stmt) | |
| def run_if_then_else(body, env): | |
| if body[0] == 'ifthenelse': | |
| test = run_if_then_else(body[1]['test'], env) | |
| if test == True: | |
| return run_if_then_else(body[1]['then'], env) | |
| elif test == False: | |
| return run_if_then_else(body[1]['else'], env) | |
| else: | |
| raw_input(test) | |
| elif body[0] == 'infix': | |
| body = body[1] | |
| if len(body) == 3: | |
| x1, x2 = run_if_then_else(body[0], env), run_if_then_else(body[2], env) | |
| if body[1] == '=': return x1 == x2 | |
| raw_input(body) | |
| else: | |
| raw_input(body) | |
| elif body[0] == 'app': | |
| body = body[1] | |
| if len(body) == 3: | |
| x1, x2 = run_if_then_else(body[0], env), run_if_then_else(body[2], env) | |
| if body[1] == '+': return int(x1) + int(x2) | |
| raw_input(body) | |
| else: | |
| raw_input(body) | |
| elif isinstance(body, str): | |
| if body in env.keys(): return env[body] | |
| elif body[0].isupper(): return body | |
| elif body.isdigit(): return int(body) | |
| raw_input(body) | |
| elif body[0] == 'tuple': | |
| return tuple(run_if_then_else(v, env) for v in body[1]) | |
| else: | |
| raw_input(body) | |
| def adjust_format_string(format_string, args, env, pattern): | |
| special_toks = { | |
| '@ ':(" '/'", None), | |
| '%%':('%', '%'), | |
| '@[':("'['", None), | |
| '@]':("']'", None), | |
| '@,':("'/'", None), | |
| '@;':(" '/'", None), | |
| '@.':("'//'", None) | |
| } | |
| ret = [] | |
| ret_format = [] | |
| args = list(args) | |
| args_out = [] | |
| cur = None | |
| def update_cur(cur): | |
| if cur is not None: | |
| if cur.strip() != '' and (cur[0].isalpha() or cur[0] in '_') and cur.replace('_', '').replace('(', '').isalnum(): | |
| #print('yes') | |
| ret.append("'%s'" % cur) | |
| ret_format.append("'%s'" % cur) | |
| else: | |
| #print('no') | |
| ret.append(cur) | |
| ret_format.append(cur) | |
| return None | |
| ocaml_assoc = None | |
| associativity = 'left associativity' | |
| precedence = None | |
| if len(env) > 0: | |
| for key, val in env.items(): | |
| if key == 'assoc' or key[0] == 'tuple' and 'assoc' in key[1]: | |
| #print(val) | |
| assert(val[0] == 'app') | |
| assert(len(val) == 2) | |
| val = val[1] | |
| assert(val[0] in KNOWN_RUNNABLE_FUNCTIONS.keys()) | |
| comp_val = run_function_on_pattern(KNOWN_RUNNABLE_FUNCTIONS[val[0]], pattern) | |
| #if not comp_val: | |
| #raw_input((val[0], pattern)) | |
| if len(comp_val) == 1: | |
| comp_val, mapping, comp_pat = comp_val[0] | |
| extra_mapping = pattern_matches(key, comp_val) | |
| assert('assoc' in extra_mapping.keys()) | |
| assoc = extra_mapping['assoc'] | |
| ocaml_assoc = assoc | |
| assert("prec'" in extra_mapping.keys()) | |
| precedence = extra_mapping["prec'"] | |
| if assoc == 'NA': | |
| associativity = 'no associativity' | |
| elif assoc == 'RtoL': | |
| associativity = 'right associativity' | |
| msg = 'XXX Is %s the same as %s in Coq?' % (assoc, associativity) | |
| associativity = '%s (* %s *)' % (associativity, msg) | |
| print(msg) | |
| elif assoc == 'LtoR': | |
| associativity = 'left associativity' | |
| msg = 'XXX Is %s the same as %s in Coq?' % (assoc, associativity) | |
| associativity = '%s (* %s *)' % (associativity, msg) | |
| print(msg) | |
| else: | |
| pass | |
| #raw_input(assoc) | |
| else: | |
| associativity = {} | |
| precedence = {} | |
| ocaml_assoc = {} | |
| for comp_val, mapping, comp_pat in comp_val: | |
| extra_mapping = pattern_matches(key, comp_val) | |
| assert('assoc' in extra_mapping.keys()) | |
| assoc = extra_mapping['assoc'] | |
| assert("prec'" in extra_mapping.keys()) | |
| cur_precedence = extra_mapping["prec'"] | |
| if assoc == 'NA': | |
| cur_associativity = 'no associativity' | |
| elif assoc == 'RtoL': | |
| cur_associativity = 'right associativity' | |
| msg = 'XXX Is %s the same as %s in Coq?' % (assoc, cur_associativity) | |
| cur_associativity = '%s (* %s *)' % (cur_associativity, msg) | |
| print(msg) | |
| elif assoc == 'LtoR': | |
| cur_associativity = 'left associativity' | |
| msg = 'XXX Is %s the same as %s in Coq?' % (assoc, cur_associativity) | |
| cur_associativity = '%s (* %s *)' % (cur_associativity, msg) | |
| print(msg) | |
| else: | |
| raw_input(assoc) | |
| for k, v in mapping.items(): | |
| if k not in associativity.keys(): associativity[k] = {} | |
| if v not in associativity[k].keys(): associativity[k][v] = cur_associativity | |
| if k not in ocaml_assoc.keys(): ocaml_assoc[k] = {} | |
| if v not in ocaml_assoc[k].keys(): ocaml_assoc[k][v] = assoc | |
| if k not in precedence.keys(): precedence[k] = {} | |
| if v not in precedence[k].keys(): precedence[k][v] = cur_precedence | |
| assert(ocaml_assoc[k][v] == assoc) | |
| assert(associativity[k][v] == cur_associativity) | |
| assert(precedence[k][v] == cur_precedence) | |
| #print((repr(format_string), type(format_string))) | |
| has_neg_break = (re.search(r'@;<[0-9]+\s+-[0-9]+>', format_string) is not None) | |
| box_stack = [] | |
| while len(format_string) > 0: | |
| cur_indent = (0 if len(box_stack) == 0 else box_stack[-1][1]) | |
| if format_string[:3] == '@[<': | |
| match = re.match(r'^@\[<(hov|h|v|hv) ([0-9]+)>(.*)$', format_string, flags=re.DOTALL) | |
| if not match: | |
| print(format_string[:10]) | |
| box_type, count, format_string = match.groups() | |
| cur = update_cur(cur) | |
| coq_box_type = box_type.replace('hov', 'hv') | |
| if has_neg_break: | |
| box_stack.append((("'[%s'" % coq_box_type), int(count))) | |
| else: | |
| box_stack.append((("'[%s%s'" % (coq_box_type, ' ' * int(count))), int(count))) | |
| if len(box_stack) == 1 or not FOR_COQ_8_6: | |
| ret_format.append(box_stack[-1][0]) | |
| elif format_string[:3] == '@;<': | |
| match = re.match(r'^@;<([0-9]+)\s+(-?[0-9]+)>(.*)$', format_string, flags=re.DOTALL) | |
| if not match: | |
| print(format_string[:10]) | |
| nspaces, offset, format_string = match.groups() | |
| cur = update_cur(cur) | |
| if has_neg_break: | |
| ret_format.append("%s'/%s'" % (' ' * int(nspaces), ' ' * (cur_indent + int(offset)))) | |
| else: | |
| ret_format.append("%s'/%s'" % (' ' * int(nspaces), ' ' * int(offset))) | |
| elif format_string[:1] == ' ': | |
| if cur is None: | |
| cur = '' | |
| elif cur.strip() == '': | |
| cur += ' ' | |
| else: | |
| cur = update_cur(cur) | |
| cur = '' | |
| format_string = format_string[1:] | |
| elif format_string[:1] == '%': | |
| if format_string[:2] in ('%a', '%s') or format_string[:3] in ('%lu', '%ld', '%Lu', '%Ld') or format_string[:5] in ('%.15F',): | |
| (arg, printer), args = args[0], args[1:] | |
| #print('cur %s' % cur) | |
| cur = update_cur(cur) | |
| if format_string[:2] in ('%a', '%s'): use_len = 2 | |
| elif format_string[:3] in ('%lu', '%ld', '%Lu', '%Ld'): use_len = 3 | |
| elif format_string[:5] in ('%.15F',): use_len = 5 | |
| info, format_string = format_string[:use_len], format_string[use_len:] | |
| if isinstance(arg, str): | |
| args_out.append((arg, printer, None, info)) | |
| if arg.strip() != '' and (arg[0].isalpha() or arg[0] in '_') and arg.replace('_', '').replace('(', '').isalnum(): | |
| ret.append("'%s'" % arg) | |
| ret_format.append("'%s'" % arg) | |
| else: | |
| ret.append(arg) | |
| ret_format.append(arg) | |
| elif len(arg) == 2 and arg[0] == 'app': | |
| notations = seq_to_notations(arg) | |
| assert(len(notations) == 1) | |
| upattern, uliteral_string, uformat_string, uargs_info \ | |
| = notations[0] | |
| assert(upattern is None) | |
| ret.extend(uliteral_string) | |
| ret_format.extend(uformat_string) | |
| args_out.extend(uargs_info) | |
| elif len(arg) == 2 and arg[0] == 'tuple': | |
| arg = arg[1] | |
| #print((format_string, printer, arg)) | |
| assert(len(arg) == 2) | |
| assert(isinstance(arg[1], str)) | |
| if arg[0] in ('true', 'false'): | |
| args_out.append((arg[1], printer + '_' + arg[0], None, info)) | |
| ret.append(arg[1]) | |
| ret_format.append(arg[1]) | |
| elif printer in FUNCTIONS_WITH_PRECEDENCE: | |
| #print((arg, printer)) | |
| #print(env) | |
| if arg[0].isdigit(): | |
| args_out.append((arg[1], printer, int(arg[0]), info)) | |
| ret.append(arg[1]) | |
| ret_format.append(arg[1]) | |
| else: | |
| found = False | |
| for key, val in env.items(): | |
| if found: continue | |
| if arg[0] == key or key[0] == 'tuple' and arg[0] in key[1]: | |
| found = True | |
| #print(val) | |
| #print(format_string) | |
| if val[0] == 'app': | |
| assert(len(val) == 2) | |
| val = val[1] | |
| assert(val[0] in KNOWN_RUNNABLE_FUNCTIONS.keys()) | |
| comp_val = run_function_on_pattern(KNOWN_RUNNABLE_FUNCTIONS[val[0]], pattern) | |
| assert(len(comp_val) == 1) | |
| comp_val, mapping, comp_pat = comp_val[0] | |
| extra_mapping = pattern_matches(key, comp_val) | |
| assert(arg[0] in extra_mapping.keys()) | |
| prec = extra_mapping[arg[0]] | |
| if prec.isdigit(): | |
| args_out.append((arg[1], printer, int(prec), info)) | |
| ret.append(arg[1]) | |
| ret_format.append(arg[1]) | |
| else: | |
| raw_input(extra_mapping[arg[0]]) | |
| raw_input((key, comp_val)) | |
| raw_input((pattern, val)) | |
| elif val[0] == 'ifthenelse': | |
| if isinstance(ocaml_assoc, str) and isinstance(precedence, str): | |
| comp_val = run_if_then_else(val, {'assoc': ocaml_assoc, "prec'":int(precedence)}) | |
| extra_mapping = pattern_matches(key, ('tuple', tuple(str(i) for i in comp_val))) | |
| assert(arg[0] in extra_mapping.keys()) | |
| prec = extra_mapping[arg[0]] | |
| if prec.isdigit(): | |
| args_out.append((arg[1], printer, int(prec), info)) | |
| ret.append(arg[1]) | |
| ret_format.append(arg[1]) | |
| else: | |
| raw_input(extra_mapping[arg[0]]) | |
| raw_input((key, comp_val)) | |
| raw_input((pattern, val)) | |
| raw_input((arg[0], extra_mapping)) | |
| else: | |
| raw_input((ocaml_assoc, precedence)) | |
| else: | |
| assert(False) | |
| assert(found) | |
| else: | |
| assert(False) | |
| else: | |
| raw_input((arg, printer)) | |
| assert(False) | |
| elif format_string[:2] in ('%@', '%%'): | |
| if cur is None or cur.strip() == '': | |
| cur = update_cur(cur) | |
| cur = '' | |
| cur += format_string[1] | |
| format_string = format_string[2:] | |
| else: | |
| raw_input(format_string[:6]) | |
| else: | |
| found = False | |
| for tok, (rep_format, rep) in reversed(sorted(special_toks.items(), | |
| key=(lambda (k,v): len(k)))): | |
| if found: continue | |
| if format_string[:len(tok)] == tok: | |
| cur = update_cur(cur) | |
| if rep is not None: ret.append(rep) | |
| if has_neg_break and "'/'" in rep_format or "'//'" in rep_format: | |
| rep_format = rep_format.replace("'/'", "'/%s'" % (' ' * cur_indent)).replace("'//'", "'//%s'" % (' ' * cur_indent)) | |
| if tok == '@[': box_stack.append((rep_format, 0)) | |
| if tok not in ('@[', '@]') or len(box_stack) == 1 or not FOR_COQ_8_6: | |
| ret_format.append(rep_format) | |
| if tok == '@]': box_stack.pop() | |
| format_string = format_string[len(tok):] | |
| found = True | |
| if not found: | |
| if format_string[0] not in '@%': | |
| #print(cur) | |
| if cur is None or cur.strip() == '': | |
| cur = update_cur(cur) | |
| cur = '' | |
| cur += format_string[0] | |
| format_string = format_string[1:] | |
| else: | |
| raw_input(format_string[:4]) | |
| cur = update_cur(cur) | |
| #print((ret_format, args)) | |
| assert(len(args) == 0) | |
| #print(ret) | |
| if precedence is not None: precedence = int(precedence) | |
| assert(precedence is None or isinstance(precedence, int)) | |
| assert(associativity is None or isinstance(associativity, str)) | |
| return (tuple(i.strip() for i in ret if i.strip() != ''), | |
| tuple(ret_format), | |
| tuple(args_out), | |
| associativity, | |
| precedence) | |
| def strip_quotes(v): | |
| if v[0] == '"' and v[-1] == '"': return v[1:-1] | |
| return v | |
| def multiply_args(pattern, args, env): | |
| if len(args) == 0: return [(pattern, args)] | |
| arg, args = args[0], args[1:] | |
| if arg[0][0] != 'app': | |
| #print('noapp') | |
| return [(pattern, tuple([arg] + list(args))) | |
| for pattern, args in multiply_args(pattern, args, env)] | |
| arg_name = arg[0][1][0] | |
| #print(('app', arg_name)) | |
| if arg_name in KNOWN_FUNCTIONS.keys(): | |
| #print('found') | |
| body, mkmap = KNOWN_FUNCTIONS[arg_name] | |
| #raw_input(expr[1:]) | |
| body = do_subst(body, mkmap(*arg[0][1][1:])) | |
| if isinstance(body, dict): | |
| assert(all(len(inner_expr) == 1 | |
| for k, v in body.items() | |
| for pats, inner_expr in v.items())) | |
| ret = [(new_pattern, new_args) | |
| for pattern, args in [(do_subst(pattern, {k:pat}), | |
| tuple([(strip_quotes(inner_expr[0]), arg[1])] + list(args))) | |
| for k, v in body.items() | |
| for pats, inner_expr in v.items() | |
| for pat in pats] | |
| for new_pattern, new_args in multiply_args(pattern, args, env)] | |
| #raw_input(ret) | |
| return ret | |
| else: | |
| return [(pattern, tuple([arg] + list(args))) | |
| for pattern, args in multiply_args(pattern, args, env)] | |
| return [(pattern, tuple([arg] + list(args))) | |
| for pattern, args in multiply_args(pattern, args, env)] | |
| def match_to_notations(branches, env, discriminee=None): | |
| notations = [] | |
| for branch in branches: | |
| format_string, args = match_branch_body_to_notation(name, branch['body']) | |
| assert(format_string[0] == '"' and format_string[-1] == '"') | |
| for pattern in branch['patterns']: | |
| if pattern == '_' and discriminee is not None: pattern = discriminee | |
| for new_pattern, new_args in multiply_args(pattern, args, env): | |
| #print('here') | |
| #print((new_args, env, new_pattern)) | |
| literal_string, new_format_string, arg_info, associativity, precedence \ | |
| = adjust_format_string(format_string[1:-1], new_args, env, new_pattern) | |
| #if '__builtin_fabs' in ' '.join(literal_string): | |
| #raw_input((literal_string, new_format_string, format_string, new_args, new_pattern, format_string)) | |
| notations.append((new_pattern, literal_string, new_format_string, arg_info, associativity, precedence)) | |
| #print(notations[-1]) | |
| #raw_input(notations[-1]) | |
| return list(reversed(notations)) | |
| def pattern_matches(loose_pattern, tight_pattern): | |
| ret = {} | |
| if loose_pattern == '_' or tight_pattern == '_': return ret | |
| if isinstance(loose_pattern, str) and isinstance(tight_pattern, str): | |
| if loose_pattern[0].isupper() and tight_pattern[0].isupper(): | |
| return ret if loose_pattern == tight_pattern else None | |
| else: | |
| ret[loose_pattern] = tight_pattern | |
| return ret | |
| if loose_pattern[0] == tight_pattern[0] and loose_pattern[0] in ('app', 'tuple'): | |
| assert(len(loose_pattern) == 2) | |
| assert(len(tight_pattern) == 2) | |
| loose_pattern, tight_pattern = loose_pattern[1], tight_pattern[1] | |
| assert(len(loose_pattern) == len(tight_pattern)) | |
| for lp, tp in zip(loose_pattern, tight_pattern): | |
| matches = pattern_matches(lp, tp) | |
| if matches is None: return None | |
| ret.update(matches) | |
| elif isinstance(loose_pattern, str) and tight_pattern[0] == 'app' and \ | |
| all(tight_pattern[1][2*i+1] == '|' | |
| for i in range(len(tight_pattern[1]) / 2)): | |
| for tp in tight_pattern[1]: | |
| if tp == '|': continue | |
| matches = pattern_matches(loose_pattern, tp) | |
| if matches is not None: | |
| ret.update(matches) | |
| return ret | |
| return None | |
| else: | |
| raw_input((loose_pattern, tight_pattern)) | |
| return ret | |
| def run_function_on_pattern(body, pattern): | |
| assert(len(body) == 1) | |
| body = body[0] | |
| assert(len(body) == 2) | |
| assert(body[0] == 'function') | |
| branches = body[1]['branches'] | |
| ret = [] | |
| for branch in branches: | |
| for branch_pattern in branch['patterns']: | |
| mapping = pattern_matches(pattern, branch_pattern) | |
| #print(('mapping', mapping, pattern, branch_pattern)) | |
| if mapping is None: continue | |
| ret.append((branch['body'], mapping, branch_pattern)) | |
| #print(ret[-1]) | |
| return ret | |
| def do_subst(body, rep_dict): | |
| if isinstance(body, str): | |
| return rep_dict.get(body, body) | |
| elif body[0] in ('strcat', 'seq', 'app', 'tuple'): | |
| assert(len(body) == 2) | |
| return (body[0], | |
| tuple(do_subst(arg, rep_dict) for arg in body[1])) | |
| elif len(body) == 1 and body[0][0] == 'function': | |
| assert(isinstance(rep_dict, tuple)) | |
| assert(len(rep_dict) == 1) | |
| body = body[0][1] | |
| return {rep_dict[0]:dict((branch['patterns'], branch['body']) | |
| for branch in body['branches'])} | |
| raw_input((body, rep_dict)) | |
| def join_notations(notations_list): | |
| def pattern_matches(p1, p2): | |
| assert(p1 is None) | |
| assert(p2 is None) | |
| return True | |
| ret_notations = [] | |
| for notations in notations_list: | |
| assert(len(notations) == 1) | |
| for pattern, literal_string, format_string, args_info, associativity, precedence in notations: | |
| if not any(pattern_matches(pattern, upattern) for upattern, uliteral_string, uformat_string, uargs_info, uassociativity, uprecedence in ret_notations): | |
| ret_notations.append([pattern, list(literal_string), list(format_string), list(args_info), associativity, precedence]) | |
| else: | |
| for upattern, uliteral_string, uformat_string, uargs_info, uassociativity, uprecedence in ret_notations: | |
| if pattern_matches(upattern, pattern): | |
| assert(pattern is None) | |
| uliteral_string.extend(literal_string) | |
| uformat_string.extend(format_string) | |
| uargs_info.extend(args_info) | |
| assert(uassociativity == associativity) | |
| assert(uprecedence == precedence) | |
| assert(isinstance(associativity, str)) | |
| assert(isinstance(precedence, int)) | |
| return [(pattern, tuple(literal_string), tuple(format_string), tuple(args_info), associativity, precedence) | |
| for pattern, literal_string, format_string, args_info, associativity, precedence in ret_notations] | |
| def seq_to_notations(expr, env=None): | |
| if env is None: env = {} | |
| if isinstance(expr, str): | |
| #print(expr) | |
| assert(expr[0] == '"' and expr[-1] == '"') | |
| expr = expr[1:-1] | |
| return [(None, [expr], [expr], tuple())] | |
| elif expr[0] in ('match', 'function'): | |
| return match_to_notations(expr[1]['branches'], env, discriminee=expr[1].get('discriminee', None)) | |
| elif expr[0] == 'app': | |
| assert(len(expr) == 2) | |
| expr = expr[1] | |
| if expr[0] in KNOWN_FUNCTIONS.keys(): | |
| body, mkmap = KNOWN_FUNCTIONS[expr[0]] | |
| #raw_input(expr[1:]) | |
| body = do_subst(body, mkmap(*expr[1:])) | |
| if isinstance(body, dict): | |
| return dict((k, | |
| dict((pat, | |
| seq_to_notations(inner_expr)) | |
| for pat, inner_expr in v.items())) | |
| for k, v in body.items()) | |
| else: | |
| return seq_to_notations(body) | |
| elif expr[0] == 'Z.to_string': | |
| assert(len(expr) == 2) | |
| expr = expr[1] | |
| if expr[0] == 'app': | |
| assert(len(expr) == 2) | |
| expr = expr[1] | |
| assert(expr[0] == 'Z.Zpos') | |
| assert(len(expr) == 2) | |
| ident = expr[1] | |
| assert(isinstance(ident, str)) | |
| return [(None, [ident], [ident], ((ident, 'positive', None, None), ))] | |
| elif isinstance(expr, str): | |
| return [(None, [expr], [expr], ((expr, 'Z', None, None), ))] | |
| else: | |
| raw_input(expr) | |
| elif expr[0] in FUNCTIONS_AS_SCOPES: | |
| assert(isinstance(expr[1], str)) | |
| assert(len(expr) == 2) | |
| scope, ident = expr | |
| return [(None, [ident], [ident], ((ident, scope, None, None), ))] | |
| else: | |
| raw_input(expr) | |
| elif expr[0] == 'strcat': | |
| assert(len(expr) == 2) | |
| expr = expr[1] | |
| return join_notations(seq_to_notations(s) for s in expr) | |
| elif len(expr) == 1 and isinstance(expr[0], str) and expr[0][0] == '"' and expr[0][-1] == '"': | |
| ident = expr[0][1:-1] | |
| return [(None, [ident], [ident], tuple())] | |
| else: | |
| raw_input(expr) | |
| def function_to_notations(name, body, env=None): | |
| notations = [] | |
| if len(body) == 1: | |
| for line in body: | |
| notations += seq_to_notations(line, env) | |
| else: | |
| if body[0] == 'letin': | |
| assert(len(body) == 2) | |
| body = body[1] | |
| if env is None: env = {} | |
| env = dict(env) | |
| env[body['ident']] = body['val'] | |
| return function_to_notations(name, body['body'], env) | |
| elif body[0] == 'seq': | |
| assert(len(body) == 2) | |
| body = body[1] | |
| if len(body) == 3 and body[0][0] == 'ifthenelse' and body[-1][0] == 'ifthenelse': | |
| if (body[0][1]['then'] == ('app', ('fprintf', var_replacements.get('p', 'p'), '"@[<hov 2>("')) and | |
| body[0][1]['else'] == ('app', ('fprintf', var_replacements.get('p', 'p'), '"@[<hov 2>"')) and | |
| body[-1][1]['then'] == ('app', ('fprintf', var_replacements.get('p', 'p'), '")@]"')) and | |
| body[-1][1]['else'] == ('app', ('fprintf', var_replacements.get('p', 'p'), '"@]"'))): | |
| body = body[1] | |
| notations = function_to_notations(name, body, env) | |
| notations = [(pattern, | |
| literal_string, | |
| tuple(["'[hv '"] + list(format_string) + ["']'"]), | |
| args_info, | |
| associativity, | |
| precedence) | |
| for pattern, literal_string, format_string, args_info, associativity, precedence in notations] | |
| return notations | |
| else: | |
| raw_input(body) | |
| else: | |
| raw_input((len(body), body)) | |
| elif body[0] == 'begin_end': | |
| assert(len(body) == 2) | |
| body = body[1] | |
| return function_to_notations(name, body, env) | |
| elif body[0] == 'function': | |
| assert(len(body) == 2) | |
| body = body[1] | |
| return match_to_notations(body['branches'], env) | |
| else: | |
| raw_input(body) | |
| return notations | |
| def sexpr_args_to_mkmap(sargs): | |
| ret = [] | |
| if sargs[0] == 'app' and len(sargs) == 2: | |
| sargs = sargs[1][1:] | |
| for arg in sargs: | |
| if isinstance(arg, str): | |
| ret.append(arg) | |
| elif arg[0] == 'app': | |
| assert(len(arg) == 2) | |
| arg = arg[1] | |
| assert(len(arg) == 3) | |
| assert(arg[1] == ':') | |
| ret.append(arg[0]) | |
| else: | |
| raw_input(arg) | |
| arg_names = tuple(ret) | |
| #print(arg_names) | |
| def mkmap(*args): | |
| assert(len(args) == len(arg_names)) | |
| return dict(zip(arg_names, args)) | |
| return mkmap | |
| elif isinstance(sargs, str): | |
| def mkmap(*args): | |
| return args | |
| return mkmap | |
| else: | |
| raw_input(sargs) | |
| def print_term(term, scope_map, needs_parens=False, known_idents=tuple()): | |
| if isinstance(term, str): | |
| if term in scope_map.keys(): | |
| scope = scope_map[term] | |
| return term + '%' + SCOPE_MAP.get(scope, scope) | |
| elif term[0].isupper() or not term[0].isalpha(): | |
| return term | |
| elif term in known_idents: | |
| return term | |
| else: | |
| print('Replacing %s with _' % term) | |
| return '_' | |
| elif term[0] == 'app': | |
| assert(len(term) == 2) | |
| term = term[1] | |
| if term[0][0].isupper() and len(term) == 2 and term[1][0] == 'tuple' and len(term[1]) == 2: | |
| term = tuple([term[0]] + list(term[1][1])) | |
| ret = ' '.join(print_term(arg, scope_map, needs_parens=True) | |
| for arg in term) | |
| if needs_parens: ret = '(%s)' % ret | |
| return ret | |
| else: | |
| fmt = '%s' if not needs_parens and len(term) > 1 else '(%s)' | |
| ret = ' '.join(print_term(arg, scope_map, needs_parens=True) | |
| for arg in term) | |
| return fmt % ret | |
| raw_input(term) | |
| DEFAULT_PRECEDENCE = 0 | |
| SINGLE_IDENT_PRECEDENCE = 10 | |
| def notations_to_coq(scope, notations, default_precedence=DEFAULT_PRECEDENCE, default_associativity='left associativity'): | |
| ret = [] | |
| specifiers = ['only printing'] | |
| scopes = set([scope]) | |
| for pattern, literal_string, format_string, args, associativity, precedence in notations: | |
| if associativity is None: associativity = default_associativity | |
| if precedence is None: precedence = default_precedence | |
| cur_specifiers = list(specifiers) | |
| scope_map = {} | |
| for arg, arg_scope, arg_precedence, fmt in args: | |
| scope_map[arg] = arg_scope | |
| if literal_string[0].strip("'") != arg.strip("'"): | |
| if arg_precedence is None: arg_precedence = precedence | |
| if arg.isalnum(): | |
| cur_specifiers.append('%s at level %d' % (arg, ocaml_to_coq_precedence(arg_precedence))) | |
| else: | |
| if arg_precedence is not None: | |
| # ERROR if we run afoul of | |
| # https://coq.inria.fr/bugs/show_bug.cgi?id=5739, | |
| # It should be possible to change the level of | |
| # the leftmost non-terminal for only printing | |
| # notations | |
| assert(precedence == arg_precedence) | |
| #precedence = arg_precedence | |
| scopes.add(arg_scope) | |
| cur_specifiers.append(associativity) | |
| cur_specifiers.append('at level %d' % ocaml_to_coq_precedence(precedence)) | |
| printed_term = print_term(pattern, scope_map) | |
| for arg, arg_scope, arg_precedence, fmt in args: | |
| if arg in printed_term: | |
| qarg = "'%s'" % arg | |
| if qarg in literal_string: | |
| literal_string = [i.replace(qarg, arg) for i in literal_string] | |
| if qarg in format_string: | |
| format_string = [i.replace(qarg, arg) for i in format_string] | |
| if len(literal_string) == 2 and len(args) == 2 and tuple(literal_string) == tuple(arg[0] for arg in args) and EVERY_STATEMENT_ON_A_NEW_LINE: | |
| format_string = [i.replace("'/'", "'//'") for i in format_string] | |
| cur_specifiers.append('format "%s"' % ' '.join(format_string)) | |
| ignore_level = False | |
| forced_specifiers = [] | |
| forced_levels = {'<':70, '>':70, '>=':70, '^':30, '-':50, '<=':70, '/':40, '*':40, '+':50, '=':70} | |
| forced_prefix_levels = {'-':35, '~':75, '!':30} | |
| forced_assoc = {'^':'right associativity', '-':'left associativity', '/':'left associativity', '+':'left associativity', '*':'left associativity'} | |
| forced_prefix_assoc = {'~':'right associativity', '-':'right associativity', '!':'right associativity'} | |
| if len(literal_string) == 3 and literal_string[1] in forced_levels.keys(): | |
| ignore_level = True | |
| forced_specifiers.append('at level %d' | |
| % forced_levels[literal_string[1]]) | |
| if literal_string[1] in forced_assoc.keys(): | |
| forced_specifiers.append(forced_assoc[literal_string[1]]) | |
| elif len(literal_string) == 2 and literal_string[0] in forced_prefix_levels.keys(): | |
| ignore_level = True | |
| forced_specifiers.append('at level %d' | |
| % forced_prefix_levels[literal_string[0]]) | |
| if literal_string[0] in forced_prefix_assoc.keys(): | |
| forced_specifiers.append(forced_prefix_assoc[literal_string[0]]) | |
| elif len(literal_string) == 1: | |
| ignore_level = True | |
| forced_specifiers.append('at level %d' % SINGLE_IDENT_PRECEDENCE) | |
| #if '__builtin_fabs' in ' '.join(literal_string): | |
| #raw_input((literal_string)) | |
| ret.append('Notation "%s" := %s (%s) : %s_scope.' | |
| % (' '.join(literal_string), | |
| print_term(pattern, scope_map, needs_parens=True), | |
| ', '.join([i for i in cur_specifiers | |
| if ('at level' not in i and 'associativity' not in i) or not ignore_level] | |
| + forced_specifiers), | |
| SCOPE_MAP.get(scope, scope))) | |
| #print(ret[-1]) | |
| return scopes, ret | |
| def assemble_coq(scopes, notations): | |
| ret = ['Require Import Clightdefs.', ''] | |
| for scope in sorted(set(SCOPE_MAP.get(scope, scope) for scope in scopes)): | |
| ret.append('Delimit Scope %s_scope with %s.' % (scope, scope)) | |
| ret.append('') | |
| ret.append('Notation "x" := (Int.repr x%%Z) (only printing, at level %d) : expr_scope.' % SINGLE_IDENT_PRECEDENCE) | |
| ret.append('') | |
| ret.extend(notations) | |
| ret.append('') | |
| ret.append('Notation "p_val -> f_val" := (Efield (Ederef p_val%expr _) f_val%extern_atom _) (only printing, right associativity, at level 99, f_val at level 200, format "p_val -> f_val") : expr_scope.') | |
| ret.append('Notation "p_val [ i_val ]" := (Ederef (Ebinop Oadd p_val%%expr i_val%%expr _) _) (only printing, left associativity, at level %d, format "p_val [ i_val ]") : expr_scope.' % ocaml_to_coq_precedence(DEFAULT_PRECEDENCE)) | |
| ret.append('Notation "x , .. , y" := (@cons expr x%%expr .. (@cons expr y%%expr (@nil expr)) .. ) (only printing, at level %d, x at level %d, y at level %d) : print_expr_list_true_scope.' % (ocaml_to_coq_precedence(DEFAULT_PRECEDENCE), ocaml_to_coq_precedence(2), ocaml_to_coq_precedence(2))) # 2 comes from print_expr_list in PrintClight.ml | |
| ret.append('''Notation "'while' ( e_val ) { s1 }" := (Swhile e_val%%expr s1%%C) (only printing, s1 at level %d, left associativity, at level %d, format "'[v' 'while' ( e_val ) { '/ ' s1 '/' } ']'") : C_scope.''' % (ocaml_to_coq_precedence(DEFAULT_PRECEDENCE), ocaml_to_coq_precedence(DEFAULT_PRECEDENCE))) | |
| ret.append('') | |
| for scope in ('expr', 'C'): | |
| ret.append('Global Open Scope %s_scope.' % scope) | |
| ret.append('') | |
| return '\n'.join(ret) | |
| if __name__ == '__main__': | |
| if len(sys.argv) != 3 or '--help' in sys.argv or '-h' in sys.argv: | |
| print('USAGE: %s COMPCERT_FOLDER OUTPUT' % sys.argv[0]) | |
| sys.exit(1) | |
| dirpath = sys.argv[1] | |
| fname = os.path.join(dirpath, 'cfrontend/PrintClight.ml') | |
| #fname = '/home/jgross/Documents/repos/VST/compcert/cfrontend/PrintClight.ml' | |
| fname2 = os.path.join(dirpath, 'cfrontend/PrintCsyntax.ml') | |
| #fname2 = '/home/jgross/Documents/repos/VST/compcert/cfrontend/PrintCsyntax.ml' | |
| with open(fname, 'r') as f: | |
| lines = f.readlines() | |
| with open(fname2, 'r') as f: | |
| lines_syntax = f.readlines() | |
| fns = dict((name, (args, body)) for name, args, body in lines_to_functions(lines_syntax)) | |
| fns.update(dict((name, (args, body)) for name, args, body in lines_to_functions(lines))) | |
| for name in ('temp_name', 'name_unop', 'name_binop'): | |
| (args, body) = fns[name] | |
| if name == 'temp_name' and TEMP_NAME_REPLACEMENT is not None: | |
| assert(TEMP_NAME_REPLACEMENT[0] in body[0]) | |
| body = tuple(b.replace(TEMP_NAME_REPLACEMENT[0], TEMP_NAME_REPLACEMENT[1]) for b in body) | |
| body, parsed_body = parse_body('\n'.join(body)) | |
| assert(body == '') | |
| extra, sargs = parse_sexpr(name + ' ' + args, extra_toks=(':',)) | |
| assert(extra == '') | |
| mkmap = sexpr_args_to_mkmap(sargs) | |
| KNOWN_FUNCTIONS[name] = (parsed_body, mkmap) | |
| name, (args, body) = 'precedence', fns['precedence'] | |
| body, precedence = parse_body('\n'.join(body)) | |
| assert(body == '') | |
| KNOWN_RUNNABLE_FUNCTIONS['precedence'] = precedence | |
| notations, scopes = [], set() | |
| for name in ('print_stmt_for', 'print_stmt', 'expr', 'print_cases', 'print_case_label'): # 'print_expr_list', | |
| (args, body) = fns[name] | |
| body, parsed_body = parse_body('\n'.join(body)) | |
| assert(body == '') | |
| cur_notations = function_to_notations(name, parsed_body) | |
| cur_scopes, cur_notations = notations_to_coq(name, cur_notations) | |
| scopes.update(cur_scopes) | |
| notations += cur_notations | |
| coq = assemble_coq(scopes, notations) | |
| with open(sys.argv[2], 'w') as f: | |
| f.write(coq) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment