| C.Sort C.Type -> "Type"
| _ -> assert false
in
- let ainnertypes,innertype,innersort =
+ let ainnertypes,innertype,innersort,expected_available =
(*CSC: Here we need the algorithm for Coscoy's double type-inference *)
(*CSC: (expected type + inferred type). Just for now we use the usual *)
(*CSC: type-inference, but the result is very poor. As a very weak *)
D.expected = None}
in
let innersort = T.type_of_aux' metasenv context synthesized in
- let ainnertypes =
+ let ainnertypes,expected_available =
if computeinnertypes then
- Some
- {annsynthesized =
- aux false (Some fresh_id'') context synthesized ;
- annexpected =
+ let annexpected,expected_available =
match expected with
- None -> None
+ None -> None,false
| Some expectedty' ->
- Some (aux false (Some fresh_id'') context expectedty')
- }
+ Some (aux false (Some fresh_id'') context expectedty'),true
+ in
+ Some
+ {annsynthesized =
+ aux false (Some fresh_id'') context synthesized ;
+ annexpected = annexpected
+ }, expected_available
else
- None
+ None,false
in
- ainnertypes, synthesized, string_of_sort innersort
+ ainnertypes,synthesized, string_of_sort innersort, expected_available
in
let add_inner_type id =
match ainnertypes with
C.Lambda _ -> true
| _ -> false
in
- if not father_is_lambda then
+ if (not father_is_lambda) || expected_available then
add_inner_type fresh_id''
end ;
C.ALambda
(* 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
let out_str = function
| MQCons s -> con s
- | MQRVar s -> out_rvar s
- | MQSVar s -> out_svar s
+ | MQSRVar s -> out_rvar s
+ | MQSSVar s -> out_svar s
| MQFunc (f, r) -> out_func f ^ out_rvar r
| MQMConclusion -> key "mainconclusion"
| MQConclusion -> key "conclusion"
| MQPattern p -> key "pattern" ^ out_pat p
| MQUnion (l1, l2) -> sep "(" ^ out_list l1 ^ key "union" ^ out_list l2 ^ sep ")"
| MQIntersect (l1, l2) -> sep "(" ^ out_list l1 ^ key "intersect" ^ out_list l2 ^ sep ")"
- | MQRVarOccur v -> key "rvaroccur" ^ v
+ | MQLRVar v -> key "rvaroccur" ^ v
let out_query = function
| MQList l -> out_list l
let mqs = if b then MQMConclusion else MQConclusion in
MQSelect (rvar,
MQUse (MQPattern r, svar),
- MQIs (MQSVar svar, mqs)
+ MQIs (MQSSVar svar, mqs)
)
let rec build_inter n = function
MQSubset (
MQSelect (
"uri2",
- MQUsedBy (MQRVarOccur "uri", "pos"),
+ MQUsedBy (MQLRVar "uri", "pos"),
MQOr (
- MQIs (MQSVar "pos", MQConclusion),
- MQIs (MQSVar "pos", MQMConclusion)
+ MQIs (MQSSVar "pos", MQConclusion),
+ MQIs (MQSSVar "pos", MQMConclusion)
)
),
universe