new disambiguator almost attached

[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 10eff13b41734ae7b192c0d3b3408139c3fc8090..8c6c94cb576f30c1397aacecfe4966ab9f0c49b8 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -22,11 +22,13 @@ let indent = ref "";;
 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 _ = ();; *)
+let pp _ = ();;
 
 let wrap_exc msg = function
   | NCicUnification.Uncertain _ -> Uncertain msg
@@ -38,7 +40,7 @@ let wrap_exc msg = function
 let exp_implicit metasenv context expty =
  let foo x = match expty with Some t -> `WithType t | None -> x in
  function      
-  | `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Type)
+  | `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Term)
   | `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type)
   | `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term)
   | _ -> assert false
@@ -46,17 +48,19 @@ let exp_implicit metasenv context expty =
 
 let force_to_sort metasenv subst context t =
   match NCicReduction.whd ~subst context t with
-  | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) as t -> 
+  | C.Meta (_,(0,(C.Irl 0 | C.Ctx []))) as t -> 
      metasenv, subst, t
-  | C.Meta (i,(_,lc)) as t ->
+  | C.Meta (i,(_,(C.Irl 0 | C.Ctx []))) -> 
+     metasenv, subst, C.Meta(i,(0,C.Irl 0))
+  | C.Meta (i,(_,lc)) ->
      let len = match lc with C.Irl len->len | C.Ctx l->List.length l in
-     let metasenv, subst, _ = 
+     let metasenv, subst, newmeta = 
        if len > 0 then
          NCicMetaSubst.restrict metasenv subst i (HExtlib.list_seq 1 (len+1)) 
-       else metasenv, subst, 0
+       else metasenv, subst, i
      in
-     metasenv, subst, t
-  | C.Sort _ -> metasenv, subst, t 
+     metasenv, subst, C.Meta (newmeta,(0,C.Irl 0))
+  | C.Sort _ as t -> metasenv, subst, t 
   | _ -> assert false
 ;;
 
@@ -71,9 +75,9 @@ let sort_of_prod
    | C.Sort (C.Type u1), C.Sort (C.Type u2) ->
         metasenv, subst, C.Sort (C.Type (u1@u2)) 
    | C.Sort C.Prop,C.Sort (C.Type _) -> metasenv, subst, t2
-   | C.Meta _, C.Sort _
-   | C.Meta _, C.Meta _
-   | C.Sort _, C.Meta  _ -> metasenv, subst, t2
+   | C.Meta _, C.Sort _ 
+   | C.Meta _, C.Meta (_,(_,_))
+   | C.Sort _, C.Meta (_,(_,_)) -> metasenv, subst, t2 
    | x, (C.Sort _ | C.Meta _) | _, x -> 
       let y, context, orig = 
         if x == t1 then s, context, orig_s 
@@ -94,29 +98,32 @@ let check_allowed_sort_elimination localise r orig =
    let rec aux metasenv subst context ind arity1 arity2 =
      (*D*)inside 'S'; try let rc = 
      let arity1 = NCicReduction.whd ~subst context arity1 in
+     pp (lazy(NCicPp.ppterm ~subst ~metasenv ~context arity1 ^ "   elimsto   " ^
+        NCicPp.ppterm ~subst ~metasenv ~context arity2 ^ "\nMENV:\n"^
+        NCicPp.ppmetasenv ~subst metasenv));
      match arity1 with
      | C.Prod (name,so1,de1) (* , t ==?== C.Prod _ *) ->
         let metasenv, meta, _ = 
-          NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) `Typeless 
+          NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) `Type 
         in
         let metasenv, subst = 
           try NCicUnification.unify metasenv subst context 
-                (C.Prod (name, so1, meta)) arity2 
+                arity2 (C.Prod (name, so1, meta)) 
           with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf
             "expected %s, found %s" (* XXX localizzare meglio *)
-            (NCicPp.ppterm ~subst ~metasenv ~context arity1)
+            (NCicPp.ppterm ~subst ~metasenv ~context (C.Prod (name, so1, meta)))
             (NCicPp.ppterm ~subst ~metasenv ~context arity2))) exc)
         in
         aux metasenv subst ((name, C.Decl so1)::context)
          (mkapp (NCicSubstitution.lift 1 ind) (C.Rel 1)) de1 meta
      | C.Sort _ (* , t ==?== C.Prod _ *) ->
-        let metasenv, meta, _ = NCicMetaSubst.mk_meta metasenv [] `Typeless in
+        let metasenv, meta, _ = NCicMetaSubst.mk_meta metasenv [] `Type in
         let metasenv, subst = 
           try NCicUnification.unify metasenv subst context 
-                (C.Prod ("_", ind, meta)) arity2 
+                arity2 (C.Prod ("_", ind, meta)) 
           with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf
             "expected %s, found %s" (* XXX localizzare meglio *)
-            (NCicPp.ppterm ~subst ~metasenv ~context arity1)
+            (NCicPp.ppterm ~subst ~metasenv ~context (C.Prod ("_", ind, meta)))
             (NCicPp.ppterm ~subst ~metasenv ~context arity2))) exc)
         in
         (try NCicTypeChecker.check_allowed_sort_elimination
@@ -160,6 +167,7 @@ let rec typeof
     fun t as orig -> 
     (*D*)inside 'R'; try let rc = 
     pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t));
+    pp (lazy (NCicPp.ppmetasenv ~subst metasenv));
     let metasenv, subst, t, infty = 
     match t with
     | C.Rel n ->
@@ -288,6 +296,9 @@ let rec typeof
               let ty_branch = 
                 NCicTypeChecker.type_of_branch 
                   ~subst context leftno outtype cons ty_cons in
+              pp (lazy ("TYPEOFBRANCH: " ^
+               NCicPp.ppterm ~metasenv ~subst ~context p ^ " ::: " ^
+               NCicPp.ppterm ~metasenv ~subst ~context ty_branch ));
               let metasenv, subst, p, _ = 
                 typeof_aux metasenv subst context (Some ty_branch) p in
               j+1, metasenv, subst, p :: branches)
@@ -298,6 +309,8 @@ let rec typeof
       NCicReduction.head_beta_reduce (C.Appl (outtype::arguments@[term]))
     | C.Match _ -> assert false
     in
+    pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " :: "^
+         NCicPp.ppterm ~metasenv ~subst ~context infty ));
       force_ty metasenv subst context orig t infty expty
     (*D*)in outside(); rc with exc -> outside (); raise exc
   in
@@ -314,7 +327,8 @@ and eat_prods localise metasenv subst context orig_he he ty_he args =
             typeof ~localise metasenv subst context arg (Some s) in
           let t = NCicSubstitution.subst ~avoid_beta_redexes:true arg t in
           aux metasenv subst (arg :: args_so_far) t tl
-      | t ->
+      | C.Meta _
+      | C.Appl (C.Meta _ :: _) as t ->
           let metasenv, subst, arg, ty_arg = 
             typeof ~localise metasenv subst context arg None in
           let metasenv, meta, _ = 
@@ -323,20 +337,35 @@ and eat_prods localise metasenv subst context orig_he he ty_he args =
           in
           let flex_prod = C.Prod ("_", ty_arg, meta) in
           pp (lazy ( "UNIFICATION in CTX:\n"^ 
-            NCicPp.ppcontext ~metasenv ~subst context ^ "\nMENV:\n" ^
-            NCicPp.ppmetasenv ~subst metasenv ^ "\nOF: " ^
+            NCicPp.ppcontext ~metasenv ~subst context
+            ^ "\nOF: " ^
             NCicPp.ppterm ~metasenv ~subst ~context t ^  " === " ^
             NCicPp.ppterm ~metasenv ~subst ~context flex_prod ^ "\n"));
           let metasenv, subst = 
              try NCicUnification.unify metasenv subst context t flex_prod 
              with exc -> raise (wrap_exc (lazy (localise orig_he, Printf.sprintf
-              ("The term %s is here applied to %d arguments but expects " ^^
-              "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he)
-              (List.length args) (List.length args_so_far))) exc)
+              ("The term %s has an inferred type %s, but is applied to the" ^^
+               " argument %s of type %s")
+              (NCicPp.ppterm ~metasenv ~subst ~context he)
+              (NCicPp.ppterm ~metasenv ~subst ~context t)
+              (NCicPp.ppterm ~metasenv ~subst ~context arg)
+              (NCicPp.ppterm ~metasenv ~subst ~context ty_arg))) exc)
               (* XXX coerce to funclass *)
           in
           let meta = NCicSubstitution.subst ~avoid_beta_redexes:true arg meta in
           aux metasenv subst (arg :: args_so_far) meta tl
+      | C.Match (_,_,C.Meta _,_) 
+      | C.Match (_,_,C.Appl (C.Meta _ :: _),_) 
+      | C.Appl (C.Const (NReference.Ref (_, NReference.Fix _)) :: _) ->
+          raise (Uncertain (lazy (localise orig_he, Printf.sprintf
+            ("The term %s is here applied to %d arguments but expects " ^^
+            "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he)
+            (List.length args) (List.length args_so_far))))
+      | _ ->
+          raise (RefineFailure (lazy (localise orig_he, Printf.sprintf
+            ("The term %s is here applied to %d arguments but expects " ^^
+            "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he)
+            (List.length args) (List.length args_so_far))))
   in
    aux metasenv subst [] ty_he args
   (*D*)in outside(); rc with exc -> outside (); raise exc