more accurate treatment of constraints: restrict permissive mode to output;

--- 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))

--- 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;