X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=22f14db13aefed439158fd04be4c3695bc115fd9;hb=f6b7c6ae353e014761a3d24dbc87e00d828d7f2d;hp=b4a20c20259347bca72f16a95505fe989967664a;hpb=729e08f5fb86b3ffee460fda4577b024ab5888aa;p=helm.git

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index b4a20c202..22f14db13 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -36,65 +36,6 @@ type options = {
   do_heavy_checks: bool ; 
 }
 
-let concat_nuris uris nuris =
-   match uris,nuris with
-   | `New uris, `New nuris -> `New (nuris@uris)
-   | _ -> assert false
-;;
-
-type eval_ast =
- {ea_go:
-  'term 'lazy_term 'reduction 'obj 'ident.
-
-  disambiguate_command:
-   (GrafiteTypes.status ->
-    (GrafiteAst.command) disambiguator_input ->
-    GrafiteTypes.status * GrafiteAst.command) ->
-
-  ?do_heavy_checks:bool ->
-  GrafiteTypes.status ->
-  (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement)
-  disambiguator_input ->
-  GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
- }
-
-type 'a eval_command =
- {ec_go: 'term 'obj.
-  disambiguate_command:
-   (GrafiteTypes.status -> GrafiteAst.command disambiguator_input ->
-    GrafiteTypes.status * GrafiteAst.command) -> 
-  options -> GrafiteTypes.status -> 
-    GrafiteAst.command disambiguator_input ->
-   GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
- }
-
-type 'a eval_comment =
- {ecm_go: 'term 'lazy_term 'reduction_kind 'obj 'ident.
-  disambiguate_command:
-   (GrafiteTypes.status -> GrafiteAst.command disambiguator_input ->
-    GrafiteTypes.status * GrafiteAst.command) -> 
-  options -> GrafiteTypes.status -> 
-    (('term,'lazy_term,'reduction_kind,'obj,'ident) GrafiteAst.comment) disambiguator_input ->
-   GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
- }
-
-type 'a eval_executable =
- {ee_go: 'term 'lazy_term 'reduction 'obj 'ident.
-
-  disambiguate_command:
-   (GrafiteTypes.status ->
-    GrafiteAst.command disambiguator_input ->
-    GrafiteTypes.status * GrafiteAst.command) ->
-
-  options ->
-  GrafiteTypes.status ->
-  (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code) disambiguator_input ->
-  GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
- }
-
-type 'a eval_from_moo =
- { efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status }
-      
 let basic_eval_unification_hint (t,n) status =
  NCicUnifHint.add_user_provided_hint status t n
 ;;
@@ -120,7 +61,7 @@ let eval_unification_hint status t n =
  let status = basic_eval_unification_hint (t,n) status in
  let dump = inject_unification_hint (t,n)::status#dump in
  let status = status#set_dump dump in
-  status,`New []
+  status,[]
 ;;
 
 let basic_index_obj l status =
@@ -269,18 +210,7 @@ let eval_add_constraint status u1 u2 =
  let status = basic_eval_add_constraint (u1,u2) status in
  let dump = inject_constraint (u1,u2)::status#dump in
  let status = status#set_dump dump in
-  status,`New []
-;;
-
-let eval_ng_punct (_text, _prefix_len, punct) =
-  match punct with
-  | GrafiteAst.Dot _ -> NTactics.dot_tac 
-  | GrafiteAst.Semicolon _ -> fun x -> x
-  | GrafiteAst.Branch _ -> NTactics.branch_tac ~force:false
-  | GrafiteAst.Shift _ -> NTactics.shift_tac 
-  | GrafiteAst.Pos (_,l) -> NTactics.pos_tac l
-  | GrafiteAst.Wildcard _ -> NTactics.wildcard_tac 
-  | GrafiteAst.Merge _ -> NTactics.merge_tac 
+  status,[]
 ;;
 
 let eval_ng_tac tac =
@@ -449,7 +379,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
            let uris = uri::List.rev uris_rev in
 *)
            let status = status#set_ng_mode `CommandMode in
