a few missing ~subst added to whd

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index 4092e7ae035250f11a43f1151d0ea8263a057da5..7f9ab1b6e2cdaeec66445d02617a4dbad71b8bcb 100644 (file)
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -187,7 +187,7 @@ let interpretate_term
            List.nth itl indtyp_no
           with _ -> assert false in
          let rec count_prod t =
-           match NCicReduction.whd [] t with
+                 match NCicReduction.whd ~subst:[] [] t with
                NCic.Prod (_, _, t) -> 1 + (count_prod t)
              | _ -> 0 
          in 

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index a7dfc50fad582819e0a62a2d97c076e8b51d9db9..7dbe379e4144f77801abfd6631cfdeaec547391d 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -165,7 +165,7 @@ module Reduction(RS : Strategy) = struct
     aux
   ;;
 
-  let whd ?(delta=0) ?(subst=[]) context t = 
+  let whd ?(delta=0) ~subst context t = 
    unwind (fst (reduce ~delta ~subst context (0, [], t, [])))
   ;;
 

diff --git a/helm/software/components/ng_kernel/nCicReduction.mli b/helm/software/components/ng_kernel/nCicReduction.mli
index 696723bf6ad158b4bab916b2c5c9c72a4e7505c5..006dba9d4ed7b88615e6bc3a417d977791fc7bf8 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.mli
+++ b/helm/software/components/ng_kernel/nCicReduction.mli
@@ -12,7 +12,7 @@
 (* $Id$ *)
 
 val whd : 
