# HG changeset patch # User haftmann # Date 1548004475 0 # Node ID 4d95261fab5af9384dc05793482ddb86307fb95c # Parent 9fd395ff57bcfc83430ce19c42b198911dea89e9 more conventional syntax for code_stmts antiquotation diff -r 9fd395ff57bc -r 4d95261fab5a NEWS --- a/NEWS Sun Jan 20 21:26:15 2019 +0100 +++ b/NEWS Sun Jan 20 17:14:35 2019 +0000 @@ -85,6 +85,9 @@ proper module frame, nothing is added magically any longer. INCOMPATIBILITY. +* Code generation: slightly more conventional syntax for +'code_stmts' antiquotation. Minor INCOMPATIBILITY. + * Simplified syntax setup for big operators under image. In rare situations, type conversions are not inserted implicitly any longer and need to be given explicitly. Auxiliary abbreviations INFIMUM, diff -r 9fd395ff57bc -r 4d95261fab5a src/Doc/Codegen/Foundations.thy --- a/src/Doc/Codegen/Foundations.thy Sun Jan 20 21:26:15 2019 +0100 +++ b/src/Doc/Codegen/Foundations.thy Sun Jan 20 17:14:35 2019 +0000 @@ -191,7 +191,7 @@ \ text %quote \ - @{code_stmts dequeue (consts) dequeue (Haskell)} + @{code_stmts dequeue constant: dequeue (Haskell)} \ text \ @@ -283,7 +283,7 @@ \ text %quote \ - @{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)} + @{code_stmts strict_dequeue constant: strict_dequeue (Haskell)} \ text \ @@ -325,7 +325,7 @@ \ text %quote \ - @{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)} + @{code_stmts strict_dequeue' constant: empty_queue strict_dequeue' (Haskell)} \ text \ diff -r 9fd395ff57bc -r 4d95261fab5a src/Doc/Codegen/Further.thy --- a/src/Doc/Codegen/Further.thy Sun Jan 20 21:26:15 2019 +0100 +++ b/src/Doc/Codegen/Further.thy Sun Jan 20 17:14:35 2019 +0000 @@ -194,7 +194,7 @@ \ text %quote \ - @{code_stmts funpows (consts) Nat.funpow funpows (Haskell)} + @{code_stmts funpows constant: Nat.funpow funpows (Haskell)} \ diff -r 9fd395ff57bc -r 4d95261fab5a src/Doc/Codegen/Refinement.thy --- a/src/Doc/Codegen/Refinement.thy Sun Jan 20 21:26:15 2019 +0100 +++ b/src/Doc/Codegen/Refinement.thy Sun Jan 20 17:14:35 2019 +0000 @@ -32,7 +32,7 @@ \ text %quote \ - @{code_stmts fib (consts) fib (Haskell)} + @{code_stmts fib constant: fib (Haskell)} \ text \ @@ -69,7 +69,7 @@ \ text %quote \ - @{code_stmts fib (consts) fib fib_step (Haskell)} + @{code_stmts fib constant: fib fib_step (Haskell)} \ diff -r 9fd395ff57bc -r 4d95261fab5a src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Sun Jan 20 21:26:15 2019 +0100 +++ b/src/Tools/Code/code_target.ML Sun Jan 20 17:14:35 2019 +0000 @@ -513,25 +513,29 @@ check_code ctxt all_public (Code_Thingol.read_const_exprs ctxt raw_cs) seris; +val (constantK, type_constructorK, type_classK, class_relationK, class_instanceK, code_moduleK) = + (\<^keyword>\constant\, \<^keyword>\type_constructor\, \<^keyword>\type_class\, + \<^keyword>\class_relation\, \<^keyword>\class_instance\, \<^keyword>\code_module\); + local val parse_const_terms = Scan.repeat1 Args.term >> (fn ts => fn ctxt => map (Code.check_const (Proof_Context.theory_of ctxt)) ts); -fun parse_names category parse internalize mark_symbol = - Scan.lift (Args.parens (Args.$$$ category)) |-- Scan.repeat1 parse +fun parse_names keyword parse internalize mark_symbol = + Scan.lift (keyword --| Args.colon) |-- Scan.repeat1 parse >> (fn xs => fn ctxt => map (mark_symbol o internalize ctxt) xs); -val parse_consts = parse_names "consts" Args.term +val parse_consts = parse_names constantK Args.term (Code.check_const o Proof_Context.theory_of) Constant; -val parse_types = parse_names "types" (Scan.lift Args.name) +val parse_types = parse_names type_constructorK (Scan.lift Args.name) (Sign.intern_type o Proof_Context.theory_of) Type_Constructor; -val parse_classes = parse_names "classes" (Scan.lift Args.name) +val parse_classes = parse_names type_classK (Scan.lift Args.name) (Sign.intern_class o Proof_Context.theory_of) Type_Class; -val parse_instances = parse_names "instances" (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name)) +val parse_instances = parse_names class_instanceK (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name)) (fn ctxt => fn (raw_tyco, raw_class) => let val thy = Proof_Context.theory_of ctxt; @@ -646,10 +650,6 @@ (** Isar setup **) -val (constantK, type_constructorK, type_classK, class_relationK, class_instanceK, code_moduleK) = - (\<^keyword>\constant\, \<^keyword>\type_constructor\, \<^keyword>\type_class\, - \<^keyword>\class_relation\, \<^keyword>\class_instance\, \<^keyword>\code_module\); - local val parse_constants = constantK |-- Scan.repeat1 Parse.term >> map Constant;