attached macros: hint(partial), check

[helm.git] / helm / matita / matitaScript.ml

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
 
+