try.ocamlpro.com of TAPL https://github.com/roehst/tapl-implementations/blob/master/fomsub/syntax.ml

gistfile1.txt

https://try.ocamlpro.com/#code/open'Format!!exception'Exit'of'int!!type'info'='FI'of'string'*'int'*'int'$5'UNKNOWN!type'$,a'withinfo'='$4i:'info;'v:'$,a$6!!let'dummyinfo'='UNKNOWN!let'createInfo'f'l'c'='FI(f,'l,'c)!!let'errf'f'=!print_flush();!open_vbox'0;!open_hvbox'0;'f();'print_cut();'close_box();'print_newline();!raise'(Exit'1)!!let'printInfo'=!''(*'In'the'text'of'the'book,'file'positions'in'error'messages'are'replaced!with'the'string'$(Error:$('*)!function!FI(f,l,c)'-$.!print_string'f;!print_string'$(:$(;!print_int'l;'print_string'$(.$(;!print_int'c;'print_string'$(:$(!$5'UNKNOWN'-$.!print_string'$($-Unknown'file'and'line$.:'$(!!let'errfAt'fi'f'='errf(fun()-$.'printInfo'fi;'print_space();'f())!!let'err's'='errf'(fun()-$.'print_string'$(Error:'$(;'print_string's;'print_newline())!!let'error'fi's'='errfAt'fi'(fun()-$.'print_string's;'print_newline())!!let'warning's'=!print_string'$(Warning:'$(;'print_string's;!print_newline()!!let'warningAt'fi's'=!printInfo'fi;'print_string'$('Warning:'$(;!print_string's;'print_newline()!!(*'The'printing'functions'call'these'utility'functions'to'insert'grouping!''information'and'line-breaking'hints'for'the'pretty-printing'library:!'''''obox'''Open'a'$(box$('whose'contents'will'be'indented'by'two'spaces'if!''''''''''''the'whole'box'cannot'fit'on'the'current'line!'''''obox0''Same'but'indent'continuation'lines'to'the'same'column'as'the!''''''''''''beginning'of'the'box'rather'than'2'more'columns'to'the'right!'''''cbox'''Close'the'current'box!'''''break''Insert'a'breakpoint'indicating'where'the'line'maybe'broken'if!''''''''''''necessary.!''See'the'documentation'for'the'Format'module'in'the'OCaml'library'for!''more'details.'!*)!!let'obox()'='open_hvbox'2!!let'obox0()'='open_hvbox'0!!let'cbox()'='close_box()!let'break()'='print_break'0'0!let'pr'='Format.print_string!!type'kind'=!KnStar!$5'KnArr'of'kind'*'kind!!type'ty'=!TyTop!$5'TyVar'of'int'*'int!$5'TyArr'of'ty'*'ty!$5'TyAll'of'string'*'ty'*'ty!$5'TyAbs'of'string'*'kind'*'ty!$5'TyApp'of'ty'*'ty!!type'term'=!TmVar'of'info'*'int'*'int!$5'TmAbs'of'info'*'string'*'ty'*'term!$5'TmApp'of'info'*'term'*'term!$5'TmTAbs'of'info'*'string'*'ty'*'term!$5'TmTApp'of'info'*'term'*'ty!!type'binding'=!NameBind!$5'VarBind'of'ty!$5'TyVarBind'of'ty!!type'context'='(string'*'binding)'list!!type'command'=!$5'Eval'of'info'*'term!$5'Bind'of'info'*'string'*'binding!!(*'----------------------------------------------------------------------'*)!(*'Context'management'*)!!let'emptycontext'='$/$1!!let'ctxlength'ctx'='List.length'ctx!!let'addbinding'ctx'x'bind'='(x,bind)::ctx!!let'addname'ctx'x'='addbinding'ctx'x'NameBind!!let'rec'isnamebound'ctx'x'=!match'ctx'with!$/$1'-$.'false!$5'(y,_)::rest'-$.!if'y=x'then'true!else'isnamebound'rest'x!!let'rec'pickfreshname'ctx'x'=!if'isnamebound'ctx'x'then'pickfreshname'ctx'(x$2$($,$()!else'((x,NameBind)::ctx),'x!!let'index2name'fi'ctx'x'=!try!let'(xn,_)'='List.nth'ctx'x'in!xn!with'Failure'_'-$.!let'msg'=!Printf.sprintf'$(Variable'lookup'failure:'offset:'$+d,'ctx'size:'$+d$('in!error'fi'(msg'x'(List.length'ctx))!!let'rec'name2index'fi'ctx'x'=!match'ctx'with!$/$1'-$.'error'fi'($(Identifier'$('$2'x'$2'$('is'unbound$()!$5'(y,_)::rest'-$.!if'y=x'then'0!else'1'+'(name2index'fi'rest'x)!!(*'----------------------------------------------------------------------'*)!(*'Shifting'*)!!let'tymap'onvar'c'tyT'=!let'rec'walk'c'tyT'='match'tyT'with!TyArr(tyT1,tyT2)'-$.'TyArr(walk'c'tyT1,walk'c'tyT2)!$5'TyTop'-$.'TyTop!$5'TyVar(x,n)'-$.'onvar'c'x'n!$5'TyAll(tyX,tyT1,tyT2)'-$.'TyAll(tyX,walk'c'tyT1,walk'(c+1)'tyT2)!$5'TyAbs(tyX,knK1,tyT2)'-$.'TyAbs(tyX,knK1,walk'(c+1)'tyT2)!$5'TyApp(tyT1,tyT2)'-$.'TyApp(walk'c'tyT1,walk'c'tyT2)!in'walk'c'tyT!!let'tmmap'onvar'ontype'c't'=!let'rec'walk'c't'='match't'with!TmVar(fi,x,n)'-$.'onvar'fi'c'x'n!$5'TmAbs(fi,x,tyT1,t2)'-$.'TmAbs(fi,x,ontype'c'tyT1,walk'(c+1)'t2)!$5'TmApp(fi,t1,t2)'-$.'TmApp(fi,walk'c't1,walk'c't2)!$5'TmTAbs(fi,tyX,tyT1,t2)'-$.!TmTAbs(fi,tyX,ontype'c'tyT1,walk'(c+1)'t2)!$5'TmTApp(fi,t1,tyT2)'-$.'TmTApp(fi,walk'c't1,ontype'c'tyT2)!in'walk'c't!!let'typeShiftAbove'd'c'tyT'=!tymap!(fun'c'x'n'-$.'if'x$.=c'then'TyVar(x+d,n+d)'else'TyVar(x,n+d))!c'tyT!!let'termShiftAbove'd'c't'=!tmmap!(fun'fi'c'x'n'-$.'if'x$.=c'then'TmVar(fi,x+d,n+d)!else'TmVar(fi,x,n+d))!(typeShiftAbove'd)!c't!!let'termShift'd't'='termShiftAbove'd'0't!!let'typeShift'd'tyT'='typeShiftAbove'd'0'tyT!!let'bindingshift'd'bind'=!match'bind'with!NameBind'-$.'NameBind!$5'VarBind(tyT)'-$.'VarBind(typeShift'd'tyT)!$5'TyVarBind(tyS)'-$.'TyVarBind(typeShift'd'tyS)!!(*'----------------------------------------------------------------------'*)!(*'Substitution'*)!!let'termSubst'j's't'=!tmmap!(fun'fi'j'x'n'-$.'if'x=j'then'termShift'j's'else'TmVar(fi,x,n))!(fun'j'tyT'-$.'tyT)!j't!!let'termSubstTop's't'=!termShift'(-1)'(termSubst'0'(termShift'1's)'t)!!let'typeSubst'tyS'j'tyT'=!tymap!(fun'j'x'n'-$.'if'x=j'then'(typeShift'j'tyS)'else'(TyVar(x,n)))!j'tyT!!let'typeSubstTop'tyS'tyT'=!typeShift'(-1)'(typeSubst'(typeShift'1'tyS)'0'tyT)!!let'rec'tytermSubst'tyS'j't'=!tmmap'(fun'fi'c'x'n'-$.'TmVar(fi,x,n))!(fun'j'tyT'-$.'typeSubst'tyS'j'tyT)'j't!!let'tytermSubstTop'tyS't'=!termShift'(-1)'(tytermSubst'(typeShift'1'tyS)'0't)!!(*'----------------------------------------------------------------------'*)!(*'Context'management'(continued)'*)!!let'rec'getbinding'fi'ctx'i'=!try!let'(_,bind)'='List.nth'ctx'i'in!bindingshift'(i+1)'bind!with'Failure'_'-$.!let'msg'=!Printf.sprintf'$(Variable'lookup'failure:'offset:'$+d,'ctx'size:'$+d$('in!error'fi'(msg'i'(List.length'ctx))!let'getTypeFromContext'fi'ctx'i'=!match'getbinding'fi'ctx'i'with!VarBind(tyT)'-$.'tyT!$5'_'-$.'error'fi!($(getTypeFromContext:'Wrong'kind'of'binding'for'variable'$(!$2'(index2name'fi'ctx'i))!!let'rec'maketop'k'='match'k'with!KnStar'-$.'TyTop!$5'KnArr(knK1,knK2)'-$.'TyAbs($(_$(,knK1,maketop'knK2)!(*'----------------------------------------------------------------------'*)!(*'Extracting'file'info'*)!!let'tmInfo't'='match't'with!TmVar(fi,_,_)'-$.'fi!$5'TmAbs(fi,_,_,_)'-$.'fi!$5'TmApp(fi,'_,'_)'-$.'fi!$5'TmTAbs(fi,_,_,_)'-$.'fi!$5'TmTApp(fi,_,'_)'-$.'fi!!(*'----------------------------------------------------------------------'*)!(*'Printing'*)!!(*'The'printing'functions'call'these'utility'functions'to'insert'grouping!''information'and'line-breaking'hints'for'the'pretty-printing'library:!'''''obox'''Open'a'$(box$('whose'contents'will'be'indented'by'two'spaces'if!''''''''''''the'whole'box'cannot'fit'on'the'current'line!'''''obox0''Same'but'indent'continuation'lines'to'the'same'column'as'the!''''''''''''beginning'of'the'box'rather'than'2'more'columns'to'the'right!'''''cbox'''Close'the'current'box!'''''break''Insert'a'breakpoint'indicating'where'the'line'maybe'broken'if!''''''''''''necessary.!''See'the'documentation'for'the'Format'module'in'the'OCaml'library'for!''more'details.'!*)!!let'obox0()'='open_hvbox'0!let'obox()'='open_hvbox'2!let'cbox()'='close_box()!let'break()'='print_break'0'0!!let'small't'=!match't'with!TmVar(_,_,_)'-$.'true!$5'_'-$.'false!!let'rec'printkn_kind'outer'ctx'k'='match'k'with!knK'-$.'printkn_arrowkind'outer'ctx'knK!!and'printkn_arrowkind'outer'ctx'k'='match'k'with!KnArr(knK1,knK2)'-$.!obox0();!printkn_akind'false'ctx'knK1;!if'outer'then'pr'$('$(;!pr'$(=$.$(;!if'outer'then'print_space()'else'break();!printkn_arrowkind'outer'ctx'knK2;!cbox()!$5'knK'-$.'printkn_akind'outer'ctx'knK!!and'printkn_akind'outer'ctx'k'='match'k'with!KnStar'-$.'pr'$(*$(!$5'knK'-$.'pr'$(($(;'printkn_kind'outer'ctx'knK;'pr'$()$(!!let'printkn'ctx'knK'='printkn_kind'true'ctx'knK!!let'prokn'ctx'knK'=!if'knK'$-$.'KnStar'then'(pr'$(::$(;'printkn_kind'false'ctx'knK)!!let'rec'printty_Type'outer'ctx'tyT'='match'tyT'with!TyAll(tyX,tyT1,tyT2)'-$.!let'(ctx1,tyX)'='(pickfreshname'ctx'tyX)'in!obox();'pr'$(All'$(;'pr'tyX;!proty'ctx'tyT1;!pr'$(.$(;!print_space'();!printty_Type'outer'ctx1'tyT2;!cbox()!$5'TyAbs(tyX,knK1,tyT2)'-$.!let'(ctx$,,x$,)'='(pickfreshname'ctx'tyX)'in!obox();'pr'$(lambda'$(;!pr'x$,;'prokn'ctx'knK1;!pr'$(.$(;'if'outer'then'print_space()'else'break();!printty_Type'outer'ctx$,'tyT2;!cbox()!$5'tyT'-$.'printty_ArrowType'outer'ctx'tyT!!and'printty_ArrowType'outer'ctx''tyT'='match'tyT'with!TyArr(tyT1,tyT2)'-$.!obox0();!printty_AppType'false'ctx'tyT1;!if'outer'then'pr'$('$(;!pr'$(-$.$(;!if'outer'then'print_space()'else'break();!printty_ArrowType'outer'ctx'tyT2;!cbox()!$5'tyT'-$.'printty_AppType'outer'ctx'tyT!!and'proty'ctx'tyS'=!if'tyS'$-$.'TyTop'then'(pr'$($-:$(;'printty_Type'false'ctx'tyS)!!and'printty_AppType'outer'ctx'k'='match'k'with!TyApp(tyT1,tyT2)'-$.!obox0();!printty_AppType'false'ctx'tyT1;!print_space();!printty_AType'false'ctx'tyT2;!cbox()!$5'tyT'-$.'printty_AType'outer'ctx'tyT!!and'printty_AType'outer'ctx'tyT'='match'tyT'with!TyTop'-$.'pr'$(Top$(!$5'TyVar(x,n)'-$.!if'ctxlength'ctx'='n'then!pr'(index2name'dummyinfo'ctx'x)!else!pr'($($/bad'index:'$('$2'(string_of_int'x)'$2'$(/$('$2'(string_of_int'n)!$2'$('in'$4$(!$2'(List.fold_left'(fun's'(x,_)'-$.'s'$2'$('$('$2'x)'$($('ctx)!$2'$('$6$1$()!$5'tyT'-$.'pr'$(($(;'printty_Type'outer'ctx'tyT;'pr'$()$(!!let'printty'ctx'tyT'='printty_Type'true'ctx'tyT!!let'rec'printtm_Term'outer'ctx't'='match't'with!TmAbs(fi,x,tyT1,t2)'-$.!(let'(ctx$,,x$,)'='(pickfreshname'ctx'x)'in!obox();'pr'$(lambda'$(;!pr'x$,;'pr'$(:$(;'printty_Type'false'ctx'tyT1;'pr'$(.$(;!if'(small't2)'&&'not'outer'then'break()'else'print_space();!printtm_Term'outer'ctx$,'t2;!cbox())!$5'TmTAbs(fi,x,tyS,t)'-$.!(let'(ctx1,x)'='(pickfreshname'ctx'x)'in!obox();'pr'$(lambda'$(;'pr'x;!proty'ctx'tyS;!pr'$(.$(;!if'(small't)'&&'not'outer'then'break()'else'print_space();!printtm_Term'outer'ctx1't;!cbox())!$5't'-$.'printtm_AppTerm'outer'ctx't!!and'printtm_AppTerm'outer'ctx't'='match't'with!TmApp(fi,'t1,'t2)'-$.!obox0();!printtm_AppTerm'false'ctx't1;!print_space();!printtm_ATerm'false'ctx't2;!cbox()!$5'TmTApp(fi,t,tyS)'-$.!obox0();!printtm_AppTerm'false'ctx't;!print_space();!pr'$($/$(;'printty_Type'false'ctx'tyS;'pr'$($1$(;!cbox()!$5't'-$.'printtm_ATerm'outer'ctx't!!and'printtm_ATerm'outer'ctx't'='match't'with!TmVar(fi,x,n)'-$.!if'ctxlength'ctx'='n'then!pr'(index2name'fi'ctx'x)!else!pr'($($/bad'index:'$('$2'(string_of_int'x)'$2'$(/$('$2'(string_of_int'n)!$2'$('in'$4$(!$2'(List.fold_left'(fun's'(x,_)'-$.'s'$2'$('$('$2'x)'$($('ctx)!$2'$('$6$1$()!$5't'-$.'pr'$(($(;'printtm_Term'outer'ctx't;'pr'$()$(!!let'printtm'ctx't'='printtm_Term'true'ctx't!!let'prbinding'ctx'b'='match'b'with!NameBind'-$.'()!$5'VarBind(tyT)'-$.'pr'$(:'$(;'printty'ctx'tyT!$5'TyVarBind(tyS)'-$.'pr'$($-:'$(;printty_Type'false'ctx'tyS