From: Enrico Tassi Date: Fri, 17 Oct 2008 12:12:52 +0000 (+0000) Subject: new command eval added X-Git-Tag: make_still_working~4675 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=75de1f4c87166f120d8bb42d98926adaf407c98c;p=helm.git new command eval added --- diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 180d687c9..560e680b4 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -132,7 +132,7 @@ type print_kind = [ `Env | `Coer ] 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 @@ -140,6 +140,7 @@ type 'term macro = | 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 @@ -180,7 +181,7 @@ type ('term,'lazy_term,'reduction,'ident) non_punctuation_tactical = 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 diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 189d172f8..8e23e56b5 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -248,7 +248,7 @@ let pp_arg ~term_pp arg = 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 -> "" @@ -269,6 +269,7 @@ let pp_macro ~term_pp = | 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 @@ -277,6 +278,8 @@ let pp_macro ~term_pp = | 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" @@ -347,7 +350,7 @@ let pp_non_punctuation_tactical ~term_pp ~lazy_term_pp = 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 diff --git a/helm/software/components/grafite/grafiteAstPp.mli b/helm/software/components/grafite/grafiteAstPp.mli index 647d38bbe..8f6904545 100644 --- a/helm/software/components/grafite/grafiteAstPp.mli +++ b/helm/software/components/grafite/grafiteAstPp.mli @@ -47,7 +47,10 @@ val pp_command: 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) -> diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 887e767e6..2efbc6811 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -32,7 +32,7 @@ exception Drop 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 @@ -406,8 +406,8 @@ type eval_ast = 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 -> @@ -443,8 +443,8 @@ type 'a eval_executable = 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 -> diff --git a/helm/software/components/grafite_engine/grafiteEngine.mli b/helm/software/components/grafite_engine/grafiteEngine.mli index c868bc615..1dabfaaa1 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.mli +++ b/helm/software/components/grafite_engine/grafiteEngine.mli @@ -27,7 +27,7 @@ exception Drop 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 @@ -47,8 +47,8 @@ val eval_ast : 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 -> diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 219ed6cd8..47e7a8627 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -513,6 +513,8 @@ let disambiguate_macro 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 @@ -529,6 +531,10 @@ let disambiguate_macro | 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 diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.mli b/helm/software/components/grafite_parser/grafiteDisambiguate.mli index 798fa75f5..f482741f3 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli @@ -52,5 +52,5 @@ val disambiguate_macro: 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 diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 976bea700..558eed081 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -524,6 +524,8 @@ EXTEND 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; diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index d585cfbee..e1821ed88 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -325,3 +325,15 @@ let procedural_txt_of_cic_term ~map_unicode_to_tex n ?depth context term = ~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 +;; + + diff --git a/helm/software/matita/applyTransformation.mli b/helm/software/matita/applyTransformation.mli index 06bea6cc6..95712f78e 100644 --- a/helm/software/matita/applyTransformation.mli +++ b/helm/software/matita/applyTransformation.mli @@ -78,6 +78,12 @@ val txt_of_inline_macro: ?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 -> diff --git a/helm/software/matita/dist/ChangeLog b/helm/software/matita/dist/ChangeLog index 66d728fa3..3fe53afa6 100644 --- a/helm/software/matita/dist/ChangeLog +++ b/helm/software/matita/dist/ChangeLog @@ -1,4 +1,5 @@ 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 diff --git a/helm/software/matita/help/C/sec_commands.xml b/helm/software/matita/help/C/sec_commands.xml index 4d788f39a..102e375ad 100644 --- a/helm/software/matita/help/C/sec_commands.xml +++ b/helm/software/matita/help/C/sec_commands.xml @@ -74,6 +74,32 @@ + + eval + eval red on t + + + + Synopsis: + + eval + &reduction-kind; + on + &term; + + + + Action: + + Opens a CIC browser window that shows + the reduct of + t + together with its type. + + + + + coercion coercion u with ariety saturation nocomposites diff --git a/helm/software/matita/matita.lang b/helm/software/matita/matita.lang index 3c9b1fa79..6c0f4c8dc 100644 --- a/helm/software/matita/matita.lang +++ b/helm/software/matita/matita.lang @@ -177,6 +177,7 @@ inline procedural check + eval hint set auto diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index cbaa08721..65d7be828 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -378,33 +378,22 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status (* 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) -> @@ -414,14 +403,14 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status | _ -> 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 *) @@ -436,7 +425,8 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status 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 @@ -472,6 +462,32 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status 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 =