(* A Hyacc parser, made from spi.y with hyacc version Hyacc version 1.22 (derived from GNU Bison) *) open "spi_tab_h"; open "yyerror_h"; open "gensym_h"; val constructors = ref ({"0", "s" (*, "nil", "cons"*) } : string set); val |[ matches = cons_matches, subst = cons_subst, ... ]| = regexp "^__c"; (*"^t([0-9]+)$";*) val private_funs = ref ({"__eq", "__nu"}); val funs = ref ({"crypt" => 2, "acrypt" => 2, "__eq" => 1, "pub" => 1, "prv" => 1, "0" => 0, "s" => 1, "__nu" => 2 (*, "nil" => 0, "cons" => 2 *)} : string -m> int); fun is_constructor f = f inset !constructors orelse cons_matches f; fun is_fun f = f inset !funs orelse cons_matches f; fun fun_arity f = if cons_matches f then intofstring (cons_subst "\\1") else ?(!funs) f; val procs = ref ({"dy_synthesizer" => 2, "dy_analyzer" => 2} : string -m> int); val expected_procs = ref ({} : string -m> int); fun copy_loc loc = let val loc' = iarray (4, 0) in iupdate (loc', 0, isub (loc,0)); iupdate (loc', 1, isub (loc,1)); iupdate (loc', 2, isub (loc,2)); iupdate (loc', 3, isub (loc,3)); loc' end; val ploc = print_yyloc stderr; fun ploc2 (loc1, loc2) = let val loc = iarray(4,0) in iupdate (loc, 0, isub (loc1,0)); iupdate (loc, 1, isub (loc1,1)); iupdate (loc, 2, isub (loc2,2)); iupdate (loc, 3, isub (loc2,3)); ploc loc end val eput = #put stderr; val eflush = #flush stderr; fun loc_proc_2 (loc1, loc2, proc) = (proc, isub (loc1, 0), isub (loc1, 1), isub (loc2, 2), isub (loc2, 3)); fun loc_proc (loc, proc) = loc_proc_2 (loc, loc, proc); fun loc_proc_end (loc, proc) = (proc, isub (loc, 2), isub (loc, 3), isub (loc, 2), isub (loc, 3)); fun M_i i = let val f as |[convert, ...]| = outstring "M" in print f (pack (i:int)); convert () end; fun in_vars (i, k, loc, args, f) = if i=k then f (rev args) else let val Mi = M_i (i+1) in loc_proc (loc, SPI_IN (SPI_VAR "c_in", Mi, in_vars (i+1, k, loc, Mi::args, f))) end; val dummy_loc = iarray (4, 0); fun f_synthesizer (f, loc, k) = in_vars (0, k, loc, nil, fn args => loc_proc (loc, SPI_OUT (SPI_VAR "c_out", SPI_APPL (f, [SPI_VAR x | x in list args]), loc_proc (loc, SPI_ZERO)))); val synthesizer = ref ([f_synthesizer (f, dummy_loc, k) | f => k in map !private_funs <-| !funs]) fun vars_upto k = let val ir = ref 0 in [(inc ir; M_i (!ir)) |while !ir k in map !constructors <| !funs]) fun newvar loc = let val f as |[put, convert, ...]| = outstring "__Z_" in print f (pack (isub (loc, 0))); put "_"; print f (pack (isub (loc, 1))); put "_"; print f (pack (isub (loc, 2))); put "_"; print f (pack (isub (loc, 3))); convert () end; fun var_of_term (SPI_VAR x) = x | var_of_term t = gensym "__Var_" (* let val f = outstring "__Var_" in print_spi_term (mangle f) t; #convert f () end *) (* fun tuple l = let val f as |[convert, ...]| = outstring "t" in print f (pack (len l)); SPI_APPL (convert (), l) end; *) fun tuple nil = SPI_APPL ("nil", nil) | tuple (t::l) = SPI_APPL ("cons", [t, tuple l]); fun fv (SPI_VAR x) = {x} | fv (SPI_APPL (_, l)) = union {fv t | t in list l}; fun pat_bv (SPI_VAR x) = {x} | pat_bv (SPI_APPL ("__eq", [_])) = {} | pat_bv (SPI_APPL ("crypt", [pat, t])) = pat_bv pat | pat_bv (SPI_APPL ("acrypt", [pat, t])) = pat_bv pat | pat_bv (SPI_APPL (f, l)) = patl_bv l and patl_bv l = union {pat_bv pat | pat in list l}; fun pat_fv (SPI_VAR _) = {} | pat_fv (SPI_APPL ("__eq", [t])) = fv t | pat_fv (SPI_APPL ("crypt", [pat, t])) = pat_fv pat U fv t | pat_fv (SPI_APPL ("acrypt", [pat, t])) = pat_fv pat U fv t | pat_fv (SPI_APPL (f, l)) = patl_fv l and patl_fv l = union {pat_fv pat | pat in list l}; fun mk_vars args = let val alreadyseen = ref ({} : string set) val vars = [let val var = ref (var_of_term t) in while !var inset !alreadyseen do var := !var ^ "'"; !var end | t in list args] in vars end; fun mk_let (loc, var :: othervars, arg :: otherargs, p) = if arg=SPI_VAR var then mk_let (loc, othervars, otherargs, p) else loc_proc_end (loc, SPI_LET (var, arg, mk_let (loc, othervars, otherargs, p))) | mk_let (_, _, _, p) = p exception MkIf; fun mk_if (SPI_DIFF (t, u), thenb, elseb) = mk_if (SPI_EQ (t, u), elseb, thenb) | mk_if (SPI_EQ (t, u), thenb, elseb) = SPI_IF (t, u, thenb, elseb) | mk_if arg = raise MkIf; exception MkPatsMatch; fun mk_pat_match (loc, pat as SPI_VAR x, u, thenb, elseb) = if pat=u then thenb else loc_proc_end (loc, SPI_LET (x, u, thenb)) | mk_pat_match (loc, SPI_APPL ("crypt", [pat, k]), u, thenb, elseb) = let val x = var_of_term pat in loc_proc_end (loc, SPI_DECRYPT_SYM (u, x, k, mk_pat_match (loc, pat, SPI_VAR x, thenb, elseb), elseb)) end | mk_pat_match (loc, SPI_APPL ("acrypt", [pat, k]), u, thenb, elseb) = let val x = var_of_term pat in loc_proc_end (loc, SPI_DECRYPT_ASYM (u, x, k, mk_pat_match (loc, pat, SPI_VAR x, thenb, elseb), elseb)) end | mk_pat_match (loc, SPI_APPL ("__eq", [t]), u, thenb, elseb) = loc_proc_end (loc, mk_if (SPI_EQ (t, u), thenb, elseb)) | mk_pat_match (loc, SPI_APPL (f, pats), u, thenb, elseb) = let val vars = mk_vars pats in loc_proc_end (loc, SPI_DESTRUCT (u, f, vars, mk_pats_match (loc, pats, [SPI_VAR x | x in list vars], thenb, elseb), elseb)) end and mk_pats_match (_, nil, nil, thenb, _) = thenb | mk_pats_match (loc, pat::pats, u::us, thenb, elseb) = mk_pat_match (loc, pat, u, mk_pats_match (loc, pats, us, thenb, elseb), elseb) | mk_pats_match arg = raise MkPatsMatch; local val hyacc_error = NONE; val yydefault = fn hyd => SOME (hyacc_value hyd 0 handle _ => hyacc_default_value hyd); val yyfinal = 150 val yyflag = ~32768 val yyntbase = 38 val max_user_token = 292; val nsyms = 62; val yytranslate = [ 0, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37 ]; val yyprhs = [ 0, 0, 2, 4, 9, 13, 18, 23, 25, 27, 29, 33, 35, 40, 43, 44, 48, 52, 54, 59, 62, 64, 68, 73, 78, 80, 82, 84, 88, 89, 91, 95, 98, 103, 106, 112, 115, 118, 122, 127, 134, 142, 150, 157, 166, 171, 175, 181, 183, 185, 189, 191, 196, 198, 202, 205, 210, 215, 217, 220, 222, 225, 227, 229, 230, 233, 234 ]; val yyrhs = [ 60, 0, 3, 0, 3, 6, 41, 7, 0, 6, 40, 7, 0, 10, 40, 11, 39, 0, 8, 40, 9, 39, 0, 4, 0, 41, 0, 39, 0, 41, 12, 39, 0, 17, 0, 17, 8, 4, 9, 0, 43, 13, 0, 0, 39, 15, 39, 0, 39, 16, 39, 0, 3, 0, 3, 6, 47, 7, 0, 15, 39, 0, 32, 0, 6, 46, 7, 0, 10, 46, 11, 39, 0, 8, 46, 9, 39, 0, 4, 0, 47, 0, 45, 0, 47, 12, 45, 0, 0, 49, 0, 13, 43, 49, 0, 13, 43, 0, 6, 51, 7, 43, 0, 59, 43, 0, 59, 6, 41, 7, 43, 0, 42, 49, 0, 18, 43, 0, 19, 4, 48, 0, 20, 44, 22, 49, 0, 20, 44, 22, 49, 23, 49, 0, 24, 6, 39, 12, 46, 7, 48, 0, 25, 6, 39, 12, 40, 7, 48, 0, 26, 47, 15, 41, 24, 49, 0, 26, 47, 15, 41, 24, 49, 23, 49, 0, 27, 40, 21, 50, 0, 46, 31, 49, 0, 50, 23, 46, 31, 49, 0, 52, 0, 49, 0, 52, 28, 49, 0, 30, 0, 59, 61, 15, 51, 0, 54, 0, 55, 36, 54, 0, 53, 55, 0, 58, 59, 5, 43, 0, 57, 59, 5, 43, 0, 34, 0, 35, 34, 0, 33, 0, 35, 33, 0, 3, 0, 4, 0, 0, 60, 56, 0, 0, 6, 47, 7, 0 ]; val yyrline = [ 0, 342, 362, 383, 407, 408, 411, 414, 417, 426, 427, 430, 431, 434, 435, 438, 439, 442, 463, 487, 488, 489, 490, 498, 506, 509, 518, 519, 547, 548, 549, 550, 553, 554, 573, 594, 595, 596, 597, 599, 601, 608, 610, 628, 645, 653, 660, 669, 675, 676, 679, 682, 722, 723, 726, 735, 753, 771, 772, 775, 776, 779, 780, 784, 785, 788, 789 ]; val yytname = [| "$","error","$illegal.","identifier", "VAR","kw_slash","kw_open_paren","kw_close_paren","kw_open_bracket","kw_close_bracket", "kw_open_curly","kw_close_curly","kw_comma","kw_semicolon","kw_period","kw_equal", "kw_different","kw_bang","kw_zero","kw_new","kw_if","kw_of","kw_then","kw_else", "kw_in","kw_out","kw_let","kw_case","kw_par","kw_event","kw_proc","kw_implies", "kw_any","kw_data","kw_fun","kw_private","kw_and","kw_eof","spi","term","term_sequence", "term_list","bang","optional_semicolon","fact","pattern","pattern_sequence", "pattern_list","continuation","atomic_process","matches","process","process_list", "proc","single_proc_declaration","proc_declaration","declaration","fun","data", "id_or_var","declaration_list","optional_args","" |]; val yyr1 = [ 0, 38, 39, 39, 39, 39, 39, 39, 40, 41, 41, 42, 42, 43, 43, 44, 44, 45, 45, 45, 45, 45, 45, 45, 45, 46, 47, 47, 48, 48, 48, 48, 49, 49, 49, 49, 49, 49, 49, 49, 49, 49, 49, 49, 49, 50, 50, 51, 52, 52, 53, 54, 55, 55, 56, 56, 56, 57, 57, 58, 58, 59, 59, 60, 60, 61, 61 ]; val yyr2 = [ 0, 1, 1, 4, 3, 4, 4, 1, 1, 1, 3, 1, 4, 2, 0, 3, 3, 1, 4, 2, 1, 3, 4, 4, 1, 1, 1, 3, 0, 1, 3, 2, 4, 2, 5, 2, 2, 3, 4, 6, 7, 7, 6, 8, 4, 3, 5, 1, 1, 3, 1, 4, 1, 3, 2, 4, 4, 1, 2, 1, 2, 1, 1, 0, 2, 0, 3 ]; val yydefact = [ 63, 1, 50, 59, 57, 0, 0, 64, 0, 0, 60, 58, 61, 62, 52, 54, 65, 0, 0, 0, 0, 0, 14, 14, 53, 17, 24, 0, 0, 0, 0, 20, 26, 0, 0, 56, 55, 0, 0, 25, 0, 0, 2, 7, 0, 0, 0, 19, 66, 0, 0, 11, 14, 0, 0, 0, 0, 0, 0, 0, 48, 51, 47, 14, 13, 0, 21, 0, 0, 0, 9, 0, 8, 0, 0, 27, 0, 0, 36, 28, 0, 0, 0, 0, 0, 0, 35, 0, 0, 33, 18, 23, 22, 0, 4, 0, 0, 0, 14, 0, 14, 37, 29, 0, 0, 0, 0, 0, 0, 0, 49, 0, 3, 10, 6, 5, 32, 12, 31, 15, 16, 38, 0, 0, 0, 0, 44, 14, 30, 0, 0, 0, 0, 0, 0, 34, 39, 28, 28, 42, 45, 0, 40, 41, 0, 0, 43, 46, 0, 0, 0 ]; val yydefgoto = [ 148, 70, 71, 72, 59, 35, 81, 32, 38, 39, 101, 102, 126, 61, 62, 6, 14, 15, 7, 8, 9, 63, 1, 21 ]; val yypact = [~ 32768, ~ 21,~ 32768,~ 32768,~ 32768,~ 15, 60,~ 32768, 60, 60,~ 32768, ~ 32768,~ 32768,~ 32768,~ 32768,~ 25, 34, 37, 41, 60, 18, 40,~ 32768,~ 32768,~ 32768, 43,~ 32768, 18, 18, 18, 48, ~ 32768,~ 32768, 3, 150, 62, 62, 18, 58, 65, 70, 74, 80,~ 32768, 48, 48, 48,~ 32768,~ 32768, 18, 150, 79,~ 32768, 84, 48, 83, 85, 18, 48, 150,~ 32768, ~ 32768, 64, 87,~ 32768, 22,~ 32768, 48, 48, 48,~ 32768, 90, 78, 91, 96,~ 32768, 94, 98, 62, 100, 52, 72, 48, 48, 24, 88,~ 32768, 150, 48, 62,~ 32768, ~ 32768,~ 32768, 50,~ 32768, 48, 48, 48,~ 32768, 103,~ 32768, ~ 32768,~ 32768, 48, 48, 150, 102, 104, 48, 18,~ 32768, 54,~ 32768,~ 32768,~ 32768,~ 32768, 62,~ 32768, 125,~ 32768,~ 32768, 92, 18, 48, 8, 99, 109,~ 32768,~ 32768, 150, 114, 115, 150, 150, 18, 62,~ 32768, 100, 100, 110,~ 32768, 105,~ 32768,~ 32768, 150, 150,~ 32768,~ 32768, 123, 134,~ 32768 ]; val yypgoto = [~ 32768, ~ 23,~ 41,~ 61,~ 32768,~ 22,~ 32768, 86,~ 26,~ 14,~ 68, ~ 34,~ 32768, 89,~ 32768,~ 32768, 118,~ 32768,~ 32768,~ 32768,~ 32768, 29,~ 32768,~ 32768 ]; val yylast = 177 val yytable = [ 60, 36, 40, 41, 73, 74, 33, 47, 93, 2, 48, 19, 3, 4, 5, 49, 60, 85, 10, 11, 95, 25, 26, 65, 27, 86, 28, 111, 29, 90, 78, 80, 132, 30, 49, 16, 49, 17, 18, 108, 20, 89, 22, 84, 91, 92, 23, 124, 16, 37, 31, 42, 43, 110, 44, 34, 45, 112, 46, 106, 107, 127, 95, 12, 13, 66, 95, 103, 104, 142, 143, 121, 113, 114, 115, 64, 116, 49, 118, 67, 119, 120, 131, 125, 128, 68, 69, 77, 79, 82, 95, 83, 87, 88, 105, 136, 130, 94, 139, 140, 96, 98, 99, 12, 13, 135, 50, 97, 141, 109, 146, 147, 117, 100, 122, 129, 123, 51, 52, 53, 54, 137, 138, 149, 55, 56, 57, 58, 12, 13, 133, 50, 134, 144, 150, 75, 145, 24, 64, 76, 0, 0, 51, 52, 53, 54, 0, 0, 0, 55, 56, 57, 58, 12, 13, 0, 50, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 51, 52, 53, 54, 0, 0, 0, 55, 56, 57, 58 ]; val yycheck = [ 34, 23, 28, 29, 45, 46, 20, 30, 69, 30, 7, 36, 33, 34, 35, 12, 50, 58, 33, 34, 12, 3, 4, 37, 6, 59, 8, 88, 10, 7, 52, 54, 24, 15, 12, 6, 12, 8, 9, 15, 6, 63, 5, 57, 67, 68, 5, 108, 19, 6, 32, 3, 4, 87, 6, 15, 8, 7, 10, 82, 83, 7, 12, 3, 4, 7, 12, 15, 16, 137, 138, 105, 95, 96, 97, 13, 98, 12, 100, 9, 103, 104, 123, 109, 118, 11, 6, 8, 4, 6, 12, 6, 28, 6, 22, 129, 122, 7, 132, 133, 9, 7, 4, 3, 4, 127, 6, 11, 134, 21, 144, 145, 9, 13, 12, 23, 12, 17, 18, 19, 20, 7, 7, 0, 24, 25, 26, 27, 3, 4, 31, 6, 23, 23, 0, 49, 31, 19, 13, 50,~ 1, ~ 1, 17, 18, 19, 20,~ 1,~ 1,~ 1, 24, 25, 26, 27, 3, 4,~ 1, 6,~ 1,~ 1,~ 1,~ 1, ~ 1,~ 1,~ 1,~ 1,~ 1,~ 1, 17, 18, 19, 20, ~ 1,~ 1,~ 1, 24, 25, 26, 27 ]; val yyaction = [yydefault, (fn hyd => ( let val spi_value = hyacc_value hyd val sdl spi_val0 = spi_value ~0 val spi_location = hyacc_location hyd val spi_loc0 = spi_location ~0 in let val procs = {f => (args, p) | SPI_PROC (f, args, p) in list spi_val0} in if "main" inset procs then (SOME o spi) |[funs = !funs, constructors = !constructors, processes = procs ++ {"dy_synthesizer" => (["c_in", "c_out"], spi_par (dummy_loc, !synthesizer)), "dy_analyzer" => (["c_in", "c_out"], spi_par (dummy_loc, !analyzer))} ]| else (eput "Line "; ploc spi_loc0; eput ": identifier 'main' undefined. "; hyacc_error) end end)), (fn hyd => ( let val spi_value = hyacc_value hyd val string spi_val0 = spi_value ~0 val spi_location = hyacc_location hyd val spi_loc0 = spi_location ~0 in if is_fun spi_val0 then let val expected_n = fun_arity spi_val0 in if expected_n <> 0 then (eput "Line "; ploc spi_loc0; eput ": identifier "; eput spi_val0; eput " expects "; print stderr (pack expected_n); eput (if expected_n<=1 then " argument" else " arguments"); eput ", got none. "; hyacc_error) else (SOME o st) (SPI_APPL (spi_val0, nil)) end else (eput "Line "; ploc spi_loc0; eput ": identifier "; eput spi_val0; eput " undeclared. "; hyacc_error) end)), (fn hyd => ( let val spi_value = hyacc_value hyd val string spi_val3 = spi_value ~3 val stl spi_val1 = spi_value ~1 val spi_location = hyacc_location hyd val spi_loc3 = spi_location ~3 in if is_fun spi_val3 then let val n = len spi_val1 val expected_n = fun_arity spi_val3 in if expected_n <> n then (eput "Line "; ploc spi_loc3; eput ": identifier "; eput spi_val3; eput " expects "; print stderr (pack expected_n); eput (if expected_n<=1 then " argument" else " arguments"); eput ", got "; print stderr (pack n); eput ". "; hyacc_error) else (SOME o st) (SPI_APPL (spi_val3, rev spi_val1)) end else (eput "Line "; ploc spi_loc3; eput ": identifier "; eput spi_val3; eput " undeclared. "; hyacc_error) end)), (fn hyd => ( let val spi_value = hyacc_value hyd val st spi_val1 = spi_value ~1 in (SOME o st) spi_val1 end)), (fn hyd => ( let val spi_value = hyacc_value hyd val st spi_val2 = spi_value ~2 val st spi_val0 = spi_value ~0 in (SOME o st) (SPI_APPL ("crypt", [spi_val2, spi_val0])) end)), (fn hyd => ( let val spi_value = hyacc_value hyd val st spi_val2 = spi_value ~2 val st spi_val0 = spi_value ~0 in (SOME o st) (SPI_APPL ("acrypt", [spi_val2, spi_val0])) end)), (fn hyd => ( let val spi_value = hyacc_value hyd val string spi_val0 = spi_value ~0 in (SOME o st) (SPI_VAR spi_val0) end)), (fn hyd => ( let val spi_value = hyacc_value hyd val stl spi_val0 = spi_value ~0 in (SOME o st) (case spi_val0 of nil => tuple nil | [t] => t | l => tuple (rev l)) end)), (fn hyd => ( let val spi_value = hyacc_value hyd val st spi_val0 = spi_value ~0 in (SOME o stl) [spi_val0] end)), (fn hyd => ( let val spi_value = hyacc_value hyd val st spi_val0 = spi_value ~0 val stl spi_val2 = spi_value ~2 in (SOME o stl) (spi_val0::spi_val2) end)), (fn hyd => ( (SOME o string) "Pid" )), (fn hyd => ( let val spi_value = hyacc_value hyd val string spi_val1 = spi_value ~1 in (SOME o string) spi_val1 end)), yydefault, yydefault, (fn hyd => ( let val spi_value = hyacc_value hyd val st spi_val2 = spi_value ~2 val st spi_val0 = spi_value ~0 in (SOME o sf) (SPI_EQ (spi_val2, spi_val0)) end)), (fn hyd => ( let val spi_value = hyacc_value hyd val st spi_val2 = spi_value ~2 val st spi_val0 = spi_value ~0 in (SOME o sf) (SPI_DIFF (spi_val2, spi_val0)) end)), (fn hyd => ( let val spi_value = hyacc_value hyd val string spi_val0 = spi_value ~0 val spi_location = hyacc_location hyd val spi_loc0 = spi_location ~0 in if is_constructor spi_val0 then let val expected_n = fun_arity spi_val0 in if expected_n <> 0 then (eput "Line "; ploc spi_loc0; eput ": identifier "; eput spi_val0; eput " expects "; print stderr (pack expected_n); eput (if expected_n<=1 then " argument" else " arguments"); eput ", got none. "; hyacc_error) else (SOME o st) (SPI_APPL (spi_val0, nil)) end else (eput "Line "; ploc spi_loc0; eput ": identifier "; eput spi_val0; eput " undeclared. "; hyacc_error) end)), (fn hyd => ( let val spi_value = hyacc_value hyd val string spi_val3 = spi_value ~3 val stl spi_val1 = spi_value ~1 val spi_location = hyacc_location hyd val spi_loc3 = spi_location ~3 in if is_constructor spi_val3 then let val n = len spi_val1 val expected_n = fun_arity spi_val3 in if expected_n <> n then (eput "Line "; ploc spi_loc3; eput ": identifier "; eput spi_val3; eput " expects "; print stderr (pack expected_n); eput (if expected_n<=1 then " argument" else " arguments"); eput ", got "; print stderr (pack n); eput ". "; hyacc_error) else (SOME o st) (SPI_APPL (spi_val3, rev spi_val1)) end else (eput "Line "; ploc spi_loc3; eput ": identifier "; eput spi_val3; eput " undeclared. "; hyacc_error) end)), (fn hyd => ( let val spi_value = hyacc_value hyd val st spi_val0 = spi_value ~0 in (SOME o st) (SPI_APPL ("__eq", [spi_val0])) end)), (fn hyd => ( let val spi_location = hyacc_location hyd val spi_loc0 = spi_location ~0 in (SOME o st) (SPI_VAR (newvar spi_loc0)) end)), (fn hyd => ( let val spi_value = hyacc_value hyd val st spi_val1 = spi_value ~1 in (SOME o st) spi_val1 end)), (fn hyd => ( let val spi_value = hyacc_value hyd val st spi_val2 = spi_value ~2 val st spi_val0 = spi_value ~0 val spi_location = hyacc_location hyd val spi_loc3 = spi_location ~3 val spi_loc0 = spi_location ~0 in case pat_bv spi_val2 & fv spi_val0 of {x, ...} => (eput "Line "; ploc2 (spi_loc3, spi_loc0); eput ": ambiguous pattern, variable "; eput x; eput " occurs both bound by plaintext pattern and free in key. "; hyacc_error) | _ => (SOME o st) (SPI_APPL ("crypt", [spi_val2, spi_val0])) end)), (fn hyd => ( let val spi_value = hyacc_value hyd val st spi_val2 = spi_value ~2 val st spi_val0 = spi_value ~0 val spi_location = hyacc_location hyd val spi_loc3 = spi_location ~3 val spi_loc0 = spi_location ~0 in case pat_bv spi_val2 & fv spi_val0 of {x, ...} => (eput "Line "; ploc2 (spi_loc3, spi_loc0); eput ": ambiguous pattern, variable "; eput x; eput " occurs both bound by plaintext pattern and free in key. "; hyacc_error) | _ => (SOME o st) (SPI_APPL ("acrypt", [spi_val2, spi_val0])) end)), (fn hyd => ( let val spi_value = hyacc_value hyd val string spi_val0 = spi_value ~0 in (SOME o st) (SPI_VAR spi_val0) end)), (fn hyd => ( let val spi_value = hyacc_value hyd val stl spi_val0 = spi_value ~0 in (SOME o st) (case spi_val0 of nil => tuple nil | [t] => t | l => tuple (rev l)) end)), (fn hyd => ( let val spi_value = hyacc_value hyd val st spi_val0 = spi_value ~0 in (SOME o stl) [spi_val0] end)), (fn hyd => ( let val spi_value = hyacc_value hyd val stl spi_val2 = spi_value ~2 val st spi_val0 = spi_value ~0 val spi_location = hyacc_location hyd val spi_loc0 = spi_location ~0 val spi_loc2 = spi_location ~2 in case patl_bv spi_val2 & pat_bv spi_val0 of {x, ...} => (eput "Line "; ploc spi_loc0; eput ": non-linear pattern, variable "; eput x; eput " occurs already at line "; ploc spi_loc2; eput ". "; hyacc_error) | _ => (case patl_bv spi_val2 & pat_fv spi_val0 of {x, ...} => (eput "Line "; ploc spi_loc2; eput ": ambiguous pattern, variable "; eput x; eput " occurs both bound in pattern\ \ and free at line "; ploc spi_loc0; eput ". "; hyacc_error) | _ => (case patl_fv spi_val2 & pat_bv spi_val0 of {x, ...} => (eput "Line "; ploc spi_loc0; eput ": ambiguous pattern, \ \variable "; eput x; eput " occurs both bound in\ \ pattern and free at line "; ploc spi_loc2; eput ". "; hyacc_error) | _ => (SOME o stl) (spi_val0::spi_val2))) end)), (fn hyd => ( let val spi_location = hyacc_location hyd val spi_loc0 = spi_location ~0 in (SOME o sp) (loc_proc_end (spi_loc0, SPI_ZERO)) end)), (fn hyd => ( let val spi_value = hyacc_value hyd val sp spi_val0 = spi_value ~0 in (SOME o sp) spi_val0 end)), (fn hyd => ( let val spi_value = hyacc_value hyd val sp spi_val0 = spi_value ~0 in (SOME o sp) spi_val0 end)), (fn hyd => ( let val spi_location = hyacc_location hyd val spi_loc1 = spi_location ~1 in (SOME o sp) (loc_proc_end (spi_loc1, SPI_ZERO)) end)), (fn hyd => ( let val spi_value = hyacc_value hyd val sp spi_val2 = spi_value ~2 in (SOME o sp) spi_val2 end)), (fn hyd => ( let val spi_value = hyacc_value hyd val string spi_val1 = spi_value ~1 val spi_location = hyacc_location hyd val spi_loc1 = spi_location ~1 val spi_loc0 = spi_location ~0 in let val n = if spi_val1 inset !procs then ?(!procs) spi_val1 else if spi_val1 inset !expected_procs then ?(!expected_procs) spi_val1 else (expected_procs := {spi_val1 => 0}; 0) in if n=0 then (SOME o sp) (loc_proc (spi_loc1, SPI_CALL (spi_val1, nil))) else (eput "Line "; ploc spi_loc0; eput ": expected "; print stderr (pack n); eput (if n<=1 then " argument" else " arguments"); eput ", got none. "; hyacc_error) end end)), (fn hyd => ( let val spi_value = hyacc_value hyd val stl spi_val2 = spi_value ~2 val string spi_val4 = spi_value ~4 val spi_location = hyacc_location hyd val spi_loc4 = spi_location ~4 val spi_loc1 = spi_location ~1 val spi_loc3 = spi_location ~3 in let val args = rev spi_val2 val nargs = len args val n = if spi_val4 inset !procs then ?(!procs) spi_val4 else if spi_val4 inset !expected_procs then ?(!expected_procs) spi_val4 else (expected_procs := {spi_val4 => nargs}; nargs) in if n=nargs then (SOME o sp) (loc_proc_2 (spi_loc4, spi_loc1, SPI_CALL (spi_val4, args))) else (eput "Line "; ploc spi_loc3; eput ": expected "; print stderr (pack n); eput (if n<=1 then " argument" else " arguments"); eput ", got "; print stderr (pack nargs); eput ". "; hyacc_error) end end)), (fn hyd => ( let val spi_location = hyacc_location hyd val spi_loc1 = spi_location ~1 val spi_value = hyacc_value hyd val string spi_val1 = spi_value ~1 val sp spi_val0 = spi_value ~0 in (SOME o sp) (loc_proc_2 (spi_loc1, spi_loc1, SPI_BANG (spi_val1, spi_val0))) end)), (fn hyd => ( let val spi_location = hyacc_location hyd val spi_loc1 = spi_location ~1 in (SOME o sp) (loc_proc (spi_loc1, SPI_ZERO)) end)), (fn hyd => ( let val spi_location = hyacc_location hyd val spi_loc2 = spi_location ~2 val spi_loc1 = spi_location ~1 val spi_value = hyacc_value hyd val string spi_val1 = spi_value ~1 val sp spi_val0 = spi_value ~0 in (SOME o sp) (loc_proc_2 (spi_loc2, spi_loc1, SPI_NEW (spi_val1, spi_val0))) end)), (fn hyd => ( let val spi_location = hyacc_location hyd val spi_loc3 = spi_location ~3 val spi_loc2 = spi_location ~2 val spi_value = hyacc_value hyd val sf spi_val2 = spi_value ~2 val sp spi_val0 = spi_value ~0 val spi_loc0 = spi_location ~0 in (SOME o sp) (loc_proc_2 (spi_loc3, spi_loc2, mk_if (spi_val2, spi_val0, loc_proc_end (spi_loc0, SPI_ZERO)))) end)), (fn hyd => ( let val spi_location = hyacc_location hyd val spi_loc5 = spi_location ~5 val spi_loc4 = spi_location ~4 val spi_value = hyacc_value hyd val sf spi_val4 = spi_value ~4 val sp spi_val2 = spi_value ~2 val sp spi_val0 = spi_value ~0 in (SOME o sp) (loc_proc_2 (spi_loc5, spi_loc4, mk_if (spi_val4, spi_val2, spi_val0))) end)), (fn hyd => ( let val spi_value = hyacc_value hyd val st spi_val2 = spi_value ~2 val spi_location = hyacc_location hyd val spi_loc6 = spi_location ~6 val spi_loc1 = spi_location ~1 val st spi_val4 = spi_value ~4 val sp spi_val0 = spi_value ~0 in let val x = var_of_term spi_val2 in (SOME o sp) (loc_proc_2 (spi_loc6, spi_loc1, SPI_IN (spi_val4, x, mk_pat_match (spi_loc1, spi_val2, SPI_VAR x, spi_val0, loc_proc_end (spi_loc1, SPI_ZERO))))) end end)), (fn hyd => ( let val spi_location = hyacc_location hyd val spi_loc6 = spi_location ~6 val spi_loc1 = spi_location ~1 val spi_value = hyacc_value hyd val st spi_val4 = spi_value ~4 val st spi_val2 = spi_value ~2 val sp spi_val0 = spi_value ~0 in (SOME o sp) (loc_proc_2 (spi_loc6, spi_loc1, SPI_OUT (spi_val4, spi_val2, spi_val0))) end)), (fn hyd => ( let val spi_value = hyacc_value hyd val stl spi_val4 = spi_value ~4 val stl spi_val2 = spi_value ~2 val spi_location = hyacc_location hyd val spi_loc2 = spi_location ~2 val spi_loc5 = spi_location ~5 val spi_loc1 = spi_location ~1 val sp spi_val0 = spi_value ~0 val spi_loc0 = spi_location ~0 in let val patlen = len spi_val4 val tlen = len spi_val2 in if patlen<>tlen then (eput "Line "; ploc spi_loc2; eput ": expecting "; print stderr (pack patlen); eput (if patlen<=1 then " term" else " terms"); eput ", got "; print stderr (pack tlen); eput ". "; hyacc_error) else (SOME o sp) (loc_proc_2 (spi_loc5, spi_loc2, #1 (mk_pats_match (spi_loc1, spi_val4, spi_val2, spi_val0, loc_proc_end (spi_loc0, SPI_ZERO))))) end end)), (fn hyd => ( let val spi_value = hyacc_value hyd val stl spi_val6 = spi_value ~6 val stl spi_val4 = spi_value ~4 val spi_location = hyacc_location hyd val spi_loc4 = spi_location ~4 val spi_loc7 = spi_location ~7 val spi_loc3 = spi_location ~3 val sp spi_val2 = spi_value ~2 val sp spi_val0 = spi_value ~0 in let val patlen = len spi_val6 val tlen = len spi_val4 in if patlen<>tlen then (eput "Line "; ploc spi_loc4; eput ": expecting "; print stderr (pack patlen); eput (if patlen<=1 then " term" else " terms"); eput ", got "; print stderr (pack tlen); eput ". "; hyacc_error) else (SOME o sp) (loc_proc_2 (spi_loc7, spi_loc4, #1 (mk_pats_match (spi_loc3, spi_val6, spi_val4, spi_val2, spi_val0)))) end end)), (fn hyd => ( let val spi_value = hyacc_value hyd val scase spi_val0 = spi_value ~0 val st spi_val2 = spi_value ~2 val spi_location = hyacc_location hyd val spi_loc0 = spi_location ~0 in (SOME o sp) (spi_val0 (spi_val2, loc_proc_end (spi_loc0, SPI_ZERO))) end)), (fn hyd => ( let val spi_location = hyacc_location hyd val spi_loc2 = spi_location ~2 val spi_loc1 = spi_location ~1 val spi_value = hyacc_value hyd val st spi_val2 = spi_value ~2 val sp spi_val0 = spi_value ~0 in let val loc1 = spi_loc2 val loc2 = spi_loc1 in (SOME o scase) (fn (u, cont) => loc_proc_2 (loc1, loc2, #1 (mk_pat_match (loc2, spi_val2, u, spi_val0, cont)))) end end)), (fn hyd => ( let val spi_location = hyacc_location hyd val spi_loc2 = spi_location ~2 val spi_loc1 = spi_location ~1 val spi_value = hyacc_value hyd val scase spi_val4 = spi_value ~4 val st spi_val2 = spi_value ~2 val sp spi_val0 = spi_value ~0 in let val loc1 = spi_loc2 val loc2 = spi_loc1 in (SOME o scase) (fn (u, cont) => spi_val4 (u, loc_proc_2 (loc1, loc2, #1 (mk_pat_match (loc2, spi_val2, u, spi_val0, cont))))) end end)), (fn hyd => ( let val spi_value = hyacc_value hyd val spl spi_val0 = spi_value ~0 val spi_location = hyacc_location hyd val spi_loc0 = spi_location ~0 in case spi_val0 of [p] => (SOME o sp) p | _ => (SOME o sp) (spi_par (spi_loc0, rev spi_val0)) end)), (fn hyd => ( let val spi_value = hyacc_value hyd val sp spi_val0 = spi_value ~0 in (SOME o spl) [spi_val0] end)), (fn hyd => ( let val spi_value = hyacc_value hyd val sp spi_val0 = spi_value ~0 val spl spi_val2 = spi_value ~2 in (SOME o spl) (spi_val0::spi_val2) end)), (fn hyd => ( expected_procs := {}; (SOME o spinone) () )), (fn hyd => ( let val spi_value = hyacc_value hyd val string spi_val3 = spi_value ~3 val spi_location = hyacc_location hyd val spi_loc3 = spi_location ~3 val stl spi_val2 = spi_value ~2 val spi_loc1 = spi_location ~1 val sp spi_val0 = spi_value ~0 val spi_loc0 = spi_location ~0 in if spi_val3 inset !procs then (eput "Line "; ploc spi_loc3; eput ": attempt to redefine process "; eput spi_val3; eput ". "; hyacc_error) else let val nargs = len spi_val2 val vars = mk_vars spi_val2 in if spi_val3 inset !expected_procs then let val n = ?(!expected_procs) spi_val3 in if n=nargs then (procs := !procs ++ {spi_val3 => n}; expected_procs := {spi_val3} <-| !expected_procs; (SOME o sd) (SPI_PROC (spi_val3, vars, mk_pats_match (spi_loc1, spi_val2, [SPI_VAR x | x in list vars], spi_val0, loc_proc_end (spi_loc0, SPI_ZERO))))) else (eput "Line "; ploc spi_loc3; eput ": was used previously on "; print stderr (pack n); eput (if n<=1 then " argument" else " arguments"); eput ", defined here as taking "; print stderr (pack nargs); eput ". "; hyacc_error) end else (procs := !procs ++ {spi_val3 => nargs}; (SOME o sd) (SPI_PROC (spi_val3, vars, mk_pats_match (spi_loc1, spi_val2, [SPI_VAR x | x in list vars], spi_val0, loc_proc_end (spi_loc0, SPI_ZERO))))) end end)), (fn hyd => ( let val spi_value = hyacc_value hyd val sd spi_val0 = spi_value ~0 in (SOME o sdl) [spi_val0] end)), (fn hyd => ( let val spi_value = hyacc_value hyd val sd spi_val0 = spi_value ~0 val sdl spi_val2 = spi_value ~2 in (SOME o sdl) (spi_val0::spi_val2) end)), (fn hyd => ( let val spi_value = hyacc_value hyd val sdl spi_val0 = spi_value ~0 val spi_location = hyacc_location hyd val spi_loc1 = spi_location ~1 val spi_loc0 = spi_location ~0 in (case !expected_procs of {} => (SOME o sdl) spi_val0 | {f => _, ...} => (eput "Line "; ploc2 (spi_loc1, spi_loc0); eput ": process "; eput f; eput " called, not defined. "; hyacc_error)) end)), (fn hyd => ( let val spi_value = hyacc_value hyd val string spi_val2 = spi_value ~2 val spi_location = hyacc_location hyd val spi_loc2 = spi_location ~2 val string spi_val1 = spi_value ~1 val sb spi_val3 = spi_value ~3 in if is_fun spi_val2 then (eput "Line "; ploc spi_loc2; eput ": identifier "; eput spi_val2; eput " already declared, redeclaration ignored. "; hyacc_error) else let val n = intofstring (substr (spi_val1, 1, size spi_val1)) in funs := !funs ++ {spi_val2 => n}; constructors := !constructors ++ {spi_val2}; if spi_val3 then private_funs := !private_funs U {spi_val2} else (synthesizer := f_synthesizer (spi_val2, spi_loc2, n) :: !synthesizer; analyzer := f_analyzer (spi_val2, spi_loc2, n) :: !analyzer); (SOME o sdl) nil end end)), (fn hyd => ( let val spi_value = hyacc_value hyd val string spi_val2 = spi_value ~2 val spi_location = hyacc_location hyd val spi_loc2 = spi_location ~2 val string spi_val1 = spi_value ~1 val sb spi_val3 = spi_value ~3 in if is_fun spi_val2 then (eput "Line "; ploc spi_loc2; eput ": identifier "; eput spi_val2; eput " already declared, redeclaration ignored. "; hyacc_error) else let val n = intofstring (substr (spi_val1, 1, size spi_val1)) in funs := !funs ++ {spi_val2 => n}; if spi_val3 then private_funs := !private_funs U {spi_val2} else synthesizer := f_synthesizer (spi_val2, spi_loc2, n) :: !synthesizer; (SOME o sdl) nil end end)), (fn hyd => ( (SOME o sb) false )), (fn hyd => ( (SOME o sb) true )), (fn hyd => ( (SOME o sb) false )), (fn hyd => ( (SOME o sb) true )), (fn hyd => ( let val spi_value = hyacc_value hyd val string spi_val0 = spi_value ~0 in (SOME o string) spi_val0 end)), (fn hyd => ( let val spi_value = hyacc_value hyd val string spi_val0 = spi_value ~0 in (SOME o string) spi_val0 end)), (fn hyd => ( (SOME o sdl) nil )), (fn hyd => ( let val spi_value = hyacc_value hyd val sdl spi_val0 = spi_value ~0 val sdl spi_val1 = spi_value ~1 in (SOME o sdl) (spi_val0 @ spi_val1) end)), (fn hyd => ( (SOME o stl) nil )), (fn hyd => ( let val spi_value = hyacc_value hyd val stl spi_val1 = spi_value ~1 in (SOME o stl) (rev spi_val1) end)) ] in val spiparse = hyacc (hyacc_tables (yyaction, yytname, yyfinal, yyflag, yyntbase, max_user_token, nsyms, yylast, yyr1, yyr2, yydefact, yydefgoto, yypact, yypgoto, yytable, yycheck, yytranslate, yyprhs, yyrhs, yyrline)) end;