X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnTacStatus.ml;h=31260d5ed837ea595caa9bf49944b60567edbb0a;hb=bbf85ddcdfe0809fee0c6ca9812ce0da30c238af;hp=99c35d7ff2e8505fb8946342e18ba86a8c2d7fc8;hpb=3a3517f9a23d9344ff6461e76e1c6c429d44db57;p=helm.git

diff --git a/matita/components/ng_tactics/nTacStatus.ml b/matita/components/ng_tactics/nTacStatus.ml
index 99c35d7ff..31260d5ed 100644
--- a/matita/components/ng_tactics/nTacStatus.ml
+++ b/matita/components/ng_tactics/nTacStatus.ml
@@ -29,9 +29,12 @@ let wrap fname f x =
   with 
   | MultiPassDisambiguator.DisambiguationError _ 
   | NCicRefiner.RefineFailure _ 
+  | NCicRefiner.Uncertain _ 
   | NCicUnification.UnificationFailure _ 
+  | NCicUnification.Uncertain _ 
   | NCicTypeChecker.TypeCheckerFailure _ 
-  | NCicMetaSubst.MetaSubstFailure _ as exn -> fail ~exn (lazy fname)
+  | NCicMetaSubst.MetaSubstFailure _
+  | NCicMetaSubst.Uncertain _ as exn -> fail ~exn (lazy fname)
 ;;
 
 class type g_eq_status =
@@ -45,7 +48,7 @@ class eq_status =
   method eq_cache = eq_cache
   method set_eq_cache v = {< eq_cache = v >}
   method set_eq_status
-   : 'status. #g_eq_status as 'status -> 'self
+   : 'status. (#g_eq_status as 'status) -> 'self
    = fun o -> self#set_eq_cache o#eq_cache
  end
 
@@ -60,7 +63,7 @@ class auto_status =
   method auto_cache = auto_cache
   method set_auto_cache v = {< auto_cache = v >}
   method set_auto_status
-   : 'status. #g_auto_status as 'status -> 'self
+   : 'status. (#g_auto_status as 'status) -> 'self
    = fun o -> self#set_auto_cache o#auto_cache
  end
 
@@ -81,7 +84,7 @@ class virtual pstatus =
    val obj = o
    method obj = obj
    method set_obj o = {< obj = o >}
