the commit contnues by updating the RTM and modifying the typechecker accordingly

diff --git a/helm/software/helena/.depend.opt b/helm/software/helena/.depend.opt
index 8843aa957e85c50d7c8c22bd0c0a010a56ea7541..8f1a57695177b2ede69a86a82d99f3f5c859d100 100644 (file)
--- a/helm/software/helena/.depend.opt
+++ b/helm/software/helena/.depend.opt
@@ -153,14 +153,14 @@ src/basic_rg/brgReduction.cmx: src/common/status.cmx src/lib/share.cmx \
     src/common/ccs.cmx src/basic_rg/brgOutput.cmx \
     src/basic_rg/brgEnvironment.cmx src/basic_rg/brg.cmx \
     src/basic_rg/brgReduction.cmi
     src/common/ccs.cmx src/basic_rg/brgOutput.cmx \
     src/basic_rg/brgEnvironment.cmx src/basic_rg/brg.cmx \
     src/basic_rg/brgReduction.cmi

-src/basic_rg/brgValid.cmi: src/common/status.cmx \
+src/basic_rg/brgValidity.cmi: src/common/status.cmx \

     src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx
     src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx

-src/basic_rg/brgValid.cmo: src/lib/log.cmi src/common/entity.cmx \
+src/basic_rg/brgValidity.cmo: src/lib/log.cmi src/common/entity.cmx \

     src/basic_rg/brgReduction.cmi src/basic_rg/brgEnvironment.cmi \
     src/basic_rg/brgReduction.cmi src/basic_rg/brgEnvironment.cmi \

-    src/basic_rg/brg.cmx src/basic_rg/brgValid.cmi
-src/basic_rg/brgValid.cmx: src/lib/log.cmx src/common/entity.cmx \
+    src/basic_rg/brg.cmx src/basic_rg/brgValidity.cmi
+src/basic_rg/brgValidity.cmx: src/lib/log.cmx src/common/entity.cmx \

     src/basic_rg/brgReduction.cmx src/basic_rg/brgEnvironment.cmx \
     src/basic_rg/brgReduction.cmx src/basic_rg/brgEnvironment.cmx \

-    src/basic_rg/brg.cmx src/basic_rg/brgValid.cmi
+    src/basic_rg/brg.cmx src/basic_rg/brgValidity.cmi

 src/basic_rg/brgType.cmi: src/common/status.cmx src/basic_rg/brgReduction.cmi \
     src/basic_rg/brg.cmx
 src/basic_rg/brgType.cmo: src/lib/share.cmx src/lib/log.cmi \
 src/basic_rg/brgType.cmi: src/common/status.cmx src/basic_rg/brgReduction.cmi \
     src/basic_rg/brg.cmx
 src/basic_rg/brgType.cmo: src/lib/share.cmx src/lib/log.cmi \


@@ -176,11 +176,11 @@ src/basic_rg/brgType.cmx: src/lib/share.cmx src/lib/log.cmx \
 src/basic_rg/brgUntrusted.cmi: src/common/status.cmx \
     src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx
 src/basic_rg/brgUntrusted.cmo: src/lib/log.cmi src/common/entity.cmx \
 src/basic_rg/brgUntrusted.cmi: src/common/status.cmx \
     src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx
 src/basic_rg/brgUntrusted.cmo: src/lib/log.cmi src/common/entity.cmx \

-    src/basic_rg/brgValid.cmi src/basic_rg/brgType.cmi \
+    src/basic_rg/brgValidity.cmi src/basic_rg/brgType.cmi \

     src/basic_rg/brgReduction.cmi src/basic_rg/brgEnvironment.cmi \
     src/basic_rg/brg.cmx src/basic_rg/brgUntrusted.cmi
 src/basic_rg/brgUntrusted.cmx: src/lib/log.cmx src/common/entity.cmx \
     src/basic_rg/brgReduction.cmi src/basic_rg/brgEnvironment.cmi \
     src/basic_rg/brg.cmx src/basic_rg/brgUntrusted.cmi
 src/basic_rg/brgUntrusted.cmx: src/lib/log.cmx src/common/entity.cmx \

