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=8407f8357e04d3f7f8603759cbeb7432060d58b3;hpb=6248703e9f479d4c3edfcf227908ffd9d2dd7adc;p=helm.git diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml index 8407f8357..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,92 +165,147 @@ let fix_according_to_type ty hd tl = aux expected_arity ty tl [hd] ;; -let eta_fix metasenv t = - let rec eta_fix' t = -(* prerr_endline ("entering aux with: term=" ^ CicPp.ppterm t); +let eta_fix metasenv context t = + let rec eta_fix' context t = + (* 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' 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 None, _ -> None - | _, Some t -> Some (eta_fix' t) + | _, Some t -> Some (eta_fix' context t) | Some _, None -> assert false (* due to typing rules *)) canonical_context l in C.Meta (n,l') | C.Sort s -> C.Sort s - | C.Implicit -> C.Implicit - | C.Cast (v,t) -> C.Cast (eta_fix' v, eta_fix' t) - | C.Prod (n,s,t) -> C.Prod (n, eta_fix' s, eta_fix' t) - | C.Lambda (n,s,t) -> C.Lambda (n, eta_fix' s, eta_fix' t) - | C.LetIn (n,s,t) -> C.LetIn (n, eta_fix' s, eta_fix' t) + | 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 + (n, eta_fix' context s, eta_fix' ((Some (n,(C.Decl s)))::context) t) + | C.Lambda (n,s,t) -> + C.Lambda + (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,None))))::context) t) | C.Appl l as appl -> - let l' = List.map eta_fix' l + 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' 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' 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' 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) -> - C.MutCase (uri, tyno, eta_fix' outty, - eta_fix' term, List.map eta_fix' patterns) + | 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 = + 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 + ) in + let (_,_,_,constructors) = List.nth inductive_types tyno in + let constructor_types = + let rec clean_up t = + function + [] -> t + | a::tl -> + (match t with + Cic.Prod (_,_,t') -> clean_up (S.subst a t') tl + | _ -> assert false) in + if noparams = 0 then + List.map (fun (_,t) -> t) constructors + else + let term_type,_ = + CicTypeChecker.type_of_aux' metasenv context term + CicUniv.empty_ugraph + in + (match term_type with + C.Appl (hd::params) -> + 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 + 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 C.Fix (funno, List.map (fun (name, no, ty, bo) -> - (name, no, eta_fix' ty, eta_fix' bo)) funs) + (name, no, eta_fix' context ty, eta_fix' (fun_types@context) bo)) + funs) | C.CoFix (funno, funs) -> + let fun_types = + List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) funs in C.CoFix (funno, List.map (fun (name, ty, bo) -> - (name, eta_fix' ty, eta_fix' bo)) funs) - in - eta_fix' t + (name, eta_fix' context ty, eta_fix' (fun_types@context) bo)) funs) + 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 ;; - - -