X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=6533e3f86397dbfc38b34a552a5b4880427ba0ef;hb=f8830ea7f8b308241d73e558092089a24ab2f867;hp=e02bd159fe0d13544c5cc33252810b2d5bdcff0e;hpb=d6484aac4ff287a3a3646807801eab4b27cfb054;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index e02bd159f..6533e3f86 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -86,11 +86,11 @@ let rec tactic_of_ast status ast =
   | GrafiteAst.ApplyP (_, term) -> Tactics.applyP term
   | GrafiteAst.ApplyS (_, term, params) ->
      Tactics.applyS ~term ~params ~dbd:(LibraryDb.instance ())
-       ~automation_cache:status.GrafiteTypes.automation_cache
+       ~automation_cache:status#automation_cache
   | GrafiteAst.Assumption _ -> Tactics.assumption
   | GrafiteAst.AutoBatch (_,params) ->
       Tactics.auto ~params ~dbd:(LibraryDb.instance ()) 
-	~automation_cache:status.GrafiteTypes.automation_cache
+	~automation_cache:status#automation_cache
   | GrafiteAst.Cases (_, what, pattern, (howmany, names)) ->
       Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(namer_of names)
         ~pattern what
@@ -112,7 +112,7 @@ let rec tactic_of_ast status ast =
   | GrafiteAst.Demodulate (_, params) -> 
       Tactics.demodulate 
 	~dbd:(LibraryDb.instance ()) ~params 
-          ~automation_cache:status.GrafiteTypes.automation_cache
+          ~automation_cache:status#automation_cache
   | GrafiteAst.Destruct (_,xterms) -> Tactics.destruct xterms
   | GrafiteAst.Elim (_, what, using, pattern, (depth, names)) ->
       Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
@@ -183,12 +183,12 @@ let rec tactic_of_ast status ast =
   | GrafiteAst.Suppose (_, t, id, t1) -> Declarative.suppose t id t1
   | GrafiteAst.By_just_we_proved (_, just, ty, id, t1) ->
      Declarative.by_just_we_proved ~dbd:(LibraryDb.instance())
-      ~automation_cache:status.GrafiteTypes.automation_cache just ty id t1
+      ~automation_cache:status#automation_cache just ty id t1
   | GrafiteAst.We_need_to_prove (_, t, id, t2) ->
      Declarative.we_need_to_prove t id t2
   | GrafiteAst.Bydone (_, t) ->
      Declarative.bydone ~dbd:(LibraryDb.instance())
-      ~automation_cache:status.GrafiteTypes.automation_cache t
+      ~automation_cache:status#automation_cache t
   | GrafiteAst.We_proceed_by_cases_on (_, t, t1) ->
      Declarative.we_proceed_by_cases_on t t1
   | GrafiteAst.We_proceed_by_induction_on (_, t, t1) ->
@@ -197,14 +197,14 @@ let rec tactic_of_ast status ast =
   | GrafiteAst.Thesisbecomes (_, t) -> Declarative.thesisbecomes t
   | GrafiteAst.ExistsElim (_, just, id1, t1, id2, t2) ->
      Declarative.existselim ~dbd:(LibraryDb.instance())
-      ~automation_cache:status.GrafiteTypes.automation_cache just id1 t1 id2 t2
+      ~automation_cache:status#automation_cache just id1 t1 id2 t2
   | GrafiteAst.Case (_,id,params) -> Declarative.case id params
   | GrafiteAst.AndElim(_,just,id1,t1,id2,t2) ->
      Declarative.andelim ~dbd:(LibraryDb.instance ())
-      ~automation_cache:status.GrafiteTypes.automation_cache just id1 t1 id2 t2
+      ~automation_cache:status#automation_cache just id1 t1 id2 t2
   | GrafiteAst.RewritingStep (_,termine,t1,t2,cont) ->
      Declarative.rewritingstep ~dbd:(LibraryDb.instance ())
-      ~automation_cache:status.GrafiteTypes.automation_cache termine t1 t2 cont
+      ~automation_cache:status#automation_cache termine t1 t2 cont
 
 let classify_tactic tactic = 
   match tactic with
@@ -347,13 +347,13 @@ let apply_tactic ~disambiguate_tactic (text,prefix_len,tactic) (status, goal) =
   proof', opened_goals
  in
  let incomplete_proof =
-   match status.GrafiteTypes.proof_status with
+   match status#proof_status with
    | GrafiteTypes.Incomplete_proof p -> p
    | _ -> assert false
  in
