diff options
| author | Brian Campbell | 2018-05-03 11:03:27 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-05-03 11:03:34 +0100 |
| commit | 449e8a54371b0c707bb7e3c5acdb4fd475a016d0 (patch) | |
| tree | 53d69c3e99c296f1420e9908407ba8757bac88be /src/parser.mly | |
| parent | fb4c8689e417d4f02dcfa61d44ee2271855161f1 (diff) | |
Work in progress on the coq backend
- originally based on the Lem backend
- added externs to some of the library files and tests
- added wildcard to extern valspecs in parser
- added Type_check.get_val_spec_orig to return the valspec with the
function's original names for bound type variables
Note that most of the tests will fail currently
Diffstat (limited to 'src/parser.mly')
| -rw-r--r-- | src/parser.mly | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/parser.mly b/src/parser.mly index 0846d4bb..3b7a435b 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -61,9 +61,11 @@ let default_opt x = function | None -> x | Some y -> y -let assoc_opt key assocs = +let assoc_opt key (assocs, default) = try Some (List.assoc key assocs) with - | Not_found -> None + | Not_found -> default + +let cons_fst h (t,x) = (h::t,x) let string_of_id = function | Id_aux (Id str, _) -> str @@ -1193,9 +1195,11 @@ let_def: externs: | id Colon String - { [(string_of_id $1, $3)] } + { ([(string_of_id $1, $3)], None) } + | Under Colon String + { ([], Some $3) } | id Colon String Comma externs - { (string_of_id $1, $3) :: $5 } + { cons_fst (string_of_id $1, $3) $5 } val_spec_def: | Doc val_spec_def |