]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_engine/grafiteEngine.ml
Added an implicit parameter to branch_tac to allow branching on a
[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml
index 310f3793fe943458490b3f29016c0c548713e599..239d30d2d1480ff0b0c354a757cacbf4105cc058 100644 (file)
@@ -507,8 +507,10 @@ let eval_unification_hint status t n =
 let basic_index_obj l status =
   status#set_auto_cache 
     (List.fold_left
-      (fun t (k,v) -> 
-         NDiscriminationTree.DiscriminationTree.index t k v) 
+      (fun t (ks,v) -> 
+         List.fold_left (fun t k ->
+           NDiscriminationTree.DiscriminationTree.index t k v)
+          t ks) 
     status#auto_cache l) 
 ;;     
 
@@ -519,7 +521,7 @@ let record_index_obj =
  =
     basic_index_obj
       (List.map 
-        (fun k,v -> refresh_uri_in_term k, refresh_uri_in_term v) 
+        (fun ks,v -> List.map refresh_uri_in_term ks, refresh_uri_in_term v) 
       l)
  in
   NCicLibrary.Serializer.register#run "index_obj"
@@ -529,19 +531,100 @@ let record_index_obj =
 ;;
 
 let index_obj_for_auto status (uri, height, _, _, kind) = 
+ (*prerr_endline (string_of_int height);*)
+ let mk_item orig_ty spec =
+   let ty,_,_ = NCicMetaSubst.saturate ~delta:max_int [] [] [] orig_ty 0 in
+   let keys = 
+     match ty with
+     | NCic.Const (NReference.Ref (_,NReference.Def h)) 
+     | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Def h))::_) 
+        when h > 0 ->
+          let ty',_,_= NCicMetaSubst.saturate ~delta:(h-1) [] [] [] orig_ty 0 in
+          [ty;ty']
+     | _ -> [ty]
+   in
+   keys,NCic.Const(NReference.reference_of_spec uri spec)
+ in
  let data = 
   match kind with
-  | NCic.Fixpoint _ -> []
-  | NCic.Inductive _ -> []
-  | NCic.Constant (_,_,_, ty, _) ->
-      let ty = (* saturare *) ty in
-      [ty,NCic.Const(NReference.reference_of_spec uri (NReference.Def height))]
+  | NCic.Fixpoint (ind,ifl,_) -> 
+     HExtlib.list_mapi 
+       (fun (_,_,rno,ty,_) i -> 
+          if ind then mk_item ty (NReference.Fix (i,rno,height)) 
+          else mk_item ty (NReference.CoFix height)) ifl
+  | NCic.Inductive (b,lno,itl,_) -> 
+     HExtlib.list_mapi 
+       (fun (_,_,ty,_) i -> mk_item ty (NReference.Ind (b,i,lno))) itl 
+     @
+     List.map (fun ((_,_,ty),i,j) -> mk_item ty (NReference.Con (i,j+1,lno)))
+       (List.flatten (HExtlib.list_mapi 
+         (fun (_,_,_,cl) i -> HExtlib.list_mapi (fun x j-> x,i,j) cl)
+         itl))
+  | NCic.Constant (_,_,Some _, ty, _) -> 
+     [ mk_item ty (NReference.Def height) ]
+  | NCic.Constant (_,_,None, ty, _) ->
+     [ mk_item ty NReference.Decl ]
+ in
+ let data = HExtlib.filter_map
+   (fun (keys, t) ->
+     let keys = List.filter
+       (function 
+         | (NCic.Meta _) 
+         | (NCic.Appl (NCic.Meta _::_)) -> false 
+         | _ -> true) 
+       keys
+     in
+     if keys <> [] then 
+      begin
+        HLog.debug ("Indexing:" ^ 
+          NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
+        HLog.debug ("With keys:" ^ String.concat "\n" (List.map (fun t ->
+          NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t) keys));
+        Some (keys,t) 
+      end
+     else 
+      begin
+        HLog.debug ("Not indexing:" ^ 
+          NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
+        None
+      end)
+   data
  in
  let status = basic_index_obj data status in
  let dump = record_index_obj data :: status#dump in
  status#set_dump dump
 ;; 
 
+let index_eq uri status =
+  let eq_status = status#eq_cache in
+  let eq_status1 = NCicParamod.index_obj eq_status uri in
+    status#set_eq_cache eq_status1
+;;
+
+let record_index_eq =
+ let basic_index_eq uri
+   ~refresh_uri_in_universe 
+   ~refresh_uri_in_term 
+   = index_eq (NCicLibrary.refresh_uri uri) 
+ in
+  NCicLibrary.Serializer.register#run "index_eq"
+   object(_ : 'a NCicLibrary.register_type)
+     method run = basic_index_eq
+   end
+;;
+
+let index_eq_for_auto status uri =
+ if NnAuto.is_a_fact_obj status uri then
+   let newstatus = index_eq uri status in
+     if newstatus#eq_cache == status#eq_cache then status 
+     else
+       ((*prerr_endline ("recording " ^ (NUri.string_of_uri uri));*)
+       let dump = record_index_eq uri :: newstatus#dump 
+       in newstatus#set_dump dump)
+ else 
+   ((*prerr_endline "Not a fact";*)
+   status)
+;; 
 
 let basic_eval_add_constraint (u1,u2) status =
  NCicLibrary.add_constraint status u1 u2
@@ -669,7 +752,7 @@ 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 
+  | GrafiteAst.Branch _ -> NTactics.branch_tac ~force:false
   | GrafiteAst.Shift _ -> NTactics.shift_tac 
   | GrafiteAst.Pos (_,l) -> NTactics.pos_tac l
   | GrafiteAst.Wildcard _ -> NTactics.wildcard_tac 
@@ -680,6 +763,8 @@ 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.NSmartApply (_loc, t) -> 
+      NnAuto.smart_apply_tac (text,prefix_len,t) 
   | GrafiteAst.NAssert (_loc, seqs) ->
      NTactics.assert_tac
       ((List.map
@@ -694,7 +779,7 @@ let eval_ng_tac tac =
   | GrafiteAst.NAuto (_loc, (l,a)) ->
       NAuto.auto_tac
        ~params:(List.map (fun x -> "",0,x) l,a)
-  | GrafiteAst.NBranch _ -> NTactics.branch_tac 
+  | GrafiteAst.NBranch _ -> NTactics.branch_tac ~force:false
   | GrafiteAst.NCases (_loc, what, where) ->
       NTactics.cases_tac 
         ~what:(text,prefix_len,what)
@@ -707,6 +792,9 @@ let eval_ng_tac tac =
      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.NDiscriminate (_,what) -> NDestructTac.discriminate_tac ~what:(text,prefix_len,what)
+  | GrafiteAst.NSubst (_,what) -> NDestructTac.subst_tac ~what:(text,prefix_len,what)*)
+  | GrafiteAst.NDestruct _ -> NDestructTac.destruct_tac
   | GrafiteAst.NDot _ -> NTactics.dot_tac 
   | GrafiteAst.NElim (_loc, what, where) ->
       NTactics.elim_tac 
@@ -723,6 +811,7 @@ let eval_ng_tac tac =
         ~what:(text,prefix_len,what) name
   | GrafiteAst.NMerge _ -> NTactics.merge_tac 
   | GrafiteAst.NPos (_,l) -> NTactics.pos_tac l
+  | GrafiteAst.NPosbyname (_,s) -> NTactics.case_tac s
   | GrafiteAst.NReduce (_loc, reduction, where) ->
       NTactics.reduce_tac ~reduction ~where:(text,prefix_len,where)
   | GrafiteAst.NRewrite (_loc,dir,what,where) ->
@@ -794,6 +883,12 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
         let old_status = status in
         let status = NCicLibrary.add_obj status obj in
         let status = index_obj_for_auto status obj in
+        let status = index_eq_for_auto status uri in
+(*
+         try 
+           index_eq uri status
+         with _ -> prerr_endline "got an exception"; status
+       in *)
 (*         prerr_endline (NCicPp.ppobj obj); *)
         HLog.message ("New object: " ^ NUri.string_of_uri uri);
          (try
@@ -816,11 +911,18 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
             List.fold_left
              (fun (status,uris) boxml ->
                try
-                let status,nuris =
+                let nstatus,nuris =
                  eval_ncommand opts status
                   ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml))
                 in
-                status, concat_nuris uris nuris
+                if nstatus#ng_mode <> `CommandMode then
+                  begin
+                    HLog.error "error in generating projection/eliminator";
+                    prerr_endline (NCicPp.ppobj nstatus#obj);
+                    nstatus, uris
+                  end
+                else
+                  nstatus, concat_nuris uris nuris
                with
                | MultiPassDisambiguator.DisambiguationError _ 
                | NCicTypeChecker.TypeCheckerFailure _ ->
@@ -842,6 +944,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                        fst (match menv with
                              [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
                            | _ -> status,`New []))
+                       (* XXX *)
                       with _ -> HLog.warn "error in generating inversion principle"; 
                                 let status = status#set_ng_mode `CommandMode in status)
                   status
@@ -931,6 +1034,24 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
           [] ->
            eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
         | _ -> status,`New [])
+  | GrafiteAst.NDiscriminator (_,_) -> assert false (*(loc, 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 indtyno, (_,_,tys,_,_) = match indty with
+            NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,_))) as r) ->
+              indtyno, NCicEnvironment.get_checked_indtys r
+          | _ -> prerr_endline ("engine: indty expected... (fix this error message)"); assert false in
+        let it = List.nth tys indtyno in
+        let status,obj =  NDestructTac.mk_discriminator it status in
+        let _,_,menv,_,_ = obj in
+          (match menv with
+               [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+             | _ -> prerr_endline ("Discriminator: non empty metasenv");
+                    status, `New []) *)
   | GrafiteAst.NInverter (loc, name, indty, selection, sort) ->
      if status#ng_mode <> `CommandMode then
       raise (GrafiteTypes.Command_error "Not in command mode")