From 5fd9ee2d682c86c08a58651347c35abd93ab5b74 Mon Sep 17 00:00:00 2001 From: Alexander Diemand Date: Wed, 31 May 2023 21:09:42 +0200 Subject: [PATCH] convenient record update syntax from https://github.com/tchajed/coq-record-update Signed-off-by: Alexander Diemand --- .gitignore | 4 ++++ lxr.ml | 47 ++++++++++++++++++++++++++++++++++++------ lxr.mli | 12 +++++++++++ theories/Environment.v | 28 ++++++++----------------- 4 files changed, 66 insertions(+), 25 deletions(-) diff --git a/.gitignore b/.gitignore index 7c7266d..8966747 100644 --- a/.gitignore +++ b/.gitignore @@ -38,3 +38,7 @@ test8M testCHAR *.swp + +/html +/mlihtml + diff --git a/lxr.ml b/lxr.ml index 6684111..0b29fd5 100644 --- a/lxr.ml +++ b/lxr.ml @@ -75,6 +75,11 @@ type z = | Zpos of positive | Zneg of positive +(** val const : 'a1 -> 'a2 -> 'a1 **) + +let const a _ = + a + module Pos = struct type mask = @@ -1162,6 +1167,18 @@ module Assembly = else None end +type 't settable = + 't -> 't + (* singleton inductive, whose constructor was Build_Settable *) + +type ('r, 't) setter = ('t -> 't) -> 'r -> 'r + +(** val set : + ('a1 -> 'a2) -> ('a1, 'a2) setter -> ('a2 -> 'a2) -> 'a1 -> 'a1 **) + +let set _ setter0 = + setter0 + module Environment = struct type environment = { cur_assembly : Assembly.AssemblyPlainWritable.coq_H; @@ -1197,6 +1214,12 @@ module Environment = let keys e = e.keys + (** val etaX : environment settable **) + + let etaX x = + { cur_assembly = x.cur_assembly; cur_buffer = x.cur_buffer; config = + x.config; fblocks = x.fblocks; keys = x.keys } + (** val initial_environment : Configuration.configuration -> environment **) let initial_environment c = @@ -1207,22 +1230,34 @@ module Environment = let recreate_assembly e = let (a, b) = Assembly.AssemblyPlainWritable.create e.config in - { cur_assembly = a; cur_buffer = b; config = e.config; fblocks = - e.fblocks; keys = e.keys } + set (fun e0 -> e0.cur_assembly) (fun f -> + let h = fun r -> f r.cur_assembly in + (fun x -> { cur_assembly = (h x); cur_buffer = x.cur_buffer; config = + x.config; fblocks = x.fblocks; keys = x.keys })) (const a) + (set (fun e0 -> e0.cur_buffer) (fun f -> + let b0 = fun r -> f r.cur_buffer in + (fun x -> { cur_assembly = x.cur_assembly; cur_buffer = (b0 x); + config = x.config; fblocks = x.fblocks; keys = x.keys })) (const b) e) (** val env_add_file_block : string -> environment -> Assembly.blockinformation -> environment **) let env_add_file_block fname0 e bi = - { cur_assembly = e.cur_assembly; cur_buffer = e.cur_buffer; config = - e.config; fblocks = ((fname0, bi) :: e.fblocks); keys = e.keys } + set (fun e0 -> e0.fblocks) (fun f -> + let l = fun r -> f r.fblocks in + (fun x -> { cur_assembly = x.cur_assembly; cur_buffer = x.cur_buffer; + config = x.config; fblocks = (l x); keys = x.keys })) (fun bs -> + (fname0, bi) :: bs) e (** val env_add_aid_key : string -> environment -> Assembly.keyinformation -> environment **) let env_add_aid_key aid0 e ki = - { cur_assembly = e.cur_assembly; cur_buffer = e.cur_buffer; config = - e.config; fblocks = e.fblocks; keys = ((aid0, ki) :: e.keys) } + set (fun e0 -> e0.keys) (fun f -> + let l = fun r -> f r.keys in + (fun x -> { cur_assembly = x.cur_assembly; cur_buffer = x.cur_buffer; + config = x.config; fblocks = x.fblocks; keys = (l x) })) (fun ks -> + (aid0, ki) :: ks) e (** val key_for_aid : environment -> Assembly.aid_t -> Assembly.keyinformation option **) diff --git a/lxr.mli b/lxr.mli index 860ff27..4f9905a 100644 --- a/lxr.mli +++ b/lxr.mli @@ -36,6 +36,8 @@ type z = | Zpos of positive | Zneg of positive +val const : 'a1 -> 'a2 -> 'a1 + module Pos : sig type mask = @@ -396,6 +398,14 @@ module Assembly : Buffer.BufferPlain.buffer_t option end +type 't settable = + 't -> 't + (* singleton inductive, whose constructor was Build_Settable *) + +type ('r, 't) setter = ('t -> 't) -> 'r -> 'r + +val set : ('a1 -> 'a2) -> ('a1, 'a2) setter -> ('a2 -> 'a2) -> 'a1 -> 'a1 + module Environment : sig type environment = { cur_assembly : Assembly.AssemblyPlainWritable.coq_H; @@ -414,6 +424,8 @@ module Environment : val keys : environment -> (string * Assembly.keyinformation) list + val etaX : environment settable + val initial_environment : Configuration.configuration -> environment val recreate_assembly : environment -> environment diff --git a/theories/Environment.v b/theories/Environment.v index 6839275..8abc44f 100644 --- a/theories/Environment.v +++ b/theories/Environment.v @@ -5,7 +5,9 @@ Module Export Environment. Require Import NArith PArith. -From Coq Require Import NArith.BinNat Lists.List Strings.String. +From Coq Require Import NArith.BinNat Lists.List Strings.String Program.Basics. + +From RecordUpdate Require Import RecordUpdate. (* Open Scope positive_scope. *) Open Scope N_scope. @@ -25,6 +27,8 @@ Record environment : Type := ; keys : list (string * Assembly.keyinformation) }. +#[export] Instance etaX : Settable _ := settable! mkenvironment . + Definition initial_environment (c : configuration) : environment := let (a,b) := AssemblyPlainWritable.create c in {| cur_assembly := a @@ -36,27 +40,13 @@ Definition initial_environment (c : configuration) : environment := Definition recreate_assembly (e : environment) : environment := let (a,b) := AssemblyPlainWritable.create (config e) in - {| cur_assembly := a - ; cur_buffer := b - ; config := config e - ; fblocks := fblocks e - ; keys := keys e - |}. + set cur_assembly (const a) (set cur_buffer (const b) e). + Definition env_add_file_block (fname : string) (e : environment) (bi : Assembly.blockinformation) : environment := - {| cur_assembly := cur_assembly e - ; cur_buffer := cur_buffer e - ; config := config e - ; fblocks := (fname,bi) :: fblocks e - ; keys := keys e - |}. + set fblocks (fun bs => (fname,bi) :: bs) e. Definition env_add_aid_key (aid : string) (e : environment) (ki : keyinformation) : environment := - {| cur_assembly := cur_assembly e - ; cur_buffer := cur_buffer e - ; config := config e - ; fblocks := fblocks e - ; keys := (aid,ki) :: keys e - |}. + set keys (fun ks => (aid,ki) :: ks) e. (* find a key for an aid *) Definition key_for_aid (e : environment) (aid : Assembly.aid_t) : option keyinformation :=