| C.Var uri -> type_of_variable uri
| C.Meta (n,l) ->
(* Let's visit all the subterms that will not be visited later *)
- let _ =
- List.iter
- (function
- None -> ()
- | Some t -> ignore (type_of_aux context t None)
- ) l
+ let (_,canonical_context,_) =
+ List.find (function (m,_,_) -> n = m) metasenv
in
- let (_,canonical_context,ty) =
- List.find (function (m,_,_) -> n = m) metasenv
+ let lifted_canonical_context =
+ let rec aux i =
+ 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.Def t))::tl ->
+ (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+ | None::tl -> None::(aux (i+1) tl)
+ in
+ aux 1 canonical_context
in
- (* Checks suppressed *)
- CicSubstitution.lift_meta l ty
+ let _ =
+ List.iter2
+ (fun t ct ->
+ match t,ct with
+ _,None -> ()
+ | Some t,Some (_,C.Def ct) ->
+ let expected_type =
+ R.whd context
+ (CicTypeChecker.type_of_aux' metasenv context ct)
+ in
+ (* Maybe I am a bit too paranoid, because *)
+ (* if the term is well-typed than t and ct *)
+ (* are convertible. Nevertheless, I compute *)
+ (* the expected type. *)
+ ignore (type_of_aux context t (Some expected_type))
+ | Some t,Some (_,C.Decl ct) ->
+ ignore (type_of_aux context t (Some ct))
+ | _,_ -> assert false (* the term is not well typed!!! *)
+ ) l lifted_canonical_context
+ in
+ let (_,canonical_context,ty) =
+ List.find (function (m,_,_) -> n = m) metasenv
+ in
+ (* Checks suppressed *)
+ CicSubstitution.lift_meta l ty
| C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
| C.Implicit -> raise (Impossible 21)
| C.Cast (te,ty) ->
(* Checks suppressed *)
C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t None)
| C.Appl (he::tl) when List.length tl > 0 ->
- let hetype = type_of_aux context he None in
- let tlbody_and_type =
- let rec aux =
- function
- _,[] -> []
- | C.Prod (n,s,t),he::tl ->
- (he, type_of_aux context he (Some (head_beta_reduce s)))::
- (aux (R.whd context (S.subst he t), tl))
- | _ -> assert false
- in
- aux (R.whd context hetype, tl)
+ let expected_hetype =
+ (* Inefficient, the head is computed twice. But I know *)
+ (* of no other solution. *)
+ R.whd context (CicTypeChecker.type_of_aux' metasenv context he)
in
- eat_prods context hetype tlbody_and_type
+ let hetype = type_of_aux context he (Some expected_hetype) in
+ let tlbody_and_type =
+ let rec aux =
+ function
+ _,[] -> []
+ | C.Prod (n,s,t),he::tl ->
+ (he, type_of_aux context he (Some (head_beta_reduce s)))::
+ (aux (R.whd context (S.subst he t), tl))
+ | _ -> assert false
+ in
+ aux (expected_hetype, tl)
+ in
+ eat_prods context hetype tlbody_and_type
| C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
| C.Const (uri,cookingsno) ->
cooked_type_of_constant uri cookingsno
(* the synthesized type. Let's forget it. *)
{synthesized = synthesized' ; expected = None}, synthesized
| Some expectedty' ->
-prerr_endline ("t: " ^ CicPp.ppterm t) ; flush stderr ;
-prerr_endline (CicPp.ppterm synthesized' ^ " <-> " ^ CicPp.ppterm expectedty') ; flush stderr ;
{synthesized = synthesized' ; expected = Some expectedty'},
expectedty'
in