X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Feta_fixing.ml;h=68dec37d6b04230f1468665e0a6f77516ccdb365;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=d6293d2434ad61af36b7c94203a0cf7b6c8641c7;hpb=c706b1cb2c7cbdd23a3281d35d3f0b10c3a684cf;p=helm.git diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml index d6293d243..68dec37d6 100644 --- a/helm/ocaml/cic_omdoc/eta_fixing.ml +++ b/helm/ocaml/cic_omdoc/eta_fixing.ml @@ -23,9 +23,7 @@ * http://cs.unibo.it/helm/. *) -exception ReferenceToVariable;; -exception RferenceToCurrentProof;; -exception ReferenceToInductiveDefinition;; +exception ReferenceToNonVariable;; let prerr_endline _ = ();; @@ -132,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 @@ -163,7 +165,7 @@ 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 ; *) @@ -172,16 +174,11 @@ let eta_fix metasenv t = 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 @@ -192,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 @@ -207,48 +204,47 @@ let eta_fix metasenv t = 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 - fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l'' - | _ -> 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 @@ -260,11 +256,21 @@ 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 @@ -285,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 ;; - - - - -