- { status with GrafiteTypes.proof_status =
-    GrafiteTypes.Incomplete_proof
-     { incomplete_proof with GrafiteTypes.proof = proof } },
+  status#set_proof_status
+   (GrafiteTypes.Incomplete_proof
+     { incomplete_proof with GrafiteTypes.proof = proof }),
  opened_goals, closed_goals
 
 let apply_atomic_tactical ~disambiguate_tactic ~patch (text,prefix_len,tactic) (status, goal) =
@@ -381,13 +381,13 @@ let apply_atomic_tactical ~disambiguate_tactic ~patch (text,prefix_len,tactic) (
   proof', opened_goals
  in
  let incomplete_proof =
-   match status.GrafiteTypes.proof_status with
+   match status#proof_status with
    | GrafiteTypes.Incomplete_proof p -> p
    | _ -> assert false
  in
- { status with GrafiteTypes.proof_status =
-    GrafiteTypes.Incomplete_proof
-     { incomplete_proof with GrafiteTypes.proof = proof } },
+  status#set_proof_status
+   (GrafiteTypes.Incomplete_proof
+     { incomplete_proof with GrafiteTypes.proof = proof }),
  opened_goals, closed_goals
 type eval_ast =
  {ea_go:
@@ -475,24 +475,267 @@ let basic_eval_unification_hint (t,n) status =
 ;;
 
 let inject_unification_hint =
- let basic_eval_unification_hint (t,n) ~refresh_uri_in_term =
+ let basic_eval_unification_hint (t,n) 
+   ~refresh_uri_in_universe 
+   ~refresh_uri_in_term
+ =
   let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n)
  in
   NRstatus.Serializer.register "unification_hints" basic_eval_unification_hint
 ;;
 
 let eval_unification_hint status t n = 
- let estatus = GrafiteTypes.get_estatus status in
- let metasenv,subst,estatus,t =
-  GrafiteDisambiguate.disambiguate_nterm None estatus [] [] [] ("",0,t) in
+ let metasenv,subst,status,t =
+  GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,t) in
  assert (metasenv=[]);
  let t = NCicUntrusted.apply_subst subst [] t in
