]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaInterpreter.ml
connected change tactic (proof of concept)
[helm.git] / helm / matita / matitaInterpreter.ml
index c9d5a71612d7e1893c11b033307b518d54759eec..4d3137d55e74e56bea5de9e36979a7993b2a2e74 100644 (file)
@@ -47,7 +47,7 @@ let uri name =
 *)
 
 let baseuri = lazy (ref ("cic:/matita/" ^ Helm_registry.get "matita.owner"))
-let basedir = ref ((Unix.getpwuid (Unix.getuid ())).Unix.pw_dir) ;;
+let basedir = lazy (ref (Helm_registry.get "matita.basedir"))
 
 let qualify name =
   let baseuri = !(Lazy.force baseuri) in
@@ -60,45 +60,17 @@ let split_obj = function
   | Cic.Variable (name, body, ty, _, attrs) -> (name, body, ty, attrs)
   | _ -> assert false
 
-let canonical_context metano metasenv =
-  try
-    let (_, context, _) = List.find (fun (m, _, _) -> m = metano) metasenv in
-    context
-  with Not_found ->
-    failwith (sprintf "Can't find canonical context for %d" metano)
-
-let get_context_and_metasenv (currentProof:MatitaTypes.currentProof) =
-  if currentProof#onGoing () then
-    let proof = currentProof#proof in
-    let metasenv = proof#metasenv in
-    let goal = proof#goal in
-    (canonical_context goal metasenv, metasenv)
-  else
-    ([], [])
-
-  (** term AST -> Cic.term. Uses disambiguator and change imperatively the
-  * metasenv as needed *)
-let disambiguate ~(disambiguator:MatitaTypes.disambiguator) ~currentProof ast =
-  if currentProof#onGoing () then begin
-    let proof = currentProof#proof in
-    let metasenv = proof#metasenv in
-    let goal = proof#goal in
-    let context = canonical_context goal metasenv in
-    let (_, metasenv, term,ugraph) as retval =
-      disambiguator#disambiguateTermAst ~context ~metasenv ast
-    in
-    proof#set_metasenv metasenv;
-    retval
-  end else
-    disambiguator#disambiguateTermAst ast
-
 class virtual interpreterState = 
     (* static values, shared by all states inheriting this class *)
   let loc = ref None in
   let history = ref [] in
-  fun ~(console: MatitaTypes.console) ->
+  fun ~(console: #MatitaTypes.console) ->
   object (self)
 
+    val dbd = MatitaMisc.dbd_instance ()
+    val currentProof = MatitaProof.instance ()
+    val disambiguator = MatitaDisambiguator.instance ()
+
       (** eval a toplevel phrase in the current state and return the new state
       *)
     method parsePhrase s =
@@ -134,11 +106,8 @@ class virtual interpreterState =
 
   (** Implements phrases that should be accepted in all states *)
 class sharedState
-  ~(disambiguator: MatitaTypes.disambiguator)
-  ~(currentProof: MatitaTypes.currentProof)
-  ~(console: MatitaTypes.console)
+  ~(console: #MatitaTypes.console)
   ?(mathViewer: MatitaTypes.mathViewer option)
-  ~(dbd: Mysql.dbd)
   ()
 =
   object (self)
@@ -159,17 +128,20 @@ class sharedState
             !(Lazy.force baseuri));
           Quiet
       | TacticAst.Command (TacticAst.Basedir (Some path)) ->
-          basedir := path;
+          Lazy.force basedir := path;
           console#echo_message (sprintf "base dir set to \"%s\"" path);
           Quiet
       | TacticAst.Command (TacticAst.Basedir None) ->
-          console#echo_message (sprintf "base dir is \"%s\"" !basedir);
+          console#echo_message (sprintf "base dir is \"%s\""
+            !(Lazy.force basedir));
           Quiet
       | TacticAst.Command (TacticAst.Check term) ->
           let (_, _, term,ugraph) = 
