# HG changeset patch # User wenzelm # Date 1729423637 -7200 # Node ID 893b056542e7915c3278b12623fe24552496b866 # Parent 00df78aa2b0c94950854855947be5ebac91aa754 more accurate treatment of constraints: restrict permissive mode to output; diff -r 00df78aa2b0c -r 893b056542e7 src/Pure/Syntax/ast.ML --- a/src/Pure/Syntax/ast.ML Sun Oct 20 13:13:17 2024 +0200 +++ b/src/Pure/Syntax/ast.ML Sun Oct 20 13:27:17 2024 +0200 @@ -27,7 +27,8 @@ val unfold_ast_p: string -> ast -> ast list * ast val trace: bool Config.T val stats: bool Config.T - val normalize: Proof.context -> (string -> (ast * ast) list) -> ast -> ast + val normalize: Proof.context -> {permissive_constraints: bool} -> + (string -> (ast * ast) list) -> ast -> ast end; structure Ast: AST = @@ -159,22 +160,22 @@ exception NO_MATCH; -fun const_match (Constant a) b = a = b - | const_match (Variable a) b = a = b - | const_match (Appl [Constant "_constrain", ast, _]) b = const_match ast b - | const_match _ _ = false; +fun const_match _ (Constant a) b = a = b + | const_match _ (Variable a) b = a = b + | const_match true (Appl [Constant "_constrain", ast, _]) b = const_match false ast b + | const_match _ _ _ = false; -fun match1 ast (Constant b) env = if const_match ast b then env else raise NO_MATCH - | match1 ast (Variable x) env = Symtab.update (x, ast) env - | match1 (Appl asts) (Appl pats) env = match2 asts pats env - | match1 _ _ _ = raise NO_MATCH -and match2 (ast :: asts) (pat :: pats) env = match1 ast pat env |> match2 asts pats - | match2 [] [] env = env - | match2 _ _ _ = raise NO_MATCH; +fun match1 p ast (Constant b) env = if const_match p ast b then env else raise NO_MATCH + | match1 p ast (Variable x) env = Symtab.update (x, ast) env + | match1 p (Appl asts) (Appl pats) env = match2 p asts pats env + | match1 p _ _ _ = raise NO_MATCH +and match2 p (ast :: asts) (pat :: pats) env = match1 p ast pat env |> match2 p asts pats + | match2 _ [] [] env = env + | match2 _ _ _ _ = raise NO_MATCH; in -fun match ast pat = +fun match p ast pat = let val (head, args) = (case (ast, pat) of @@ -184,7 +185,7 @@ else (ast, []) end | _ => (ast, [])); - in SOME (Symtab.build (match1 head pat), args) handle NO_MATCH => NONE end; + in SOME (Symtab.build (match1 p head pat), args) handle NO_MATCH => NONE end; end; @@ -214,7 +215,7 @@ in (*the normalizer works yoyo-like: top-down, bottom-up, top-down, ...*) -fun normalize ctxt get_rules pre_ast = +fun normalize ctxt {permissive_constraints = p} get_rules pre_ast = let val trace = Config.get ctxt trace; val stats = Config.get ctxt stats; @@ -224,7 +225,7 @@ val changes = Unsynchronized.ref 0; fun rewrite1 ((lhs, rhs) :: pats) ast = - (case match ast lhs of + (case match p ast lhs of SOME (env, args) => (Unsynchronized.inc changes; SOME (mk_appl (subst env rhs) args)) | NONE => (Unsynchronized.inc failed_matches; rewrite1 pats ast)) diff -r 00df78aa2b0c -r 893b056542e7 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Sun Oct 20 13:13:17 2024 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Sun Oct 20 13:27:17 2024 +0200 @@ -387,11 +387,9 @@ let val syn = Proof_Context.syntax_of ctxt; val tr = Syntax.parse_translation syn; - val parse_rules = Syntax.parse_rules syn; + val normalize = Ast.normalize ctxt {permissive_constraints = false} (Syntax.parse_rules syn); val (ambig_msgs, asts) = parse_asts ctxt false root input; - val results = - (map o apsnd o Exn.maps_res) - (Ast.normalize ctxt parse_rules #> Exn.result (ast_to_term ctxt tr)) asts; + val results = (map o apsnd o Exn.maps_res) (normalize #> Exn.result (ast_to_term ctxt tr)) asts; in (ambig_msgs, results) end; @@ -830,7 +828,7 @@ end; in t_to_ast ctxt (Syntax.print_translation syn) t - |> Ast.normalize ctxt (Syntax.print_rules syn) + |> Ast.normalize ctxt {permissive_constraints = true} (Syntax.print_rules syn) |> pretty_ast pretty_flags language_markup end;