+ | C.MutCase (uri, i, outtype, term, pl) ->
+ (* first, get the inductive type (and noparams) in the environment *)
+ let (_,b,arity,constructors), expl_params, no_left_params =
+ match CicEnvironment.get_cooked_obj ~trust:true uri with
+ C.InductiveDefinition (l,expl_params,parsno) ->
+ List.nth l i , expl_params, parsno
+ | _ ->
+ raise
+ (RefineFailure
+ ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) in
+ let rec count_prod t =
+ match CicReduction.whd ~subst context t with
+ C.Prod (_, _, t) -> 1 + (count_prod t)
+ | _ -> 0 in
+ let no_args = count_prod arity in
+ (* now, create a "generic" MutInd *)
+ let metasenv,left_args =
+ CicMkImplicit.n_fresh_metas metasenv subst context no_left_params in
+ 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 actual_type,subst,metasenv =
+ type_of_aux subst metasenv context term in
+ let _, subst, metasenv =
+ type_of_aux subst metasenv context expected_type
+ in
+ let actual_type = CicReduction.whd ~subst context actual_type in
+ let subst,metasenv =
+ fo_unif_subst subst context metasenv expected_type actual_type
+ in
+ (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
+ let (_,outtypeinstances,subst,metasenv) =
+ List.fold_left
+ (fun (j,outtypeinstances,subst,metasenv) 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 actual_type,subst,metasenv =
+ type_of_aux subst metasenv context p in
+ let expected_type, subst, metasenv =
+ type_of_aux subst metasenv context constructor in
+ let outtypeinstance,subst,metasenv =
+ check_branch
+ 0 context metasenv subst
+ no_left_params actual_type constructor expected_type in
+ (j+1,outtypeinstance::outtypeinstances,subst,metasenv))
+ (1,[],subst,metasenv) 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 *)
+
+ (* easy case *)
+ let _, subst, metasenv =
+ type_of_aux subst metasenv context
+ (C.Appl ((outtype :: right_args) @ [term]))
+ in
+ let (subst,metasenv) =
+ List.fold_left
+ (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
+ let instance' =
+ let appl =
+ let outtype' =
+ CicSubstitution.lift constructor_args_no outtype
+ in
+ C.Appl (outtype'::args)
+ in
+(*
+ (* if appl is not well typed then the type_of below solves the
+ * problem *)
+ let (_, subst, metasenv) =
+ type_of_aux subst metasenv context appl
+ in
+*)
+ (* DEBUG
+ let prova1 = CicMetaSubst.whd subst context appl in
+ let prova2 = CicReduction.whd ~subst context appl in
+ if not (prova1 = prova2) then
+ begin
+ prerr_endline ("prova1 =" ^ (CicPp.ppterm prova1));
+ prerr_endline ("prova2 =" ^ (CicPp.ppterm prova2));
+ end;
+ *)
+ (* CicMetaSubst.whd subst context appl *)
+ CicReduction.whd ~subst context appl
+ in
+ fo_unif_subst subst context metasenv instance instance')
+ (subst,metasenv) outtypeinstances in
+ CicReduction.whd ~subst
+ context (C.Appl(outtype::right_args@[term])),subst,metasenv
+ | C.Fix (i,fl) ->
+ let subst,metasenv,types =
+ List.fold_left
+ (fun (subst,metasenv,types) (n,_,ty,_) ->
+ let _,subst',metasenv' = type_of_aux subst metasenv context ty in
+ subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
+ ) (subst,metasenv,[]) fl
+ in
+ let len = List.length types in
+ let context' = types@context in
+ let subst,metasenv =
+ List.fold_left
+ (fun (subst,metasenv) (name,x,ty,bo) ->
+ let ty_of_bo,subst,metasenv =
+ type_of_aux subst metasenv context' bo
+ in
+ fo_unif_subst subst context' metasenv
+ ty_of_bo (CicSubstitution.lift len ty)
+ ) (subst,metasenv) fl in
+ let (_,_,ty,_) = List.nth fl i in
+ ty,subst,metasenv
+ | C.CoFix (i,fl) ->
+ let subst,metasenv,types =
+ List.fold_left
+ (fun (subst,metasenv,types) (n,ty,_) ->
+ let _,subst',metasenv' = type_of_aux subst metasenv context ty in
+ subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
+ ) (subst,metasenv,[]) fl
+ in
+ let len = List.length types in
+ let context' = types@context in
+ let subst,metasenv =
+ List.fold_left
+ (fun (subst,metasenv) (name,ty,bo) ->
+ let ty_of_bo,subst,metasenv =
+ type_of_aux subst metasenv context' bo
+ in
+ fo_unif_subst subst context' metasenv
+ ty_of_bo (CicSubstitution.lift len ty)
+ ) (subst,metasenv) fl in
+
+ let (_,ty,_) = List.nth fl i in
+ ty,subst,metasenv