From: Claudio Sacerdoti Coen Date: Fri, 10 Jun 2005 11:06:24 +0000 (+0000) Subject: head_beta_reduce used to create applications of applications. Fixed. X-Git-Tag: PRE_STORAGE~87 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=33cb5e3b6c50933f3af870ab66616e034638719d;p=helm.git head_beta_reduce used to create applications of applications. Fixed. head_beta_reduce renamed to beta_reduce (since it performs full beta reduction). --- diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml index 6bfced57e..7f09da689 100644 --- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml +++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml @@ -105,64 +105,64 @@ let rec does_not_occur n = ) fl true ;; -(*CSC: potrebbe creare applicazioni di applicazioni *) -(*CSC: ora non e' piu' head, ma completa!!! *) -let rec head_beta_reduce = +let rec beta_reduce = let module S = CicSubstitution in let module C = Cic in function C.Rel _ as t -> t | C.Var (uri,exp_named_subst) -> let exp_named_subst' = - List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst + List.map (function (i,t) -> i, beta_reduce t) exp_named_subst in C.Var (uri,exp_named_subst) | C.Meta (n,l) -> C.Meta (n, List.map - (function None -> None | Some t -> Some (head_beta_reduce t)) l + (function None -> None | Some t -> Some (beta_reduce t)) l ) | C.Sort _ as t -> t | C.Implicit _ -> assert false | C.Cast (te,ty) -> - C.Cast (head_beta_reduce te, head_beta_reduce ty) + C.Cast (beta_reduce te, beta_reduce ty) | C.Prod (n,s,t) -> - C.Prod (n, head_beta_reduce s, head_beta_reduce t) + C.Prod (n, beta_reduce s, beta_reduce t) | C.Lambda (n,s,t) -> - C.Lambda (n, head_beta_reduce s, head_beta_reduce t) + C.Lambda (n, beta_reduce s, beta_reduce t) | C.LetIn (n,s,t) -> - C.LetIn (n, head_beta_reduce s, head_beta_reduce t) + C.LetIn (n, beta_reduce s, beta_reduce t) | C.Appl ((C.Lambda (name,s,t))::he::tl) -> let he' = S.subst he t in if tl = [] then - head_beta_reduce he' + beta_reduce he' else - head_beta_reduce (C.Appl (he'::tl)) + (match he' with + C.Appl l -> beta_reduce (C.Appl (l@tl)) + | _ -> beta_reduce (C.Appl (he'::tl))) | C.Appl l -> - C.Appl (List.map head_beta_reduce l) + C.Appl (List.map beta_reduce l) | C.Const (uri,exp_named_subst) -> let exp_named_subst' = - List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst + List.map (function (i,t) -> i, beta_reduce t) exp_named_subst in C.Const (uri,exp_named_subst') | C.MutInd (uri,i,exp_named_subst) -> let exp_named_subst' = - List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst + List.map (function (i,t) -> i, beta_reduce t) exp_named_subst in C.MutInd (uri,i,exp_named_subst') | C.MutConstruct (uri,i,j,exp_named_subst) -> let exp_named_subst' = - List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst + List.map (function (i,t) -> i, beta_reduce t) exp_named_subst in C.MutConstruct (uri,i,j,exp_named_subst') | C.MutCase (sp,i,outt,t,pl) -> - C.MutCase (sp,i,head_beta_reduce outt,head_beta_reduce t, - List.map head_beta_reduce pl) + C.MutCase (sp,i,beta_reduce outt,beta_reduce t, + List.map beta_reduce pl) | C.Fix (i,fl) -> let fl' = List.map (function (name,i,ty,bo) -> - name,i,head_beta_reduce ty,head_beta_reduce bo + name,i,beta_reduce ty,beta_reduce bo ) fl in C.Fix (i,fl') @@ -170,7 +170,7 @@ let rec head_beta_reduce = let fl' = List.map (function (name,ty,bo) -> - name,head_beta_reduce ty,head_beta_reduce bo + name,beta_reduce ty,beta_reduce bo ) fl in C.CoFix (i,fl') @@ -405,7 +405,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = | C.Implicit _ -> raise (Impossible 21) | C.Cast (te,ty) -> (* Let's visit all the subterms that will not be visited later *) - let _ = type_of_aux context te (Some (head_beta_reduce ty)) in + let _ = type_of_aux context te (Some (beta_reduce ty)) in let _ = type_of_aux context ty None in (* Checks suppressed *) ty @@ -423,7 +423,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = let ty = match R.whd context expectedty' with C.Prod (_,_,expected_target_type) -> - head_beta_reduce expected_target_type + beta_reduce expected_target_type | _ -> assert false in Some ty @@ -453,7 +453,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = let expected_hetype = (* Inefficient, the head is computed twice. But I know *) (* of no other solution. *) - (head_beta_reduce + (beta_reduce (R.whd context (xxx_type_of_aux' metasenv context he))) in let hetype = type_of_aux context he (Some expected_hetype) in @@ -462,7 +462,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = function _,[] -> [] | C.Prod (n,s,t),he::tl -> - (he, type_of_aux context he (Some (head_beta_reduce s))):: + (he, type_of_aux context he (Some (beta_reduce s))):: (aux (R.whd context (S.subst he t), tl)) | _ -> assert false in @@ -473,7 +473,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = function _,[] -> [] | C.Prod (n,s,t),he::tl -> - (he, type_of_aux context he (Some (head_beta_reduce s))):: + (he, type_of_aux context he (Some (beta_reduce s))):: (aux (R.whd context (S.subst he t), tl)) | _ -> assert false in @@ -521,7 +521,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = in match R.whd context (type_of_aux context term - (Some (head_beta_reduce type_of_term))) + (Some (beta_reduce type_of_term))) with (*CSC manca il caso dei CAST *) C.MutInd (uri',i',exp_named_subst) -> @@ -562,7 +562,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = (xxx_type_of_aux' metasenv context cons) in ignore (type_of_aux context p - (Some (head_beta_reduce expectedtype))) ; + (Some (beta_reduce expectedtype))) ; j+1 ) 1 (List.combine pl cl) in @@ -588,7 +588,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = List.iter (fun (_,_,ty,bo) -> let expectedty = - head_beta_reduce (CicSubstitution.lift (List.length fl) ty) + beta_reduce (CicSubstitution.lift (List.length fl) ty) in ignore (type_of_aux context' bo (Some expectedty)) ) fl @@ -612,7 +612,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = List.iter (fun (_,ty,bo) -> let expectedty = - head_beta_reduce (CicSubstitution.lift (List.length fl) ty) + beta_reduce (CicSubstitution.lift (List.length fl) ty) in ignore (type_of_aux context' bo (Some expectedty)) ) fl @@ -621,7 +621,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = let (_,ty,_) = List.nth fl i in ty in - let synthesized' = head_beta_reduce synthesized in + let synthesized' = beta_reduce synthesized in let types,res = match expectedty with None ->