- let status = GrafiteTypes.set_estatus estatus status in
- let estatus =
-  basic_eval_unification_hint (t,n) (GrafiteTypes.get_estatus status) in
- let dump = inject_unification_hint (t,n)::estatus#dump in
- let estatus = estatus#set_dump dump in
- let status = GrafiteTypes.set_estatus estatus status in
+ 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 []
+;;
+
+let product f l1 l2 =
+  List.fold_left
+    (fun acc x ->
+      List.fold_left 
+        (fun acc y ->
+           f x y :: acc)
+        acc l2)
+    [] l1  
+;;
+
+let pos_in_list x l =
+      match 
+        HExtlib.list_findopt (fun y i -> if y = x then Some i else None) l
+      with
+      | Some i -> i
+      | None -> assert false
+;;
+
+let pos_of x t = 
+  match t with
+  | NCic.Appl l -> pos_in_list x l
+  | _ -> assert false
+;;
+
+let rec count_prod = function
+  | NCic.Prod (_,_,x) -> 1 + count_prod x
+  | _ -> 0
+;;
+
+let term_at i t =
+  match t with
+  | NCic.Appl l -> 
+      (match 
+        HExtlib.list_findopt (fun y j -> if i+1=j then Some y else None) l
+      with
+      | Some i -> i
+      | None -> assert false)
+  | _ -> assert false
+;;
+
+let src_tgt_of_ty_cpos_arity ty cpos arity =
+  let pis = count_prod ty in
+  let tpos = pis - arity in
+  let rec aux i j = function
+    | NCic.Prod (_,s,_) when i = j -> s
+    | NCic.Prod (_,_,t) -> aux (i+1) j t
+    | t -> assert (i = j); t
+  in
+  let mask t =
+    let rec aux () = function
+      | NCic.Meta _ 
+      | NCic.Implicit _ as x -> x
+      | NCic.Rel _ -> NCic.Implicit `Type
+      | t -> NCicUtils.map (fun _ () -> ()) () aux t
+    in
+     aux () t
+  in 
+  mask (aux 0 cpos ty), mask (aux 0 tpos ty)
+;;
+
+let close_in_context t metasenv = 
+  let rec aux m_subst subst ctx = function
+   | (i,(tag,[],ty)) :: tl ->
+        let name = "x" ^ string_of_int (List.length ctx) in
+        let subst = (i,(tag,[],NCic.Rel (List.length tl+1),ty))::subst in
+        let ty = NCicUntrusted.apply_subst (m_subst (List.length ctx)) ctx ty in
+        let m_subst m = 
+          (i,(tag,[],NCic.Rel (m-List.length ctx),ty))::(m_subst m)
+        in
+        NCic.Lambda (name, ty, aux m_subst subst ((name,NCic.Decl ty)::ctx) tl)
+   | [] -> NCicUntrusted.apply_subst subst ctx
+             (NCicSubstitution.lift (List.length ctx) t)
+   | _ -> assert false
+  in
+  aux (fun _ -> []) [] [] metasenv
+;;
+
+let toposort metasenv = 
+  let module T = HTopoSort.Make(
+    struct type t = int * NCic.conjecture let compare (i,_) (j,_) = i-j end) 
+  in
+  let deps (_,(_,_,t)) =
+    List.filter (fun (j,_) -> 
+      List.mem j (NCicUntrusted.metas_of_term [] [] t)) metasenv
+  in
+  T.topological_sort metasenv deps
+;;
+
+let basic_eval_ncoercion (name,t,s,d,p,a) status =
+  let to_s = 
+    NCicCoercion.look_for_coercion status [] [] [] (NCic.Implicit `Type) s
+  in
+  let from_d = 
+    NCicCoercion.look_for_coercion status [] [] [] d (NCic.Implicit `Type)
+  in
+  let status = NCicCoercion.index_coercion status t s d a p in
+  let c =
+    List.find 
+     (function (_,NCic.Appl (x::_),_,_) -> x = t | _ -> assert false) 
+      (NCicCoercion.look_for_coercion status [] [] [] s d)
+  in
+  let composites = 
+    let to_s_o_c = 
+      product (fun (m1,t1,_,j) (mc,c,_,i) -> m1@mc,c,[i,t1],j,a) 
+        to_s [c]
+    in
+    let c_o_from_d = 
+      product (fun (mc,c,_,j) (m1,t1,ty,i) -> m1@mc,t1,[i,c],j,count_prod ty) 
+        [c] from_d
+    in
+    let to_s_o_c_o_from_d =
+      product (fun (m1,t1,_,j) (m,t,upl,i,a)-> 
+       m@m1,t,(i,t1)::upl,j,a)
+       to_s c_o_from_d
+    in
+    to_s_o_c @ c_o_from_d @ to_s_o_c_o_from_d
+  in
+  let composites =
+    HExtlib.filter_map
+     (fun (metasenv, bo, upl, p, arity) ->
+        try
+         let metasenv, subst = 
+           List.fold_left 
+            (fun (metasenv,subst) (a,b) ->
+                NCicUnification.unify status metasenv subst [] a b)
+            (metasenv,[]) upl
+         in
+         let bo = NCicUntrusted.apply_subst subst [] bo in
+         let metasenv = toposort metasenv in
+         let bo = close_in_context bo metasenv in
+         let pos = 
+           match p with 
+           | NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv) 
+           | _ -> assert false
+         in
+         let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] bo in
+         let src,tgt = src_tgt_of_ty_cpos_arity ty pos arity in
+         prerr_endline (
+           NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] bo ^ " : " ^
+           NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty ^ " as " ^
+           NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
+           NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^
+           " cpos=" ^ string_of_int pos ^ " arity=" ^ string_of_int arity);
+         Some (bo,src,tgt,arity,pos)
+       with 
+       | NCicTypeChecker.TypeCheckerFailure _
+       | NCicUnification.UnificationFailure _ 
+       | NCicUnification.Uncertain _ -> None
+     ) composites
+  in
+  List.fold_left 
+    (fun st (t,s,d,a,p) -> NCicCoercion.index_coercion st t s d a p) 
+    status composites
+;;
+
+let inject_ncoercion =
+ let basic_eval_ncoercion x ~refresh_uri_in_universe ~refresh_uri_in_term =
+  basic_eval_ncoercion x
+ in
+  NRstatus.Serializer.register "ncoercion" basic_eval_ncoercion
+;;
+
+let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
+  let status, src, cpos = 
+    let rec aux cpos ctx = function
+      | NCic.Prod (name,ty,bo) ->
+         if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo
+         else
+           (try 
+            let metasenv,subst,status,src =
+              GrafiteDisambiguate.disambiguate_nterm 
+                None status ctx [] [] ("",0,src) in
+            let src = NCicUntrusted.apply_subst subst [] src in
+            (* CHECK that the declared pattern matches the abstraction *)
+            let _ = NCicUnification.unify status metasenv subst ctx ty src in
+            status, src, cpos
+           with 
+           | NCicUnification.UnificationFailure _
+           | NCicUnification.Uncertain _
+           | MultiPassDisambiguator.DisambiguationError _ ->
+               raise (GrafiteTypes.Command_error "bad source pattern"))
+      | _ -> assert false
+    in
+      aux 0 [] ty
+  in
+  let status, tgt, arity = 
+    let metasenv,subst,status,tgt =
+      GrafiteDisambiguate.disambiguate_nterm 
+        None status [] [] [] ("",0,tgt) in
+    let tgt = NCicUntrusted.apply_subst subst [] tgt in
+    (* CHECK che sia unificabile mancante *)
+    let rec count_prod = function
+      | NCic.Prod (_,_,x) -> 1 + count_prod x
+      | _ -> 0
+    in
+     status, tgt, count_prod tgt
+  in
+  status, src, tgt, cpos, arity
+;;
+
+let eval_ncoercion status name t ty (id,src) tgt = 
+
+ let metasenv,subst,status,ty =
+  GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,ty) in
+ assert (metasenv=[]);
+ let ty = NCicUntrusted.apply_subst subst [] ty in
+ let metasenv,subst,status,t =
+  GrafiteDisambiguate.disambiguate_nterm (Some ty) status [] [] [] ("",0,t) in
+ assert (metasenv=[]);
+ let t = NCicUntrusted.apply_subst subst [] t in
+
+ let status, src, tgt, cpos, arity = 
+   src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt
+ in
+
+ let status = basic_eval_ncoercion (name,t,src,tgt,cpos,arity) status in
+ let dump = inject_ncoercion (name,t,src,tgt,cpos,arity)::status#dump in
+ let status = status#set_dump dump in
+  status,`New []
+;;
+
+let basic_eval_add_constraint (s,u1,u2) status =
+ NCicLibrary.add_constraint status s u1 u2
+;;
+
+let inject_constraint =
+ let basic_eval_add_constraint (s,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)
+ 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 status = status#set_dump dump in
   status,`Old []
 ;;
 
@@ -508,7 +751,7 @@ let add_coercions_of_lemmas lemmas status =
       lemmas
   in
   let status = GrafiteTypes.add_moo_content moo_content status in 
-  {status with GrafiteTypes.coercions = CoercDb.dump () }, 
+   status#set_coercions (CoercDb.dump ()), 
   lemmas
 
 let eval_coercion status ~add_composites uri arity saturations =
@@ -520,7 +763,7 @@ let eval_coercion status ~add_composites uri arity saturations =
  let status, lemmas =
   GrafiteSync.add_coercion ~add_composites 
     ~pack_coercion_obj:CicRefine.pack_coercion_obj
-   status uri arity saturations (GrafiteTypes.get_baseuri status) in
+   status uri arity saturations status#baseuri in
  let moo_content = coercion_moo_statement_of (uri,arity,saturations,0) in
  let status = GrafiteTypes.add_moo_content [moo_content] status in 
   add_coercions_of_lemmas lemmas status
@@ -581,11 +824,11 @@ let non_punctuation_tactical_of_ast (text,prefix_len,punct) =
 let eval_tactical status tac =
   let status, _, _ = MatitaTacticals.eval tac (status, ~-1) in
   let status =  (* is proof completed? *)
-    match status.GrafiteTypes.proof_status with
+    match status#proof_status with
     | GrafiteTypes.Incomplete_proof
        { GrafiteTypes.stack = stack; proof = proof }
       when Continuationals.Stack.is_empty stack ->
-        { status with GrafiteTypes.proof_status = GrafiteTypes.Proof proof }
+       status#set_proof_status (GrafiteTypes.Proof proof)
     | _ -> status
   in
   status
@@ -603,7 +846,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) ->
@@ -655,100 +899,91 @@ 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 s =
-  let u,h,metasenv, subst,o = s.NTacStatus.istatus.NTacStatus.pstatus in
+let subst_metasenv_and_fix_names status =
+  let u,h,metasenv, subst,o = status#obj in
   let o = 
     NCicUntrusted.map_obj_kind ~skip_body:true 
      (NCicUntrusted.apply_subst subst []) o
   in
-  { s with NTacStatus.istatus =
-     { s.NTacStatus.istatus with NTacStatus.pstatus =
-        u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o}}
+   status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o)
 ;;
 
 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) ->
+      eval_ncoercion status name t ty source target
   | GrafiteAst.NQed loc ->
-      (match status.GrafiteTypes.ng_status with
-       | GrafiteTypes.ProofMode
-          { NTacStatus.istatus =
-             { NTacStatus.pstatus = pstatus; estatus = estatus } } ->
-            let uri,height,menv,subst,obj_kind = pstatus in
-             if menv <> [] then
-              raise
-               (GrafiteTypes.Command_error"You can't Qed an incomplete theorem")
-             else
-              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
-              (* fix the height inside the object *)
-              let rec fix () = function 
-                | NCic.Const (NReference.Ref (u,spec)) when NUri.eq u uri -> 
-                   NCic.Const (NReference.reference_of_spec u
-                    (match spec with
-                    | NReference.Def _ -> NReference.Def height
-                    | NReference.Fix (i,j,_) -> NReference.Fix(i,j,height)
-                    | NReference.CoFix _ -> NReference.CoFix height
-                    | NReference.Ind _ | NReference.Con _
-                    | NReference.Decl as s -> s))
-                | t -> NCicUtils.map (fun _ () -> ()) () fix t
-              in
-              let obj_kind = 
-                match obj_kind with
-                | NCic.Fixpoint _ -> 
-                    NCicUntrusted.map_obj_kind (fix ()) obj_kind 
-                | _ -> obj_kind
-              in
-              let obj = uri,height,[],[],obj_kind in
-               NCicTypeChecker.typecheck_obj obj;
-               let estatus = NCicLibrary.add_obj estatus uri obj in
-               let objs = NCicElim.mk_elims obj in
-               let timestamp,uris_rev =
-                 List.fold_left
-                  (fun (estatus,uris_rev) (uri,_,_,_,_) as obj ->
-                    NCicTypeChecker.typecheck_obj obj;
-                    let estatus = NCicLibrary.add_obj estatus uri obj in
-                     estatus,uri::uris_rev
-                  ) (estatus,[]) objs in
-               let uris = uri::List.rev uris_rev in
-                GrafiteTypes.set_estatus estatus
-                 {status with 
-                  GrafiteTypes.ng_status = 
-                   GrafiteTypes.CommandMode estatus },`New uris
-       | _ -> raise (GrafiteTypes.Command_error "Not in proof mode"))
+     if status#ng_mode <> `ProofMode then
+      raise (GrafiteTypes.Command_error "Not in proof mode")
+     else
+      let uri,height,menv,subst,obj_kind = status#obj in
+       if menv <> [] then
+        raise
+         (GrafiteTypes.Command_error"You can't Qed an incomplete theorem")
+       else
+        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
+        (* fix the height inside the object *)
+        let rec fix () = function 
+          | NCic.Const (NReference.Ref (u,spec)) when NUri.eq u uri -> 
+             NCic.Const (NReference.reference_of_spec u
+              (match spec with
+              | NReference.Def _ -> NReference.Def height
+              | NReference.Fix (i,j,_) -> NReference.Fix(i,j,height)
+              | NReference.CoFix _ -> NReference.CoFix height
+              | NReference.Ind _ | NReference.Con _
+              | NReference.Decl as s -> s))
+          | t -> NCicUtils.map (fun _ () -> ()) () fix t
+        in
+        let obj_kind = 
+          match obj_kind with
+          | NCic.Fixpoint _ -> 
+              NCicUntrusted.map_obj_kind (fix ()) obj_kind 
+          | _ -> 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
   | GrafiteAst.NObj (loc,obj) ->
