X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=0806057ec14ab1d67189dba4832028c6509576db;hb=ddd6560f4e70ec3306d223738a441d5f1dd3eac9;hp=5d1ea50962f211c333732ebc1fafb1622194b640;hpb=2338b758114eb40daf3fadf4fb016a9a1af541b6;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 5d1ea5096..0806057ec 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -33,6 +33,7 @@ exception IncludedFileNotCompiled of string * string
 exception Macro of
  GrafiteAst.loc *
   (Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro)
+exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
 
 type 'a disambiguator_input = string * int * 'a
 
@@ -40,6 +41,11 @@ type options = {
   do_heavy_checks: bool ; 
 }
 
+let concat_nuris uris nuris =
+   match uris,nuris with
+   | `New uris, `New nuris -> `New (nuris@uris)
+   | _ -> assert false
+;;
 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
   * names as long as they are available, then it fallbacks to name generation
   * using FreshNamesGenerator module *)
@@ -495,25 +501,25 @@ let eval_unification_hint status t n =
   status,`New []
 ;;
 
-let basic_eval_add_constraint (s,u1,u2) status =
- NCicLibrary.add_constraint status s u1 u2
+let basic_eval_add_constraint (u1,u2) status =
+ NCicLibrary.add_constraint status u1 u2
 ;;
 
 let inject_constraint =
- let basic_eval_add_constraint (s,u1,u2) 
+ let basic_eval_add_constraint (u1,u2) 
        ~refresh_uri_in_universe 
        ~refresh_uri_in_term
  =
   let u1 = refresh_uri_in_universe u1 in 
   let u2 = refresh_uri_in_universe u2 in 
-  basic_eval_add_constraint (s,u1,u2)
+  basic_eval_add_constraint (u1,u2)
  in
   NRstatus.Serializer.register "constraints" basic_eval_add_constraint
 ;;
 
-let eval_add_constraint status s u1 u2 = 
- let status = basic_eval_add_constraint (s,u1,u2) status in
- let dump = inject_constraint (s,u1,u2)::status#dump in
+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,`Old []
 ;;
@@ -625,7 +631,8 @@ let eval_ng_punct (_text, _prefix_len, punct) =
   | GrafiteAst.Merge _ -> NTactics.merge_tac 
 ;;
 
-let rec eval_ng_tac (text, prefix_len, tac) =
+let eval_ng_tac tac =
+ let rec aux f (text, prefix_len, tac) =
   match tac with
   | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) 
   | GrafiteAst.NAssert (_loc, seqs) ->
@@ -651,6 +658,10 @@ let rec eval_ng_tac (text, prefix_len, tac) =
   | GrafiteAst.NChange (_loc, pat, ww) -> 
       NTactics.change_tac 
        ~where:(text,prefix_len,pat) ~with_what:(text,prefix_len,ww) 
+  | GrafiteAst.NConstructor (_loc,num,args) -> 
+     NTactics.constructor_tac 
+       ?num ~args:(List.map (fun x -> text,prefix_len,x) args)
+  | GrafiteAst.NCut (_loc, t) -> NTactics.cut_tac (text,prefix_len,t) 
   | GrafiteAst.NDot _ -> NTactics.dot_tac 
   | GrafiteAst.NElim (_loc, what, where) ->
       NTactics.elim_tac 
@@ -661,6 +672,7 @@ let rec eval_ng_tac (text, prefix_len, tac) =
       NTactics.generalize_tac ~where:(text,prefix_len,where)
   | GrafiteAst.NId _ -> (fun x -> x)
   | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
+  | GrafiteAst.NLApply (_loc, t) -> NTactics.lapply_tac (text,prefix_len,t) 
   | GrafiteAst.NLetIn (_loc,where,what,name) ->
       NTactics.letin_tac ~where:(text,prefix_len,where) 
         ~what:(text,prefix_len,what) name
@@ -677,8 +689,14 @@ let rec eval_ng_tac (text, prefix_len, tac) =
   | GrafiteAst.NUnfocus _ -> NTactics.unfocus_tac
   | GrafiteAst.NWildcard _ -> NTactics.wildcard_tac 
   | GrafiteAst.NTry (_,tac) -> NTactics.try_tac
-      (eval_ng_tac (text, prefix_len, tac))
+      (aux f (text, prefix_len, tac))
   | GrafiteAst.NAssumption _ -> NTactics.assumption_tac
+  | GrafiteAst.NBlock (_,l) -> 
+      NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l)
+  |GrafiteAst.NRepeat (_,tac) ->
+      NTactics.repeat_tac (f f (text, prefix_len, tac))
+ in
+  aux aux tac (* trick for non uniform recursion call *)
 ;;
       
 let subst_metasenv_and_fix_names status =
@@ -693,6 +711,8 @@ let subst_metasenv_and_fix_names status =
 let rec eval_ncommand opts status (text,prefix_len,cmd) =
   match cmd with
   | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
+  | GrafiteAst.NCoercion (loc, name, t, ty, source, target) ->
+      NCicCoercDeclaration.eval_ncoercion status name t ty source target
   | GrafiteAst.NQed loc ->
      if status#ng_mode <> `ProofMode then
       raise (GrafiteTypes.Command_error "Not in proof mode")