-           let status = LexiconSync.add_aliases_for_objs status (`New [uri]) in
+           let status = LexiconSync.add_aliases_for_objs status [uri] in
            let status,uris =
             List.fold_left
              (fun (status,uris) boxml ->
@@ -464,13 +394,13 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                     status, uris
                   end
                 else
-                  nstatus, concat_nuris uris nuris
+                  nstatus, uris@nuris
                with
                | MultiPassDisambiguator.DisambiguationError _
                | NCicTypeChecker.TypeCheckerFailure _ ->
                   (*HLog.warn "error in generating projection/eliminator";*)
                   status,uris
-             ) (status,`New [] (* uris *)) boxml in             
+             ) (status,[] (* uris *)) boxml in             
            let _,_,_,_,nobj = obj in 
            let status = match nobj with
                NCic.Inductive (is_ind,leftno,[it],_) ->
@@ -487,7 +417,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                        let _,_,menv,_,_ = invobj in
                        fst (match menv with
                              [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
-                           | _ -> status,`New []))
+                           | _ -> status,[]))
                        (* XXX *)
                       with _ -> (*HLog.warn "error in generating inversion principle"; *)
                                 let status = status#set_ng_mode `CommandMode in status)
@@ -518,7 +448,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                      basic_eval_and_record_ncoercion_from_t_cpos_arity 
                       status (name,t,cpos,arity)
                  in
-                 let uris = concat_nuris nuris uris in
+                 let uris = nuris@uris in
                  status, uris
                with MultiPassDisambiguator.DisambiguationError _-> 
                  HLog.warn ("error in generating coercion: "^name);
@@ -577,7 +507,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
       (match nmenv with
           [] ->
            eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
-        | _ -> status,`New [])
+        | _ -> status,[])
   | GrafiteAst.NDiscriminator (_,_) -> assert false (*(loc, indty) ->
       if status#ng_mode <> `CommandMode then
         raise (GrafiteTypes.Command_error "Not in command mode")
@@ -595,7 +525,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
           (match menv with
                [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
              | _ -> prerr_endline ("Discriminator: non empty metasenv");
-                    status, `New []) *)
+                    status, []) *)
   | GrafiteAst.NInverter (loc, name, indty, selection, sort) ->
      if status#ng_mode <> `CommandMode then
       raise (GrafiteTypes.Command_error "Not in command mode")
@@ -631,45 +561,41 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
       eval_add_constraint status [`Type,u1] [`Type,u2]
 ;;
 
-let rec eval_command = {ec_go = fun ~disambiguate_command opts status
-(text,prefix_len,cmd) ->
+let eval_comment ~disambiguate_command opts status (text,prefix_len,c) =
+ status, []
+
+let rec eval_command ~disambiguate_command opts status (text,prefix_len,cmd) =
  let status,cmd = disambiguate_command status (text,prefix_len,cmd) in
  let status,uris =
   match cmd with
-  | GrafiteAst.Drop loc -> raise Drop
-  | GrafiteAst.Include (loc, mode, new_or_old, baseuri) ->
-     (* Old Include command is not recursive; new one is *)
+  | GrafiteAst.Include (loc, baseuri) ->
      let status =
-      if new_or_old = `OldAndNew then
-       let moopath_rw, moopath_r = 
-        LibraryMisc.obj_file_of_baseuri 
-          ~must_exist:false ~baseuri ~writable:true,
-        LibraryMisc.obj_file_of_baseuri 
-          ~must_exist:false ~baseuri ~writable:false in
-       let moopath = 
-        if Sys.file_exists moopath_r then moopath_r else
-          if Sys.file_exists moopath_rw then moopath_rw else
-            raise (IncludedFileNotCompiled (moopath_rw,baseuri))
-       in
-        eval_from_moo.efm_go status moopath
-      else
-       status
+      let moopath_rw, moopath_r = 
+       LibraryMisc.obj_file_of_baseuri 
+         ~must_exist:false ~baseuri ~writable:true,
+       LibraryMisc.obj_file_of_baseuri 
+         ~must_exist:false ~baseuri ~writable:false in
+      let moopath = 
+       if Sys.file_exists moopath_r then moopath_r else
+         if Sys.file_exists moopath_rw then moopath_rw else
+           raise (IncludedFileNotCompiled (moopath_rw,baseuri))
+      in
+       eval_from_moo status moopath
      in
       let status =
        NCicLibrary.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
         status in
       let status =
        GrafiteTypes.add_moo_content
-        [GrafiteAst.Include (loc,mode,`New,baseuri)] status
+        [GrafiteAst.Include (loc,baseuri)] status
       in
-       status,`New []
-  | GrafiteAst.Print (_,_) -> status,`New []
-  | GrafiteAst.Set (loc, name, value) -> status, `New []
+       status,[]
+  | GrafiteAst.Print (_,_) -> status,[]
+  | GrafiteAst.Set (loc, name, value) -> status, []
  in
   status,uris
 
-} and eval_executable = {ee_go = fun ~disambiguate_command
- opts status (text,prefix_len,ex) ->
+and eval_executable ~disambiguate_command opts status (text,prefix_len,ex) =
   match ex with
   | GrafiteAst.NTactic (_(*loc*), tacl) ->
       if status#ng_mode <> `ProofMode then
@@ -682,15 +608,15 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
             subst_metasenv_and_fix_names status)
           status tacl
        in
-        status,`New []
+        status,[]
   | GrafiteAst.Command (_, cmd) ->
-      eval_command.ec_go ~disambiguate_command opts status (text,prefix_len,cmd)
+      eval_command ~disambiguate_command opts status (text,prefix_len,cmd)
   | GrafiteAst.NCommand (_, cmd) ->
       eval_ncommand opts status (text,prefix_len,cmd)
   | GrafiteAst.NMacro (loc, macro) ->
      raise (NMacro (loc,macro))
 
-} and eval_from_moo = {efm_go = fun status fname ->
+and eval_from_moo status fname =
   let ast_of_cmd cmd =
     ("",0,GrafiteAst.Executable (HExtlib.dummy_floc,
       GrafiteAst.Command (HExtlib.dummy_floc,
@@ -701,28 +627,20 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
     (fun status ast -> 
       let ast = ast_of_cmd ast in
       let status,lemmas =
-       eval_ast.ea_go
-         ~disambiguate_command:(fun status (_,_,cmd) -> status,cmd)
+       eval_ast ~disambiguate_command:(fun status (_,_,cmd) -> status,cmd)
          status ast
       in
-       assert (lemmas=`New []);
+       assert (lemmas=[]);
        status)
     status moo
-} and eval_ast = {ea_go = fun ~disambiguate_command
-?(do_heavy_checks=false) status
+
+and eval_ast ~disambiguate_command ?(do_heavy_checks=false) status
 (text,prefix_len,st)
-->
+=
   let opts = { do_heavy_checks = do_heavy_checks ; } in
   match st with
   | GrafiteAst.Executable (_,ex) ->
-     eval_executable.ee_go ~disambiguate_command
-      opts status (text,prefix_len,ex)
+     eval_executable ~disambiguate_command opts status (text,prefix_len,ex)
   | GrafiteAst.Comment (_,c) -> 
-      eval_comment.ecm_go ~disambiguate_command opts status (text,prefix_len,c) 
-} and eval_comment = { ecm_go = fun ~disambiguate_command opts status (text,prefix_len,c) -> 
-    status, `New []
-}
+      eval_comment ~disambiguate_command opts status (text,prefix_len,c) 
 ;;
-
-
-let eval_ast = eval_ast.ea_go