-     let estatus =
-       match status.GrafiteTypes.ng_status with
-       | GrafiteTypes.ProofMode _ -> assert false
-       | GrafiteTypes.CommandMode es -> es 
-     in
-     let estatus,obj =
-      GrafiteDisambiguate.disambiguate_nobj estatus
-       ~baseuri:(GrafiteTypes.get_baseuri status) (text,prefix_len,obj) in
-     let uri,height,nmenv,nsubst,nobj = obj in
-     let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
-     let status =
-      { status with
-         GrafiteTypes.ng_status = 
-          GrafiteTypes.ProofMode
-           (subst_metasenv_and_fix_names
-            { NTacStatus.gstatus = ninitial_stack; 
-             istatus = { NTacStatus.pstatus = obj; estatus = estatus}})
-             }
-     in
-     (match nmenv with
-         [] ->
-          eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
-       | _ -> status,`New [])
+     if status#ng_mode <> `CommandMode then
+      raise (GrafiteTypes.Command_error "Not in command mode")
+     else
+      let status,obj =
+       GrafiteDisambiguate.disambiguate_nobj status
+        ~baseuri:status#baseuri (text,prefix_len,obj) in
+      let uri,height,nmenv,nsubst,nobj = obj in
+      let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
+      let status = status#set_obj obj in
+      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
+      (match nmenv with
+          [] ->
+           eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+        | _ -> status,`New [])
   | GrafiteAst.NUnivConstraint (loc,strict,u1,u2) ->
-      NCicEnvironment.add_constraint strict [false,u1] [false,u2];
-      status, `New [u1;u2]
+      eval_add_constraint status strict [false,u1] [false,u2]
 ;;
 
 let rec eval_command = {ec_go = fun ~disambiguate_command opts status
@@ -760,13 +995,13 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
 	assert false (* TODO: for user input *)
   | GrafiteAst.Index (loc,Some key,uri) -> 
       let universe = 
-        status.GrafiteTypes.automation_cache.AutomationCache.univ
+        status#automation_cache.AutomationCache.univ
       in
       let universe = Universe.index universe key (CicUtil.term_of_uri uri) in
       let cache = { 
-        status.GrafiteTypes.automation_cache with AutomationCache.univ = universe } 
+        status#automation_cache with AutomationCache.univ = universe } 
       in
-      let status = { status with GrafiteTypes.automation_cache = cache } in
+      let status = status#set_automation_cache cache in
 (* debug
       let msg =
        let candidates = Universe.get_candidates status.GrafiteTypes.universe key in
@@ -778,20 +1013,20 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       let status = GrafiteTypes.add_moo_content [cmd] status in
       status,`Old [] 
   | GrafiteAst.Select (_,uri) as cmd ->
-      if List.mem cmd status.GrafiteTypes.moo_content_rev then status, `Old []
+      if List.mem cmd status#moo_content_rev then status, `Old []
       else 
        let cache = 
-         AutomationCache.add_term_to_active status.GrafiteTypes.automation_cache
+         AutomationCache.add_term_to_active status#automation_cache
            [] [] [] (CicUtil.term_of_uri uri) None
        in
-       let status = { status with GrafiteTypes.automation_cache = cache } in
+       let status = status#set_automation_cache cache in
        let status = GrafiteTypes.add_moo_content [cmd] status in
        status, `Old []
   | GrafiteAst.Pump (_,steps) ->
       let cache = 
-        AutomationCache.pump status.GrafiteTypes.automation_cache steps
+        AutomationCache.pump status#automation_cache steps
       in
-      let status = { status with GrafiteTypes.automation_cache = cache } in
+      let status = status#set_automation_cache cache in
       status, `Old []
   | GrafiteAst.PreferCoercion (loc, coercion) ->
      eval_prefer_coercion status coercion
@@ -801,7 +1036,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
      in
       res,`Old uris
   | GrafiteAst.Inverter (loc, name, indty, params) ->
-     let buri = GrafiteTypes.get_baseuri status in 
+     let buri = status#baseuri in 
      let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") in
      let indty_uri = 
        try CicUtil.uri_of_term indty
@@ -815,39 +1050,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))
+  | GrafiteAst.Include (loc, mode, new_or_old, baseuri) ->
+     (* Old Include command is not recursive; new one is *)
+     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
      in
-     let status = eval_from_moo.efm_go status moopath in
-     let estatus = GrafiteTypes.get_estatus status in
-     let estatus =
+      let status =
        NRstatus.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
-        estatus in
-     let status = GrafiteTypes.set_estatus estatus status in
-(* debug
-     let lt_uri = UriManager.uri_of_string "cic:/matita/nat/orders/lt.con" in
-     let nat_uri = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind" in
-     let nat = Cic.MutInd(nat_uri,0,[]) in
-     let zero = Cic.MutConstruct(nat_uri,0,1,[]) in
-     let succ = Cic.MutConstruct(nat_uri,0,2,[]) in
-     let fake= Cic.Meta(-1,[]) in
-     let term= Cic.Appl [Cic.Const (lt_uri,[]);zero;Cic.Appl[succ;zero]] in     let msg =
-       let candidates = Universe.get_candidates status.GrafiteTypes.universe term in
-       ("candidates for " ^ (CicPp.ppterm term) ^ " = " ^ 
-	  (String.concat "\n" (List.map CicPp.ppterm candidates))) 
-     in
-     prerr_endline msg;
-*)
-     status,`Old []
+        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));
@@ -855,7 +1083,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
   | GrafiteAst.Print (_,_) -> status,`Old []
   | GrafiteAst.Qed loc ->
       let uri, metasenv, _subst, bo, ty, attrs =
-        match status.GrafiteTypes.proof_status with
+        match status#proof_status with
         | GrafiteTypes.Proof (Some uri, metasenv, subst, body, ty, attrs) ->
             uri, metasenv, subst, body, ty, attrs
         | GrafiteTypes.Proof (None, metasenv, subst, body, ty, attrs) -> 
@@ -873,7 +1101,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       let name = UriManager.name_of_uri uri in
       let obj = Cic.Constant (name,Some (Lazy.force bo),ty,[],attrs) in
       let status, lemmas = add_obj uri obj status in
-       {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
+       status#set_proof_status GrafiteTypes.No_proof,
         (*CSC: I throw away the arities *)
         `Old (uri::lemmas)
   | GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) -> 
@@ -890,7 +1118,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
           ".ind",
           (match types with (name,_,_,_)::_ -> name | _ -> assert false)
        | _ -> assert false in
-     let buri = GrafiteTypes.get_baseuri status in 
+     let buri = status#baseuri in 
      let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ext) in
      let obj = CicRefine.pack_coercion_obj obj in
      let metasenv = GrafiteTypes.get_proof_metasenv status in
