- (* 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
+ (* 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
+ (*
+ (* if appl is not well typed then the type_of below solves the
+ * problem *)
+ let (_, subst, metasenv,ugraph1) =
+ type_of_aux subst metasenv context appl ugraph
+ 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' 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