From 885b29af55a246589b6a8966d9d1438fbb8155d3 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 29 Nov 2006 17:23:59 +0000 Subject: [PATCH] - decompose tactic: decomposable constants are now allowed (they are unfolded) - inline macro: now accepts an optional name prefix for disambiguation purposes - transcript: now handles local objects correctly --- components/binaries/transcript/.depend.opt | 12 +++ components/binaries/transcript/engine.ml | 36 +++++--- components/binaries/transcript/grafite.ml | 9 +- components/binaries/transcript/types.ml | 7 +- components/binaries/transcript/v8Lexer.mll | 24 ++--- components/binaries/transcript/v8Parser.mly | 97 +++++++++++++++------ components/extlib/hExtlib.ml | 11 +++ components/extlib/hExtlib.mli | 1 + components/grafite/grafiteAst.ml | 2 +- components/grafite/grafiteAstPp.ml | 3 +- components/grafite_engine/grafiteEngine.ml | 2 +- components/grafite_parser/grafiteParser.ml | 5 +- components/tactics/eliminationTactics.ml | 69 +++++++++------ components/tactics/eliminationTactics.mli | 2 +- components/tactics/proofEngineTypes.ml | 2 +- components/tactics/tactics.mli | 16 ++-- components/whelp/fwdQueries.ml | 4 +- components/whelp/fwdQueries.mli | 2 +- 18 files changed, 206 insertions(+), 98 deletions(-) create mode 100644 components/binaries/transcript/.depend.opt diff --git a/components/binaries/transcript/.depend.opt b/components/binaries/transcript/.depend.opt new file mode 100644 index 000000000..61ce486f9 --- /dev/null +++ b/components/binaries/transcript/.depend.opt @@ -0,0 +1,12 @@ +v8Parser.cmi: types.cmx +grafite.cmi: types.cmx +v8Parser.cmo: types.cmx v8Parser.cmi +v8Parser.cmx: types.cmx v8Parser.cmi +v8Lexer.cmo: v8Parser.cmi +v8Lexer.cmx: v8Parser.cmx +grafite.cmo: types.cmx grafite.cmi +grafite.cmx: types.cmx grafite.cmi +engine.cmo: v8Parser.cmi v8Lexer.cmx types.cmx grafite.cmi engine.cmi +engine.cmx: v8Parser.cmx v8Lexer.cmx types.cmx grafite.cmx engine.cmi +top.cmo: engine.cmi +top.cmx: engine.cmx diff --git a/components/binaries/transcript/engine.ml b/components/binaries/transcript/engine.ml index 3b1e8d773..9824426da 100644 --- a/components/binaries/transcript/engine.ml +++ b/components/binaries/transcript/engine.ml @@ -143,6 +143,12 @@ let require st name inc = let get_coercion st str = try List.assoc str st.coercions with Not_found -> "" +let make_path path = + List.fold_left Filename.concat "" (List.rev path) + +let make_prefix path = + String.concat "__" (List.rev path) ^ "__" + let commit st name = let i = get_index st name in let script = st.scripts.(i) in @@ -165,24 +171,31 @@ let produce st = let produce st name = let in_base_uri = Filename.concat st.input_base_uri name in let out_base_uri = Filename.concat st.output_base_uri name in - let filter = function - | T.Inline (k, obj) -> + let filter path = function + | T.Inline (b, k, obj, p) -> + let obj, p = + if b then Filename.concat (make_path path) obj, make_prefix path + else obj, p + in let s = obj ^ G.string_of_inline_kind k in - Some (T.Inline (k, Filename.concat in_base_uri s)) - | T.Include s -> + path, Some (T.Inline (b, k, Filename.concat in_base_uri s, p)) + | T.Include s -> begin - try Some (T.Include (List.assoc s st.requires)) - with Not_found -> None + try path, Some (T.Include (List.assoc s st.requires)) + with Not_found -> path, None end - | T.Coercion (b, obj) -> + | T.Coercion (b, obj) -> let str = get_coercion st obj in let base_uri = if str <> "" then str else if b then out_base_uri else in_base_uri in let s = obj ^ G.string_of_inline_kind T.Con in - Some (T.Coercion (b, Filename.concat base_uri s)) - | item -> Some item + path, Some (T.Coercion (b, Filename.concat base_uri s)) + | T.Section (b, id, _) as item -> + let path = if b then id :: path else List.tl path in + path, Some item + | item -> path, 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 @@ -190,8 +203,9 @@ let produce st = let lexbuf = Lexing.from_channel ich in try let items = V8Parser.items V8Lexer.token lexbuf in - close_in ich; - let items = List.rev (X.list_rev_map_filter filter items) in + close_in ich; + let _, rev_items = X.list_rev_map_filter_fold filter [] items in + let items = List.rev rev_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 diff --git a/components/binaries/transcript/grafite.ml b/components/binaries/transcript/grafite.ml index dcc6b9fb1..cc1b465d7 100644 --- a/components/binaries/transcript/grafite.ml +++ b/components/binaries/transcript/grafite.ml @@ -81,10 +81,12 @@ let require value = let coercion value = command_of_obj (G.Coercion (floc, UM.uri_of_string value, true, 0)) -let inline value = - command_of_macro (G.Inline (floc, value)) +let inline (uri, prefix) = + command_of_macro (G.Inline (floc, uri, prefix)) let commit och items = + let trd (_, _, x) = x in + let trd_rth (_, _, x, y) = x, y in let commit = function | T.Heading heading -> out_preamble och heading | T.Line line -> out_line_comment och line @@ -92,7 +94,8 @@ let commit och items = | T.Include script -> out_command och (require script) | T.Coercion specs -> out_command och (coercion (snd specs)) | T.Notation specs -> out_unexported och "NOTATION" (snd specs) (**) - | T.Inline specs -> out_command och (inline (snd specs)) + | T.Inline specs -> out_command och (inline (trd_rth specs)) + | T.Section specs -> out_unexported och "UNEXPORTED" (trd specs) | T.Comment comment -> out_comment och comment | T.Unexport unexport -> out_unexported och "UNEXPORTED" unexport | T.Verbatim verbatim -> out_verbatim och verbatim diff --git a/components/binaries/transcript/types.ml b/components/binaries/transcript/types.ml index 73420ee59..de7c1036e 100644 --- a/components/binaries/transcript/types.ml +++ b/components/binaries/transcript/types.ml @@ -27,6 +27,10 @@ type local = bool type inline_kind = Con | Ind | Var +type source = string + +type prefix = string + type item = Heading of (string * int) | Line of string | Comment of string @@ -35,7 +39,8 @@ type item = Heading of (string * int) | Include of string | Coercion of (local * string) | Notation of (local * string) - | Inline of (inline_kind * string) + | Section of (local * string * string) + | Inline of (local * inline_kind * source * prefix) | Verbatim of string | Discard of string diff --git a/components/binaries/transcript/v8Lexer.mll b/components/binaries/transcript/v8Lexer.mll index 0fea9c9eb..5a90aabf7 100644 --- a/components/binaries/transcript/v8Lexer.mll +++ b/components/binaries/transcript/v8Lexer.mll @@ -13,7 +13,7 @@ let RAWID = QT [^ '"']* QT let NUM = "-"? FIG+ rule token = parse - | "Let" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } + | "Let" { let s = Lexing.lexeme lexbuf in out "LET" s; P.LET s } | "Remark" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } | "Lemma" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } | "Theorem" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } @@ -26,19 +26,19 @@ rule token = parse | "Variables" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s } | "Hypothesis" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s } | "Hypotheses" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s } - | "Axiom" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s } + | "Axiom" { let s = Lexing.lexeme lexbuf in out "AX" s; P.AX s } | "Inductive" { let s = Lexing.lexeme lexbuf in out "IND" s; P.IND s } | "Record" { let s = Lexing.lexeme lexbuf in out "IND" s; P.IND s } | "Section" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } - | "End" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } - | "Hint" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } - | "Unset" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } - | "Print" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } - | "Opaque" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } - | "Transparent" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } - | "Ltac" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } - | "Tactic" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } - | "Declare" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } + | "End" { let s = Lexing.lexeme lexbuf in out "END" s; P.END s } + | "Hint" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "Unset" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "Print" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "Opaque" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "Transparent" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "Ltac" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "Tactic" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "Declare" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } | "Require" { let s = Lexing.lexeme lexbuf in out "REQ" s; P.REQ s } | "Export" { let s = Lexing.lexeme lexbuf in out "XP" s; P.XP s } | "Import" { let s = Lexing.lexeme lexbuf in out "IP" s; P.IP s } @@ -49,7 +49,7 @@ rule token = parse | "Infix" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } | "Identity" { let s = Lexing.lexeme lexbuf in out "ID" s; P.ID s } | "Coercion" { let s = Lexing.lexeme lexbuf in out "CO" s; P.COERC s } - | "let" { let s = Lexing.lexeme lexbuf in out "LET" s; P.LET s } + | "let" { let s = Lexing.lexeme lexbuf in out "ABBR" s; P.ABBR s } | "in" { let s = Lexing.lexeme lexbuf in out "IN" s; P.IN s } | SPC { let s = Lexing.lexeme lexbuf in out "SPC" s; P.SPC s } | ID { let s = Lexing.lexeme lexbuf in out "ID" s; P.IDENT s } diff --git a/components/binaries/transcript/v8Parser.mly b/components/binaries/transcript/v8Parser.mly index 06d4d908b..ff70df713 100644 --- a/components/binaries/transcript/v8Parser.mly +++ b/components/binaries/transcript/v8Parser.mly @@ -34,8 +34,8 @@ let cat x = String.concat " " x - let mk_vars idents = - let map ident = T.Inline (T.Var, trim ident) in + let mk_vars local idents = + let map ident = T.Inline (local, T.Var, trim ident, "") in List.map map idents let strip2 s = @@ -51,7 +51,7 @@ [T.Notation (false, str); T.Notation (true, str)] %} %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 + %token ABBR IN LET TH PROOF QED VAR AX IND SEC END UNX REQ XP IP SET NOT LOAD ID COERC %token EOF %start items @@ -72,16 +72,38 @@ | { "" } | SPC rspcs { $1 ^ $2 } ; + xident: + | IDENT { $1 } + | LET { $1 } + | TH { $1 } + | QED { $1 } + | PROOF { $1 } + | VAR { $1 } + | AX { $1 } + | IND { $1 } + | SEC { $1 } + | END { $1 } + | UNX { $1 } + | REQ { $1 } + | LOAD { $1 } + | NOT { $1 } + | ID { $1 } + | COERC { $1 } + ; fs: FS spcs { $1 ^ $2 }; - ident: IDENT spcs { $1 ^ $2 }; + ident: xident spcs { $1 ^ $2 }; th: TH spcs { $1 ^ $2 }; + xlet: LET spcs { $1 ^ $2 }; proof: PROOF spcs { $1 ^ $2 }; qed: QED spcs { $1 ^ $2 }; sec: SEC spcs { $1 ^ $2 }; + xend: END spcs { $1 ^ $2 }; + unx: UNX spcs { $1 ^ $2 }; def: DEF spcs { $1 ^ $2 }; op: OP spcs { $1 ^ $2 }; - xlet: LET spcs { $1 ^ $2 }; + abbr: ABBR spcs { $1 ^ $2 }; var: VAR spcs { $1 ^ $2 }; + ax: AX spcs { $1 ^ $2 }; req: REQ spcs { $1 ^ $2 }; load: LOAD spcs { $1 ^ $2 }; xp: XP spcs { $1 ^ $2 }; @@ -121,7 +143,7 @@ | CC { $1 } | COE { $1 } | STR { $1 } - | xlet extends0 IN { $1 ^ $2 ^ $3 } + | abbr extends0 IN { $1 ^ $2 ^ $3 } | op extends1 CP { $1 ^ $2 ^ $3 } ; @@ -175,7 +197,7 @@ | COE { $1 } | STR { $1 } | OP { $1 } - | LET { $1 } + | ABBR { $1 } | IN { $1 } | CP { $1 } | DEF { $1 } @@ -220,9 +242,13 @@ | CC { $1 } | SC { $1 } | TH { $1 } + | LET { $1 } | VAR { $1 } + | AX { $1 } | IND { $1 } | SEC { $1 } + | END { $1 } + | UNX { $1 } | REQ { $1 } | XP { $1 } | IP { $1 } @@ -245,46 +271,65 @@ ; qid: - | IDENT { [$1] } + | xident { [$1] } | qid AC { strip1 $2 :: $1 } ; macro_step: | th ident restricts fs proof FS steps qed FS - { out "TH" $2; $7 @ [T.Inline (T.Con, trim $2)] } + { out "TH" $2; $7 @ [T.Inline (false, T.Con, trim $2, "")] } | th ident restricts fs proof restricts FS - { out "TH" $2; [T.Inline (T.Con, trim $2)] } + { out "TH" $2; [T.Inline (false, T.Con, trim $2, "")] } | th ident restricts fs steps qed FS - { out "TH" $2; $5 @ [T.Inline (T.Con, trim $2)] } + { out "TH" $2; $5 @ [T.Inline (false, T.Con, trim $2, "")] } | th ident restricts def restricts FS - { out "TH" $2; [T.Inline (T.Con, trim $2)] } + { out "TH" $2; [T.Inline (false, T.Con, trim $2, "")] } | th ident def restricts FS - { out "TH" $2; [T.Inline (T.Con, trim $2)] } + { out "TH" $2; [T.Inline (false, T.Con, trim $2, "")] } + | xlet ident restricts fs proof FS steps qed FS + { out "LET" $2; $7 @ [T.Inline (true, T.Con, trim $2, "")] } + | xlet ident restricts fs proof restricts FS + { out "LET" $2; [T.Inline (true, T.Con, trim $2, "")] } + | xlet ident restricts fs steps qed FS + { out "LET" $2; $5 @ [T.Inline (true, T.Con, trim $2, "")] } + | xlet ident restricts def restricts FS + { out "LET" $2; [T.Inline (true, T.Con, trim $2, "")] } + | xlet ident def restricts FS + { out "LET" $2; [T.Inline (true, T.Con, trim $2, "")] } | var idents xres FS - { out "VAR" (cat $2); mk_vars $2 } + { out "VAR" (cat $2); mk_vars true $2 } + | ax idents xres FS + { out "AX" (cat $2); mk_vars false $2 } | ind ident unexports FS - { out "IND" $2; T.Inline (T.Ind, trim $2) :: snd $3 } - | sec unexports FS - { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] } + { out "IND" $2; T.Inline (false, T.Ind, trim $2, "") :: snd $3 } + | sec ident FS + { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)] } + | xend ident FS + { out "END" $2; [T.Section (false, trim $2, $1 ^ $2)] } + | unx unexports FS + { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] } | req xp ident FS - { out "REQ" $3; [T.Include (trim $3)] } + { out "REQ" $3; [T.Include (trim $3)] } | req ip ident FS - { out "REQ" $3; [T.Include (trim $3)] } + { out "REQ" $3; [T.Include (trim $3)] } | req ident FS - { out "REQ" $2; [T.Include (trim $2)] } + { out "REQ" $2; [T.Include (trim $2)] } | load str FS - { out "REQ" $2; [T.Include (strip2 (trim $2))] } + { out "REQ" $2; [T.Include (strip2 (trim $2))] } | coerc qid spcs cn unexports FS - { out "COERCE" (hd $2); coercion (hd $2) } + { out "COERCE" (hd $2); coercion (hd $2) } | id coerc qid spcs cn unexports FS - { out "COERCE" (hd $3); coercion (hd $3) } + { out "COERCE" (hd $3); 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) } + | ax idents error + { let vs = cat $2 in + out "ERROR" vs; failwith ("macro_step " ^ vs) } ; item: | OQ verbatims CQ { [T.Comment $2] } diff --git a/components/extlib/hExtlib.ml b/components/extlib/hExtlib.ml index d4572789a..073c56959 100644 --- a/components/extlib/hExtlib.ml +++ b/components/extlib/hExtlib.ml @@ -164,6 +164,17 @@ let list_rev_map_filter f l = in aux [] l +let list_rev_map_filter_fold f v l = + let rec aux v a = function + | [] -> v, a + | hd :: tl -> + begin match f v hd with + | v, None -> aux v a tl + | v, Some b -> aux v (b :: a) tl + end + in + aux v [] l + let list_concat ?(sep = []) = let rec aux acc = function diff --git a/components/extlib/hExtlib.mli b/components/extlib/hExtlib.mli index 907259a8f..5b467d005 100644 --- a/components/extlib/hExtlib.mli +++ b/components/extlib/hExtlib.mli @@ -76,6 +76,7 @@ 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_rev_map_filter_fold: ('c -> 'a -> 'c * 'b option) -> 'c -> 'a list -> 'c * '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/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index 7108a323a..26a65b531 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -114,7 +114,7 @@ type 'term macro = (* real macros *) | Check of loc * 'term | Hint of loc - | Inline of loc * string (* the string is a URI or a base-uri *) + | Inline of loc * string * string (* URI or base-uri, name prefix *) (** To be increased each time the command type below changes, used for "safe" * marshalling *) diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index 366c0e264..98e57b5c4 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -203,7 +203,8 @@ let pp_macro ~term_pp = (* real macros *) | Check (_, term) -> sprintf "check %s" (term_pp term) | Hint _ -> "hint" - | Inline (_,suri) -> sprintf "inline \"%s\"" suri + | Inline (_, suri, "") -> sprintf "inline \"%s\"" suri + | Inline (_, suri, prefix) -> sprintf "inline \"%s\" \"%s\"" suri prefix let pp_associativity = function | Gramext.LeftA -> "left associative" diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index df01f8467..f95829797 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -79,7 +79,7 @@ let tactic_of_ast status ast = Tactics.cut ~mk_fresh_name_callback:(namer_of names) term | GrafiteAst.Decompose (_, types, what, names) -> let to_type = function - | GrafiteAst.Type (uri, typeno) -> uri, typeno + | GrafiteAst.Type (uri, typeno) -> uri, Some typeno | GrafiteAst.Ident _ -> assert false in let user_types = List.rev_map to_type types in diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index 9b9a5da22..b41ae8ebc 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -401,8 +401,9 @@ EXTEND macro: [ [ [ IDENT "check" ]; t = term -> GrafiteAst.Check (loc, t) - | [ IDENT "inline"]; suri = QSTRING -> - GrafiteAst.Inline (loc,suri) + | [ IDENT "inline"]; suri = QSTRING; prefix = OPT QSTRING -> + let prefix = match prefix with None -> "" | Some prefix -> prefix in + GrafiteAst.Inline (loc,suri,prefix) | [ IDENT "hint" ] -> GrafiteAst.Hint loc | [ IDENT "whelp"; "match" ] ; t = term -> GrafiteAst.WMatch (loc,t) diff --git a/components/tactics/eliminationTactics.ml b/components/tactics/eliminationTactics.ml index 37a4f7136..f1a9988eb 100644 --- a/components/tactics/eliminationTactics.ml +++ b/components/tactics/eliminationTactics.ml @@ -32,9 +32,29 @@ module S = ProofEngineStructuralRules module F = FreshNamesGenerator module E = ProofEngineTypes module H = ProofEngineHelpers +module R = ReductionTactics + +(* +(* search in term the Inductive Types and return a list of uris as triples like this: (uri,typeno,exp_named_subst) *) +let search_inductive_types ty = + let rec aux types = function + | C.MutInd (uri, typeno, _) when (not (List.mem (uri, typeno) types)) -> + (uri, typeno) :: types + | C.Appl applist -> List.fold_left aux types applist + | _ -> types + in + aux [] ty +(* N.B: in un caso tipo (and A forall C:Prop.(or B C)) l'or *non* viene selezionato! *) +*) (* unexported tactics *******************************************************) +type type_class = Other + | Ind + | Con of C.lazy_term + +let premise_pattern what = None, [what, C.Implicit (Some `Hole)], None + let rec scan_tac ~old_context_length ~index ~tactic = let scan_tac status = let (proof, goal) = status in @@ -51,29 +71,37 @@ let rec scan_tac ~old_context_length ~index ~tactic = in try E.apply_tactic tac status with E.Fail _ -> aux (pred index) - in aux (index + context_length - old_context_length - 1) + in aux (index + context_length - old_context_length) in E.mk_tactic scan_tac -let rec check_inductive_types types = function - | C.MutInd (uri, typeno, _) -> List.mem (uri, typeno) types - | C.Appl (hd :: tl) -> check_inductive_types types hd - | _ -> false +let rec check_types types = function + | C.MutInd (uri, typeno, _) -> + if List.mem (uri, Some typeno) types then Ind else Other + | C.Const (uri, _) as t -> + if List.mem (uri, None) types then Con (E.const_lazy_term t) else Other + | C.Appl (hd :: tl) -> check_types types hd + | _ -> Other -let elim_clear_tac ~mk_fresh_name_callback ~types ~what = - let elim_clear_tac status = +let elim_clear_unfold_tac ~mk_fresh_name_callback ~types ~what = + let elim_clear_unfold_tac status = let (proof, goal) = status in let _, metasenv, _, _ = proof in let _, context, _ = CicUtil.lookup_meta goal metasenv in let index, ty = H.lookup_type metasenv context what in - if check_inductive_types types ty then - let tac = T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index)) - ~continuation:(S.clear [what]) - in - E.apply_tactic tac status - else raise (E.Fail (lazy "unexported elim_clear: not an eliminable type")) + match check_types types ty with + | Ind -> + let tac = T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index)) + ~continuation:(S.clear [what]) + in + E.apply_tactic tac status + | Con t -> + let tac = R.unfold_tac (Some t) ~pattern:(premise_pattern what) in + E.apply_tactic tac status + | Other -> + raise (E.Fail (lazy "unexported elim_clear: not an eliminable type")) in - E.mk_tactic elim_clear_tac + E.mk_tactic elim_clear_unfold_tac (* elim type ****************************************************************) @@ -102,17 +130,6 @@ let debug_print = fun _ -> () (** debugging print *) let warn s = debug_print (lazy ("DECOMPOSE: " ^ (Lazy.force s))) -(* search in term the Inductive Types and return a list of uris as triples like this: (uri,typeno,exp_named_subst) *) -let search_inductive_types ty = - let rec aux types = function - | C.MutInd (uri, typeno, _) when (not (List.mem (uri, typeno) types)) -> - (uri, typeno) :: types - | C.Appl applist -> List.fold_left aux types applist - | _ -> types - in - aux [] ty -(* N.B: in un caso tipo (and A forall C:Prop.(or B C)) l'or *non* viene selezionato! *) - (* roba seria ------------------------------------------------------------- *) let decompose_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) @@ -122,7 +139,7 @@ let decompose_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) let _, metasenv,_,_ = proof in let _, context, _ = CicUtil.lookup_meta goal metasenv in let types = List.rev_append user_types (FwdQueries.decomposables dbd) in - let tactic = elim_clear_tac ~mk_fresh_name_callback ~types in + let tactic = elim_clear_unfold_tac ~mk_fresh_name_callback ~types in let old_context_length = List.length context in let tac = match what with | Some what -> diff --git a/components/tactics/eliminationTactics.mli b/components/tactics/eliminationTactics.mli index 45fbed6e8..379166ac0 100644 --- a/components/tactics/eliminationTactics.mli +++ b/components/tactics/eliminationTactics.mli @@ -29,5 +29,5 @@ val elim_type_tac: val decompose_tac: ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - ?user_types:((UriManager.uri * int) list) -> + ?user_types:((UriManager.uri * int option) list) -> ?what:string -> dbd:HMysql.dbd -> ProofEngineTypes.tactic diff --git a/components/tactics/proofEngineTypes.ml b/components/tactics/proofEngineTypes.ml index 56b4155ae..b887c4bcd 100644 --- a/components/tactics/proofEngineTypes.ml +++ b/components/tactics/proofEngineTypes.ml @@ -79,7 +79,7 @@ let conclusion_pattern t = let t' = match t with | None -> None - | Some t -> Some (fun _ m u -> t, m, u) + | Some t -> Some (const_lazy_term t) in t',[],Some (Cic.Implicit (Some `Hole)) diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index 88179e4c8..d765a8ac0 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -1,17 +1,15 @@ +(* GENERATED FILE, DO NOT EDIT. STAMP:Tue Nov 28 11:13:28 CET 2006 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : dbd:HMysql.dbd -> - term:Cic.term -> - params:(string * string) list -> - universe:Universe.universe -> - ProofEngineTypes.tactic + term:Cic.term -> + params:(string * string) list -> + universe:Universe.universe -> ProofEngineTypes.tactic val assumption : ProofEngineTypes.tactic val auto : - params:(string * string) list -> - dbd:HMysql.dbd -> - universe:Universe.universe -> - ProofEngineTypes.tactic + params:(string * string) list -> + dbd:HMysql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic val change : pattern:ProofEngineTypes.lazy_pattern -> Cic.lazy_term -> ProofEngineTypes.tactic @@ -24,7 +22,7 @@ val cut : Cic.term -> ProofEngineTypes.tactic val decompose : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - ?user_types:(UriManager.uri * int) list -> + ?user_types:(UriManager.uri * int option) list -> ?what:string -> dbd:HMysql.dbd -> ProofEngineTypes.tactic val demodulate : dbd:HMysql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic diff --git a/components/whelp/fwdQueries.ml b/components/whelp/fwdQueries.ml index 1f4e508fc..5387d3aeb 100644 --- a/components/whelp/fwdQueries.ml +++ b/components/whelp/fwdQueries.ml @@ -104,7 +104,8 @@ let decomposables ~dbd = | None -> None | Some str -> match CicUtil.term_of_uri (UriManager.uri_of_string str) with - | Cic.MutInd (uri, typeno, _) -> Some (uri, typeno) + | Cic.MutInd (uri, typeno, _) -> Some (uri, Some typeno) + | Cic.Const (uri, _) -> Some (uri, None) | _ -> raise (UriManager.IllFormedUri str) in @@ -112,4 +113,3 @@ let decomposables ~dbd = let query = Printf.sprintf "SELECT %s FROM %s" select from in let decomposables = HMysql.map ~f:map (HMysql.exec dbd query) in filter_map_n (fun _ x -> x) 0 decomposables - diff --git a/components/whelp/fwdQueries.mli b/components/whelp/fwdQueries.mli index 7f580a541..200670335 100644 --- a/components/whelp/fwdQueries.mli +++ b/components/whelp/fwdQueries.mli @@ -24,5 +24,5 @@ *) val fwd_simpl: dbd:HMysql.dbd -> Cic.term -> UriManager.uri list -val decomposables: dbd:HMysql.dbd -> (UriManager.uri * int) list +val decomposables: dbd:HMysql.dbd -> (UriManager.uri * int option) list -- 2.39.2