- when (U.eq equri Logic.eq_URI) or
- (U.eq equri Logic_Type.eqt_URI) -> (
- match tty with (* some inductive type *)
- (C.MutInd (turi,typeno,exp_named_subst))
- | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
-prerr_endline ("XXXX term " ^ CicPp.ppterm term) ;
-prerr_endline ("XXXX termty " ^ CicPp.ppterm termty) ;
-prerr_endline ("XXXX t1 " ^ CicPp.ppterm t1) ;
-prerr_endline ("XXXX t2 " ^ CicPp.ppterm t2) ;
-prerr_endline ("XXXX tty " ^ CicPp.ppterm tty) ;
- let t1',t2',consno = (* sono i due sottotermini che differiscono *)
- match t1,t2 with
- ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::applist1)),
- (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::applist2)))
- when (uri1 = uri2) && (typeno1 = typeno2) && (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) -> (* controllo ridondante *)
- (List.nth applist1 (i-1)),(List.nth applist2 (i-1)),consno2
- | _ -> raise (ProofEngineTypes.Fail "Injection: qui non dovrei capitarci mai")
- in
- let tty' = (CicTypeChecker.type_of_aux' metasenv context t1') in
-prerr_endline ("XXXX tty' " ^ CicPp.ppterm tty') ;
-prerr_endline ("XXXX t1' " ^ CicPp.ppterm t1') ;
-prerr_endline ("XXXX t2' " ^ CicPp.ppterm t2') ;
-prerr_endline ("XXXX consno " ^ string_of_int consno) ;
- let pattern =
- match (CicEnvironment.get_obj turi) with
- C.InductiveDefinition (ind_type_list,_,nr_ind_params_dx) ->
- let _,_,_,constructor_list = (List.nth ind_type_list typeno) in
- let i_constr_id,_ = List.nth constructor_list (consno - 1) in
- List.map
- (function (id,cty) ->
- let reduced_cty = CicReduction.whd context cty in
- let rec aux t k =
- match t with
- C.Prod (_,_,target) when (k <= nr_ind_params_dx) ->
- aux target (k+1)
- | C.Prod (binder,source,target) when (k > nr_ind_params_dx) ->
- let binder' =
- match binder with
- C.Name b -> C.Name b
- | C.Anonymous -> C.Name "y"
- in
- C.Lambda (binder',source,(aux target (k+1)))
- | _ ->
- let nr_param_constr = k - 1 - nr_ind_params_dx in
- if (id = i_constr_id)
- then C.Rel (nr_param_constr - i + 1)
- else S.lift (nr_param_constr + 1) t1' (* + 1 per liftare anche il lambda agguinto esternamente al case *)
- in aux reduced_cty 1
- )
- constructor_list
- | _ -> raise (ProofEngineTypes.Fail "Discriminate: object is not an Inductive Definition: it's imposible")
+ when (U.eq equri Logic.eq_URI) -> (
+ match tty with (* some inductive type *)
+ (C.MutInd (turi,typeno,exp_named_subst))
+ | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
+ let t1',t2',consno = (* sono i due sottotermini che differiscono *)
+ match t1,t2 with
+ ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::applist1)),
+ (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::applist2)))
+ when (uri1 = uri2) && (typeno1 = typeno2) && (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) -> (* controllo ridondante *)
+ (List.nth applist1 (i-1)),(List.nth applist2 (i-1)),consno2
+ | _ -> assert false