- no longer build mathql per default

[helm.git] / helm / ocaml / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 2a7f8c4ae16ed82a9c7800df1345577cae5756fb..6789c4dff8213acdf53d18aef9b286c0bd46744f 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -42,7 +42,7 @@ let debug t context =
    raise (TypeCheckerFailure (List.fold_right debug_aux (t::context) ""))
 ;;
 
-let debug_print = prerr_endline ;;
+let debug_print = fun _ -> () ;;
 
 let rec split l n =
  match (l,n) with
@@ -184,7 +184,7 @@ let rec type_of_constant ~logger uri ugraph =
                CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
              | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
         with Invalid_argument s ->
-          (*prerr_endline s;*)
+          (*debug_print s;*)
           uobj,ugraph_dust       
   in
    match cobj,ugraph with
@@ -225,7 +225,7 @@ and type_of_variable ~logger uri ugraph =
             | CicEnvironment.CheckedObj _ 
              | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
          with Invalid_argument s ->
-           (*prerr_endline s;*)
+           (*debug_print s;*)
            ty,ugraph2)
    |  _ ->
        raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri))
@@ -574,7 +574,7 @@ and type_of_mutual_inductive_defs ~logger uri i ugraph =
             )
           with
               Invalid_argument s ->
-                (*prerr_endline s;*)
+                (*debug_print s;*)
                 uobj,ugraph1_dust
   in
     match cobj with
@@ -609,7 +609,7 @@ and type_of_mutual_inductive_constr ~logger uri i j ugraph =
                       raise CicEnvironmentError)
            with
                Invalid_argument s ->
-                 (*prerr_endline s;*)
+                 (*debug_print s;*)
                  uobj,ugraph1_dust
   in
     match cobj with
@@ -903,7 +903,7 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
        (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
        exp_named_subst true
    | C.MutCase (uri,i,outtype,term,pl) ->
-      (match term with
+      (match CicReduction.whd context term with
           C.Rel m when List.mem m safes || m = x ->
            let (tys,len,isinductive,paramsno,cl) =
            let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
@@ -1395,12 +1395,12 @@ and check_metasenv_consistency ~logger ?(subst=[]) metasenv context
      function
          [] -> []
        | (Some (n,C.Decl t))::tl ->
-           (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+           (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
        | (Some (n,C.Def (t,None)))::tl ->
-           (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
+           (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
        | None::tl -> None::(aux (i+1) tl)
        | (Some (n,C.Def (t,Some ty)))::tl ->
-           (Some (n,C.Def ((S.lift_meta l (S.lift i t)),Some (S.lift_meta l (S.lift i ty)))))::(aux (i+1) tl)
+           (Some (n,C.Def ((S.subst_meta l (S.lift i t)),Some (S.subst_meta l (S.lift i ty)))))::(aux (i+1) tl)
     in
      aux 1 canonical_context
    in
@@ -1482,15 +1482,15 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
              ~subst metasenv context canonical_context l ugraph
          in
             (* assuming subst is well typed !!!!! *)
-            ((CicSubstitution.lift_meta l ty), ugraph1)
-              (* type_of_aux context (CicSubstitution.lift_meta l term) *)
+            ((CicSubstitution.subst_meta l ty), ugraph1)
+              (* type_of_aux context (CicSubstitution.subst_meta l term) *)
        with CicUtil.Subst_not_found _ ->
          let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
           let ugraph1 = 
            check_metasenv_consistency ~logger
              ~subst metasenv context canonical_context l ugraph
          in
-            ((CicSubstitution.lift_meta l ty),ugraph1))
+            ((CicSubstitution.subst_meta l ty),ugraph1))
       (* TASSI: CONSTRAINTS *)
     | C.Sort (C.Type t) -> 
        let t' = CicUniv.fresh() in
@@ -1680,8 +1680,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
               else raise 
                (TypeCheckerFailure 
                   (sprintf
-                     ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}")
-                     (CicPp.ppterm typ) (U.string_of_uri uri) i))
+                     ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
+                     (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))
           | C.Appl 
              ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
               if U.eq uri uri' && i = i' then
@@ -1691,8 +1691,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
               else raise 
                (TypeCheckerFailure 
                   (sprintf
-                     "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}"
-                     (CicPp.ppterm typ') (U.string_of_uri uri) i))
+                     ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
+                     (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))
           | _ ->
               raise 
                (TypeCheckerFailure 
@@ -1766,12 +1766,14 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
           if not branches_ok then
            raise
             (TypeCheckerFailure "Case analysys: wrong branch type");
-          if not need_dummy then
-            (C.Appl ((outtype::arguments)@[term])),ugraph5
-          else if arguments = [] then
-            outtype,ugraph5
-          else
-            (C.Appl (outtype::arguments)),ugraph5
+          let arguments =
+           if not need_dummy then outtype::arguments@[term]
+           else outtype::arguments in
+          let outtype =
+           if arguments = [] then outtype
+           else CicReduction.head_beta_reduce (C.Appl arguments)
+          in
+           outtype,ugraph5
    | C.Fix (i,fl) ->
       let types_times_kl,ugraph1 =
        (* WAS: list rev list map *)
@@ -2037,12 +2039,12 @@ let typecheck uri ugraph =
    (* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *)
    match CicEnvironment.is_type_checked ~trust:false ugraph uri with
      CicEnvironment.CheckedObj (cobj,ugraph') -> 
-       (* prerr_endline ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*)
+       (* debug_print ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*)
        cobj,ugraph'
    | CicEnvironment.UncheckedObj uobj ->
       (* let's typecheck the uncooked object *)
       logger#log (`Start_type_checking uri) ;
-      (* prerr_endline ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *)
+      (* debug_print ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *)
       let ugraph1 = 
        (match uobj with
          C.Constant (_,Some te,ty,_,_) ->
@@ -2111,15 +2113,15 @@ let typecheck uri ugraph =
              object.
            *)
            Invalid_argument s -> 
-             (*prerr_endline s;*)
+             (*debug_print s;*)
              uobj,ugraph1
 ;;
 
 (** wrappers which instantiate fresh loggers *)
 
-let type_of_aux' ?(subst = []) metasenv context t =
+let type_of_aux' ?(subst = []) metasenv context t ugraph =
   let logger = new CicLogger.logger in
-  type_of_aux' ~logger ~subst metasenv context t
+  type_of_aux' ~logger ~subst metasenv context t ugraph
 
 let typecheck_mutual_inductive_defs uri (itl, uris, indparamsno) =
   let logger = new CicLogger.logger in