- fixed hint generation, more hints are generated

[helm.git] / helm / software / components / ng_refiner / nCicRefiner.ml

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 6779667d9ca8f4bd4bf83cb6ea2bc9edcc31a688..1cd2e54b96614a37ae097022799f109a964d7765 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -23,12 +23,9 @@ let inside c = indent := !indent ^ String.make 1 c;;
 let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
 
 
-(*
 let pp s = 
   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
 ;;  
-*)
-
 
 let pp _ = ();;
 
@@ -111,7 +108,7 @@ let rec typeof hdb
        | _ ->
           pp (lazy (
           (NCicPp.ppterm ~metasenv ~subst ~context infty) ^  " === " ^
-          (NCicPp.ppterm ~metasenv ~subst ~context expty)));
+          (NCicPp.ppterm ~metasenv ~subst:[] ~context expty)));
            try 
              let metasenv, subst =
                NCicUnification.unify hdb metasenv subst context infty expty 
@@ -127,7 +124,9 @@ let rec typeof hdb
     fun t as orig -> 
     (*D*)inside 'R'; try let rc = 
     pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t));
-    pp (lazy (NCicPp.ppmetasenv ~subst metasenv));
+    pp (lazy (if expty = None then "NONE" else "SOME"));
+    if (List.exists (fun (i,_) -> i=29) subst) then 
+      pp (lazy (NCicPp.ppsubst ~metasenv subst));
     let metasenv, subst, t, infty = 
     match t with
     | C.Rel n ->
@@ -225,10 +224,17 @@ let rec typeof hdb
        let bo_ty = NCicSubstitution.subst ~avoid_beta_redexes:true t bo_ty in
        metasenv, subst, C.LetIn (n, ty, t, bo), bo_ty
     | C.Appl ((he as orig_he)::(_::_ as args)) ->
+       let upto = 
+         match orig_he with C.Meta _ -> List.length args | _ -> 0
+       in
        let metasenv, subst, he, ty_he = 
          typeof_aux metasenv subst context None he in
-       eat_prods hdb ~localise ~look_for_coercion 
-         metasenv subst context orig_he he ty_he args
+       let metasenv, subst, t, ty = 
+         eat_prods hdb ~localise ~look_for_coercion 
+           metasenv subst context orig_he he ty_he args
+       in
+       let t = if upto > 0 then NCicReduction.head_beta_reduce ~upto t else t in
+       metasenv, subst, t, ty
    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
    | C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as r,
           outtype,(term as orig_term),pl) as orig ->
@@ -240,9 +246,19 @@ let rec typeof hdb
       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
+      let parameters, arguments = HExtlib.split_nth leftno args in
+      let outtype =  
+        match outtype with
+        | C.Implicit _ as ot -> 
+             let rec aux = function
+               | [] -> NCic.Lambda ("_",NCic.Implicit `Type,ot)
+               | _::tl -> NCic.Lambda ("_",NCic.Implicit `Type,aux tl)
+             in
+               aux arguments
+        | _ -> outtype
+      in 
       let metasenv, subst, outtype, outsort = 
         typeof_aux metasenv subst context None outtype in
-      let parameters, arguments = HExtlib.split_nth leftno args in
       (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
       let ind =
         if parameters = [] then C.Const r
@@ -257,6 +273,14 @@ let rec typeof hdb
       if List.length pl <> constructorsno then
        raise (RefineFailure (lazy (localise orig, 
          "Wrong number of cases in a match")));
+(*
+      let metasenv, subst =
+        match expty with
+        | None -> metasenv, subst
+        | Some expty -> 
+           NCicUnification.unify hdb metasenv subst context resty expty 
+      in
+*)
       let _, metasenv, subst, pl_rev =
         List.fold_left
           (fun (j, metasenv, subst, branches) p ->
@@ -278,12 +302,10 @@ let rec typeof hdb
               j+1, metasenv, subst, p :: branches)
           (1, metasenv, subst, []) pl
       in
-      metasenv, subst, 
-      C.Match (r, outtype, term, List.rev pl_rev),
-      NCicReduction.head_beta_reduce (C.Appl (outtype::arguments@[term]))
-    | C.Match _ as orig -> 
-        prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context orig);
-        assert false
+      let resty = C.Appl (outtype::arguments@[term]) in
+      let resty = NCicReduction.head_beta_reduce ~subst resty in
+      metasenv, subst, C.Match (r, outtype, term, List.rev pl_rev),resty
+    | C.Match _ as orig -> assert false
     in
     pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " :: "^
          NCicPp.ppterm ~metasenv ~subst ~context infty ));