Skip to content

Commit 9651dca

Browse files
committed
Try to handle underscores in Parse.parse_in_context
Expose and use the `ctxt_absyn_to_preterm` function created in HOL-Theorem-Prover@ba1eb9a Aims to fix HOL-Theorem-Prover#1489
1 parent 725300c commit 9651dca

File tree

2 files changed

+5
-1
lines changed

2 files changed

+5
-1
lines changed

src/parse/Parse.sml

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -460,11 +460,14 @@ fun smashErrm m =
460460
| errormonad.Some (_, result) => result
461461
val stdprinters = SOME(term_to_string,type_to_string)
462462

463+
fun ctxt_absyn_to_preterm fvs a =
464+
TermParse.ctxt_absyn_to_preterm (term_grammar()) fvs a
465+
463466
fun parse_in_context FVs q =
464467
let
465468
open errormonad
466469
val m =
467-
(q |> Absyn |> absyn_to_preterm) >-
470+
(q |> Absyn |> ctxt_absyn_to_preterm FVs) >-
468471
TermParse.ctxt_preterm_to_term stdprinters NONE FVs
469472
in
470473
smashErrm m

src/parse/TermParse.sig

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ sig
1616
val preterm : grammar -> tygrammar -> term quotation -> preterm in_env
1717
val typed_preterm : grammar -> tygrammar -> hol_type -> term quotation ->
1818
preterm in_env
19+
val ctxt_absyn_to_preterm : grammar -> term list -> absyn -> preterm in_env
1920
val absyn_to_preterm : grammar -> absyn -> preterm in_env
2021
val absyn_to_preterm_in_env : grammar -> absyn -> Parse_support.preterm_in_env
2122
val absyn_to_term : pprinters -> grammar -> absyn -> term

0 commit comments

Comments
 (0)