From 04cc46f9b4b92dd4d7d684db77e2564cb32043bc Mon Sep 17 00:00:00 2001 From: bu Date: Sun, 4 Nov 2018 18:56:59 +0100 Subject: [PATCH] New Config With AFP components and a thin interface for monitor-checking. --- Isa_DOF.thy | 14 +- RegExp.thy | 50 ++++- RegExpChecker.sml | 339 +++++++++++++++++++++++++++++++++ RegExpInterface.thy | 113 +++++++++++ ontologies/scholarly_paper.thy | 111 +++++++++++ 5 files changed, 616 insertions(+), 11 deletions(-) create mode 100644 RegExpChecker.sml create mode 100644 RegExpInterface.thy diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 89034f8..1fdfa9d 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -12,9 +12,9 @@ text\ Offering text\ In this section, we develop on the basis of a management of references Isar-markups that provide direct support in the PIDE framework. \ -theory Isa_DOF (* Isabelle Document Ontology Framework *) - imports Main (* Isa_MOF *) - RegExp +theory Isa_DOF (* Isabelle Document Ontology Framework *) + imports Main + RegExpInterface (* Interface to functional regular automata for monitoring *) Assert keywords "+=" ":=" @@ -65,9 +65,9 @@ structure DOF_core = struct type docclass_struct = {params : (string * sort) list, (*currently not used *) name : binding, thy_name : string, id : serial, (* for pide *) - inherits_from : (typ list * string) option, - attribute_decl : (binding * typ * term option) list, - rex : term list } + inherits_from : (typ list * string) option, (* imports *) + attribute_decl : (binding * typ * term option) list, (* class local *) + rex : term list } (* monitoring regexps --- product semantics*) type docclass_tab = docclass_struct Symtab.table @@ -169,7 +169,7 @@ fun upd_monitor_tabs f {docobj_tab,docclass_tab,ISA_transformer_tab, monitor_tab fun get_accepted_cids ({accepted_cids, regexp_stack }:open_monitor_info) = accepted_cids -fun get_regexp_stack ({accepted_cids, regexp_stack }:open_monitor_info) = regexp_stack +fun get_regexp_stack ({accepted_cids, regexp_stack }:open_monitor_info) = regexp_stack (* doc-class-name management: We still use the record-package for internally diff --git a/RegExp.thy b/RegExp.thy index 3b8af21..5638a1e 100644 --- a/RegExp.thy +++ b/RegExp.thy @@ -22,7 +22,7 @@ definition rep1 :: "'a rexp \ 'a rexp" ("\(_)\\<^sup where "\A\\<^sup>+ \ A ~~ \A\\<^sup>*" definition opt :: "'a rexp \ 'a rexp" ("\(_)\") - where "\A\ \ A || Zero" + where "\A\ \ A || One" value "Star (Conc(Alt (Atom(CHR ''a'')) (Atom(CHR ''b''))) (Atom(CHR ''c'')))" text{* or better equivalently: *} @@ -37,12 +37,14 @@ i.e. we give a direct meaning for regular expressions in some universe of ``deno This universe of denotations is in our concrete case: *} +definition enabled :: "('a,'\ set)da \ '\ set \ 'a list \ 'a list" + where "enabled A \ = filter (\x. next A x \ \ {}) " text{* Now the denotational semantics for regular expression can be defined on a post-card: *} fun L :: "'a rexp => 'a lang" where L_Emp : "L Zero = {}" - |L_One: "L One = {[]}" + |L_One: "L One = {[]}" |L_Atom: "L (\a\) = {[a]}" |L_Un: "L (el || er) = (L el) \ (L er)" |L_Conc: "L (el ~~ er) = {xs@ys | xs ys. xs \ L el \ ys \ L er}" @@ -58,11 +60,51 @@ fun L\<^sub>s\<^sub>u\<^sub>b :: "'a::order rexp => 'a lang" |L\<^sub>s\<^sub>u\<^sub>b_Conc: "L\<^sub>s\<^sub>u\<^sub>b (el ~~ er) = {xs@ys | xs ys. xs \ L\<^sub>s\<^sub>u\<^sub>b el \ ys \ L\<^sub>s\<^sub>u\<^sub>b er}" |L\<^sub>s\<^sub>u\<^sub>b_Star: "L\<^sub>s\<^sub>u\<^sub>b (Star e) = Regular_Set.star(L\<^sub>s\<^sub>u\<^sub>b e)" + +definition XX where "XX = (rexp2na example_expression)" +definition YY where "YY = na2da(rexp2na example_expression)" (* reminder from execute *) value "NA.accepts (rexp2na example_expression) [0,1,1,0,0,1]" - value "DA.accepts (na2da (rexp2na example_expression)) [0,1,1,0,0,1]" - + +definition zero where "zero = (0::nat)" +definition one where "one = (1::nat)" + +typ "'a set" + + +export_code zero one Suc Int.nat nat_of_integer int_of_integer + Zero One Atom Plus Times Star + rexp2na na2da enabled + NA.accepts DA.accepts + + example_expression + + in SML + + + module_name RegExpChecker file "RegExpChecker.sml" + +SML_file "RegExpChecker.sml" + +ML\ open RegExpChecker;\ + +(* +ML{* use "RegExpChecker.sml"; open RegExpChecker; + +val eq_int = {equal = curry(op =) : int -> int -> bool}; +val eq_bool_list = {equal = curry(op =) : bool list -> bool list -> bool}; +val eq_mynat = {equal = fn x:RegExpChecker.nat => fn y => x = y} +val s = RegExpChecker.rexp2na eq_int; +val xxx = na2da eq_mynat; +val ((init), (next,fin)) = na2da eq_bool_list (RegExpChecker.rexp2na eq_mynat example_expression); +val Set X = next zero init; +val Set Y = next one init; +val Set Z = next (Suc one) init; +*} +*) + + no_notation Atom ("\_\") diff --git a/RegExpChecker.sml b/RegExpChecker.sml new file mode 100644 index 0000000..23d75c6 --- /dev/null +++ b/RegExpChecker.sml @@ -0,0 +1,339 @@ +structure RegExpChecker : sig + type 'a equal + type num + type int + datatype nat = Zero_nat | Suc of nat + type 'a set + datatype 'a rexp = Zero | Onea | Atom of 'a | Plus of 'a rexp * 'a rexp | + Times of 'a rexp * 'a rexp | Star of 'a rexp + val nat : int -> nat + val accepts : 'a * (('b -> 'a -> 'a) * ('a -> bool)) -> 'b list -> bool + val acceptsa : + 'a equal -> 'a * (('b -> 'a -> 'a set) * ('a -> bool)) -> 'b list -> bool + val na2da : + 'a equal -> + 'a * (('b -> 'a -> 'a set) * ('a -> bool)) -> + 'a set * (('b -> 'a set -> 'a set) * ('a set -> bool)) + val rexp2na : + 'a equal -> + 'a rexp -> + bool list * (('a -> bool list -> (bool list) set) * (bool list -> bool)) + val one : nat + val zero : nat + val enabled : + 'a set * (('b -> 'a set -> 'a set) * ('a set -> bool)) -> + 'a set -> 'b list -> 'b list + val example_expression : nat rexp + val nat_of_integer : IntInf.int -> nat + val int_of_integer : IntInf.int -> int +end = struct + +fun equal_boola p true = p + | equal_boola p false = not p + | equal_boola true p = p + | equal_boola false p = not p; + +type 'a equal = {equal : 'a -> 'a -> bool}; +val equal = #equal : 'a equal -> 'a -> 'a -> bool; + +val equal_bool = {equal = equal_boola} : bool equal; + +fun eq A_ a b = equal A_ a b; + +fun equal_lista A_ [] (x21 :: x22) = false + | equal_lista A_ (x21 :: x22) [] = false + | equal_lista A_ (x21 :: x22) (y21 :: y22) = + eq A_ x21 y21 andalso equal_lista A_ x22 y22 + | equal_lista A_ [] [] = true; + +fun equal_list A_ = {equal = equal_lista A_} : ('a list) equal; + +datatype num = One | Bit0 of num | Bit1 of num; + +datatype int = Zero_int | Pos of num | Neg of num; + +datatype nat = Zero_nat | Suc of nat; + +datatype 'a set = Set of 'a list | Coset of 'a list; + +datatype 'a rexp = Zero | Onea | Atom of 'a | Plus of 'a rexp * 'a rexp | + Times of 'a rexp * 'a rexp | Star of 'a rexp; + +fun dup (Neg n) = Neg (Bit0 n) + | dup (Pos n) = Pos (Bit0 n) + | dup Zero_int = Zero_int; + +fun plus_nat (Suc m) n = plus_nat m (Suc n) + | plus_nat Zero_nat n = n; + +val one_nat : nat = Suc Zero_nat; + +fun nat_of_num (Bit1 n) = let + val m = nat_of_num n; + in + Suc (plus_nat m m) + end + | nat_of_num (Bit0 n) = let + val m = nat_of_num n; + in + plus_nat m m + end + | nat_of_num One = one_nat; + +fun nat (Pos k) = nat_of_num k + | nat Zero_int = Zero_nat + | nat (Neg k) = Zero_nat; + +fun uminus_int (Neg m) = Pos m + | uminus_int (Pos m) = Neg m + | uminus_int Zero_int = Zero_int; + +fun plus_num (Bit1 m) (Bit1 n) = Bit0 (plus_num (plus_num m n) One) + | plus_num (Bit1 m) (Bit0 n) = Bit1 (plus_num m n) + | plus_num (Bit1 m) One = Bit0 (plus_num m One) + | plus_num (Bit0 m) (Bit1 n) = Bit1 (plus_num m n) + | plus_num (Bit0 m) (Bit0 n) = Bit0 (plus_num m n) + | plus_num (Bit0 m) One = Bit1 m + | plus_num One (Bit1 n) = Bit0 (plus_num n One) + | plus_num One (Bit0 n) = Bit1 n + | plus_num One One = Bit0 One; + +val one_int : int = Pos One; + +fun bitM One = One + | bitM (Bit0 n) = Bit1 (bitM n) + | bitM (Bit1 n) = Bit1 (Bit0 n); + +fun sub (Bit0 m) (Bit1 n) = minus_int (dup (sub m n)) one_int + | sub (Bit1 m) (Bit0 n) = plus_int (dup (sub m n)) one_int + | sub (Bit1 m) (Bit1 n) = dup (sub m n) + | sub (Bit0 m) (Bit0 n) = dup (sub m n) + | sub One (Bit1 n) = Neg (Bit0 n) + | sub One (Bit0 n) = Neg (bitM n) + | sub (Bit1 m) One = Pos (Bit0 m) + | sub (Bit0 m) One = Pos (bitM m) + | sub One One = Zero_int +and plus_int (Neg m) (Neg n) = Neg (plus_num m n) + | plus_int (Neg m) (Pos n) = sub n m + | plus_int (Pos m) (Neg n) = sub m n + | plus_int (Pos m) (Pos n) = Pos (plus_num m n) + | plus_int Zero_int l = l + | plus_int k Zero_int = k +and minus_int (Neg m) (Neg n) = sub n m + | minus_int (Neg m) (Pos n) = Neg (plus_num m n) + | minus_int (Pos m) (Neg n) = Pos (plus_num m n) + | minus_int (Pos m) (Pos n) = sub m n + | minus_int Zero_int l = uminus_int l + | minus_int k Zero_int = k; + +fun list_ex p [] = false + | list_ex p (x :: xs) = p x orelse list_ex p xs; + +fun bex (Set xs) p = list_ex p xs; + +fun snd (x1, x2) = x2; + +fun fst (x1, x2) = x1; + +fun next a = fst (snd a); + +fun foldl f a [] = a + | foldl f a (x :: xs) = foldl f (f a x) xs; + +fun foldl2 f xs a = foldl (fn aa => fn b => f b aa) a xs; + +fun delta a = foldl2 (next a); + +fun filter p [] = [] + | filter p (x :: xs) = (if p x then x :: filter p xs else filter p xs); + +fun membera A_ [] y = false + | membera A_ (x :: xs) y = eq A_ x y orelse membera A_ xs y; + +fun member A_ x (Coset xs) = not (membera A_ xs x) + | member A_ x (Set xs) = membera A_ xs x; + +fun removeAll A_ x [] = [] + | removeAll A_ x (y :: xs) = + (if eq A_ x y then removeAll A_ x xs else y :: removeAll A_ x xs); + +fun inserta A_ x xs = (if membera A_ xs x then xs else x :: xs); + +fun insert A_ x (Coset xs) = Coset (removeAll A_ x xs) + | insert A_ x (Set xs) = Set (inserta A_ x xs); + +fun fold f (x :: xs) s = fold f xs (f x s) + | fold f [] s = s; + +fun sup_set A_ (Coset xs) a = Coset (filter (fn x => not (member A_ x a)) xs) + | sup_set A_ (Set xs) a = fold (insert A_) xs a; + +val bot_set : 'a set = Set []; + +fun sup_seta A_ (Set xs) = fold (sup_set A_) xs bot_set; + +fun map f [] = [] + | map f (x21 :: x22) = f x21 :: map f x22; + +fun image f (Set xs) = Set (map f xs); + +fun deltaa A_ a [] p = insert A_ p bot_set + | deltaa A_ aa (a :: w) p = + sup_seta A_ (image (deltaa A_ aa w) (next aa a p)); + +fun null [] = true + | null (x :: xs) = false; + +fun start a = fst a; + +fun fin a = snd (snd a); + +fun accepts a = (fn w => fin a (delta a w (start a))); + +fun acceptsa A_ a w = bex (deltaa A_ a w (start a)) (fin a); + +fun or x = + (fn (ql, (dl, fl)) => fn (qr, (dr, fr)) => + ([], ((fn a => fn b => + (case b + of [] => + sup_set (equal_list equal_bool) + (image (fn aa => true :: aa) (dl a ql)) + (image (fn aa => false :: aa) (dr a qr)) + | true :: s => image (fn aa => true :: aa) (dl a s) + | false :: s => image (fn aa => false :: aa) (dr a s))), + (fn a => + (case a of [] => fl ql orelse fr qr | true :: s => fl s + | false :: s => fr s))))) + x; + +fun is_empty (Set xs) = null xs; + +fun na2da A_ a = + (insert A_ (start a) bot_set, + ((fn aa => fn q => sup_seta A_ (image (next a aa) q)), + (fn q => bex q (fin a)))); + +fun atom A_ a = + ([true], + ((fn b => fn s => + (if equal_lista equal_bool s [true] andalso eq A_ b a + then insert (equal_list equal_bool) [false] bot_set else bot_set)), + (fn s => equal_lista equal_bool s [false]))); + +fun conc x = + (fn (ql, (dl, fl)) => fn (qr, (dr, fr)) => + (true :: ql, + ((fn a => fn b => + (case b of [] => bot_set + | true :: s => + sup_set (equal_list equal_bool) + (image (fn aa => true :: aa) (dl a s)) + (if fl s then image (fn aa => false :: aa) (dr a qr) + else bot_set) + | false :: s => image (fn aa => false :: aa) (dr a s))), + (fn a => + (case a of [] => false + | left :: s => + left andalso (fl s andalso fr qr) orelse + not left andalso fr s))))) + x; + +fun plus x = + (fn (q, (d, f)) => + (q, ((fn a => fn s => + sup_set (equal_list equal_bool) (d a s) + (if f s then d a q else bot_set)), + f))) + x; + +val epsilon : + bool list * (('a -> bool list -> (bool list) set) * (bool list -> bool)) + = ([], ((fn _ => fn _ => bot_set), null)); + +fun star a = or epsilon (plus a); + +fun rexp2na A_ Zero = ([], ((fn _ => fn _ => bot_set), (fn _ => false))) + | rexp2na A_ Onea = epsilon + | rexp2na A_ (Atom a) = atom A_ a + | rexp2na A_ (Plus (r, s)) = or (rexp2na A_ r) (rexp2na A_ s) + | rexp2na A_ (Times (r, s)) = conc (rexp2na A_ r) (rexp2na A_ s) + | rexp2na A_ (Star r) = star (rexp2na A_ r); + +fun apsnd f (x, y) = (x, f y); + +val one : nat = one_nat; + +val zero : nat = Zero_nat; + +fun enabled a sigma = filter (fn x => not (is_empty (next a x sigma))); + +val example_expression : nat rexp = + let + val r0 = Atom Zero_nat; + val r1 = Atom one_nat; + in + Times (Star (Plus (Times (r1, r1), r0)), Star (Plus (Times (r0, r0), r1))) + end; + +fun sgn_integer k = + (if ((k : IntInf.int) = (0 : IntInf.int)) then (0 : IntInf.int) + else (if IntInf.< (k, (0 : IntInf.int)) then (~1 : IntInf.int) + else (1 : IntInf.int))); + +fun divmod_integer k l = + (if ((k : IntInf.int) = (0 : IntInf.int)) + then ((0 : IntInf.int), (0 : IntInf.int)) + else (if ((l : IntInf.int) = (0 : IntInf.int)) then ((0 : IntInf.int), k) + else (apsnd o (fn a => fn b => IntInf.* (a, b)) o sgn_integer) l + (if (((sgn_integer k) : IntInf.int) = (sgn_integer l)) + then IntInf.divMod (IntInf.abs k, IntInf.abs l) + else let + val (r, s) = + IntInf.divMod (IntInf.abs k, IntInf.abs l); + in + (if ((s : IntInf.int) = (0 : IntInf.int)) + then (IntInf.~ r, (0 : IntInf.int)) + else (IntInf.- (IntInf.~ r, (1 : IntInf.int)), + IntInf.- (IntInf.abs l, s))) + end))); + +fun nat_of_integer k = + (if IntInf.<= (k, (0 : IntInf.int)) then Zero_nat + else let + val (l, j) = divmod_integer k (2 : IntInf.int); + val la = nat_of_integer l; + val lb = plus_nat la la; + in + (if ((j : IntInf.int) = (0 : IntInf.int)) then lb + else plus_nat lb one_nat) + end); + +fun times_num (Bit1 m) (Bit1 n) = + Bit1 (plus_num (plus_num m n) (Bit0 (times_num m n))) + | times_num (Bit1 m) (Bit0 n) = Bit0 (times_num (Bit1 m) n) + | times_num (Bit0 m) (Bit1 n) = Bit0 (times_num m (Bit1 n)) + | times_num (Bit0 m) (Bit0 n) = Bit0 (Bit0 (times_num m n)) + | times_num One n = n + | times_num m One = m; + +fun times_int (Neg m) (Neg n) = Pos (times_num m n) + | times_int (Neg m) (Pos n) = Neg (times_num m n) + | times_int (Pos m) (Neg n) = Neg (times_num m n) + | times_int (Pos m) (Pos n) = Pos (times_num m n) + | times_int Zero_int l = Zero_int + | times_int k Zero_int = Zero_int; + +fun int_of_integer k = + (if IntInf.< (k, (0 : IntInf.int)) + then uminus_int (int_of_integer (IntInf.~ k)) + else (if ((k : IntInf.int) = (0 : IntInf.int)) then Zero_int + else let + val (l, j) = divmod_integer k (2 : IntInf.int); + val la = times_int (Pos (Bit0 One)) (int_of_integer l); + in + (if ((j : IntInf.int) = (0 : IntInf.int)) then la + else plus_int la one_int) + end)); + +end; (*struct RegExpChecker*) diff --git a/RegExpInterface.thy b/RegExpInterface.thy new file mode 100644 index 0000000..08b2bd9 --- /dev/null +++ b/RegExpInterface.thy @@ -0,0 +1,113 @@ +theory RegExpInterface +imports "Functional-Automata.Execute" +begin + +term Atom +value "Star (Times(Plus (Atom(CHR ''a'')) (Atom(CHR ''b''))) (Atom(CHR ''c'')))" + +notation Star ("\(_)\\<^sup>*" [0]100) +notation Plus (infixr "||" 55) +notation Times (infixr "~~" 60) +notation Atom ("\_\" 65) + +(* +datatype 'a rexp = Empty ("<>") + | Atom 'a ("\_\" 65) + | Alt "('a rexp)" "('a rexp)" (infixr "||" 55) + | Conc "('a rexp)" "('a rexp)" (infixr "~~" 60) + | Star "('a rexp)" ("\(_)\\<^sup>*" [0]100) +*) + +definition rep1 :: "'a rexp \ 'a rexp" ("\(_)\\<^sup>+") + where "\A\\<^sup>+ \ A ~~ \A\\<^sup>*" + +definition opt :: "'a rexp \ 'a rexp" ("\(_)\") + where "\A\ \ A || One" + +value "Star (Conc(Alt (Atom(CHR ''a'')) (Atom(CHR ''b''))) (Atom(CHR ''c'')))" +text{* or better equivalently: *} +value "\(\CHR ''a''\ || \CHR ''b''\) ~~ \CHR ''c''\\\<^sup>*" + +section{* Definition of a semantic function: the ``language'' of the regular expression *} +text\ This is just a reminder - already defined in @{theory Regular_Exp} as @{term lang}.\ + +text{* In the following, we give a semantics for our regular expressions, which so far have +just been a term language (i.e. abstract syntax). The semantics is a ``denotational semantics'', +i.e. we give a direct meaning for regular expressions in some universe of ``denotations''. + +This universe of denotations is in our concrete case: *} + +definition enabled :: "('a,'\ set)da \ '\ set \ 'a list \ 'a list" + where "enabled A \ = filter (\x. next A x \ \ {}) " + +text{* Now the denotational semantics for regular expression can be defined on a post-card: *} + +fun L :: "'a rexp => 'a lang" + where L_Emp : "L Zero = {}" + |L_One: "L One = {[]}" + |L_Atom: "L (\a\) = {[a]}" + |L_Un: "L (el || er) = (L el) \ (L er)" + |L_Conc: "L (el ~~ er) = {xs@ys | xs ys. xs \ L el \ ys \ L er}" + |L_Star: "L (Star e) = Regular_Set.star(L e)" + + +text\A more useful definition is the \ +fun L\<^sub>s\<^sub>u\<^sub>b :: "'a::order rexp => 'a lang" + where L\<^sub>s\<^sub>u\<^sub>b_Emp: "L\<^sub>s\<^sub>u\<^sub>b Zero = {}" + |L\<^sub>s\<^sub>u\<^sub>b_One: "L\<^sub>s\<^sub>u\<^sub>b One = {[]}" + |L\<^sub>s\<^sub>u\<^sub>b_Atom: "L\<^sub>s\<^sub>u\<^sub>b (\a\) = {z . \x. x \ a \ z=[x]}" + |L\<^sub>s\<^sub>u\<^sub>b_Un: "L\<^sub>s\<^sub>u\<^sub>b (el || er) = (L\<^sub>s\<^sub>u\<^sub>b el) \ (L\<^sub>s\<^sub>u\<^sub>b er)" + |L\<^sub>s\<^sub>u\<^sub>b_Conc: "L\<^sub>s\<^sub>u\<^sub>b (el ~~ er) = {xs@ys | xs ys. xs \ L\<^sub>s\<^sub>u\<^sub>b el \ ys \ L\<^sub>s\<^sub>u\<^sub>b er}" + |L\<^sub>s\<^sub>u\<^sub>b_Star: "L\<^sub>s\<^sub>u\<^sub>b (Star e) = Regular_Set.star(L\<^sub>s\<^sub>u\<^sub>b e)" + + +definition XX where "XX = (rexp2na example_expression)" +definition YY where "YY = na2da(rexp2na example_expression)" +(* reminder from execute *) +value "NA.accepts (rexp2na example_expression) [0,1,1,0,0,1]" +value "DA.accepts (na2da (rexp2na example_expression)) [0,1,1,0,0,1]" + +definition zero where "zero = (0::nat)" +definition one where "one = (1::nat)" + +typ "'a set" + + +export_code zero one Suc Int.nat nat_of_integer int_of_integer + Zero One Atom Plus Times Star + rexp2na na2da enabled + NA.accepts DA.accepts + + example_expression + + in SML + + + module_name RegExpChecker file "RegExpChecker.sml" + +SML_file "RegExpChecker.sml" + +ML\ +(*use "RegExpChecker.sml"; +open RegExpChecker; *)\ + +(* +ML{* use "RegExpChecker.sml"; open RegExpChecker; + +val eq_int = {equal = curry(op =) : int -> int -> bool}; +val eq_bool_list = {equal = curry(op =) : bool list -> bool list -> bool}; +val eq_mynat = {equal = fn x:RegExpChecker.nat => fn y => x = y} +val s = RegExpChecker.rexp2na eq_int; +val xxx = na2da eq_mynat; +val ((init), (next,fin)) = na2da eq_bool_list (RegExpChecker.rexp2na eq_mynat example_expression); +val Set X = next zero init; +val Set Y = next one init; +val Set Z = next (Suc one) init; +*} +*) + + +no_notation Atom ("\_\") + + +end diff --git a/ontologies/scholarly_paper.thy b/ontologies/scholarly_paper.thy index a564d44..87bcf4a 100644 --- a/ontologies/scholarly_paper.thy +++ b/ontologies/scholarly_paper.thy @@ -88,5 +88,116 @@ doc_class article = gen_sty_template + +ML\ +val term = @{term "(title ~~ + \subtitle\ ~~ + \author\\<^sup>+ ~~ + abstract ~~ + introduction ~~ + \technical || example\\<^sup>+ ~~ + conclusion ~~ + bibliography)"} + +\ + + +ML\ +use "RegExpChecker.sml"; + +structure RegExpInterface : sig + type automaton + type env + val alphabet: term list -> env + val conv : term -> env -> int RegExpChecker.rexp (* for debugging *) + val rexp_term2da: term -> env -> automaton + val enabled : automaton -> env -> string list + val next : automaton -> env -> string -> automaton + val final : automaton -> bool + val accepts : automaton -> env -> string list -> bool + end + = +struct +local open RegExpChecker in + + type state = bool list RegExpChecker.set + type env = string list + + type automaton = state * ((Int.int -> state -> state) * (state -> bool)) + + val add_atom = fold_aterms (fn Const(c as(_,Type(@{type_name "rexp"},_)))=> insert (op=) c |_=>I); + fun alphabet termS = rev(map fst (fold add_atom termS [])); + + fun conv (Const(@{const_name "Regular_Exp.rexp.Zero"},_)) _ = Zero + |conv (Const(@{const_name "Regular_Exp.rexp.One"},_)) _ = Onea + |conv (Const(@{const_name "Regular_Exp.rexp.Times"},_) $ X $ Y) env = Times(conv X env, conv Y env) + |conv (Const(@{const_name "Regular_Exp.rexp.Plus"},_) $ X $ Y) env = Plus(conv X env, conv Y env) + |conv (Const(@{const_name "Regular_Exp.rexp.Star"},_) $ X) env = Star(conv X env) + |conv (Const(@{const_name "RegExpInterface.opt"},_) $ X) env = Plus(conv X env, Onea) + |conv (Const(@{const_name "RegExpInterface.rep1"},_) $ X) env = Times(conv X env, Star(conv X env)) + |conv (Const (s, @{typ "doc_class rexp"})) env = + let val n = find_index (fn x => x = s) env + val _ = if n<0 then error"conversion error of regexp." else () + in Atom(n) end + |conv S _ = error("conversion error of regexp:" ^ (Syntax.string_of_term (@{context})S)) + + val eq_int = {equal = curry(op =) : Int.int -> Int.int -> bool}; + val eq_bool_list = {equal = curry(op =) : bool list -> bool list -> bool}; + + fun rexp_term2da term env = let val rexp = conv term env; + val nda = RegExpChecker.rexp2na eq_int rexp; + val da = RegExpChecker.na2da eq_bool_list nda; + in da end; + + + (* here comes the main interface of the module: + - "enabled" gives the part of the alphabet "env" for which the automatan does not + go into a final state + - next provides an automata transformation that produces an automaton that + recognizes the rest of a word after a *) + fun enabled (da as (state,(_,_))) env = + let val inds = RegExpChecker.enabled da state (0 upto (length env - 1)) + in map (fn i => nth env i) inds end + + fun next (current_state, (step,fin)) env a = + let val index = find_index (fn x => x = a) env + in if index < 0 then error"undefined id for monitor" + else (step index current_state,(step,fin)) + end + + fun final (current_state, (_,fin)) = fin current_state + + fun accepts da env word = let fun index a = find_index (fn x => x = a) env + val indexL = map index word + val _ = if forall (fn x => x >= 0) indexL then () + else error"undefined id for monitor" + in RegExpChecker.accepts da indexL end + +end; (* local *) +end (* struct *) +\ +ML\ +val alpha = (RegExpInterface.alphabet [term]); +val DA as (init,(next,fin)) = RegExpInterface.rexp_term2da term (RegExpInterface.alphabet [term]) ; +RegExpChecker.accepts DA [0,2,3,4,5,6,7,8]; + + +val S0 = init +val E1 = RegExpChecker.enabled DA S0 [0,1,2,3,4,5,6,7,8]; +val S1 = next 0 init; +val E2 = RegExpChecker.enabled DA S1 [0,1,2,3,4,5,6,7,8]; +val S2 = next 2 S1; (* uffz. it works. *) +val E3 = RegExpChecker.enabled DA S2 [0,1,2,3,4,5,6,7,8]; +val S3 = next 3 S2; (* uffz. it works. *) +\ + +ML\ +RegExpInterface.enabled DA alpha; +val DA' = RegExpInterface.next DA alpha "scholarly_paper.title"; +RegExpInterface.enabled DA' alpha; +val DA'' = RegExpInterface.next DA' alpha "scholarly_paper.author"; +RegExpInterface.enabled DA'' alpha; +\ + end