-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"
<helm_registry>
<section name="package">
<key name="name">CoRN</key>
- <key name="base_uri">cic:/matita/CoRN-Decl</key>
+ <key name="input_base_uri">cic:/CoRN</key>
+ <key name="output_base_uri">cic:/matita/CoRN-Decl</key>
<key name="input_path">/projects/helm/exportation/CoRN</key>
<key name="output_path">$(transcript.helm_dir)/matita/contribs/CoRN-Decl</key>
<key name="script_type">.v</key>
all: transcript .depend
@echo -n
-opt: transcript.opt $(EXTRAS) .depend
+
+opt: transcript.opt $(EXTRAS) .depend.opt
#echo -n
transcript: $(CMIS) $(CMOS) $(EXTRAS)
@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)
@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 $<"
include ../../../Makefile.defs
+ifeq ($(MAKECMDGOALS), opt)
+ include .depend.opt
+endif
+
ifeq ($(MAKECMDGOALS), all)
include .depend
endif
*)
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 = {
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;
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";
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
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
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
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
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"
*)
val commit: out_channel -> Types.items -> unit
+
+val string_of_inline_kind: Types.inline_kind -> string
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
}
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 | "\'")*
| 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 }
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 =
let strip1 s =
String.sub s 1 (String.length s - 1)
-
- let hd = List.hd
%}
%token <string> SPC STR IDENT INT EXTRA AC OP CP OC CC OQ CQ DEF FS COE CN SC
%token <string> LET IN TH PROOF QED VAR IND SEC REQ XP IP SET NOT LOAD ID COERC
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 { [] }
| 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
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
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
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
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
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"
| 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 =
(* 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
(* 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
projects / helm.git / commitdiff