From ad17757edcc6cf75be576268fab8cf52751d679a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 15 Nov 2006 19:47:41 +0000 Subject: [PATCH] transcript updated --- components/METAS/meta.helm-tactics.src | 2 +- components/binaries/transcript/CoRN.conf.xml | 3 +- components/binaries/transcript/Makefile | 15 +++++- components/binaries/transcript/engine.ml | 38 +++++++++++--- components/binaries/transcript/grafite.ml | 32 +++++++++--- components/binaries/transcript/grafite.mli | 2 + components/binaries/transcript/types.ml | 3 +- components/binaries/transcript/v8Lexer.mll | 3 +- components/binaries/transcript/v8Parser.mly | 52 ++++++++++---------- components/extlib/hExtlib.ml | 11 +++++ components/extlib/hExtlib.mli | 1 + components/tactics/equalityTactics.ml | 5 +- components/tactics/fwdSimplTactic.ml | 3 +- components/tactics/proofEngineHelpers.ml | 11 ----- components/tactics/proofEngineHelpers.mli | 2 - 15 files changed, 121 insertions(+), 62 deletions(-) diff --git a/components/METAS/meta.helm-tactics.src b/components/METAS/meta.helm-tactics.src index 6e704ba06..5f620680a 100644 --- a/components/METAS/meta.helm-tactics.src +++ b/components/METAS/meta.helm-tactics.src @@ -1,4 +1,4 @@ -requires="helm-cic_proof_checking helm-cic_unification helm-whelp" +requires="helm-extlib helm-cic_proof_checking helm-cic_unification helm-whelp" version="0.0.1" archive(byte)="tactics.cma" archive(native)="tactics.cmxa" diff --git a/components/binaries/transcript/CoRN.conf.xml b/components/binaries/transcript/CoRN.conf.xml index e952b23e4..6be3a5634 100644 --- a/components/binaries/transcript/CoRN.conf.xml +++ b/components/binaries/transcript/CoRN.conf.xml @@ -2,7 +2,8 @@
CoRN - cic:/matita/CoRN-Decl + cic:/CoRN + cic:/matita/CoRN-Decl /projects/helm/exportation/CoRN $(transcript.helm_dir)/matita/contribs/CoRN-Decl .v diff --git a/components/binaries/transcript/Makefile b/components/binaries/transcript/Makefile index 87f9ea0a3..1252d345f 100644 --- a/components/binaries/transcript/Makefile +++ b/components/binaries/transcript/Makefile @@ -21,7 +21,8 @@ OCAMLLEX = ocamllex all: transcript .depend @echo -n -opt: transcript.opt $(EXTRAS) .depend + +opt: transcript.opt $(EXTRAS) .depend.opt #echo -n transcript: $(CMIS) $(CMOS) $(EXTRAS) @@ -40,6 +41,10 @@ clean: @echo " OCAMLDEP $(MLIS) $(MLS)" $(H)$(OCAMLDEP) $(MLIS) $(MLS) > .depend +.depend.opt: $(MLIS) $(MLS) $(EXTRAS) + @echo " OCAMLDEP -native $(MLIS) $(MLS)" + $(H)$(OCAMLDEP) -native $(MLIS) $(MLS) > .depend.opt + test: transcript transcript.conf.xml $(PACKAGES:%=%.conf.xml) @echo " TRANSCRIPT $(PACKAGES)" $(H)$< $(PACKAGES) @@ -53,7 +58,9 @@ export: clean @echo " TAR transcript" $(H)cd .. && tar --exclude=transcript/.svn -czf transcript.tgz transcript -depend: .depend +depend: .depend + +depend.opt: .depend.opt %.cmi: %.mli $(EXTRAS) @echo " OCAMLC $<" @@ -73,6 +80,10 @@ depend: .depend include ../../../Makefile.defs +ifeq ($(MAKECMDGOALS), opt) + include .depend.opt +endif + ifeq ($(MAKECMDGOALS), all) include .depend endif diff --git a/components/binaries/transcript/engine.ml b/components/binaries/transcript/engine.ml index 92c3c73b4..e0d62a8cb 100644 --- a/components/binaries/transcript/engine.ml +++ b/components/binaries/transcript/engine.ml @@ -24,10 +24,13 @@ *) module R = Helm_registry +module X = HExtlib +module T = Types +module G = Grafite type script = { name: string; - contents: Types.items + contents: T.items } type status = { @@ -35,7 +38,8 @@ type status = { heading_path: string; heading_lines: int; package: string; - base_uri: string; + input_base_uri: string; + output_base_uri: string; input_path: string; output_path: string; script_ext: string; @@ -89,7 +93,8 @@ let make registry = heading_path = R.get_string "transcript.heading_path"; heading_lines = R.get_int "transcript.heading_lines"; package = R.get_string "package.name"; - base_uri = R.get_string "package.base_uri"; + input_base_uri = R.get_string "package.input_base_uri"; + output_base_uri = R.get_string "package.output_base_uri"; input_path = R.get_string "package.input_path"; output_path = R.get_string "package.output_path"; script_ext = R.get_string "package.script_type"; @@ -120,11 +125,11 @@ let set_items st name items = let set_heading st name = let heading = Filename.concat st.helm_dir st.heading_path, st.heading_lines in - set_items st name [Types.Heading heading] + set_items st name [T.Heading heading] let set_baseuri st name = - let baseuri = Filename.concat st.base_uri name in - set_items st name [Types.BaseUri baseuri] + let baseuri = Filename.concat st.output_base_uri name in + set_items st name [T.BaseUri baseuri] let commit st name = let i = get_index st name in @@ -134,13 +139,25 @@ let commit st name = let cmd = Printf.sprintf "mkdir -p %s" path in let _ = Sys.command cmd in let och = open_out name in - Grafite.commit och script.contents; + G.commit och script.contents; close_out och; st.scripts.(i) <- default_script let produce st = let init name = set_heading st name; set_baseuri st name in + let partition = function + | T.Coercion _ + | T.Notation _ -> false + | _ -> true + in let produce st name = + let base_uri = Filename.concat st.input_base_uri name in + let filter = function + | T.Inline (k, obj) -> + let s = obj ^ G.string_of_inline_kind k in + Some (T.Inline (k, Filename.concat base_uri s)) + | item -> Some item + in Printf.eprintf "processing file name: %s ...\n" name; flush stderr; let file = Filename.concat st.input_path (name ^ st.script_ext) in let ich = open_in file in @@ -148,7 +165,12 @@ let produce st = try let items = V8Parser.items V8Lexer.token lexbuf in close_in ich; - init name; set_items st name items; commit st name + let items = List.rev (X.list_rev_map_filter filter items) in + let local_items, global_items = List.partition partition items in + let comment = T.Line (Printf.sprintf "From %s" name) in + if global_items <> [] then + set_items st st.package (comment :: global_items); + init name; set_items st name local_items; commit st name with e -> prerr_endline (Printexc.to_string e); close_in ich in diff --git a/components/binaries/transcript/grafite.ml b/components/binaries/transcript/grafite.ml index 9900b8bc8..374d3bda6 100644 --- a/components/binaries/transcript/grafite.ml +++ b/components/binaries/transcript/grafite.ml @@ -36,11 +36,17 @@ let out_verbatim och s = Printf.fprintf och "%s" s let out_comment och s = + let s = if s <> "" && s.[0] = '*' then "#" ^ s else s in Printf.fprintf och "%s%s%s\n\n" "(*" s "*)" +let out_unexported och head s = + let s = Printf.sprintf " %s\n%s\n" head s in + out_comment och s + let out_line_comment och s = let l = 70 - String.length s in - Printf.fprintf och "%s %s %s%s\n\n" "(*" s (String.make l '*') "*)" + let s = Printf.sprintf " %s %s" s (String.make l '*') in + out_comment och s let out_preamble och (path, lines) = let ich = open_in path in @@ -62,23 +68,35 @@ let out_command och cmd = let command_of_obj obj = G.Executable (floc, G.Command (floc, obj)) +let command_of_macro macro = + G.Executable (floc, G.Macro (floc, macro)) + let set key value = command_of_obj (G.Set (floc, key, value)) let require value = command_of_obj (G.Include (floc, value ^ ".ma")) +let inline value = + command_of_macro (G.Inline (floc, value)) + let commit och items = let commit = function | T.Heading heading -> out_preamble och heading + | T.Line line -> out_line_comment och line | T.BaseUri baseuri -> out_command och (set "baseuri" baseuri) - | T.Include inc -> () (* *) - | T.Coercion coercion -> () (* *) - | T.Notation notation -> () (* *) - | T.Inline iniline -> () (* *) - | T.Comment comment -> () (* out_comment och comment *) - | T.Unexport unexport -> () (* *) + | T.Include inc -> out_unexported och "INCLUDE" inc (**) + | T.Coercion coercion -> out_unexported och "COERCION" coercion (**) + | T.Notation notation -> out_unexported och "NOTATION" notation (**) + | T.Inline (_, uri) -> out_command och (inline uri) + | T.Comment comment -> out_comment och comment + | T.Unexport unexport -> out_unexported och "UNEXPORTED" unexport | T.Verbatim verbatim -> out_verbatim och verbatim | T.Discard _ -> () in List.iter commit (List.rev items) + +let string_of_inline_kind = function + | T.Con -> ".con" + | T.Var -> ".var" + | T.Ind -> ".ind" diff --git a/components/binaries/transcript/grafite.mli b/components/binaries/transcript/grafite.mli index b0b5fcafc..53aff6990 100644 --- a/components/binaries/transcript/grafite.mli +++ b/components/binaries/transcript/grafite.mli @@ -24,3 +24,5 @@ *) val commit: out_channel -> Types.items -> unit + +val string_of_inline_kind: Types.inline_kind -> string diff --git a/components/binaries/transcript/types.ml b/components/binaries/transcript/types.ml index d7770ade7..e51122b3f 100644 --- a/components/binaries/transcript/types.ml +++ b/components/binaries/transcript/types.ml @@ -26,7 +26,8 @@ type inline_kind = Con | Ind | Var type item = Heading of (string * int) - | Comment of string + | Line of string + | Comment of string | Unexport of string | BaseUri of string | Include of string diff --git a/components/binaries/transcript/v8Lexer.mll b/components/binaries/transcript/v8Lexer.mll index cddb728bd..0fea9c9eb 100644 --- a/components/binaries/transcript/v8Lexer.mll +++ b/components/binaries/transcript/v8Lexer.mll @@ -5,7 +5,7 @@ } let QT = '"' -let SPC = [' ' '\t' '\n']+ +let SPC = [' ' '\t' '\n' '\r']+ let ALPHA = ['A'-'Z' 'a'-'z' '_'] let FIG = ['0'-'9'] let ID = ALPHA (ALPHA | FIG | "\'")* @@ -56,6 +56,7 @@ rule token = parse | RAWID { let s = Lexing.lexeme lexbuf in out "STR" s; P.STR s } | NUM { let s = Lexing.lexeme lexbuf in out "INT" s; P.INT s } | ":=" { let s = Lexing.lexeme lexbuf in out "DEF" s; P.DEF s } + | ":>" { let s = Lexing.lexeme lexbuf in out "COE" s; P.COE s } | "." ID { let s = Lexing.lexeme lexbuf in out "AC" s; P.AC s } | "." SPC { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s } | "." eof { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s } diff --git a/components/binaries/transcript/v8Parser.mly b/components/binaries/transcript/v8Parser.mly index 9529bfb62..7fd69615d 100644 --- a/components/binaries/transcript/v8Parser.mly +++ b/components/binaries/transcript/v8Parser.mly @@ -28,10 +28,14 @@ let out t s = () (* prerr_endline ("-- " ^ t ^ " " ^ s) *) + let trim = HExtlib.trim_blanks + + let hd = List.hd + let cat x = String.concat " " x let mk_vars idents = - let map ident = T.Inline (T.Var, ident) in + let map ident = T.Inline (T.Var, trim ident) in List.map map idents let strip2 s = @@ -39,8 +43,6 @@ let strip1 s = String.sub s 1 (String.length s - 1) - - let hd = List.hd %} %token SPC STR IDENT INT EXTRA AC OP CP OC CC OQ CQ DEF FS COE CN SC %token LET IN TH PROOF QED VAR IND SEC REQ XP IP SET NOT LOAD ID COERC @@ -242,47 +244,47 @@ macro_step: | th ident restricts fs proof FS steps qed FS - { out "TH" $2; $7 @ [T.Inline (T.Con, $2)] } + { out "TH" $2; $7 @ [T.Inline (T.Con, trim $2)] } | th ident restricts fs proof restricts FS - { out "TH" $2; [T.Inline (T.Con, $2)] } + { out "TH" $2; [T.Inline (T.Con, trim $2)] } | th ident restricts fs steps qed FS - { out "TH" $2; $5 @ [T.Inline (T.Con, $2)] } + { out "TH" $2; $5 @ [T.Inline (T.Con, trim $2)] } | th ident restricts def restricts FS - { out "TH" $2; [T.Inline (T.Con, $2)] } + { out "TH" $2; [T.Inline (T.Con, trim $2)] } | th ident def restricts FS - { out "TH" $2; [T.Inline (T.Con, $2)] } + { out "TH" $2; [T.Inline (T.Con, trim $2)] } | var idents xres FS - { out "VAR" (cat $2); mk_vars $2 } + { out "VAR" (cat $2); mk_vars $2 } | ind ident unexports FS - { out "IND" $2; snd $3 @ [T.Inline (T.Ind, $2)] } + { out "IND" $2; snd $3 @ [T.Inline (T.Ind, trim $2)] } | sec unexports FS - { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ $3)] } + { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] } | req xp ident FS - { out "REQ" $3; [T.Include $3] } + { out "REQ" $3; [T.Include (trim $3)] } | req ip ident FS - { out "REQ" $3; [T.Include $3] } + { out "REQ" $3; [T.Include (trim $3)] } | req ident FS - { out "REQ" $2; [T.Include $2] } + { out "REQ" $2; [T.Include (trim $2)] } | load str FS - { out "REQ" $2; [T.Include (strip2 $2)] } + { out "REQ" $2; [T.Include (strip2 (trim $2))] } | coerc qid spcs cn unexports FS - { out "COERCE" (hd $2); [T.Coercion (hd $2)] } + { out "COERCE" (hd $2); [T.Coercion (hd $2)] } | id coerc qid spcs cn unexports FS - { out "COERCE" (hd $3); [T.Coercion (hd $3)] } + { out "COERCE" (hd $3); [T.Coercion (hd $3)] } | th ident error - { out "ERROR" $2; failwith ("macro_step " ^ $2) } + { out "ERROR" $2; failwith ("macro_step " ^ $2) } | ind ident error - { out "ERROR" $2; failwith ("macro_step " ^ $2) } + { out "ERROR" $2; failwith ("macro_step " ^ $2) } | var idents error { let vs = cat $2 in - out "ERROR" vs; failwith ("macro_step " ^ vs) } + out "ERROR" vs; failwith ("macro_step " ^ vs) } ; item: - | comment { [T.Comment $1] } - | macro_step { $1 } - | set unexports FS { [T.Unexport ($1 ^ fst $2 ^ $3)] } - | notation unexports FS { [T.Notation ($1 ^ fst $2 ^ $3)] } - | error { out "ERROR" "item"; failwith "item" } + | OQ verbatims CQ { [T.Comment $2] } + | macro_step { $1 } + | set unexports FS { [T.Unexport ($1 ^ fst $2 ^ trim $3)] } + | notation unexports FS { [T.Notation ($1 ^ fst $2 ^ trim $3)] } + | error { out "ERROR" "item"; failwith "item" } ; items: | rspcs EOF { [] } diff --git a/components/extlib/hExtlib.ml b/components/extlib/hExtlib.ml index c0364315a..d4572789a 100644 --- a/components/extlib/hExtlib.ml +++ b/components/extlib/hExtlib.ml @@ -153,6 +153,17 @@ let rec filter_map f = | None -> filter_map f tl | Some v -> v :: filter_map f tl) +let list_rev_map_filter f l = + let rec aux a = function + | [] -> a + | hd :: tl -> + begin match f hd with + | None -> aux a tl + | Some b -> aux (b :: a) tl + end + in + aux [] l + let list_concat ?(sep = []) = let rec aux acc = function diff --git a/components/extlib/hExtlib.mli b/components/extlib/hExtlib.mli index 0c2206a08..907259a8f 100644 --- a/components/extlib/hExtlib.mli +++ b/components/extlib/hExtlib.mli @@ -75,6 +75,7 @@ val trim_blanks: string -> string (** strip heading and trailing blanks *) val list_uniq: ?eq:('a->'a->bool) -> 'a list -> 'a list (** uniq unix filter on lists *) val filter_map: ('a -> 'b option) -> 'a list -> 'b list (** filter + map *) +val list_rev_map_filter: ('a -> 'b option) -> 'a list -> 'b list val list_concat: ?sep:'a list -> 'a list list -> 'a list (**String.concat-like*) val list_findopt: ('a -> 'b option) -> 'a list -> 'b option val flatten_map: ('a -> 'b list) -> 'a list -> 'b list diff --git a/components/tactics/equalityTactics.ml b/components/tactics/equalityTactics.ml index 5a07e4e63..cd066250f 100644 --- a/components/tactics/equalityTactics.ml +++ b/components/tactics/equalityTactics.ml @@ -38,6 +38,7 @@ module S = CicSubstitution module TC = CicTypeChecker module LO = LibraryObjects module DTI = DoubleTypeInference +module HEL = HExtlib let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equality = let _rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status @@ -423,7 +424,7 @@ let subst_tac ~hyp = Some (rewrite (None, [(s, hole)], None)) | _ -> None in - let rew_hips = PEH.list_rev_map_filter (map hyp) context in + let rew_hips = HEL.list_rev_map_filter (map hyp) context in let rew_concl = rewrite (None, [], Some hole) in let clear = PESR.clear ~hyps:[hyp; var] in let tactics = List.rev_append (rew_concl :: rew_hips) [clear] in @@ -441,7 +442,7 @@ let subst_tac = let (proof, goal) = status in let (_, metasenv, _, _) = proof in let _, context, _ = CicUtil.lookup_meta goal metasenv in - let tactics = PEH.list_rev_map_filter map context in + let tactics = HEL.list_rev_map_filter map context in PET.apply_tactic (T.seq ~tactics) status in PET.mk_tactic subst_tac diff --git a/components/tactics/fwdSimplTactic.ml b/components/tactics/fwdSimplTactic.ml index ffc90c1cc..fa7d4aef1 100644 --- a/components/tactics/fwdSimplTactic.ml +++ b/components/tactics/fwdSimplTactic.ml @@ -35,6 +35,7 @@ module T = Tacticals module FNG = FreshNamesGenerator module MI = CicMkImplicit module PESR = ProofEngineStructuralRules +module HEL = HExtlib let fail_msg0 = "unexported clearbody: invalid argument" let fail_msg2 = "fwd: no applicable simplification" @@ -102,7 +103,7 @@ let get_clearables context terms = | Cic.Appl (Cic.Rel i :: _) -> PEH.get_name context i | _ -> None in - PEH.list_rev_map_filter aux terms + HEL.list_rev_map_filter aux terms let lapply_tac_aux ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) (* ?(substs = []) *) ?how_many ?(to_what = []) what = diff --git a/components/tactics/proofEngineHelpers.ml b/components/tactics/proofEngineHelpers.ml index 6e7b5a8e7..b4e9a4e94 100644 --- a/components/tactics/proofEngineHelpers.ml +++ b/components/tactics/proofEngineHelpers.ml @@ -689,17 +689,6 @@ let lookup_type metasenv context hyp = (* FG: **********************************************************************) -let list_rev_map_filter f l = - let rec aux a = function - | [] -> a - | hd :: tl -> - begin match f hd with - | None -> aux a tl - | Some b -> aux (b :: a) tl - end - in - aux [] l - let get_name context index = try match List.nth context (pred index) with | Some (Cic.Name name, _) -> Some name diff --git a/components/tactics/proofEngineHelpers.mli b/components/tactics/proofEngineHelpers.mli index 21628cba1..650271d5e 100644 --- a/components/tactics/proofEngineHelpers.mli +++ b/components/tactics/proofEngineHelpers.mli @@ -118,8 +118,6 @@ val lookup_type: Cic.metasenv -> Cic.context -> string -> int * Cic.term (* FG: some helper functions ************************************************) -val list_rev_map_filter: ('a -> 'b option) -> 'a list -> 'b list - val get_name: Cic.context -> int -> string option val get_rel: Cic.context -> string -> Cic.term option -- 2.39.2