New datatype for metasenv/subst: full fledged attributes in place of optional

[helm.git] / helm / software / components / ng_tactics / nTacStatus.ml

diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index 0bb0d846e9fedc5c3b9bc2a7da01f8b3701e66c5..83b97d4082fe6e9d895d098514b97720773efc85 100644 (file)
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -40,7 +40,7 @@ let pp_status status =
   prerr_endline (NCicPp.ppobj status#obj)
 ;;
 
-type cic_term = NCic.conjecture (* name, context, term *)
+type cic_term = NCic.conjecture (* attrs, context, term *)
 let ctx_of (_,c,_) = c ;;
 
 let relocate status destination (name,source,t as orig) =
@@ -117,7 +117,7 @@ let disambiguate status t ty context =
    GrafiteDisambiguate.disambiguate_nterm expty status context metasenv subst t 
  in
  let new_pstatus = uri,height,metasenv,subst,obj in
-  status#set_obj new_pstatus, (None, context, t) 
+  status#set_obj new_pstatus, ([], context, t) 
 ;;
 let disambiguate a b c d = wrap (disambiguate a b c) d;;
 
@@ -125,7 +125,7 @@ let typeof status ctx t =
   let status, (_,_,t) = relocate status ctx t in
   let _,_,metasenv,subst,_ = status#obj in
   let ty = NCicTypeChecker.typeof ~subst ~metasenv ctx t in
-  status, (None, ctx, ty)
+  status, ([], ctx, ty)
 ;;
 let typeof a b c = wrap (typeof a b) c;;
   
@@ -163,7 +163,8 @@ let fix_sorts (name,ctx,t) =
 let refine status ctx term expty =
   let status, (nt,_,term) = relocate status ctx term in
   let status, ne, expty = 
-    match expty with None -> status, None, None 
+    match expty with
+      None -> status, [], None 
     | Some e -> 
         let status, (n,_, e) = relocate status ctx e in status, n, Some e
   in
@@ -192,34 +193,34 @@ let instantiate status i t =
   status#set_obj (name,height,metasenv,subst,obj)
 ;;
 
-let mk_meta status ?name ctx bo_or_ty =
+let mk_meta status ?(attrs=[]) ctx bo_or_ty =
   match bo_or_ty with
   | `Decl ty ->
       let status, (_,_,ty) = relocate status ctx ty in
       let n,h,metasenv,subst,o = status#obj in
       let metasenv, _, instance, _ = 
-        NCicMetaSubst.mk_meta ?name metasenv ctx (`WithType ty)
+        NCicMetaSubst.mk_meta ~attrs metasenv ctx (`WithType ty)
       in
       let status = status#set_obj (n,h,metasenv,subst,o) in
-      status, (None,ctx,instance)
+      status, ([],ctx,instance)
   | `Def bo ->
       let status, (_,_,bo_ as bo) = relocate status ctx bo in
       let status, (_,_,ty) = typeof status ctx bo in
       let n,h,metasenv,subst,o = status#obj in
       let metasenv, metano, instance, _ = 
-        NCicMetaSubst.mk_meta ?name metasenv ctx (`WithType ty) in
+        NCicMetaSubst.mk_meta ~attrs metasenv ctx (`WithType ty) in
       let metasenv = List.filter (fun j,_ -> j <> metano) metasenv in
-      let subst = (metano, (name, ctx, bo_, ty)) :: subst in
+      let subst = (metano, (attrs, ctx, bo_, ty)) :: subst in
       let status = status#set_obj (n,h,metasenv,subst,o) in
-      status, (None,ctx,instance)
+      status, ([],ctx,instance)
 ;;
 
-let mk_in_scope status t = 
-  mk_meta status ~name:NCicMetaSubst.in_scope_tag (ctx_of t) (`Def t)
+let mk_in_scope status t =
+  mk_meta status ~attrs:[`InScope] (ctx_of t) (`Def t)
 ;;
 
 let mk_out_scope n status t = 
-  mk_meta status ~name:(NCicMetaSubst.out_scope_tag n) (ctx_of t) (`Def t)
+  mk_meta status ~attrs:[`OutScope n] (ctx_of t) (`Def t)
 ;;
 
 (* the following unification problem will be driven by 
@@ -237,7 +238,7 @@ let select_term
 =
   let is_found status ctx t wanted =
     (* we could lift wanted step-by-step *)
-    try true, unify status ctx (None, ctx, t) wanted
+    try true, unify status ctx ([], ctx, t) wanted
     with 
     | Error (_, Some (NCicUnification.UnificationFailure _))
     | Error (_, Some (NCicUnification.Uncertain _)) -> false, status
@@ -246,7 +247,7 @@ let select_term
     let rec aux ctx (status,already_found) t =
       let b, status = is_found status ctx t wanted in
       if b then
-         let status , (_,_,t) = found status (None, ctx, t) in 
+         let status , (_,_,t) = found status ([], ctx, t) in 
          (status,true),t
       else
         let _,_,_,subst,_ = status#obj in
@@ -313,7 +314,7 @@ let select_term
              let (status',found), t' = match_term status' ctx wanted t in
               if found then status',t' else status,t
         | None ->
-           let (status,_),t = match_term status ctx (None,ctx,t) t in
+           let (status,_),t = match_term status ctx ([],ctx,t) t in
             status,t)
     | NCic.Implicit _, t -> status, t
     | _,t -> 
@@ -340,7 +341,7 @@ let analyse_indty status ty =
  status, (ref, consno, left, right)
 ;;
 
-let mk_cic_term c t = None,c,t ;;
+let mk_cic_term c t = [],c,t ;;
 
 let apply_subst status ctx t =
  let status, (name,_,t) = relocate status ctx t in