+ let metasenv,right_args =
+ let no_right_params = no_args - no_left_params in
+ if no_right_params < 0 then assert false
+ else CicMkImplicit.n_fresh_metas
+ metasenv subst context no_right_params
+ in
+ let metasenv,exp_named_subst =
+ CicMkImplicit.fresh_subst metasenv subst context expl_params in
+ let expected_type =
+ if no_args = 0 then
+ C.MutInd (uri,i,exp_named_subst)
+ else
+ C.Appl
+ (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
+ in
+ (* check consistency with the actual type of term *)
+ let term',actual_type,subst,metasenv,ugraph1 =
+ type_of_aux subst metasenv context term ugraph in
+ let expected_type',_, subst, metasenv,ugraph2 =
+ type_of_aux subst metasenv context expected_type ugraph1
+ in
+ let actual_type = CicReduction.whd ~subst context actual_type in
+ let subst,metasenv,ugraph3 =
+ fo_unif_subst subst context metasenv
+ expected_type' actual_type ugraph2
+ in
+ (* TODO: check if the sort elimination
+ * is allowed: [(I q1 ... qr)|B] *)
+ let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
+ List.fold_left
+ (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
+ let constructor =
+ if left_args = [] then
+ (C.MutConstruct (uri,i,j,exp_named_subst))
+ else
+ (C.Appl
+ (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
+ in
+ let p',actual_type,subst,metasenv,ugraph1 =
+ type_of_aux subst metasenv context p ugraph
+ in
+ let constructor',expected_type, subst, metasenv,ugraph2 =
+ type_of_aux subst metasenv context constructor ugraph1
+ in
+ let outtypeinstance,subst,metasenv,ugraph3 =
+ check_branch 0 context metasenv subst no_left_params
+ actual_type constructor' expected_type ugraph2
+ in
+ (pl @ [p'],j+1,
+ outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
+ ([],1,[],subst,metasenv,ugraph3) pl
+ in
+
+ (* we are left to check that the outype matches his instances.
+ The easy case is when the outype is specified, that amount
+ to a trivial check. Otherwise, we should guess a type from
+ its instances
+ *)
+
+ (match outtype with
+ | C.Meta (n,l) ->
+ (let candidate,ugraph5 =
+ match outtypeinstances with
+ | [] -> raise (Uncertain "Inference of annotation for empty inductive types not implemented")
+ | (constructor_args_no,_,instance,_)::tl ->
+ try
+ let instance' =
+ CicSubstitution.delift constructor_args_no
+ (CicMetaSubst.apply_subst subst instance)
+ in
+ List.fold_left (
+ fun (candidate_oty,ugraph)
+ (constructor_args_no,_,instance,_) ->
+ match candidate_oty with
+ | None -> None,ugraph
+ | Some ty ->
+ try
+ let instance' =
+ CicSubstitution.delift
+ constructor_args_no
+ (CicMetaSubst.apply_subst subst instance)
+ in
+ let b,ugraph1 =
+ CicReduction.are_convertible context
+ instance' ty ugraph
+ in
+ if b then
+ candidate_oty,ugraph1
+ else
+ None,ugraph
+ with Failure s -> None,ugraph
+ ) (Some instance',ugraph4) tl
+ with Failure s ->
+ None,ugraph4
+ in
+ match candidate with
+ | None -> raise (Uncertain "can't solve an higher order unification problem")
+ | Some candidate ->
+ let s,m,u =
+ fo_unif_subst subst context metasenv
+ candidate outtype ugraph5
+ in
+ C.MutCase (uri, i, outtype, term', pl'),candidate,s,m,u)
+ | _ -> (* easy case *)
+ let _,_, subst, metasenv,ugraph5 =
+ type_of_aux subst metasenv context
+ (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
+ in
+ let (subst,metasenv,ugraph6) =
+ List.fold_left
+ (fun (subst,metasenv,ugraph)
+ (constructor_args_no,context,instance,args) ->
+ let instance' =
+ let appl =
+ let outtype' =
+ CicSubstitution.lift constructor_args_no outtype
+ in
+ C.Appl (outtype'::args)
+ in
+ CicReduction.whd ~subst context appl
+ in
+ fo_unif_subst subst context metasenv
+ instance instance' ugraph)
+ (subst,metasenv,ugraph5) outtypeinstances
+ in
+ C.MutCase (uri, i, outtype, term', pl'),
+ CicReduction.whd ~subst context
+ (C.Appl(outtype::right_args@[term])),
+ subst,metasenv,ugraph6)
+ | C.Fix (i,fl) ->
+ let fl_ty',subst,metasenv,types,ugraph1 =
+ List.fold_left
+ (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
+ let ty',_,subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context ty ugraph
+ in
+ fl @ [ty'],subst',metasenv',
+ Some (C.Name n,(C.Decl ty')) :: types, ugraph
+ ) ([],subst,metasenv,[],ugraph) fl
+ in
+ let len = List.length types in
+ let context' = types@context in
+ let fl_bo',subst,metasenv,ugraph2 =
+ List.fold_left
+ (fun (fl,subst,metasenv,ugraph) (name,x,ty,bo) ->
+ let bo',ty_of_bo,subst,metasenv,ugraph1 =
+ type_of_aux subst metasenv context' bo ugraph
+ in
+ let subst',metasenv',ugraph' =
+ fo_unif_subst subst context' metasenv
+ ty_of_bo (CicSubstitution.lift len ty) ugraph1
+ in
+ fl @ [bo'] , subst',metasenv',ugraph'
+ ) ([],subst,metasenv,ugraph1) fl
+ in
+ let (_,_,ty,_) = List.nth fl i in
+ (* now we have the new ty in fl_ty', the new bo in fl_bo',
+ * and we want the new fl with bo' and ty' injected in the right
+ * place.
+ *)
+ let rec map3 f l1 l2 l3 =
+ match l1,l2,l3 with
+ | [],[],[] -> []
+ | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
+ | _ -> assert false
+ in
+ let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
+ fl_ty' fl_bo' fl
+ in
+ C.Fix (i,fl''),ty,subst,metasenv,ugraph2
+ | C.CoFix (i,fl) ->
+ let fl_ty',subst,metasenv,types,ugraph1 =
+ List.fold_left
+ (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
+ let ty',_,subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context ty ugraph
+ in
+ fl @ [ty'],subst',metasenv',
+ Some (C.Name n,(C.Decl ty')) :: types, ugraph1
+ ) ([],subst,metasenv,[],ugraph) fl
+ in
+ let len = List.length types in
+ let context' = types@context in
+ let fl_bo',subst,metasenv,ugraph2 =
+ List.fold_left
+ (fun (fl,subst,metasenv,ugraph) (name,ty,bo) ->
+ let bo',ty_of_bo,subst,metasenv,ugraph1 =
+ type_of_aux subst metasenv context' bo ugraph
+ in
+ let subst',metasenv',ugraph' =
+ fo_unif_subst subst context' metasenv
+ ty_of_bo (CicSubstitution.lift len ty) ugraph1
+ in
+ fl @ [bo'],subst',metasenv',ugraph'
+ ) ([],subst,metasenv,ugraph1) fl
+ in
+ let (_,ty,_) = List.nth fl i in
+ (* now we have the new ty in fl_ty', the new bo in fl_bo',
+ * and we want the new fl with bo' and ty' injected in the right
+ * place.
+ *)
+ let rec map3 f l1 l2 l3 =
+ match l1,l2,l3 with
+ | [],[],[] -> []
+ | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
+ | _ -> assert false
+ in
+ let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
+ fl_ty' fl_bo' fl
+ in
+ C.CoFix (i,fl''),ty,subst,metasenv,ugraph2