@@ -930,10 +1158,9 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
          let _subst = [] in
          let initial_proof = (Some uri, metasenv', _subst, lazy bo, ty, attrs) in
          let initial_stack = Continuationals.Stack.of_metasenv metasenv' in
-         { status with GrafiteTypes.proof_status =
-            GrafiteTypes.Incomplete_proof
-            { GrafiteTypes.proof = initial_proof; stack = initial_stack } ;
-         },
+          status#set_proof_status
+           (GrafiteTypes.Incomplete_proof
+            { GrafiteTypes.proof = initial_proof; stack = initial_stack }),
           `Old []
      | _ ->
          if metasenv <> [] then
@@ -942,12 +1169,12 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
             CicMetaSubst.ppmetasenv [] metasenv));
          let status, lemmas = add_obj uri obj status in 
          let status,new_lemmas = add_coercions_of_lemmas lemmas status in
-          {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
+          status#set_proof_status GrafiteTypes.No_proof,
            `Old (uri::new_lemmas@lemmas)
  in
-  match status.GrafiteTypes.proof_status with
+  match status#proof_status with
      GrafiteTypes.Intermediate _ ->
-      {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},uris
+      status#set_proof_status GrafiteTypes.No_proof,uris
    | _ -> status,uris
 
 } and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command
