diff --git a/.gitignore b/.gitignore index 00b97d1..347b573 100644 --- a/.gitignore +++ b/.gitignore @@ -15,3 +15,5 @@ version.tex bin/ .depend ocamlgraph-1.7 +.merlin +make_merlin.sh \ No newline at end of file diff --git a/src/auxl.ml b/src/auxl.ml index 5c64e04..d955d44 100644 --- a/src/auxl.ml +++ b/src/auxl.ml @@ -31,11 +31,13 @@ (* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) (**************************************************************************) -open Types +open Types;; +open Location (* exceptions ************************************************************ *) exception ThisCannotHappen +exception Located_Failure of (loc option)*string (* debug, warning and error report *************************************** *) @@ -52,17 +54,33 @@ let mode_name m = match m with | Lex _ -> "Lex" | Menhir _ -> "Menhir" +let colour = ref true + +let maybe_pp_loc l = + match l with + | None -> "" + | Some l -> if !colour then "\027[1m" ^ pp_loc l ^ ":\027[0m\n" else pp_loc l ^ ":\n" + +let warning_string () = if !colour then "\027[1m\027[35mWarning: \027[0m" else "Warning: " + +let error_string () = if !colour then "\027[1m\027[31mError: \027[0m" else "Error: " + let debug_on = false let debug s = if debug_on then begin print_string s; flush stdout end -let warning s = print_endline ("warning: " ^ s); flush stdout +let warning l s = print_endline (maybe_pp_loc l ^ warning_string () ^ s); flush stdout + +let report_error l s = print_endline (maybe_pp_loc l ^ error_string () ^ s); flush stdout + + +let error l s = raise (Located_Failure (l, s)) -let error s = print_endline ("error: " ^ s); flush stdout; exit 2 +let exit_with l s = print_endline (maybe_pp_loc l ^ error_string () ^ s); flush stdout; exit 2 -let int_error s = print_endline("internal: " ^ s); flush stdout; exit 2 +let int_error s = raise (Located_Failure (None, "internal: " ^ s)) -let errorm m s = print_endline ("internal (" ^ mode_name m ^ "): " ^ s); flush stdout; exit 2 +let errorm m s = raise (Located_Failure (None, "internal (" ^ mode_name m ^ "): " ^ s)) (* ***************** *) @@ -301,7 +319,7 @@ let prod_of_prodname ?(warn=true) (xd:syntaxdefn) (pn:prodname) : prod = List.find (fun r -> List.exists (fun p -> p.prod_name=pn) r.rule_ps) xd.xd_rs - with Not_found -> if warn then warning ("internal: prod_of_prodname: searching pn = "^pn^"\n"); raise Not_found in + with Not_found -> if warn then warning None ("internal: prod_of_prodname: searching pn = "^pn^"\n"); raise Not_found in List.find (fun p -> p.prod_name=pn) r.rule_ps (* let prod_of_prod_name : prodname -> prod *) (* = fun prod_name' -> *) @@ -621,6 +639,26 @@ let hom_spec_for_hom_name hn homs = let hom_spec_for_pp_mode m homs = hom_spec_for_hom_name (hom_name_for_pp_mode m) homs +let loc_of_symterm st = match st with + | St_node (l,_) -> l + | St_nonterm (l,_,_) -> l + | St_nontermsub (l,_,_,_) -> l + | St_uninterpreted (l,_) -> l + +let loc_of_symterm_element ste = match ste with + | Types.Ste_st (loc,_) -> loc + | Types.Ste_metavar (loc,_,_) -> loc + | Types.Ste_var (loc,_,_) -> loc + | Types.Ste_list (loc,_) -> loc + +let loc_of_mvr xd mvr = (mvd_of_mvr_nonprimary xd mvr).mvd_loc + +let loc_of_ntr (xd:syntaxdefn) (ntr:nontermroot) = + (rule_of_ntr xd ntr).rule_loc + +let loc_of_prodname ?(warn=true) (xd:syntaxdefn) (pn:prodname) = + (prod_of_prodname xd pn).prod_loc + let loc_of_raw_element e = match e with | Raw_ident (l,_) @@ -1040,11 +1078,11 @@ and rename_bound map b = match b with bclu_upper = rename_suffix_item map bclu.bclu_upper } and rename_bindspec map bs = match bs with -| Bind(mse,nt)->Bind(rename_mse map mse,rename_nonterm map nt) -| AuxFnDef(auxfn,mse)->AuxFnDef(auxfn, rename_mse map mse) -| NamesEqual(mse,mse')->NamesEqual(rename_mse map mse,rename_mse map mse') -| NamesDistinct(mse,mse')->NamesDistinct(rename_mse map mse,rename_mse map mse') -| AllNamesDistinct(mse)->AllNamesDistinct(rename_mse map mse) +| Bind(loc,mse,nt)->Bind(loc,rename_mse map mse,rename_nonterm map nt) +| AuxFnDef(loc,auxfn,mse)->AuxFnDef(loc,auxfn, rename_mse map mse) +| NamesEqual(loc,mse,mse')->NamesEqual(loc,rename_mse map mse,rename_mse map mse') +| NamesDistinct(loc,mse,mse')->NamesDistinct(loc,rename_mse map mse,rename_mse map mse') +| AllNamesDistinct(loc,mse)->AllNamesDistinct(loc,rename_mse map mse) and rename_mse map mse = match mse with | MetaVarExp(mv)->MetaVarExp(rename_metavar map mv) @@ -1119,8 +1157,8 @@ and rename_freevar map fv = fv_that = rename_nt_or_mv_root map fv.fv_that; } and rename_parsing_annotations map pas = - { pa_data = List.map (fun (ntr1,pa_type,ntr2)-> - (rename_nontermroot map ntr1,pa_type,rename_nontermroot map ntr2)) pas.pa_data } + { pa_data = List.map (fun (ntr1,pa_type,ntr2,l)-> + (rename_nontermroot map ntr1,pa_type,rename_nontermroot map ntr2,l)) pas.pa_data } and rename_dependencies map xddep = { xd_dep_ts = List.map (List.map (rename_nt_or_mv_root map)) xddep.xd_dep_ts; @@ -1265,7 +1303,7 @@ let avoid xd mvs0 nts0 = match mvd.mvd_indexvar with | true -> if mvr=mvd.mvd_name then - warning ("warning: indexvar \""^mvr^"\" is primary so may give a name-clash\n") ; + warning None ("warning: indexvar \""^mvr^"\" is primary so may give a name-clash\n") ; None | false -> if mvr=mvd.mvd_name then Some mv else None @@ -1350,7 +1388,7 @@ let secondaryify xd mvs0 nts0 = match mvd.mvd_indexvar with | true -> if mvr=mvd.mvd_name then - warning ("indexvar \""^mvr^"\" is primary so may give a name-clash\n") ; + warning None ("indexvar \""^mvr^"\" is primary so may give a name-clash\n") ; Some mv | false -> Some mv @@ -1479,49 +1517,51 @@ uppercase *) let rec detect_conflicts l = match l with - | [] -> (false,"") - | (_,x)::tl -> - if List.mem x (List.map (fun x -> snd x) tl) - then (true,x) + | [] -> (false,"",dummy_loc) + | (loc,_,x)::tl -> + if List.mem x (List.map (fun (_,_,x) -> x) tl) + then (true,x,loc) else detect_conflicts tl +let remove_fst (_,x,y) = (x,y) + + let capitalize_prodnames sd = let rule_list = sd.syntax.xd_rs in let prod_list = List.flatten (List.map (fun r -> r.rule_ps) rule_list) in - let prod_name_list = List.map (fun p -> p.prod_name) prod_list in - let map_prod_names = List.map (fun pn -> (pn,String.capitalize pn)) prod_name_list in - let (conflict,err_msg) = detect_conflicts map_prod_names in + (* let prod_name_list = List.map (fun p -> p.prod_name) prod_list in *) + let map_prod_names = List.map (fun p -> (p.prod_loc, p.prod_name, String.capitalize p.prod_name)) prod_list in + let (conflict,err_msg,loc) = detect_conflicts map_prod_names in if conflict - then error ("Renaming of production name \""^err_msg^"\" generates a conflict\n") - else map_prod_names + then error (Some loc) ("Renaming of production name \""^err_msg^"\" generates a conflict\n") + else List.map remove_fst map_prod_names let uncapitalize_prodnames sd = let rule_list = sd.syntax.xd_rs in let prod_list = List.flatten (List.map (fun r -> r.rule_ps) rule_list) in - let prod_name_list = List.map (fun p -> p.prod_name) prod_list in - let map_prod_names = List.map (fun pn -> (pn,String.uncapitalize pn)) prod_name_list in - let (conflict,err_msg) = detect_conflicts map_prod_names in + let map_prod_names = List.map (fun p -> (p.prod_loc, p.prod_name, String.uncapitalize p.prod_name)) prod_list in + let (conflict,err_msg,loc) = detect_conflicts map_prod_names in if conflict - then error ("Renaming of production name \""^err_msg^"\" generates a conflict\n") - else map_prod_names + then error (Some loc) ("Renaming of production name \""^err_msg^"\" generates a conflict\n") + else List.map remove_fst map_prod_names let uncapitalize_primary_nontermroots sd = let rule_list = sd.syntax.xd_rs in - let nontermroots_list = List.map (fun r -> r.rule_ntr_name) rule_list in - let map_nontermroots = List.map (fun ntr -> (ntr,String.uncapitalize ntr)) nontermroots_list in - let (conflict,err_msg) = detect_conflicts map_nontermroots in + let nontermroots_list = List.map (fun r -> (r.rule_loc, r.rule_ntr_name)) rule_list in + let map_nontermroots = List.map (fun (loc,ntr) -> (loc,ntr,String.uncapitalize ntr)) nontermroots_list in + let (conflict,err_msg,loc) = detect_conflicts map_nontermroots in if conflict - then error ("Renaming of primary nontermroot \""^err_msg^"\" generates a conflict\n") - else map_nontermroots + then error (Some loc) ("Renaming of primary nontermroot \""^err_msg^"\" generates a conflict\n") + else List.map remove_fst map_nontermroots let uncapitalize_primary_metavarroots sd = let metavardefn_list = sd.syntax.xd_mds in - let metavarroots_list = List.map (fun mvd -> mvd.mvd_name) metavardefn_list in - let map_metavarroots = List.map (fun mvr -> (mvr,String.uncapitalize mvr)) metavarroots_list in - let (conflict,err_msg) = detect_conflicts map_metavarroots in + let metavarroots_list = List.map (fun mvd -> (mvd.mvd_loc, mvd.mvd_name)) metavardefn_list in + let map_metavarroots = List.map (fun (loc,mvr) -> (loc,mvr,String.uncapitalize mvr)) metavarroots_list in + let (conflict,err_msg,loc) = detect_conflicts map_metavarroots in if conflict - then error ("Renaming of primary metavar \""^err_msg^"\" generates a conflict\n") - else map_metavarroots + then error (Some loc) ("Renaming of primary metavar \""^err_msg^"\" generates a conflict\n") + else List.map remove_fst map_metavarroots let caml_rename sd = let map_prod_names = capitalize_prodnames sd in @@ -1741,7 +1781,7 @@ let rec pp_tex_escape_alltt s = let isa_filename_check s = match string_remove_suffix s ".thy" with - | None -> error ("Isabelle filenames must end with .thy\n") + | None -> error None ("Isabelle filenames must end with .thy\n") | Some s1 -> s1 let hol_filename_check s = @@ -1781,7 +1821,7 @@ let prod_require_nominal m xd p = List.exists ( fun bs -> match bs with - | Bind (MetaVarExp (mvr,_), nt) -> + | Bind (_, MetaVarExp (mvr,_), nt) -> is_nominal_atom m xd (mvd_of_mvr xd (primary_mvr_of_mvr xd mvr) ) | _ -> false ) p.prod_bs diff --git a/src/bounds.ml b/src/bounds.ml index 90ae2e6..64313bb 100644 --- a/src/bounds.ml +++ b/src/bounds.ml @@ -31,12 +31,12 @@ (* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) (**************************************************************************) -exception NotImplementedYet;; +exception NotImplementedYet;; open Types;; open Location;; -exception Bounds of string +exception Bounds of loc * string (** ******************************** *) @@ -55,7 +55,7 @@ let sie_null = [Si_punct ""] (* given a bounds environment be and a suffix suff, return at most one bound *) (* referenced in the suffix. fail if the suffix references >1 bound*) -let findbounds (be : bound list) (suff : suffix) : bound option +let findbounds (be : bound list) (suff : suffix) loc : bound option = let rec indices suff = match suff with | [] -> [] @@ -66,7 +66,7 @@ let findbounds (be : bound list) (suff : suffix) : bound option | [] -> None | [i] -> (*print_string ("<<<< "^string_of_int i^" >>>>");flush stdout;*) Some(List.nth be i) - | _ -> raise (Bounds "findbounds: multiple suffix indices in a suffix") + | _ -> raise (Bounds (loc, "findbounds: multiple suffix indices in a suffix")) (* collect all the nonterms/metavars in a symterm *) (* (and their nontermsub-lower-and-top data if they have it), *) @@ -75,13 +75,13 @@ let rec nt_or_mv_of_symterm (be : bound list) st : ((nt_or_mv * subntr_data) * bound option ) list = match st with | St_node (_,stnb) -> nt_or_mv_of_symterm_node_body be stnb - | St_nonterm (_,_,(ntr,sf)) -> [ (((Ntr ntr),sf),None),findbounds be sf ] - | St_nontermsub (_,ntrl,ntrt,(ntr,sf)) -> [(((Ntr ntr),sf),Some(ntrl,ntrt(*ntru*))),findbounds be sf ] + | St_nonterm (_,_,(ntr,sf)) -> [ (((Ntr ntr),sf),None),findbounds be sf (Auxl.loc_of_symterm st) ] + | St_nontermsub (_,ntrl,ntrt,(ntr,sf)) -> [(((Ntr ntr),sf),Some(ntrl,ntrt(*ntru*))),findbounds be sf (Auxl.loc_of_symterm st) ] | St_uninterpreted (_,_)-> [] and nt_or_mv_of_symterm_element be ste = match ste with | Ste_st (_,st) -> nt_or_mv_of_symterm be st - | Ste_metavar (_,_,(mvr,sf)) -> [ (((Mvr mvr),sf),None),findbounds be sf ] + | Ste_metavar (_,_,(mvr,sf)) -> [ (((Mvr mvr),sf),None),findbounds be sf (Auxl.loc_of_symterm_element ste) ] | Ste_var _ -> [] | Ste_list (_,stlis) -> List.concat (List.map (nt_or_mv_of_symterm_list_item be) stlis) @@ -102,7 +102,7 @@ let nt_or_mv_of_symterms sts = (* check for each Bound_dotform bound that it occurs with only one length constraint. Return the bounds without duplicates *) -let check_length_consistency : +let check_length_consistency loc : ((nt_or_mv* subntr_data) * bound option ) list -> bound list = function xys -> @@ -115,7 +115,7 @@ let check_length_consistency : (try ( let i=List.assoc (bd.bd_lower,bd.bd_upper) acc in if i=bd.bd_length then f acc bounds' - else raise (Bounds ("bound "^Grammar_pp.pp_plain_bound b^" has inconsistent length constraints, \""^Grammar_pp.pp_plain_dots i ^"\" and \""^ Grammar_pp.pp_plain_dots bd.bd_length ^ "\""))) + else raise (Bounds (loc, "bound "^Grammar_pp.pp_plain_bound b^" has inconsistent length constraints, \""^Grammar_pp.pp_plain_dots i ^"\" and \""^ Grammar_pp.pp_plain_dots bd.bd_length ^ "\""))) with Not_found -> f (((bd.bd_lower,bd.bd_upper),bd.bd_length)::acc) bounds' ) | b::bounds' -> f acc bounds' in @@ -142,7 +142,7 @@ let check_length_consistency : (* check for each nt_or_mv (and subntr data) that it doesn't appear with *) (* multiple different bounds, and return a list without duplicates *) -let check_bounds_consistency : +let check_bounds_consistency loc : ((nt_or_mv*subntr_data) * bound option) list -> ((nt_or_mv*subntr_data) * bound option) list = function xbos -> @@ -154,8 +154,9 @@ let check_bounds_consistency : | None -> f ((x,bo)::acc) xbos' | Some bo' -> (if bo=bo' then f acc xbos' - else - raise (Bounds ("inconsistent bounds for "^Grammar_pp.pp_plain_nt_or_mv (fst x)^": "^Grammar_pp.pp_plain_bound_option bo ^" and "^Grammar_pp.pp_plain_bound_option bo' )))) in + else + (* TODO *) + raise (Bounds (loc, "inconsistent bounds for "^Grammar_pp.pp_plain_nt_or_mv (fst x)^": "^Grammar_pp.pp_plain_bound_option bo ^" and "^Grammar_pp.pp_plain_bound_option bo' )))) in f [] xbos (* split into those without a bound and those with one *) @@ -328,10 +329,10 @@ let dotenv23 ntmvsn_without_bounds ntmvsn_with_bounds = let bound_extraction m xd loc sts : dotenv * dotenv3 * string = try let x = nt_or_mv_of_symterms sts in - let bounds = check_length_consistency x in + let bounds = check_length_consistency loc x in let pp_bounds = String.concat " " (List.map Grammar_pp.pp_plain_bound bounds) in - let ntmvsn_with_boundopts = check_bounds_consistency x in + let ntmvsn_with_boundopts = check_bounds_consistency loc x in let ntmvsn_without_bounds,ntmvsn_with_bounds = split_bounded ntmvsn_with_boundopts in let bound_with_ntmvsnss = nt_or_mv_per_bound ntmvsn_with_bounds in let de1 = dotenv1 m xd bound_with_ntmvsnss in @@ -347,7 +348,7 @@ let bound_extraction m xd loc sts : dotenv * dotenv3 * string = ^ Grammar_pp.pp_plain_dotenv de in de, de3, s with - Bounds s' -> raise (Bounds (s'^" at "^Location.pp_loc loc)) + Bounds (_, s') -> raise (Bounds (loc, s')) (* with e -> *) (* "exception in bound_extraction" *) diff --git a/src/bounds.mli b/src/bounds.mli index ab25c19..f4a5714 100644 --- a/src/bounds.mli +++ b/src/bounds.mli @@ -31,7 +31,9 @@ (* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) (**************************************************************************) -exception Bounds of string +open Types;; + +exception Bounds of loc * string val nt_or_mv_of_symterms : Types.symterm list -> ((Types.nt_or_mv * Types.subntr_data) * Types.bound option) list diff --git a/src/context_pp.ml b/src/context_pp.ml index c21468e..0bcf113 100644 --- a/src/context_pp.ml +++ b/src/context_pp.ml @@ -84,7 +84,7 @@ let context_app_rhs m xd lookup (hole:nonterm) (target:nontermroot) (r:rule) (p: ( match m with | Caml _ -> Auxl.capitalize_prodnames_in_symterm (List.hd sts) | _ -> List.hd sts ) - | _ -> Auxl.warning ("internal: multiple parses context fake rhs: "^fake_rhs^"\n"); List.hd sts in + | _ -> Auxl.warning None ("internal: multiple parses context fake rhs: "^fake_rhs^"\n"); List.hd sts in let sie = [] in let ((de1,de2) as de,de3,pptbe) = Bounds.bound_extraction m xd dummy_loc [sts_e] in (true, Some (Grammar_pp.pp_symterm m xd sie de sts_e)) diff --git a/src/coq_induct.ml b/src/coq_induct.ml index 6ade4ff..67fbbc4 100644 --- a/src/coq_induct.ml +++ b/src/coq_induct.ml @@ -50,7 +50,7 @@ let need_induction m xd r = | _ -> false) elb.elb_es | Lang_option _ | Lang_sugaroption _ -> - Auxl.error "interal: option types not implemented in pp_induction\n" + Auxl.error (Some r.rule_loc) "interal: option types not implemented in pp_induction\n" | Lang_nonterm (_,_) | Lang_metavar (_,_) | Lang_terminal _ -> false in List.exists element_uses_list_nt p.prod_es in (not r.rule_meta) && (List.exists uses_list_nt r.rule_ps) diff --git a/src/defns.ml b/src/defns.ml index 39d83d4..7f876aa 100644 --- a/src/defns.ml +++ b/src/defns.ml @@ -31,12 +31,14 @@ (* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) (**************************************************************************) -exception NotImplementedYet;; -exception Rule_parse_error of string open Types;; open Location;; +open Auxl;; + +exception NotImplementedYet;; +exception Rule_parse_error of loc * string let rec iter_nosep f l = match l with [] -> () | x::l -> let _ = f x in iter_nosep f l @@ -508,7 +510,8 @@ let pp_defn fd (m:pp_mode) (xd:syntaxdefn) lookup (defnclass_wrapper:string) (un Printf.fprintf fd "\n #:mode (%s %s)\n\n" d.d_name (match mode with [Hom_string s] -> s - | _ -> Auxl.error ("rdx backend: cannot print mode for declaration: "^d.d_name)) + (* TODO *) + | _ -> Auxl.error (Some d.d_loc) ("rdx backend: cannot print mode for declaration: "^d.d_name)) with Not_found -> ()); iter_sep (pp_processed_semiraw_rule fd m xd) "\n\n" d.d_rules @@ -754,7 +757,7 @@ let fundefn_to_int_func (m:pp_mode) (xd:syntaxdefn) (deps:string list) (fd:funde match Auxl.hom_spec_for_hom_name "coq-struct" fd.fd_homs with | Some ([Hom_index i]) -> "{struct x" ^ string_of_int (i+1) ^ "} " | Some _ -> - Auxl.warning "malformed coq-struct homomorphism"; + Auxl.warning (* TODO *) None "malformed coq-struct homomorphism"; "{struct <<>>}" | None -> "" in @@ -918,7 +921,7 @@ let pp_fundefnclass (m:pp_mode) (xd:syntaxdefn) lookup (fdc:fundefnclass) : stri ( match h with | Some ([Hom_string s]) -> Some s | None -> None - | _ -> Auxl.warning "malformed isa-proof/hol-proof hom"; Some "<<>>" ) in + | _ -> Auxl.warning (Some fdc.fdc_loc) "malformed isa-proof/hol-proof hom"; Some "<<>>" ) in ( match m with | Coq _ | Caml _ | Lem _ -> None | Isa _ -> pp_proof (Auxl.hom_spec_for_hom_name "isa-proof" fdc.fdc_homs) @@ -932,7 +935,7 @@ let pp_fundefnclass (m:pp_mode) (xd:syntaxdefn) lookup (fdc:fundefnclass) : stri Auxl.print_with_comment m "\n" ("funs "^fdc.fdc_name) (Dependency.compute m xd int_funcs_collapsed) - | Twf _ -> Auxl.warning "internal: fundefnclass not implemented for Twelf"; "" + | Twf _ -> Auxl.warning (Some fdc.fdc_loc) "internal: fundefnclass not implemented for Twelf"; "" | Lex _ | Menhir _ -> "" @@ -1034,9 +1037,9 @@ let process_semiraw_rule (m: pp_mode) (xd: syntaxdefn) (lookup: made_parser) Grammar_parser.drule_line_annot (Grammar_lexer.my_lexer true Grammar_lexer.metalang) lexbuf with | Parsing.Parse_error | My_parse_error _ -> - raise (Rule_parse_error ("bad annotation in \""^s^"\" at "^Location.pp_loc l)) + raise (Rule_parse_error (l, "bad annotation in \""^s^"\" ")) | e -> - (print_string ("exception in parsing \""^s^"\" at "^Location.pp_loc l^"\n"); + (report_error (Some l) ("exception in parsing \""^s^"\\n"); flush stdout; raise e) in (* let categories = List.map del c in *) @@ -1108,8 +1111,8 @@ let process_semiraw_rule (m: pp_mode) (xd: syntaxdefn) (lookup: made_parser) let unfiltered_string = try Grammar_parser.unfiltered_spec_el_list (Grammar_lexer.my_lexer true Grammar_lexer.filter) lexbuf with - Parsing.Parse_error -> - Auxl.error ("unfiltered premise "^s^" cannot be parsed\n") in + Parsing.Parse_error -> + Auxl.error (Some l) ("unfiltered premise "^s^" cannot be parsed\n") in let collapsed_string = Auxl.collapse_embed_spec_el_list unfiltered_string in (*let filtered_string = Embed_pp.pp_embed_spec m xd lookup collapsed_string in*) (* walk over collapsed_string, building a new string (with -ARG- replacing each [[.]]) and a list of symterms (one for each [[.]]) *) @@ -1138,9 +1141,9 @@ let process_semiraw_rule (m: pp_mode) (xd: syntaxdefn) (lookup: made_parser) let premises = List.map fancy_parse lss1 in let conclusion = match lss2 with - | [] -> raise (Rule_parse_error ("rule with no conclusion at " ^ Location.pp_loc l)) + | [] -> raise (Rule_parse_error (l, "rule with no conclusion")) | [(l,s)] -> Term_parser.just_one_parse ~transform:(Term_parser.defn_transform prod_name) xd lookup rn_formula false l s - | _ -> raise (Rule_parse_error ("rule with multiple conclusions at " ^ Location.pp_loc l)) + | _ -> raise (Rule_parse_error (l, "rule with multiple conclusions")) in let c = Term_parser.cd_env_of_syntaxdefn xd in let dr = {drule_name = defnclass_wrapper^defn_wrapper^annot.dla_name; @@ -1230,13 +1233,13 @@ let process_raw_funclause let rhs = match e with | Ste_st(_,st) -> st - | _ -> Auxl.error "process_raw_funclause internal error - bad rhs" in + | _ -> Auxl.error (Some (Auxl.loc_of_symterm st)) "process_raw_funclause internal error - bad rhs" in (* print_string ("lhs symterm: "^ Grammar_pp.pp_plain_symterm lhs ^ "\n");flush stdout; *) (* print_string ("rhs symterm: "^ Grammar_pp.pp_plain_symterm rhs ^ "\n");flush stdout; *) { fc_lhs = lhs; fc_rhs = rhs; fc_loc = l } | _ -> - Auxl.warning ("process_raw_funclause lost symterm: " + Auxl.warning (Some (loc_of_symterm st)) ("process_raw_funclause lost symterm: " ^ Grammar_pp.pp_plain_symterm st ^ "\n"); let lhs = St_uninterpreted(l, "error") in let rhs = St_uninterpreted(l, Grammar_pp.pp_plain_symterm st) in diff --git a/src/defns.mli b/src/defns.mli index b1e928d..654021e 100644 --- a/src/defns.mli +++ b/src/defns.mli @@ -31,7 +31,11 @@ (* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) (**************************************************************************) -exception Rule_parse_error of string + +open Types;; +open Location;; + +exception Rule_parse_error of loc * string val pp_fun_or_reln_defnclass : out_channel -> Types.pp_mode -> diff --git a/src/dependency.ml b/src/dependency.ml index f51b644..9b1a7a2 100644 --- a/src/dependency.ml +++ b/src/dependency.ml @@ -216,7 +216,7 @@ let sort (l : ('b * 'b list * 'a) list) : ('b * 'a) list list * 'b list = List.assoc n (List.map (fun (x,y) -> (y,x)) !info) with Not_found -> (* Auxl.error ("internal: sort: cannot find a node labelled " ^ n ^ "\n") *) - Auxl.warning ("internal: sort: cannot find a node labelled " ^ n ^ "\n"); + Auxl.warning None ("internal: sort: cannot find a node labelled " ^ n ^ "\n"); raise Not_found in let add_vertex g i c v = @@ -231,7 +231,7 @@ let sort (l : ('b * 'b list * 'a) list) : ('b * 'a) list list * 'b list = let tnv = find_vertex tn g_vertex_info in if (not (G.mem_edge g snv tnv)) then G.add_edge g snv tnv with Not_found -> - Auxl.warning ("internal: sort: cannot connect " ^ sn ^ " to " ^ tn ^"\n") in + Auxl.warning None ("internal: sort: cannot connect " ^ sn ^ " to " ^ tn ^"\n") in (* adding vertexes *) let vl = List.map (function (x,_,_) -> x) l in @@ -310,7 +310,7 @@ let isa_primrec_collapse m xd (funcs:int_funcs) : int_funcs_collapsed = let collapse_clause m id (_, lhs, rhs) = match m with | Isa _ -> "\"" ^ id ^ " " ^ lhs ^ " = (" ^ rhs ^ ")\"\n" - | _ -> Auxl.error "internal: isa_collapse called with wrong target\n" in + | _ -> Auxl.error None "internal: isa_collapse called with wrong target\n" in let collapse_clauses m id clauses = String.concat "| " (List.map (collapse_clause m id) clauses) in @@ -341,19 +341,19 @@ let isa_primrec_collapse m xd (funcs:int_funcs) : int_funcs_collapsed = let rx_inp_type = Str.regexp ".*\"\\(.*\\) =>.*" in if Str.string_match rx_inp_type header 0 then Str.matched_group 1 header - else Auxl.error "internal: cannot extract the inp type from the header\n" in + else Auxl.error None "internal: cannot extract the inp type from the header\n" in let (inp_type,inp_type_list) = ( match List.map (fun x -> extract_inp_type x.r_fun_header) g with | h::t -> (h,t) | _ -> raise Auxl.ThisCannotHappen ) in if not (List.for_all (fun t -> String.compare inp_type t = 0) inp_type_list) - then Auxl.error "internal: collapsing functions over different types\n"; + then Auxl.error None "internal: collapsing functions over different types\n"; let extract_ret_type (header,_,_) = let rx_ret_type = Str.regexp ".*=> \\(.*\\)\"" in if Str.string_match rx_ret_type header 0 then Str.matched_group 1 header - else Auxl.error "internal: cannot extract the out type from the header\n" in + else Auxl.error None "internal: cannot extract the out type from the header\n" in let ret_types = List.map (fun x -> extract_ret_type x.r_fun_header) g in let output_type = @@ -373,7 +373,7 @@ let isa_primrec_collapse m xd (funcs:int_funcs) : int_funcs_collapsed = let compare_lhs l1 l2 = List.for_all2 (fun lc1 lc2 -> String.compare lc1 lc2 = 0) l1 l2 in if not (List.for_all (fun f -> compare_lhs lhs (extract_lhs f)) (List.tl g)) - then Auxl.error "internal: non equal lhs when collapsing"; + then Auxl.error None "internal: non equal lhs when collapsing"; (* 5- the rhs *) let extract_rhs f = @@ -576,13 +576,13 @@ let collapse m xd (funcs:int_funcs) : int_funcs_collapsed = | Coq _ -> coq_collapse m xd funcs | Twf _ -> twf_collapse m xd funcs | Caml _ -> caml_collapse m xd funcs - | Tex _ | Ascii _ -> Auxl.error "internal: collapse of Tex-Ascii\n" + | Tex _ | Ascii _ -> Auxl.error None "internal: collapse of Tex-Ascii\n" (* *** the printer *) let print m xd (sorting,refl) = match m with - | Tex _ | Ascii _ -> Auxl.error "internal: print of Tex-Ascii\n" + | Tex _ | Ascii _ -> Auxl.error None "internal: print of Tex-Ascii\n" | Isa io -> let print_lemma block = if ( List.exists diff --git a/src/grammar_lexer.mll b/src/grammar_lexer.mll index 76f96ee..46b7a31 100644 --- a/src/grammar_lexer.mll +++ b/src/grammar_lexer.mll @@ -47,6 +47,10 @@ open Grammar_parser exception Eof exception CannotHappen +let mkloc p = + [ { Location.loc_start = p; + Location.loc_end = p } ] + let incr_linenum lexbuf = let pos = lexbuf.Lexing.lex_curr_p in lexbuf.Lexing.lex_curr_p <- @@ -162,9 +166,9 @@ let my_lexer : bool -> lexer -> lexer = next_token () with ex -> - (print_string ("Lexing error at "^pp_position2 lexbuf.Lexing.lex_curr_p^"\n"); - flush stdout; - raise ex) + let loc = mkloc lexbuf.Lexing.lex_curr_p in + (error (Some loc) ("Lexing error"); + ) let trim : string -> string = fun s -> @@ -463,10 +467,13 @@ and comments surrounding_lexer level = parse | _ { comments surrounding_lexer level lexbuf } | eof - { warning ("open comment at " - ^ pp_position2 - (match level with p::ps->p | []->raise CannotHappen) - ^ " is not closed"); + { let + loc = + match level with + | p::ps -> mkloc p + | [] -> raise CannotHappen + in + warning None ("open comment is not closed "); raise End_of_file } and linecomment surrounding_lexer = parse diff --git a/src/grammar_parser.mly b/src/grammar_parser.mly index 50c37ee..7e6beab 100644 --- a/src/grammar_parser.mly +++ b/src/grammar_parser.mly @@ -52,8 +52,8 @@ let mkp () = (* {desc=x; loc=l} *) let parse_error s = - raise (My_parse_error ("Parse error: " ^ s ^ " " - ^ Location.pp_position2 (Parsing.symbol_end_pos () ))) + raise (My_parse_error (Some (mkl ()), "Problem parsing: " ^ s + )) (* %token EQUAL *) %} diff --git a/src/grammar_pp.ml b/src/grammar_pp.ml index befd1ef..d391e73 100644 --- a/src/grammar_pp.ml +++ b/src/grammar_pp.ml @@ -323,7 +323,7 @@ and pp_raw_dots n = | 0 -> pp_DOTDOT | 1 -> pp_DOTDOTDOT | 2 -> pp_DOTDOTDOTDOT - | _ -> Auxl.error "internal: >2 in pp_raw_dots" + | _ -> Auxl.error None "internal: >2 in pp_raw_dots" and pp_raw_prod p = pad 60 ((match p.raw_prod_flavour with Bar -> pp_BAR) @@ -757,7 +757,7 @@ let pp_tex_DOTDOTDOTDOT = "...." let pp_tex_NAME_PREFIX m = match m with | Tex xo -> xo.ppt_name_prefix - | _ -> Auxl.error "internal: pp_tex_NAME_PREFIX" + | _ -> Auxl.error None "internal: pp_tex_NAME_PREFIX" let pp_tex_METAVARS_NAME m = "\\"^pp_tex_NAME_PREFIX m^"metavars" let pp_tex_RULES_NAME m = "\\"^pp_tex_NAME_PREFIX m^"grammar" @@ -1225,7 +1225,7 @@ and pp_nt_or_mv_root_ty m xd ntmvr = | Ntr ntr -> pp_nontermroot_ty m xd ntr | Mvr mvr -> pp_metavarroot_ty m xd mvr -and coq_maybe_decide_equality m xd homs ntmvr = +and coq_maybe_decide_equality m xd homs ntmvr loc = match try Some (List.assoc "coq-equality" homs) with Not_found -> None with @@ -1246,7 +1246,7 @@ and coq_maybe_decide_equality m xd homs ntmvr = ^ ( match eh with | [ ] -> " decide equality; auto with ott_coq_equality arith." | [ Hom_string s ] -> s - | _ -> Auxl.error "malformed coq-equality homomorphism\n" ) + | _ -> Auxl.error (Some loc) "malformed coq-equality homomorphism\n" ) ^ "\nDefined.\n" ^ "Hint Resolve eq_" ^ type_name ^ " : ott_coq_equality.\n" @@ -1259,7 +1259,7 @@ and pp_metavardefn m xd mvd = (function (mvr,homs)->pp_metavarroot m xd mvr) mvd.mvd_names)) ^ " " ^ pp_CCE ^ " " - ^ pp_metavarrep m xd mvd.mvd_rep "" ^ "\n" + ^ (pp_metavarrep m xd mvd.mvd_rep "" mvd.mvd_loc) ^ "\n" | Tex xo -> " $ " ^ (String.concat " ,\\, "(List.map @@ -1273,8 +1273,8 @@ and pp_metavardefn m xd mvd = | Coq co -> let type_name = pp_metavarroot_ty m xd mvd.mvd_name in "Definition " ^ type_name ^ " := " - ^ pp_metavarrep m xd mvd.mvd_rep type_name ^ "." ^ pp_com ^ "\n" - ^ coq_maybe_decide_equality m xd mvd.mvd_rep (Mvr mvd.mvd_name) + ^ (pp_metavarrep m xd mvd.mvd_rep type_name mvd.mvd_loc) ^ "." ^ pp_com ^ "\n" + ^ coq_maybe_decide_equality m xd mvd.mvd_rep (Mvr mvd.mvd_name) mvd.mvd_loc | Rdx ro -> "" (* let type_name = pp_metavarroot_ty m xd mvd.mvd_name in *) (* ";; grammar_pp, 1279: " ^ type_name ^ " := " *) @@ -1284,7 +1284,7 @@ and pp_metavardefn m xd mvd = "type " ^ type_name ^ " = " - ^ pp_metavarrep m xd mvd.mvd_rep type_name + ^ pp_metavarrep m xd mvd.mvd_rep type_name mvd.mvd_loc ^ pp_com ^ "\n" | Isa io -> let type_name = pp_metavarroot_ty m xd mvd.mvd_name in @@ -1293,20 +1293,20 @@ and pp_metavardefn m xd mvd = "atom_decl \"" ^ type_name ^ "\"" ^ pp_com ^ "\n" else "type_synonym \"" ^ type_name ^ "\" = \"" - ^ pp_metavarrep m xd mvd.mvd_rep type_name^ "\"" ^ pp_com ^ "\n" + ^ (pp_metavarrep m xd mvd.mvd_rep type_name mvd.mvd_loc)^ "\"" ^ pp_com ^ "\n" | Hol ho -> let type_name = pp_metavarroot_ty m xd mvd.mvd_name in "val _ = type_abbrev(\"" ^ type_name ^ "\", ``:" - ^ pp_metavarrep m xd mvd.mvd_rep type_name ^ "``);" + ^ (pp_metavarrep m xd mvd.mvd_rep type_name mvd.mvd_loc) ^ "``);" ^ pp_com ^ "\n" | Lem lo -> let type_name = pp_metavarroot_ty m xd mvd.mvd_name in "type " ^ type_name ^ " = " - ^ pp_metavarrep m xd mvd.mvd_rep type_name + ^ pp_metavarrep m xd mvd.mvd_rep type_name mvd.mvd_loc ^ pp_com ^ "\n" | Twf _ -> "%abbrev " @@ -1316,7 +1316,7 @@ and pp_metavardefn m xd mvd = | Menhir _ -> "" | Ascii _ | Tex _ -> raise Auxl.ThisCannotHappen )) -and pp_metavarrep m xd mvd_rep type_name = +and pp_metavarrep m xd mvd_rep type_name loc = match m with | Ascii ao -> pp_homomorphism_list m xd mvd_rep @@ -1326,37 +1326,37 @@ and pp_metavarrep m xd mvd_rep type_name = ( try let hs = List.assoc "isa" mvd_rep in pp_hom_spec m xd hs - with Not_found -> Auxl.warning ("undefined isa metavarrep for "^type_name^"\n"); "UNDEFINED" ) + with Not_found -> Auxl.warning (Some loc) ("undefined isa metavarrep for "^type_name^"\n"); "UNDEFINED" ) | Hol ho -> ( try let hs = List.assoc "hol" mvd_rep in pp_hom_spec m xd hs - with Not_found -> Auxl.warning ("undefined hol metavarrep for "^type_name^"\n"); "UNDEFINED" ) + with Not_found -> Auxl.warning (Some loc) ("undefined hol metavarrep for "^type_name^"\n"); "UNDEFINED" ) | Lem lo -> ( try let hs = List.assoc "lem" mvd_rep in pp_hom_spec m xd hs - with Not_found -> Auxl.warning ("undefined lem metavarrep for "^type_name^"\n"); "UNDEFINED" ) + with Not_found -> Auxl.warning (Some loc) ("undefined lem metavarrep for "^type_name^"\n"); "UNDEFINED" ) | Coq co -> ( try let hs = List.assoc "coq" mvd_rep in pp_hom_spec m xd hs - with Not_found -> Auxl.warning ("undefined coq metavarrep for "^type_name^"\n"); "UNDEFINED" ) + with Not_found -> Auxl.warning (Some loc) ("undefined coq metavarrep for "^type_name^"\n"); "UNDEFINED" ) | Rdx ro -> ( try let hs = List.assoc "rdx" mvd_rep in pp_hom_spec m xd hs - with Not_found -> Auxl.warning ("undefined rdx metavarrep for "^type_name^"\n"); "UNDEFINED" ) + with Not_found -> Auxl.warning (Some loc) ("undefined rdx metavarrep for "^type_name^"\n"); "UNDEFINED" ) | Twf wo -> ( try let hs = List.assoc "twf" mvd_rep in pp_hom_spec m xd hs - with Not_found -> Auxl.warning ("undefined Twelf metavarrep for "^type_name^"\n"); "UNDEFINED" ) + with Not_found -> Auxl.warning (Some loc) ("undefined Twelf metavarrep for "^type_name^"\n"); "UNDEFINED" ) | Caml oo -> ( try let hs = List.assoc "ocaml" mvd_rep in pp_hom_spec m xd hs - with Not_found -> Auxl.warning ("undefined OCaml metavarrep for "^type_name^"\n"); "UNDEFINED" ) + with Not_found -> Auxl.warning (Some loc) ("undefined OCaml metavarrep for "^type_name^"\n"); "UNDEFINED" ) and pp_prodname m xd pn = (* FZ this is never called *) match m with @@ -1678,15 +1678,15 @@ and pp_plain_dotenv3 de3 = and pp_plain_bindspec bs = match bs with - | Bind (mse, nonterm) -> "Bind ("^pp_plain_mse mse^", "^pp_plain_nonterm nonterm^")" - | AuxFnDef (f,mse) -> "AuxFnDef ("^f^", "^pp_plain_mse mse^")" - | NamesEqual (_,_) -> "NamesEqual" - | NamesDistinct (_,_) -> "NamesDistinct" + | Bind (loc, mse, nonterm) -> "Bind ("^pp_plain_mse mse^", "^pp_plain_nonterm nonterm^")" + | AuxFnDef (loc, f,mse) -> "AuxFnDef ("^f^", "^pp_plain_mse mse^")" + | NamesEqual (loc,_,_) -> "NamesEqual" + | NamesDistinct (loc,_,_) -> "NamesDistinct" | AllNamesDistinct _ -> "AllNamesDistinct" and pp_bindspec m xd sie de bs = match bs with - | Bind (mse,nt) -> + | Bind (loc,mse,nt) -> ( match m with | Ascii ao -> pp_BIND^" " ^ pp_mse_string m xd sie de mse ^ " " @@ -1695,12 +1695,12 @@ and pp_bindspec m xd sie de bs = pp_tex_BIND ^ "\\; " ^ pp_mse_string m xd sie de mse ^ "\\; " ^ pp_tex_IN ^ "\\; " ^ pp_nonterm m xd nt | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) - | AuxFnDef (f,mse) -> + | AuxFnDef (loc,f,mse) -> ( match m with | Ascii ao -> pp_auxfn m xd f ^ "" ^ pp_EQ ^ "" ^ pp_mse_string m xd sie de mse | Tex xo -> pp_auxfn m xd f ^ "" ^ pp_tex_EQ ^ "" ^ pp_mse_string m xd sie de mse | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) - | NamesEqual (mse,mse') -> + | NamesEqual (loc,mse,mse') -> ( match m with | Ascii ao -> pp_NAMES ^ "" ^ pp_LPAREN ^ "" ^ pp_mse_string m xd sie de mse ^ "" ^ pp_RPAREN @@ -1711,7 +1711,7 @@ and pp_bindspec m xd sie de bs = ^ "" ^ pp_tex_RPAREN ^ "\\," ^ pp_tex_EQ ^ "\\," ^ pp_tex_NAMES ^ "" ^ pp_tex_LPAREN ^ "" ^ pp_mse_string m xd sie de mse' ^ "" ^ pp_tex_RPAREN | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) - | NamesDistinct (mse,mse') -> + | NamesDistinct (loc,mse,mse') -> ( match m with | Ascii ao -> pp_NAMES ^ "" ^ pp_LPAREN ^ "" ^ pp_mse_string m xd sie de mse ^ "" ^ pp_RPAREN @@ -1723,7 +1723,7 @@ and pp_bindspec m xd sie de bs = ^ pp_tex_NAMES ^ "" ^ pp_tex_LPAREN ^ "" ^ pp_mse_string m xd sie de mse' ^ ""^pp_tex_RPAREN | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen ) - | AllNamesDistinct mse -> + | AllNamesDistinct (loc,mse) -> ( match m with | Ascii ao -> pp_DISTINCTNAMES ^ "" ^ pp_LPAREN ^ "" ^ pp_mse_string m xd sie de mse @@ -2398,7 +2398,7 @@ and pp_nominal_prod m xd rnn rpw p = let rec arrange np bs = match bs with | [] -> np - | (Bind (MetaVarExp mv, nt)) :: bst -> + | (Bind (loc, MetaVarExp mv, nt)) :: bst -> let rnp = Auxl.option_map ( fun (bl,el) -> @@ -2669,7 +2669,7 @@ and pp_rule m xd r = (* returns a string option *) ^ "") | Coq co -> pp_internal_coq_buffer := !pp_internal_coq_buffer ^ - coq_maybe_decide_equality m xd r.rule_homs (Ntr r.rule_ntr_name); + coq_maybe_decide_equality m xd r.rule_homs (Ntr r.rule_ntr_name) r.rule_loc; if r.rule_meta || r.rule_phantom then None else @@ -3138,8 +3138,8 @@ and extract_nonterms_deep_ste_list slil = ( match slil with | [] -> [] | Stli_single (_,stel)::tl -> (extract_nonterms_deep stel) @ (extract_nonterms_deep_ste_list tl) - | Stli_listform _::tl -> - Auxl.warning "<>>"; + | Stli_listform hd::tl -> + Auxl.warning (Some hd.stl_loc) "<>>"; extract_nonterms_deep_ste_list tl ) and extract_nonterms_deep s = @@ -3151,7 +3151,7 @@ and extract_nonterms_deep s = | (Ste_st (_,St_node (_,stnb)))::t -> (extract_nonterms_deep stnb.st_es) @ (extract_nonterms_deep t) | (Ste_list (_,slil))::t -> (extract_nonterms_deep_ste_list slil) @ (extract_nonterms_deep t) | h::t -> - Auxl.warning + Auxl.warning (Some (Auxl.loc_of_symterm_element h)) ("internal: extract_nonterms_deep case failure\n " ^ (pp_plain_symterm_element h) ^ "\n\n"); (extract_nonterms_deep t) @@ -3163,13 +3163,13 @@ and extract_nonterms s = | (Ste_st (_,St_node (_,stnb)))::t -> (stnb.st_rule_ntr_name,[]) :: (extract_nonterms t) (* | (Ste_st (_,St_node (_,stnb)))::t -> (extract_nonterms stnb.st_es) @ (extract_nonterms t) *) | h::t -> - Auxl.warning + Auxl.warning (Some (Auxl.loc_of_symterm_element h)) ("internal: extract_nonterms case failure\n " ^ (pp_plain_symterm_element h) ^ "\n\n"); (extract_nonterms t) and pp_symterm_node_body_fancy_formula m xd sie de stnb : string = (* pull out the real symterm list *) - let sts = Auxl.option_map (function ste -> match ste with Ste_st(_,st) -> Some st | _ -> Auxl.error "internal: non Ste_st found in pp_symterm_node_body_fancy_formula") stnb.st_es in + let sts = Auxl.option_map (function ste -> match ste with Ste_st(_,st) -> Some st | _ -> Auxl.error None "internal: non Ste_st found in pp_symterm_node_body_fancy_formula") stnb.st_es in let pp_sts = List.map (pp_symterm m xd sie de) sts in let strings = Str.full_split (Str.regexp_string "-ARG-") stnb.st_prod_name in let pp_string s = match m with @@ -3191,7 +3191,7 @@ and pp_symterm_node_body m xd sie de stnb : string = try let ntrt,pps = List.assoc stnb.st_rule_ntr_name xd.xd_srd.srd_subrule_pn_promotion in try List.assoc stnb.st_prod_name pps with - Not_found -> Auxl.error ("internal error: pp_symterm_node_body \""^stnb.st_prod_name^"\" Not_found in pps "^pp_plain_pps pps) + Not_found -> Auxl.error (Some stnb.st_loc) ("internal error: pp_symterm_node_body \""^stnb.st_prod_name^"\" Not_found in pps "^pp_plain_pps pps) with Not_found -> stnb.st_prod_name in let p = Auxl.prod_of_prodname xd promoted_pn in @@ -3248,7 +3248,7 @@ and pp_symterm_node_body m xd sie de stnb : string = | Lem lo -> pp_symterm_element_judge_lem_plain m xd sie de p'' stnb'' | Ascii _ | Tex _ | Lex _ | Menhir _ -> raise ThisCannotHappen - | Caml _ -> Auxl.error "internal: Caml pp_symterm for proper symterms not supported" + | Caml _ -> Auxl.error (Some p''.prod_loc) "internal: Caml pp_symterm for proper symterms not supported" ) | _ -> raise (Invalid_argument ("pp_symterm_node_body2: strange production in formula_judgement"))) | _ -> raise (Invalid_argument ("pp_symterm_node_body3: strange production in formula judgement "))) @@ -3268,7 +3268,7 @@ and pp_symterm_node_body m xd sie de stnb : string = (match m with | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.errorm m "formula_dots" - | Caml _ -> Auxl.error "internal: Caml pp_symterm for proper symterms not supported" + | Caml _ -> Auxl.error (Some stnb.st_loc) "internal: Caml pp_symterm for proper symterms not supported" | Isa io -> (match isa_fancy_syntax_hom_for_prod m xd io p with | None -> @@ -3697,7 +3697,7 @@ and pp_symterm_list_items m xd sie (de :dotenv) tmopt prod_es stlis : (string * | (Lang_nonterm(ntr,_))::t -> ntr :: (intern t) | (Lang_metavar(mvr,_))::t -> mvr :: (intern t) | (Lang_terminal _)::t -> intern t - | _::t -> Auxl.warning "internal: elements_to_string never happen\n"; intern t ) + | _::t -> Auxl.warning None "internal: elements_to_string never happen\n"; intern t ) in (* List.rev *) (intern ls) in let include_terminals = @@ -3798,7 +3798,7 @@ and pp_symterm_list_item m xd sie (de :dotenv) tmopt include_terminals prod_es s | (Lang_nonterm(ntr,_))::t -> ntr :: (intern t) | (Lang_metavar(mvr,_))::t -> mvr :: (intern t) | (Lang_terminal _)::t -> intern t - | _::t -> Auxl.warning "internal: elements_to_string never happen\n"; intern t ) + | _::t -> Auxl.warning None "internal: elements_to_string never happen\n"; intern t ) in (* List.rev *) (intern ls) in match stli with @@ -3991,7 +3991,7 @@ and pp_symterm_list_body m xd sie (de :dotenv) tmopt include_terminals prod_es s (Auxl.promote_ntr xd ntr,b) :: (intern t) | (Lang_metavar(mvr,_))::t -> (mvr,false) :: (intern t) | (Lang_terminal _)::t -> intern t - | _::t -> Auxl.warning "internal: elements_to_string never happen\n"; intern t ) + | _::t -> Auxl.warning None "internal: elements_to_string never happen\n"; intern t ) in (* List.rev *) (intern ls) in let ty_list = Str.split (Str.regexp "(\\|*\\|)") de1i.de1_coq_type_of_pattern in @@ -4263,8 +4263,8 @@ and make_name_element m xd typ e = match e with | Ste_st (_,st) -> make_name_symterm m xd typ st | Ste_metavar (_,mvr,_) -> if typ then pp_metavarroot_ty m xd mvr else pp_metavarroot m xd mvr - | Ste_var (_,mvr,_) -> (* mvr *) Auxl.error "internal: Ste_var in make_name_element" - | Ste_list (_,stlil) -> Auxl.error "internal: Ste_list in make_name_element" + | Ste_var (_,mvr,_) -> (* mvr *) Auxl.error None "internal: Ste_var in make_name_element" + | Ste_list (_,stlil) -> Auxl.error None "internal: Ste_list in make_name_element" and make_name_elements m xd typ es = let sep = if typ then "*" else "_" in let lst = List.map (make_name_element m xd typ) es in @@ -4285,7 +4285,7 @@ and make_dep_element e = | Ste_st (_,st) -> make_dep_symterm st | Ste_metavar (_,mvr,_) -> [ mvr ] | Ste_var (_,mvr,_) -> [ mvr ] - | Ste_list (_,stlil) -> Auxl.error "internal: Ste_list in make_dep_element" + | Ste_list (_,stlil) -> Auxl.error None "internal: Ste_list in make_dep_element" and make_dep_elements es = List.concat (List.map make_dep_element es) diff --git a/src/grammar_typecheck.ml b/src/grammar_typecheck.ml index 0beea1c..1b6d11b 100644 --- a/src/grammar_typecheck.ml +++ b/src/grammar_typecheck.ml @@ -49,6 +49,13 @@ let rec firstdup xs = match xs with [] -> None | x::xs -> if (List.mem x xs) then Some x else firstdup xs +let rec firstdup_with f xs = + let rec helper xs keys = + match (xs,keys) with + | ([],[]) -> None + | (x::xs, key::keys) -> if (List.mem key keys) then Some x else helper xs keys + in helper xs (List.map f xs) + (* synthesising a raw aux-annotated rule *) @@ -375,14 +382,15 @@ let subrule (xd:syntaxdefn) (include_meta_prods:bool) (fun pu -> (include_meta_prods || not(pu.prod_meta)) && subprod subrule_graph pl pu) ru.rule_ps in match pus with | [] -> - ty_error + ty_error2 pl.prod_loc ( "subrule check failed: production " ^ Auxl.the (Grammar_pp.pp_prod error_opts xd "" "" pl) ^ " of rule " ^ rl.rule_ntr_name ^ " cannot be matched in rule " ^ ru.rule_ntr_name) "" | [pu] -> (pl.prod_name,pu.prod_name) | pu::pu'::pus' -> - Auxl.warning + (* TIDI get loc *) + Auxl.warning (Some pl.prod_loc) ("production \""^pl.prod_name^"\" is a subproduction of more than one production: "^String.concat ", " (List.map (function pu -> "\""^pu.prod_name^"\"") pus) ^" (taking the first)\n"); (pl.prod_name,pu.prod_name) ) @@ -561,8 +569,8 @@ let rec cd_hom hu c (es : element list) ((hn,hs,l0):raw_homomorphism): homomorph (* hmm - maybe we should check that this s is in fact one of the terminals *) (* of the grammar. But that info isn't to hand (eg in c) at present *) if not (rule_has_terminal (snd id) es) then begin - Auxl.warning ("Free variables in hom element " ^ Grammar_pp.pp_raw_hom_spec_el hse - ^ " at " ^ Location.pp_loc l0) + Auxl.warning (Some l0) ("Free variables in hom element " ^ Grammar_pp.pp_raw_hom_spec_el hse + ) end; Hom_terminal (snd id) ) with @@ -779,16 +787,16 @@ and cd_mse c (mse:raw_mse) : mse = and cd_bindspec c (bs:raw_bindspec) : bindspec = ( match bs with - | Raw_Bind (_,mse,(_,nt)) -> + | Raw_Bind (loc,mse,(_,nt)) -> ( match c.ident_lexer nt Location.dummy_pos (* TODO more useful pos *) with - | OP_Some (Tok_nonterm (_,ntr)) -> Bind (cd_mse c mse, ntr) + | OP_Some (Tok_nonterm (_,ntr)) -> Bind (loc,cd_mse c mse, ntr) | _ -> ty_error2 (Auxl.loc_of_raw_bindspec bs) ("bindspec must have a nonterminal on the right hand side, not \""^nt^"\"") "" ) - | Raw_AuxFnDef(_,(_,f),mse) -> AuxFnDef(f, cd_mse c mse) - | Raw_NamesEqual(_,mse,mse') -> NamesEqual(cd_mse c mse, cd_mse c mse') - | Raw_NamesDistinct(_,mse,mse') -> NamesDistinct(cd_mse c mse, cd_mse c mse') - | Raw_AllNamesDistinct(_,mse) -> AllNamesDistinct(cd_mse c mse) ) + | Raw_AuxFnDef(loc,(_,f),mse) -> AuxFnDef(loc,f, cd_mse c mse) + | Raw_NamesEqual(loc,mse,mse') -> NamesEqual(loc,cd_mse c mse, cd_mse c mse') + | Raw_NamesDistinct(loc,mse,mse') -> NamesDistinct(loc,cd_mse c mse, cd_mse c mse') + | Raw_AllNamesDistinct(loc,mse) -> AllNamesDistinct(loc,cd_mse c mse) ) and cd_metavarrep c (raw_mvd_name: string) (mvr:raw_metavarrep) : metavarrep = List.map @@ -1118,7 +1126,7 @@ and cd_element c (e:raw_element) : semiraw_element = elb_es = es' } in Sr_el(Lang_list elb) | (Raw_sugaroption (_, _)|Raw_nelist (_, _)|Raw_list (_, _)|Raw_option (_, _)) - -> Auxl.error "internal: sugaroption, nelist, list and option not supported" + -> Auxl.error (Some (Auxl.loc_of_raw_element e)) "internal: sugaroption, nelist, list and option not supported" and cd_comp_bound : cd_env -> raw_comp_bound -> bound * metavarroot = fun c rcb -> match rcb with @@ -1203,7 +1211,8 @@ and cd_subrules c (rsrs:raw_subrule list) : subrule list * subrule_data= (* report error if there is a cycle *) let ntrs_in_cycles = Auxl.option_map (fun (ntr,ntr') -> if ntr=ntr' then Some ntr else None) tc_edges in if ntrs_in_cycles <> [] then - ty_error ("subrule order has a cycle containing: "^String.concat " " (List.map (fun ntr -> "\""^Grammar_pp.pp_plain_nontermroot ntr^"\"") ntrs_in_cycles)) ""; + ty_error2 (List.hd srs0).sr_loc + ("subrule order has a cycle containing: "^String.concat " " (List.map (fun ntr -> "\""^Grammar_pp.pp_plain_nontermroot ntr^"\"") ntrs_in_cycles)) ""; let top_nodes = List.filter (fun ntr -> not (List.exists (fun (ntr',ntr'')-> ntr=ntr') tc_edges )) nodes0 in @@ -1211,7 +1220,7 @@ and cd_subrules c (rsrs:raw_subrule list) : subrule list * subrule_data= List.iter (fun ntr -> match tops_above ntr with [] | [_] -> () | ntrs -> - ty_error ("subrule order has multiple tops above \""^ntr^"\", ie "^String.concat " " (List.map (fun ntr -> "\""^Grammar_pp.pp_plain_nontermroot ntr^"\"") ntrs)) "") + ty_error2 (List.hd srs0).sr_loc ("subrule order has multiple tops above \""^ntr^"\", ie "^String.concat " " (List.map (fun ntr -> "\""^Grammar_pp.pp_plain_nontermroot ntr^"\"") ntrs)) "") nodes0; let promote_to_top ntr = @@ -1323,7 +1332,7 @@ and cd_parsing_annotation all_prod_names (par:raw_parsing_annotations) : parsing (fun (raw_pn1,pa,raw_pn2) -> check_prod_name raw_pn1; check_prod_name raw_pn2; - (raw_pn1, pa, raw_pn2)) + (raw_pn1, pa, raw_pn2,par.raw_pa_loc)) par.raw_pa_data and cd_parsing_annotations c pars = @@ -1359,7 +1368,7 @@ let check_structure (xd:syntaxdefn) (str:structure) : unit = | Mvr _ -> () | Ntr rd -> if not (List.mem rd (rgtosee@rgseen)) - then ty_error ("rule \""^r^"\" depends on rule \"" ^rd + then ty_error2 (Auxl.loc_of_ntr xd r) ("rule \""^r^"\" depends on rule \"" ^rd ^"\" which belongs to a future group of rules.\n") "") r_deps; end; @@ -1866,11 +1875,11 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b (fun rr -> (List.map fst rr.raw_rule_ntr_names)) rsd'.raw_sd_rs)) in (* collect together all the nontermroots, primaried, that occur on the left of a <:: *) - let wrapped_primary_ntr_of_ntr ntr = try + let wrapped_primary_ntr_of_ntr rsr ntr = try primary_ntr_of_ntr ntr with - | Not_found -> ty_error ("\""^ntr^"\" in subrule declaration is not a nonterminal root ") "" in - let srs_lowers = List.map (fun sr -> (wrapped_primary_ntr_of_ntr sr.raw_sr_lower)) rsd'.raw_sd_srs in + | Not_found -> ty_error2 rsr.raw_sr_loc ("\""^ntr^"\" in subrule declaration is not a nonterminal root ") "" in + let srs_lowers = List.map (fun sr -> (wrapped_primary_ntr_of_ntr sr sr.raw_sr_lower)) rsd'.raw_sd_srs in (* let srs_uppers = List.map (fun sr -> (wrapped_primary_ntr_of_ntr sr.raw_sr_upper)) rsd'.raw_sd_srs in *) (* 6- make a preliminary ident_lexer that doesn't know about any terminals *) @@ -2023,34 +2032,45 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b (* TODO: should check the bindspecs are consistent across subrules *) - let rec extract_auxfns_bindspec ntr b = + let rec merge_auxfns auxfns = + let fns = List.sort_uniq compare (List.map (fun (f,ntr,_) -> (f,ntr)) auxfns) + in let fnLocs = List.map + (fun fntr -> (fntr, + List.map (fun (_,_,l) -> l) + (List.filter (fun (f,ntr,_) -> (f,ntr) = fntr) auxfns) )) fns + in List.map (fun ((f,ntr),locs) -> (f,ntr,List.fold_right List.append locs [] )) fnLocs + + and auxfn_list_list_union lsts = merge_auxfns (Auxl.setlist_list_union lsts) + + and extract_auxfns_bindspec ntr b = ( match b with - | Bind (mse,nt) -> [] - | AuxFnDef (f,mse) -> [(f,ntr)] - | NamesEqual (mse,mse') -> [] - | NamesDistinct (mse,mse') -> [] - | AllNamesDistinct (mse) -> [] ) + | Bind (loc, mse,nt) -> [] + | AuxFnDef (loc,f,mse) -> [(f,ntr,loc)] + | NamesEqual (loc,mse,mse') -> [] + | NamesDistinct (loc,mse,mse') -> [] + | AllNamesDistinct (loc,mse) -> [] ) and extract_auxfns_production ntr p = - Auxl.setlist_list_union + auxfn_list_list_union (List.map (extract_auxfns_bindspec ntr) (p.prod_bs)) and extract_auxfns_rule r = - Auxl.setlist_list_union + auxfn_list_list_union (List.map (extract_auxfns_production r.rule_ntr_name) r.rule_ps) and extract_auxfns_syntaxdefn sd = - let auxfns0 = Auxl.setlist_list_union - (List.map extract_auxfns_rule + let auxfns00 = (List.map extract_auxfns_rule (List.filter (fun r -> not r.rule_meta) xd.xd_rs)) in - let comp (f,ntr) (f',ntr') = + let auxfns0 = Auxl.setlist_list_union auxfns00 + in + let comp (f,ntr,_) (f',ntr',_) = let x = String.compare f f' in if x <> 0 then x else compare ntr ntr' in List.sort comp auxfns0 in - let (auxfns : (auxfn * nontermroot) list) = extract_auxfns_syntaxdefn xd in + let (auxfns : (auxfn * nontermroot * loc) list) = extract_auxfns_syntaxdefn xd in (* print_string "extracted auxfns:\n"; *) (* List.iter (function (f,ntr) -> print_string (f^": "^ntr^" -> "^"?"^"\n")) auxfns; *) @@ -2075,7 +2095,7 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b | (pn,l)::pnls' -> (try let l' = List.assoc pn pnls' in - ty_error ("production name \""^pn^"\" is used for multiple productions, at "^Location.pp_loc l^" and "^Location.pp_loc l') "" + ty_error2 (l@l') ("production name \""^pn^"\" is used for multiple productions, at "^Location.pp_loc l^" and "^Location.pp_loc l') "" with Not_found -> find_first_duplicate2 pnls') | [] -> () in @@ -2136,7 +2156,7 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b (* ( "Auxiliary " ^ f ^ " in MSE not defined for nonterminal root " *) (* ^ Grammar_pp.pp_nontermroot error_opts xd ntr') "t_mse Aux2" ; *) if not (List.exists - (fun (f'',ntr'') -> f=f'' && Auxl.promote_ntr xd (primary_ntr_of_ntr ntr)=ntr'') + (fun (f'',ntr'',_) -> f=f'' && Auxl.promote_ntr xd (primary_ntr_of_ntr ntr)=ntr'') auxfns) then ty_error2 @@ -2159,7 +2179,7 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b (* ( "Auxiliary " ^ f ^ " in MSE not defined for nonterminal root " *) (* ^ Grammar_pp.pp_nontermroot error_opts xd ntr') "t_mse Aux2" ; *) if not(List.exists - (fun (f'',ntr'') -> f=f'' && Auxl.promote_ntr xd (primary_ntr_of_ntr ntr)=ntr'') + (fun (f'',ntr'',loc) -> f=f'' && Auxl.promote_ntr xd (primary_ntr_of_ntr ntr)=ntr'') auxfns) then ty_error2 @@ -2173,7 +2193,7 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b and t_bindspec ntr (es : element list) (l : loc) (b : bindspec) : mse_type = match b with - | Bind(mse,((ntr,suff) as nt)) -> + | Bind(loc,mse,((ntr,suff) as nt)) -> let mse_ty = (t_mse ntr es mse l) in if not (nt_in_es (Auxl.primary_ntr_of_ntr xd ntr,nt,[]) es) then @@ -2199,12 +2219,12 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b "manifestly null mse" "t_bindspec Bind2"; mse_ty - | AuxFnDef(f,mse) -> + | AuxFnDef(loc,f,mse) -> let mse_ty = t_mse ntr es mse l in (Mse_ty_aux f)::mse_ty - | NamesEqual(mse,mse') -> t_mse ntr es mse l @ t_mse ntr es mse' l - | NamesDistinct(mse,mse') -> t_mse ntr es mse l @ t_mse ntr es mse' l - | AllNamesDistinct(mse) -> t_mse ntr es mse l + | NamesEqual(loc,mse,mse') -> t_mse ntr es mse l @ t_mse ntr es mse' l + | NamesDistinct(loc,mse,mse') -> t_mse ntr es mse l @ t_mse ntr es mse' l + | AllNamesDistinct(loc,mse) -> t_mse ntr es mse l (* there is no t_element as anything that isn't recognised as a nonterminal or metavar is treated as a terminal *) @@ -2232,14 +2252,14 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b | [] -> [] | b :: bs -> ( match b with - | AuxFnDef(f,mse) -> f :: fs_actually_here bs + | AuxFnDef(loc,f,mse) -> f :: fs_actually_here bs | _ -> fs_actually_here bs ) ) in let fs_should_be_here = - List.map fst (List.filter (fun (f',ntr') -> ntr=ntr') auxfns) in + List.map (fun (x,y,z) -> x) (List.filter (fun (f',ntr' ,_) -> ntr=ntr') auxfns) in if (List.sort compare (fs_actually_here p.prod_bs) <> List.sort compare fs_should_be_here) then - ty_error + ty_error2 p.prod_loc ("auxiliaries are not uniquely defined in production " ^ p.prod_name) "t_production 1"; mse_tys); @@ -2263,10 +2283,11 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b (* | Some nt -> tcheck' false ("Repeated nonterminal "^Grammar_pp.pp_nonterm m nt^" in production "^p.prod_name) "t_production 2" *) and t_rule (r:rule) : mse_type list = - let ns = List.map (fun p -> p.prod_name) r.rule_ps in - ( match firstdup ns with + ( match firstdup_with (fun x -> x.prod_name) r.rule_ps with | None -> () - | Some x -> ty_error ("Repeated production name \"" ^ x^"\"") "t_productions 1"); + | Some x -> + (* TODO report both locs *) + ty_error2 x.prod_loc ("Repeated production name \"" ^ x.prod_name^"\"") "t_productions 1"); let mse_tys = if r.rule_meta then [] @@ -2305,7 +2326,11 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b add_vertices fs (n+1) ((f,n,v)::acc) in let auxfn_names = Auxl.remove_duplicates - (List.map (function (f,ntr)->f) auxfns) in + (List.map (function (f,ntr,loc)->f) auxfns) in + + (*TODO make faster*) + let auxfn_loc f = (fun (_,_,l) -> l) (List.hd (List.filter (fun (ff,_,_) -> ff == f ) auxfns ) ) in + let vertex_info = add_vertices auxfn_names 0 [] in @@ -2362,11 +2387,11 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b let ntmvrs = ntmvrs_of_component vs in match ntmvrs with | [ntmvr] -> (vs,ntmvr) - | [] -> ty_error ( + | [] -> ty_error2 (auxfn_loc (auxfn_of_vertex (List.hd vs)) ) ( "auxfns " ^ String.concat " " (List.map (function v->auxfn_of_vertex v) vs) ^ " have unconstrained result type") "" - | _ -> ty_error ( + | _ -> ty_error2 (auxfn_loc (auxfn_of_vertex (List.hd vs)) ) ( "auxfns " ^ String.concat " " (List.map (function v->auxfn_of_vertex v) vs) ^ " have overconstrained result type: " @@ -2383,7 +2408,7 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b (function (vs,ntmvr) -> List.mem v vs) components_with_ntmvr) in let ntrs = Auxl.option_map - (function (f',ntr')-> if f'=f then Some ntr' else None) + (function (f',ntr',_)-> if f'=f then Some ntr' else None) auxfns in (f,(ntrs,ntmvr))) auxfn_names in @@ -2404,11 +2429,11 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b let xd = { xd with xd_axs = axs } in (* hack: to allow repeated secondary nonterm roots, comment out the second of these *) - let ns = List.flatten - (List.map (fun r -> List.map fst r.rule_ntr_names) xd.xd_rs) in - ( match firstdup ns with + let ns = List.flatten (*TODO also highlight conflicting name*) + (List.map (fun r -> List.map (fun pr -> (fst pr, r)) r.rule_ntr_names) xd.xd_rs) in + ( match firstdup_with (fun pr -> fst pr) ns with | None -> () - | Some v -> ty_error ("repeated rule name "^v^"") "t_grammar 1"); + | Some (v,r) -> ty_error2 r.rule_loc ("repeated rule name "^v^"") "t_grammar 1"); (* check that subrules don't involve any semi-meta rules. *) (* TODO: should also check that they don't involve any rules with type homs *) @@ -2417,7 +2442,7 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b List.iter (fun ntr -> if (Auxl.rule_of_ntr xd ntr).rule_semi_meta - then ty_error ("cannot have semi-meta rule \""^ntr^"\" in a subrule relationship") "") + then ty_error2 (Auxl.loc_of_ntr xd ntr) ("cannot have semi-meta rule \""^ntr^"\" in a subrule relationship") "") nodes0 ; @@ -2479,25 +2504,26 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b (* VV: We do not check that contextrules with the hole filled are of the right type right now, but later when a parser has been constructed. *) - let rec count_holes_element (el:element) : int = + + let rec count_holes_element prod (el:element) : int = match el with | Lang_nonterm _ -> 0 | Lang_terminal "__" -> 1 | Lang_terminal _ -> 0 | Lang_metavar _ -> 0 - | Lang_list elb -> count_holes_elements elb.elb_es + | Lang_list elb -> count_holes_elements prod elb.elb_es | Lang_option _ | Lang_sugaroption _ -> - ty_error + ty_error2 prod.prod_loc ( "count_holes_rule check failed: hole __ found in an" ^ " option or sugaroption form") "" - and count_holes_elements (els:element list) : int = - List.fold_left (+) 0 (List.map count_holes_element els) in + and count_holes_elements prod (els:element list) : int = + List.fold_left (+) 0 (List.map (count_holes_element prod) els) in let count_holes_prod (pl:prod) : unit = - let n = count_holes_elements pl.prod_es in + let n = count_holes_elements pl pl.prod_es in if n <> 1 then - ty_error( "count_holes_rule check failed: hole __ found nonlinearly " + ty_error2 pl.prod_loc ( "count_holes_rule check failed: hole __ found nonlinearly " ^ "(" ^ string_of_int n ^ " times) in production " ^ Auxl.the (Grammar_pp.pp_prod error_opts xd "" "" pl)) "" else () in @@ -2512,7 +2538,7 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b let ctxrule_can_promote_hole ntr = let ntr_p = Auxl.promote_ntr xd (Auxl.primary_ntr_of_ntr xd ntr) in if not (String.compare ntr ntr_p = 0) - then ty_error( "ctxrule_can_promote check failed: the type of hole " + then ty_error2 (Auxl.loc_of_ntr xd ntr) ( "ctxrule_can_promote check failed: the type of hole " ^ ntr ^ " can be promoted to " ^ ntr_p ) "" else () in List.iter (fun cr -> ctxrule_can_promote_hole cr.cr_hole) xd.xd_crs; @@ -2578,7 +2604,7 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b List.iter (fun ntr1 -> let idx1 = vertex_of_ntr ntr1 in List.iter (fun ntr2 -> if ntr2 = ntr1 then - ty_error ("non-terminal " ^ ntr1 ^ " has a non-productive self-loop.") "" + ty_error2 (Auxl.loc_of_ntr xd ntr1) ("non-terminal " ^ ntr1 ^ " has a non-productive self-loop.") "" else G.add_edge g idx1 (vertex_of_ntr ntr2)) tos) @@ -2616,7 +2642,8 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b let (scc_vertex_sets : G.V.t list list) = G.Components.scc_list g in List.iter (fun x -> if List.length x > 1 then - ty_error ("There is a non-productive cycle among the following non-terminals: " ^ ntrs_to_string x) "" + ty_error2 (Auxl.loc_of_ntr xd (ntr_of_vertex (List.hd x))) + ("There is a non-productive cycle among the following non-terminals: " ^ ntrs_to_string x) "" else ()) scc_vertex_sets; @@ -2641,7 +2668,7 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b else ( match Auxl.find_first_duplicate2 (fun (_,s1) -> fun (_,s2) -> (compare s1 s2) = 0 ) (List.rev candidate) with | None -> candidate - | Some s -> ty_error ("duplicated subrule: "^(Auxl.dump_structure_entry s)) "" ) in + | Some s -> ty_error2 (fst s) ("duplicated subrule: "^(Auxl.dump_structure_entry s)) "" ) in let structure_crs = List.map (fun cr -> (cr.cr_loc, (Struct_crs [(cr.cr_ntr, cr.cr_target, cr.cr_hole)]))) @@ -2741,13 +2768,13 @@ let rec check_and_disambiguate m_tex (quotient_rules:bool) (generate_aux_rules:b | (Struct_axs l1,Struct_axs l2) -> Struct_axs (l1@l2) | (Struct_sbs l1,Struct_sbs l2) -> Struct_sbs (l1@l2) | (Struct_fvs l1,Struct_fvs l2) -> Struct_fvs (l1@l2) - | _ -> Auxl.error "internal: collapsing incompatible structure elements.\n" in + | _ -> Auxl.error None "internal: collapsing incompatible structure elements.\n" in let out_c_a current auxfns = match current,auxfns with | None, [] -> [] | Some (l,rsec), [] -> [(l,rsec)] - | None, xs -> Auxl.error "internal: out_c_a, auxfns but undefined current" + | None, xs -> Auxl.error None "internal: out_c_a, auxfns but undefined current" | Some (l,rsec), xs -> (l,rsec)::[(l,Struct_axs xs)] in @@ -2830,7 +2857,7 @@ let check_with_parser (lookup : made_parser) (xd: syntaxdefn) : unit = ( match Context_pp.context_app_rhs error_opts xd lookup (hole,[]) target rl pl with (* FZ think about error_opts and the empty suffix *) | (false, _) -> - ty_error + ty_error2 pl.prod_loc ( "ctxrule check failed: production\n" ^ Auxl.the (Grammar_pp.pp_prod error_opts xd "" "" pl) ^ "\n of rule " ^ ntr diff --git a/src/lex_menhir_pp.ml b/src/lex_menhir_pp.ml index 119920e..3376444 100644 --- a/src/lex_menhir_pp.ml +++ b/src/lex_menhir_pp.ml @@ -255,7 +255,7 @@ let token_names_of_syntaxdefn yo xd : token_data = (try let hs = List.assoc "ocaml" mvd.mvd_rep in Grammar_pp.pp_hom_spec m xd hs - with Not_found -> Auxl.error ("ocamllex output: undefined ocaml hom for "^mvd.mvd_name^"\n")) in + with Not_found -> Auxl.error (Some mvd.mvd_loc) ("ocamllex output: undefined ocaml hom for "^mvd.mvd_name^"\n")) in let ocamllex_hom_opt = (try let hs = List.assoc "ocamllex" mvd.mvd_rep in @@ -270,9 +270,9 @@ let token_names_of_syntaxdefn yo xd : token_data = | Some ocamllex_hom, false -> Some (token_name_of mvd.mvd_name, mvd.mvd_name, TK_metavar(ocaml_type, Some ocamllex_hom)) | None, false -> - Auxl.error ("ocamllex output: no ocamllex or ocamllex-remove hom for "^mvd.mvd_name^"\n") + Auxl.error (Some mvd.mvd_loc) ("ocamllex output: no ocamllex or ocamllex-remove hom for "^mvd.mvd_name^"\n") | Some ocamllex_hom, false -> - Auxl.error ("ocamllex output: both ocamllex and ocamllex-remove hom for "^mvd.mvd_name^"\n") + Auxl.error (Some mvd.mvd_loc) ("ocamllex output: both ocamllex and ocamllex-remove hom for "^mvd.mvd_name^"\n") | None, true -> Some (token_name_of mvd.mvd_name, mvd.mvd_name, TK_metavar(ocaml_type, None)) ) @@ -350,7 +350,7 @@ let pp_lex_systemdefn m sd oi = ; output_string fd "\n\n{\n}\n\n"; close_out fd - | _ -> Auxl.error "must specify only one output file in the lex backend.\n" + | _ -> Auxl.error None "must specify only one output file in the lex backend.\n" (** ******************************************************************** *) @@ -479,7 +479,7 @@ let rec element_data_of_element ts (allow_lists:bool) e : element_data = | (1,None) -> "nonempty_list(" ^ body ^ ")" | (2,Some t) -> "separated_nonempty2_list(" ^ t ^ "," ^ body ^ ")" | (2,None) -> "nonempty2_list(" ^ body ^ ")" - | (_,_) -> Auxl.error ("unexpected length in pp_menhir_element") + | (_,_) -> Auxl.error None ("unexpected length in pp_menhir_element") in let body0 = (match element_data with @@ -652,6 +652,7 @@ let pp_menhir_prod yo generate_aux_info_here xd ts r p = let pp_menhir_hse hse = match hse with | Hom_string s -> s + (* TODO, arbitrary failure? *) | Hom_index i -> let e = List.nth es'' (*or es? *) i in let d=element_data_of_element ts true e in (match d.semantic_action with Some s -> s | None -> raise (Failure ("pp_menhir_hse Hom_index " ^ string_of_int i ^ " at " ^ Location.pp_loc p.prod_loc))) | Hom_terminal s -> s | Hom_ln_free_index (mvs,s) -> raise (Failure "Hom_ln_free_index not implemented") in @@ -686,7 +687,7 @@ let pp_menhir_prod yo generate_aux_info_here xd ts r p = - | None -> ignore(Auxl.error ("no ocaml hom for production "^p.prod_name));"") + | None -> ignore(Auxl.error (Some (r.rule_loc)) ("no ocaml hom for production "^p.prod_name));"") in let aux_wrapper_l, aux_wrapper_r = @@ -803,7 +804,7 @@ let pp_pp_raw_rule yo generate_aux_info xd ts r = (match Auxl.hom_spec_for_hom_name "pp-raw" r.rule_homs with | Some hs -> Some (pp_pp_raw_name r.rule_ntr_name ^ " " ^ Grammar_pp.pp_hom_spec (Menhir yo) xd hs ^"\n\n") - | None -> (Auxl.error ("no pp-raw hom for phantom production "^r.rule_ntr_name)); + | None -> (Auxl.error (Some r.rule_loc) ("no pp-raw hom for phantom production "^r.rule_ntr_name)); ) else let generate_aux_info_here = generate_aux_info_for_rule generate_aux_info r in @@ -845,7 +846,7 @@ let pp_pp_rule yo generate_aux_info xd ts r = (match Auxl.hom_spec_for_hom_name "pp" r.rule_homs with | Some hs -> Some (pp_pp_name r.rule_ntr_name ^ " " ^ Grammar_pp.pp_hom_spec (Menhir yo) xd hs ^"\n\n") - | None -> (Auxl.error ("no pp hom for phantom production "^r.rule_ntr_name)); + | None -> (Auxl.error (Some r.rule_loc) ("no pp hom for phantom production "^r.rule_ntr_name)); ) else let generate_aux_info_here = generate_aux_info_for_rule generate_aux_info r in @@ -914,7 +915,7 @@ let pp_menhir_syntaxdefn m sources _(*xd_quotiented*) xd_unquotiented lookup gen List.iter (function r -> output_string fd (pp_menhir_rule yo generate_aux_info xd_unquotiented ts r)) xd_unquotiented.xd_rs; close_out fd - | _ -> Auxl.error "must specify only one output file in the menhir backend.\n" + | _ -> Auxl.error None "must specify only one output file in the menhir backend.\n" (* output pp source file (should be called with quotiented syntaxdefn file) *) let pp_pp_syntaxdefn m sources xd_quotiented xd_unquotiented xd_quotiented_unaux generate_aux_info oi = @@ -938,5 +939,5 @@ let pp_pp_syntaxdefn m sources xd_quotiented xd_unquotiented xd_quotiented_unaux ); close_out fd; - | _ -> Auxl.error "must specify only one output file in the menhir backend.\n" + | _ -> Auxl.error None "must specify only one output file in the menhir backend.\n" diff --git a/src/ln_transform.ml b/src/ln_transform.ml index 462f01c..a9c04d0 100644 --- a/src/ln_transform.ml +++ b/src/ln_transform.ml @@ -58,7 +58,7 @@ let rec collect_mv_in_mse mse = match mse with | MetaVarExp mv -> [mv] | Union (mse1,mse2) -> (collect_mv_in_mse mse1) @ (collect_mv_in_mse mse2) - | _ -> Auxl.warning "internal: collect ln bindspec not implemented\n"; [] + | _ -> Auxl.warning None "internal: collect ln bindspec not implemented\n"; [] (* LIBRARY *) @@ -95,9 +95,9 @@ let binders p = ( fun bs -> (* print_endline (Grammar_pp.pp_plain_bindspec bs); *) match bs with - | Bind (MetaVarExp mv,_) -> Some [mv] - | AuxFnDef (_,mse) -> Some (collect_mv_in_mse mse) - | Bind _ -> Auxl.warning "internal: binders not implemented - 1\n"; None + | Bind (loc,MetaVarExp mv,_) -> Some [mv] + | AuxFnDef (loc,_,mse) -> Some (collect_mv_in_mse mse) + | Bind _ -> Auxl.warning None "internal: binders not implemented - 1\n"; None | _ -> None ) p.prod_bs) @@ -107,9 +107,9 @@ let binders_for_nt p nt = ( fun bs -> (* print_endline (Grammar_pp.pp_plain_bindspec bs); *) match bs with - | Bind (MetaVarExp mv,nt1) when compare nt nt1 = 0 -> Some [mv] - | Bind (MetaVarExp mv,nt1) when not (compare nt nt1 = 0) -> None - | Bind _ -> Auxl.warning "internal: binders not implemented - 2\n"; None + | Bind (loc,MetaVarExp mv,nt1) when compare nt nt1 = 0 -> Some [mv] + | Bind (loc,MetaVarExp mv,nt1) when not (compare nt nt1 = 0) -> None + | Bind _ -> Auxl.warning None "internal: binders not implemented - 2\n"; None | _ -> None ) p.prod_bs) @@ -125,7 +125,7 @@ let is_bindable xd mv p = (* for a ln mvr, record the rules where it has been splitted *) let rules_with_bindable_mvr (xd:syntaxdefn) (mvr:metavarroot) : rule list = - if not((Auxl.mvd_of_mvr xd mvr).mvd_locally_nameless) then Auxl.error ("internal: rules_with_bindable_mvr: "^mvr^" does not have a ln repr.\n"); + if not((Auxl.mvd_of_mvr xd mvr).mvd_locally_nameless) then Auxl.error (Some (Auxl.loc_of_mvr xd mvr)) ("internal: rules_with_bindable_mvr: "^mvr^" does not have a ln repr.\n"); List.filter (fun r -> (not r.rule_meta) && @@ -199,21 +199,21 @@ let check_single_binder xd = let one_bind = ref false in List.iter (fun bs -> match bs with - | AuxFnDef _ -> - Auxl.warning "locally-nameless: auxfns are not supported by the locally-nameless backend\n" - | Bind (NonTermExp _,_) -> - Auxl.warning "locally-nameless: bindspec binding a nonterminal are not supported by the locally-nameless backend\n" - | Bind (MetaVarListExp _,_) -> - Auxl.warning "locally-nameless: bindspec binding a list of metavars are not supported by the locally-nameless backend\n" - | Bind (NonTermListExp _,_) -> - Auxl.warning "locally-nameless: bindspec binding a list of nonterminals are not supported by the locally-nameless backend\n" - | Bind (MetaVarExp mv,_) -> + | AuxFnDef (loc,_,_) -> + Auxl.warning (Some loc) "locally-nameless: auxfns are not supported by the locally-nameless backend\n" + | Bind (loc,NonTermExp _,_) -> + Auxl.warning (Some loc) "locally-nameless: bindspec binding a nonterminal are not supported by the locally-nameless backend\n" + | Bind (loc,MetaVarListExp _,_) -> + Auxl.warning (Some loc) "locally-nameless: bindspec binding a list of metavars are not supported by the locally-nameless backend\n" + | Bind (loc,NonTermListExp _,_) -> + Auxl.warning (Some loc) "locally-nameless: bindspec binding a list of nonterminals are not supported by the locally-nameless backend\n" + | Bind (loc,MetaVarExp mv,_) -> (* check if mv has a locally nameless representation *) let mvd = Auxl.mvd_of_mvr xd (Auxl.primary_mvr_of_mvr xd (fst mv)) in if mvd.mvd_locally_nameless then if !one_bind then - Auxl.warning "locally-nameless: multiple bind declaration on the same production are not supported by the locally-nameless backend\n" + Auxl.warning (Some mvd.mvd_loc) "locally-nameless: multiple bind declaration on the same production are not supported by the locally-nameless backend\n" else one_bind := true else () | _ -> ()) @@ -682,14 +682,14 @@ let pp_open_prod m xd mvr wrt (ov:string) (rule_ntr_name:nontermroot) (p:prod) : let mv1_s = Grammar_pp.pp_metavar_with_de_with_sie m xd sie de mv1 in let mv2_s = Grammar_pp.pp_metavar_with_de_with_sie m xd sie de mv2 in ( "if (k === "^mv1_s^") then (List.nth "^mv2_s^" "^ov^" "^"("^p.prod_name^" 0 0)"^") else (" ^ s^ " "^mv1_s^" "^mv2_s^")" , [] ) - | _ -> Auxl.error "internal: weird lhs_stnb in pp_open_prod\n" ) + | _ -> Auxl.error (Some (lhs_stnb.st_loc)) "internal: weird lhs_stnb in pp_open_prod\n" ) else ( let unshifted_nonterms = Auxl.option_map ( fun bs -> match bs with - | Bind (MetaVarExp (mvr1,_),nt) -> + | Bind (loc, MetaVarExp (mvr1,_),nt) -> let mvr1 = Auxl.primary_mvr_of_mvr xd mvr1 in if (String.compare mvr mvr1 = 0) then Some nt else None | _ -> None ) @@ -778,7 +778,7 @@ let pp_open m xd : int_funcs_collapsed = { i_funcs = ifuncs; i_funcs_proof = None } - | _ -> Auxl.warning "internal: pp_open implemented only for Coq\n"; [] + | _ -> Auxl.warning None "internal: pp_open implemented only for Coq\n"; [] (* ******************************************************************** *) (* lc (locally closed) *) @@ -849,7 +849,7 @@ let pp_lcs fd m xd : unit = ("lcs, rule "^r.rule_ntr_name^", binders in prod " ^ p.prod_name^ " for ntr "^ntr ^ " = "^String.concat " , " (List.map Grammar_pp.pp_plain_metavar mvs)); - if List.length mvs > 1 then Auxl.error "locally_nameless - not implemented: several mvs bind the same nt\n"; + if List.length mvs > 1 then Auxl.error None "locally_nameless - not implemented: several mvs bind the same nt\n"; if List.length mvs = 1 (* build premise with cofinite quantification *) @@ -870,7 +870,7 @@ let pp_lcs fd m xd : unit = in p.prod_name with Not_found -> - Auxl.error ("internal: lns, make_premises, cannot find singleton production for " + Auxl.error (Some r.rule_loc) ("internal: lns, make_premises, cannot find singleton production for " ^ (fst (List.hd mvs)) ^ " starting from rule " ^ r.rule_ntr_name ^ "\n") in let st_rule_name_s = @@ -1050,7 +1050,7 @@ let pp_arity_prod m xd_transformed f ntr p = (Auxl.option_map ( fun bs -> match bs with - | AuxFnDef (f',mse) when String.compare f f' = 0 -> Some mse + | AuxFnDef (loc,f',mse) when String.compare f f' = 0 -> Some mse | _ -> None ) p.prod_bs) in let rec mse_to_rhs mse = @@ -1163,14 +1163,14 @@ let build_open_symterm m xd open_wrt st = match st with | St_nonterm (_,ntr,_) -> Auxl.primary_ntr_of_ntr xd ntr | St_nontermsub (_,_,ntr,_) -> Auxl.primary_ntr_of_ntr xd ntr - | _ -> Auxl.error "internal: build_open_symterm, not a nonterm\n" in + | _ -> Auxl.error (Some (Auxl.loc_of_symterm st)) "internal: build_open_symterm, not a nonterm\n" in let r = Auxl.rule_of_ntr xd ntr in let find_var_prod mv = let mv1 = match mv with | Ste_metavar (_,mv1,_) -> mv1 | Ste_var (_,mv1,_) -> mv1 - | _ -> Auxl.error "internal: find_var_prod ln not ste_metavar\n" in + | _ -> Auxl.error (Some (Auxl.loc_of_symterm st)) "internal: find_var_prod ln not ste_metavar\n" in let p = List.find ( fun p -> match p.prod_es with @@ -1187,7 +1187,7 @@ let build_open_symterm m xd open_wrt st = match mv with | Ste_metavar (_,mv1,_) -> mv1 | Ste_var (_,mv1,_) -> mv1 - | _ -> Auxl.error "internal: find_var_prod ln not ste_metavar\n" in + | _ -> Auxl.error (Some (Auxl.loc_of_symterm_element mv)) "internal: find_var_prod ln not ste_metavar\n" in let r = List.find (fun r -> @@ -1351,7 +1351,7 @@ let ln_transform_symterms (m:pp_mode) (xd:syntaxdefn) (stlp:(string option * sym then None else Some (Ste_var (l,mvrp,var)) | (Ste_list (l,stlis),_) -> - (* Auxl.warning "internal: remove_binders_symterm_element ste_list not implemented\n"; *) + (* Auxl.warning None "internal: remove_binders_symterm_element ste_list not implemented\n"; *) Some (Ste_list (l,stlis)) (* FZ *) in @@ -1367,7 +1367,7 @@ let ln_transform_symterms (m:pp_mode) (xd:syntaxdefn) (stlp:(string option * sym Auxl.option_map ( fun bs -> match bs with - | Bind (MetaVarExp mv, nt) -> + | Bind (loc,MetaVarExp mv, nt) -> let mvo = List.nth stnb.st_es (find_occurrence_mv p.prod_es 0 mv) in let o = find_occurrence_nt nt p.prod_es 1 in Some (mvo,nt,o,(St_node (l,stnb))) @@ -1457,7 +1457,7 @@ let ln_transform_symterms (m:pp_mode) (xd:syntaxdefn) (stlp:(string option * sym ( fun ste -> match ste with | Ste_metavar (_,mvr,mv) -> (ste,(Ste_var (dummy_loc,mvr, ((*"TX_"^*)(Grammar_pp.pp_plain_metavar mv))))) - | _ -> Auxl.error "internal: nt_longest" ) + | _ -> Auxl.error (Some (Auxl.loc_of_symterm_element ste)) "internal: nt_longest" ) stel )) nt_longest in @@ -1483,7 +1483,7 @@ let ln_transform_symterms (m:pp_mode) (xd:syntaxdefn) (stlp:(string option * sym Auxl.option_map ( fun bs -> match bs with - | Bind (MetaVarExp mv, nt) -> + | Bind (loc,MetaVarExp mv, nt) -> let mvo = List.nth stnb.st_es (find_occurrence_mv p.prod_es 0 mv) in let o = find_occurrence_nt nt p.prod_es 1 in Some (mvo,nt,o) @@ -1518,9 +1518,10 @@ let ln_transform_symterms (m:pp_mode) (xd:syntaxdefn) (stlp:(string option * sym let current_str = List.map Grammar_pp.pp_plain_symterm_element current_binding in List.iter - (fun str -> if List.mem str current_str - then Auxl.error ("locally-nameless: a rule definition contains a repeated binder: "^str^";\n try alpha-converting one of the occurrences.\n")) - (List.map Grammar_pp.pp_plain_symterm_element extra_binders); + (fun ste -> let str = Grammar_pp.pp_plain_symterm_element ste in + if List.mem str current_str + then Auxl.error (Some (Auxl.loc_of_symterm_element ste)) ("locally-nameless: a rule definition contains a repeated binder: "^str^";\n try alpha-converting one of the occurrences.\n")) + extra_binders; let binders = (* print_endline ("removed = " ^ String.concat " " (List.map Grammar_pp.pp_plain_symterm_element removed_binders)); *) @@ -1577,7 +1578,8 @@ let ln_transform_symterms (m:pp_mode) (xd:syntaxdefn) (stlp:(string option * sym match mvsr with | [] -> st | mv::tl -> - let mvr = match mv with Ste_metavar (_,mvr,_) -> mvr | Ste_var (_,mvr,_) -> mvr | _ -> Auxl.error "internal: cofinite quantify not metavar" in + let mvr = match mv with Ste_metavar (_,mvr,_) -> mvr | Ste_var (_,mvr,_) -> mvr | _ -> + Auxl.error (Some (Auxl.loc_of_symterm st) ) "internal: cofinite quantify not metavar" in let cq_st = St_node ( dummy_loc, { st_rule_ntr_name = "formula"; @@ -1637,7 +1639,7 @@ let ln_transform_defn m xd d = List.map (fun psr -> match psr with | PSR_Rule dr -> PSR_Rule (ln_transform_drule m xd dr) - | PSR_Defncom _ -> Auxl.error "internal: ln transform defncom not implemented" ) + | PSR_Defncom _ -> Auxl.error None "internal: ln transform defncom not implemented" ) d.d_rules } let ln_transform_reln_defnclass m xd dc = @@ -1648,7 +1650,7 @@ let ln_transform_fun_or_reln_defnclass_list m (xd:syntaxdefn) (frdcs:fun_or_reln_defnclass list) : fun_or_reln_defnclass list = List.map ( fun frdc -> match frdc with - | FDC fdc -> Auxl.error "internal: fdc transform not implemented" + | FDC fdc -> Auxl.error None "internal: fdc transform not implemented" | RDC dc -> RDC (ln_transform_reln_defnclass m xd dc) ) frdcs diff --git a/src/location.ml b/src/location.ml index f51d9a8..68be775 100644 --- a/src/location.ml +++ b/src/location.ml @@ -50,7 +50,10 @@ let loc_of_filename name len = Lexing.pos_cnum =len } } ] -let pp_position +(* We don't use these anymore, +since all errors/warnings should be converting +their positiosn into locations *) +(* let pp_position { Lexing.pos_fname = f; Lexing.pos_lnum = l; Lexing.pos_bol = b; @@ -58,23 +61,23 @@ let pp_position "fname=" ^ f ^ " lnum=" ^ string_of_int l ^ " bol="^string_of_int b^" cnum=" ^string_of_int c -let pp_position2 +let pp_position2' { Lexing.pos_fname = f; Lexing.pos_lnum = l; Lexing.pos_bol = b; Lexing.pos_cnum = c } = (if f="" then "" else "file=" ^ f ^ " ") - ^ "line=" ^ string_of_int l ^ " char=" ^ string_of_int (c-b) + ^ "line=" ^ string_of_int l ^ " char=" ^ string_of_int (c-b) *) let pp_t {loc_start=ls;loc_end=le} = if ls.Lexing.pos_fname = le.Lexing.pos_fname && ls.Lexing.pos_lnum = le.Lexing.pos_lnum then (* start and end are in the same file and line *) - (if ls.Lexing.pos_fname="" then "" else "file " ^ ls.Lexing.pos_fname ^ " ") + (if ls.Lexing.pos_fname="" then "" else "File " ^ ls.Lexing.pos_fname ^ " on ") ^ "line " ^ string_of_int ls.Lexing.pos_lnum - ^ " char " + ^ ", column " ^ string_of_int (ls.Lexing.pos_cnum - ls.Lexing.pos_bol) ^ " - " ^ string_of_int (le.Lexing.pos_cnum - le.Lexing.pos_bol) @@ -83,22 +86,22 @@ let pp_t {loc_start=ls;loc_end=le} = && le.Lexing.pos_cnum - le.Lexing.pos_bol = 0 then (* start and end are in the same file but different lines, at the starts of those lines *) - (if ls.Lexing.pos_fname="" then "" else "file " ^ ls.Lexing.pos_fname ^ " ") + (if ls.Lexing.pos_fname="" then "" else "File " ^ ls.Lexing.pos_fname ^ " on ") ^ "line " ^ string_of_int ls.Lexing.pos_lnum ^ " - " ^ string_of_int le.Lexing.pos_lnum else (* start and end are in the same file but different lines, at some non-start chars *) - (if ls.Lexing.pos_fname="" then "" else "file " ^ ls.Lexing.pos_fname ^ " ") + (if ls.Lexing.pos_fname="" then "" else "File " ^ ls.Lexing.pos_fname ^ " on ") ^ "line " ^ string_of_int ls.Lexing.pos_lnum - ^ " char " + ^ ", column " ^ string_of_int (ls.Lexing.pos_cnum - ls.Lexing.pos_bol) ^ " - " ^ "line " ^ string_of_int le.Lexing.pos_lnum - ^ " char " + ^ ", column " ^ string_of_int (le.Lexing.pos_cnum - le.Lexing.pos_bol) @@ -126,7 +129,7 @@ let dummy_t = { loc_start=dummy_pos; loc_end=dummy_pos } -let pp_loc l = String.concat " " ((List.map pp_t) l) +let pp_loc l = String.concat " ; " ((List.map pp_t) l) let pos_plus_offset pos n = {pos with Lexing.pos_bol = pos.Lexing.pos_bol + n; diff --git a/src/main.ml b/src/main.ml index 99f2cf7..beb37c6 100644 --- a/src/main.ml +++ b/src/main.ml @@ -108,13 +108,13 @@ let options = Arg.align [ Arg.String (fun s -> match !write_systemdefn_filename_opt with | None -> write_systemdefn_filename_opt := Some s - | Some _ -> Auxl.error "\nError: multiple -writesys not suppported\n"), + | Some _ -> Auxl.error None "\nError: multiple -writesys not suppported\n"), " Output system definition" ); ( "-readsys", Arg.String (fun s -> match !read_systemdefn_filename_opt with | None -> read_systemdefn_filename_opt := Some s - | Some _ -> Auxl.error "\nError: multiple -readsys not suppported\n"), + | Some _ -> Auxl.error None "\nError: multiple -readsys not suppported\n"), " Input system definition" ); (* filter filenames *) @@ -179,7 +179,7 @@ let options = Arg.align [ (* options for ascii output *) ( "-colour", - Arg.Bool (fun b -> colour := b), + Arg.Bool (fun b -> Auxl.colour := b; colour := b), "<"^string_of_bool !colour ^"> Use (vt220) colour for ASCII pretty print" ); ( "-show_sort", Arg.Bool (fun b -> show_sort := b), @@ -295,7 +295,7 @@ let _ = Arg.parse options (fun s -> if !i_arguments - then Auxl.error "\nError: must either use -i or specify filenames at the end\n" + then Auxl.error None "\nError: must either use -i or specify filenames at the end\n" else extra_arguments := (In,s) ::(!extra_arguments)) usage_msg; file_arguments := !file_arguments @ !extra_arguments @@ -343,14 +343,14 @@ let classify_file_argument arg = (match file_type name with | Some e when (List.mem e input_types) -> (In,e,name) - | _ -> Auxl.error + | _ -> Auxl.error None ("\nError: unrecognised extension of input file \""^name ^ "\" (must be one of " ^ String.concat "," (List.map extension_of_type input_types) ^")\n")) | (Out,name) -> (match file_type name with | Some e when (List.mem e output_types) -> (Out,e,name) - | _ -> Auxl.error + | _ -> Auxl.error None ("\nError: unrecognised extension of output file \""^name ^ "\" (must be one of "^String.concat "," (List.map extension_of_type output_types) ^")\n")) @@ -446,7 +446,7 @@ let target_ocaml_ast_module = all_file_arguments in match target_ocaml_filenames with | [n] -> String.capitalize (Filename.chop_extension n) - | _ -> Auxl.error "\n if there is a menhir output file, there must be exactly one ocaml output file" + | _ -> Auxl.error None "\n if there is a menhir output file, there must be exactly one ocaml output file" else "" @@ -465,7 +465,7 @@ let target_ocaml_parser_module = all_file_arguments in match target_menhir_filenames with | [n] -> String.capitalize (Filename.chop_extension n) - | _ -> Auxl.error "\n if there is an ocamllex output file, there must be exactly one menhir output file" + | _ -> Auxl.error None "\n if there is an ocamllex output file, there must be exactly one menhir output file" else "" @@ -526,7 +526,7 @@ let process source_filenames = (match !alltt_filename_opt,source_filenames with | None,_ -> () | Some alltt_filename,([] | _::_::_) -> - Auxl.error ("\nUsage: -alltt option can only be used with exactly one source file at a time\n"); + Auxl.error None ("\nUsage: -alltt option can only be used with exactly one source file at a time\n"); | Some alltt_filename,[(source_filetype,source_filename)] -> let c = open_in source_filename in let c' = open_out alltt_filename in @@ -544,9 +544,8 @@ let process source_filenames = output_string c' (Grammar_lexer.de_lex_tex t); flush c'; process_input () with - My_parse_error s-> - (* Auxl.error ("\n"^s^" in file: "^filter_filename^"\n") in*) - Auxl.error ("\n"^s^"\n") in + My_parse_error (loc, s)-> + Auxl.error loc (s) in process_input (); output_string c' "\\end{alltt}\n"; let _ = close_in c in @@ -564,9 +563,9 @@ let process source_filenames = (try Grammar_parser.main (Grammar_lexer.my_lexer true Grammar_lexer.metalang) lexbuf with - My_parse_error s-> + My_parse_error (loc,s)-> (* Auxl.error ("\n"^s^" in file: "^filter_filename^"\n") in*) - Auxl.error ("\n"^s^"\n")) in + Auxl.error loc ("\n"^s^"\n")) in let _ = close_in c in ris | _ -> @@ -605,8 +604,8 @@ let process source_filenames = try Grammar_typecheck.check_and_disambiguate m_tex quotient generate_aux targets_non_tex (List.map snd source_filenames) (!merge_fragments) document with - | Typecheck_error (s1,s2) -> - Auxl.error ("(in checking and disambiguating "^(if quotient then "quotiented " else "") ^ "syntax)\n"^s1 + | Typecheck_error (loc,s1,s2) -> + Auxl.error (Some loc) ("(in checking and disambiguating "^(if quotient then "quotiented " else "") ^ "syntax)\n"^s1 ^ (if s2<>"" then " ("^s2^")" else "") ^ "\n") in @@ -642,8 +641,8 @@ let process source_filenames = begin try Grammar_typecheck.check_with_parser lookup xd with - | Typecheck_error (s1,s2) -> - Auxl.error ("(in checking syntax)\n"^s1 + | Typecheck_error (loc,s1,s2) -> + Auxl.error (Some loc) ("(in checking syntax)\n"^s1 ^ (if s2<>"" then " ("^s2^")\n" else "\n")) end; @@ -659,8 +658,10 @@ let process source_filenames = sources = sources} in sd with - | Bounds.Bounds s | Defns.Rule_parse_error s | Typecheck_error (s,_)-> - Auxl.error ("\nError in processing definitions:\n"^s^"\n") + | Defns.Rule_parse_error (loc,s) -> + Auxl.error (Some loc) ("\nError in processing definitions:\n"^s^"\n") + | Bounds.Bounds (loc,s) | Typecheck_error (loc,s,_)-> + Auxl.error (Some loc) ("\nError in processing definitions:\n"^s^"\n") ) else (print_endline "********** NOT PROCESSING DEFINITIONS *************\n"; flush stdout; @@ -684,7 +685,7 @@ let read_systemdefn read_systemdefn_filename = let fd = open_in_bin read_systemdefn_filename in let sd,lookup ,sd_unquotiented, sd_quotiented_unaux = try Marshal.from_channel fd - with Failure s -> Auxl.error ("Cannot read dumped systemdefn\n " ^ s ^"\n") + with Failure s -> Auxl.error None ("Cannot read dumped systemdefn\n " ^ s ^"\n") in close_in fd; sd,lookup,sd_unquotiented,sd_quotiented_unaux @@ -730,7 +731,7 @@ let output_stage (sd,lookup,sd_unquotiented,sd_quotiented_unaux) = | [] -> [] | (In,ft,fn)::xs -> compute_output (fn::ib) xs | (Out,ft,fn)::xs -> ( - if ib = [] then Auxl.warning ("warning: no input files for the output file: "^fn^".\n"); + if ib = [] then Auxl.warning None ("warning: no input files for the output file: "^fn^".\n"); (fn,ib)::(compute_output [] xs)) in List.map (fun (t,fs) -> t, compute_output [] fs) sources_per_target @@ -749,7 +750,7 @@ let output_stage (sd,lookup,sd_unquotiented,sd_quotiented_unaux) = | 0 -> sd | 1 -> Auxl.avoid_primaries_systemdefn false sd | 2 -> Auxl.avoid_primaries_systemdefn true sd - | _ -> Auxl.error "coq type-name avoidance must be in {0,1,2}" ) in + | _ -> Auxl.error None "coq type-name avoidance must be in {0,1,2}" ) in System_pp.pp_systemdefn_core_io m_coq sd lookup fi !merge_fragments | "isa" -> System_pp.pp_systemdefn_core_io m_isa sd lookup fi !merge_fragments @@ -813,8 +814,8 @@ let output_stage (sd,lookup,sd_unquotiented,sd_quotiented_unaux) = Grammar_parser.unfiltered_spec_el_list (Grammar_lexer.my_lexer true Grammar_lexer.filter) lexbuf with | Parsing.Parse_error -> - Auxl.error ("unfiltered document "^src_filename^" cannot be parsed\n") - | My_parse_error s -> Auxl.error s + Auxl.error None ("unfiltered document "^src_filename^" cannot be parsed\n") + | My_parse_error (loc,s) -> Auxl.error loc s in Embed_pp.pp_embed_spec fd_dst m sd.syntax lookup (Auxl.collapse_embed_spec_el_list unfiltered_document); let _ = close_in fd_src in @@ -845,7 +846,7 @@ let _ = Gc.minor_heap_size = 2*1024*1024 (* 8/16 MB in 32/64bit machines *); Gc.major_heap_increment = 5*1024*1024 (* 40/80 MB in 32/64bit machines *)};; -let _ = match source_filenames, !read_systemdefn_filename_opt with +let _ = try ( match source_filenames, !read_systemdefn_filename_opt with | (_::_),None -> let (sd,lookup,sd_unquotiented,sd_quotiented_unaux) = process source_filenames in output_stage (sd,lookup,sd_unquotiented,sd_quotiented_unaux) @@ -854,5 +855,8 @@ let _ = match source_filenames, !read_systemdefn_filename_opt with output_stage (sd,lookup,sd_unquotiented,sd_quotiented_unaux) | [],None -> Arg.usage options usage_msg; - Auxl.error "\nError: must specify either some source filenames or a readsys option\n" -| (_::_),Some _ -> Auxl.error "\nError: must not specify both source filenames and a readsys option\n" + Auxl.error None "\nError: must specify either some source filenames or a readsys option\n" +| (_::_),Some _ -> Auxl.error None "\nError: must not specify both source filenames and a readsys option\n" + + ) with + | Auxl.Located_Failure (l, s) -> Auxl.exit_with l s diff --git a/src/new_term_parser.ml b/src/new_term_parser.ml index 00a1be7..c8219cb 100644 --- a/src/new_term_parser.ml +++ b/src/new_term_parser.ml @@ -901,7 +901,7 @@ let build_grammar (xd : syntaxdefn) end; List.iter - (fun (pn1, annot, pn2) -> + (fun (pn1, annot, pn2, loc) -> let (i1, i1') = Hashtbl.find prodname_to_index2 pn1 in let (i2, i2') = Hashtbl.find prodname_to_index2 pn2 in let entry = diff --git a/src/subrules_pp.ml b/src/subrules_pp.ml index 96a3e0e..002ccec 100644 --- a/src/subrules_pp.ml +++ b/src/subrules_pp.ml @@ -488,7 +488,7 @@ let pp_subrules m xd srs : int_funcs_collapsed = ( Auxl.pp_is srl sru ^ " : " ^ Grammar_pp.pp_nontermroot_ty m xd sru ^ " -> type.\n", "","") - | Tex _ | Ascii _ | Lex _ | Menhir _ -> Auxl.error "pp_subprod" + | Tex _ | Ascii _ | Lex _ | Menhir _ -> Auxl.error (Some (Auxl.loc_of_ntr xd srl)) "pp_subprod" ) in diff --git a/src/substs_pp.ml b/src/substs_pp.ml index 9507f1b..537d481 100644 --- a/src/substs_pp.ml +++ b/src/substs_pp.ml @@ -245,7 +245,7 @@ let auxfn_usages (bs : bindspec list) : (auxfn * nonterm) list = let all_binding_mses = Auxl.option_map (function b -> match b with - | Bind(mse,nt) -> Some(mse) + | Bind(loc,mse,nt) -> Some(mse) | _ -> None) bs in Auxl.remove_duplicates @@ -286,7 +286,7 @@ let pp_auxfn_clauses m xd f ntr ntmvr = Auxl.option_map ( fun b -> match b with - | AuxFnDef(f',mse) when f'=f -> Some mse + | AuxFnDef(loc,f',mse) when f'=f -> Some mse | _ -> None ) p.prod_bs with | [mse] -> mse @@ -456,7 +456,7 @@ let glommed_bound_things_for_nonterm let relevant_bind_clauses_around_this_nonterm : (mse * nonterm) list = Auxl.option_map (function b -> match b with - | Bind(mse',nt') -> + | Bind(loc,mse',nt') -> if nt'=nt && Auxl.result_type_of_mse xd mse'= that_var_root then Some (mse',nt) else None @@ -492,7 +492,7 @@ let glommed_bound_things_for_nonterm | Empty -> false in List.exists (function bs -> match bs with - | Bind (mse'',nt'') -> nt_occurs mse'' + | Bind (loc,mse'',nt'') -> nt_occurs mse'' | _ -> false) (p.prod_bs) in @@ -533,7 +533,7 @@ let directly_binding_usages_of_this_metavar | Empty -> false in List.exists (function bs -> match bs with - | Bind (mse'',nt'') -> mv_occurs mse'' + | Bind (loc,mse'',nt'') -> mv_occurs mse'' | _ -> false) (p.prod_bs) @@ -1435,7 +1435,7 @@ let pp_subst_rule : subst -> pp_mode -> syntaxdefn -> nontermroot list -> rule - ^ Grammar_pp.pp_nontermroot_ty m xd r.rule_ntr_name ^ " -> " ^ Grammar_pp.pp_nontermroot_ty m xd r.rule_ntr_name ^ " -> type.\n") ) , "", "") - | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.error "pp_subst_rule") + | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.error (Some r.rule_loc) "pp_subst_rule") in @@ -1745,7 +1745,7 @@ and pp_fv_symterm_list_body | _ -> Some "[]"), funcs | _ -> ( match m with - | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.error "pp_fv_symterm_list_body" + | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.error (Some p.prod_loc) "pp_fv_symterm_list_body" | Isa io when io.ppi_isa_primrec -> let args = String.concat "_" diff --git a/src/system_pp.ml b/src/system_pp.ml index 9813e85..96cbc57 100644 --- a/src/system_pp.ml +++ b/src/system_pp.ml @@ -110,7 +110,8 @@ let pp_functions_locally_nameless fd m sd xd_transformed = let set_locally_nameless m = match m with | Coq co -> co.coq_locally_nameless := true - | _ -> Auxl.error "locally-nameless: only the Coq backend understand {{ repr-locally-nameless }}.\n" + (* TODO *) + | _ -> Auxl.error None "locally-nameless: only the Coq backend understand {{ repr-locally-nameless }}.\n" let pp_systemdefn_core_locally_nameless fd m sd lookup = set_locally_nameless m; @@ -427,7 +428,7 @@ let pp_systemdefn_core_io m sd lookup oi merge_fragments = if merge_fragments then begin let o = match oi with (o,is)::[] -> o - | _ -> Auxl.error "must specify only one output file .\n" in + | _ -> Auxl.error None "must specify only one output file .\n" in let fn = Auxl.filename_check m o in let fd = open_out o in pp_systemdefn fd m sd lookup fn; @@ -450,7 +451,7 @@ let pp_systemdefn_core_io m sd lookup oi merge_fragments = | false -> ["Bool"; "Metatheory"; "List"; "Ott.ott_list_core"]); pp_systemdefn_core_locally_nameless fd m sd lookup; close_out fd - | _ -> Auxl.error "must specify only one output file in the Coq locally-nameless backend.\n" ) + | _ -> Auxl.error None "must specify only one output file in the Coq locally-nameless backend.\n" ) else begin @@ -554,7 +555,7 @@ let is_wrap_pre (l,hn,es) = if hn = "tex-wrap-pre" then Some (l,"tex",es) else N let is_wrap_post (l,hn,es) = if hn = "tex-wrap-post" then Some (l,"tex",es) else None let pp_systemdefn_core_tex m sd lookup oi = - let xo = match m with | Tex xo -> xo | _ -> Auxl.error "internal: pp_systemdefn_core_tex on non-tex pp_mode\n" in + let xo = match m with | Tex xo -> xo | _ -> Auxl.error None "internal: pp_systemdefn_core_tex on non-tex pp_mode\n" in match oi with | (o,is)::[] -> let fd = open_out o in @@ -623,6 +624,5 @@ let pp_systemdefn_core_tex m sd lookup oi = | post_wrap -> Embed_pp.pp_embeds fd m sd.syntax lookup post_wrap end; close_out fd; - - | _ -> Auxl.error "must specify only one output file in the TeX backend.\n" + | _ -> Auxl.error None "must specify only one output file in the TeX backend.\n" diff --git a/src/term_parser.ml b/src/term_parser.ml index 8277f4d..6c2d407 100644 --- a/src/term_parser.ml +++ b/src/term_parser.ml @@ -28,7 +28,7 @@ (* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *) (* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *) (* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *) -(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMGE. *) (**************************************************************************) (* @@ -37,6 +37,8 @@ rules, ie with metavars and nonterms, as well as object-level vars). *) open Types;; +open Auxl;; +open String;; exception ThisCannotHappen;; exception Parse_error of loc * string;; @@ -452,7 +454,7 @@ let parse_dots_with_length_constraint length_constraint = | None | Some 0 -> f ["..";"...";"...."] | Some 1 -> f ["...";"...."] | Some 2 -> f ["...."] - | _ -> Auxl.error "internal: parse_dots with length_constraint > 2" + | _ -> Auxl.error None "internal: parse_dots with length_constraint > 2" let parse_dots_without_length_constraint = let f ds = parse_map (function s -> String.length s - 2) @@ -1134,13 +1136,15 @@ about multiple parses *) let just_one_parse ?(transform : symterm list -> symterm list = user_syntax_transform) (xd: syntaxdefn) (lookup: made_parser) (ntr: nontermroot) (concrete: bool) (l: loc) (s: string): symterm = + let Ascii oldopts = pp_ascii_opts_default in + let opts = Ascii {oldopts with ppa_colour = !Auxl.colour} in let sts = parse_complete lookup ntr concrete s in let sts = transform sts in match sts with [st] -> st | [] -> let error_str = no_parses_error_string s in - Format.printf "\nno parses of \"%s\" at %s:\n%s\n" s (Location.pp_loc l) error_str; + report_error (Some l) (Format.sprintf "no parses of \"%s\":\n%s\n" s error_str); St_uninterpreted (l, error_str) | hs::ts -> if @@ -1152,16 +1156,20 @@ let just_one_parse ?(transform : symterm list -> symterm list = user_syntax_tran List.for_all (fun st -> s = (Grammar_pp.pp_symterm pp_mode xd [] de_empty st)) ts) pp_list then hs - else begin - Format.printf "\nmultiple parses of \"%s\" at %s:\n" s (Location.pp_loc l); - List.iter - (fun st -> - Format.printf "%s\n or plain:%s\n" - (Grammar_pp.pp_symterm pp_ascii_opts_default xd [] de_empty st) - (Grammar_pp.pp_plain_symterm st)) - sts; - St_uninterpreted(l, "multiple parses") - end + else + let + sstart = Format.sprintf "multiple parses of \"%s\":\n" s + and intermed : string list = (List.map + (fun st -> + Format.sprintf "%s\n or plain:%s\n" + (Grammar_pp.pp_symterm opts xd [] de_empty st) + (Grammar_pp.pp_plain_symterm st)) + sts) + in + begin + report_error (Some l) (sstart ^ concat "" intermed); + St_uninterpreted(l, "multiple parses") + end (*----------------------------------------------------------------------------*) (** {2 Make parser} *) diff --git a/src/transform.ml b/src/transform.ml index 6d7c84f..fbf123c 100644 --- a/src/transform.ml +++ b/src/transform.ml @@ -124,7 +124,7 @@ let expand_element (m:pp_mode) (xd:syntaxdefn) (bs:bindspec list) (e:element) : | Lang_nonterm (ntr,_) -> Some (Ntr (Auxl.promote_ntr xd ntr)) | Lang_metavar (mvr,_) -> Some (Mvr mvr) | Lang_terminal t -> None - | _ -> Auxl.error "internal: expand element, cannot happen.\n" ) + | _ -> Auxl.error None "internal: expand element, cannot happen.\n" ) elb.elb_es in let id = (*Auxl.pp_coq_type_name*) @@ -151,32 +151,32 @@ let expand_element (m:pp_mode) (xd:syntaxdefn) (bs:bindspec list) (e:element) : let rec update_bs bs ss = ( match bs with - | AuxFnDef (f,AuxList (g,(nt,s),b)) :: t -> + | AuxFnDef (loc,f,AuxList (g,(nt,s),b)) :: t -> if List.mem (Ntr nt) ss (* FZ add primary? *) - then ((AuxFnDef (f,Aux (g,id_nt))), Ic_Aux (g,nt,dummy_ret_type)) :: (update_bs t ss) - else ((AuxFnDef (f,AuxList (g,(nt,s),b))), Ic_None) :: (update_bs t ss) + then ((AuxFnDef (loc,f,Aux (g,id_nt))), Ic_Aux (g,nt,dummy_ret_type)) :: (update_bs t ss) + else ((AuxFnDef (loc,f,AuxList (g,(nt,s),b))), Ic_None) :: (update_bs t ss) - | AuxFnDef (f,NonTermListExp ((ntr,s),b)) :: t -> + | AuxFnDef (loc,f,NonTermListExp ((ntr,s),b)) :: t -> if List.mem (Ntr (Auxl.primary_ntr_of_ntr xd ntr)) ss - then ((AuxFnDef (f,Aux (f,id_nt))), Ic_NonTermListExp (f,ntr,dummy_ret_type) ) :: (update_bs t ss) - else ((AuxFnDef (f,NonTermListExp ((ntr,s),b))), Ic_None) :: (update_bs t ss) + then ((AuxFnDef (loc,f,Aux (f,id_nt))), Ic_NonTermListExp (f,ntr,dummy_ret_type) ) :: (update_bs t ss) + else ((AuxFnDef (loc,f,NonTermListExp ((ntr,s),b))), Ic_None) :: (update_bs t ss) - | AuxFnDef (f,MetaVarListExp ((mvr,s),b)) :: t -> + | AuxFnDef (loc,f,MetaVarListExp ((mvr,s),b)) :: t -> if List.mem (Mvr (Auxl.primary_mvr_of_mvr xd mvr)) ss - then ((AuxFnDef (f,Aux (f,id_nt))), Ic_MetaVarListExp (f,mvr,dummy_ret_type) ) :: (update_bs t ss) - else ((AuxFnDef (f,MetaVarListExp ((mvr,s),b))), Ic_None) :: (update_bs t ss) + then ((AuxFnDef (loc,f,Aux (f,id_nt))), Ic_MetaVarListExp (f,mvr,dummy_ret_type) ) :: (update_bs t ss) + else ((AuxFnDef (loc,f,MetaVarListExp ((mvr,s),b))), Ic_None) :: (update_bs t ss) - | Bind ((NonTermListExp ((ntr,s),b)), nt) :: t -> + | Bind (loc,(NonTermListExp ((ntr,s),b)), nt) :: t -> let auxfnname= "bind_"^id in if List.mem (Ntr (Auxl.primary_ntr_of_ntr xd ntr)) ss - then (Bind ((Aux (auxfnname,id_nt)),nt), Ic_NonTermListExp (auxfnname,ntr,Ntr ntr)) :: (update_bs t ss) - else (Bind ((NonTermListExp ((ntr,s),b)),nt), Ic_None) :: (update_bs t ss) + then (Bind (loc,(Aux (auxfnname,id_nt)),nt), Ic_NonTermListExp (auxfnname,ntr,Ntr ntr)) :: (update_bs t ss) + else (Bind (loc,(NonTermListExp ((ntr,s),b)),nt), Ic_None) :: (update_bs t ss) - | Bind ((MetaVarListExp ((mvr,s),b)), nt) :: t -> + | Bind (loc,(MetaVarListExp ((mvr,s),b)), nt) :: t -> let auxfnname= "bind_"^id in if List.mem (Mvr (Auxl.primary_mvr_of_mvr xd mvr)) ss - then (Bind ((Aux (auxfnname,id_nt)),nt), Ic_MetaVarListExp (auxfnname,mvr,Mvr mvr)) :: (update_bs t ss) - else (Bind ((MetaVarListExp ((mvr,s),b)),nt), Ic_None) :: (update_bs t ss) + then (Bind (loc,(Aux (auxfnname,id_nt)),nt), Ic_MetaVarListExp (auxfnname,mvr,Mvr mvr)) :: (update_bs t ss) + else (Bind (loc,(MetaVarListExp ((mvr,s),b)),nt), Ic_None) :: (update_bs t ss) | b :: t -> (b,Ic_None)::(update_bs t ss) | [] -> [] ) in @@ -196,9 +196,9 @@ let expand_element (m:pp_mode) (xd:syntaxdefn) (bs:bindspec list) (e:element) : ( fun i -> match i with | Ic_None -> None - | Ic_Aux (f,_,_) -> Some (AuxFnDef (f,Empty)) - | Ic_MetaVarListExp (f,_,_) -> Some (AuxFnDef (f,Empty)) - | Ic_NonTermListExp (f,_,_) -> Some (AuxFnDef (f,Empty)) ) + | Ic_Aux (f,_,_) -> Some (AuxFnDef (dummy_loc,f,Empty)) + | Ic_MetaVarListExp (f,_,_) -> Some (AuxFnDef (dummy_loc,f,Empty)) + | Ic_NonTermListExp (f,_,_) -> Some (AuxFnDef (dummy_loc,f,Empty)) ) aux_to_def; prod_loc = dummy_loc } in @@ -208,7 +208,7 @@ let expand_element (m:pp_mode) (xd:syntaxdefn) (bs:bindspec list) (e:element) : | Lang_nonterm (ntr,(ntr',_)) -> Lang_nonterm (ntr,(ntr',[])) | Lang_metavar (mvr,(mvr',_)) -> Lang_metavar (mvr,(mvr',[])) | Lang_terminal t -> Lang_terminal t - | _ -> Auxl.error "internal: remove suffix, cannot happen\n" ) in + | _ -> Auxl.error None "internal: remove suffix, cannot happen\n" ) in { prod_name = "Cons_" ^ id; prod_flavour = Bar; prod_meta = false; @@ -223,13 +223,13 @@ let expand_element (m:pp_mode) (xd:syntaxdefn) (bs:bindspec list) (e:element) : | Ic_None -> None | Ic_Aux (f,nt,_) -> (* FZ simple suffixes only *) let mse = Union (Aux (f,(nt,[])), Aux (f,id_nt)) in - Some (AuxFnDef (f,mse)) + Some (AuxFnDef (dummy_loc,f,mse)) | Ic_MetaVarListExp (f,mvr,_) -> let mse = Union ((MetaVarExp (mvr,[])), Aux (f,id_nt) ) in - Some (AuxFnDef (f,mse)) + Some (AuxFnDef (dummy_loc,f,mse)) | Ic_NonTermListExp (f,ntr,_) -> let mse = Union ((NonTermExp (ntr,[])), Aux (f,id_nt) ) in - Some (AuxFnDef (f,mse)) ) + Some (AuxFnDef (dummy_loc,f,mse)) ) aux_to_def; prod_loc = dummy_loc } in diff --git a/src/types.ml b/src/types.ml index f08788a..5594333 100644 --- a/src/types.ml +++ b/src/types.ml @@ -166,11 +166,11 @@ and dotenv3 = (nt_or_mv*subntr_data) list and dotenv = dotenv1 * dotenv2 (* (de1,de2) as de *) and bindspec = (* bs *) - | Bind of mse * nonterm - | AuxFnDef of auxfn * mse - | NamesEqual of mse * mse (* not currently implemented *) - | NamesDistinct of mse * mse (* not currently implemented *) - | AllNamesDistinct of mse (* not currently implemented *) + | Bind of loc * mse * nonterm + | AuxFnDef of loc * auxfn * mse + | NamesEqual of loc * mse * mse (* not currently implemented *) + | NamesDistinct of loc * mse * mse (* not currently implemented *) + | AllNamesDistinct of loc * mse (* not currently implemented *) and mse = (* mse *) (* mse stands for `metavar set expression', but includes nonterms too *) | MetaVarExp of metavar | NonTermExp of nonterm @@ -292,7 +292,7 @@ and xd_dependencies = (* xddep *) and embed = (* embed *) embedmorphism -and parsing_annotation = (prodname*parsing_annotation_type*prodname) (* pa *) +and parsing_annotation = (prodname*parsing_annotation_type*prodname*loc) (* pa *) and parsing_annotations = (* pas *) { pa_data : parsing_annotation list; } @@ -473,7 +473,7 @@ type ('t,'v) parser = ('t list -> 'v -> unit) -> 't list -> unit type made_parser = nontermroot -> bool -> string -> symterm list -exception My_parse_error of string +exception My_parse_error of loc option * string (** ************************ *) @@ -975,7 +975,7 @@ let lemTODOmo m s1 s2o = match s2o with None -> None | Some s2 -> Some (lemTODOm (* from grammar_typecheck *) -exception Typecheck_error of string*string;; +exception Typecheck_error of loc*string*string;; -let ty_error s1 s2 = raise (Typecheck_error(s1,s2)) -let ty_error2 l s1 s2 = raise (Typecheck_error(s1^" at "^Location.pp_loc l,s2)) +(* let ty_error s1 s2 = raise (Typecheck_error(None, s1,s2)) *) +let ty_error2 l s1 s2 = raise (Typecheck_error(l, s1,s2))