X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaScript.ml;h=c64653c798bde6e90382880bd5070e060657e260;hb=195cc290eb6e6dc5d5dc9b34bddef083c5c5b0b8;hp=94a7d1424c46c1f9846962bd74d91d86f1cad451;hpb=de9a83f286eee12117fb478ea2db18f7faebac9a;p=helm.git

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 94a7d1424..c64653c79 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,69 @@ 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.Match (_,term) -> 
+        let dbd = MatitaDb.instance () in
+        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 (_env,_metasenv,term,_graph) = 
+          let interps =
+            MatitaDisambiguator.disambiguate_term dbd context metasenv aliases term 
+          in
+          match interps with 
+          | [x] -> x
+          | _ -> assert false
+        in
+        List.iter prerr_endline (MetadataQuery.match_term ~dbd:dbd term);
+        assert false;
+     | TacticAst.Instance (_,term) ->
+        let dbd = MatitaDb.instance () in
+        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 (_env,_metasenv,term,_graph) = 
+          let interps =
+            MatitaDisambiguator.disambiguate_term dbd context metasenv aliases term 
+          in
+          match interps with 
+          | [x] -> x
+          | _ -> assert false
+        in
+        List.iter prerr_endline (MetadataQuery.instance ~dbd term);
+        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 +182,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 +317,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
 
+