- grafiteAst: semantics of the Include flag changed: now true means normal include, New Inline flags Coercions, Comments (activated) Debug (not yet)
- library: eq_plus_Zplus moved from Z/times to Z/plus
now Z/plus.ma Z/times.ma are fully reconstructed :)
| flavour when List.mem flavour th_flavours ->
let ast = proc_proof v in
let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in
- let text = Printf.sprintf "%s\n%s%s: %u\n%s: %u\n%s"
- "COMMENTS" info "Tactics" steps "Final nodes" nodes "END"
+ let text =
+ if List.mem G.IPComments params then
+ Printf.sprintf "%s\n%s%s: %u\n%s: %u\n%s"
+ "COMMENTS" info "Tactics" steps "Final nodes" nodes "END"
+ else
+ ""
in
T.Statement (flavour, Some s, t, None, "") :: ast @ [T.Qed text]
| flavour when List.mem flavour def_flavours ->
module C = Cic
module I = CicInspect
module S = CicSubstitution
+module R = CicReduction
module TC = CicTypeChecker
module Un = CicUniv
module UM = UriManager
case : int list
}
-let debug = ref true
+let debug = ref false
(* helpers ******************************************************************)
| None -> false
| Some (uri, i, j) -> st.defaults && Obj.is_eq_URI uri && i = 1 && j = 1
+let are_convertible st pred sx dx =
+ let pred, sx, dx = H.cic pred, H.cic sx, H.cic dx in
+ let sx, dx = C.Appl [pred; sx], C.Appl [pred; dx] in
+ fst (R.are_convertible st.context sx dx Un.default_ugraph)
+
(* proof construction *******************************************************)
let anonymous_premise = C.Name "UNNAMED"
note sname (ppterm csty) (ppterm cety)
else ""
in
- if H.alpha_equivalence ~flatten:true st.context csty cety then [T.Note note] else
+ if H.alpha ~flatten:true st.context csty cety then [T.Note note] else
let sty, ety = H.acic_bc st.context sty, H.acic_bc st.context ety in
match name with
| None -> [T.Change (sty, ety, None, e, note)]
let a = ref "" in Ut.pp_term (fun s -> a := !a ^ s) [] st.context t; !a
in
assert (List.length tl = 5);
- let predicate = List.nth tl 2 in
- let dtext = if !debug then dtext ^ ppterm (H.cic predicate) else dtext in
- let e = Cn.mk_pattern 1 ity predicate in
+ let pred, sx, dx = List.nth tl 2, List.nth tl 1, List.nth tl 4 in
+ let dtext = if !debug then dtext ^ ppterm (H.cic pred) else dtext in
+ let e = Cn.mk_pattern 1 ity pred in
let script = [T.Branch (qs, "")] in
- if (Cn.does_not_occur e) then script else
+ if Cn.does_not_occur e then script else
+ if are_convertible st pred sx dx then
+ let dtext = "convertible rewrite" ^ dtext in
+ let ity, ety, e = Cn.beta sx pred, Cn.beta dx pred, Cn.hole "" in
+ let city, cety = H.cic ity, H.cic ety in
+ if H.alpha ~flatten:true st.context city cety then script else
+ T.Change (ity, ety, None, e, dtext) :: script
+ else
T.Rewrite (direction, where, None, e, dtext) :: script
let rec proc_lambda st what name v t =
let script = if proceed then
let st, hyp, rqv = match get_inner_types st what, get_inner_types st v with
| Some (C.ALetIn (_, _, iv, iw, _), _), _ when
- H.alpha_equivalence ~flatten:true st.context (H.cic v) (H.cic iv) &&
- H.alpha_equivalence ~flatten:true st.context (H.cic w) (H.cic iw)
+ H.alpha ~flatten:true st.context (H.cic v) (H.cic iv) &&
+ H.alpha ~flatten:true st.context (H.cic w) (H.cic iw)
->
st, C.Def (H.cic v, H.cic w), [T.Intros (Some 1, [intro], dtext)]
| _, Some (ity, ety) ->
let mk_pattern psno ity predicate =
clear_absts (convert (generalize psno) ity) psno 0 predicate
+let beta v = function
+ | C.ALambda (_, _, _, t) -> subst 1 v t
+ | _ -> assert false
+
let get_clears c p xtypes =
let meta = C.Implicit None in
let rec aux c names p it et = function
val mk_pattern: int -> Cic.annterm -> Cic.annterm -> Cic.annterm
+val beta: Cic.annterm -> Cic.annterm -> Cic.annterm
+
val get_clears:
Cic.context -> Cic.term -> (Cic.term * Cic.term) option ->
Cic.context * string list
let sober ?(flatten=false) c t =
if flatten then flatten_appls t else (assert (Ut.is_sober c t); t)
-let alpha_equivalence ?flatten c t1 t2 =
+let alpha ?flatten c t1 t2 =
let t1 = sober ?flatten c t1 in
let t2 = sober ?flatten c t2 in
Ut.alpha_equivalence t1 t2
let occurs c ~what ~where =
let result = ref false in
let equality c t1 t2 =
- let r = alpha_equivalence ~flatten:true c t1 t2 in
+ let r = alpha ~flatten:true c t1 t2 in
result := !result || r; r
in
let context, what, with_what = c, [what], [C.Rel 0] in
(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> Cic.context -> Cic.annterm ->
bool
-val alpha_equivalence:
+val alpha:
?flatten:bool -> Cic.context -> Cic.term -> Cic.term -> bool
(* debugging ****************************************************************)
-let debug = ref true
+let debug = ref false
(* term optimization ********************************************************)
gallina8Parser.cmi: types.cmx
grafiteParser.cmi: types.cmx
grafite.cmi: types.cmx
-engine.cmi:
-types.cmo:
-types.cmx:
-options.cmo:
-options.cmx:
gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi
gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi
gallina8Lexer.cmo: options.cmx gallina8Parser.cmi
let heading = st.heading_path, st.heading_lines in
set_items st name [T.Heading heading]
-let require st name src inc =
- set_items st name [T.Include (src, inc)]
+let require st name moo inc =
+ set_items st name [T.Include (moo, inc)]
let get_coercion st str =
try List.assoc str st.coercions with Not_found -> ""
let get_iparams st name =
let map = function
| "nodefaults" -> GA.IPNoDefaults
+ | "coercions" -> GA.IPCoercions
+ | "comments" -> GA.IPComments
| s -> failwith ("unknown inline parameter: " ^ s)
in
List.map map (X.list_assoc_all name st.iparams)
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
- let full_s = Filename.concat in_base_uri s in
- let params = params @ get_iparams st (Filename.concat name obj) in
- path, Some (T.Inline (b, k, full_s, p, f, params))
- | T.Include (src, s) ->
+ in
+ let ext = G.string_of_inline_kind k in
+ let s = Filename.concat in_base_uri (obj ^ ext) in
+ let params =
+ params @
+ get_iparams st "*" @
+ get_iparams st ("*" ^ ext) @
+ get_iparams st (Filename.concat name obj)
+ in
+ path, Some (T.Inline (b, k, s, p, f, params))
+ | T.Include (moo, s) ->
begin
- try path, Some (T.Include (src, List.assoc s st.requires))
+ try path, Some (T.Include (moo, List.assoc s st.requires))
with Not_found -> path, None
end
| T.Coercion (b, obj) ->
| item -> path, Some item
in
let set_includes st name =
- try require st name false (List.assoc name st.includes)
+ try require st name true (List.assoc name st.includes)
with Not_found -> ()
in
let rec remove_lines ich n =
set_items st st.input_package (comment :: global_items);
init name;
begin match st.input_type with
- | T.Grafite "" -> require st name true file
- | _ -> require st name true st.input_package
+ | T.Grafite "" -> require st name false file
+ | _ -> require st name false st.input_package
end;
set_includes st name; set_items st name local_items; commit st name
with e ->
List.iter (produce st) st.files
| T.Grafite s ->
let theory = Filename.concat st.input_path s in
- require st st.input_package true theory;
+ require st st.input_package false theory;
List.iter (produce st) st.files;
commit st st.input_package
| _ ->
| unx xskips FS
{ out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
| req xp ident FS
- { out "REQ" $3; [T.Include (false, trim $3)] }
+ { out "REQ" $3; [T.Include (true, trim $3)] }
| req ident FS
- { out "REQ" $2; [T.Include (false, trim $2)] }
+ { out "REQ" $2; [T.Include (true, trim $2)] }
| load str FS
- { out "REQ" $2; [T.Include (false, strip2 (trim $2))] }
+ { out "REQ" $2; [T.Include (true, strip2 (trim $2))] }
| coerc qid spcs skips FS
{ out "COERCE" (hd $2); coercion (hd $2) }
| id coerc qid spcs skips FS
let command_of_macro macro =
G.Executable (floc, G.Macro (floc, macro))
-let require src value =
- command_of_obj (G.Include (floc, src, value ^ ".ma"))
+let require moo value =
+ command_of_obj (G.Include (floc, moo, value ^ ".ma"))
let coercion value =
command_of_obj (G.Coercion (floc, UM.uri_of_string value, true, 0, 0))
| T.Heading heading -> out_preamble och heading
| T.Line line ->
if !O.comments then out_line_comment och line
- | T.Include (src, script) -> out_command och (require src script)
+ | T.Include (moo, script) -> out_command och (require moo script)
| T.Coercion specs ->
if !O.comments then out_unexported och "COERCION" (snd specs)
| T.Notation specs ->
type print_kind = [ `Env | `Coer ]
-type inline_param = IPPrefix of string
- | IPAs of Cic.object_flavour
- | IPProcedural
- | IPNoDefaults
- | IPLevel of int
- | IPDepth of int
+type inline_param = IPPrefix of string (* undocumented *)
+ | IPAs of Cic.object_flavour (* preferred flavour *)
+ | IPProcedural (* procedural rendering *)
+ | IPNoDefaults (* no default-based tactics *)
+ | IPLevel of int (* granularity level *)
+ | IPDepth of int (* undocumented *)
+ | IPComments (* show statistics *)
+ | IPCoercions (* show coercions *)
+ | IPDebug of int (* set debug level *)
type ('term,'lazy_term) macro =
(* Whelp's stuff *)
| UnificationHint of loc * 'term * int (* term, precedence *)
| Default of loc * string * UriManager.uri list
| Drop of loc
- | Include of loc * bool (* source? *) * string
+ | Include of loc * bool (* normal? *) * string
| Obj of loc * 'obj
| Relation of
loc * string * 'term * 'term * 'term option * 'term option * 'term option
let pp_inline_params l =
let pp_param = function
| IPPrefix prefix -> "prefix = \"" ^ prefix ^ "\""
- | IPAs flavour -> flavour_pp flavour
- | IPProcedural -> "procedural"
- | IPNoDefaults -> "nodefaults"
+ | IPAs flavour -> flavour_pp flavour
+ | IPProcedural -> "procedural"
+ | IPNoDefaults -> "nodefaults"
| IPDepth depth -> "depth = " ^ string_of_int depth
| IPLevel level -> "level = " ^ string_of_int level
+ | IPComments -> "comments"
+ | IPCoercions -> "coercions"
+ | IPDebug debug -> "debug = " ^ string_of_int debug
in
let s = String.concat " " (List.map pp_param l) in
if s = "" then s else " " ^ s
"unification hint " ^ string_of_int n ^ " " ^ term_pp t
| Default (_,what,uris) -> pp_default what uris
| Drop _ -> "drop"
- | Include (_,false,path) -> "include \"" ^ path ^ "\""
- | Include (_,true,path) -> "include source \"" ^ path ^ "\""
+ | Include (_,true,path) -> "include \"" ^ path ^ "\""
+ | Include (_,false,path) -> "include source \"" ^ path ^ "\""
| Obj (_,obj) -> obj_pp obj
| Qed _ -> "qed"
| Relation (_,id,a,aeq,refl,sym,trans) ->
true, (UriDep (UriManager.uri_of_string u) :: acc)
| [< '("IDENT", "include"); '("QSTRING", fname) >] ->
true, (IncludeDep fname :: acc)
- | [< '("IDENT", "include"); '("IDENT", "source"); '("QSTRING", fname) >] ->
+ | [< '("IDENT", "include"); '("IDENT", "lexicon"); '("QSTRING", fname) >] ->
true, (IncludeDep fname :: acc)
| [< '("IDENT", "include'"); '("QSTRING", fname) >] ->
true, (IncludeDep fname :: acc)
| IDENT "nodefaults" -> G.IPNoDefaults
| IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth
| IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level
+ | IDENT "comments" -> G.IPComments
+ | IDENT "coercions" -> G.IPCoercions
+ | IDENT "debug"; SYMBOL "="; debug = int -> G.IPDebug debug
] -> params
]
];
include_command: [ [
IDENT "include" ; path = QSTRING ->
- loc,path,false,L.WithPreferences
+ loc,path,true,L.WithPreferences
| IDENT "include" ; IDENT "source" ; path = QSTRING ->
- loc,path,true,L.WithPreferences
+ loc,path,false,L.WithPreferences
| IDENT "include'" ; path = QSTRING ->
- loc,path,false,L.WithoutPreferences
+ loc,path,true,L.WithoutPreferences
]];
grafite_command: [ [
let stm = G.Comment (loc, com) in
!grafite_callback status stm;
status, LSome stm
- | (iloc,fname,source,mode) = include_command ; SYMBOL "." ->
+ | (iloc,fname,normal,mode) = include_command ; SYMBOL "." ->
fun ?(never_include=false) ~include_paths status ->
let stm =
- G.Executable (loc, G.Command (loc, G.Include (iloc, source, fname)))
+ G.Executable (loc, G.Command (loc, G.Include (iloc, normal, fname)))
in
!grafite_callback status stm;
let _root, buri, fullpath, _rrelpath =
Librarian.baseuri_of_script ~include_paths fname
in
- let stm =
- G.Executable (loc, G.Command (loc, G.Include (iloc, source, buri)))
- in
let status =
if never_include then raise (NoInclusionPerformed fullpath)
else LE.eval_command status (L.Include (iloc,buri,mode,fullpath))
in
+ let stm =
+ G.Executable (loc, G.Command (loc, G.Include (iloc, normal, buri)))
+ in
status, LSome stm
| scom = lexicon_command ; SYMBOL "." ->
fun ?(never_include=false) ~include_paths status ->
pp.cmi: terms.cmi
+fosubst.cmi: terms.cmi
founif.cmi: terms.cmi
index.cmi: terms.cmi
orderings.cmi: terms.cmi
-fosubst.cmi: terms.cmi
nCicBlob.cmi: terms.cmi
cicBlob.cmi: terms.cmi
terms.cmo: terms.cmi
terms.cmx: terms.cmi
pp.cmo: terms.cmi pp.cmi
pp.cmx: terms.cmx pp.cmi
+fosubst.cmo: terms.cmi fosubst.cmi
+fosubst.cmx: terms.cmx fosubst.cmi
founif.cmo: terms.cmi fosubst.cmi founif.cmi
founif.cmx: terms.cmx fosubst.cmx founif.cmi
index.cmo: terms.cmi index.cmi
index.cmx: terms.cmx index.cmi
orderings.cmo: terms.cmi orderings.cmi
orderings.cmx: terms.cmx orderings.cmi
-fosubst.cmo: terms.cmi fosubst.cmi
-fosubst.cmx: terms.cmx fosubst.cmi
nCicBlob.cmo: terms.cmi nCicBlob.cmi
nCicBlob.cmx: terms.cmx nCicBlob.cmi
cicBlob.cmo: terms.cmi cicBlob.cmi
-terms.cmi:
pp.cmi: terms.cmi
+fosubst.cmi: terms.cmi
founif.cmi: terms.cmi
index.cmi: terms.cmi
orderings.cmi: terms.cmi
+nCicBlob.cmi: terms.cmi
+cicBlob.cmi: terms.cmi
terms.cmo: terms.cmi
terms.cmx: terms.cmi
-pp.cmo: pp.cmi
-pp.cmx: pp.cmi
-founif.cmo: founif.cmi
-founif.cmx: founif.cmi
+pp.cmo: terms.cmi pp.cmi
+pp.cmx: terms.cmx pp.cmi
+fosubst.cmo: terms.cmi fosubst.cmi
+fosubst.cmx: terms.cmx fosubst.cmi
+founif.cmo: terms.cmi fosubst.cmi founif.cmi
+founif.cmx: terms.cmx fosubst.cmx founif.cmi
index.cmo: terms.cmi index.cmi
index.cmx: terms.cmx index.cmi
orderings.cmo: terms.cmi orderings.cmi
orderings.cmx: terms.cmx orderings.cmi
+nCicBlob.cmo: terms.cmi nCicBlob.cmi
+nCicBlob.cmx: terms.cmx nCicBlob.cmi
+cicBlob.cmo: terms.cmi cicBlob.cmi
+cicBlob.cmx: terms.cmx cicBlob.cmi
+paramod.cmo: terms.cmi pp.cmi nCicBlob.cmi founif.cmi paramod.cmi
+paramod.cmx: terms.cmx pp.cmx nCicBlob.cmx founif.cmx paramod.cmi
match raw_preamble with
| None ->
pp (GA.Executable(floc,
- GA.Command(floc,GA.Include(floc,false,"logic/equality.ma"))))
+ GA.Command(floc,GA.Include(floc,true,"logic/equality.ma"))))
| Some s -> s buri
in
let extra_statements_end = [] in
let aux = function
| G.Executable (_, G.Command (_, G.Obj (_, N.Inductive _))) as stm
->
+ let hc = !Acic2content.hide_coercions in
+ if List.mem G.IPCoercions params then
+ Acic2content.hide_coercions := false;
enable_notations false;
let str = stm_pp stm in
enable_notations true;
+ Acic2content.hide_coercions := hc;
str
(* FG: we disable notation for Inductive to avoid recursive notation *)
| G.Executable (_, G.Tactic _) as stm ->
Acic2content.hide_coercions := hc;
str
(* FG: we show coercion because the reconstruction is not aware of them *)
- | stm -> stm_pp stm
+ | stm ->
+ let hc = !Acic2content.hide_coercions in
+ if List.mem G.IPCoercions params then
+ Acic2content.hide_coercions := false;
+ let str = stm_pp stm in
+ Acic2content.hide_coercions := hc;
+ str
in
let script =
Acic2Procedural.procedural_of_acic_object
<key name="inline">logic/equality/eq_elim_r nodefaults</key>
<key name="inline">logic/equality/eq_f nodefaults</key>
<key name="inline">logic/equality/eq_f' nodefaults</key>
+ <key name="inline">Z/plus/eq_plus_Zplus nocoercions</key>
</section>
</helm_registry>
| (neg n) \Rightarrow (neg (pred ((S m)+(S n))))] ].
interpretation "integer plus" 'plus x y = (Zplus x y).
-
+
+theorem eq_plus_Zplus: \forall n,m:nat. Z_of_nat (n+m) =
+Z_of_nat n + Z_of_nat m.
+intro.cases n;intro
+ [reflexivity
+ |cases m
+ [simplify.rewrite < plus_n_O.reflexivity
+ |simplify.reflexivity.
+ ]]
+qed.
+
theorem Zplus_z_OZ: \forall z:Z. z+OZ = z.
intro.elim z.
simplify.reflexivity.
variant distr_Ztimes_Zplus: \forall x,y,z.
x * (y + z) = x*y + x*z \def
distributive_Ztimes_Zplus.
-
-theorem eq_plus_Zplus: \forall n,m:nat. Z_of_nat (n+m) =
-Z_of_nat n + Z_of_nat m.
-intro.cases n;intro
- [reflexivity
- |cases m
- [simplify.rewrite < plus_n_O.reflexivity
- |simplify.reflexivity.
- ]]
-qed.
<keyword>rec</keyword>
<keyword>record</keyword>
<keyword>return</keyword>
+ <keyword>source</keyword>
<keyword>to</keyword>
<keyword>using</keyword>
<keyword>with</keyword>
<keyword>hint</keyword>
<keyword>set</keyword>
<keyword>auto</keyword>
+ <keyword>nodefaults</keyword>
+ <keyword>coercions</keyword>
+ <keyword>comments</keyword>
+ <keyword>debug</keyword>
</keyword-list>
<keyword-list _name = "Whelp Macro" style = "Others 3"
(Helm_registry.get_bool "matita.paste_unicode_as_tex")
in
output_string och str
- | G.Executable (loc, G.Command (_, G.Include (_, true, _))) -> ()
+ | G.Executable (loc, G.Command (_, G.Include (_, false, _))) -> ()
| stm ->
output_string och (pp_statement stm); nl (); nl ()
in
projects / helm.git / commitdiff