-           disambiguate ~disambiguator ~currentProof term 
+           MatitaCicMisc.disambiguate ~disambiguator ~currentProof term 
          in
-          let (context, metasenv) = get_context_and_metasenv currentProof in
+          let (context, metasenv) =
+            MatitaCicMisc.get_context_and_metasenv currentProof
+          in
 (* this is the Eval Compute
           let term = CicReduction.whd context term in
 *)         
@@ -179,10 +151,9 @@ class sharedState
          in
            (* TASSI: here ugraph1 is unused.... FIXME *)
           let expr = Cic.Cast (term, ty) in
-          let sequent = (dummyno, context, expr) in
           (match mathViewer with
-          | None -> ()
-          | Some v -> v#checkTerm sequent metasenv);
+          | Some v -> v#checkTerm (`Cic expr)
+          | _ -> ());
           Quiet
       | TacticAst.Command (TacticAst.Search_pat (search_kind, pat)) ->
           let uris =
@@ -283,14 +254,26 @@ let inddef_of_ast params indTypes (disambiguator:MatitaTypes.disambiguator) =
   let cicIndTypes = List.rev cicIndTypes in
   (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
 
-let 
- save_object_to_disk uri obj 
-=
+let save_object_to_disk uri obj =
+  let ensure_path_exists path =
+    let dir = Filename.dirname path in
+    try 
+      let stats = Unix.stat dir in
+      if stats.Unix.st_kind <> Unix.S_DIR then
+        raise (Failure (dir ^ " already exists and is not a directory"))
+      else
+        ()
+    with
+      Unix.Unix_error (_,_,_) -> 
+        let pstatus = Unix.system ("mkdir -p " ^ dir) in
+        match pstatus with
+        | Unix.WEXITED n when n = 0 -> ()
+        | _ -> raise (Failure ("Unable to create " ^ dir))
+  in
   (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
   let annobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ =
     Cic2acic.acic_object_of_cic_object ~eta_fix:false obj
   in 
-
   (* prepare XML *)
   let xml, bodyxml =
    Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
@@ -300,45 +283,41 @@ let
    Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
     ~ask_dtd_to_the_getter:false
   in
-  
   (* prepare URIs and paths *)
   let innertypesuri = UriManager.innertypesuri_of_uri uri in
   let bodyuri = UriManager.bodyuri_of_uri uri in
   let innertypesfilename = Str.replace_first (Str.regexp "^cic:") ""
-        (UriManager.string_of_uri innertypesuri) ^ ".xml" in
-  let innertypespath = !basedir ^ "/" ^ innertypesfilename in
-  let xmlfilename = Str.replace_first (Str.regexp "^cic:") ""
-        (UriManager.string_of_uri uri) ^ ".xml" in
-  let xmlpath = !basedir ^ "/" ^ xmlfilename in
-  let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:") ""
-        (UriManager.string_of_uri uri) ^ ".body.xml" in
-  let xmlbodypath = !basedir ^ "/" ^  xmlbodyfilename in
-  let path_scheme_of path = "file:/" ^ path in
-
+        (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in
+  let innertypespath = !(Lazy.force basedir) ^ "/" ^ innertypesfilename in
+  let xmlfilename = Str.replace_first (Str.regexp "^cic:/") ""
+        (UriManager.string_of_uri uri) ^ ".xml.gz" in
+  let xmlpath = !(Lazy.force basedir) ^ "/" ^ xmlfilename in
+  let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") ""
+        (UriManager.string_of_uri uri) ^ ".body.xml.gz" in
+  let xmlbodypath = !(Lazy.force basedir) ^ "/" ^  xmlbodyfilename in
+  let path_scheme_of path = "file://" ^ path in
+  MatitaMisc.mkdirs (List.map Filename.dirname [innertypespath; xmlpath]);
    (* now write to disk *)
-    Xml.pp ~quiet:true xmlinnertypes (Some innertypespath) ;
-    Xml.pp ~quiet:true xml (Some xmlpath) ;
-
+    ensure_path_exists innertypespath;
+    Xml.pp ~gzip:true xmlinnertypes (Some innertypespath) ;
+    ensure_path_exists xmlpath;
+    Xml.pp ~gzip:true xml (Some xmlpath) ;
+    
    (* now register to the getter *)
     Http_getter.register' innertypesuri (path_scheme_of innertypespath); 
     Http_getter.register' uri (path_scheme_of xmlpath);
-   
     (* now the optional body, both write and register *)
     (match bodyxml,bodyuri with
        None,None -> ()
      | Some bodyxml,Some bodyuri->
-         Xml.pp ~quiet:true bodyxml (Some xmlbodypath) ;
+         ensure_path_exists xmlbodypath;
+         Xml.pp ~gzip:true bodyxml (Some xmlbodypath) ;
          Http_getter.register' bodyuri (path_scheme_of xmlbodypath)
      | _-> assert false) 
-;;
-
-
 
-  (* TODO Zack a lot more to be done here:
-    * - save object to disk in xml format
-    * - register uri to the getter 
+  (* TODO ZACK a lot more to be done here:
     * - save universe file *)
-let add_constant_to_world ~(console:MatitaTypes.console)
+let add_constant_to_world ~(console: #MatitaTypes.console)
   ~dbd ~uri ?body ~ty ?(params = []) ?(attrs = []) ~ugraph ()
 =
   let suri = UriManager.string_of_uri uri in
@@ -349,13 +328,12 @@ let add_constant_to_world ~(console:MatitaTypes.console)
     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
-      ~owner:(Helm_registry.get "matita.owner") ~uri ~body ~ty;
+    MetadataDb.index_constant ~dbd ~uri ~body ~ty;
     save_object_to_disk uri obj;  
     console#echo_message (sprintf "%s constant defined" suri)
   end
 
-let add_inductive_def_to_world ~(console:MatitaTypes.console)
+let add_inductive_def_to_world ~(console: #MatitaTypes.console)
   ~dbd ~uri ~indTypes ?(params = []) ?(leftno = 0) ?(attrs = []) ~ugraph ()
 =
   let suri = UriManager.string_of_uri uri in
@@ -366,8 +344,7 @@ let add_inductive_def_to_world ~(console:MatitaTypes.console)
     let obj = Cic.InductiveDefinition (indTypes, 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
-      ~owner:(Helm_registry.get "matita.owner") ~uri ~types:indTypes;
+    MetadataDb.index_inductive_def ~dbd ~uri ~types:indTypes;
     save_object_to_disk uri obj;  
     console#echo_message (sprintf "%s inductive type defined" suri);
     let elim sort =
@@ -389,17 +366,8 @@ let add_inductive_def_to_world ~(console:MatitaTypes.console)
   end
 
   (** Implements phrases that should be accepted only in Command state *)
-class commandState
-  ~(disambiguator: MatitaTypes.disambiguator)
-  ~(currentProof: MatitaTypes.currentProof)
-  ~(console: MatitaTypes.console)
-  ?mathViewer
-  ~(dbd: Mysql.dbd)
-  ()
-=
-  let shared =
-    new sharedState ~disambiguator ~currentProof ~console ?mathViewer ~dbd ()
-  in
+class commandState ~(console: #MatitaTypes.console) ?mathViewer () =
+  let shared = new sharedState ~console ?mathViewer () in
   object (self)
     inherit interpreterState ~console
 
@@ -548,67 +516,65 @@ let namer_of names =
 
   (** Implements phrases that should be accepted only in Proof state, basically
   * tacticals *)
-class proofState
-  ~(disambiguator: MatitaTypes.disambiguator)
-  ~(currentProof: MatitaTypes.currentProof)
-  ~(console: MatitaTypes.console)
-  ?mathViewer
-  ~(dbd: Mysql.dbd)
-  ()
-=
-  let disambiguate ast =
-    let (_, _, term, _) = disambiguate ~disambiguator ~currentProof ast in
-    term
-  in
-    (** tactic AST -> ProofEngineTypes.tactic *)
-  let rec lookup_tactic = function
-    | TacticAst.LocatedTactic (_, tactic) -> lookup_tactic tactic
-    | TacticAst.Intros (_, names) ->  (* TODO Zack implement intros length *)
-        PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
-    | TacticAst.Reflexivity -> Tactics.reflexivity
-    | TacticAst.Assumption -> Tactics.assumption
-    | TacticAst.Contradiction -> Tactics.contradiction
-    | TacticAst.Exists -> Tactics.exists
-    | TacticAst.Fourier -> Tactics.fourier
-    | TacticAst.Left -> Tactics.left
-    | TacticAst.Right -> Tactics.right
-    | TacticAst.Ring -> Tactics.ring
-    | TacticAst.Split -> Tactics.split
-    | TacticAst.Symmetry -> Tactics.symmetry
-    | TacticAst.Transitivity term -> Tactics.transitivity (disambiguate term)
-    | TacticAst.Apply term -> Tactics.apply (disambiguate term)
-    | TacticAst.Absurd term -> Tactics.absurd (disambiguate term)
-    | TacticAst.Exact term -> Tactics.exact (disambiguate term)
-    | TacticAst.Cut term -> Tactics.cut (disambiguate term)
-    | TacticAst.Elim (term, _) -> (* TODO Zack implement "using" argument *)
-        Tactics.elim_intros_simpl (disambiguate term)
-    | TacticAst.ElimType term -> Tactics.elim_type (disambiguate term)
-    | TacticAst.Replace (what, with_what) ->
-        Tactics.replace ~what:(disambiguate what)
-          ~with_what:(disambiguate with_what)
-    | TacticAst.Auto -> Tactics.auto_new ~dbd
-  (*
-    (* TODO Zack a lot more of tactics to be implemented here ... *)
-    | TacticAst.Change of 'term * 'term * 'ident option
-    | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
-    | TacticAst.Decompose of 'ident * 'ident list
-    | TacticAst.Discriminate of 'ident
-    | TacticAst.Fold of reduction_kind * 'term
-    | TacticAst.Injection of 'ident
-    | TacticAst.LetIn of 'term * 'ident
-    | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
-    | TacticAst.Replace_pattern of 'term pattern * 'term
-    | TacticAst.Rewrite of direction * 'term * 'ident option
-  *)
-    | _ ->
-        MatitaTypes.not_implemented "some tactic"
-  in
-  let shared =
-    new sharedState ~disambiguator ~currentProof ~console ?mathViewer ~dbd ()
-  in
+class proofState ~(console: #MatitaTypes.console) ?mathViewer () =
+  let shared = new sharedState ~console ?mathViewer () in
   object (self)
     inherit interpreterState ~console
 
+    method private disambiguate ast =
+      let (_, _, term, _) =
+        MatitaCicMisc.disambiguate ~disambiguator ~currentProof ast
+      in
+      term
+
+    (** tactic AST -> ProofEngineTypes.tactic *)
+    method private lookup_tactic = function
+      | TacticAst.LocatedTactic (_, tactic) -> self#lookup_tactic tactic
+      | TacticAst.Intros (_, names) ->  (* TODO Zack implement intros length *)
+          PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names)
+            ()
+      | TacticAst.Reflexivity -> Tactics.reflexivity
+      | TacticAst.Assumption -> Tactics.assumption
+      | TacticAst.Contradiction -> Tactics.contradiction
+      | TacticAst.Exists -> Tactics.exists
+      | TacticAst.Fourier -> Tactics.fourier
+      | TacticAst.Left -> Tactics.left
+      | TacticAst.Right -> Tactics.right
+      | TacticAst.Ring -> Tactics.ring
+      | TacticAst.Split -> Tactics.split
+      | TacticAst.Symmetry -> Tactics.symmetry
+      | TacticAst.Transitivity term ->
+          Tactics.transitivity (self#disambiguate term)
+      | TacticAst.Apply term -> Tactics.apply (self#disambiguate term)
+      | TacticAst.Absurd term -> Tactics.absurd (self#disambiguate term)
+      | TacticAst.Exact term -> Tactics.exact (self#disambiguate term)
+      | TacticAst.Cut term -> Tactics.cut (self#disambiguate term)
+      | TacticAst.Elim (term, _) -> (* TODO Zack implement "using" argument *)
+          Tactics.elim_intros_simpl (self#disambiguate term)
+      | TacticAst.ElimType term -> Tactics.elim_type (self#disambiguate term)
+      | TacticAst.Replace (what, with_what) ->
+          Tactics.replace ~what:(self#disambiguate what)
+            ~with_what:(self#disambiguate with_what)
+      | TacticAst.Auto -> Tactics.auto_new ~dbd
+      | TacticAst.Change (what, with_what, _) ->
+          let what = self#disambiguate what in
+          let with_what = self#disambiguate with_what in
+          Tactics.change ~what ~with_what
+    (*
+      (* TODO Zack a lot more of tactics to be implemented here ... *)
+      | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
+      | TacticAst.Change of 'term * 'term * 'ident option
+      | TacticAst.Decompose of 'ident * 'ident list
+      | TacticAst.Discriminate of 'ident
+      | TacticAst.Fold of reduction_kind * 'term
+      | TacticAst.Injection of 'ident
+      | TacticAst.LetIn of 'term * 'ident
+      | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
+      | TacticAst.Replace_pattern of 'term pattern * 'term
+      | TacticAst.Rewrite of direction * 'term * 'ident option
+    *)
+      | _ -> MatitaTypes.not_implemented "some tactic"
+
     method evalTactical = function
       | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical
       | TacticAst.Command TacticAst.Abort ->
@@ -638,7 +604,6 @@ class proofState
           if not b then failwith "Wrong proof";
           add_constant_to_world ~console ~dbd ~uri ~body:bo ~ty ~ugraph ();
           currentProof#abort ();
-          (match mathViewer with None -> () | Some v -> v#unload ());
           console#echo_message (sprintf "%s defined" suri);
           New_state Command
       | TacticAst.Seq tacticals ->
@@ -646,26 +611,15 @@ class proofState
           List.iter (fun t -> ignore (self#evalTactical t)) tacticals;
           New_state Proof
       | TacticAst.Tactic tactic_phrase ->
-          let tactic = lookup_tactic tactic_phrase in
+          let tactic = self#lookup_tactic tactic_phrase in
           currentProof#proof#apply_tactic tactic;
           New_state Proof
       | tactical -> shared#evalTactical tactical
   end
 
-class interpreter
-  ~(disambiguator: MatitaTypes.disambiguator)
-  ~(currentProof: MatitaTypes.currentProof)
-  ~(console: MatitaTypes.console)
-  ?mathViewer
-  ~(dbd: Mysql.dbd)
-  ()
-=
-  let commandState =
-    new commandState ~disambiguator ~currentProof ~console ?mathViewer ~dbd ()
-  in
-  let proofState =
-    new proofState ~disambiguator ~currentProof ~console ?mathViewer ~dbd ()
-  in
+class interpreter ~(console: #MatitaTypes.console) ?mathViewer () =
+  let commandState = new commandState ~console ?mathViewer () in
+  let proofState = new proofState ~console ?mathViewer () in
   object (self)
     val mutable state = commandState
 
@@ -691,3 +645,6 @@ class interpreter
     method evalAst ast = self#eval (fun () -> state#evalAst ast)
   end
 
+let interpreter ~(console: #MatitaTypes.console) ?mathViewer () =
+  new interpreter ~console ?mathViewer ()
+