-  ?delta:int -> ?subst:NCic.substitution -> 
+  ?delta:int -> subst:NCic.substitution -> 
   NCic.context -> NCic.term -> 
     NCic.term
 

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index da130c55574c07a501db14f6cd73ef0d676f0588..c09b036b67b21a9e93675cd6bb07eab59b02a81f 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -235,7 +235,7 @@ let check_homogeneous_call ~subst context indparamsno n uri reduct tl =
    (fun k x ->
      if k = 0 then 0
      else
-      match R.whd context x with
+      match R.whd ~subst context x with
       | C.Rel m when m = n - (indparamsno - k) -> k - 1
       | _ -> raise (TypeCheckerFailure (lazy 
          ("Argument "^string_of_int (indparamsno - k + 1) ^ " (of " ^
@@ -268,7 +268,7 @@ let rec weakly_positive ~subst context n nn uri indparamsno posuri te =
      are skipped because we already know that are_all_occurrences_positive
      of uri in te. *)
   let rec aux context n nn te =
-    match R.whd context te with
+    match R.whd ~subst context te with
      | t when t = dummy -> true
      | C.Appl (te::rargs) when te = dummy ->
         List.for_all (does_not_occur ~subst context n nn) rargs
@@ -286,7 +286,7 @@ let rec weakly_positive ~subst context n nn uri indparamsno posuri te =
      aux context n nn (subst_inductive_type_with_dummy () te)
 
 and strictly_positive ~subst context n nn indparamsno posuri te =
-  match R.whd context te with
+  match R.whd ~subst context te with
    | t when does_not_occur ~subst context n nn t -> true
    | C.Rel _ when indparamsno = 0 -> true
    | C.Appl ((C.Rel m)::tl) as reduct when m > n && m <= nn ->
@@ -314,7 +314,7 @@ and strictly_positive ~subst context n nn indparamsno posuri te =
        
 (* the inductive type indexes are s.t. n < x <= nn *)
 and are_all_occurrences_positive ~subst context uri indparamsno i n nn te =
-  match R.whd context te with
+  match R.whd ~subst context te with
   |  C.Appl ((C.Rel m)::tl) as reduct when m = i ->
       check_homogeneous_call ~subst context indparamsno n uri reduct tl;
       List.for_all (does_not_occur ~subst context n nn) tl
@@ -714,7 +714,7 @@ and is_non_recursive_singleton ~subst (Ref.Ref (uri,_)) iname ity cty =
 
 and is_non_informative ~metasenv ~subst paramsno c =
  let rec aux context c =
-   match R.whd context c with
+   match R.whd ~subst context c with
     | C.Prod (n,so,de) ->
        let s = typeof ~metasenv ~subst context so in
        s = C.Sort C.Prop && aux ((n,(C.Decl so))::context) de
@@ -1001,7 +1001,7 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen nn =
    aux context 0 nn false t
                                                                       
 and recursive_args ~subst ~metasenv context n nn te =
-  match R.whd context te with
+  match R.whd ~subst context te with
   | C.Rel _ | C.Appl _ | C.Const _ -> []
   | C.Prod (name,so,de) ->
      (not (does_not_occur ~subst context n nn so)) ::

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index 2fc29d5978193fa19f0d3b18e3a1f4d302ae3981..b8f31c805e18c414c1b1f85c5bdde2043ee86b70 100644 (file)
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -40,7 +40,8 @@ let db () =
             let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in
             let src, tgt = 
               let cty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] c in
-              match NCicMetaSubst.saturate ~delta:max_int [] [] cty (arity+1) 
+              match 
+               NCicMetaSubst.saturate ~delta:max_int [] [] [] cty (arity+1) 
               with
               | NCic.Prod (_, src, tgt),_,_ -> 
                 src, NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt 
@@ -58,8 +59,7 @@ let db () =
     (DB.empty,DB.empty) (CoercDb.to_list ())
 ;;
 
-(* XXX saturate takes no subst!!!! *)
-let look_for_coercion (db_src,db_tgt) metasenv _subst context infty expty =
+let look_for_coercion (db_src,db_tgt) metasenv subst context infty expty =
   let set_src = DB.retrieve_unifiables db_src infty in
   let set_tgt = DB.retrieve_unifiables db_tgt expty in
   let candidates = CoercionSet.inter set_src set_tgt in
@@ -68,11 +68,11 @@ let look_for_coercion (db_src,db_tgt) metasenv _subst context infty expty =
     (fun (t,arity,arg) ->
         let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t in
         let ty, metasenv, args = 
-          NCicMetaSubst.saturate ~delta:max_int metasenv context ty arity
+          NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity
         in
         prerr_endline (
           NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^ 
-          NCicPp.ppterm ~metasenv ~subst:_subst ~context
+          NCicPp.ppterm ~metasenv ~subst ~context
           (NCicUntrusted.mk_appl t args) ^ " --- " ^ 
             string_of_int (List.length args) ^ " == " ^ string_of_int arg);
         metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index 5e72d90c77eac85827b0cef8ae790b9f51b40396..6a0406747abba552d2811eb2337b44055b79d83a 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -363,7 +363,7 @@ let mk_meta ?name metasenv context ty =
     mk_meta name (newmeta ()) metasenv context ty
 ;;
 
-let saturate ?(delta=0) metasenv context ty goal_arity =
+let saturate ?(delta=0) metasenv subst context ty goal_arity =
  assert (goal_arity >= 0);
   let rec aux metasenv = function
    | NCic.Prod (name,s,t) ->
@@ -377,7 +377,7 @@ let saturate ?(delta=0) metasenv context ty goal_arity =
        else
          t, metasenv1, arg::args, pno+1
    | ty ->
-        match NCicReduction.whd context ty ~delta with
+        match NCicReduction.whd ~subst context ty ~delta with
         | NCic.Prod _ as ty -> aux metasenv ty
         | ty -> ty, metasenv, [], 0
   in

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli
index 21ac5c3ccce704a8473cd7cc7f23f53c1d33d559..1d7b6729e11ee5d6be2db10be7f2bbe3c8e08ebd 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.mli
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli
@@ -61,6 +61,7 @@ val mk_meta:
 
 (* returns the resulting type, the metasenv and the arguments *)
 val saturate:
-    ?delta:int -> NCic.metasenv -> NCic.context -> NCic.term -> int ->
+    ?delta:int -> NCic.metasenv -> NCic.substitution -> 
+    NCic.context -> NCic.term -> int ->
        NCic.term * NCic.metasenv * NCic.term list
 

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index e9d0e97fd8e9f3ede237fdb4185a2c3bd4b18aba..7ea11f3120035edaf8d4c63e43f7be8830c270fd 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -225,7 +225,7 @@ let rec typeof
       let _, _, arity, cl = List.nth itl tyno in
       let constructorsno = List.length cl in
       let _, metasenv, args = 
-        NCicMetaSubst.saturate metasenv context arity 0 in
+        NCicMetaSubst.saturate metasenv subst context arity 0 in
       let ind = if args = [] then C.Const r else C.Appl (C.Const r::args) in
       let metasenv, subst, term, _ = 
         typeof_aux metasenv subst context (Some ind) term in