-   method set_pstatus : 'status. #g_pstatus as 'status -> 'self
+   method set_pstatus : 'status. (#g_pstatus as 'status) -> 'self
    = fun o ->
     (((self#set_disambiguate_status o)#set_obj o#obj)#set_auto_status o)#set_eq_status o
   end
@@ -94,24 +97,24 @@ let ctx_of (c,_) = c ;;
 let mk_cic_term c t = c,t ;;
 
 let ppterm (status:#pstatus) t =
- let uri,height,metasenv,subst,obj = status#obj in
+ let _uri,_height,metasenv,subst,_obj = status#obj in
  let context,t = t in
   status#ppterm ~metasenv ~subst ~context t
 ;;
 
 let ppcontext (status: #pstatus) c =
- let uri,height,metasenv,subst,obj = status#obj in
+ let _uri,_height,metasenv,subst,_obj = status#obj in
   status#ppcontext ~metasenv ~subst c
 ;;
 
 let ppterm_and_context (status: #pstatus) t =
- let uri,height,metasenv,subst,obj = status#obj in
+ let _uri,_height,metasenv,subst,_obj = status#obj in
  let context,t = t in
   status#ppcontext ~metasenv ~subst context ^ "\n ⊢ "^ 
   status#ppterm ~metasenv ~subst ~context t
 ;;
 
-let relocate status destination (source,t as orig) =
+let relocate status destination (source,_t as orig) =
  pp(lazy("relocate:\n" ^ ppterm_and_context status orig));
  pp(lazy("relocate in:\n" ^ ppcontext status destination));
  let rc = 
@@ -131,13 +134,13 @@ let relocate status destination (source,t as orig) =
             compute_ops (e::ctx) (cl1,cl2)
           else
             [ `Delift ctx; `Lift (List.rev ex) ]
-      | (n1, NCic.Def (b1,t1) as e)::cl1 as ex, (n2, NCic.Decl t2)::cl2 ->
+      | (n1, NCic.Def (_b1,t1) as e)::cl1 as ex, (n2, NCic.Decl t2)::cl2 ->
           if n1 = n2 && 
              NCicReduction.are_convertible status ctx ~subst ~metasenv t1 t2 then
             compute_ops (e::ctx) (cl1,cl2)
           else
             [ `Delift ctx; `Lift (List.rev ex) ]
-      | (n1, NCic.Decl _)::cl1 as ex, (n2, NCic.Def _)::cl2 -> 
+      | (_n1, NCic.Decl _)::_cl1 as ex, (_n2, NCic.Def _)::_cl2 -> 
             [ `Delift ctx; `Lift (List.rev ex) ]
       | _::_ as ex, [] -> [ `Lift (List.rev ex) ]
       | [], _::_ -> [ `Delift ctx ]
@@ -184,9 +187,11 @@ let term_of_cic_term s t c =
 let disambiguate status context t ty =
  let status, expty = 
    match ty with 
-   | None -> status, None 
-   | Some ty -> 
-       let status, (_,x) = relocate status context ty in status, Some x 
+   | `XTSome ty -> 
+       let status, (_,x) = relocate status context ty in status, `XTSome x 
+   | `XTNone -> status, `XTNone 
+   | `XTSort -> status, `XTSort
+   | `XTInd  -> status, `XTInd
  in
  let uri,height,metasenv,subst,obj = status#obj in
  let metasenv, subst, status, t = 
@@ -227,6 +232,15 @@ let normalize status ?delta ctx t =
   status, (ctx, t)
 ;;
   
+let are_convertible status ctx a b =
+  let status, (_,a) = relocate status ctx a in
+  let status, (_,b) = relocate status ctx b in
+  let _n,_h,metasenv,subst,_o = status#obj in
+  let res = NCicReduction.are_convertible status metasenv subst ctx a b in
+   status, res
+;;
+let are_convertible a b c d = wrap "are_convertible" (are_convertible a b c) d;;
+
 let unify status ctx a b =
   let status, (_,a) = relocate status ctx a in
   let status, (_,b) = relocate status ctx b in
@@ -251,9 +265,11 @@ let refine status ctx term expty =
   let status, (_,term) = relocate status ctx term in
   let status, expty = 
     match expty with
-      None -> status, None 
-    | Some e -> 
-        let status, (_, e) = relocate status ctx e in status, Some e
+    | `XTSome e -> 
+        let status, (_, e) = relocate status ctx e in status, `XTSome e
+    | `XTNone -> status, `XTNone 
+    | `XTSort -> status, `XTSort
+    | `XTInd  -> status, `XTInd
   in
   let name,height,metasenv,subst,obj = status#obj in
   let metasenv,subst,t,ty = 
@@ -277,7 +293,7 @@ let get_subst status =
 
 let to_subst status i entry =
  let name,height,metasenv,subst,obj = status#obj in
- let metasenv = List.filter (fun j,_ -> j <> i) metasenv in
+ let metasenv = List.filter (fun (j,_) -> j <> i) metasenv in
  let subst = (i, entry) :: subst in
   status#set_obj (name,height,metasenv,subst,obj)
 ;;
@@ -286,7 +302,7 @@ let instantiate status ?refine:(dorefine=true) i t =
  let _,_,metasenv,_,_ = status#obj in
  let gname, context, gty = List.assoc i metasenv in
   if dorefine then
-   let status, (_,t), (_,ty) = refine status context t (Some (context,gty)) in
+   let status, (_,t), (_,ty) = refine status context t (`XTSome (context,gty)) in
     to_subst status i (gname,context,t,ty)
   else
    let status,(_,ty) = typeof status context t in
@@ -297,7 +313,7 @@ let instantiate_with_ast status i t =
  let _,_,metasenv,_,_ = status#obj in
  let gname, context, gty = List.assoc i metasenv in
  let ggty = mk_cic_term context gty in
- let status, (_,t) = disambiguate status context t (Some ggty) in
+ let status, (_,t) = disambiguate status context t (`XTSome ggty) in
   to_subst status i (gname,context,t,gty)
 ;;
 
@@ -318,7 +334,7 @@ let mk_meta status ?(attrs=[]) ctx bo_or_ty kind =
       let metasenv, metano, instance, _ = 
         NCicMetaSubst.mk_meta ~attrs metasenv ctx ~with_type:ty kind in
       let attrs,_,_ = NCicUtils.lookup_meta metano metasenv in
-      let metasenv = List.filter (fun j,_ -> j <> metano) metasenv in
+      let metasenv = List.filter (fun (j,_) -> j <> metano) metasenv in
       let subst = (metano, (attrs, ctx, bo_, ty)) :: subst in
       let status = status#set_obj (n,h,metasenv,subst,o) in
       status, (ctx,instance)
@@ -362,7 +378,7 @@ let select_term
       else
         let _,_,_,subst,_ = status#obj in
         match t with
-        | NCic.Meta (i,lc) when List.mem_assoc i subst ->
+        | NCic.Meta (i,_lc) when List.mem_assoc i subst ->
             let _,_,t,_ = NCicUtils.lookup_subst i subst in
             aux ctx (status,already_found) t
         | NCic.Meta _ -> (status,already_found),t
@@ -421,7 +437,7 @@ let select_term
     | NCic.Implicit `Hole, t -> 
         (match wanted with
         | Some wanted -> 
-             let status', wanted = disambiguate status ctx wanted None in
+             let status', wanted = disambiguate status ctx wanted `XTNone in
              pp(lazy("wanted: "^ppterm status' wanted));
              let (status',found), t' = match_term status' ctx wanted t in
               if found then status',t' else status,t
@@ -453,7 +469,7 @@ let analyse_indty status ty =
  let _,_,_,cl = List.nth tl i in
  let consno = List.length cl in
  let left, right = HExtlib.split_nth lno args in
- status, (ref, consno, left, right)
+ status, (ref, consno, left, right, cl)
 ;;
 
 let apply_subst status ctx t =
@@ -487,17 +503,17 @@ class virtual ['stack] status =
    val stack = s
    method stack = stack
    method set_stack s = {< stack = s >}
-   method set_status : 'status. 'stack #g_status as 'status -> 'self
+   method set_status : 'status. ('stack #g_status as 'status) -> 'self
    = fun o -> (self#set_pstatus o)#set_stack o#stack
   end
 
 class type virtual lowtac_status = [unit] status
 
-type 'status lowtactic = #lowtac_status as 'status -> int -> 'status
+type 'status lowtactic = (#lowtac_status as 'status) -> int -> 'status
 
 class type virtual tac_status = [Continuationals.Stack.t] status
 
-type 'status tactic = #tac_status as 'status -> 'status
+type 'status tactic = (#tac_status as 'status) -> 'status
 
 let pp_tac_status (status: #tac_status) = 
   prerr_endline (status#ppobj status#obj);
@@ -552,8 +568,8 @@ let compare e1 e2 =
   match e1,e2 with
   | Constant (u1,a1),Constant (u2,a2) -> 
        let x = NUri.compare u1 u2 in
-       if x = 0 then Pervasives.compare a1 a2 else x
-  | e1,e2 -> Pervasives.compare e1 e2
+       if x = 0 then Stdlib.compare a1 a2 else x
+  | e1,e2 -> Stdlib.compare e1 e2
 ;;
 
 
@@ -562,7 +578,7 @@ end
 module Ncic_termOT : Set.OrderedType with type t = cic_term =
  struct
    type t = cic_term
-   let compare = Pervasives.compare
+   let compare = Stdlib.compare
  end
 
 module Ncic_termSet : Set.S with type elt = cic_term = Set.Make(Ncic_termOT)