Defs in context may now have an optional type (when unknown).

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index e5e8469824226e37c5a2c013345f5e8d17c7d879..881c72bfd516852218105dc56ce71653219ce4d8 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -96,7 +96,9 @@ and type_of_aux' metasenv context t =
        (try
          match List.nth context (n - 1) with
             Some (_,C.Decl t) -> S.lift n t,subst,metasenv
-          | Some (_,C.Def bo) ->
+          | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
+          | Some (_,C.Def (bo,None)) ->
+             prerr_endline "##### DA INVESTIGARE E CAPIRE" ;
              type_of_aux subst metasenv context (S.lift n bo)
          | None -> raise RelToHiddenHypothesis
         with
@@ -160,9 +162,9 @@ and type_of_aux' metasenv context t =
           C.Prod (n,s,type2),subst'''',metasenv''''
    | C.LetIn (n,s,t) ->
       (* only to check if s is well-typed *)
-      let _,subst',metasenv' = type_of_aux subst metasenv context s in
+      let ty,subst',metasenv' = type_of_aux subst metasenv context s in
       let inferredty,subst'',metasenv'' =
-       type_of_aux subst' metasenv' ((Some (n,(C.Def s)))::context) t
+       type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
       in
        (* One-step LetIn reduction. Even faster than the previous solution.
           Moreover the inferred type is closer to the expected one. *)
@@ -224,9 +226,10 @@ and type_of_aux' metasenv context t =
          [] -> []
        | (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.Def t))::tl ->
-          (Some (n,C.Def (S.lift_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)
        | None::tl -> None::(aux (i+1) tl)
+       | (Some (_,C.Def (_,Some _)))::_ -> assert false
      in
       aux 1 canonical_context
     in
@@ -234,7 +237,7 @@ and type_of_aux' metasenv context t =
       (fun (subst,metasenv) t ct -> 
         match (t,ct) with
            _,None -> subst,metasenv
-         | Some t,Some (_,C.Def ct) ->
+         | Some t,Some (_,C.Def (ct,_)) ->
             (try
               CicUnification.fo_unif_subst subst context metasenv t ct
              with _ -> raise MetasenvInconsistency)