attached macros: hint(partial), check

now matitaScript has a mathviewer to show terms...

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 078ba00db77d87346e0a9eb0b0ccdc88001d204c..69295bd7e0793af4c3792092db418e239a60353b 100644 (file)
--- 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 addf9763cc2350125be11b57792f8d41d1a5f506..05f5246e5518bbfbe50de186a51f7376faea3d7c 100644 (file)
--- 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 da187a7c5988d340890e2e1511c4167988b47ecb..e26352dadb1fbaab7dcc9601cc4e3078d68389aa 100644 (file)
--- 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 58fa388091e7c165ff76783141c82e6d55efd798..41b96793884d88546a2cd42ce06101551ddeef44 100644 (file)
--- 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 1d51eca1991f09e75650966f3e0b1720ce8de07c..4f2905a24873e42f62249047f83b9f7a47afd14a 100644 (file)
--- 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 94a7d1424c46c1f9846962bd74d91d86f1cad451..2d1c4d702f023c59b83439e69a62126d4cc83667 100644 (file)
--- 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 2529376f1880b7e3effb524b06ffd5e5002ff675..f7c86fc3c3298a0a79bf9f57edbe89e6be2853da 100644 (file)
--- 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 f14e3d1269044d63e15eec3e931c8bc7ab9e1c1b..fbcac945ae0a50e9d188e5ada89e2210003c8c65 100644 (file)
--- 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 48d419341ca4b2fad4aefbf7891c23dc4b1b868a..454c17a7f521afc53be9b9fc9460d75ba3a4b564 100644 (file)
--- 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
+