From: acondolu Date: Mon, 28 May 2018 13:03:00 +0000 (+0200) Subject: Detection of divergents X-Git-Tag: weak-reduction-separation X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=inline;p=fireball-separation.git Detection of divergents --- diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 340b955..c6cecec 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -657,9 +657,9 @@ let env_of_sigma freshno sigma should_explode = e,Pure.lift (-n-1) (snd (List.find (fun (i,_) -> i = n) sigma)),[] with Not_found -> - if should_explode && n = hd_of_i_var (cast_to_i_var !bomb) - then ([], (let f t = Pure.A(t,t) in f (Pure.L (f (Pure.V 0)))), []) - else ([],Pure.V n,[]))::e + if n = hd_of_i_var (cast_to_i_var !bomb) + then ([], Pure.omega should_explode, []) + else ([], Pure.V n, []) ) :: e in aux 0 ;; (* ************************************************************************** *) @@ -712,22 +712,22 @@ let solve p = let ps = List.map scott_of_nf p.ps in let sigma' = List.map (fun (x,inst) -> x, scott_of_nf inst) sigma in - let e' = env_of_sigma freshno sigma' false (* FIXME shoudl_explode *) in + let e' = env_of_sigma freshno sigma' false in + let e'' = env_of_sigma freshno sigma' true in prerr_endline "-----------------"; - let pure_bomb = ToScott.t_of_nf (!bomb) in (* Pure.B *) (function | Some div -> print_endline (Pure.print div); let t = Pure.mwhd (e',div,[]) in prerr_endline ("*:: " ^ (Pure.print t)); - assert (t = pure_bomb) + assert (Pure.diverged t) | None -> ()) div; List.iter (fun n -> verbose ("_::: " ^ (Pure.print n)); - let t = Pure.mwhd (e',n,[]) in + let t = Pure.mwhd (e'',n,[]) in verbose ("_:: " ^ (Pure.print t)); - assert (t <> pure_bomb) + assert (not (Pure.diverged t)) ) conv ; List.iteri (fun i n -> verbose ((string_of_int i) ^ "::: " ^ (Pure.print n)); diff --git a/ocaml/pure.ml b/ocaml/pure.ml index 95dae15..29288aa 100644 --- a/ocaml/pure.ml +++ b/ocaml/pure.ml @@ -101,6 +101,13 @@ let mwhd m = | (_,L _,[]) as m -> m in unwind (aux m) +let omega should_explode = + if should_explode + then let f t = A(t,t) in f (L (f (V 0))) + else B +;; + +let diverged = (=) B;; end diff --git a/ocaml/pure.mli b/ocaml/pure.mli index a6b90ac..1b60c09 100644 --- a/ocaml/pure.mli +++ b/ocaml/pure.mli @@ -3,8 +3,9 @@ module Pure : type t = V of int | A of t * t | L of t | B val print : ?l:string list -> t -> string val lift : int -> t -> t - val unwind : ?tbl:('a list * t * 'a list as 'a, t) Hashtbl.t -> 'a -> t val mwhd : (('a * t * ('b list as 'c) as 'b) list as 'a) * t * 'c -> t + val omega : bool -> t + val diverged : t -> bool end module Scott :