-    src/basic_rg/brgValid.cmx src/basic_rg/brgType.cmx \
+    src/basic_rg/brgValidity.cmx src/basic_rg/brgType.cmx \

     src/basic_rg/brgReduction.cmx src/basic_rg/brgEnvironment.cmx \
     src/basic_rg/brg.cmx src/basic_rg/brgUntrusted.cmi
 src/basic_ag/bag.cmo: src/lib/log.cmi src/common/entity.cmx src/lib/cps.cmx
     src/basic_rg/brgReduction.cmx src/basic_rg/brgEnvironment.cmx \
     src/basic_rg/brg.cmx src/basic_rg/brgUntrusted.cmi
 src/basic_ag/bag.cmo: src/lib/log.cmi src/common/entity.cmx src/lib/cps.cmx

diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml
index 98747ab55a810f10ee463d28cb8270f56dd16a76..d4b5e68fdc111b8fd1a2c3d4380e332875590e2a 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgReduction.ml
+++ b/helm/software/helena/src/basic_rg/brgReduction.ml
@@ -13,6 +13,7 @@ module U  = NUri
 module C  = Cps
 module W  = Share
 module L  = Log
 module C  = Cps
 module W  = Share
 module L  = Log

+module H  = Hierarchy

 module E  = Entity
 module N  = Level
 module O  = Output
 module E  = Entity
 module N  = Level
 module O  = Output


@@ -23,11 +24,15 @@ module BO = BrgOutput
 module BE = BrgEnvironment
 
 type kam = {
 module BE = BrgEnvironment
 
 type kam = {

-   e: B.lenv;                 (* environment *)
-   s: (B.lenv * B.term) list; (* stack       *)
-   d: int                     (* depth       *)
+   e: B.lenv;                 (* environment              *)
+   s: (B.lenv * B.term) list; (* stack                    *)
+   l: int;                    (* level                    *)
+   d: int;                    (* inferred type iterations *)
+   n: int option;             (* expected type iterations *)

 }
 
 }
 

+type message = (kam, B.term) L.message
+

 (* Internal functions *******************************************************)
 
 let level = 5
 (* Internal functions *******************************************************)
 
 let level = 5


@@ -37,7 +42,7 @@ let log1 s c t =
    L.log BO.specs level (L.et_items1 sc c st t)
 
 let log2 s cu u ct t =
    L.log BO.specs level (L.et_items1 sc c st t)
 
 let log2 s cu u ct t =

-   let s1, s2, s3 = s ^ " in the environment", "the term", "and in the environment" in
+   let s1, s2, s3 = s ^ " in the environment (expected)", "the term", "and in the environment (inferred)" in

    L.log BO.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
 
 let rec list_and map = function
    L.log BO.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
 
 let rec list_and map = function


@@ -45,6 +50,8 @@ let rec list_and map = function
       if map hd1 hd2 then list_and map (tl1, tl2) else false
    | l1, l2                 -> l1 = l2
 
       if map hd1 hd2 then list_and map (tl1, tl2) else false
    | l1, l2                 -> l1 = l2
 

+let zero = Some 0
+

 (* check closure *)
 let are_alpha_convertible err f t1 t2 =
    let rec aux f = function
 (* check closure *)
 let are_alpha_convertible err f t1 t2 =
    let rec aux f = function


@@ -69,50 +76,64 @@ let are_alpha_convertible err f t1 t2 =
    in
    if W.eq t1 t2 then f () else aux f (t1, t2)
 
    in
    if W.eq t1 t2 then f () else aux f (t1, t2)
 

