Porting to ocaml 5

[helm.git] / matita / components / ng_cic_content / interpretations.ml

diff --git a/matita/components/ng_cic_content/interpretations.ml b/matita/components/ng_cic_content/interpretations.ml
index 84638ad6dfa43e03cf473ff0e8d56b3d3b44a38c..44d7751d500d74232d482a0e5117ddce72a6d066 100644 (file)
--- a/matita/components/ng_cic_content/interpretations.ml
+++ b/matita/components/ng_cic_content/interpretations.ml
@@ -38,10 +38,12 @@ let hide_coercions = ref true;;
 
 type cic_id = string
 
+(*
 type term_info =
   { sort: (cic_id, Ast.sort_kind) Hashtbl.t;
     uri: (cic_id, NReference.reference) Hashtbl.t;
   }
+*)
 
 module IntMap = Map.Make(struct type t = int let compare = compare end);;
 module StringMap = Map.Make(String);;
@@ -107,7 +109,7 @@ let add_idrefs =
   List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
 
 let instantiate32 idrefs env symbol args =
-  let rec instantiate_arg = function
+  let instantiate_arg = function
     | Ast.IdentArg (n, name) ->
         let t = 
           try List.assoc name env 
@@ -185,7 +187,7 @@ let lookup_interpretations status ?(sorted=true) symbol =
           dsc, args, appl_pattern
       ) (StringMap.find symbol status#interp_db.interpretations)
     in
-    if sorted then HExtlib.list_uniq (List.sort Pervasives.compare raw)
+    if sorted then HExtlib.list_uniq (List.sort Stdlib.compare raw)
               else raw
   with Not_found -> raise Interpretation_not_found
 
@@ -267,7 +269,7 @@ let nast_of_cic0 status
     | NCic.Lambda (n,s,t) ->
         idref (Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k ~context s)),
          k ~context:((n,NCic.Decl s)::context) t))
-    | NCic.LetIn (n,s,ty,NCic.Rel 1) ->
+    | NCic.LetIn (_n,s,ty,NCic.Rel 1) ->
         idref (Ast.Cast (k ~context ty, k ~context s))
     | NCic.LetIn (n,s,ty,t) ->
         idref (Ast.LetIn ((Ast.Ident (n,None), Some (k ~context s)), k ~context
@@ -305,6 +307,7 @@ let nast_of_cic0 status
                  [arg] -> idref (k ~context arg)
                | _ -> idref (Ast.Appl (List.map (k ~context) args))))
     | NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) ->
+       (try
         let name = NUri.name_of_uri uri in
 (* CSC
         let uri_str = UriManager.string_of_uri uri in
@@ -323,7 +326,7 @@ let nast_of_cic0 status
         in
        let rec eat_branch n ctx ty pat =
           match (ty, pat) with
-         | NCic.Prod (name, s, t), _ when n > 0 ->
+         | NCic.Prod (_name, _s, t), _ when n > 0 ->
              eat_branch (pred n) ctx t pat 
           | NCic.Prod (_, _, t), NCic.Lambda (name, s, t') ->
               let cv, rhs = eat_branch 0 ((name,NCic.Decl s)::ctx) t t' in
@@ -351,6 +354,12 @@ let nast_of_cic0 status
           | `Term -> Some case_indty
         in
          idref (Ast.Case (k ~context te, indty, Some (k ~context outty), patterns))
+     with
+      NCicEnvironment.ObjectNotFound msg ->
+       idref (Ast.Case(k ~context te,Some ("NOT_FOUND: " ^ Lazy.force msg,None),
+       Some (k ~context outty),
+       (List.map (fun t -> Ast.Pattern ("????", None, []), k ~context t)
+         patterns))))
 ;;
 
 let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term =
@@ -424,7 +433,7 @@ let nmap_context0 status ~idref ~metasenv ~subst context =
    ) context ([],[]))
 ;;
 
-let nmap_sequent0 status ~idref ~metasenv ~subst (i,(n,context,ty)) =
+let nmap_sequent0 status ~idref ~metasenv ~subst (i,(_n,context,ty)) =
  let module K = Content in
  let nast_of_cic =
   nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst in
@@ -450,7 +459,7 @@ let gen_id prefix seed =
   res
 ;;
 
-let build_def_item seed context metasenv id n t ty =
+let build_def_item seed _context _metasenv id n t ty =
  let module K = Content in
 (*
   try
@@ -536,7 +545,7 @@ let build_inductive b seed =
             K.inductive_constructors = build_constructors seed cl
            }
 in
-let build_fixpoint b seed = 
+let build_fixpoint _b seed = 
       fun (_,n,_,ty,t) ->
         let t = nast_of_cic ~context:[] t in
         let ty = nast_of_cic ~context:[] ty in
@@ -632,16 +641,16 @@ let nmap_obj0 status ~idref (_, _, metasenv, subst, kind) =
       n, is_ind, ty, List.map (build_constractor lno context) cl
    in
    match kind with
-      | NCic.Constant (_, n, xbo, ty, (_, flavour, pragma)) ->
+      | NCic.Constant (_, n, xbo, ty, attrs) ->
         let ty = nast_of_cic ~context:[] ty in
          let xbo = match xbo with 
            | Some bo -> Some (nast_of_cic ~context:[] bo)
            | None    -> None
         in
-        N.Theorem (flavour, n, ty, xbo, pragma)
-      | NCic.Inductive (is_ind, lno, itl, (_, `Regular)) ->      
+        N.Theorem (n, ty, xbo, attrs)
+      | NCic.Inductive (is_ind, lno, itl, (src, `Regular)) ->      
          let captures, context = build_captures lno itl in
-        N.Inductive (captures, List.map (build_inductive is_ind lno context) itl)
+        N.Inductive (captures, List.map (build_inductive is_ind lno context) itl, src)
       | _ -> assert false  (* NCic.Fixpoint (is_rec, ifl, _) -> *)
 
 let nmap_obj status = with_idrefs nmap_obj0 status