X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Feta_fixing.ml;h=68dec37d6b04230f1468665e0a6f77516ccdb365;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=876c5c6783190d7da4829bec4d8bb848dddcf038;hpb=059db27238ba60f5c6bdf229bdb2265fa194a280;p=helm.git diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml index 876c5c678..68dec37d6 100644 --- a/helm/ocaml/cic_omdoc/eta_fixing.ml +++ b/helm/ocaml/cic_omdoc/eta_fixing.ml @@ -23,9 +23,9 @@ * http://cs.unibo.it/helm/. *) -exception ReferenceToVariable;; -exception RferenceToCurrentProof;; -exception ReferenceToInductiveDefinition;; +exception ReferenceToNonVariable;; + +let prerr_endline _ = ();; (* let rec fix_lambdas_wrt_type ty te = @@ -130,7 +130,11 @@ let fix_according_to_type ty hd tl = let rec aux n ty tl res = if n = 0 then (match tl with - [] -> C.Appl res + [] -> + (match res with + [] -> assert false + | [res] -> res + | _ -> C.Appl res) | _ -> match res with [] -> assert false @@ -161,25 +165,20 @@ let fix_according_to_type ty hd tl = aux expected_arity ty tl [hd] ;; -let eta_fix metasenv t = +let eta_fix metasenv context 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 C.Rel n -> C.Rel n | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map - (function i,t -> i, (eta_fix' context t)) exp_named_subst - in - C.Var (uri,exp_named_subst') + let exp_named_subst' = fix_exp_named_subst context exp_named_subst in + C.Var (uri,exp_named_subst') | C.Meta (n,l) -> - let (_,canonical_context,_) = - List.find (function (m,_,_) -> n = m) metasenv - in - let l' = + let (_,canonical_context,_) = CicUtil.lookup_meta n metasenv in + let l' = List.map2 (fun ct t -> match (ct, t) with @@ -190,7 +189,7 @@ let eta_fix metasenv t = in C.Meta (n,l') | C.Sort s -> C.Sort s - | C.Implicit -> C.Implicit + | C.Implicit _ as t -> t | C.Cast (v,t) -> C.Cast (eta_fix' context v, eta_fix' context t) | C.Prod (n,s,t) -> C.Prod @@ -200,57 +199,52 @@ let eta_fix metasenv t = (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 (match l' with + [] -> assert false + | he::tl -> + let ty,_ = + CicTypeChecker.type_of_aux' metasenv context he + CicUniv.empty_ugraph + in + fix_according_to_type ty he tl +(* C.Const(uri,exp_named_subst)::l'' -> let constant_type = (match CicEnvironment.get_obj uri with C.Constant (_,_,ty,_) -> ty | C.Variable _ -> raise ReferenceToVariable - | C.CurrentProof (_,_,_,_,params) -> raise RferenceToCurrentProof + | C.CurrentProof (_,_,_,_,params) -> raise ReferenceToCurrentProof | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - ) - in - 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 - | _ -> C.Appl l' ) + ) in + fix_according_to_type + constant_type (C.Const(uri,exp_named_subst)) l'' + | _ -> C.Appl l' *)) | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - List.map - (function i,t -> i, (eta_fix' context t)) exp_named_subst - in - C.Const (uri,exp_named_subst') + let exp_named_subst' = fix_exp_named_subst context exp_named_subst in + C.Const (uri,exp_named_subst') | C.MutInd (uri,tyno,exp_named_subst) -> - let exp_named_subst' = - List.map - (function i,t -> i, (eta_fix' context t)) exp_named_subst - in + let exp_named_subst' = fix_exp_named_subst context exp_named_subst in C.MutInd (uri, tyno, exp_named_subst') | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let exp_named_subst' = - List.map - (function i,t -> i, (eta_fix' context t)) exp_named_subst - in + let exp_named_subst' = fix_exp_named_subst context exp_named_subst in C.MutConstruct (uri, tyno, consno, exp_named_subst') | C.MutCase (uri, tyno, outty, term, patterns) as prima -> let outty' = eta_fix' context outty in let term' = eta_fix' context term in let patterns' = List.map (eta_fix' context) patterns in let inductive_types,noparams = - (match CicEnvironment.get_obj uri with + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + (match o with Cic.Constant _ -> assert false | Cic.Variable _ -> assert false | Cic.CurrentProof _ -> assert false - | Cic.InductiveDefinition (l,_,n) -> l,n + | 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 @@ -262,21 +256,26 @@ let eta_fix metasenv t = 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 + CicUniv.empty_ugraph + in (match term_type with C.Appl (hd::params) -> - List.map (fun (_,t) -> clean_up t params) constructors + let rec first_n n l = + if n = 0 then [] + else + (match l with + a::tl -> a::(first_n (n-1) tl) + | _ -> assert false) in + List.map + (fun (_,t) -> + clean_up t (first_n noparams params)) constructors | _ -> prerr_endline ("QUA"); assert false) in 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 @@ -292,11 +291,21 @@ let eta_fix metasenv t = List.map (fun (name, ty, bo) -> (name, eta_fix' context ty, eta_fix' (fun_types@context) bo)) funs) - in - eta_fix' [] t + and fix_exp_named_subst context exp_named_subst = + List.rev + (List.fold_left + (fun newsubst (uri,t) -> + let t' = eta_fix' context t in + let ty = + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + match o with + Cic.Variable (_,_,ty,_,_) -> + CicSubstitution.subst_vars newsubst ty + | _ -> raise ReferenceToNonVariable + in + let t'' = fix_according_to_type ty t' [] in + (uri,t'')::newsubst + ) [] exp_named_subst) + in + eta_fix' context t ;; - - - - -