X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReduction.ml;h=aaca61942aa323467bfb0d29a4914f3405681005;hb=e6b28085c97ae7b9bd3f3262b105f6b84f42b047;hp=687a46549a5455f2253b085c4f83b49a552fd55d;hpb=0575a1cb077087970f311b48f2e45dc4a01a6867;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml index 687a46549..aaca61942 100644 --- a/helm/ocaml/cic_proof_checking/cicReduction.ml +++ b/helm/ocaml/cic_proof_checking/cicReduction.ml @@ -33,6 +33,8 @@ exception ReferenceToVariable;; exception ReferenceToCurrentProof;; exception ReferenceToInductiveDefinition;; +let debug_print = fun _ -> () + let fdebug = ref 1;; let debug t env s = let rec debug_aux t i = @@ -41,7 +43,7 @@ let debug t env s = CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i in if !fdebug = 0 then - prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "") + debug_print (s ^ "\n" ^ List.fold_right debug_aux (t::env) "") ;; module type Strategy = @@ -347,15 +349,15 @@ module Reduction(RS : Strategy) = ) | C.Var (uri,exp_named_subst) -> (* -prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens)) ; +debug_print ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens)) ; *) if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then CicSubstitution.lift m (RS.from_ens (List.assq uri ens)) else let params = - let o,_ = - CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri - in + let o,_ = + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri + in (match o with C.Constant _ -> raise ReferenceToConstant | C.Variable (_,_,_,params,_) -> params @@ -385,9 +387,9 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) - | C.Appl l -> C.Appl (List.map (unwind_aux m) l) | C.Const (uri,exp_named_subst) -> let params = - let o,_ = - CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri - in + let o,_ = + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri + in (match o with C.Constant (_,_,_,params,_) -> params | C.Variable _ -> raise ReferenceToVariable @@ -401,9 +403,9 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) - C.Const (uri,exp_named_subst') | C.MutInd (uri,i,exp_named_subst) -> let params = - let o,_ = - CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri - in + let o,_ = + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri + in (match o with C.Constant _ -> raise ReferenceToConstant | C.Variable _ -> raise ReferenceToVariable @@ -417,9 +419,9 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) - C.MutInd (uri,i,exp_named_subst') | C.MutConstruct (uri,i,j,exp_named_subst) -> let params = - let o,_ = - CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri - in + let o,_ = + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri + in (match o with C.Constant _ -> raise ReferenceToConstant | C.Variable _ -> raise ReferenceToVariable @@ -493,10 +495,11 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) - | _::tl -> filter_and_lift already_instantiated tl (* | (uri,_)::tl -> -prerr_endline ("---- SKIPPO " ^ UriManager.string_of_uri uri) ; -if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst' then prerr_endline "---- OK1" ; -prerr_endline ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ; -if List.mem uri params then prerr_endline "---- OK2" ; +debug_print ("---- SKIPPO " ^ UriManager.string_of_uri uri) ; +if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) +exp_named_subst' then debug_print "---- OK1" ; +debug_print ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ; +if List.mem uri params then debug_print "---- OK2" ; filter_and_lift tl *) in @@ -510,7 +513,7 @@ if List.mem uri params then prerr_endline "---- OK2" ; unwind' 0 ;; - let reduce ?(subst = []) context : config -> Cic.term = + let reduce ~delta ?(subst = []) context : config -> Cic.term = let module C = Cic in let module S = CicSubstitution in let rec reduce = @@ -543,8 +546,8 @@ if List.mem uri params then prerr_endline "---- OK2" ; reduce (0, [], [], RS.from_ens (List.assq uri ens), s) else ( let o,_ = - CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri - in + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri + in match o with C.Constant _ -> raise ReferenceToConstant | C.CurrentProof _ -> raise ReferenceToCurrentProof @@ -559,9 +562,9 @@ if List.mem uri params then prerr_endline "---- OK2" ; ) | (k, e, ens, (C.Meta (n,l) as t), s) -> (try - let (_, term,_) = CicUtil.lookup_subst n subst in + let (_, term,_) = CicUtil.lookup_subst n subst in reduce (k, e, ens,CicSubstitution.subst_meta l term,s) - with CicUtil.Subst_not_found _ -> + with CicUtil.Subst_not_found _ -> let t' = unwind k e ens t in if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))) | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *) @@ -599,11 +602,14 @@ if List.mem uri params then prerr_endline "---- OK2" ; | (k, e, ens, C.Appl l, s) -> C.Appl (List.append (List.map (unwind k e ens) l) s) *) + | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) when delta=false-> + let t' = unwind k e ens t in + if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)) | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) -> (let o,_ = - CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri - in - match o with + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri + in + match o with C.Constant (_,Some body,_,_,_) -> let ens' = push_exp_named_subst k e ens exp_named_subst in (* constants are closed *) @@ -658,13 +664,13 @@ if List.mem uri params then prerr_endline "---- OK2" ; reduce (k, e, ens, (List.nth pl (j-1)), s) | C.Appl (C.MutConstruct (_,_,j,_) :: tl) -> let (arity, r) = - let o,_ = - CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind - in - match o with + let o,_ = + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind + in + match o with C.InductiveDefinition (tl,ingredients,r,_) -> - let (_,_,arity,_) = List.nth tl i in - (arity,r) + let (_,_,arity,_) = List.nth tl i in + (arity,r) | _ -> raise WrongUriToInductiveDefinition in let ts = @@ -679,7 +685,7 @@ if List.mem uri params then prerr_endline "---- OK2" ; in (* ts are already unwinded because they are a sublist of tl *) reduce (k, e, ens, (List.nth pl (j-1)), (RS.to_stack_list ts)@s) - | C.Cast _ | C.Implicit _ -> + | C.Cast _ | C.Implicit _ -> raise (Impossible 2) (* we don't trust our whd ;-) *) | _ -> let t' = unwind k e ens t in @@ -715,7 +721,7 @@ if List.mem uri params then prerr_endline "---- OK2" ; (name,recindex,unwind k e ens typ, unwind' leng k e ens body) in - List.map unwind_fl fl + List.map unwind_fl fl in let new_env = let counter = ref 0 in @@ -754,13 +760,13 @@ if List.mem uri params then prerr_endline "---- OK2" ; try reduce context (0, [], [], t, []) with Not_found -> - prerr_endline (CicPp.ppterm t) ; + debug_print (CicPp.ppterm t) ; raise Not_found ;; *) - let rec whd ?(subst=[]) context t = - reduce ~subst context (0, [], [], t, []) + let rec whd ?(delta=true) ?(subst=[]) context t = + reduce ~delta ~subst context (0, [], [], t, []) ;; @@ -770,11 +776,11 @@ let whd context t = let rescsc = CicReductionNaif.whd context t in if not (CicReductionNaif.are_convertible context res rescsc) then begin - prerr_endline ("PRIMA: " ^ CicPp.ppterm t) ; + debug_print ("PRIMA: " ^ CicPp.ppterm t) ; flush stderr ; - prerr_endline ("DOPO: " ^ CicPp.ppterm res) ; + debug_print ("DOPO: " ^ CicPp.ppterm res) ; flush stderr ; - prerr_endline ("CSC: " ^ CicPp.ppterm rescsc) ; + debug_print ("CSC: " ^ CicPp.ppterm rescsc) ; flush stderr ; CicReductionNaif.fdebug := 0 ; let _ = CicReductionNaif.are_convertible context res rescsc in @@ -835,142 +841,142 @@ let are_convertible ?(subst=[]) ?(metasenv=[]) = with Invalid_argument _ -> false,ugraph ) - else - false,ugraph + else + false,ugraph | (C.Meta (n1,l1), C.Meta (n2,l2)) -> - if n1 = n2 then - let b2, ugraph1 = - let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in - let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in - List.fold_left2 - (fun (b,ugraph) t1 t2 -> - if b then - match t1,t2 with - None,_ - | _,None -> true,ugraph - | Some t1',Some t2' -> - aux test_equality_only context t1' t2' ugraph - else - false,ugraph - ) (true,ugraph) l1 l2 - in - if b2 then true,ugraph1 else false,ugraph - else - false,ugraph + if n1 = n2 then + let b2, ugraph1 = + let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in + let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in + List.fold_left2 + (fun (b,ugraph) t1 t2 -> + if b then + match t1,t2 with + None,_ + | _,None -> true,ugraph + | Some t1',Some t2' -> + aux test_equality_only context t1' t2' ugraph + else + false,ugraph + ) (true,ugraph) l1 l2 + in + if b2 then true,ugraph1 else false,ugraph + else + false,ugraph + (* TASSI: CONSTRAINTS *) + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only -> + true,(CicUniv.add_eq t2 t1 ugraph) + (* TASSI: CONSTRAINTS *) + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> + true,(CicUniv.add_ge t2 t1 ugraph) + (* TASSI: CONSTRAINTS *) + | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph (* TASSI: CONSTRAINTS *) - | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only -> - true,(CicUniv.add_eq t2 t1 ugraph) - (* TASSI: CONSTRAINTS *) - | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> - true,(CicUniv.add_ge t2 t1 ugraph) - (* TASSI: CONSTRAINTS *) - | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph - (* TASSI: CONSTRAINTS *) | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> - let b',ugraph' = aux true context s1 s2 ugraph in - if b' then + let b',ugraph' = aux true context s1 s2 ugraph in + if b' then aux test_equality_only ((Some (name1, (C.Decl s1)))::context) - t1 t2 ugraph' - else - false,ugraph + t1 t2 ugraph' + else + false,ugraph | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) -> let b',ugraph' = aux test_equality_only context s1 s2 ugraph in if b' then - aux test_equality_only ((Some (name1, (C.Decl s1)))::context) - t1 t2 ugraph' - else - false,ugraph + aux test_equality_only ((Some (name1, (C.Decl s1)))::context) + t1 t2 ugraph' + else + false,ugraph | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) -> let b',ugraph' = aux test_equality_only context s1 s2 ugraph in - if b' then + if b' then aux test_equality_only ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph' - else - false,ugraph + else + false,ugraph | (C.Appl l1, C.Appl l2) -> (try List.fold_right2 (fun x y (b,ugraph) -> - if b then - aux test_equality_only context x y ugraph - else - false,ugraph) l1 l2 (true,ugraph) + if b then + aux test_equality_only context x y ugraph + else + false,ugraph) l1 l2 (true,ugraph) with Invalid_argument _ -> false,ugraph ) | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) -> let b' = U.eq uri1 uri2 in - if b' then + if b' then (try List.fold_right2 (fun (uri1,x) (uri2,y) (b,ugraph) -> - if b && U.eq uri1 uri2 then - aux test_equality_only context x y ugraph - else - false,ugraph + if b && U.eq uri1 uri2 then + aux test_equality_only context x y ugraph + else + false,ugraph ) exp_named_subst1 exp_named_subst2 (true,ugraph) with Invalid_argument _ -> false,ugraph ) - else - false,ugraph + else + false,ugraph | (C.MutInd (uri1,i1,exp_named_subst1), C.MutInd (uri2,i2,exp_named_subst2) ) -> let b' = U.eq uri1 uri2 && i1 = i2 in - if b' then + if b' then (try List.fold_right2 (fun (uri1,x) (uri2,y) (b,ugraph) -> if b && U.eq uri1 uri2 then - aux test_equality_only context x y ugraph - else - false,ugraph + aux test_equality_only context x y ugraph + else + false,ugraph ) exp_named_subst1 exp_named_subst2 (true,ugraph) with Invalid_argument _ -> false,ugraph ) - else - false,ugraph + else + false,ugraph | (C.MutConstruct (uri1,i1,j1,exp_named_subst1), C.MutConstruct (uri2,i2,j2,exp_named_subst2) ) -> let b' = U.eq uri1 uri2 && i1 = i2 && j1 = j2 in - if b' then + if b' then (try List.fold_right2 (fun (uri1,x) (uri2,y) (b,ugraph) -> - if b && U.eq uri1 uri2 then - aux test_equality_only context x y ugraph - else - false,ugraph + if b && U.eq uri1 uri2 then + aux test_equality_only context x y ugraph + else + false,ugraph ) exp_named_subst1 exp_named_subst2 (true,ugraph) with Invalid_argument _ -> false,ugraph ) - else - false,ugraph + else + false,ugraph | (C.MutCase (uri1,i1,outtype1,term1,pl1), C.MutCase (uri2,i2,outtype2,term2,pl2)) -> let b' = U.eq uri1 uri2 && i1 = i2 in - if b' then + if b' then let b'',ugraph''=aux test_equality_only context - outtype1 outtype2 ugraph in - if b'' then - let b''',ugraph'''= aux test_equality_only context - term1 term2 ugraph'' in - List.fold_right2 - (fun x y (b,ugraph) -> - if b then - aux test_equality_only context x y ugraph - else - false,ugraph) - pl1 pl2 (true,ugraph''') - else - false,ugraph - else - false,ugraph + outtype1 outtype2 ugraph in + if b'' then + let b''',ugraph'''= aux test_equality_only context + term1 term2 ugraph'' in + List.fold_right2 + (fun x y (b,ugraph) -> + if b then + aux test_equality_only context x y ugraph + else + false,ugraph) + pl1 pl2 (b''',ugraph''') + else + false,ugraph + else + false,ugraph | (C.Fix (i1,fl1), C.Fix (i2,fl2)) -> let tys = List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1 @@ -979,17 +985,17 @@ let are_convertible ?(subst=[]) ?(metasenv=[]) = List.fold_right2 (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) (b,ugraph) -> if b && recindex1 = recindex2 then - let b',ugraph' = aux test_equality_only context ty1 ty2 - ugraph in - if b' then - aux test_equality_only (tys@context) bo1 bo2 ugraph' - else - false,ugraph - else - false,ugraph) - fl1 fl2 (true,ugraph) - else - false,ugraph + let b',ugraph' = aux test_equality_only context ty1 ty2 + ugraph in + if b' then + aux test_equality_only (tys@context) bo1 bo2 ugraph' + else + false,ugraph + else + false,ugraph) + fl1 fl2 (true,ugraph) + else + false,ugraph | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) -> let tys = List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1 @@ -997,18 +1003,18 @@ let are_convertible ?(subst=[]) ?(metasenv=[]) = if i1 = i2 then List.fold_right2 (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) -> - if b then - let b',ugraph' = aux test_equality_only context ty1 ty2 - ugraph in - if b' then - aux test_equality_only (tys@context) bo1 bo2 ugraph' - else - false,ugraph - else - false,ugraph) - fl1 fl2 (true,ugraph) - else - false,ugraph + if b then + let b',ugraph' = aux test_equality_only context ty1 ty2 + ugraph in + if b' then + aux test_equality_only (tys@context) bo1 bo2 ugraph' + else + false,ugraph + else + false,ugraph) + fl1 fl2 (true,ugraph) + else + false,ugraph | (C.Cast _, _) | (_, C.Cast _) | (C.Implicit _, _) | (_, C.Implicit _) -> assert false @@ -1019,11 +1025,11 @@ let are_convertible ?(subst=[]) ?(metasenv=[]) = debug t1 [t2] "PREWHD"; (* (match t1 with - Cic.Meta _ -> - prerr_endline (CicPp.ppterm t1); - prerr_endline (CicPp.ppterm (whd ~subst context t1)); - prerr_endline (CicPp.ppterm t2); - prerr_endline (CicPp.ppterm (whd ~subst context t2)) + Cic.Meta _ -> + debug_print (CicPp.ppterm t1); + debug_print (CicPp.ppterm (whd ~subst context t1)); + debug_print (CicPp.ppterm t2); + debug_print (CicPp.ppterm (whd ~subst context t2)) | _ -> ()); *) let t1' = whd ~subst context t1 in let t2' = whd ~subst context t2 in @@ -1034,3 +1040,66 @@ let are_convertible ?(subst=[]) ?(metasenv=[]) = aux false (*c t1 t2 ugraph *) ;; + +let rec normalize ?(delta=true) ?(subst=[]) ctx term = + let module C = Cic in + let t = whd ~delta ~subst ctx term in + let aux = normalize ~delta ~subst in + let decl name t = Some (name, C.Decl t) in + let def name t = Some (name, C.Def (t,None)) in + match t with + | C.Rel n -> t + | C.Var (uri,exp_named_subst) -> + C.Var (uri, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst) + | C.Meta (i,l) -> + C.Meta (i,List.map (function Some t -> Some (aux ctx t) | None -> None) l) + | C.Sort _ -> t + | C.Implicit _ -> t + | C.Cast (te,ty) -> C.Cast (aux ctx te, aux ctx ty) + | C.Prod (n,s,t) -> + let s' = aux ctx s in + C.Prod (n, s', aux ((decl n s')::ctx) t) + | C.Lambda (n,s,t) -> + let s' = aux ctx s in + C.Lambda (n, s', aux ((decl n s')::ctx) t) + | C.LetIn (n,s,t) -> + (* the term is already in weak head normal form *) + assert false + | C.Appl (h::l) -> C.Appl (h::(List.map (aux ctx) l)) + | C.Appl [] -> assert false + | C.Const (uri,exp_named_subst) -> + C.Const (uri, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst) + | C.MutInd (uri,typeno,exp_named_subst) -> + C.MutInd (uri,typeno, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst) + | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> + C.MutConstruct (uri, typeno, consno, + List.map (fun (n,t) -> n,aux ctx t) exp_named_subst) + | C.MutCase (sp,i,outt,t,pl) -> + C.MutCase (sp,i, aux ctx outt, aux ctx t, List.map (aux ctx) pl) +(*CSC: to be completed, I suppose *) + | C.Fix _ -> t + | C.CoFix _ -> t + +let normalize ?delta ?subst ctx term = +(* prerr_endline ("NORMALIZE:" ^ CicPp.ppterm term); *) + let t = normalize ?delta ?subst ctx term in +(* prerr_endline ("NORMALIZED:" ^ CicPp.ppterm t); *) + t + + +(* performs an head beta/cast reduction *) +let rec head_beta_reduce = + function + (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) -> + let he'' = CicSubstitution.subst he' t in + if tl' = [] then + he'' + else + let he''' = + match he'' with + Cic.Appl l -> Cic.Appl (l@tl') + | _ -> Cic.Appl (he''::tl') + in + head_beta_reduce he''' + | Cic.Cast (te,_) -> head_beta_reduce te + | t -> t