From 8ed18544e1591dd3068e2d9095b05d0c4349209c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 4 Jun 2009 18:35:24 +0000 Subject: [PATCH] - doubleTypeInference: we check for unreferenced letins in the inferred type also after beta-reduction because beta-reduction can cause unreferenced letins - procedural: bugfix in the use of inner types, the expected type was sometimes used in place of the inferred type; context cleaning is now disabled because the clear tactics are not generated; debugging mode is now activated nat/ord.ma is now fully reconstructed :) --- .../components/acic_procedural/procedural2.ml | 46 +++++++++------- .../acic_procedural/proceduralConversion.ml | 36 ++++++------- .../acic_procedural/proceduralConversion.mli | 4 +- .../acic_procedural/proceduralOptimizer.ml | 2 +- .../cic_acic/doubleTypeInference.ml | 53 +++++++++++-------- .../components/syntax_extensions/.depend | 3 -- 6 files changed, 79 insertions(+), 65 deletions(-) diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml index 777ccd5f5..06fc9b358 100644 --- a/helm/software/components/acic_procedural/procedural2.ml +++ b/helm/software/components/acic_procedural/procedural2.ml @@ -57,7 +57,7 @@ type status = { case : int list } -let debug = ref false +let debug = ref true (* helpers ******************************************************************) @@ -135,8 +135,8 @@ let get_inner_types st v = try let id = Ut.id_of_annterm v in try match Hashtbl.find st.types id with - | {A.annsynthesized = st; A.annexpected = Some et} -> Some (st, et) - | {A.annsynthesized = st; A.annexpected = None} -> Some (st, st) + | {A.annsynthesized = ity; A.annexpected = Some ety} -> Some (ity, ety) + | {A.annsynthesized = ity; A.annexpected = None} -> Some (ity, ity) with Not_found -> None with Invalid_argument _ -> failwith "P2.get_inner_types" @@ -289,15 +289,20 @@ let mk_fwd_rewrite st dtext name tl direction v t ity ety = end | _ -> assert false -let mk_rewrite st dtext where qs tl direction t ety = +let mk_rewrite st dtext where qs tl direction t ity = + let ppterm t = + let a = ref "" in Ut.pp_term (fun s -> a := !a ^ s) [] st.context t; !a + in assert (List.length tl = 5); let predicate = List.nth tl 2 in - let e = Cn.mk_pattern 1 ety predicate in + let dtext = if !debug then dtext ^ ppterm (H.cic predicate) else dtext in + let e = Cn.mk_pattern 1 ity predicate in let script = [T.Branch (qs, "")] in if (Cn.does_not_occur e) then script else T.Rewrite (direction, where, None, e, dtext) :: script let rec proc_lambda st what name v t = + let dtext = if !debug then CicPp.ppcontext st.context else "" in let name = match name with | C.Anonymous -> H.mk_fresh_name true st.context anonymous_premise | name -> name @@ -305,7 +310,7 @@ let rec proc_lambda st what name v t = let entry = Some (name, C.Decl (H.cic v)) in let intro = get_intro name in let script = proc_proof (add st entry) t in - let script = T.Intros (Some 1, [intro], "") :: script in + let script = T.Intros (Some 1, [intro], dtext) :: script in mk_preamble st what script and proc_letin st what name v w t = @@ -367,9 +372,9 @@ and proc_appl st what hd tl = in let classes, rc = Cl.classify st.context ty in let goal_arity, goal = match get_inner_types st what with - | None -> 0, None - | Some (ity, ety) -> - snd (PEH.split_with_whd (st.context, H.cic ity)), Some (H.cic ety) + | None -> 0, None + | Some (ity, _) -> + snd (PEH.split_with_whd (st.context, H.cic ity)), Some (H.cic ity) in let parsno, argsno = List.length classes, List.length tl in let decurry = parsno - argsno in @@ -397,8 +402,8 @@ and proc_appl st what hd tl = let synth2 = I.S.add 1 synth in let names = H.get_ind_names uri tyno in let qs = proc_bkd_proofs (next st) synth2 names classes2 tl2 in - let ety = match get_inner_types st what with - | Some (_, ety) -> ety + let ity = match get_inner_types st what with + | Some (ity, _) -> ity | None -> Cn.fake_annotate "" st.context (get_type "TC3" st what) in @@ -407,12 +412,12 @@ and proc_appl st what hd tl = let b, hd, qs = mk_exp_args hd tl classes synth qs in script @ [tactic b hd (dtext ^ text); T.Branch (qs, "")] else if is_rewrite_right st hd then - script2 @ mk_rewrite st dtext where qs tl2 false what ety + script2 @ mk_rewrite st dtext where qs tl2 false what ity else if is_rewrite_left st hd then - script2 @ mk_rewrite st dtext where qs tl2 true what ety + script2 @ mk_rewrite st dtext where qs tl2 true what ity else let predicate = List.nth tl2 (parsno - i) in - let e = Cn.mk_pattern j ety predicate in + let e = Cn.mk_pattern j ity predicate in let using = Some hd in script2 @ [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")] @@ -436,12 +441,12 @@ and proc_case st what uri tyno u v ts = let ps, _ = H.get_ind_parameters st.context (H.cic v) in let _, rps = HEL.split_nth lpsno ps in let rpsno = List.length rps in - let ety = match get_inner_types st what with - | Some (_, ety) -> ety + let ity = match get_inner_types st what with + | Some (ity, _) -> ity | None -> Cn.fake_annotate "" st.context (get_type "TC4" st what) in - let e = Cn.mk_pattern rpsno ety u in + let e = Cn.mk_pattern rpsno ity u in let text = "" in let script = List.rev (mk_arg st v) in script @ [T.Cases (v, e, dtext ^ text); T.Branch (qs, "")] @@ -458,14 +463,17 @@ and proc_other st what = and proc_proof st t = let f st = +(* let xtypes, note = match get_inner_types st t with | Some (it, et) -> Some (H.cic it, H.cic et), (Printf.sprintf "\nInferred: %s\nExpected: %s" (Pp.ppterm (H.cic it)) (Pp.ppterm (H.cic et))) | None -> None, "\nNo types" - in - let context, _clears = Cn.get_clears st.context (H.cic t) xtypes in + in + let context, clears = Cn.get_clears st.context (H.cic t) xtypes in {st with context = context} +*) + st in match t with | C.ALambda (_, name, w, t) as what -> proc_lambda (f st) what name w t diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml index f6dd83be3..65d5f1edf 100644 --- a/helm/software/components/acic_procedural/proceduralConversion.ml +++ b/helm/software/components/acic_procedural/proceduralConversion.ml @@ -195,29 +195,29 @@ let generalize n = in gen_term -let convert g ety k predicate = +let convert g ity k predicate = let rec aux = function - | C.ALambda (_, _, b, ety), C.ALambda (id, n, u, pred) -> - C.ALambda (id, n, aux (b, u), aux (ety, pred)) - | C.AProd (_, _, b, ety), C.AProd (id, n, u, pred) -> - C.AProd (id, n, aux (b, u), aux (ety, pred)) - | C.ALetIn (_, _, a, b, ety), C.ALetIn (id, n, v, u, pred) -> - C.ALetIn (id, n, aux (a, v), aux (b, u), aux (ety, pred)) + | C.ALambda (_, _, b, ity), C.ALambda (id, n, u, pred) -> + C.ALambda (id, n, aux (b, u), aux (ity, pred)) + | C.AProd (_, _, b, ity), C.AProd (id, n, u, pred) -> + C.AProd (id, n, aux (b, u), aux (ity, pred)) + | C.ALetIn (_, _, a, b, ity), C.ALetIn (id, n, v, u, pred) -> + C.ALetIn (id, n, aux (a, v), aux (b, u), aux (ity, pred)) | C.AAppl (_, bs), C.AAppl (id, us) when List.length bs = List.length us -> let map b u = aux (b,u) in C.AAppl (id, List.map2 map bs us) - | C.ACast (_, ety, b), C.ACast (id, pred, u) -> - C.ACast (id, aux (ety, pred), aux (b, u)) - | ety, C.AAppl (_, C.ALambda (_, _, _, pred) :: v :: []) -> - aux (ety, subst 1 v pred) - | ety, C.AAppl (id, C.ALambda (_, _, _, pred) :: v :: vs) -> - aux (ety, C.AAppl (id, subst 1 v pred :: vs)) + | C.ACast (_, ity, b), C.ACast (id, pred, u) -> + C.ACast (id, aux (ity, pred), aux (b, u)) + | ity, C.AAppl (_, C.ALambda (_, _, _, pred) :: v :: []) -> + aux (ity, subst 1 v pred) + | ity, C.AAppl (id, C.ALambda (_, _, _, pred) :: v :: vs) -> + aux (ity, C.AAppl (id, subst 1 v pred :: vs)) | _, pred -> pred in - g k (aux (ety, predicate)) + g k (aux (ity, predicate)) -let mk_pattern psno ety predicate = - clear_absts (convert (generalize psno) ety) psno 0 predicate +let mk_pattern psno ity predicate = + clear_absts (convert (generalize psno) ity) psno 0 predicate let get_clears c p xtypes = let meta = C.Implicit None in @@ -270,7 +270,7 @@ let clear c hyp = | entry :: tail -> aux (entry :: c) tail in aux [] c - +(* let elim_inferred_type context goal arg using cpattern = let metasenv, ugraph = [], Un.default_ugraph in let ety = H.get_type "elim_inferred_type" context using in @@ -282,7 +282,7 @@ let elim_inferred_type context goal arg using cpattern = let ty = C.Appl (predicate :: actual_args) in let upto = List.length actual_args in Rd.head_beta_reduce ~delta:false ~upto ty - +*) let does_not_occur = function | C.AImplicit (_, None) -> true | _ -> false diff --git a/helm/software/components/acic_procedural/proceduralConversion.mli b/helm/software/components/acic_procedural/proceduralConversion.mli index 210813331..2e556511b 100644 --- a/helm/software/components/acic_procedural/proceduralConversion.mli +++ b/helm/software/components/acic_procedural/proceduralConversion.mli @@ -38,8 +38,8 @@ val get_clears: Cic.context * string list val clear: Cic.context -> string -> Cic.context - +(* val elim_inferred_type: Cic.context -> Cic.term -> Cic.term -> Cic.term -> Cic.term -> Cic.term - +*) val does_not_occur: Cic.annterm -> bool diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml index c5a27efc4..2faade402 100644 --- a/helm/software/components/acic_procedural/proceduralOptimizer.ml +++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml @@ -42,7 +42,7 @@ module Cl = ProceduralClassify (* debugging ****************************************************************) -let debug = ref false +let debug = ref true (* term optimization ********************************************************) diff --git a/helm/software/components/cic_acic/doubleTypeInference.ml b/helm/software/components/cic_acic/doubleTypeInference.ml index 7f93716b2..c60bf90f4 100644 --- a/helm/software/components/cic_acic/doubleTypeInference.ml +++ b/helm/software/components/cic_acic/doubleTypeInference.ml @@ -97,64 +97,72 @@ let rec does_not_occur n = ) fl true ;; -let rec beta_reduce = +(* FG: if ~clean:true, unreferenced letins are removed *) +(* (beta-reducttion can cause unreferenced letins) *) +let rec beta_reduce ?(clean=false)= 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, beta_reduce t) exp_named_subst + List.map (function (i,t) -> i, beta_reduce ~clean 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 (beta_reduce t)) l + (function None -> None | Some t -> Some (beta_reduce ~clean t)) l ) | C.Sort _ as t -> t | C.Implicit _ -> assert false | C.Cast (te,ty) -> - C.Cast (beta_reduce te, beta_reduce ty) + C.Cast (beta_reduce ~clean te, beta_reduce ~clean ty) | C.Prod (n,s,t) -> - C.Prod (n, beta_reduce s, beta_reduce t) + C.Prod (n, beta_reduce ~clean s, beta_reduce ~clean t) | C.Lambda (n,s,t) -> - C.Lambda (n, beta_reduce s, beta_reduce t) + C.Lambda (n, beta_reduce ~clean s, beta_reduce ~clean t) | C.LetIn (n,s,ty,t) -> - C.LetIn (n, beta_reduce s, beta_reduce ty, beta_reduce t) + let t' = beta_reduce ~clean t in + if clean && does_not_occur 1 t' then + (* since [Rel 1] does not occur in typ, substituting any term *) + (* in place of [Rel 1] is equivalent to delifting once *) + CicSubstitution.subst (C.Implicit None) t' + else + C.LetIn (n, beta_reduce ~clean s, beta_reduce ~clean ty, t') | C.Appl ((C.Lambda (name,s,t))::he::tl) -> let he' = S.subst he t in if tl = [] then - beta_reduce he' + beta_reduce ~clean he' else (match he' with - C.Appl l -> beta_reduce (C.Appl (l@tl)) - | _ -> beta_reduce (C.Appl (he'::tl))) + C.Appl l -> beta_reduce ~clean (C.Appl (l@tl)) + | _ -> beta_reduce ~clean (C.Appl (he'::tl))) | C.Appl l -> - C.Appl (List.map beta_reduce l) + C.Appl (List.map (beta_reduce ~clean) l) | C.Const (uri,exp_named_subst) -> let exp_named_subst' = - List.map (function (i,t) -> i, beta_reduce t) exp_named_subst + List.map (function (i,t) -> i, beta_reduce ~clean 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, beta_reduce t) exp_named_subst + List.map (function (i,t) -> i, beta_reduce ~clean 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, beta_reduce t) exp_named_subst + List.map (function (i,t) -> i, beta_reduce ~clean t) exp_named_subst in C.MutConstruct (uri,i,j,exp_named_subst') | C.MutCase (sp,i,outt,t,pl) -> - C.MutCase (sp,i,beta_reduce outt,beta_reduce t, - List.map beta_reduce pl) + C.MutCase (sp,i,beta_reduce ~clean outt,beta_reduce ~clean t, + List.map (beta_reduce ~clean) pl) | C.Fix (i,fl) -> let fl' = List.map (function (name,i,ty,bo) -> - name,i,beta_reduce ty,beta_reduce bo + name,i,beta_reduce ~clean ty,beta_reduce ~clean bo ) fl in C.Fix (i,fl') @@ -162,7 +170,7 @@ let rec beta_reduce = let fl' = List.map (function (name,ty,bo) -> - name,beta_reduce ty,beta_reduce bo + name,beta_reduce ~clean ty,beta_reduce ~clean bo ) fl in C.CoFix (i,fl') @@ -367,10 +375,10 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = (* Checks suppressed *) type_of_aux ((Some (n,(C.Def (s,ty))))::context) t None in (* CicSubstitution.subst s t_typ *) - if does_not_occur 1 t_typ then - (* since [Rel 1] does not occur in typ, substituting any term *) + if does_not_occur 1 t_typ then + (* since [Rel 1] does not occur in typ, substituting any term *) (* in place of [Rel 1] is equivalent to delifting once *) - CicSubstitution.subst (C.Implicit None) t_typ + CicSubstitution.subst (C.Implicit None) t_typ) else C.LetIn (n,s,ty,t_typ) | C.Appl (he::tl) when List.length tl > 0 -> @@ -551,7 +559,8 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = let (_,ty,_) = List.nth fl i in ty in - let synthesized' = beta_reduce synthesized in +(* FG: beta-reduction can cause unreferenced letins *) + let synthesized' = beta_reduce ~clean:true synthesized in let synthesized' = !pack_coercion metasenv context synthesized' in let types,res = match expectedty with diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend index 25e67131f..f3c6a8bd1 100644 --- a/helm/software/components/syntax_extensions/.depend +++ b/helm/software/components/syntax_extensions/.depend @@ -1,5 +1,2 @@ -utf8Macro.cmi: -utf8MacroTable.cmo: -utf8MacroTable.cmx: utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi -- 2.39.2