@@ -705,7 +725,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
         let obj_kind =
          NCicUntrusted.map_obj_kind 
           (NCicUntrusted.apply_subst subst []) obj_kind in
-        let height = NCicTypeChecker.height_of_obj_kind uri obj_kind in
+        let height = NCicTypeChecker.height_of_obj_kind uri [] obj_kind in
         (* fix the height inside the object *)
         let rec fix () = function 
           | NCic.Const (NReference.Ref (u,spec)) when NUri.eq u uri -> 
@@ -725,16 +745,105 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
           | _ -> obj_kind
         in
         let obj = uri,height,[],[],obj_kind in
-         let status = NCicLibrary.add_obj status obj in
-         let objs = NCicElim.mk_elims obj in
-         let timestamp,uris_rev =
-           List.fold_left
-            (fun (status,uris_rev) (uri,_,_,_,_) as obj ->
-              let status = NCicLibrary.add_obj status obj in
-               status,uri::uris_rev
-            ) (status,[]) objs in
-         let uris = uri::List.rev uris_rev in
-          status#set_ng_mode `CommandMode,`New uris
+        let old_status = status in
+        let status = NCicLibrary.add_obj status obj in
+        HLog.message ("New object: " ^ NUri.string_of_uri uri);
+         (try
+       (*prerr_endline (NCicPp.ppobj obj);*)
+           let boxml = NCicElim.mk_elims obj in
+           let boxml = boxml @ NCicElim.mk_projections obj in
+(*
+           let objs = [] in
+           let timestamp,uris_rev =
+             List.fold_left
+              (fun (status,uris_rev) (uri,_,_,_,_) as obj ->
+                let status = NCicLibrary.add_obj status obj in
+                 status,uri::uris_rev
+              ) (status,[]) objs in
+           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,uris =
+            List.fold_left
+             (fun (status,uris) boxml ->
+               try
+                let status,nuris =
+                 eval_ncommand opts status
+                  ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml))
+                in
+                status, concat_nuris uris nuris
+               with
+               | MultiPassDisambiguator.DisambiguationError _ 
+               | NCicTypeChecker.TypeCheckerFailure _ ->
+                  HLog.warn "error in generating projection/eliminator";
+                  status,uris
+             ) (status,`New [] (* uris *)) boxml in
+           let coercions =
+            match obj with
+              _,_,_,_,NCic.Inductive
+               (true,leftno,[_,_,_,[_,_,_]],(_,`Record fields))
+               ->
+                HExtlib.filter_map
+                 (fun (name,is_coercion,arity) ->
+                   if is_coercion then Some(name,leftno,arity) else None) fields
+            | _ -> [] in
+           let status,uris =
+            List.fold_left
+             (fun (status,uris) (name,cpos,arity) ->
+               try
+                 let metasenv,subst,status,t =
+                  GrafiteDisambiguate.disambiguate_nterm None status [] [] []
+                   ("",0,CicNotationPt.Ident (name,None)) in
+                 assert (metasenv = [] && subst = []);
+                 let status, nuris = 
+                   NCicCoercDeclaration.
+                     basic_eval_and_record_ncoercion_from_t_cpos_arity 
+                      status (name,t,cpos,arity)
+                 in
+                 let uris = concat_nuris nuris uris in
+                 status, uris
+               with MultiPassDisambiguator.DisambiguationError _-> 
+                 HLog.warn ("error in generating coercion: "^name);
+                 status, uris) 
+             (status,uris) coercions
+           in
+            status,uris
+          with
+           exn ->
+            NCicLibrary.time_travel old_status;
+            raise exn)
+  | GrafiteAst.NCopy (log,tgt,src_uri, map) ->
+     if status#ng_mode <> `CommandMode then
+      raise (GrafiteTypes.Command_error "Not in command mode")
+     else
+       let tgt_uri_ext, old_ok = 
+         match NCicEnvironment.get_checked_obj src_uri with
+         | _,_,[],[], (NCic.Inductive _ as ok) -> ".ind", ok
+         | _,_,[],[], (NCic.Fixpoint _ as ok) -> ".con", ok
+         | _,_,[],[], (NCic.Constant _ as ok) -> ".con", ok
+         | _ -> assert false
+       in
+       let tgt_uri = NUri.uri_of_string (status#baseuri^"/"^tgt^tgt_uri_ext) in
+       let map = (src_uri, tgt_uri) :: map in
+       let ok = 
+         let rec subst () = function
+           | NCic.Meta _ -> assert false
+           | NCic.Const (NReference.Ref (u,spec)) as t ->
+               (try NCic.Const 
+                 (NReference.reference_of_spec (List.assoc u map)spec)
+               with Not_found -> t)
+           | t -> NCicUtils.map (fun _ _ -> ()) () subst t
+         in
+         NCicUntrusted.map_obj_kind ~skip_body:false (subst ()) old_ok
+       in
+       let ninitial_stack = Continuationals.Stack.of_nmetasenv [] in
+       let status = status#set_obj (tgt_uri,0,[],[],ok) in
+       (*prerr_endline (NCicPp.ppobj (tgt_uri,0,[],[],ok));*)
+       let status = status#set_stack ninitial_stack in
+       let status = subst_metasenv_and_fix_names status in
+       let status = status#set_ng_mode `ProofMode in
+       eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
   | GrafiteAst.NObj (loc,obj) ->
      if status#ng_mode <> `CommandMode then
       raise (GrafiteTypes.Command_error "Not in command mode")
@@ -752,8 +861,29 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
           [] ->
            eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
         | _ -> status,`New [])
-  | GrafiteAst.NUnivConstraint (loc,strict,u1,u2) ->
-      eval_add_constraint status strict [false,u1] [false,u2]
+  | GrafiteAst.NInverter (loc, name, indty) ->
+     if status#ng_mode <> `CommandMode then
+      raise (GrafiteTypes.Command_error "Not in command mode")
+     else
+      let status = status#set_ng_mode `ProofMode in
+      let metasenv,subst,status,indty =
+       GrafiteDisambiguate.disambiguate_nterm None status [] [] [] (text,prefix_len,indty) in
+      let _,leftno,tys,_,_ = match indty with
+          NCic.Const r -> NCicEnvironment.get_checked_indtys r
+        | _ -> assert false in
+      let it = match tys with
+          hd::tl -> hd
+        | _ -> assert false
+      in
+     let status,obj =
+      NInversion.mk_inverter name it leftno status status#baseuri in
+     let _,_,menv,_,_ = obj in
+     (match menv with
+        [] ->
+          eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+      | _ -> assert false)
+  | GrafiteAst.NUnivConstraint (loc,u1,u2) ->
+      eval_add_constraint status [`Type,u1] [`Type,u2]
 ;;
 
 let rec eval_command = {ec_go = fun ~disambiguate_command opts status
@@ -820,24 +950,32 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
      LibraryObjects.set_default what uris;
      GrafiteTypes.add_moo_content [cmd] status,`Old []
   | GrafiteAst.Drop loc -> raise Drop
-  | GrafiteAst.Include (loc, _, baseuri) ->
-     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
-     let status = eval_from_moo.efm_go status moopath in
+  | GrafiteAst.Include (loc, mode, new_or_old, baseuri) ->
+     (* Old Include command is not recursive; new one is *)
      let status =
-       NRstatus.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
-        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
      in
-      status,`Old []
+      let status =
+       NRstatus.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
+        status in
+      let status =
+       GrafiteTypes.add_moo_content
+        [GrafiteAst.Include (loc,mode,`New,baseuri)] status
+      in
+       status,`Old []
   | GrafiteAst.Print (_,"proofterm") ->
       let _,_,_,p,_, _ = GrafiteTypes.get_current_proof status in
       prerr_endline (Auto.pp_proofterm (Lazy.force p));
@@ -984,6 +1122,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       eval_ncommand opts status (text,prefix_len,cmd)
   | GrafiteAst.Macro (loc, macro) ->
      raise (Macro (loc,disambiguate_macro status (text,prefix_len,macro)))
+  | GrafiteAst.NMacro (loc, macro) ->
+     raise (NMacro (loc,macro))
 
 } and eval_from_moo = {efm_go = fun status fname ->
   let ast_of_cmd cmd =