+let assert_tstep m vo = match m.n with
+   | Some n -> n > m.d
+   | None   -> vo
+
+let tstep m = {m with d = succ m.d}
+

 let get m i =
    let _, c, a, b = B.get m.e i in c, a, b
 
 (* to share *)
 let rec step st m x = 
 let get m i =
    let _, c, a, b = B.get m.e i in c, a, b
 
 (* to share *)
 let rec step st m x = 

-(*   L.warn "entering R.step"; *)
+   log1 (Printf.sprintf "entering R.step: l:%u d:%i n:%s" m.l m.d (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e x;

    match x with
    match x with

-   | B.Sort _                     -> m, None, x
+   | B.Sort (a, h)                ->
+      if assert_tstep m false then
+         step st (tstep m) (B.Sort (a, H.apply h))      
+      else m, x, None

    | B.GRef (_, uri)              ->
       begin match BE.get_entity uri with
    | B.GRef (_, uri)              ->
       begin match BE.get_entity uri with

-         | _, _, E.Abbr v when st.S.delta   ->
+         | _, _, E.Abbr v when st.S.delta               ->

            O.add ~gdelta:1 (); step st m v
            O.add ~gdelta:1 (); step st m v

-         | _, _, E.Abst (_, w) when st.S.rt ->
-            O.add ~grt:1 (); step st m w        
-        | a, _, E.Abbr v                   ->
-           let e = E.apix C.err C.start a in
-           m, Some (e, a, B.Abbr v), x   
-        | a, _, E.Abst (n, w)              ->
-           let e = E.apix C.err C.start a in
-           m, Some (e, a, B.Abst (n, w)), x
-        | _, _, E.Void                     -> assert false
+         | _, _, E.Abst (_, w) when assert_tstep m true ->
+            O.add ~grt:1 (); step st (tstep m) w
+        | _, _, E.Abbr v                               ->
+           m, x, Some v
+        | _, _, E.Abst _                               ->
+           m, x, None   
+        | _, _, E.Void                                 ->
+            assert false

       end
    | B.LRef (_, i)                ->
       begin match get m i with
       end
    | B.LRef (_, i)                ->
       begin match get m i with

-        | c, _, B.Abbr v                   ->
+        | c, _, B.Abbr v                          ->

            O.add ~ldelta:1 ();
            step st {m with e = c} v
            O.add ~ldelta:1 ();
            step st {m with e = c} v

-        | c, _, B.Abst (_, w) when st.S.rt ->
+        | c, _, B.Abst (_, w) when assert_tstep m true ->

             O.add ~lrt:1 ();
             O.add ~lrt:1 ();

-            step st {m with e = c} w
-        | c, _, B.Void                     ->
+            step st {(tstep m) with e = c} w
+        | _, a, B.Abst _                               ->
+          m, B.LRef (a, i), None
+        | _, _, B.Void                                 ->

            assert false
            assert false

-        | c, a, (B.Abst _ as b)            ->
-           let e = E.apix C.err C.start a in
-           {m with e = c}, Some (e, a, b), x

       end
       end

-   | B.Cast (_, _, t)             ->
-      O.add ~tau:1 ();
-      step st m t
+   | B.Cast (_, u, t)             ->
+      if assert_tstep m false then begin
+         O.add ~e:1 ();
+         step st (tstep m) u
+      end else begin
+         O.add ~epsilon:1 ();
+         step st m t
+      end

    | B.Appl (_, v, t)             ->
       step st {m with s = (m.e, v) :: m.s} t   
    | B.Bind (a, B.Abst (n, w), t) ->
    | B.Appl (_, v, t)             ->
       step st {m with s = (m.e, v) :: m.s} t   
    | B.Bind (a, B.Abst (n, w), t) ->

+      let n = N.minus n m.d in
+      let x = B.Bind (a, B.Abst (n, w), t) in

       begin match m.s with
       begin match m.s with

-         | []          -> m, None, x
+         | []          -> m, x, None

         | (c, v) :: s ->
             if N.is_zero n then Q.add_nonzero st.S.cc a;
            O.add ~beta:1 ~theta:(List.length s) ();
         | (c, v) :: s ->
             if N.is_zero n then Q.add_nonzero st.S.cc a;
            O.add ~beta:1 ~theta:(List.length s) ();


@@ -124,51 +145,64 @@ let rec step st m x =
       let e = B.push m.e m.e a b in 
       step st {m with e = e} t
 
       let e = B.push m.e m.e a b in 
       step st {m with e = e} t
 

+let reset m ?(e=m.e) n =
+   {m with e = e; n = n; s = []; d = 0} 
+
+let assert_iterations m1 m2 = match m1.n, m2.n with
+      | Some n1, Some n2 -> n1 - m1.d = n2 - m2.d
+      | _                -> false 
+

 let push m a b = 
    assert (m.s = []);
 let push m a b = 
    assert (m.s = []);

-   let a, d = match b with
-      | B.Abst _ -> E.Apix m.d :: a, succ m.d
-      | b        -> a, m.d
+   let a, l = match b with
+      | B.Abst _ -> E.Apix m.l :: a, succ m.l
+      | b        -> a, m.l

    in
    let e = B.push m.e m.e a b in
    in
    let e = B.push m.e m.e a b in

-   {m with e = e; d = d}
-
-let rec ac_nfs st (m1, r1, u) (m2, r2, t) =
-   log2 "Now converting nfs" m1.e u m2.e t;
-   match r1, u, r2, t with
-      | _, B.Sort (_, h1), _, B.Sort (_, h2)                   ->
-         h1 = h2  
-      | Some (e1, _, B.Abst _), _, Some (e2, _, B.Abst _), _   ->
+   {m with e = e; l = l}
+
+let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
+   log2 "Now converting nfs" m1.e t1 m2.e t2;
+   match t1, r1, t2, r2 with
+      | B.Sort (_, h1), _, B.Sort (_, h2), _                ->
+         h1 = h2
+      | B.LRef (a1, _), _, B.LRef (a2, _), _                ->
+         let e1 = E.apix C.err C.start a1 in
+         let e2 = E.apix C.err C.start a2 in

         if e1 = e2 then ac_stacks st m1 m2 else false
         if e1 = e2 then ac_stacks st m1 m2 else false

-      | Some (e1, _, B.Abbr v1), _, Some (e2, _, B.Abbr v2), _ ->
-         if e1 = e2 then
-           if ac_stacks st m1 m2 then true else begin
-              O.add ~gdelta:2 (); ac st m1 v1 m2 v2
-           end
-        else if e1 < e2 then begin 
+      | B.GRef (_, u1), None, B.GRef (_, u2), None          ->
+        if U.eq u1 u2 & assert_iterations m1 m2 then ac_stacks st m1 m2 else false
+      | B.GRef (a1, u1), Some v1, B.GRef (a2, u2), Some v2  ->
+         let e1 = E.apix C.err C.start a1 in
+         let e2 = E.apix C.err C.start a2 in
+         if e1 < e2 then begin 

             O.add ~gdelta:1 ();
             O.add ~gdelta:1 ();

-           ac_nfs st (m1, r1, u) (step st m2 v2)
-        end else begin
+           ac_nfs st (m1, t1, r1) (step st m2 v2)
+        end else if e2 < e1 then begin

            O.add ~gdelta:1 ();
            O.add ~gdelta:1 ();

-           ac_nfs st (step st m1 v1) (m2, r2, t) 
-         end
-      | _, _, Some (_, _, B.Abbr v2), _                        ->
-         O.add ~gdelta:1 ();
-        ac_nfs st (m1, r1, u) (step st m2 v2)      
-      | Some (_, _, B.Abbr v1), _, _, _                        ->
+           ac_nfs st (step st m1 v1) (m2, t2, r2) 
+         end else if U.eq u1 u2 & assert_iterations m1 m2 && ac_stacks st m1 m2 then true
+         else begin
+           O.add ~gdelta:2 ();
+           ac st m1 v1 m2 v2
+         end 
+      | _, _, B.GRef _, Some v2                             ->

          O.add ~gdelta:1 ();
          O.add ~gdelta:1 ();

-        ac_nfs st (step st m1 v1) (m2, r2, t)             
-      | _, B.Bind (a1, (B.Abst (n1, w1) as b1), t1), 
-        _, B.Bind (a2, (B.Abst (n2, w2) as b2), t2)            ->
+        ac_nfs st (m1, t1, r1) (step st m2 v2)
+      | B.GRef _, Some v1, _, _                             ->
+        O.add ~gdelta:1 ();
+        ac_nfs st (step st m1 v1) (m2, t2, r2)
+      | B.Bind (a1, (B.Abst (n1, w1) as b1), t1), _, 
+        B.Bind (a2, (B.Abst (n2, w2) as b2), t2), _         ->

         if n1 = n2 then () else Q.add_equal st.S.cc a1 a2;
         if n1 = n2 then () else Q.add_equal st.S.cc a1 a2;

-        if ac {st with S.si = false} m1 w1 m2 w2 then
+         if ac {st with S.si = false} (reset m1 zero) w1 (reset m2 zero) w2 then

            ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
         else false
            ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
         else false

-      | _, B.Sort _, _, B.Bind (a, (B.Abst (n, _) as b), t)    ->
+      | B.Sort _, _, B.Bind (a, (B.Abst (n, _) as b), t), _ ->

          if N.is_zero n then () else Q.add_zero st.S.cc a;
         O.add ~si:1 ();
          if N.is_zero n then () else Q.add_zero st.S.cc a;
         O.add ~si:1 ();

-        ac st (push m1 a b) u (push m2 a b) t
-      | _                                                      -> false
+        ac st (push m1 a b) t1 (push m2 a b) t
+      | _                                                   -> false

 
 and ac st m1 t1 m2 t2 =
 (*   L.warn "entering R.are_convertible"; *)
 
 and ac st m1 t1 m2 t2 =
 (*   L.warn "entering R.are_convertible"; *)


@@ -178,7 +212,7 @@ 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
    let map (c1, v1) (c2, v2) =
 (*   L.warn "entering R.are_convertible_stacks"; *)
    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
+      let m1, m2 = reset m1 ~e:c1 zero, reset m2 ~e:c2 zero in

       ac {st with S.si = false} m1 v1 m2 v2
    in
    list_and map (m1.s, m2.s)
       ac {st with S.si = false} m1 v1 m2 v2
    in
    list_and map (m1.s, m2.s)


@@ -186,21 +220,21 @@ and ac_stacks st m1 m2 =
 (* Interface functions ******************************************************)
 
 let empty_kam = { 
 (* Interface functions ******************************************************)
 
 let empty_kam = { 

-   e = B.empty; s = []; d = 0
+   e = B.empty; s = []; l = 0; d = 0; n = None

 }
 
 let get m i =
    assert (m.s = []);
    let _, _, _, b = B.get m.e i in b
 
 }
 
 let get m i =
    assert (m.s = []);
    let _, _, _, b = B.get m.e i in b
 

-let xwhd st m t =
+let xwhd st m n t =

    L.box level; log1 "Now scanning" m.e t;   
    L.box level; log1 "Now scanning" m.e t;   

-   let m, _, t = step {st with S.delta = true; S.rt = true} m t in
+   let m, t, _ = step {st with S.delta = true} (reset m n) t in

    L.unbox level; m, t
 
    L.unbox level; 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 S.delta = st.S.expand; S.rt = false} mu u mw w in   
+let are_convertible st m1 n1 t1 m2 n2 t2 = 
+   L.box level; log2 "Now converting" m1.e t1 m2.e t2;
+   let r = ac {st with S.delta = st.S.expand} (reset m1 n1) t1 (reset m2 n2) t2 in

    L.unbox level; r
 (*    let err _ = in 
       if W.eq mu mw then are_alpha_convertible err f u w else err () *)
    L.unbox level; r
 (*    let err _ = in 
       if W.eq mu mw then are_alpha_convertible err f u w else err () *)

diff --git a/helm/software/helena/src/basic_rg/brgReduction.mli b/helm/software/helena/src/basic_rg/brgReduction.mli
index e8df9f7aa4a1141a2705661527e07e9c4f09b8fa..e73d2df8a8508d793a80182e938c13398d6cabeb 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgReduction.mli
+++ b/helm/software/helena/src/basic_rg/brgReduction.mli
@@ -11,16 +11,18 @@
 
 type kam
 
 
 type kam
 

+type message = (kam, Brg.term) Log.message
+

 val empty_kam: kam
 
 val get: kam -> int -> Brg.bind
 
 val push: kam -> Entity.attrs -> Brg.bind -> kam
 
 val empty_kam: kam
 
 val get: kam -> int -> Brg.bind
 
 val push: kam -> Entity.attrs -> Brg.bind -> kam
 

-val xwhd: Status.status -> kam -> Brg.term -> kam * Brg.term 
+val xwhd: Status.status -> kam -> int option -> Brg.term -> kam * Brg.term 

 
 (* arguments: expected type, inferred type *) 
 val are_convertible: 
 
 (* arguments: expected type, inferred type *) 
 val are_convertible: 

-   Status.status -> kam -> Brg.term -> kam -> Brg.term -> bool
+   Status.status -> kam -> int option -> Brg.term -> kam -> int option -> Brg.term -> bool

 
 val specs: (kam, Brg.term) Log.specs
 
 val specs: (kam, Brg.term) Log.specs

diff --git a/helm/software/helena/src/basic_rg/brgType.ml b/helm/software/helena/src/basic_rg/brgType.ml
index f23da87d09fad4304838ccff99d8c5420756b5ae..9dcce08a6781d51f6a1471713ffc887fcfd73efd 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgType.ml
+++ b/helm/software/helena/src/basic_rg/brgType.ml
@@ -21,8 +21,6 @@ module BE = BrgEnvironment
 module BS = BrgSubstitution
 module BR = BrgReduction
 
 module BS = BrgSubstitution
 module BR = BrgReduction
 

-type message = (BR.kam, B.term) Log.message
-

 (* Internal functions *******************************************************)
 
 let level = 4
 (* Internal functions *******************************************************)
 
 let level = 4


@@ -51,15 +49,15 @@ let error3 err m t1 t2 ?mu t3 =
    err (message3 m t1 t2 ?mu t3)
 
 let assert_convertibility err f st m u w v =
    err (message3 m t1 t2 ?mu t3)
 
 let assert_convertibility err f st m u w v =

-   if BR.are_convertible st m u m w then f () else
+   if BR.are_convertible st m (Some 0) u m (Some 0) w then f () else

    error3 err m v w u
 
 let assert_applicability err f st m u w v =
    error3 err m v w u
 
 let assert_applicability err f st m u w v =

-   match BR.xwhd st m u with 
+   match BR.xwhd st m None u with 

       | _, B.Sort _                      ->
          error1 err "not a function type" m u
       | mu, B.Bind (_, B.Abst (_, u), _) -> 
       | _, B.Sort _                      ->
          error1 err "not a function type" m u
       | mu, B.Bind (_, B.Abst (_, u), _) -> 

-         if BR.are_convertible st mu u m w then f () else
+         if BR.are_convertible st mu (Some 0) u m (Some 0) w then f () else

         error3 err m v w ~mu u
       | _                                -> assert false (**)
 
         error3 err m v w ~mu u
       | _                                -> assert false (**)