diff options
| author | Kathy Gray | 2015-12-14 15:55:50 +0000 |
|---|---|---|
| committer | Kathy Gray | 2015-12-14 15:56:00 +0000 |
| commit | fd1c1502ab59cd8a392af86376be99b0dc6b6b1f (patch) | |
| tree | 94316aae8826271fd7e794fd44d9fa4c205d331c | |
| parent | 4fa10da0d4b6d8cfbb10455644836f7e1a802a2c (diff) | |
Adding new location constructor for location of generated terms
| -rw-r--r-- | language/l2.lem | 3 | ||||
| -rw-r--r-- | language/l2.ott | 3 | ||||
| -rw-r--r-- | language/l2_parse.ml | 1 | ||||
| -rw-r--r-- | language/l2_parse.ott | 1 | ||||
| -rw-r--r-- | src/sail_lib.ml | 7 |
5 files changed, 10 insertions, 5 deletions
diff --git a/language/l2.lem b/language/l2.lem index 7abd595c..dbfcb832 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -7,8 +7,9 @@ open import Set_extra type l = | Unknown - | Int of string * maybe l (*Internally generated*) + | Int of string * l option (*internal types, functions*) | Range of string * nat * nat * nat * nat + | Generated of l (*location for a generated node, where l is the location of the closest original source*) type annot 'a = l * 'a diff --git a/language/l2.ott b/language/l2.ott index fcd3abe8..94362c44 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -57,8 +57,9 @@ open import Set_extra type l = | Unknown - | Int of string * maybe l (*Internally generated*) + | Int of string * l option (*internal types, functions*) | Range of string * nat * nat * nat * nat + | Generated of l (*location for a generated node, where l is the location of the closest original source*) type annot 'a = l * 'a diff --git a/language/l2_parse.ml b/language/l2_parse.ml index 76fa09b8..db50ecb6 100644 --- a/language/l2_parse.ml +++ b/language/l2_parse.ml @@ -6,6 +6,7 @@ type text = string type l = | Unknown | Int of string * l option + | Generated of l | Range of Lexing.position * Lexing.position type 'a annot = l * 'a diff --git a/language/l2_parse.ott b/language/l2_parse.ott index 83da93ad..ae6d89bb 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -46,6 +46,7 @@ type text = string type l = | Unknown | Int of string * l option + | Generated of l | Range of Lexing.position * Lexing.position type 'a annot = l * 'a diff --git a/src/sail_lib.ml b/src/sail_lib.ml index d1a5b891..4cfc1331 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -19,11 +19,12 @@ let parse_exps s = let msg = Printf.sprintf "syntax error on character %d" pos.Lexing.pos_cnum in failwith msg | Parse_ast.Parse_error_locn(l,m) -> - let loc = match l with + let rec format l = match l with | Parse_ast.Unknown -> "???" | Parse_ast.Range(p1,p2) -> Printf.sprintf "%d:%d" p1.Lexing.pos_cnum p2.Lexing.pos_cnum - | Parse_ast.Int(s,_) -> Printf.sprintf "code generated by: %s" s in - let msg = Printf.sprintf "syntax error: %s %s" loc m in + | Parse_ast.Generated l -> Printf.sprintf "code generated near: %s" (format l) + | Parse_ast.Int(s,_) -> Printf.sprintf "code for by: %s" s in + let msg = Printf.sprintf "syntax error: %s %s" (format l) m in failwith msg | Lexer.LexError(s,p) -> let msg = Printf.sprintf "lexing error: %s %d" s p.Lexing.pos_cnum in |