@@ -971,19 +1198,17 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       eval_tactical status
        (punctuation_tactical_of_ast (text,prefix_len,punct)),`Old []
   | GrafiteAst.NTactic (_(*loc*), tacl) ->
-      (match status.GrafiteTypes.ng_status with
-      | GrafiteTypes.CommandMode _ -> assert false
-      | GrafiteTypes.ProofMode nstatus ->
-         let nstatus =
-          List.fold_left 
-            (fun nstatus tac ->
-              let nstatus = eval_ng_tac (text,prefix_len,tac) nstatus in
-              subst_metasenv_and_fix_names nstatus)
-            nstatus tacl
-         in
-         NTacStatus.pp_tac_status nstatus;
-         { status with GrafiteTypes.ng_status= GrafiteTypes.ProofMode nstatus },
-         `New [])
+      if status#ng_mode <> `ProofMode then
+       raise (GrafiteTypes.Command_error "Not in proof mode")
+      else
+       let status =
+        List.fold_left 
+          (fun status tac ->
+            let status = eval_ng_tac (text,prefix_len,tac) status in
+            subst_metasenv_and_fix_names status)
+          status tacl
+       in
+        status,`New []
   | GrafiteAst.NonPunctuationTactical (_, tac, punct) ->
      let status = 
       eval_tactical status