> module Parse where > import Char(isDigit)--1.3 > import Token > import Unparse > import Build_Tm > import Build_itrm > import Core_datatype > import Type_defs > import Attributes > import Kernel > import Sub_Core1 > import Sub_Core2 > import Sub_Core3 > import Sub_Core4 > import Vtslib > type Parse_State = ( [ Tag ] , Sgn ) -- for parser without Maybe types -- simplified if Maybes pushed into parser -- push fns into parser? > parse_trm sg tgL s > = case parse_itm ( tgL , sg ) s of > ( Opnd ( Itrm itm )) -> Ok itm > Prs_Err mesg -> Bad mesg > parse_Thm_M sg ps str > = if is_valid_Thm th > then Ok th > else Bad mesg > where > th = parse_Thm sg ps str > ( TH_Err mesg ) = th > parse_Thm sg ps = parse_deriv (ps, sg) . parse_itm (ps, sg) > parse_Trm sg ps = parse_tm ( ps , sg ) > trm_to_Trm = build_trm' > dec_to_Dec = build_dc > sgn_to_Sgn = build_sg > parse_tm (tgL , sg ) str > = build_trm sg flag_itm > where > ( flag_itm , _ ) = drive_parse ( tgL , sg ) str > parse_itm sg str > = itm > where > (itm , _ ) = drive_parse sg str The driver function for the parser takes a signature and a string, returning an ITrm (with will contain the wrapper Opnd or Prs_Err depending on success) and an unused list of tokens. (In normal usage this will be empty?) The term parser is given the terminator token (Rvd "") which cannot occur naturally in the input list but is appended to the token list by the tokeniser. > drive_parse :: Parse_State -> String -> ( Flagged_ITrm , [Token] ) > drive_parse sg str > = term sg [Rvd ""] ( tokenise str ) A term is formed by folding the term constructor App into the list of individual terms produced by term'. A term is first parsed into a list by term' in order to allow for possible re-ordering of the component terms by `prioritise'. The arguments are the parse state on which parsing is to take place, a list of terminating tokens whose presence on the input list of tokens will indicate that the parse is complete and the input list of tokens itself. The result is as for `parse_tm' above. > term :: Parse_State -> [Token] -> [Token] -> (Flagged_ITrm , [Token]) > term sg tmnL tkL > = ( tm , tkL2 ) > where > tm = foldl1 app' ( prioritise tmL ) > ( tmL , tkL2 ) = term' sg tmnL tkL term' is the 'meat' of the term parser. It has a case for each alternative defined for terms is the syntax. It is defined as a case analysis taking the same arguments as its driving function `term' above. In all clauses the term generator functions ( cond' , let' etc ) pass back errors in the first argument in which one is found without forcing evaluation of the remaining arguments. This allows parsing of these remaining arguments to proceed on the assumption that their prerequisite components are valid. (see if expression below for a documented example) Also, in all cases where only a single terminator token is being sought, the element at the head of the returned list may be discarded as it must match the required token for a successful parse. ( If the parse was unsuccessful, the list will not be required anyway--functions must merely ensure that their returned list contain at least one dummy element) Again, see the if clause below for a documented example of this. NOTE: these two features are not documented in subsequent clauses where they are employed. Note also that many of the necessary attributes are added by the generator funcions (if',let' etc.) contained in the module `build_itrm'. > term' :: Parse_State -> [Token] -> [Token] -> ([Flagged_ITrm] , [Token]) if expression An if expression consists of three sub-expressions, a declaration and two terms (dc, t_tm & f_tm) representing the predicate and the cases for true and false respectively. These are parsed used `hyp', `term' and `term' respectively. Note that the hypothesis may only be terminated when the `then' is encountered and `t_tm' only when the `else' is encountered. i.e. if the original termination tokens `tmnL' are found here an error has occured. These original tokens come back into force to terminate the `else' clause. Note that the else clause extends "as far as possible" to the right. Hence the list of terms returned has only one element `cond_tm'. (The component terms t_tm and f_tm have already been made into a single ITrm rather than a list by means of the `term' function rather than `term''. Also note that since `hyp' and the t_tm must have been terminated by the single terminator token indicated, it must occur at the head of the returned list of tokens `tkL2' and `tkL3' and hence may simply be discarded. (If a parse error occured the list will not be examined further as all such errors are considered fatal. The if generator function `cond'' takes care to return a parse error of the first of its arguments which indicates one. i.e. if an error occurs during the parsing of `dc', no attempt will be made to parse `t_tm' or `f_tm'. The variable introduced in the predicate is in scope throughout the terms `t_tm' and `f_tm' hence the use of the extended signature `sg2'. (`sg2' will only be evaluated if no parse error occured during the parsing of `dc'--see paragraph above and `pst_extend' below.) > term' sg tmnL ( Rvd "if" : tkL ) > = ( [ cond_tm ] , tkL4 ) > where > cond_tm = cond' dc t_tm f_tm > ( dc , _ : tkL2 ) = hyp sg [ Rvd "then" ] tkL > ( t_tm , _ : tkL3 ) = term sg2 [ Rvd "else" ] tkL2 > ( f_tm , tkL4 ) = term sg2 tmnL tkL3 > sg2 = pst_extend dc sg let expression A let expression, similarly to `if' consists of a declaration (dc) and two terms (tm1) and (tm2) and has the semantics:- let dc = tm1 in tm2 is equivalent to ( \dc.tm2 ) tm1 Again similarly to `if', the second term (tm2) extends "as far as possible" to the right. The intermediate declaration and term (dc & tm1) are terminated by the tokens "=" & "in" as shown with the second term (and hence the entire expression) being terminated by the original termination tokens (tmnL). Note that the variable introduced in `dc' is in scope for `tm2' but not for `tm1'. The reason for this is apparent if the semantics above are examined as `tm2' is the body of the lambda abstraction. > term' sg tmnL ( Rvd "let" : tkL ) > = ( [ let' dc tm1 tm2 ] , tkL4 ) > where > ( dc , _ : tkL2 ) = abdec sg [ IfxOp "=" ] tkL > ( tm1 , _ : tkL3 ) = term sg [ Rvd "in" ] tkL2 > ( tm2 , tkL4 ) = term sg2 tmnL tkL3 > sg2 = pst_extend dc sg recurse recurse is the primitive recursion function. It consists of a series if atomic terms (tmL) defining the operations on each of the constructors of a type and an obligatory typing for the term (srt). The function `recurse_cls' deals with the details of the parsing of the component terms. The empty list indicated is an initialisation of the accumulated list of terms returned by the function. Note : recurse clause (recurse_cls) throws away separators ( no need for _:) > term' sg tmnL ( Rvd "recurse" : tkL ) > = ( [ recurse' tmL srt ] , tkL3 ) > where > ( tmL , tkL2 ) = recurse_cls sg [] tkL > ( srt , tkL3 ) = term sg tmnL tkL2 fn > {- > term' sg tmnl ( Rvd "fn" : tkl ) > = case tkl? of > Rvd "|" : tkl?' -> > -} subscripted application All applications are treated as a dummy operator ( Spl "" ). A subscripted application is treated as a BinR operator of precedence 100. (Normal application is left associative (BinL)). The function being applied will have already been parsed prior to encountering the open subscript character. The argument (argtm) follows immediately and is terminated by the close subscript character Unlike `if' and `let' expressions, the subscripted application may be followed by further terms taking their place in the term list produced by term' (tmL). They are placed in the list after `argtm'. The prioritise function will rearrange them into their correct positions in the expression. `argtm' itself is already folded into a single expression by use of the `term' function rather than `term''. Note that the only valid terminator during the parsing of this term is the close subscript character. (185 = open subscript , 176 = close subscript ) > term' sg tmnL ( Rvd "\185" : tkL ) > = ( app_op : argtm : tmL , tkL3 ) > where > ( argtm , _ : tkL2 ) = term sg [ Rvd "\176" ] tkL > ( tmL , tkL3 ) = term' sg tmnL tkL2 > app_op = Opr ( Spl "" ) BinR 100 prefix binders Prefix binders will already have been identified by the tokeniser. They all follow the same pattern, a declaration (dc) followed by a "." and a body (tm). Similarly to 'if' and 'let', the body of the term extends as far to the right as possible, hence `bdr_tm' forms a single element list. The function `binder'' maps the binder name (nm) into the correct binder. Note that the declaration is in scope within the body of the binder expression (tm). > term' sg tmnL ( Bdr nm : tkL ) > = ( [ bdr_tm ] , tkL3 ) > where > bdr_tm = binder' nm dc tm > ( dc , _ : tkL2 ) = bdec sg [ Rvd "." ] tkL > ( tm , tkL3 ) = term sg2 tmnL tkL2 > sg2 = pst_extend dc sg pairs A pair consists of two terms separated by "," character. A pair is treated as a special operator (Spl ",") which actually forms the pair when it is expanded by `app'' ( see module build_itrm). The pair is optionally followed by a `typed' expression, hence the keyword `typed' is added to the list of termination tokens for the second argument (as for subscripted application, the first argument will have already been parsed prior to encountering the ","). The "typed" term itself (if present) will be dealt with by a separate clause. Note that the second argument is left as an unfolded list (term' used) to allow for expressions of higher precedence than pair. It also extends as far to the right as possible. > term' sg tmnL ( Rvd "," : tkL ) > = ( pair_op : argtmL , tkL2 ) > where > ( argtmL, tkL2 ) = term' sg ( Rvd "typed" : tmnL ) tkL > pair_op = Opr ( Spl "," ) BinR 20 The 'typed' extension (of pairs etc.) is, similarly to pairs, treated as a special operator ( Spl "typed" ). Its argument is a single term and extends as far to the right as possible. As for pairs, the first argument to "typed" will already have been parsed prior to encountering the "typed". > term' sg tmnL ( Rvd "typed" : tkL ) > = ( [ tpe_op , tpe ] , tkL2 ) > where > ( tpe , tkL2 ) = term sg tmnL tkL > tpe_op = Opr ( Spl "typed" ) BinL 1 symbols Explicit reference to symbols may be pattern matched directly off the token list. The function 'sym'' ensures that the arguments `no1' and `no2' are valid integers. The symbol so formed is added to the term list together with the parsed remainder of the input (tmL). (168 = open < , 169 = close > ) > term' sg tmnL ( Rvd "\168": Clr no1 : Rvd ",": Clr no2 : Rvd "\169": tkL ) > = ( sym' no1 no2 : tmL , tkL2 ) > where > ( tmL , tkL2 ) = term' sg tmnL tkL constructors Explicit reference to constructors are handled analogously to symbols described above. (168 = open < , 169 = close > ) > term' sg tmnL ( Rvd "\168" : Clr no1 : Rvd "," : Clr no2 : Rvd "," : > Clr no3 : Rvd "\169" : tkL ) > = ( const' no1 no2 no3 : tmL , tkL2 ) > where > ( tmL , tkL2 ) = term' sg tmnL tkL subtypes Subtypes consist of a declaration followed by a term in curly braces. i.e. { dc | tm }. The declaration is in scope in the term (tm,sg2). Since the subtype only extends as far as the `}' character, `term' must continue to parse the remainder of the term (tmL). Subtypes are treated as binders (binder') similarly to prefix binders. > term' sg tmnL ( Rvd "{" : tkL ) > = ( binder' Subtype dc tm : tmL , tkL4 ) > where > ( dc , _ : tkL2 ) = bdec sg [ Rvd "|" ] tkL > ( tm , _ : tkL3 ) = term sg2 [ Rvd "}" ] tkL2 > ( tmL , tkL4 ) = term' sg tmnL tkL3 > sg2 = pst_extend dc sg declarations in '['']' Declarations in square brackets will occur in the input stream before the object to which they refer (infix binders). The declaration is parsed and added to the list of "terms" produced as output. (Use of the type Flagged_ITrm allows declarations to be included as well as terms. If no errors are present, they will be removed when the function `app'' is folded into the list.) Special operators (for infix binders) will allow for declarations occuring as their first argument. Note that the remainder of the list of terms being generated (tmL) is parsed on the extended signature (sg2). > term' sg tmnL ( Rvd "[" : tkL ) > = ( dc : tmL , tkL3 ) > where > ( dc , _ : tkL2 ) = bdec sg [ Rvd "]" ] tkL > ( tmL , tkL3 ) = term' sg2 tmnL tkL2 > sg2 = pst_extend dc sg infix binders Infix binders are mapped into operators by the function `make_prebdr' and then added to the result list of terms (bdrop). (The operator contains the corresponding prefix binder constructor (Lambda etc.), associativity and precedence of the binder.) The operator and its arguments will be mapped into a binder ITrm construction when the function `app'' (defined in module build_itrm) is folded into the list of terms produced as a result of this function. The first agument (which may be a declaration or a term) will have already been parsed. (the function app' deals with the two cases of term or dec.) The second argument will be contained in the list `tmL'.) > term' sg tmnL ( IfxBdr bdr : tkL ) > = ( bdrop : tmL , tkL2 ) > where > bdrop = make_prebdr bdr > ( tmL , tkL2 ) = term' sg tmnL tkL infix operators ( And Or etc ) The handling of infix operators is analogous to the handling of infix binders above. The function `make_iop' generates an operator (iop) which will be mapped into an ITrm operator construction by the function `app''. In this case however, the first argument must be a term. (This is enforced by `app''.) > term' sg tmnL ( IfxOp op : tkL ) > = ( iop : tmL , tkL2 ) > where > iop = make_iop op > ( tmL , tkL2 ) = term' sg tmnL tkL prefix (not) operator The prefix operator, not, is treated analogously to the infix operators described above. Since only one such operator is present, the operator representing it is explicitely generated here (not_op). Not's single argument will be contained in the list `tmL'. No argument will have been parsed previously as it is a prefix operator. > term' sg tmnL ( Rvd "\181" : tkL ) > = ( not_op : tmL , tkL2 ) > where > not_op = Opr ( Spl "Not" ) Pre 60 > ( tmL , tkL2 ) = term' sg tmnL tkL parenthesised term A parenthesised term is dealt with simple by calling the function `term' to parse upto the closing `)'. The function `term' folds its result into a single term, hence `tm' may be added as a single entity into the function result list achieving the desired result of binding the entities within the parentheses into a single term. Note that the closing `)' is the only valid terminator here. If one of the terminators in `tmnL' occurs before the closing `)', an error has occured. > term' sg tmnL ( Rvd "(" : tkL ) > = ( tm : tmL , tkL3 ) > where > ( tm , _ : tkL2 ) = term sg [ Rvd ")" ] tkL > ( tmL , tkL3 ) = term' sg tmnL tkL2 \@ is not implemented yet. > term' sg tmnL ( Rvd "@" : tkL ) > = ( [ Prs_Err "@ not implemented " ] , dmy ) universes Any identifier beginning with a `U' and continuing with non-empty list of integers (arg) represents a universe (the pattern checks for this). If so, the universe ITrm may be build directly using the `read' function to convert the argument into the desired integer (i). Note that negative universes cannot occur as they require the character `-' which is not a digit. > term' sg tmnL ( Clr ( 'U' : arg@(_:_) ) : tkL ) | and ( map isDigit arg ) > = ( universe : tmL , tkL2 ) > where > universe = ( Opnd . Itrm ) ( Constant ( Univ i ) [] [] ) > i = read arg > ( tmL , tkL2 ) = term' sg tmnL tkL constant symbols The constant symbols `true', `false' and `bool' may be mapped directly into their ITrm constant representations. As for Universes, the remainder or the input (tkL) is parsed for the remainder of the result list of terms (tmL). > term' sg tmnL ( Clr nm : tkL ) | nm == "true" || nm == "false" || nm == "bool" > = ( cst : tmL , tkL2 ) > where > cst = ( Opnd . Itrm ) ( Constant ( ctr nm ) [] [] ) > ctr "true" = T > ctr "false" = F > ctr "bool" = Bool' > ( tmL , tkL2 ) = term' sg tmnL tkL tags > term' pst@( tgL , sg ) tmnL ( Clr nm : tkL ) > = if in_tgL then ( tag' tg argL : tmL2 , tkL3 ) > else ( sym_id : tmL1 , tkL2' ) > where > sym_id = lookUp nm sg > ( tmL1 , tkL2' ) = term' pst tmnL tkL > ( tmL2 , tkL3 ) = term' pst tmnL tkL2 > ( in_tgL , tg@( _ , arg_kndL , _ )) = fetch_tg nm tgL > ( argL , tkL2 ) = parse_tag_arg [] arg_kndL tkL > parse_tag_arg tg_resL ( knd : kndL ) lcl_tkL > = parse_tag_arg ( tg_res : tg_resL ) kndL lcl_tkL3 > where > ( tg_res , lcl_tkL3 ) > = case knd of > Term_Arg -> ( Tg_Trm trm_res , lcl_tkL2 ) > Deriv_Arg -> ( Tg_Thm thm_res , lcl_tkL2 ) > Int_Arg -> parse_iL lcl_tkL > trm_res = build_trm sg res_tm > thm_res = parse_deriv pst res_tm > ( res_tm , lcl_tkL2 ) = aterm pst [] lcl_tkL > parse_tag_arg tg_resL [] lcl_tkL > = ( reverse tg_resL , lcl_tkL ) symbol names Any identifier which has not been trapped by the above two clauses is assumed to represent an entry on the signature (sg). The function `lookup' is used to retrieve the entry. It returns the necessary Flagged_ITrm for the symbol if it is present on the signature (sym_id) or alternatively a parse error if it is not found. > {- > term' pst@( _ , sg) tmnL ( Clr nm : tkL ) > = ( sym_id : tmL , tkL2 ) -- also checks tag list > where > sym_id = lookup nm sg > ( tmL , tkL2 ) = term' pst tmnL tkL > -} last clauses - termination and error conditions check for terminator token If the next token is in the termination list (tmnL), then the parse is complete and the empty list of terms is returned. The input token list (tkL) is returned unchanged. > term' sg tmnL tkL@( tk : _ ) | tk `elem` tmnL > = ( [] , tkL ) Any reserved word which has not been already dealt with and was not in the termination list (tmnL), is unexpected and an error. (The termination list was checked in the above clause.) > term' sg tmnl ( Rvd str : tkl ) >-- = ( [ Prs_Err (" unexpected '" ++ str ++ "' (term)") ], dmy ) > = ( [ Prs_Err (" unexpected '" ++ str ++ "'"++ " (term) tmnl: " ++ concat ( map disp_tk tmnl )++ "|") ], dmy ) If the input stream is empty then cease parsing (enhance later) > term' sg tmnl [] | Rvd "" `elem` tmnl > = ( [] , [] ) > term' sg tmnl [] > = ( [] , [] ) > {- end of file with tmnl not empty is not necessarily an error e.g. ';' in sig > = ( [ Prs_Err mesg ] , dmy ) > where > mesg = " expecting '" ++ concat ( map disp_tk tmnl ) ++ "'" > -} pass on tokeniser error unchanged as a parse error. No attempt is made to parse the remainder of the input. (`dmy' is a single element dummy token list returned to ensure that pattern matches on non-empty token lists do not fail even if a parse error has occured.) > term' sg _ ( Scan_Err mesg : _ ) > = ( [ Prs_Err mesg ] , dmy ) aterm -- added for sig , merge with term'? aterm and the corresponding clauses in term' are to be merged. (documentation on the clauses is given in term' above.) symbols (168 = open < , 169 = close > ) > aterm sg tmnl ( Rvd "\168": Clr no1 : Rvd ",": Clr no2 : Rvd "\169": tkl ) > = ( sym' no1 no2 , tkl ) constructors (168 = open < , 169 = close > ) > aterm sg tmnl ( Rvd "\168" : Clr no1 : Rvd "," : Clr no2 : Rvd "," : > Clr no3 : Rvd "\169" : tkl ) > = ( const' no1 no2 no3 , tkl ) subtypes > aterm sg tmnl ( Rvd "{" : tkl ) > = ( binder' Subtype dc tm , tkl3 ) > where > ( dc , _ : tkl2 ) = bdec sg [ Rvd "|" ] tkl > ( tm , tkl3 ) = term sg2 [ Rvd "}" ] tkl2 > sg2 = pst_extend dc sg universes (Note : ensure argument is non-empty list of digits) > aterm sg tmnl ( Clr ( 'U' : arg@(_:_) ) : tkl ) | and ( map isDigit arg ) > = ( universe , tkl ) > where > universe = ( Opnd . Itrm ) ( Constant ( Univ i ) [] [] ) > i = read arg constant symbols > aterm sg tmnl ( Clr nm : tkl ) | nm == "true" || nm == "false" || nm == "bool" > = ( cst , tkl ) > where > cst = ( Opnd . Itrm ) ( Constant ( ctr nm ) [] [] ) > ctr "true" = T > ctr "false" = F > ctr "bool" = Bool' parenthesised term > aterm sg tmnl ( Rvd "(" : tkl ) > = ( tm , tkl2 ) > where > ( tm , _ : tkl2 ) = term sg [ Rvd ")" ] tkl symbol names > aterm ( _ , sg ) tmnl ( Clr nm : tkl ) > = ( sym_id , tkl ) -- also checks tag list > where > sym_id = lookUp nm sg > aterm sg tmnl ( tk : tkl ) > = ( Prs_Err (" unexpected '" ++ disp_tk tk ++ "' (aterm -- no tmnl check)" ) , dmy ) end aterm `hyp' generates a declaration from the list contained between `[' and `]' or alternatively an anonymous declaration if no square brackets are present. If a declaration (btm) is contained within `[' and `]' then a valid terminator token should immediately follow it (head of `tkL2'). An error also occurs if `tkL2' is empty. The case analysis checks for these conditions. {- Is this clause necessary since term' can catch [] on its own? (Or optimise just to include a check for term' returning dc or tm and take appropriate action. note if dec in [ ] then a terminator must immediately follow the ']' -} > hyp :: Parse_State -> [Token] -> [Token] -> ( Flagged_ITrm , [Token] ) > hyp sg tmnL ( Rvd "[" : tkL ) > = case tkL2 of > nxt : _ | nxt `elem` tmnL > -> ( btm , tkL2 ) > nxt : _ -> ( Prs_Err mesg1 , dmy ) > where > mesg1 = "Unexpected token '"++ disp_tk nxt ++"'" > _ -> ( Prs_Err mesg2 , dmy ) > where > ( btm , _ : tkL2 ) = bdec sg [ Rvd "]" ] tkL > mesg2 = "Unexpected end of file" If no square brackets are found then an anonymous declaration is generated. The input stream (tkL) is parsed as a term which is taken as the sort of the anonymous declaration. The name of the declaration is defined to be "_" and the attribute `hyp_ndpnd' is added to the attribute list to show that it is anonymous. > hyp sg tmnL tkL > = ( anon_dc , tkL2 ) > where > anon_dc = symbol_dec' tm ( Name "_" ) [ hyp_ndpnd ] > ( tm , tkL2 ) = term sg tmnL tkL binding declarations This is the driver function for the declaration parser. It uses the function `bdec'' to generate a declaration (nxt_dc) and then checks the remaining input stream (tkL2) for further declarations. If there are further declarations (`;' is at the head of the list), `bdec' itself is used to generate them (rest) on a signature extended with the first declaration (sg2). (Using `bdec' rather than `bdec'' here allows for further `;' characters after the next declaration.) The component declarations are joined together using `decpair''. The attribute `un_grp' is added to indicate that the declarations were ungrouped. (Grouped declarations are dealt with by `bdec_name' below.) Note that since `decpair'' applies a single declaration (nxt_dc) to the already paired declarations (rest) (paired by the recursive call to `bdec'), `;' is right associative. Note also that a valid terminator token should occur at the head of the remaining input (tkL2) for a correct termination. (This is a design decision to charge `bdec' with ensuring that the valid terminator occurs after the declarations. The alternative would involve placing a check for terminator after each call to `bdec'.) Note that the terminator token is still passed back at the head of the remaining input (tkL2). > bdec :: Parse_State -> [Token] -> [Token] -> ( Flagged_ITrm , [Token] ) > bdec sg tmnL tkL > = case tkL2 of > Rvd ";" : tkL2' > -> ( decpair' [un_grp] nxt_dc rest , tkL3 ) > where > ( rest , tkL3 ) = bdec sg2 tmnL tkL2' > tk : _ | tk `elem` tmnL > -> ( nxt_dc , tkL2 ) >-- oth -> ( Prs_Err "Malformed declaration" , dmy ) > oth -> error ( "Bdec: " ++ concat ( map disp_tk oth ) ++ "\ntmnl: " ++ concat ( map disp_tk tmnL ) ++ "|" ) > where > ( nxt_dc , tkL2 ) = bdec' sg tmnL tkL > sg2 = pst_extend nxt_dc sg bdec' performs a check for parentheses in a declaration. If they are present, it uses the function `bdec' to generate a single declaration from the tokens contained within the parentheses. If they are not, the function `bdec_name' is used to generate a grouped set of declarations. The empty list represents the initialisation of the accumulated list of declarations within the group generated by `bdec_name'. > bdec' :: Parse_State -> [Token] -> [Token] -> ( Flagged_ITrm , [Token] ) > bdec' sg tmnL ( Rvd "(" : tkL ) > = ( nxt_dc , tkL2 ) > where > ( nxt_dc , _ : tkL2 ) = bdec sg [ Rvd ")" ] tkL > bdec' sg tmnL tkL > = bdec_name sg ( Rvd ";" : tmnL ) [] tkL `bdec_name' generates a grouped set of declarations (separated by ','). Firstly a name is generated from the input stream (nm). If the name is valid (case nm), a case analysis is performed on the following token (head of tkL2). If a ',' is found, another element in the group follows. In this case, `bdec_name' is called recusively with the current name (nm) being added to the accumulated list of group names (nmL). If ':' is found, a term representing the sort of each element in the group follows. This is parsed by `term'. The function `make_dc' is then used to assign this sort to each name in the accumulated name list (nmL). Since only one sort declaration can occur per group, parsing of the group list is now complete. The attribute `dec_tpe' is added to indicate that a sort was explicitely given for the group. A group will also terminate if any token other than ',' or ':' is encountered. In this case a default sort (currently temporrarily set to U0 (dft), is assigned to each name in the group. The function `make_dc' is again used for this purpose. The attribute `dec_untpe' is added to indicate that no explicit sort was given for the group. > bdec_name :: Parse_State -> [Token] -> [Name'] -> [Token] > -> (Flagged_ITrm , [Token]) > bdec_name sg tmnL nmL tkL > = case nm of > Ok inm -> switch inm tkL2 > Bad mesg -> ( Prs_Err mesg , dmy ) > where > ( nm , tkL2 ) = name tkL > switch inm ( Rvd "," : tkL2' ) = bdec_name sg tmnL ( inm : nmL ) tkL2' > switch inm ( IfxOp ":" : tkL2' ) > = ( make_dc ( reverse ( inm : nmL )) srt dec_tpe , tkL3 ) > where > ( srt , tkL3 ) = term sg ( Rvd ";" : tmnL ) tkL2' > switch inm tkL > = ( make_dc ( reverse ( inm : nmL )) dft dec_untpe , tkL ) > dft = Opnd ( Itrm ( Constant ( Univ 0 ) [] [] )) --temporary default `make_dc' is an auxiliary function to `bdec_name' defined above. Its function is to take a list of names and a sort and generate a single paired declaration containing all the given names assigned with the given sort. It also adds the supplied attribute to each individual declaration (tped). `make_dcL' assigns the given sort to each name in nmL producing a list of declaration (dcL). The function `decpair'' is then folded into this list to produce a single declaration. The attribute `grp' is added to each paired declaration indicating that it is part of a group. (Note that attributes indicating grouped/ungrouped are added to each decpair declaration while attributes indicating typed/untyped are added to the component symbol declarations.) > make_dc :: [Name'] -> Flagged_ITrm -> Attribute -> Flagged_ITrm > make_dc nmL ( Opnd ( Itrm srt )) tped > = case dcL of > [] -> Prs_Err "empty declaration" > _ -> foldr1 ( decpair' [grp] ) dcL > where > dcL = make_dcL 0 nmL > make_dcL cnt ( nm : nmL ) > = dc : ( make_dcL ( cnt + 1 ) nmL ) > where > dc = Opnd ( Idec ( Symbol_dec shft_srt [ sym_nm nm , tped ])) > shft_srt = shift_trm [] cnt srt > make_dcL _ [] = [] > make_dc nmL ( Prs_Err mesg ) _ > = Prs_Err mesg > make_dc nmL _ _ = error "unexpected term in make_dc" Atomic binding declarations consist of either a binding declaration enclosed in `(' `)' or an untyped, single named declaration. If a `(' token appears at the head of the list, the function `bdec' may be used to build a declaration from the contents of the parentheses. If not, a `name' is generated from the input list (2nd clause tkL). A declaration is then build from this name using a default sort (dft) (currently temporarily set to U0.) If a parse error occured during the name parse, the error is passed back unchanged (case nm). > abdec :: Parse_State -> [Token] -> [Token] -> ( Flagged_ITrm , [Token] ) > abdec sg tmnL ( Rvd "(" : tkL ) > = ( nxt_dc , tkL2 ) > where > ( nxt_dc , _ : tkL2 ) = bdec sg [ Rvd ")" ] tkL > abdec sg tmnL tkL > = case nm of > Ok inm -> ( symbol_dec' dft inm [] , tkL2 ) > Bad mesg -> ( Prs_Err mesg , dmy ) > where > ( nm , tkL2 ) = name tkL > dft = Opnd ( Itrm ( Constant ( Univ 0 ) [] [] )) --temporary default Names consist of a single string identifier or an operator declaration contained in `{' `}'. >-- name :: [Token] -> ( MayBe Name' , [Token] ) If a `{' character is found, the identifier of the operator will be next on the list (id). The functions `optyp' and `opprc' are then used to find the type (in the sense of prefix, postfix etc.) and precedence of the operator respectively. They will return defaults if no explicit values are found. The token `}' should occur at the head of the list returned by the precedence parser `opprc' (tkl3). If this is not found an error is returned. > name ( Rvd "{" : Clr id : tkL ) > = case tkL3 of > Rvd "}" : tkL3' -> ( Ok ( Operator' id prc optype ) , tkL3' ) > _ -> ( Bad "missing '}'" , dmy ) > where > ( optype , tkL2 ) = optyp tkL > ( prc , tkL3 ) = opprc tkL2 If no '{' is found, the single identifer (id) represents the name of the object. i.e. the name is a string identifier. The name cannot be a reserved word (must be `Clr' token constructor.) If a reserved word is found (oth in following cluase) an error message is generated. An error message is also generated if the input list is empty. > name ( Clr id : tkL ) > = ( Ok ( Name id ) , tkL ) > name ( oth : tkL ) > = ( Bad ( " unexpected '" ++ disp_tk oth ++ "' (name)" ) , dmy ) > name [] = ( Bad "empty identifier" , dmy ) `optyp' returns the type of an operator (in the sense of prefix, postfix etc.) The function merely maps the string representing the type into its corresponding constructor of type `Oprtype'). If the token does not match one of the four types of operators, a default of binary left associative (BinL) is returned (final clause). Note here that the input token list (tkL) is returned unchanged as it will be required by the precedence parser `opprc'. (Since neither the type or precedence is compulsory, no input should be `eaten' if no matching token is found.) > optyp :: [Token] -> ( Oprtype , [Token] ) > optyp ( Rvd "Pre" : tkL ) > = ( Pre , tkL ) > optyp ( Rvd "BinL" : tkL ) > = ( BinL , tkL ) > optyp ( Rvd "BinR" : tkL ) > = ( BinR , tkL ) > optyp ( Rvd "Post" : tkL ) > = ( Post , tkL ) default BinL > optyp tkL > = ( BinL , tkL ) `opprc' returns the precedence of an operator. If the token at the head of the input list is a string of digits, the string is converted to an integer by `read' and returned. Otherwise a default precedence (currently 1) is returned. The input list is returned unchanged in this case. > opprc :: [Token] -> ( Int , [Token] ) > opprc ( Clr prcid : tkL ) | and ( map isDigit prcid ) > = ( read prcid , tkL ) > opprc tkL > = ( 1 , tkL ) recurse fns This is an auxiliary function dealing with the Recurse expression. The function accumulates atomic terms (fnL) representing the cases of a Recurse expression until the keywords `end' followed by `typed' are found. (recurse must be typed) The argument to the keyword `typed' is dealt with by the calling function (a clause of term') as is the generation of the recurse expression itself. > recurse_cls :: Parse_State -> [Flagged_ITrm] -> [Token] -> ( [Flagged_ITrm] , [Token]) > recurse_cls sg fnL tkL > = case tkL2 of > Rvd "end" : Rvd "typed" : tkL2' > -> ( fn : fnL , tkL2' ) > Rvd "end" : _ > -> ( [ Prs_Err " recurse must be typed " ] , dmy ) > _ -> recurse_cls sg ( fn : fnL ) tkL2 > where > ( fn , tkL2 ) = aterm sg [ Rvd "end" ] tkL fn clauses -- incomplete > {- > fn_clauses > = case ident_type tkL of > Ok ( i , j , k ) > -> match ctrL nmL ( i , j ) tkL > where > ( Data _ ctrL [ dat_nm nmL ] ) > = fetch_type sg i j > Bad mesg -> ( Prs_Err mesg , dmy ) > match sg ctrL ( tpe_nm : nmL ) tp_id tkl > = ( recurse' fnL srt , tkl2 ) > where > ( fnL , tkl2 ) = match_cls > match_cls ctr_argL nm > = case tkl2 of > Rvd "\167" : tkl2' -> make_rhs > otherwise -> error "" > where > ( ( nm , fmls ) , tkl2 ) = parg sg nm tmnl abdec True tkl > sg2 = extend' sg ( fmls ++ rcL ) > rcL = find_recursive ctr_argL tp_id fmls > make_rhs > = case tkl2 of > Rvd "|" : tkl2' -> match_cls > tk : _ | tk `elem` tmnl -> ( clsL , tkl2 ) > where > tm = add_lambda > ( rhs , tkl2 ) = term sg2 tmnl tkl2' > find_recursive ( arg : argL ) tp_id > ident_type sg ( Clr nm : tkl ) > = case lookUp nm sg of > ( True , Const i j k _ _ ) -> Ok ( i , j , k ) > otherwise -> ident_type sg tkl > ident_type sg ( Rvd "\167" : _ ) > = Bad "No constructor before '\167'" > ident_type sg ( Rvd tk : _ ) > = Bad " Unexpected '" ++ disp_tk tk ++ "'" > -} --END FN-- Prioritise The prioritiser rearranges the list of terms produced by `term'' into their correct precedence order before the `app'' function is folded into resulting list. The following driver function initialises the `stacks' for the main prioritisor function `ptse' and checks that the resulting list is non-empty. > prioritise :: [Flagged_ITrm] -> [Flagged_ITrm] > prioritise tmL = case ptse [] [] False tmL of > [] -> [ Prs_Err "Empty term" ] > oth -> oth The precedence algorithm is described in the clauses of the function which follows. The algorithm uses two list, an operand list (opnds) on which the final, reordered term list will emerge, and an operator stack (oprs), which is used as a temporary store for operators while they are being reordered. The constructor at the head of each Flagged_ITrm indicates whether its component ITrm is an operator or an operand. The final list of terms is in prefix form (function before arguments) thus allowing the `app'' function to be folded into the list to produce a single term. > type Flag_I = Flagged_ITrm -- shorthand > ptse :: [Flag_I] -> [Flag_I] -> Bool -> [Flag_I] -> [Flag_I] If a component of the term list contains an error, the error is passed back without examining the remaining terms (opL) (which in normal circumstances will be empty anyway). > ptse opnds oprs _ ( Prs_Err tm : opL ) > = [ Prs_Err tm ] The boolean flag (third argument to `ptse') is used to indicate that the previous term was another operand. If this case a dummy operator for application is inserted between the two operands. This allows function application to be treated as any other operator and allows operators of higher precedence than application to be included. If an operand is encountered with the flag False (previous term was not an operand) the operand is merely pushed onto the operand list and `ptse' called on the next remaining term list (opL). The flag is now set to True to indicate the presence of an operand. > ptse opnds oprs False ( Opnd tm : opL ) > = ptse ( Opnd tm : opnds ) oprs True opL If an operand is encountered and the flag is True, (previous term was an operand), the dummy operator (app_op) is added to the current list of terms (opL) and `ptse' reinvoked to deal with the new operator. Note: the operand is left on the term list (opL) to be reexamined after the dummy operator has been dealt with. It is not immediately added to the operand list. This is because the dummy operator for application is treated as a binary infix operator and hence is expected to occur between its two operands. > ptse opnds oprs True opL@( Opnd _ : _ ) > = ptse opnds oprs True ( app_op : opL ) > where > app_op = Opr ( Spl "" ) BinL 100 The following clauses deal with the different kinds of operators. Note that operators are placed on the operand list (in a way dependent on its lind) as well as the operator stack. (Operand list is therefore a slight misnomer and is really a resulting list of terms.) prefix operators (op) are always added to the operator stack irregardless of the precedence of the operator on top of the stack. Its precedence only takes note of operators to its right in the original expression. (e.g. the `not' in `not x' will be expected to bind with `x' irregardless of the precedence of the operator preceding `not'). The operator may be added to the operand list directly as it is already in prefix form (its argument follows it in the original expression). > ptse opnds oprs _ ( op@( Opr _ Pre prc ) : opL ) > = ptse ( op : opnds ) ( op : oprs ) False opL For infix operators, one argument preceeds the operator. The `swap_op' function is thus required to place the operator before its first argument (which will be at the head of the argument list) in the operand list. The operator will precede its second argument. No further reordering is thus necessary for this argument. Before this however, all operators of higher precedence that the operator are popped for the operator stack and added to the operand list (flush). (the function `flush' also allows for an extra test as well as higher precedence to be used to determine if an operator is to be popped. This is not necessary here so `null_op' is employed.) The new operator (op) may now be added to the operator stack (oprs). > ptse opnds oprs _ ( op@( Opr _ BinL prc ) : opL ) > = ptse ( swap_op op opnds' ) ( op : oprs' ) False opL > where > ( opnds' , oprs' ) = flush opnds oprs prc null_op Right associative infix operators are identical to left associative infix operators except that another test is necessary to determine if the operator at the head of the operator stack (oprs) should be popped before the current operator (op) is added to it. The operator at the head of `oprs' should also be popped if it is also right associative and its precedence is LESS than or equal to the precedence of the current operator (right associative operator precedences work "backwards"). The function `cmp_op' defines the test. > ptse opnds oprs _ ( op@( Opr op_nm BinR prc ) : opL ) > = ptse ( swap_op op opnds' ) ( op : oprs' ) False opL > where > ( opnds' , oprs' ) = flush opnds oprs prc cmp_op > cmp_op ( Opr _ BinR prc' ) = prc' <= prc > cmp_op _ = False The argument to a postfix operator precedes it in the original expression. The `swap_op' function is hence required to transpose them in the resulting list. Again, the operator stack is `flushed' of higher precence operators first. The operator is not added to the operator stack however as (conversely to prefix operators above) its precedence only affects operators to its left. (The "'" in "a'" should also bind to "a" even if a higher precedence operator occurs to the right of the "'".) Also for this reason, the flag (fl) indicating juxtaposition of operands is not reset to False. A dummy application operator needs to be generated for two operands separated by one or more postfix operators operators. > ptse opnds oprs fl ( op@( Opr _ Post prc ) : opL ) >-- = ptse ( swap_op op opnds' ) ( op : oprs' ) False opL > = ptse ( swap_op op opnds' ) oprs' fl opL > where > ( opnds' , oprs' ) = flush opnds oprs prc null_op When all the terms have been considered, the operator stack should be `flushed' of all remaining operators. The operand list will now represent the correctly reordered term list. > ptse opnds oprs _ [] > = opnds' > where > ( opnds' , _ ) = flush opnds oprs (-1) null_op Dummy comparison operator for use with `flush' function when no further comparison is required. > null_op :: a -> Bool > null_op _ = False `swap_op' addes the given operator (op) prior to the head item on the operand list. It also forms an application of the two terms to ensure that any future `swap_op' operations take the two terms as a single term. e.g in 3 / 4 + 5, the + should be placed before the application of / to 3 (and also 4) not only the 3 itself which would be the case if the / was not bound to the 3 as soon as the `swap' takes place. This results in + ( / 3 4 ) 5 not (/ + 3 4 5 ) which is incorrect. > swap_op :: Flagged_ITrm -> [Flagged_ITrm] -> [Flagged_ITrm] > swap_op op ( top_op : opnds ) > = app' op top_op : opnds > swap_op op [] = [ op ] Clear the operator stack of operators of higher precedence than the precedence of the current operator (pprc) plus any operators meeting the additional properties of the predicate `cmp' (in practice, this applies only to right associative infix operators---see above). If the operator at the head of the operator stack is of higher precedence, the function `add_op' is applied to the operand list to perform any term binding and operand swapping required (see `add_op' below). `flush' is then called recursively on the tail of the operand stack (opL). The operand list (opnds) and operator stack (oprs) are returned unchanged when an operator of lower precedence is encountered or the operator stack is empty (2nd clause) (the calling function is responsible for adding the new operator onto the operator stack). > flush :: [Flagged_ITrm] -> [Flagged_ITrm] -> Int > -> ( Flagged_ITrm -> Bool ) -> ( [Flagged_ITrm] , [Flagged_ITrm] ) > flush opnds oprs@( op@(Opr op_nm op_tpe prc) : opL ) pprc cmp > = if pprc > prc || cmp op > then ( opnds , oprs ) > else flush opnds' opL pprc cmp > where > opnds' = add_op op_nm op_tpe opnds > flush opnds [] _ _ = ( opnds , [] ) `add_op' is called by 'flush' when an operator is flushed from the operator stack. The operator itself will already be on the operand list (`ptse' adds all operators to the operand list---see above) hence all that is required is to bind the operator to an argument. `add_op' binds a function to an argument which occurs after it in the original expression. The function 'swap_op' will have already been used to bind it to an argument which precedes it in the original expression. (An example is given in `swap_op' showing why `app'' is used to bind the function and argument pair at this stage. It is to prevent future swapping operation `getting between them' in the operand list as it has now been established that the two elements on the top of the operand list should be applied to each other. It is the result of this application which will be the argument to a further function, not the components themselves.) Prefix and infix operators all have arguments following them in the original expression and hence the `app'' function is applied to the two elements on the top of the list in these cases ( arg & fn ). The resulting application is added back to the head of the operand list. Note that postfix operators have no argument following them in the original expression and hence the operand list is returned unchanged in this case. (Compare this with `ptse' above where `swap_op' is applied in all but the prefix case to form the bond between an operator and an argument which occurs before it in the original expression. Infix operators have an argument occuring before and after them in the original expression and hence `swap_op' and `app_op' will be applied at the appreopriate time (by `ptse' and `flush')). Note that if the operand list does not contain two elements an error has occured. Also note that for infix operators, the term `fn' will consist of the application of the relevant operator applied to its first argument rather than the operator itself. (The first argument (op) is used only in the generation of the error message by the final clause.) > add_op :: Operator -> Oprtype -> [Flagged_ITrm] -> [Flagged_ITrm] > add_op op Pre ( arg : fn : opnds ) > = app' fn arg : opnds > add_op op BinL ( arg : fn : opnds ) > = app' fn arg : opnds > add_op op BinR ( arg : fn : opnds ) > = app' fn arg : opnds postfix operator has already been applied to operand (as have BinL and BinR to their first operand ) > add_op op Post opnds > = opnds > add_op op _ _ > = [ Prs_Err ( " Insufficient arguments for operator" ) ] -- ++ op ) ] end prioritise infix binders The following function assigns the ITrm binder constructor and precedence of an infix binder. (All infix binders are infix right associative.) An operator is returned representing the binder. (This allows it to be reordered by `prioritise' into its correct place in the resulting ITrm.) The special operator `OpBdr' is used to represent infix beinders. These will be expanded by `app'' later to form an ITrm when the arguments to the binder are known. > make_prebdr :: String -> Flagged_ITrm > make_prebdr bdr > = Opr ( OpBdr prefix_form ) BinR prc > where > ( prefix_form , prc ) = map_bdr bdr > map_bdr "\167" = ( Lambda , 5 ) > map_bdr "\183" = ( Pi , 80 ) > map_bdr "\184" = ( Sigma , 90 ) > map_bdr "\182" = ( Imp , 20 ) > map_bdr "\187" = ( Delta , 10 ) infix operators This function is analogous to `make_prebdr' above except it returns an operator representing infix operators with their respective precedences. The special operator `OpIfx' is used for infix operators. ":" is a special case (assigning type of first operand to the second) treated as shown. (app' appies a separate partial op for ":" as it does not map into a Binary_conn in the resultant itrm.) > make_iop :: String -> Flagged_ITrm > make_iop ":" > = Opr ( Spl ":" ) BinL 15 > make_iop op > = Opr ( OpIfx oprep ) BinR prc > where > ( oprep , prc ) = map_op op > map_op "\179" = ( And , 40 ) > map_op "\180" = ( Or , 30 ) > map_op "=" = ( Eq' , 15 ) > map_op "\172" = ( Issubtype , 70 ) lookup function analogous to table lookup (used outside parser) (returns option type) > lookup_name sg nm > = case lookUp nm sg of > Opnd (Itrm tm ) -> SOME tm > Prs_Err _ -> NONE > _ -> error "could be ok, check 'lookup_name' in parse.lhs" temporary lookup function The lookup function returns a term (symbol or constructor) representing the identifier `nm' if it is defined on the current signature (sg). The counter `i', `j' and `k' (for contructors only) are the indices of the symbol or constructor term. They are incremented as the signature is searched and will represent the correct values for an identifier, if and when it is encountered. The first (top level) function initialises the count for `i' and calls `lookup'' to search each declaration of the signature (sg). > lookUp :: String -> Sgn -> Flagged_ITrm > lookUp nm sg > = lookup' isg nm 0 > where > isg = internal_Sgn sg The function `lookup_dc' is used to search the next declaration on the signature (dc). If the identifier is found (in_dc True), the accompanying term (tm) given by `lookup_dc' is returned. If the identifier is not found (in_dc False), `lookup'' is called recursively on the rest of the signature (sg). The count `i' is incremented to indicate that the next declaration on the signature is under consideration. If the signature is empty (2nd clause), the identifier is undefined and an error message is returned. Note that the initialised values to `lookup_dc' ( [] and 0 ) are the list of unsearched declarations (the second components of decpairs which have not been searched yet) and the count `j' of the symbol's position in the decpair "tree" respectively. > lookup' :: ISgn -> String -> Int -> Flagged_ITrm > lookup' ( Extend dc sg _ ) nm i > = if in_dc then tm > else lookup' sg nm ( i + 1 ) > where > ( in_dc , tm ) = lookup_dc dc [] nm i 0 > lookup' ( Empty _ ) nm i > = Prs_Err ( " Undefined symbol: " ++ nm ) `lookup_dc' is the driver function for the declaration search function. It uses the function `lookup_dc'' to examine a given declaration (dc) for a match. If a match is found (found True), the accompanying term (tm) is returned. If no match is found (found False), any remaining unsearched declarations (dcL) are examined. This is achieved by calling `lookup_dc' recursively incrementing the compound declaration pointer `j'. If the list (dcL) is empty, the symbol is undefined and a False flag is returned (the accompanying term is undefined in this case (error ""). > lookup_dc :: IDec -> [IDec] -> String -> Int -> Int -> ( Bool , Flagged_ITrm ) > lookup_dc dc dcL nm i j > = if found then ( found , tm ) > else case dcL of > dc : dcL' -> lookup_dc dc dcL' nm i ( j + 1 ) > [] -> ( False , error "" ) > where > ( found , tm ) = lookup_dc' dc dcL nm i j `lookup_dc'' examines a declaration for a given identifier (nm) by performing a case analysis on the declaration. > lookup_dc' :: IDec -> [IDec] -> String -> Int -> Int -> (Bool , Flagged_ITrm) If the declaration is a pair, search the first component declaration (dc1) using 'lookup_dc'. Add the second component (dc2) to the list of as yet unsearched declaration. This will be searched by `lookup_dc' is the search of `dc1' is unsuccessful. Note that the compound declaration position count `j' is incremented. > lookup_dc' ( Decpair dc1 dc2 _ ) dcL nm i j > = lookup_dc dc1 ( dc2 : dcL ) nm i ( j + 1 ) If the declaration is a symbol, the function `lookup_nm' is used to compare the required identifier (nm) against the symbol name (nm'). > lookup_dc' ( Symbol_dec _ ( ( _ , Symbol_Name nm' ) : _ ) ) _ nm i j > = lookup_nm nm' nm i j > lookup_dc' ( Axiom_dec _ ( ( _ , Symbol_Name nm' ) : _ ) ) _ nm i j > = lookup_nm nm' nm i j If the declaration is a datatype, the list of constructor names (nmL) is searched for a match using the function `lookup_nml'. > lookup_dc' ( Data _ _ [ ( _ , Datatype_Name nmL ) ] ) _ nm i j > = lookup_nml nmL nm i j 0 If the declaration is a definition, the function `lookup_nm' may again be used to compare the definition name (nm') against the required identifier (nm). > lookup_dc' ( Def _ _ [ ( _ , Symbol_Name nm' )] ) _ nm i j > = lookup_nm nm' nm i j Compare the given string identifier (nm) against a given name. A name is either a string identifier itself or an operator. > lookup_nm :: Name' -> String -> Int -> Int -> ( Bool , Flagged_ITrm ) If the name is a string identifier, a match occurs if the identifiers are the same ( nm == nm' ). In this case a symbol is returned representing the name (the required indices `i' and `j' are passed into the function. (The attribute `sym_nmd' is the name of the symbol.) If no match occurs, the flag False is returned. The accompanying term is undefined (error "") in this case. > lookup_nm ( Name nm' ) nm i j > | nm == nm' = ( True , ( Opnd . Itrm ) ( Sym i j [] [sym_nmd] ) ) > | otherwise = ( False , error "" ) If the `name' is an operator, a match occurs if the name of the operator (nm') matches the required identifier (nm). Again a symbol is returned for the identifier in this case (the symbol is flagged to be an operator (Opr) rather than an operand (Opnd) in this case however). If no match occurs the flag False is returned together with an undefined term as above. > lookup_nm ( Operator' nm' prc opt ) nm i j > | nm == nm' = ( True , Opr ( OpItrm ( Sym i j [] [sym_nmd] )) opt prc ) > | otherwise = ( False , error "" ) `lookup_nml' is similar to `lookup_nm' defined above except that a list of names is searched for a match rather that a single name. Here, if no match occurs, the tail of the list (nmL) is searched for a further match. Only if this list is empty is a flag returned indicating that no match has occured (3rd clause). The function is used to search a list of constructor names for a match. A constructor ITrm (Const) is hence returned rather than a symbol ITrm (Sym) The count `k' indicates that position in the list where a match occurs and is thus increment whenever a match fails and the tail of the list is considered. The other indices `i' and `j' are passed into the function. > lookup_nml :: [Name'] -> String -> Int -> Int -> Int -> (Bool , Flagged_ITrm) > lookup_nml ( Name nm' : nml ) nm i j k > | nm == nm' = ( True , ( Opnd . Itrm ) ( Const i j k [] [sym_nmd] ) ) > | otherwise = lookup_nml nml nm i j ( k + 1 ) > lookup_nml ( Operator' nm' prc opt : nml ) nm i j k > | nm == nm' = ( True , Opr > ( OpItrm ( Const i j k [] [sym_nmd] )) opt prc ) > | otherwise = lookup_nml nml nm i j ( k + 1 ) > lookup_nml [] _ _ _ _ > = ( False , error "" ) dummy token list returned with error messages. Used to ensure parse function looking for a separator is given one hence preventing failure to pattern match in ( _ : tkl ) expresions (see introduction to `term'' function above). > dmy :: [Token] > dmy = [ Rvd "" ] extend a signature embedded in a parse state with a declaration expressed as a flagged_itrm. (lazy evaluation ensures that this function will not be evaluated if the declaration argument is not Idec.) > pst_extend :: Flagged_ITrm -> Parse_State -> Parse_State > pst_extend ( Opnd ( Idec idc )) ( tgL , sg ) > = ( tgL , extend dc sg ) > where > dc = build_dc sg idc check for a tag in tag list > fetch_tg tg_nm1 ( tg@( tg_nm2 , _ , _ ) : tgL ) > | tg_nm1 == tg_nm2 = ( True , tg ) > | otherwise = fetch_tg tg_nm1 tgL > fetch_tg _ [] = ( False , ( "" , [] , [] ) ) derivation parser build derivations > parse_deriv :: Parse_State -> Flagged_ITrm -> Thm > parse_deriv pst ( Opnd ( Itrm itm )) > = deriv pst itm > parse_deriv _ _ > = TH_Err "unimplemented feature" > deriv :: Parse_State -> ITrm -> Thm > deriv pst@( tgL , sg ) ( Tagid ( str , _ , cnv_fnL ) argL ) > = case fetch_fn cnv_fnL of > Ok cnv_fn -> cnv_fn argL > Bad mesg -> TH_Err mesg > where > fetch_fn ( Thm_Fn fn : _ ) = Ok fn > fetch_fn ( _ : oth ) = fetch_fn oth > fetch_fn [] = Bad ( "cannot convert tag " ++ str ++ " to theorem" ) > deriv pst@( tgL , sg ) ( Binder Delta idc itm _ _ ) > = case typ_of_trm sg2 dc_typ of > Constant Bool' _ _ -> discharge th > Constant ( Univ _ ) _ _ -> generalise th > otherwise -> TH_Err "dc type not bool or univ" > where > th = deriv ( tgL , extend dc sg ) itm > ( dc_typ , _ , sg2 ) = internal_Trm ( typ_of_Dec dc ) > dc = build_dc sg idc > deriv pst@( _ , sg ) ( App itm1 itm2 _ _ ) > = case th_tm of > Binder Forall _ _ _ _ -> specialise th1 tm > Binder Imp _ _ _ _ -> modus_ponens th1 th2 > otherwise -> TH_Err "not \177 or \182" > where > th1 = deriv pst itm1 > th2 = deriv pst itm2 > tm = build_trm' sg itm2 > ( th_tm , _ ) = internal_Thm th1 > deriv pst@( _ , sg ) ( Pair itm1 itm2 _ _ _ ) > = modus_ponens ( modus_ponens spec_th th1 ) th2 > where > spec_th = specialise ( specialise th tm1 ) tm2 > tm1 = typ_of_Thm th1 > tm2 = typ_of_Thm th2 > th1 = deriv pst itm1 > th2 = deriv pst itm2 > th = taut ( parse_tm pst str ) > str = "\177 a:bool. \177 b:bool.a \182 b \182 a \179 b" > deriv ( _ , sg ) ( Sym i j _ _ ) > = axiom sg i j > deriv pst@( _ , SG isg ) itm > = TH_Err (" Invalid construction: " ++ unparse' isg itm ) > deriv _ _ = error "deriv error" integer list parser errors made into term argument (Tag_Trm) and passed back as malformed term. (integer lists do not have an error constructor). Otherwise Tag_Int with accompanying list returned. > parse_iL :: [Token] -> ( Tag_Arg , [Token] ) > parse_iL ( Rvd "\168" : tkL ) > = parse_iL' [] tkL > parse_iL _ = ( Tg_Trm ( TM_Err "Malformed integer list" ) , dmy ) > parse_iL' iL ( Clr str : tkL ) | and ( map isDigit str ) > = parse_iL'' ( read str : iL ) tkL > parse_iL' iL ( Rvd "\169" : tkL ) > = ( Tg_Int iL , tkL ) > parse_iL' iL ( tk : _ ) > = ( Tg_Trm ( TM_Err ( "Malformed item in integer list: " ++ disp_tk tk )) , dmy ) > parse_iL' iL [] > = ( Tg_Trm ( TM_Err "Unexpected end of input" ) , dmy ) > parse_iL'' iL ( Rvd "\169" : tkL ) > = ( Tg_Int iL , tkL ) > parse_iL'' iL ( Rvd "," : tkL ) > = parse_iL' iL tkL > parse_iL'' iL _ > = ( Tg_Trm ( TM_Err " ',' or '\169' expected " ) , dmy )