From: Ferruccio Guidi Date: Mon, 14 Dec 2009 14:36:44 +0000 (+0000) Subject: the sort hierarchy parameter enter the kernel status X-Git-Tag: make_still_working~3165 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0e6bf0ef18e3879a359b2b6f63d600c20102f0ab;hp=f2771b346a41445df23adb6acccd7ee6b1578666;p=helm.git the sort hierarchy parameter enter the kernel status --- diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index f0d13c9a2..c71e6771b 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -1,9 +1,17 @@ +lib/nUri.cmi: lib/nUri.cmo: lib/nUri.cmi lib/nUri.cmx: lib/nUri.cmi +lib/cps.cmo: +lib/cps.cmx: +lib/share.cmo: +lib/share.cmx: +lib/log.cmi: lib/log.cmo: lib/cps.cmx lib/log.cmi lib/log.cmx: lib/cps.cmx lib/log.cmi lib/time.cmo: lib/log.cmi lib/time.cmx: lib/log.cmx +automath/aut.cmo: +automath/aut.cmx: automath/autProcess.cmi: automath/aut.cmx automath/autProcess.cmo: automath/aut.cmx automath/autProcess.cmi automath/autProcess.cmx: automath/aut.cmx automath/autProcess.cmi @@ -17,12 +25,14 @@ automath/autParser.cmo: automath/aut.cmx automath/autParser.cmi automath/autParser.cmx: automath/aut.cmx automath/autParser.cmi automath/autLexer.cmo: lib/log.cmi automath/autParser.cmi automath/autLexer.cmx: lib/log.cmx automath/autParser.cmx +common/hierarchy.cmi: common/hierarchy.cmo: lib/cps.cmx common/hierarchy.cmi common/hierarchy.cmx: lib/cps.cmx common/hierarchy.cmi +common/output.cmi: common/output.cmo: lib/log.cmi common/output.cmi common/output.cmx: lib/log.cmx common/output.cmi -common/entity.cmo: lib/nUri.cmi automath/aut.cmx -common/entity.cmx: lib/nUri.cmx automath/aut.cmx +common/entity.cmo: lib/nUri.cmi common/hierarchy.cmi automath/aut.cmx +common/entity.cmx: lib/nUri.cmx common/hierarchy.cmx automath/aut.cmx common/library.cmi: common/hierarchy.cmi common/entity.cmx common/library.cmo: lib/nUri.cmi common/hierarchy.cmi common/entity.cmx \ lib/cps.cmx common/library.cmi @@ -54,7 +64,7 @@ basic_ag/bagReduction.cmo: lib/nUri.cmi lib/log.cmi common/entity.cmx \ basic_ag/bagReduction.cmx: lib/nUri.cmx lib/log.cmx common/entity.cmx \ lib/cps.cmx basic_ag/bagSubstitution.cmx basic_ag/bagOutput.cmx \ basic_ag/bagEnvironment.cmx basic_ag/bag.cmx basic_ag/bagReduction.cmi -basic_ag/bagType.cmi: common/hierarchy.cmi basic_ag/bag.cmx +basic_ag/bagType.cmi: common/entity.cmx basic_ag/bag.cmx basic_ag/bagType.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi \ common/hierarchy.cmi common/entity.cmx lib/cps.cmx \ basic_ag/bagReduction.cmi basic_ag/bagOutput.cmi \ @@ -63,7 +73,7 @@ basic_ag/bagType.cmx: lib/share.cmx lib/nUri.cmx lib/log.cmx \ common/hierarchy.cmx common/entity.cmx lib/cps.cmx \ basic_ag/bagReduction.cmx basic_ag/bagOutput.cmx \ basic_ag/bagEnvironment.cmx basic_ag/bag.cmx basic_ag/bagType.cmi -basic_ag/bagUntrusted.cmi: common/hierarchy.cmi basic_ag/bag.cmx +basic_ag/bagUntrusted.cmi: common/entity.cmx basic_ag/bag.cmx basic_ag/bagUntrusted.cmo: lib/nUri.cmi lib/log.cmi common/entity.cmx \ basic_ag/bagType.cmi basic_ag/bagEnvironment.cmi basic_ag/bag.cmx \ basic_ag/bagUntrusted.cmi @@ -94,8 +104,8 @@ basic_rg/brgReduction.cmo: lib/share.cmx common/output.cmi lib/nUri.cmi \ basic_rg/brgReduction.cmx: lib/share.cmx common/output.cmx lib/nUri.cmx \ lib/log.cmx common/entity.cmx lib/cps.cmx basic_rg/brgOutput.cmx \ basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgReduction.cmi -basic_rg/brgType.cmi: lib/log.cmi common/hierarchy.cmi common/entity.cmx \ - basic_rg/brgReduction.cmi basic_rg/brg.cmx +basic_rg/brgType.cmi: lib/log.cmi common/entity.cmx basic_rg/brgReduction.cmi \ + basic_rg/brg.cmx basic_rg/brgType.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi \ common/hierarchy.cmi common/entity.cmx lib/cps.cmx \ basic_rg/brgSubstitution.cmi basic_rg/brgReduction.cmi \ @@ -106,7 +116,7 @@ basic_rg/brgType.cmx: lib/share.cmx lib/nUri.cmx lib/log.cmx \ basic_rg/brgSubstitution.cmx basic_rg/brgReduction.cmx \ basic_rg/brgOutput.cmx basic_rg/brgEnvironment.cmx basic_rg/brg.cmx \ basic_rg/brgType.cmi -basic_rg/brgUntrusted.cmi: common/hierarchy.cmi basic_rg/brgType.cmi \ +basic_rg/brgUntrusted.cmi: common/entity.cmx basic_rg/brgType.cmi \ basic_rg/brg.cmx basic_rg/brgUntrusted.cmo: lib/nUri.cmi lib/log.cmi common/entity.cmx \ basic_rg/brgType.cmi basic_rg/brgReduction.cmi \ diff --git a/helm/software/lambda-delta/basic_ag/bagType.ml b/helm/software/lambda-delta/basic_ag/bagType.ml index dbf1bd4eb..ec7d92c89 100644 --- a/helm/software/lambda-delta/basic_ag/bagType.ml +++ b/helm/software/lambda-delta/basic_ag/bagType.ml @@ -46,12 +46,12 @@ let mk_gref u l = (* Interface functions ******************************************************) -let rec b_type_of f ~si g c x = +let rec b_type_of f st c x = (* L.warn "Entering T.b_type_of"; *) log1 "Now checking" c x; match x with | B.Sort h -> - let h = H.apply g h in f x (B.Sort h) + let h = H.apply st.Y.g h in f x (B.Sort h) | B.LRef i -> let f = function | Some (_, B.Abst w) -> f x w @@ -75,25 +75,25 @@ let rec b_type_of f ~si g c x = let f xv xt tt = f (S.sh2 v xv t xt x (B.bind_abbr l id)) (B.bind_abbr l id xv tt) in - let f xv cc = b_type_of (f xv) ~si g cc t in + let f xv cc = b_type_of (f xv) st cc t in let f xv = B.push "type abbr" (f xv) c l id (B.Abbr xv) in let f xv vv = match xv with | B.Cast _ -> f xv | _ -> f (B.Cast (vv, xv)) in - type_of f ~si g c v + type_of f st c v | B.Bind (l, id, B.Abst u, t) -> let f xu xt tt = f (S.sh2 u xu t xt x (B.bind_abst l id)) (B.bind_abst l id xu tt) in - let f xu cc = b_type_of (f xu) ~si g cc t in + let f xu cc = b_type_of (f xu) st cc t in let f xu _ = B.push "type abst" (f xu) c l id (B.Abst xu) in - type_of f ~si g c u + type_of f st c u | B.Bind (l, id, B.Void, t) -> let f xt tt = f (S.sh1 t xt x (B.bind l id B.Void)) (B.bind l id B.Void tt) in - let f cc = b_type_of f ~si g cc t in + let f cc = b_type_of f st cc t in B.push "type void" f c l id B.Void | B.Appl (v, t) -> let f xv vv xt tt = function @@ -106,22 +106,22 @@ let rec b_type_of f ~si g c x = if a then f (S.sh2 v xv t xt x B.appl) (B.appl xv tt) else error3 c xv vv w in - R.are_convertible f ~si c w vv + R.are_convertible f ~si:st.Y.si c w vv | _ -> error1 "not a function" c xt in let f xv vv xt tt = R.ho_whd (f xv vv xt tt) c tt in - let f xv vv = b_type_of (f xv vv) ~si g c t in - type_of f ~si g c v + let f xv vv = b_type_of (f xv vv) st c t in + type_of f st c v | B.Cast (u, t) -> let f xu xt tt a = (* L.warn (Printf.sprintf "Convertible: %b" a); *) if a then f (S.sh2 u xu t xt x B.cast) xu else error3 c xt tt xu in - let f xu xt tt = R.are_convertible (f xu xt tt) ~si c xu tt in - let f xu _ = b_type_of (f xu) ~si g c t in - type_of f ~si g c u + let f xu xt tt = R.are_convertible (f xu xt tt) ~si:st.Y.si c xu tt in + let f xu _ = b_type_of (f xu) st c t in + type_of f st c u -and type_of f ?(si=false) g c x = +and type_of f st c x = let f t u = L.unbox level; f t u in - L.box level; b_type_of f ~si g c x + L.box level; b_type_of f st c x diff --git a/helm/software/lambda-delta/basic_ag/bagType.mli b/helm/software/lambda-delta/basic_ag/bagType.mli index d44b1cfe2..31a421bda 100644 --- a/helm/software/lambda-delta/basic_ag/bagType.mli +++ b/helm/software/lambda-delta/basic_ag/bagType.mli @@ -12,5 +12,5 @@ exception TypeError of Bag.message val type_of: - (Bag.term -> Bag.term -> 'a) -> ?si:bool -> - Hierarchy.graph -> Bag.lenv -> Bag.term -> 'a + (Bag.term -> Bag.term -> 'a) -> + Entity.status -> Bag.lenv -> Bag.term -> 'a diff --git a/helm/software/lambda-delta/basic_ag/bagUntrusted.ml b/helm/software/lambda-delta/basic_ag/bagUntrusted.ml index 8c6cbb47e..33d6a5fbd 100644 --- a/helm/software/lambda-delta/basic_ag/bagUntrusted.ml +++ b/helm/software/lambda-delta/basic_ag/bagUntrusted.ml @@ -19,11 +19,11 @@ module T = BagType (* Interface functions ******************************************************) (* to share *) -let type_check f ?(si=false) g = function +let type_check f st = function | a, uri, Y.Abst t -> let f xt tt = E.set_entity (f tt) (a, uri, Y.Abst xt) in - L.loc := U.string_of_uri uri; T.type_of f ~si g B.empty_lenv t + L.loc := U.string_of_uri uri; T.type_of f st B.empty_lenv t | a, uri, Y.Abbr t -> let f xt tt = E.set_entity (f tt) (a, uri, Y.Abbr xt) in - L.loc := U.string_of_uri uri; T.type_of f ~si g B.empty_lenv t + L.loc := U.string_of_uri uri; T.type_of f st B.empty_lenv t | _, _, Y.Void -> assert false diff --git a/helm/software/lambda-delta/basic_ag/bagUntrusted.mli b/helm/software/lambda-delta/basic_ag/bagUntrusted.mli index 1d25e3da7..af967408e 100644 --- a/helm/software/lambda-delta/basic_ag/bagUntrusted.mli +++ b/helm/software/lambda-delta/basic_ag/bagUntrusted.mli @@ -10,5 +10,4 @@ V_______________________________________________________________ *) val type_check: - (Bag.term -> Bag.entity -> 'a) -> ?si:bool -> - Hierarchy.graph -> Bag.entity -> 'a + (Bag.term -> Bag.entity -> 'a) -> Entity.status -> Bag.entity -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml index 5dff4647b..03ed05b05 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.ml +++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml @@ -170,7 +170,7 @@ and ac st m1 t1 m2 t2 = and ac_stacks st m1 m2 = (* L.warn "entering R.are_convertible_stacks"; *) -(* if List.length m1.s <> List.length m2.s then false else *) + if List.length m1.s <> List.length m2.s then false else let map (c1, v1) (c2, v2) = let m1, m2 = {m1 with e = c1; s = []}, {m2 with e = c2; s = []} in ac {st with Y.si = false} m1 v1 m2 v2 @@ -194,7 +194,7 @@ let xwhd st m t = let are_convertible st mu u mw w = L.box level; log2 "Now converting" mu.e u mw.e w; - let r = ac {st with Y.delta = false; Y.rt = false} mu u mw w in + let r = ac {st with Y.delta = st.Y.expand; Y.rt = false} mu u mw w in L.unbox level; r (* let err _ = in if S.eq mu mw then are_alpha_convertible err f u w else err () *) diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml index 728e3ff41..8443cd166 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.ml +++ b/helm/software/lambda-delta/basic_rg/brgType.ml @@ -62,11 +62,11 @@ let assert_applicability err f st m u w v = error3 err m v w ~mu u | _ -> assert false (**) -let rec b_type_of err f st g m x = +let rec b_type_of err f st m x = log1 "Now checking" m x; match x with | B.Sort (a, h) -> - let h = H.apply g h in f x (B.Sort (a, h)) + let h = H.apply st.Y.g h in f x (B.Sort (a, h)) | B.LRef (_, i) -> begin match R.get m i with | B.Abst w -> @@ -89,43 +89,43 @@ let rec b_type_of err f st g m x = let f xv xt tt = f (A.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt) in - let f xv m = b_type_of err (f xv) st g m t in + let f xv m = b_type_of err (f xv) st m t in let f xv = f xv (R.push m a (B.abbr xv)) in let f xv vv = match xv with | B.Cast _ -> f xv | _ -> f (B.Cast ([], vv, xv)) in - type_of err f st g m v + type_of err f st m v | B.Bind (a, B.Abst u, t) -> let f xu xt tt = f (A.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt) in - let f xu m = b_type_of err (f xu) st g m t in + let f xu m = b_type_of err (f xu) st m t in let f xu _ = f xu (R.push m a (B.abst xu)) in - type_of err f st g m u + type_of err f st m u | B.Bind (a, B.Void, t) -> let f xt tt = f (A.sh1 t xt x (B.bind_void a)) (B.bind_void a tt) in - b_type_of err f st g (R.push m a B.Void) t + b_type_of err f st (R.push m a B.Void) t | B.Appl (a, v, t) -> let f xv vv xt tt = let f _ = f (A.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in assert_applicability err f st m tt vv xv in - let f xv vv = b_type_of err (f xv vv) st g m t in - type_of err f st g m v + let f xv vv = b_type_of err (f xv vv) st m t in + type_of err f st m v | B.Cast (a, u, t) -> let f xu xt tt = let f _ = f (A.sh2 u xu t xt x (B.cast a)) xu in assert_convertibility err f st m xu tt xt in - let f xu _ = b_type_of err (f xu) st g m t in - type_of err f st g m u + let f xu _ = b_type_of err (f xu) st m t in + type_of err f st m u (* Interface functions ******************************************************) -and type_of err f st g m x = +and type_of err f st m x = let f t u = L.unbox level; f t u in - L.box level; b_type_of err f st g m x + L.box level; b_type_of err f st m x diff --git a/helm/software/lambda-delta/basic_rg/brgType.mli b/helm/software/lambda-delta/basic_rg/brgType.mli index b235b47e9..5d9350b49 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.mli +++ b/helm/software/lambda-delta/basic_rg/brgType.mli @@ -13,4 +13,4 @@ type message = (BrgReduction.kam, Brg.term) Log.message val type_of: (message -> 'a) -> (Brg.term -> Brg.term -> 'a) -> - Entity.status -> Hierarchy.graph -> BrgReduction.kam -> Brg.term -> 'a + Entity.status -> BrgReduction.kam -> Brg.term -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml index 959a74619..311061aaa 100644 --- a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml +++ b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml @@ -20,17 +20,15 @@ module T = BrgType (* Interface functions ******************************************************) (* to share *) -let type_check err f ?(si=false) g = function +let type_check err f st = function | a, uri, Y.Abst t -> let f xt tt = let e = E.set_entity (a, uri, Y.Abst xt) in f tt e in - let st = Y.initial_status si in - L.loc := U.string_of_uri uri; T.type_of err f st g R.empty_kam t + L.loc := U.string_of_uri uri; T.type_of err f st R.empty_kam t | a, uri, Y.Abbr t -> let f xt tt = let e = E.set_entity (a, uri, Y.Abbr xt) in f tt e in - let st = Y.initial_status si in - L.loc := U.string_of_uri uri; T.type_of err f st g R.empty_kam t + L.loc := U.string_of_uri uri; T.type_of err f st R.empty_kam t | _, _, Y.Void -> assert false diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.mli b/helm/software/lambda-delta/basic_rg/brgUntrusted.mli index 9c0568f10..d395eb535 100644 --- a/helm/software/lambda-delta/basic_rg/brgUntrusted.mli +++ b/helm/software/lambda-delta/basic_rg/brgUntrusted.mli @@ -11,4 +11,4 @@ val type_check: (BrgType.message -> 'a) -> (Brg.term -> Brg.entity -> 'a) -> - ?si:bool -> Hierarchy.graph -> Brg.entity -> 'a + Entity.status -> Brg.entity -> 'a diff --git a/helm/software/lambda-delta/common/entity.ml b/helm/software/lambda-delta/common/entity.ml index 5bef9ff33..d6314150b 100644 --- a/helm/software/lambda-delta/common/entity.ml +++ b/helm/software/lambda-delta/common/entity.ml @@ -28,9 +28,11 @@ type 'term entity = attrs * uri * 'term bind (* attrs, name, binder *) type uri_generator = string -> string type status = { - delta: bool; (* global delta-expansion *) - rt: bool; (* reference typing *) - si: bool (* sort inclusion *) + g: Hierarchy.graph; (* sort hierarchy parameter *) + delta: bool; (* global delta-expansion *) + rt: bool; (* reference typing *) + si: bool; (* sort inclusion *) + expand: bool (* always expand global definitions *) } (* helpers ******************************************************************) @@ -94,6 +96,6 @@ let xlate f xlate_term = function | _, _, Void -> assert false -let initial_status si = { - delta = false; rt = false; si = si +let initial_status g expand si = { + g = g; delta = false; rt = false; si = si; expand = expand } diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index dff0bbe10..c1c353844 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -42,17 +42,19 @@ type status = { ac : AO.counters; mc : MO.counters; brgc: BrgO.counters; - bagc: BagO.counters + bagc: BagO.counters; + kst : Y.status } -let initial_status mk_uri cover = { +let initial_status mk_uri cover g expand si = { ac = AO.initial_counters; mc = MO.initial_counters; brgc = BrgO.initial_counters; bagc = BagO.initial_counters; mst = MA.initial_status ~cover (); dst = DA.initial_status (mk_uri cover); - ast = AP.initial_status + ast = AP.initial_status; + kst = Y.initial_status g expand si } let flush_all () = L.flush 0; L.flush_err () @@ -120,12 +122,12 @@ let export_entity si g moch = function end | BagEntity _ -> () -let type_check st si g k = +let type_check st k = let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in let ok _ _ = st in match k with - | BrgEntity entity -> BrgU.type_check brg_err ok ~si g entity - | BagEntity entity -> BagU.type_check ok ~si g entity + | BrgEntity entity -> BrgU.type_check brg_err ok st.kst entity + | BagEntity entity -> BagU.type_check ok st.kst entity | CrgEntity _ | MetaEntity _ -> st @@ -138,6 +140,7 @@ let progress = ref false let preprocess = ref false let use_cover = ref true let si = ref false +let expand = ref false let cc = ref false let export = ref false let graph = ref (H.graph_of_string C.err C.start "Z2") @@ -146,7 +149,7 @@ let old = ref false let process_2 st entity = let st = if !L.level > 2 then count_entity st entity else st in if !export then export_entity !si !graph !moch entity; - if !stage > 2 then type_check st !si !graph entity else st + if !stage > 2 then type_check st entity else st let process_1 st entity = if !progress then pp_progress entity; @@ -178,7 +181,7 @@ let rec process st = function let main = try - let version_string = "Helena 0.8.1 M - October 2009" in + let version_string = "Helena 0.8.1 M - December 2009" in let set_hierarchy s = let err () = L.warn (P.sprintf "Unknown type hierarchy: %s" s) in let f g = graph := g in @@ -220,7 +223,8 @@ try | Bag -> Bag.mk_uri in let cover = if !use_cover then base_name else "" in - let st = process (initial_status mk_uri cover) book in + let st = initial_status mk_uri cover !graph !expand !si in + let st = process st book in if !L.level > 0 then T.utime_stamp "processed"; if !L.level > 2 then begin AO.print_counters C.start st.ac; @@ -236,7 +240,7 @@ try flush_all () in let help = - "Usage: helena [ -Vcijmopux | -Ss | -hk ] ...\n\n" ^ + "Usage: helena [ -Vcgijmopux | -Ss | -hk ] ...\n\n" ^ "Summary levels: 0 just errors (default), 1 time stamps, 2 processed file names, \ 3 data information, 4 typing information, 5 reduction information\n\n" ^ "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n" @@ -245,6 +249,7 @@ try let help_V = " show version information" in let help_c = " output conversion constraints" in + let help_g = " always expand global definitions" in let help_h = " set type hierarchy (default: Z2)" in let help_i = " show local references by index" in let help_j = " show URI of processed kernel objects" in @@ -263,6 +268,7 @@ try ("-S", Arg.Int set_summary, help_S); ("-V", Arg.Unit print_version, help_V); ("-c", Arg.Set cc, help_c); + ("-g", Arg.Set expand, help_g); ("-h", Arg.String set_hierarchy, help_h); ("-i", Arg.Set O.indexes, help_i); ("-j", Arg.Set progress, help_j);