exception RferenceToCurrentProof;;
exception ReferenceToInductiveDefinition;;
+let prerr_endline _ = ();;
+
(*
let rec fix_lambdas_wrt_type ty te =
let module C = Cic in
let eta_fix metasenv t =
let rec eta_fix' context t =
- prerr_endline ("entering aux with: term=" ^ CicPp.ppterm t);
- flush stderr ;
+ (* prerr_endline ("entering aux with: term=" ^ CicPp.ppterm t);
+ flush stderr ; *)
let module C = Cic in
let module S = CicSubstitution in
match t with
(n, eta_fix' context s, eta_fix' ((Some (n,(C.Decl s)))::context) t)
| C.LetIn (n,s,t) ->
C.LetIn
- (n, eta_fix' context s, eta_fix' ((Some (n,(C.Def s)))::context) t)
+ (n,eta_fix' context s,eta_fix' ((Some (n,(C.Def (s,None))))::context) t)
| C.Appl l as appl ->
let l' = List.map (eta_fix' context) l
in
| C.Variable _ -> raise ReferenceToVariable
| C.CurrentProof (_,_,_,_,params) -> raise RferenceToCurrentProof
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
- )
- in
+ ) in
+ fix_according_to_type
+ constant_type (C.Const(uri,exp_named_subst)) l''
+(*
let result = fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l'' in
if not (CicReduction.are_convertible [] appl result) then
(prerr_endline ("prima :" ^(CicPp.ppterm appl));
prerr_endline ("dopo :" ^(CicPp.ppterm result)));
- result
+ result *)
| _ -> C.Appl l' )
| C.Const (uri,exp_named_subst) ->
let exp_named_subst' =
| Cic.InductiveDefinition (l,_,n) -> l,n
) in
let (_,_,_,constructors) = List.nth inductive_types tyno in
- prerr_endline ("QUI");
let constructor_types =
let rec clean_up t =
function
if noparams = 0 then
List.map (fun (_,t) -> t) constructors
else
- let term_type =
- CicTypeChecker.type_of_aux' metasenv context term in
+ let term_type =
+ CicTypeChecker.type_of_aux' metasenv context term
+ in
(match term_type with
C.Appl (hd::params) ->
List.map (fun (_,t) -> clean_up t params) constructors
let patterns2 =
List.map2 fix_lambdas_wrt_type
constructor_types patterns in
- let dopo =
- C.MutCase (uri, tyno, outty',term',patterns2) in
- if not (CicReduction.are_convertible [] prima dopo) then
- (prerr_endline ("prima :" ^(CicPp.ppterm prima));
- prerr_endline ("dopo :" ^(CicPp.ppterm dopo)));
- dopo
+ C.MutCase (uri, tyno, outty',term',patterns2)
| C.Fix (funno, funs) ->
let fun_types =
List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) funs in
+
+
+
+
+
+