(**************************************************************************)
include "ground/lib/functions.ma".
-include "ground/lib/exteq.ma".
include "apps_2/functional/flifts_flifts_basic.ma".
include "apps_2/functional/mf_vlift.ma".
(**************************************************************************)
include "ground/lib/functions.ma".
-include "ground/lib/exteq.ma".
include "apps_2/functional/flifts_flifts_basic.ma".
include "apps_2/functional/mf_vpush.ma".
(* *)
(**************************************************************************)
-include "ground/lib/exteq.ma".
include "apps_2/models/model_vpush.ma".
include "apps_2/models/tm.ma".
.PHONY: all clean
+.SUFFIXES:
+
%.ml: %.aml
$(H)$(ALPHA) < $< > $@
--- /dev/null
+EXECS = mrc recomm
+
+REQUIRES =
+
+include ../Makefile.common
+
+clean::
+ @$(RM) recommGc*.ml*
+
+test:
+ @./recomm.native $(O) -C ../../ground/steps . | sort | uniq > log.txt
+
+MRCS = $(wildcard *.mrc)
+
+mrc: $(MRCS:%.mrc=recommGc%.ml)
+ @./mrc.native .
+
+recommGc%.ml recommGc%.mli: %.mrc mrc.ml
+ @./mrc.native $<
+
+.PHONY: test mrc
--- /dev/null
+PcsAnd b "" true false
+rtc_max, max
+rtc_shift, shift
+rtc_ism, test for constrained rt-transition counter
+rtc_ist, test for t-transition counter
--- /dev/null
+PccFor d "" true false
+T-BOUND RT-TRANSITION COUNTERS, RT-TRANSITION COUNTER
+T-TRANSITION COUNTERS, T-TRANSITION COUNTER
--- /dev/null
+module EI = MrcInput
+module EO = MrcOutput
+
+let process file =
+ if Sys.is_directory file then begin
+ let st = EI.read_dir file in
+ if st <> EI.read_index file then begin
+ Printf.eprintf "indexing: %S\n" file;
+ EO.write_index st
+ end
+ end else if Filename.extension file = ".mrc" then begin
+ Printf.eprintf "processing: %S\n" file;
+ EO.write_component (EI.read_file file)
+ end else begin
+ Printf.eprintf "skipping: %S\n" file
+ end
+
+let main =
+ Arg.parse [
+ ] process ""
--- /dev/null
+module ET = MrcTypes
+
+let read_substs substs ich =
+ let map subst =
+ let words = String.split_on_char ' ' subst in
+ List.filter ((<>) "") words
+ in
+ while true do
+ let line = input_line ich in
+ let subst = String.split_on_char ',' line in
+ substs := List.map map subst :: !substs
+ done
+
+let read_file file =
+ let ich = open_in file in
+ let line = input_line ich in
+ let scan r f d p o = r, f, d, p, o in
+ let rmod, rfun, dmod, para, optn =
+ Scanf.sscanf line "%s %s %S %b %b" scan
+ in
+ let substs = ref [] in
+ begin
+ try read_substs substs ich with
+ | End_of_file -> close_in ich
+ end;
+ {
+ ET.cmod = Filename.remove_extension file;
+ rmod; rfun; dmod; para; optn;
+ substs = !substs;
+ }
+
+let list_rev_filter_map filter map l =
+ let rec aux r = function
+ | [] -> r
+ | hd :: tl -> if filter hd then aux (map hd :: r) tl else aux r tl
+ in
+ aux [] l
+
+let read_dir file =
+ let filter name =
+ Filename.extension name = ".mrc"
+ in
+ let map name =
+ Filename.remove_extension name
+ in
+ let dir = Array.to_list (Sys.readdir file) in
+ let mods = List.fast_sort Pervasives.compare (list_rev_filter_map filter map dir) in
+ {
+ ET.cdir = file; mods;
+ }
+
+let rec read_mods mods ich =
+ let line = input_line ich in
+ let scan _ m =
+ mods := m :: !mods
+ in
+ Scanf.sscanf line "module %s = RecommGc%s" scan;
+ read_mods mods ich
+
+let read_index dir =
+ let file = Filename.concat dir "recommGc.ml" in
+ let mods = ref [] in
+ if Sys.file_exists file then begin
+ let ich = open_in file in
+ try read_mods mods ich with
+ | End_of_file -> close_in ich
+ end;
+ let mods = List.fast_sort Pervasives.compare !mods in
+ {
+ ET.cdir = dir; mods;
+ }
--- /dev/null
+val read_file: string -> MrcTypes.mrc_status
+
+val read_dir: string -> MrcTypes.idx_status
+
+val read_index: string -> MrcTypes.idx_status
--- /dev/null
+module ET = MrcTypes
+
+let cap = String.capitalize_ascii
+
+let ok b =
+ if b then "true" else "ok"
+
+let write_mli name =
+ let file = name ^ ".mli" in
+ if Sys.file_exists file then ()
+ else begin
+ let och = open_out file in
+ close_out och
+ end
+
+let write_subst st och subst =
+ let iter hd words =
+ let lhs = List.map (Printf.sprintf "%S :: ") words in
+ let rhs = List.map (Printf.sprintf "%S :: ") hd in
+ Printf.fprintf och " | %stl -> k %s (%souts) tl\n"
+ (String.concat "" lhs) (ok st.ET.para) (String.concat "" rhs)
+ in
+ match subst with
+ | [] -> ()
+ | hd :: _ -> List.iter (iter (List.rev hd)) subst
+
+let write_component st =
+ let cmod = "recommGc" ^ st.ET.cmod in
+ let och = open_out (cmod ^ ".ml") in
+ if st.ET.dmod <> "" then begin
+ Printf.fprintf och "module D = Recomm%s\n\n" (cap st.ET.dmod)
+ end;
+ Printf.fprintf och "let step k ok outs ins =\n";
+ Printf.fprintf och " if ok then k ok outs ins else\n";
+ Printf.fprintf och " match ins with\n";
+ List.iter (write_subst st och) st.ET.substs;
+ Printf.fprintf och " | _ -> k %s outs ins\n\n" (ok st.ET.optn);
+ Printf.fprintf och "let main =\n";
+ Printf.fprintf och " Recomm%s.register_%s step\n" (cap st.ET.rmod) st.ET.rfun;
+ close_out och;
+ write_mli cmod
+
+let write_index st =
+ let cmod = Filename.concat st.ET.cdir "recommGc" in
+ let och = open_out (cmod ^ ".ml") in
+ let iter i name =
+ Printf.fprintf och "module G%u = RecommGc%s\n" (succ i) name
+ in
+ List.iteri iter st.ET.mods;
+ close_out och;
+ write_mli cmod
--- /dev/null
+val write_component: MrcTypes.mrc_status -> unit
+
+val write_index: MrcTypes.idx_status -> unit
--- /dev/null
+type word = string
+
+type words = word list
+
+type subst = words list
+
+type substs = subst list
+
+type mrc_status = {
+(* component module *)
+ cmod : string;
+(* register module *)
+ rmod : string;
+(* register function *)
+ rfun : string;
+(* optional depend module *)
+ dmod : string;
+(* parallel component *)
+ para : bool;
+(* optional component *)
+ optn : bool;
+(* substitutions *)
+ substs : substs;
+}
+
+type idx_status = {
+(* indexed directory *)
+ cdir: string;
+(* indexed modules *)
+ mods: string list;
+}
--- /dev/null
+module EC = RecommCheck
+module EL = RecommLexer
+module EI = RecommInput
+module EO = RecommOutput
+
+module P1 = RecommPccFor
+module P2 = RecommPcsAnd
+
+module G = RecommGc
+
+let write = ref false
+
+let chdir path =
+ Sys.chdir path
+
+let rec process path name =
+ let file = Filename.concat path name in
+ if Sys.is_directory file then begin
+ let dir = Sys.readdir file in
+ Array.iter (process file) dir
+ end else
+ if Filename.extension file = ".ma" then begin
+ Printf.eprintf "processing: %S\n" file;
+ let orig = EI.read_srcs file in
+ let lint = EC.recomm_srcs orig in
+ if !write && lint <> orig then EO.write_srcs file lint
+ end else begin
+ Printf.eprintf "skipping: %S\n" file
+ end
+
+let msg_C = "<dir> Set this working directory (default: .)"
+let msg_L = " Log lexer tokens (default: no)"
+let msg_c = "<int> Set these output columns (default: 78)"
+let msg_d = " Log with dark colors (default: no)"
+let msg_k = " Log key comments (default: no)"
+let msg_m = " Log mark comments (default: no)"
+let msg_n = " Log with no colors (default: yes)"
+let msg_o = " Log other comments (default: no)"
+let msg_s = " Log section comments (default: no)"
+let msg_t = " Log title comments (default: no)"
+let msg_w = " Write the output files (default: no)"
+
+let main =
+ Arg.parse [
+ "-C", Arg.String chdir, msg_C;
+ "-L", Arg.Set EL.debug, msg_m;
+ "-c", Arg.Int ((:=) EO.width), msg_c;
+ "-d", Arg.Clear EC.bw, msg_d;
+ "-k", Arg.Set EC.log_k, msg_k;
+ "-m", Arg.Set EC.log_m, msg_m;
+ "-n", Arg.Set EC.bw, msg_n;
+ "-o", Arg.Set EC.log_o, msg_o;
+ "-s", Arg.Set EC.log_s, msg_s;
+ "-t", Arg.Set EC.log_t, msg_t;
+ "-w", Arg.Set write, msg_w;
+ ] (process "") ""
--- /dev/null
+module ES = RecommStep
+module ET = RecommTypes
+
+let c_line = ref ES.id
+
+let s_line = ref ES.id
+
+let k_final b ws1 ws2 = b, ws1, ws2
+
+type status =
+ {
+ r: ET.srcs; (* reversed result *)
+ }
+
+let init () =
+ {
+ r = [];
+ }
+
+let add src st =
+ {
+ r = src :: st.r;
+ }
+
+let middle st =
+ match st.r with
+ | []
+ | ET.Line _ :: _ -> false
+ | _ -> true
+
+let mute_o = [|
+ "___ ";
+ "||M|| ";
+ "||A|| A project by Andrea Asperti ";
+ "||T|| ";
+ "||I|| Developers: ";
+ "||T|| The HELM team. ";
+ "||A|| http://helm.cs.unibo.it ";
+ "\\ / ";
+ "\\ / This file is distributed under the terms of the ";
+ "v GNU General Public License Version 2 ";
+ "";
+|]
+
+let bw = ref false
+
+let log_k = ref false
+let log_m = ref false
+let log_o = ref false
+let log_s = ref false
+let log_t = ref false
+
+let no_color = "\x1B[0m"
+let black = "\x1B[30m"
+let sky = "\x1B[38;2;0;96;128m"
+let blue = "\x1B[34m"
+let prune = "\x1B[38;2;96;0;128m"
+let red = "\x1B[31m"
+
+let log color s =
+ if !bw then Printf.printf "%S\n" s else
+ Printf.printf "%s%S%s\n" color s no_color
+
+let rec recomm srcs st =
+ match srcs with
+ | [] ->
+ st
+ | ET.Line _ as hd :: tl ->
+ recomm tl @@ add hd @@ st
+ | ET.Text _ as hd :: tl ->
+ recomm tl @@ add hd @@ st
+ | ET.Mark s as hd :: tl ->
+ if !log_m then log red s;
+ recomm tl @@ add hd @@ st
+ | ET.Key (s1, s2) as hd :: tl ->
+ if middle st then Printf.eprintf "middle: %S\n" s1;
+ if !log_k then log prune (s1^s2);
+ recomm tl @@ add hd @@ st
+ | ET.Title ss as hd :: tl ->
+ if middle st then Printf.eprintf "middle: TITLE\n";
+ let b, ss1, ss2 = !c_line k_final false [] ss in
+ let ss2 =
+ if ss2 = [] then ss2 else "*" :: ss2
+ in
+ let ss = List.rev_append ss1 ss2 in
+ let s = String.concat " " ss in
+ if !log_t then log blue s;
+ recomm tl @@ add hd @@ st
+ | ET.Slice ss as hd :: tl ->
+ if middle st then Printf.eprintf "middle: Section\n";
+ let b, ss1, ss2 = !s_line k_final false [] ss in
+ let ss2 =
+ if ss2 = [] then ss2 else "*" :: ss2
+ in
+ let ss = List.rev_append ss1 ss2 in
+ let s = String.capitalize_ascii (String.concat " " ss) in
+ if !log_s then log sky s;
+ recomm tl @@ add hd @@ st
+ | ET.Other (_, s, _) as hd :: tl ->
+ if !log_o && not (Array.mem s mute_o) then log black s;
+ recomm tl @@ add hd @@ st
+
+let recomm_srcs srcs =
+ let st = recomm srcs @@ init () in
+ List.rev st.r
+
+let register_c = ES.register c_line
+
+let register_s = ES.register s_line
--- /dev/null
+val log_k: bool ref
+
+val log_m: bool ref
+
+val log_o: bool ref
+
+val log_s: bool ref
+
+val log_t: bool ref
+
+val bw: bool ref
+
+val register_c: RecommTypes.step -> unit
+
+val register_s: RecommTypes.step -> unit
+
+val recomm_srcs: RecommTypes.srcs -> RecommTypes.srcs
--- /dev/null
+module G1 = RecommGcbGroundCounters
+module G2 = RecommGcdGroundCounters
+module G3 = RecommGcsAttr
+module G4 = RecommGcsMain
+module G5 = RecommGcsWith
--- /dev/null
+let step k ok outs ins =
+ if ok then k ok outs ins else
+ match ins with
+ | "rtc_ist" :: tl -> k true ("rtc_ist" :: outs) tl
+ | "test" :: "for" :: "t-transition" :: "counter" :: tl -> k true ("rtc_ist" :: outs) tl
+ | "rtc_ism" :: tl -> k true ("rtc_ism" :: outs) tl
+ | "test" :: "for" :: "constrained" :: "rt-transition" :: "counter" :: tl -> k true ("rtc_ism" :: outs) tl
+ | "rtc_shift" :: tl -> k true ("rtc_shift" :: outs) tl
+ | "shift" :: tl -> k true ("rtc_shift" :: outs) tl
+ | "rtc_max" :: tl -> k true ("rtc_max" :: outs) tl
+ | "max" :: tl -> k true ("rtc_max" :: outs) tl
+ | _ -> k ok outs ins
+
+let main =
+ RecommPcsAnd.register_b step
--- /dev/null
+let step k ok outs ins =
+ if ok then k ok outs ins else
+ match ins with
+ | "T-TRANSITION" :: "COUNTERS" :: tl -> k true ("COUNTERS" :: "T-TRANSITION" :: outs) tl
+ | "T-TRANSITION" :: "COUNTER" :: tl -> k true ("COUNTERS" :: "T-TRANSITION" :: outs) tl
+ | "T-BOUND" :: "RT-TRANSITION" :: "COUNTERS" :: tl -> k true ("COUNTERS" :: "RT-TRANSITION" :: "T-BOUND" :: outs) tl
+ | "RT-TRANSITION" :: "COUNTER" :: tl -> k true ("COUNTERS" :: "RT-TRANSITION" :: "T-BOUND" :: outs) tl
+ | _ -> k ok outs ins
+
+let main =
+ RecommPccFor.register_d step
--- /dev/null
+let step k ok outs ins =
+ if ok then k ok outs ins else
+ match ins with
+ | "main" :: tl -> k ok ("main" :: outs) tl
+ | "basic" :: tl -> k ok ("basic" :: outs) tl
+ | "advanced" :: tl -> k ok ("advanced" :: outs) tl
+ | _ -> k ok outs ins
+
+let main =
+ RecommCheck.register_s step
--- /dev/null
+module D = RecommGcsAttr
+
+let step k ok outs ins =
+ if ok then k ok outs ins else
+ match ins with
+ | "eliminations" :: tl -> k ok ("eliminations" :: outs) tl
+ | "eliminators" :: tl -> k ok ("eliminations" :: outs) tl
+ | "destructions" :: tl -> k ok ("destructions" :: outs) tl
+ | "forward" :: "properties" :: tl -> k ok ("destructions" :: outs) tl
+ | "forward" :: "lemmas" :: tl -> k ok ("destructions" :: outs) tl
+ | "inversions" :: tl -> k ok ("inversions" :: outs) tl
+ | "inversion" :: "properties" :: tl -> k ok ("inversions" :: outs) tl
+ | "inversion" :: "lemmas" :: tl -> k ok ("inversions" :: outs) tl
+ | "constructions" :: tl -> k ok ("constructions" :: outs) tl
+ | "properties" :: tl -> k ok ("constructions" :: outs) tl
+ | _ -> k true outs ins
+
+let main =
+ RecommCheck.register_s step
--- /dev/null
+module D = RecommGcsMain
+
+let step k ok outs ins =
+ if ok then k ok outs ins else
+ match ins with
+ | "with" :: tl -> k ok ("with" :: outs) tl
+ | _ -> k true outs ins
+
+let main =
+ RecommCheck.register_s step
--- /dev/null
+module EL = RecommLexer
+module EP = RecommParser
+
+let read_srcs file =
+ let ich = open_in file in
+ let lexbuf = Lexing.from_channel ich in
+ let srcs = EP.srcs EL.src_token lexbuf in
+ close_in ich;
+ srcs
--- /dev/null
+val read_srcs: string -> RecommTypes.srcs
--- /dev/null
+{
+ module EP = RecommParser
+
+ let debug = ref false
+
+ let keys = [|
+ "Note";
+ |]
+
+ let heads = [|
+ "Advanved";
+ "Basic";
+ "Forward";
+ "Destructions";
+ "Eliminations";
+ "Eliminators";
+ "Inversion";
+ "Inversions";
+ "Main";
+ "Properties";
+ |]
+
+ let str c = String.make 1 c
+
+ let nl lexbuf = Lexing.new_line lexbuf
+
+ let is_uppercase_ascii s =
+ let rec aux i =
+ if i < 0 then true else
+ if 'a' <= s.[i] && s.[i] <= 'z' then false else
+ aux (pred i)
+ in
+ aux (String.length s - 1)
+
+ let disambiguate_word s =
+ if is_uppercase_ascii s then EP.CW s else
+ if Array.mem s keys then EP.KW s else
+ if Array.mem s heads then EP.HW s else
+ EP.SW s
+
+ let log s =
+ if !debug then Printf.eprintf "lezer: %s\n" s
+
+ let log_s s =
+ if !debug then Printf.eprintf "lexer: %S\n" s
+
+ let log_c c =
+ if !debug then Printf.eprintf "lexer: %C\n" c
+}
+
+let CR = "\r"
+let SP = " "
+let NL = "\n"
+let SR = "*"
+let OP = "(*" SP*
+let CP = SR* "*)"
+let PP = CP SP* OP
+let WF = ['A'-'Z' 'a'-'z']
+let WB = ['A'-'Z' 'a'-'z' '_' '-']*
+let WD = WF WB
+
+rule src_token = parse
+ | CR { src_token lexbuf }
+ | NL as c { log "NL"; nl lexbuf; EP.NL (str c) }
+ | SP+ as s { log "SP"; EP.SP s }
+ | PP as s { log "PP"; EP.PP s }
+ | OP as s { log "OP"; EP.OP s }
+ | CP as s { log "CP"; EP.CP s }
+ | SR as c { log "SR"; EP.SR (str c) }
+ | WD as s { log_s s ; disambiguate_word s }
+ | _ as c { log_c c ; EP.OT (str c) }
+ | eof { log "EF"; EP.EF }
--- /dev/null
+module ET = RecommTypes
+
+let width = ref 78
+
+let complete s =
+ let l = !width - String.length s - 6 in
+ if l < 0 then begin
+ Printf.eprintf "overfull: %S\n" s;
+ ""
+ end else begin
+ String.make l '*'
+ end
+
+let out_src och = function
+ | ET.Line s ->
+ Printf.fprintf och "%s" s
+ | ET.Text s ->
+ Printf.fprintf och "%s" s
+ | ET.Mark s ->
+ Printf.fprintf och "(* %s**)" s
+ | ET.Key (s1, s2) ->
+ Printf.fprintf och "(* %s1%s2*)" s1 s2
+ | ET.Title ss ->
+ let s = String.concat " " ss in
+ Printf.fprintf och "(* %s %s*)" s (complete s)
+ | ET.Slice ss ->
+ let s = String.capitalize_ascii (String.concat " " ss) in
+ Printf.fprintf och "(* %s %s*)" s (complete s)
+ | ET.Other (s1, s2, s3) ->
+ Printf.fprintf och "%s%s%s" s1 s2 s3
+
+let write_srcs file srcs =
+ let och = open_out (file ^ ".new") in
+ List.iter (out_src och) srcs;
+ close_out och
--- /dev/null
+val width: int ref
+
+val write_srcs: string -> RecommTypes.srcs -> unit
--- /dev/null
+%{
+
+ module ET = RecommTypes
+
+ let lc = String.lowercase_ascii
+
+%}
+
+%token <string> SP NL OP CP PP SR KW CW HW SW OT
+%token EF
+
+%start srcs
+%type <RecommTypes.srcs> srcs
+
+%%
+
+inn_r:
+ | SP { $1 }
+ | NL { $1 }
+ | SW { $1 }
+ | OT { $1 }
+
+inn:
+ | inn_r { $1 }
+ | KW { $1 }
+ | CW { $1 }
+ | HW { $1 }
+
+inns_r:
+ | inn_r { $1 }
+ | inn_r inns { $1 ^ $2 }
+
+inns:
+ | inn { $1 }
+ | inn inns { $1 ^ $2 }
+
+out:
+ | SP { $1 }
+ | SR { $1 }
+ | KW { $1 }
+ | CW { $1 }
+ | HW { $1 }
+ | SW { $1 }
+ | OT { $1 }
+
+outs:
+ | out { $1 }
+ | out outs { $1 ^ $2 }
+
+sw:
+ | HW { lc $1 }
+ | SW { lc $1 }
+
+cws:
+ | { [] }
+ | SP { [] }
+ | SP CW cws { $2 :: $3 }
+
+sws:
+ | { [] }
+ | SP { [] }
+ | SP sw sws { $2 :: $3 }
+
+src_l:
+ | NL { ET.Line $1 }
+ | OP PP inns CP { ET.Mark $3 }
+ | OP KW inns CP { ET.Key ($2, $3) }
+ | OP CW cws CP { ET.Title ($2 :: $3) }
+ | OP HW sws CP { ET.Slice (lc $2 :: $3) }
+ | OP CP { ET.Other ($1, "", $2) }
+ | OP inns_r CP { ET.Other ($1, $2, $3) }
+ | OP SR inns CP { ET.Other ($1, $2 ^ $3, $4) }
+ | OP SR SR inns CP { ET.Other ($1, $2 ^ $3 ^ $4, $5) }
+
+src:
+ | outs { ET.Text $1 }
+
+srcs_l:
+ | EF { [] }
+ | src_l srcs { $1 :: $2 }
+
+srcs:
+ | srcs_l { $1 }
+ | src srcs_l { $1 :: $2 }
--- /dev/null
+module EC = RecommCheck
+module ES = RecommStep
+
+let d_line = ref ES.id
+
+let r_line = ref ES.id
+
+let k_for k ok outs ins =
+ if ok then begin
+ match ins with
+ | "for" :: tl -> !d_line k false ("for" :: outs) tl
+ | _ -> k true outs ins
+ end else begin
+ k true outs ins
+ end
+
+let k_or k ok outs ins =
+ if ok then k ok outs ins else
+ !r_line (k_for k) ok outs ins
+
+let step k ok outs ins =
+ if ok then k ok outs ins else
+ !d_line (k_or k) ok outs ins
+
+let register_d =
+ ES.register d_line
+
+let register_r =
+ ES.register r_line
+
+let main =
+ EC.register_c step
--- /dev/null
+val register_d: RecommTypes.step -> unit
+
+val register_r: RecommTypes.step -> unit
--- /dev/null
+module EC = RecommCheck
+module ES = RecommStep
+
+module D = RecommGcsWith
+
+let b_line = ref ES.id
+
+let rec k_and k ok outs ins =
+ if ok then begin
+ match ins with
+ | "and" :: tl -> step k false ("and" :: outs) tl
+ | _ -> k true outs ins
+ end else begin
+ k true outs ins
+ end
+
+and step k ok outs ins =
+ if ok then k ok outs ins else
+ !b_line (k_and k) ok outs ins
+
+let register_b =
+ ES.register b_line
+
+let main =
+ EC.register_s step
--- /dev/null
+val register_b: RecommTypes.step -> unit
--- /dev/null
+let id p = p
+
+let register line next =
+ let first = !line in
+ line := fun k -> first @@ next @@ k
--- /dev/null
+val id: ('s, 't) RecommTypes.astep
+
+val register: ('s, 't) RecommTypes.astep ref -> ('s, 't) RecommTypes.astep -> unit
+
--- /dev/null
+type text = string
+
+type word = string
+
+type words = word list
+
+type src =
+(* end of line *)
+ | Line of text
+(* other text *)
+ | Text of text
+(* mark *)
+ | Mark of text
+(* Key *)
+ | Key of word * text
+(* title *)
+ | Title of words
+(* section *)
+ | Slice of words
+(* other comment *)
+ | Other of text * text * text
+
+type srcs = src list
+
+type ('s, 't) aproc = 's -> words -> words -> 't
+
+type ('s, 't) astep = ('s, 't) aproc -> ('s, 't) aproc
+
+type step = (bool, bool * words * words) astep
--- /dev/null
+check s "" false false
+advanced
+basic
+main
--- /dev/null
+check s "GcsAttr" false true
+constructions, properties
+inversions, inversion properties, inversion lemmas
+destructions, forward properties, forward lemmas
+eliminations, eliminators
--- /dev/null
+check s "GcsMain" false true
+with
definition isrt: relation2 nat rtc ≝ λts,c.
∃∃ri,rs. 〈ri,rs,0,ts〉 = c.
-interpretation "test for costrained rt-transition counter (rtc)"
+interpretation "test for constrained rt-transition counter (rtc)"
'IsRedType ts c = (isrt ts c).
(* Basic properties *********************************************************)
(* RT-TRANSITION COUNTER ****************************************************)
-(* Properties with test for costrained rt-transition counter ****************)
+(* Properties with test for constrained rt-transition counter ***************)
lemma isr_shift: ∀c. 𝐑𝐓❪0,c❫ → 𝐑𝐓❪0,↕*c❫.
#c * #ri #rs #H destruct /2 width=3 by ex1_2_intro/
qed.
-(* Inversion properties with test for costrained rt-counter *****************)
+(* Inversion properties with test for constrained rt-transition counter *****)
lemma isrt_inv_shift: ∀n,c. 𝐑𝐓❪n,↕*c❫ → 𝐑𝐓❪0,c❫ ∧ 0 = n.
#n #c * #ri #rs #H
projects / helm.git / commitdiff