type presentation_style = Declarative
| Procedural of int option
-type 'term macro =
+type ('term,'lazy_term) macro =
(* Whelp's stuff *)
| WHint of loc * 'term
| WMatch of loc * 'term
| WLocate of loc * string
| WElim of loc * 'term
(* real macros *)
+ | Eval of loc * 'lazy_term reduction * 'term
| Check of loc * 'term
| Hint of loc * bool
| AutoInteractive of loc * 'term auto_params
type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code =
| Command of loc * ('term, 'obj) command
- | Macro of loc * 'term macro
+ | Macro of loc * ('term,'lazy_term) macro
| Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic option
* ('term, 'lazy_term, 'reduction, 'ident) punctuation_tactical
| NonPunctuationTactical of loc
else
"(" ^ s ^ ")"
-let pp_macro ~term_pp =
+let pp_macro ~term_pp ~lazy_term_pp =
let term_pp = pp_arg ~term_pp in
let style_pp = function
| Declarative -> ""
| Some `Variant -> " as variant"
| Some `Axiom -> " as axiom"
in
+ let pp_reduction_kind = pp_reduction_kind ~term_pp:lazy_term_pp in
function
(* Whelp *)
| WInstance (_, term) -> "whelp instance " ^ term_pp term
| WElim (_, t) -> "whelp elim " ^ term_pp t
| WMatch (_, term) -> "whelp match " ^ term_pp term
(* real macros *)
+ | Eval (_, kind, term) ->
+ Printf.sprintf "eval %s on %s" (pp_reduction_kind kind) (term_pp term)
| Check (_, term) -> Printf.sprintf "check %s" (term_pp term)
| Hint (_, true) -> "hint rewrite"
| Hint (_, false) -> "hint"
let pp_executable ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp =
function
- | Macro (_, macro) -> pp_macro ~term_pp macro ^ "."
+ | Macro (_, macro) -> pp_macro ~term_pp ~lazy_term_pp macro ^ "."
| Tactic (_, Some tac, punct) ->
pp_tactic ~map_unicode_to_tex ~lazy_term_pp ~term_pp tac
^ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct
term_pp:('term -> string) ->
obj_pp:('obj -> string) ->
('term,'obj) GrafiteAst.command -> string
-val pp_macro: term_pp:('term -> string) -> 'term GrafiteAst.macro -> string
+val pp_macro:
+ term_pp:('term -> string) ->
+ lazy_term_pp:('lazy_term -> string) ->
+ ('term,'lazy_term) GrafiteAst.macro -> string
val pp_comment:
map_unicode_to_tex:bool ->
term_pp:('term -> string) ->
exception IncludedFileNotCompiled of string * string
exception Macro of
GrafiteAst.loc *
- (Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro)
+ (Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro)
type 'a disambiguator_input = string * int * 'a
disambiguate_macro:
(GrafiteTypes.status ->
- ('term GrafiteAst.macro) disambiguator_input ->
- Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
+ (('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
+ Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) ->
?do_heavy_checks:bool ->
GrafiteTypes.status ->
disambiguate_macro:
(GrafiteTypes.status ->
- ('term GrafiteAst.macro) disambiguator_input ->
- Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
+ (('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
+ Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) ->
options ->
GrafiteTypes.status ->
exception IncludedFileNotCompiled of string * string
exception Macro of
GrafiteAst.loc *
- (Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro)
+ (Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro)
type 'a disambiguator_input = string * int * 'a
disambiguate_macro:
(GrafiteTypes.status ->
- ('term GrafiteAst.macro) disambiguator_input ->
- Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
+ (('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
+ Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) ->
?do_heavy_checks:bool ->
GrafiteTypes.status ->
lexicon_status_ref metasenv context (text,prefix_len, macro)
=
let disambiguate_term = disambiguate_term text prefix_len lexicon_status_ref in
+ let disambiguate_reduction_kind =
+ disambiguate_reduction_kind text prefix_len lexicon_status_ref in
match macro with
| GrafiteAst.WMatch (loc,term) ->
let metasenv,term = disambiguate_term context metasenv term in
| GrafiteAst.Check (loc,term) ->
let metasenv,term = disambiguate_term context metasenv term in
metasenv,GrafiteAst.Check (loc,term)
+ | GrafiteAst.Eval (loc,kind,term) ->
+ let metasenv, term = disambiguate_term context metasenv term in
+ let kind = disambiguate_reduction_kind kind in
+ metasenv,GrafiteAst.Eval (loc,kind,term)
| GrafiteAst.AutoInteractive (loc, params) ->
let metasenv, params =
disambiguate_auto_params disambiguate_term metasenv context params in
LexiconEngine.status ref ->
Cic.metasenv ->
Cic.context ->
- (CicNotationPt.term GrafiteAst.macro) Disambiguate.disambiguator_input ->
- Cic.metasenv * Cic.term GrafiteAst.macro
+ ((CicNotationPt.term,CicNotationPt.term) GrafiteAst.macro) Disambiguate.disambiguator_input ->
+ Cic.metasenv * (Cic.term,Cic.lazy_term) GrafiteAst.macro
macro: [
[ [ IDENT "check" ]; t = term ->
GrafiteAst.Check (loc, t)
+ | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
+ GrafiteAst.Eval (loc, kind, t)
| [ IDENT "inline"];
style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
suri = QSTRING; prefix = OPT QSTRING;
~ids_to_inner_sorts ~ids_to_inner_types ?depth "" context annterm
in
String.concat "" (List.map aux script)
+;;
+
+let txt_of_macro ~map_unicode_to_tex metasenv context m =
+ GrafiteAstPp.pp_macro
+ ~term_pp:(txt_of_cic_term ~map_unicode_to_tex 80 metasenv context)
+ ~lazy_term_pp:(fun (f : Cic.lazy_term) ->
+ let t,metasenv,_ = f context metasenv CicUniv.empty_ugraph in
+ txt_of_cic_term ~map_unicode_to_tex 80 metasenv context t)
+ m
+;;
+
+
?flavour:Cic.object_flavour -> string -> string ->
string
+val txt_of_macro:
+ map_unicode_to_tex:bool ->
+ Cic.metasenv ->
+ Cic.context ->
+ (Cic.term, Cic.lazy_term) GrafiteAst.macro -> string
+
(* columns, rendering depth, context, term *)
val procedural_txt_of_cic_term:
map_unicode_to_tex:bool -> int -> ?depth:int ->
0.5.v - dd/mm/yyy - bugfix release
+ * New macro eval
* More code in the direction of a fully functional matita status, that
improved undo reliability in the parser/notation modules
* matitac was seldom compiling up-to-date files, fixed
</variablelist>
</para>
</sect1>
+ <sect1 id="command_eval">
+ <title>eval</title>
+ <para><userinput>eval red on t</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry>
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">eval</emphasis>
+ &reduction-kind;
+ <emphasis role="bold">on</emphasis>
+ &term;</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>Opens a CIC browser window that shows
+ the reduct of
+ <command>t</command>
+ together with its type.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
<sect1 id="command_coercion">
<title>coercion</title>
<para><userinput>coercion u with ariety saturation nocomposites</userinput></para>
<keyword>inline</keyword>
<keyword>procedural</keyword>
<keyword>check</keyword>
+ <keyword>eval</keyword>
<keyword>hint</keyword>
<keyword>set</keyword>
<keyword>auto</keyword>
(* no idea why ocaml wants this *)
let parsed_text_length = String.length parsed_text in
let dbd = LibraryDb.instance () in
- let pp_macro =
- let f t = ProofEngineReduction.replace
- ~equality:(fun _ t -> match t with Cic.Meta _ -> true | _ -> false)
- ~what:[()] ~with_what:[Cic.Implicit None] ~where:t
- in
- let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
- TAPp.pp_macro
- ~term_pp:(fun x ->
- ApplyTransformation.txt_of_cic_term max_int metasenv [] (f x)
- ~map_unicode_to_tex:(Helm_registry.get_bool
- "matita.paste_unicode_as_tex"))
- in
+ let pp_macro = ApplyTransformation.txt_of_macro ~map_unicode_to_tex:true in
match mac with
(* WHELP's stuff *)
| TA.WMatch (loc, term) ->
let l = Whelp.match_term ~dbd term in
- let entry = `Whelp (pp_macro mac, l) in
+ let entry = `Whelp (pp_macro [] [] mac, l) in
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], "", parsed_text_length
| TA.WInstance (loc, term) ->
let l = Whelp.instance ~dbd term in
- let entry = `Whelp (pp_macro mac, l) in
+ let entry = `Whelp (pp_macro [] [] mac, l) in
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], "", parsed_text_length
| TA.WLocate (loc, s) ->
let l = Whelp.locate ~dbd s in
- let entry = `Whelp (pp_macro mac, l) in
+ let entry = `Whelp (pp_macro [] [] mac, l) in
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], "", parsed_text_length
| TA.WElim (loc, term) ->
| _ -> failwith "Not a MutInd"
in
let l = Whelp.elim ~dbd uri in
- let entry = `Whelp (pp_macro mac, l) in
+ let entry = `Whelp (pp_macro [] [] mac, l) in
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], "", parsed_text_length
| TA.WHint (loc, term) ->
let _subst = [] in
let s = ((None,[0,[],term], _subst, lazy (Cic.Meta (0,[])) ,term, []),0) in
let l = List.map fst (MQ.experimental_hint ~dbd s) in
- let entry = `Whelp (pp_macro mac, l) in
+ let entry = `Whelp (pp_macro [] [] mac, l) in
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], "", parsed_text_length
(* REAL macro *)
if rewrite then
let l = MQ.equations_for_goal ~dbd proof_status in
let l = List.filter (fun u -> not (LibraryObjects.in_eq_URIs u)) l in
- let entry = `Whelp (pp_macro (TA.WHint(loc, Cic.Implicit None)), l) in
+ let entry =
+ `Whelp (pp_macro [] [] (TA.WHint(loc, Cic.Implicit None)), l) in
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], "", parsed_text_length
else
fun u -> HLog.error (UriManager.string_of_uri u ^ "\n")
) selected;
assert false)
+ | TA.Eval (_, kind, term) ->
+ let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
+ let context =
+ match user_goal with
+ None -> []
+ | Some n -> GrafiteTypes.get_proof_context grafite_status n in
+ let ty,_ = CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+ let term =
+ match kind with
+ | `Normalize ->
+ CicReduction.normalize ~delta:true ~subst:[] context term
+ | `Simpl ->
+ ProofEngineReduction.simpl context term
+ | `Unfold None ->
+ ProofEngineReduction.unfold ?what:None context term
+ | `Unfold (Some lazy_term) ->
+ let what, _, _ =
+ lazy_term context metasenv CicUniv.empty_ugraph in
+ ProofEngineReduction.unfold ~what context term
+ | `Whd ->
+ CicReduction.whd ~delta:true ~subst:[] context term
+ in
+ let t_and_ty = Cic.Cast (term,ty) in
+ guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
+ [({grafite_status with proof_status = No_proof},lexicon_status), parsed_text ],"",
+ parsed_text_length
| TA.Check (_,term) ->
let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
let context =
projects / helm.git / commitdiff