(*CSC: This is a very inefficient way of computing inner types *)
(*CSC: and inner sorts: very deep terms have their types/sorts *)
(*CSC: computed again and again. *)
- let string_of_sort =
- function
+ let string_of_sort t =
+ match CicReduction.whd context t with
C.Sort C.Prop -> "Prop"
| C.Sort C.Set -> "Set"
| C.Sort C.Type -> "Type"
match expected with
None -> None,false
| Some expectedty' ->
-prerr_endline ("###: " ^ CicPp.ppterm synthesized ^ " <==> " ^ CicPp.ppterm expectedty') ; flush stderr ;
Some (aux false (Some fresh_id'') context expectedty'),true
in
Some
add_inner_type fresh_id'' ;
C.AVar (fresh_id'', uri)
| C.Meta (n,l) ->
+ let (_,canonical_context,_) =
+ List.find (function (m,_,_) -> n = m) metasenv
+ in
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" && expected_available then
add_inner_type fresh_id'' ;
C.AMeta (fresh_id'', n,
- (List.map
- (function None -> None | Some t -> Some (aux' context t)) l))
+ (List.map2
+ (fun ct t ->
+ match (ct, t) with
+ | None, _ -> None
+ | _, Some t -> Some (aux' context t)
+ | Some _, None -> assert false (* due to typing rules *))
+ canonical_context l))
| C.Sort s -> C.ASort (fresh_id'', s)
| C.Implicit -> C.AImplicit (fresh_id'')
| C.Cast (v,t) ->