From 3b5b254f2faa600a14a837e95f94f953dc9959c7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 28 Apr 2005 14:12:22 +0000 Subject: [PATCH] attached macros: hint(partial), check now matitaScript has a mathviewer to show terms... --- helm/matita/matita.ml | 7 ++++-- helm/matita/matitaMathView.ml | 5 +++++ helm/matita/matitaMathView.mli | 9 +++----- helm/matita/matitaMisc.ml | 2 ++ helm/matita/matitaMisc.mli | 1 + helm/matita/matitaScript.ml | 41 +++++++++++++++++++++++++++++----- helm/matita/matitaScript.mli | 7 +++++- helm/matita/matitaSync.ml | 4 ++-- helm/matita/matitaTypes.ml | 11 +++++++++ 9 files changed, 71 insertions(+), 16 deletions(-) diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 078ba00db..69295bd7e 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -59,8 +59,11 @@ let _ = (MatitaGui.interactive_interp_choice ()) let script = - MatitaScript.script ~buffer:gui#main#scriptTextView#buffer - ~init:(Lazy.force MatitaEngine.initial_status) () + MatitaScript.script + ~buffer:gui#main#scriptTextView#buffer + ~init:(Lazy.force MatitaEngine.initial_status) + ~mathviewer:(MatitaMathView.mathViewer ()) + () (* math viewers *) let _ = diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index addf9763c..05f5246e5 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -511,3 +511,8 @@ let default_sequentsViewer () = sequentsViewer ~notebook:gui#main#sequentsNotebook ~sequentViewer () let sequentsViewer_instance = MatitaMisc.singleton default_sequentsViewer + +let mathViewer () = + object + method show_term t = (cicBrowser ()) # loadTerm t + end diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index da187a7c5..e26352dad 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -59,16 +59,11 @@ class type sequentsViewer = exception Browser_failure of string -type term_source = - [ `Ast of DisambiguateTypes.term - | `Cic of Cic.term * Cic.metasenv - | `String of string - ] class type cicBrowser = object method loadUri: string -> unit - method loadTerm: term_source -> unit + method loadTerm: MatitaTypes.term_source -> unit end (** {2 Constructors} *) @@ -105,3 +100,5 @@ val refresh_all_browsers: unit -> unit val sequentViewer_instance: unit -> sequentViewer val sequentsViewer_instance: unit -> sequentsViewer +val mathViewer: unit -> MatitaTypes.mathViewer + diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index 58fa38809..41b967938 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -169,6 +169,8 @@ let get_proof_context status = let (_, context, _) = CicUtil.lookup_meta goal metasenv in context | _ -> [] + +let get_proof_aliases status = status.aliases let qualify status name = get_string_option status "baseuri" ^ "/" ^ name diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli index 1d51eca19..4f2905a24 100644 --- a/helm/matita/matitaMisc.mli +++ b/helm/matita/matitaMisc.mli @@ -83,4 +83,5 @@ val qualify: MatitaTypes.status -> string -> string val get_proof_status: MatitaTypes.status -> ProofEngineTypes.status val get_proof_metasenv: MatitaTypes.status -> Cic.metasenv val get_proof_context: MatitaTypes.status -> Cic.context +val get_proof_aliases: MatitaTypes.status -> DisambiguateTypes.environment diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 94a7d1424..2d1c4d702 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -55,7 +55,7 @@ let goal_ast n = let loc = CicAst.dummy_floc in A.Tactical (loc, A.Tactic (loc, A.Goal (loc, n))) -let eval_statement status user_goal s = +let eval_statement status mathviewer user_goal s = let st = CicTextualParser2.parse_statement (Stream.of_string s) in match st with | TacticAst.Command (loc, _) | TacticAst.Tactical (loc, _) -> @@ -93,10 +93,39 @@ let eval_statement status user_goal s = in [ new_status, new_text ], parsed_text_length | TacticAst.Macro (loc, mac) -> + let parsed_text_length = snd (CicAst.loc_of_floc loc) in (match mac with (* TODO *) + | TacticAst.Hint _ -> + let s = MatitaMisc.get_proof_status status in + let l = List.map fst + (MetadataQuery.experimental_hint ~dbd:(MatitaDb.instance ()) s) + in + List.iter prerr_endline l; + prerr_endline "FINITA LA HINT"; assert false + | TacticAst.Check (_,t) -> + let metasenv = MatitaMisc.get_proof_metasenv status in + let context = MatitaMisc.get_proof_context status in + let aliases = MatitaMisc.get_proof_aliases status in + let db = MatitaDb.instance () in + let (_env,_metasenv,term,_graph) = + let interps = + MatitaDisambiguator.disambiguate_term db context metasenv + aliases t + in + match interps with + | [x] -> x + | _ -> assert false + in + let ty,_ = + CicTypeChecker.type_of_aux' metasenv context term + CicUniv.empty_ugraph + in + mathviewer # show_term (`Cic (ty,metasenv) ); + [ status, "" ] , parsed_text_length | _ -> failwith "not implemented") -class script ~(buffer: GText.buffer) ~(init: MatitaTypes.status) () = +class script ~(buffer: GText.buffer) ~(init: MatitaTypes.status) + ~(mathviewer: MatitaTypes.mathViewer) () = object (self) initializer self#reset () @@ -123,7 +152,8 @@ object (self) let s = match statement with Some s -> s | None -> self#getFuture in if Pcre.pmatch ~rex:blanks_RE s then raise Margin; MatitaLog.debug ("evaluating: " ^ first_line s ^ " ..."); - let (entries, parsed_len) = eval_statement self#status userGoal s in + let (entries, parsed_len) = + eval_statement self#status mathviewer userGoal s in let (new_statuses, new_statements) = List.split entries in (* prerr_endline "evalStatement returned"; @@ -257,10 +287,11 @@ end let _script = ref None -let script ~buffer ~init () = - let s = new script ~buffer ~init () in +let script ~buffer ~init ~mathviewer () = + let s = new script ~buffer ~init ~mathviewer () in _script := Some s; s let instance () = match !_script with None -> assert false | Some s -> s + diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli index 2529376f1..f7c86fc3c 100644 --- a/helm/matita/matitaScript.mli +++ b/helm/matita/matitaScript.mli @@ -61,7 +61,12 @@ object end -val script: buffer:GText.buffer -> init:MatitaTypes.status -> unit -> script +val script: + buffer:GText.buffer -> + init:MatitaTypes.status -> + mathviewer: MatitaTypes.mathViewer-> + unit -> + script (* each time script above is called an internal ref is set, instance will return * the value of this ref *) diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index f14e3d126..fbcac945a 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -103,7 +103,7 @@ let add_constant ~uri ?body ~ty ~ugraph ?(params = []) ?(attrs = []) status = let obj = Cic.Constant (name, body, ty, params, attrs) in let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in CicEnvironment.add_type_checked_term uri (obj, ugraph); - MetadataDb.index_constant ~dbd ~uri ~body ~ty; + MetadataDb.index_obj ~dbd ~uri; (* must be in the env *) let new_stuff = save_object_to_disk status uri obj in MatitaLog.message (sprintf "%s constant defined" suri); { status with objects = new_stuff @ status.objects } @@ -126,7 +126,7 @@ let add_inductive_def let obj = Cic.InductiveDefinition (types, params, leftno, attrs) in let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in CicEnvironment.put_inductive_definition uri (obj, ugraph); - MetadataDb.index_inductive_def ~dbd ~uri ~types:types; + MetadataDb.index_obj ~dbd ~uri; (* must be in the env *) let new_stuff = save_object_to_disk status uri obj in MatitaLog.message (sprintf "%s inductive type defined" suri); let status = { status with objects = new_stuff @ status.objects } in diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 48d419341..454c17a7f 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -145,3 +145,14 @@ class type console = method show : ?msg:string -> unit -> unit end +type term_source = + [ `Ast of DisambiguateTypes.term + | `Cic of Cic.term * Cic.metasenv + | `String of string + ] + +class type mathViewer = + object + method show_term: term_source -> unit + end + -- 2.39.2