]> matita.cs.unibo.it Git - helm.git/commitdiff
new options activated
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 19 Jun 2015 16:58:43 +0000 (16:58 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 19 Jun 2015 16:58:43 +0000 (16:58 +0000)
- tracing can be restricted to specific constants with -b and -e
- restricted applications are now used by default for Automath inputs
  use -n to activate extended applications
  (this may lead to longer computations)

28 files changed:
helm/software/helena/Makefile
helm/software/helena/src/automath/autCrg.ml
helm/software/helena/src/basic_ag/bagCrg.ml
helm/software/helena/src/basic_ag/bagOutput.ml
helm/software/helena/src/basic_ag/bagReduction.ml
helm/software/helena/src/basic_ag/bagType.ml
helm/software/helena/src/basic_rg/brg.ml
helm/software/helena/src/basic_rg/brgCrg.ml
helm/software/helena/src/basic_rg/brgELPI.ml
helm/software/helena/src/basic_rg/brgELPI.mli
helm/software/helena/src/basic_rg/brgGallina.ml
helm/software/helena/src/basic_rg/brgGrafite.ml
helm/software/helena/src/basic_rg/brgOutput.ml
helm/software/helena/src/basic_rg/brgReduction.ml
helm/software/helena/src/basic_rg/brgSubstitution.ml
helm/software/helena/src/basic_rg/brgType.ml
helm/software/helena/src/basic_rg/brgUntrusted.ml
helm/software/helena/src/basic_rg/brgValidity.ml
helm/software/helena/src/common/layer.ml
helm/software/helena/src/common/options.ml
helm/software/helena/src/common/output.ml
helm/software/helena/src/complete_rg/crg.ml
helm/software/helena/src/complete_rg/crgOutput.ml
helm/software/helena/src/text/txtCrg.ml
helm/software/helena/src/toplevel/top.ml
helm/software/helena/src/xml/xmlCrg.ml
helm/software/helena/src/xml/xmlLibrary.ml
helm/software/helena/src/xml/xmlLibrary.mli

index f26c4e8579c0dd0026f71b02b0e71d8bf86ac1f6..61891b69b48f81940311c322f6145d416e097f8c 100644 (file)
@@ -40,7 +40,7 @@ PREAMBLE_ELPI = elpi/elpi.template
 
 test-si-fast: $(MAIN).opt etc
        @echo "  HELENA -o -q -1 $(INPUTFAST)"
-       $(H)./$(MAIN).opt -T 1 -o -q -1 $(O) $(INPUTFAST) > etc/log.txt
+       $(H)./$(MAIN).opt -T 1 -n -o -q -1 $(O) $(INPUTFAST) > etc/log.txt
 
 test-si: $(MAIN).opt etc
        @echo "  HELENA -d -l -p -o $(INPUT)"
@@ -87,12 +87,13 @@ export-matita matita/$(MA): $(MAIN).opt etc
 export-elpi elpi/$(ELPI): $(MAIN).opt etc
        @echo "  HELENA -l -m ELPI -o $(INPUT)"
        $(H)mkdir -p elpi
-       $(H)./$(MAIN).opt -T 1 -a n -c $(PREAMBLE_ELPI) -l -m ELPI -o $(O) $(INPUT) > etc/log.txt
+       $(H)./$(MAIN).opt -T 1 -a n -c $(PREAMBLE_ELPI) -l -m ELPI1 -o $(O) $(INPUT) >  etc/log.txt
+       $(H)./$(MAIN).opt -T 1 -a n -c $(PREAMBLE_ELPI) -l -m ELPI2 -o $(O) $(INPUT) >> etc/log.txt
 
 profile-fast: $(MAIN).opt etc
        @echo "  HELENA -o -q $(INPUTFAST) (31 TIMES)"
        $(H)rm -f etc/log.txt
-       $(H)for T in `seq 31`; do ./$(MAIN).opt -T 1 -o -q $(O) $(INPUTFAST) >> etc/log.txt; done
+       $(H)for T in `seq 31`; do ./$(MAIN).opt -T 1 -n -o -q $(O) $(INPUTFAST) >> etc/log.txt; done
        $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile.txt
 
 profile: $(MAIN).opt etc
index c17b83f07a8f477e189518b84c580b59ccc86d33..667b18cc1bfaea0c77f68dca895ed06d38a871d2 100644 (file)
@@ -118,7 +118,7 @@ let rec xlate_term f st lst y lenv = function
       let a = E.node_attrs ~sort:h () in
       f a (D.TSort (a, h))
    | A.Appl (v, t)       ->
-      let f vv at tt = f at (D.TAppl (at, vv, tt)) in
+      let f vv at tt = f at (D.TAppl (at, !G.extended, vv, tt)) in
       let f _ vv = xlate_term (f vv) st lst y lenv t in
       xlate_term f st lst false lenv v
    | A.Abst (name, w, t) ->
@@ -146,15 +146,15 @@ let rec xlate_term f st lst y lenv = function
    | A.GRef (name, args) ->
       let map1 args (id, _) = A.GRef ((id, true, []), []) :: args in
       let map2 f arg args = 
-         let f _ arg = f (D.EAppl (args, E.empty_node, arg)) in 
+         let f _ arg = f (D.EAppl (args, E.empty_node, !G.extended, arg)) in 
          xlate_term f st lst false lenv arg
       in
       let g qid a cnt =
          let gref = D.TGRef (a, uri_of_qid qid) in
         if cnt = D.ESort then f a gref else
         let f = function 
-            | D.EAppl (D.ESort, _, v) -> f a (D.TAppl (a, v, gref))
-            | args                    -> f a (D.TProj (a, args, gref))
+            | D.EAppl (D.ESort, _, x, v) -> f a (D.TAppl (a, x, v, gref))
+            | args                       -> f a (D.TProj (a, args, gref))
          in
         let f args = C.list_fold_right f map2 args D.ESort in
         D.sub_list_strict (D.fold_names f map1 args) cnt args
@@ -201,6 +201,7 @@ let xlate_entity err f st lst = function
 *)
               let b = E.Abst t in
               let entity = E.empty_root, aw, uri_of_qid qid, b in
+               G.set_current_trace lst.line;
               f {lst with line = succ lst.line} entity
            in
            xlate_term f st lst true lenv w
@@ -222,6 +223,7 @@ let xlate_entity err f st lst = function
                  let b = E.Abbr t in
                   let ra = if trans then E.empty_root else E.root_attrs ~meta:[E.Private] () in
                  let entity = ra, na, uri_of_qid qid, b in
+                  G.set_current_trace lst.line;
                  f {lst with line = succ lst.line} entity
               in
               xlate_term f st lst false lenv v
index 08f342496f1badd4e580df9e724e6ad2a47bfd73..b9ce1d3447e0b26b7d52a1f07862c1eb768818ab 100644 (file)
@@ -19,15 +19,15 @@ module Z = Bag
 (* internal functions: crg to bag term **************************************)
 
 let rec xlate_term st f c = function
-   | D.TSort (_, h)    -> f (Z.Sort h)
-   | D.TGRef (_, s)    -> f (Z.GRef s)
-   | D.TLRef (a, i)    ->
+   | D.TSort (_, h)       -> f (Z.Sort h)
+   | D.TGRef (_, s)       -> f (Z.GRef s)
+   | D.TLRef (a, i)       ->
       let _, l, _ = List.nth c i in f (Z.LRef l)
-   | D.TCast (_, u, t) ->
+   | D.TCast (_, u, t)    ->
       let f tt uu = f (Z.Cast (uu, tt)) in
       let f tt = xlate_term st (f tt) c u in
       xlate_term st f c t
-   | D.TAppl (_, v, t) ->
+   | D.TAppl (_, _, v, t) ->
       let f tt vv = f (Z.Appl (vv, tt)) in
       let f tt = xlate_term st (f tt) c v in
       xlate_term st f c t
@@ -36,7 +36,7 @@ let rec xlate_term st f c = function
 (* this case should be removed by improving alpha-conversion *)
    | D.TBind (ab, D.Abst (x, n, ws), D.TCast (ac, u, t)) ->
       xlate_term st f c (D.TCast (ac, D.TBind (ab, D.Abst (x, N.minus st n 1, ws), u), D.TBind (ab, D.Abst (x, n, ws), t)))
-   | D.TBind (a, b, t) ->
+   | D.TBind (a, b, t)    ->
       let f cc =
          let a, l, b = List.hd cc in
          let f tt = f (Z.Bind (a, l, b, tt)) in
@@ -67,7 +67,7 @@ let rec xlate_bk_term f c = function
       let f tt = xlate_bk_term (f tt) c u in
       xlate_bk_term f c t 
    | Z.Appl (u, t)       ->
-      let f tt uu = f (D.TAppl (E.empty_node, uu, tt)) in
+      let f tt uu = f (D.TAppl (E.empty_node, true, uu, tt)) in
       let f tt = xlate_bk_term (f tt) c u in
       xlate_bk_term f c t 
    | Z.Bind (a, l, b, t) ->
index 88e64e5d05e343c3791898f920fd443f27816c8f..4867c7180d53198af018af0853c0157be9f2d06f 100644 (file)
@@ -111,18 +111,18 @@ let res a l och =
    if !G.indexes then err () else name err och a
 
 let rec pp_term st c och = function
-   | Z.Sort h                 -> 
+   | Z.Sort h                   -> 
       let err () = KP.fprintf och "*%u" h in
       let f s = KP.fprintf och "%s" s in
       H.string_of_sort err f h 
-   | Z.LRef i                 -> 
+   | Z.LRef i                   -> 
       let err () = KP.fprintf och "#%s" (P.string_of_mark i) in
       let f a _ = name err och a in
       if !G.indexes then err () else Z.get err f c i
-   | Z.GRef s                    -> KP.fprintf och "$%s" (U.string_of_uri s)
-   | Z.Cast (u, t)               ->
+   | Z.GRef s                   -> KP.fprintf och "$%s" (U.string_of_uri s)
+   | Z.Cast (u, t)              ->
       KP.fprintf och "{%a}.%a" (pp_term st c) u (pp_term st c) t
-   | Z.Appl (v, t)               ->
+   | Z.Appl (v, t)              ->
       KP.fprintf och "(%a).%a" (pp_term st c) v (pp_term st c) t
    | Z.Bind (a, l, Z.Abst w, t) ->
       let f cc =
index 287978f5064dcf1a71856d4ab0d52c6798fa546d..cc3cb36f8266b8edb35cf92617f61aae552c90b6 100644 (file)
@@ -81,19 +81,19 @@ let push msg f c m a l w =
 let rec whd f c m x = 
 (*   L.warn "entering R.whd"; *)
    match x with
-   | Z.Sort h                    -> f m (Sort_ h)
-   | Z.GRef uri                  ->
+   | Z.Sort h                   -> f m (Sort_ h)
+   | Z.GRef uri                 ->
       let f entry = f m (GRef_ entry) in
       ZE.get_entity f uri
-   | Z.LRef i                    ->
+   | Z.LRef i                   ->
       let f = function
          | Z.Void   -> f m (LRef_ (i, None))
         | Z.Abst t -> f m (LRef_ (i, Some t))
         | Z.Abbr t -> whd f c m t
       in
       get f c m i
-   | Z.Cast (_, t)               -> whd f c m t
-   | Z.Appl (v, t)               -> whd f c {m with s = v :: m.s} t   
+   | Z.Cast (_, t)              -> whd f c m t
+   | Z.Appl (v, t)              -> whd f c {m with s = v :: m.s} t   
    | Z.Bind (a, l, Z.Abst w, t) ->
       begin match m.s with
          | []      -> f m (Bind_ (a, l, w, t))
@@ -102,7 +102,7 @@ let rec whd f c m x =
            let f mc = ZS.subst (whd f c {m with c = mc; s = tl}) nl l t in
            Z.push "!" f m.c a nl (Z.Abbr (Z.Cast (w, v)))
       end
-   | Z.Bind (a, l, b, t)         -> 
+   | Z.Bind (a, l, b, t)        -> 
       let nl = P.new_mark () in
       let f mc = ZS.subst (whd f c {m with c = mc}) nl l t in
       Z.push "!" f m.c a nl b
@@ -124,7 +124,7 @@ let rec ho_whd f c m x =
    whd aux c m x
    
 let ho_whd f st c t =
-   if !G.trace >= level then log1 st "Now scanning" c t;
+   if !G.ct >= level then log1 st "Now scanning" c t;
    ho_whd f c empty_machine t
 
 let rec are_convertible f st a c m1 t1 m2 t2 =
@@ -132,7 +132,7 @@ let rec are_convertible f st a c m1 t1 m2 t2 =
    let rec aux m1 r1 m2 r2 =
 (*   L.warn "entering R.are_convertible_aux"; *)
    let u, t = term_of_whdr r1, term_of_whdr r2 in
-   if !G.trace >= level then log2 st "Now really converting" c u c t;   
+   if !G.ct >= level then log2 st "Now really converting" c u c t;   
    match r1, r2 with
       | Sort_ h1, Sort_ h2                                 ->
          if h1 = h2 then f a else f false 
@@ -189,5 +189,5 @@ and are_convertible_stacks f st a c m1 m2 =
       C.list_fold_left2 f map a m1.s m2.s
 
 let are_convertible f st c u t = 
-   if !G.trace >= level then log2 st "Now converting" c u c t;
+   if !G.ct >= level then log2 st "Now converting" c u c t;
    are_convertible f st true c empty_machine u empty_machine t
index b6f3deb558624b69369345836b0cf539542c2169..009a2eaf9ec5e08d673881df3b43bdf6156fbc46 100644 (file)
@@ -45,11 +45,11 @@ let mk_gref u l =
 
 let rec b_type_of err f st c x = 
 (*   L.warn "Entering T.b_type_of"; *)
-   if !G.trace >= level then log1 st "Now checking" c x;
+   if !G.ct >= level then log1 st "Now checking" c x;
    match x with
-   | Z.Sort h                    ->
+   | Z.Sort h                   ->
       let h = H.apply h in f x (Z.Sort h) 
-   | Z.LRef i                    ->
+   | Z.LRef i                   ->
       let err0 () = error1 err "variable not found" c x in
       let f _ = function
          | Z.Abst w               -> f x w
@@ -58,7 +58,7 @@ let rec b_type_of err f st c x =
         | Z.Void                 -> error1 err "reference to excluded variable" c x     
       in
       Z.get err0 f c i
-   | Z.GRef uri                  ->
+   | Z.GRef uri                 ->
       let f = function
          | _, _, _, E.Abst w               -> f x w
         | _, _, _, E.Abbr (Z.Cast (w, v)) -> f x w
@@ -90,10 +90,10 @@ let rec b_type_of err f st c x =
       in
       let f cc = b_type_of err f st cc t in
       Z.push "type void" f c a l Z.Void   
-   | Z.Appl (v, t)            ->
+   | Z.Appl (v, t)              ->
       let f xv vv xt tt = function
         | ZR.Abst w                             -> 
-           if !G.trace > level then L.log st ZO.specs level (L.t_items1 "Just scanned" c w);
+           if !G.ct > level then L.log st ZO.specs level (L.t_items1 "Just scanned" c w);
            let f a =                
 (*            L.warn (Printf.sprintf "Convertible: %b" a); *)
               if a then f (S.sh2 v xv t xt x Z.appl) (Z.appl xv tt)
@@ -106,7 +106,7 @@ let rec b_type_of err f st c x =
       let f xv vv xt tt = ZR.ho_whd (f xv vv xt tt) st c tt in
       let f xv vv = b_type_of err (f xv vv) st c t in
       type_of err f st c v
-   | Z.Cast (u, t)            ->
+   | Z.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 Z.cast) xu else error3 err c xt tt xu
index 7be7dc939fb41834136e4b31b02ef08946dbcce8..a321a32b00e71b20a7ef13cd1583bbc29e92fbe2 100644 (file)
@@ -23,12 +23,12 @@ type bind = Void                          (*                         *)
           | Abst of bool * N.layer * term (* x-reduced?, layer, type *)
           | Abbr of term                  (* body                    *)
 
-and term = Sort of attrs * int         (* attrs, hierarchy index *)
-         | LRef of attrs * int         (* attrs, position index *)
-         | GRef of attrs * uri         (* attrs, reference *)
-         | Cast of attrs * term * term (* attrs, type, term *)
-         | Appl of attrs * term * term (* attrs, argument, function *)
-         | Bind of attrs * bind * term (* attrs, binder, scope *)
+and term = Sort of attrs * int                (* attrs, hierarchy index *)
+         | LRef of attrs * int                (* attrs, position index *)
+         | GRef of attrs * uri                (* attrs, reference *)
+         | Cast of attrs * term * term        (* attrs, type, term *)
+         | Appl of attrs * bool * term * term (* attrs, extended?, argument, function *)
+         | Bind of attrs * bind * term        (* attrs, binder, scope *)
 
 type entity = term E.entity (* attrs, uri, binder *)
 
@@ -40,7 +40,7 @@ type manager = (N.status -> entity -> bool) * (unit -> unit)
 
 (* Currified constructors ***************************************************)
 
-let abst x n w = Abst (x, n, w)
+let abst r n w = Abst (r, n, w)
 
 let abbr v = Abbr v
 
@@ -48,11 +48,11 @@ let lref a i = LRef (a, i)
 
 let cast a u t = Cast (a, u, t)
 
-let appl a u t = Appl (a, u, t)
+let appl a x u t = Appl (a, x, u, t)
 
 let bind a b t = Bind (a, b, t)
 
-let bind_abst x n a u t = Bind (a, Abst (x, n, u), t)
+let bind_abst r n a u t = Bind (a, Abst (r, n, u), t)
 
 let bind_abbr a u t = Bind (a, Abbr u, t)
 
index 1715494d49043309693f4fe944de619acc6ece03..645610dd44f4c62db2570a2d2d5888b0904a9ee3 100644 (file)
@@ -18,25 +18,25 @@ module B = Brg
 (* internal functions: crg to brg term **************************************)
 
 let rec xlate_term f = function
-   | D.TSort (a, l)     -> f (B.Sort (a, l))
-   | D.TGRef (a, n)     -> f (B.GRef (a, n))
-   | D.TLRef (a, i)     -> f (B.LRef (a, i))
-   | D.TCast (a, u, t)  ->
+   | D.TSort (a, l)       -> f (B.Sort (a, l))
+   | D.TGRef (a, n)       -> f (B.GRef (a, n))
+   | D.TLRef (a, i)       -> f (B.LRef (a, i))
+   | D.TCast (a, u, t)    ->
       let f tt uu = f (B.Cast (a, uu, tt)) in
       let f tt = xlate_term (f tt) u in
       xlate_term f t 
-   | D.TAppl (a, v, t) ->
-      let f tt vv = f (B.Appl (a, vv, tt)) in
+   | D.TAppl (a, x, v, t) ->
+      let f tt vv = f (B.Appl (a, x, vv, tt)) in
       let f tt = xlate_term (f tt) v in
       xlate_term f t 
-   | D.TProj (_, e, t)  -> 
+   | D.TProj (_, e, t)    -> 
       D.shift (xlate_term f) e t
-   | D.TBind (a, b, t)  -> 
+   | D.TBind (a, b, t)    -> 
       xlate_term (xlate_bind f a b) t
 
 and xlate_bind f a b t = match b with
-   | D.Abst (x, n, w) ->
-      let f ww = f (B.Bind (a, B.Abst (x, n, ww), t)) in 
+   | D.Abst (r, n, w) ->
+      let f ww = f (B.Bind (a, B.Abst (r, n, ww), t)) in 
       xlate_term f w
    | D.Abbr v         ->
       let f vv = f (B.Bind (a, B.Abbr vv, t)) in 
@@ -47,25 +47,25 @@ and xlate_bind f a b t = match b with
 (* internal functions: brg to crg term **************************************)
 
 let rec xlate_bk_term f = function
-   | B.Sort (a, l)     -> f (D.TSort (a, l))
-   | B.GRef (a, n)     -> f (D.TGRef (a, n))
-   | B.LRef (a, i)     -> f (D.TLRef (a, i))
-   | B.Cast (a, u, t)  ->
+   | B.Sort (a, l)       -> f (D.TSort (a, l))
+   | B.GRef (a, n)       -> f (D.TGRef (a, n))
+   | B.LRef (a, i)       -> f (D.TLRef (a, i))
+   | B.Cast (a, u, t)    ->
       let f tt uu = f (D.TCast (a, uu, tt)) in
       let f tt = xlate_bk_term (f tt) u in
       xlate_bk_term f t 
-   | B.Appl (a, u, t)  ->
-      let f tt uu = f (D.TAppl (a, uu, tt)) in
+   | B.Appl (a, x, u, t) ->
+      let f tt uu = f (D.TAppl (a, x, uu, tt)) in
       let f tt = xlate_bk_term (f tt) u in
       xlate_bk_term f t 
-   | B.Bind (a, b, t)  ->
+   | B.Bind (a, b, t)    ->
       let f tt bb = f (D.TBind (a, bb, tt)) in
       let f tt = xlate_bk_bind (f tt) b in
       xlate_bk_term f t 
 
 and xlate_bk_bind f = function
-   | B.Abst (x, n, t) ->
-      let f tt = f (D.Abst (x, n, tt)) in
+   | B.Abst (r, n, t) ->
+      let f tt = f (D.Abst (r, n, tt)) in
       xlate_bk_term f t
    | B.Abbr t         ->
       let f tt = f (D.Abbr tt) in
index 0ead752807986204f85ca6db85fddd71a87fb6da..969cb8ae99f8c7e298abe89699a3ee021bd0d34e 100644 (file)
@@ -24,7 +24,7 @@ module B  = Brg
 
 let ok = ref true
 
-let level = ref 0
+let uris = ref []
 
 let base = "elpi"
 
@@ -74,7 +74,7 @@ let out_name och a =
 
 let rec out_term st e och = function
    | B.Sort (_, h)                   ->
-      let sort = if h = 0 then "k+0" else if h = 1 then "k+1" else assert false in
+      let sort = if h = 0 then "k+set" else if h = 1 then "k+prop" else assert false in
       KP.fprintf och "(sort %s)" sort
    | B.LRef (_, i)                   ->
       let _, _, a, b = B.get e i in
@@ -83,12 +83,13 @@ let rec out_term st e och = function
       KP.fprintf och "%a" out_uri s
    | B.Cast (_, u, t)                ->
       KP.fprintf och "(cast %a %a)" (out_term st e) u (out_term st e) t 
-   | B.Appl (_, v, t)                ->
-      KP.fprintf och "(appr %a %a)" (out_term st e) v (out_term st e) t
-   | B.Bind (a, B.Abst (x, n, w), t) ->
+   | B.Appl (_, x, v, t)             ->
+      let c = if x then "appx" else "appr" in
+      KP.fprintf och "(%s %a %a)" c (out_term st e) v (out_term st e) t
+   | B.Bind (a, B.Abst (r, n, w), t) ->
       let a = R.alpha B.mem e a in
-      let ee = B.push e B.empty a (B.abst x n w) in
-      let c = if x then "prod" else "abst" in
+      let ee = B.push e B.empty a (B.abst r n w) in
+      let c = if r then "prod" else "abst" in
       let l = match N.to_string st n with
          | "1" -> "l+1"
          | "2" -> "l+2"
@@ -107,35 +108,75 @@ let rec out_term st e och = function
       KP.fprintf och "(void %a\\ %a)"
           out_name a (out_term st ee) t
 
-let output_entity och st (_, na, s, b) =
+(* variant 1 *************************************************)
+
+let output_entity_1 och st (_, na, s, b) =
 (*   if na.E.n_apix <= 4500 then begin *)
-   out_comment och (KP.sprintf "constant %u" na.E.n_apix);
+(*   out_comment och (KP.sprintf "constant %u" na.E.n_apix); *)
    match b with
       | E.Abbr t ->
-         KP.fprintf och "(gdef c+%u %a\n %a\\\n" na.E.n_apix (out_term st B.empty) t out_uri s;
-         incr level; !ok
+         KP.fprintf och "(gdef+1 c+%u %a\n %a\\\n" na.E.n_apix (out_term st B.empty) t out_uri s;
+         uris := (true, s) :: !uris; !ok
       | E.Abst u ->
-         KP.fprintf och "(gdec c+%u %a\n%a\\\n" na.E.n_apix (out_term st B.empty) u out_uri s;
-         incr level; !ok
+         KP.fprintf och "(gdec+1 c+%u %a\n%a\\\n" na.E.n_apix (out_term st B.empty) u out_uri s;
+         uris := (false, s) :: !uris; !ok
       | E.Void   -> C.err ()
 (*   end else !ok *)
 
-let close_out och () =
-   let rec aux () =
-      if !level <= 0 then KP.fprintf och "%s" "\n\n).\n" 
-      else begin KP.fprintf och "%s" ")"; decr level; aux () end
+let close_out_1 och () =
+   let aux_sep _ = KP.fprintf och "%s" ")" in
+   KP.fprintf och "%s" "gtop";   
+   List.iter aux_sep !uris;
+   out_clause och "\n\n).";
+   close_out och
+
+(* Variant 2 *************************************************)
+
+let output_entity_2 och st (_, na, s, b) =
+(*   out_comment och (KP.sprintf "constant %u" na.E.n_apix); *)
+(*   if na.E.n_apix <= 9 then begin *)
+   match b with
+      | E.Abbr t ->
+         KP.fprintf och "g+line %a c+%u\n       %a\n.\n\n"
+            out_uri s na.E.n_apix (out_term st B.empty) t;
+         uris := (true, s) :: !uris; !ok
+      | E.Abst u ->
+         KP.fprintf och "g+line %a c+%u\n       %a\n.\n\n"
+            out_uri s na.E.n_apix (out_term st B.empty) u;
+         uris := (false, s) :: !uris; !ok
+      | E.Void   -> C.err ()
+(*   end else !ok *)
+
+let close_out_2 och () =
+   let aux_name (b, s) =
+      let gde = if b then "gdef+2" else "gdec+2" in 
+      KP.fprintf och "(%s %a\n" gde out_uri s
    in
+   let aux_sep _ = KP.fprintf och "%s" ")" in
+   out_clause och "main :- grundlagen.";
+   out_clause och "grundlagen :- (gv+ ";
+   List.iter aux_name (List.rev !uris);
    KP.fprintf och "%s" "gtop";
-   aux (); close_out och
+   List.iter aux_sep !uris;
+   out_clause och "\n\n).";
+   close_out och
 
 (* Interface functions ******************************************************)
 
-let open_out fname =
+let open_out_1 fname =
    let dir = KF.concat !G.manager_dir base in 
    let path = KF.concat dir fname in
-   let och = open_out (path ^ ext) in
+   let och = open_out (path ^ "1" ^ ext) in
    out_preamble och;
    out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
    out_clause och "main :- grundlagen.";
    out_clause och "grundlagen :- gv+ (";
-   output_entity och, close_out och
+   output_entity_1 och, close_out_1 och
+
+let open_out_2 fname =
+   let dir = KF.concat !G.manager_dir base in 
+   let path = KF.concat dir fname in
+   let och = open_out (path ^ "2" ^ ext) in
+   out_preamble och;
+   out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
+   output_entity_2 och, close_out_2 och
index d96b7f45db65866224a1bcafcba92be4837d2b34..96c16ec374871ec81a95707f211245757e0e33e8 100644 (file)
@@ -9,4 +9,6 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-val open_out: string -> Brg.manager
+val open_out_1: string -> Brg.manager
+
+val open_out_2: string -> Brg.manager
index c886c27f492697db0283ece732bb4ef80e2039df..caa8ab4650b47cc27c1c240289d693ed600c3bf5 100644 (file)
@@ -85,15 +85,15 @@ let rec out_term st p e och = function
       KP.fprintf och "%a" out_uri s
    | B.Cast (_, u, t)                ->
       KP.fprintf och "(%a : %a)" (out_term st false e) t (out_term st false e) u 
-   | B.Appl (_, v, t)                ->
+   | B.Appl (_, _, v, t)             ->
       let pt = match t with B.Appl _ -> false | _ -> true in
       let op, cp = if p then "(", ")" else "", "" in
       KP.fprintf och "%s%a %a%s" op (out_term st pt e) t (out_term st true e) v cp
-   | B.Bind (a, B.Abst (x, n, w), t) ->
+   | B.Bind (a, B.Abst (r, n, w), t) ->
       let p = true in
       let op, cp = if p then "(", ")" else "", "" in
       let a = R.alpha B.mem e a in
-      let ee = B.push e B.empty a (B.abst x n w) in
+      let ee = B.push e B.empty a (B.abst r n w) in
       let ob, cb = match N.to_string st n with
          | "1" -> "forall", ","
          | "2" -> "fun", " =>"
index e6b8cd8da35014de6d45ae0e9759751cbff0bcfb..71b189dacc39263dd14e2f96fdb3bd35a420047f 100644 (file)
@@ -80,14 +80,14 @@ let rec out_term st p e och = function
       KP.fprintf och "%a" out_uri s
    | B.Cast (_, u, t)                ->
       KP.fprintf och "(%a : %a)" (out_term st false e) t (out_term st false e) u 
-   | B.Appl (_, v, t)                ->
+   | B.Appl (_, _, v, t)             ->
       let pt = match t with B.Appl _ -> false | _ -> true in
       let op, cp = if p then "(", ")" else "", "" in
       KP.fprintf och "%s%a %a%s" op (out_term st pt e) t (out_term st true e) v cp
-   | B.Bind (a, B.Abst (x, n, w), t) ->
+   | B.Bind (a, B.Abst (r, n, w), t) ->
       let op, cp = if p then "(", ")" else "", "" in
       let a = R.alpha B.mem e a in
-      let ee = B.push e B.empty a (B.abst x n w) in
+      let ee = B.push e B.empty a (B.abst r n w) in
       let binder = match N.to_string st n, a.E.n_sort with
          | "1", 0 -> "Π"
          | "1", 1 -> "∀"
index ac873ec6677dd24cdc27c8745edb996b6baea16f..5153ced0765a57d98d7fab2dd27183e237d07936 100644 (file)
@@ -63,9 +63,9 @@ let rec count_term_binder f c e = function
       f c
 
 and count_term f c e = function
-   | B.Sort _         -> 
+   | B.Sort _            ->
       f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
-   | B.LRef (_, i)    -> 
+   | B.LRef (_, i)       ->
       begin match B.get e i with
         | _, _, _, B.Abst _
         | _, _, _, B.Void   ->
@@ -73,22 +73,22 @@ and count_term f c e = function
         | _, _, _, B.Abbr _ ->
            f {c with tlrefs = succ c.tlrefs; xnodes = succ c.xnodes}
       end      
-   | B.GRef (_, u)    -> 
+   | B.GRef (_, u)       -> 
       let c =    
         if Cps.list_mem ~eq:U.eq u c.uris
         then {c with nodes = succ c.nodes}
         else {c with xnodes = succ c.xnodes}
       in
       f {c with tgrefs = succ c.tgrefs}
-   | B.Cast (_, v, t) -> 
+   | B.Cast (_, v, t)    -> 
       let c = {c with tcasts = succ c.tcasts} in
       let f c = count_term f c e t in
       count_term f c e v
-   | B.Appl (_, v, t) -> 
+   | B.Appl (_, _, v, t) -> 
       let c = {c with tappls = succ c.tappls; nodes = succ c.nodes} in
       let f c = count_term f c e t in
       count_term f c e v
-   | B.Bind (a, b, t) -> 
+   | B.Bind (a, b, t)    -> 
       let f c = count_term f c (B.push e B.empty a b) t in
       count_term_binder f c e b
 
@@ -155,12 +155,12 @@ let rec pp_term st e och = function
       KP.fprintf och "$%s" (U.string_of_uri s)
    | B.Cast (_, u, t)                ->
       KP.fprintf och "{%a}.%a" (pp_term st e) u (pp_term st e) t
-   | B.Appl (_, v, t)                ->
+   | B.Appl (_, _, v, t)             ->
       KP.fprintf och "(%a).%a" (pp_term st e) v (pp_term st e) t
-   | B.Bind (a, B.Abst (x, n, w), t) ->
+   | B.Bind (a, B.Abst (r, n, w), t) ->
       let a = R.alpha B.mem e a in
-      let ee = B.push e B.empty a (B.abst x n w) in
-      KP.fprintf och "%a%a[%a:%a].%a" (pp_level st) n pp_reduced x (name C.start) a (pp_term st e) w (pp_term st ee) t
+      let ee = B.push e B.empty a (B.abst r n w) in
+      KP.fprintf och "%a%a[%a:%a].%a" (pp_level st) n pp_reduced r (name C.start) a (pp_term st e) w (pp_term st ee) t
    | B.Bind (a, B.Abbr v, t)         ->
       let a = R.alpha B.mem e a in
       let ee = B.push e B.empty a (B.abbr v) in
index bb31fc9768a77d98c7e8150b4003206d58c1774b..6c5ac1e9809e0fe6e83026da1703f1b2770fbc64 100644 (file)
@@ -55,21 +55,21 @@ let zero = Some 0
 let are_alpha_convertible err f t1 t2 =
    let rec aux f = function
       | B.Sort (_, p1), B.Sort (_, p2)
-      | B.LRef (_, p1), B.LRef (_, p2)         ->
+      | B.LRef (_, p1), B.LRef (_, p2)               ->
          if p1 = p2 then f () else err ()
-      | B.GRef (_, u1), B.GRef (_, u2)         ->
+      | B.GRef (_, u1), B.GRef (_, u2)               ->
          if U.eq u1 u2 then f () else err ()
       | B.Cast (_, v1, t1), B.Cast (_, v2, t2)         
-      | B.Appl (_, v1, t1), B.Appl (_, v2, t2) ->
+      | B.Appl (_, _, v1, t1), B.Appl (_, _, v2, t2) ->
          let f _ = aux f (t1, t2) in
         aux f (v1, v2)
-      | B.Bind (_, b1, t1), B.Bind (_, b2, t2) ->
+      | B.Bind (_, b1, t1), B.Bind (_, b2, t2)       ->
          let f _ = aux f (t1, t2) in
         aux_bind f (b1, b2)
-      | _                                      -> err ()
+      | _                                            -> err ()
    and aux_bind f = function
       | B.Abbr v1, B.Abbr v2                                             -> aux f (v1, v2)
-      | B.Abst (x1, n1, v1), B.Abst (x2, n2, v2) when x1 = x2 && n1 = n2 -> aux f (v1, v2)
+      | B.Abst (r1, n1, v1), B.Abst (r2, n2, v2) when r1 = r2 && n1 = n2 -> aux f (v1, v2)
       | B.Void, B.Void                                                   -> f ()
       | _                                                                -> err ()
    in
@@ -92,7 +92,7 @@ let get m i =
 
 (* to share *)
 let rec step st m r = 
-   if !G.trace >= sublevel then 
+   if !G.ct >= sublevel then 
    log1 st (Printf.sprintf "entering R.step: l=%u, n=%s," m.l (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e r;
    match r with
    | B.Sort (a, h)                       ->
@@ -102,7 +102,7 @@ let rec step st m r =
    | B.GRef (_, uri)                     ->
       begin match BE.get_entity uri with
          | _, _, _, E.Abbr v ->
-            if m.n = None || !G.expand then begin
+            if !G.expand then begin
               if !G.summary then O.add ~gdelta:1 ();
                step st m v
             end else
@@ -138,7 +138,7 @@ let rec step st m r =
          if !G.summary then O.add ~epsilon:1 ();
          step st m t
       end
-   | B.Appl (_, v, t)                    ->
+   | B.Appl (_, _, v, t)                 ->
       step st {m with s = (m.e, v) :: m.s} t   
    | B.Bind (a, B.Abst (false, n, w), t) ->
       let i = tsteps m in
@@ -183,7 +183,7 @@ let push m a b =
    {m with e = e; l = l}
 
 let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
-   if !G.trace >= level then log2 st "Now converting nfs" m1.e t1 m2.e t2;
+   if !G.ct >= level then log2 st "Now converting nfs" m1.e t1 m2.e t2;
    match t1, r1, t2, r2 with
       | B.Sort (_, h1), _, B.Sort (_, h2), _               ->
          h1 = h2
@@ -238,6 +238,15 @@ and ac_stacks st m1 m2 =
    in
    list_and map (m1.s, m2.s)
 
+let rec ih_nfs st (m, t, r) =
+   match t, r with
+      | B.GRef _, Some v ->
+        if !G.summary then O.add ~gdelta:1 ();
+        ih st m v
+      | _                -> m, t
+
+and ih st m t = ih_nfs st (step st m t)
+
 (* Interface functions ******************************************************)
 
 let empty_rtm = { 
@@ -249,12 +258,11 @@ let get m i =
    let _, _, _, b = B.get m.e i in b
 
 let xwhd st m n t =
-   if !G.trace >= level then log1 st "Now scanning" m.e t;   
-   let m, t, _ = step st (reset m n) t in
-   m, t
+   if !G.ct >= level then log1 st "Now scanning" m.e t;   
+   ih st (reset m n) t
 
 let are_convertible st m1 n1 t1 m2 n2 t2 = 
-   if !G.trace >= level then log2 st "Now converting" m1.e t1 m2.e t2;
+   if !G.ct >= level then log2 st "Now converting" m1.e t1 m2.e t2;
    let r = ac st (reset m1 n1) t1 (reset m2 n2) t2 in
    r
 (*    let err _ = in 
index fe5915f74ac5aa99644b0161ee6fd87642cca8e2..5661982a3b8101db11d69b4249577303e2135823 100644 (file)
@@ -18,22 +18,22 @@ let rec icm a = function
    | B.GRef _                        -> succ a
    | B.Bind (_, B.Void, t)           -> icm (succ a) t
    | B.Cast (_, u, t)                -> icm (icm a u) t
-   | B.Appl (_, u, t)
+   | B.Appl (_, _, u, t)
    | B.Bind (_, B.Abst (_, _, u), t)
    | B.Bind (_, B.Abbr u, t)         -> icm (icm (succ a) u) t
 
 let iter map d =
    let rec iter_bind d = function
       | B.Void           -> B.Void
-      | B.Abst (x, n, w) -> B.Abst (x, n, iter_term d w)
+      | B.Abst (r, n, w) -> B.Abst (r, n, iter_term d w)
       | B.Abbr v         -> B.Abbr (iter_term d v)
    and iter_term d = function
-      | B.Sort _ as t      -> t
-      | B.GRef _ as t      -> t
+      | B.Sort _ as t       -> t
+      | B.GRef _ as t       -> t
       | B.LRef (a, i) as t -> if i < d then t else map d a i
-      | B.Cast (a, w, v)   -> B.Cast (a, iter_term d w, iter_term d v)
-      | B.Appl (a, w, u)   -> B.Appl (a, iter_term d w, iter_term d u)
-      | B.Bind (a, b, u)   -> B.Bind (a, iter_bind d b, iter_term (succ d) u)
+      | B.Cast (a, w, v)    -> B.Cast (a, iter_term d w, iter_term d v)
+      | B.Appl (a, x, w, u) -> B.Appl (a, x, iter_term d w, iter_term d u)
+      | B.Bind (a, b, u)    -> B.Bind (a, iter_bind d b, iter_term (succ d) u)
    in
    iter_term d
 
index 929dcbce85457955f7d7c4b9e9d8bda1141d9b79..15b0b851cccb8326761472db7111f9d50d0261f2 100644 (file)
@@ -55,8 +55,9 @@ let assert_convertibility err f st m u w v =
    if BR.are_convertible st m zero u m zero w then f () else
    error3 err m v w u
 
-let assert_applicability err f st m u w v =
-   match BR.xwhd st m None u with 
+let assert_applicability err f st m x u w v =
+   let mode = if x then None else zero in
+   match BR.xwhd st m mode u with 
       | _, B.Sort _                            ->
          error1 err "not a function type" m u
       | mu, B.Bind (_, B.Abst (true, n, u), _) -> 
@@ -65,32 +66,32 @@ 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 m r =
-   if !G.trace >= level then log1 st "Now checking" m r;
-   match r with
+let rec b_type_of err f st m y =
+   if !G.ct >= level then log1 st "Now checking" m y;
+   match y with
    | B.Sort (a, h)                   ->
-      let h = H.apply h in f r (B.Sort (a, h)) 
+      let h = H.apply h in f y (B.Sort (a, h)) 
    | B.LRef (_, i)                   ->
       begin match BR.get m i with
          | B.Abst (_, _, w)          ->
-           f r (BS.lift (succ i) (0) w)
+           f y (BS.lift (succ i) (0) w)
         | B.Abbr (B.Cast (_, w, _)) -> 
-           f r (BS.lift (succ i) (0) w)
+           f y (BS.lift (succ i) (0) w)
         | B.Abbr _                  -> assert false
         | B.Void                    -> 
-           error1 err "reference to excluded variable" m r
+           error1 err "reference to excluded variable" m y
       end
    | B.GRef (_, uri)                 ->
       begin match BE.get_entity uri with
-         | _, _, _, E.Abst w                  -> f r w
-        | _, _, _, E.Abbr (B.Cast (_, w, _)) -> f r w
+         | _, _, _, E.Abst w                  -> f y w
+        | _, _, _, E.Abbr (B.Cast (_, w, _)) -> f y w
         | _, _, _, E.Abbr _                  -> assert false
         | _, _, _, E.Void                    ->
-            error1 err "reference to unknown entry" m r
+            error1 err "reference to unknown entry" m y
       end
    | B.Bind (a, B.Abbr v, t)         ->
       let f rv rt tt =
-         f (S.sh2 v rv t rt r (B.bind_abbr a)) (B.bind_abbr a rv tt)
+         f (S.sh2 v rv t rt y (B.bind_abbr a)) (B.bind_abbr a rv tt)
       in
       let f rv m = b_type_of err (f rv) st m t in
       let f rv = f rv (BR.push m a (B.abbr rv)) in
@@ -99,28 +100,28 @@ let rec b_type_of err f st m r =
          | _        -> f (B.Cast (E.empty_node, vv, rv))
       in
       type_of err f st m v
-   | B.Bind (a, B.Abst (x, n, u), t) ->
+   | B.Bind (a, B.Abst (r, n, u), t) ->
       let f ru rt tt =
-        f (S.sh2 u ru t rt r (B.bind_abst x n a)) (B.bind_abst x (N.minus st n 1) a ru tt)
+        f (S.sh2 u ru t rt y (B.bind_abst r n a)) (B.bind_abst r (N.minus st n 1) a ru tt)
       in
       let f ru m = b_type_of err (f ru) st m t in
-      let f ru _ = f ru (BR.push m a (B.abst x n ru)) in
+      let f ru _ = f ru (BR.push m a (B.abst r n ru)) in
       type_of err f st m u
    | B.Bind (a, B.Void, t)           ->
       let f rt tt = 
-         f (S.sh1 t rt r (B.bind_void a)) (B.bind_void a tt)
+         f (S.sh1 t rt y (B.bind_void a)) (B.bind_void a tt)
       in
       b_type_of err f st (BR.push m a B.Void) t
-   | B.Appl (a, v, t)                ->
+   | B.Appl (a, x, v, t)             ->
       let f rv vv rt tt = 
-         let f _ = f (S.sh2 v rv t rt r (B.appl a)) (B.appl a rv tt) in
-         assert_applicability err f st m tt vv rv
+         let f _ = f (S.sh2 v rv t rt y (B.appl a x)) (B.appl a x rv tt) in
+         assert_applicability err f st m tt vv rv
       in
       let f rv vv = b_type_of err (f rv vv) st m t in
       type_of err f st m v
    | B.Cast (a, u, t)                ->
       let f ru rt tt =  
-        let f _ = f (S.sh2 u ru t rt r (B.cast a)) ru in
+        let f _ = f (S.sh2 u ru t rt y (B.cast a)) ru in
          assert_convertibility err f st m ru tt rt
       in
       let f ru _ = b_type_of err (f ru) st m t in
@@ -128,4 +129,4 @@ let rec b_type_of err f st m r =
 
 (* Interface functions ******************************************************)
 
-and type_of err f st m r = b_type_of err f st m r
+and type_of err f st m t = b_type_of err f st m t
index 8425774d2a6bc890cb4cd439b67fec74ee9ab24c..877fee9d8380e6f739d237ed385660a3e446bfb7 100644 (file)
@@ -44,7 +44,7 @@ let validate err f st e =
    let uri, t = match e with
       | _, _, uri, E.Abst t -> uri, t
       | _, _, uri, E.Abbr t -> uri, t
-      | _, _, _,   E.Void   -> assert false
+      | _, _, _,    E.Void   -> assert false
    in
    let err msg = err (L.Uri uri :: msg) in
    let f () = let _ = BE.set_entity e in f () in
index ad4154fc17241316160c8405211210d7471720ee..c616b22df68c023eedc60257548cc96d9279a446 100644 (file)
@@ -46,41 +46,42 @@ let zero = Some 0
 let one = Some 1
 
 let assert_convertibility err f st m u t =
-   if !G.trace >= level then warn "Asserting convertibility for cast";
+   if !G.ct >= level then warn "Asserting convertibility for cast";
    if BR.are_convertible st m zero u m one t then f () else
    error2 err m u m t
 
-let assert_applicability err f st m v t =
-   if !G.trace >= level then warn "Asserting applicability";
-   match BR.xwhd st m None t with 
-      | _, B.Sort _                            ->
-         error1 err "not a function" m t
+let assert_applicability err f st m x v t =
+   let mode, msg = if x then None, "extended" else one, "restricted" in 
+   if !G.ct >= level then warn ("Asserting " ^ msg ^ " applicability");
+   match BR.xwhd st m mode t with 
       | mw, B.Bind (_, B.Abst (true, n, w), _) ->
          if !G.cc && not (N.assert_not_zero st n) then error1 err "not a function" m t
          else begin
-            if !G.trace >= level then warn "Asserting convertibility for application";
+            if !G.ct >= level then warn "Asserting convertibility for application";
             if BR.are_convertible st mw zero w m one v then f () else
            error2 err mw w m v
          end
-      | _                                -> assert false (**)
+      | _, B.Sort _                            ->
+         error1 err "not a function" m t
+      | _                                      -> assert false (**)
 
-let rec b_validate err f st m x =
-   if !G.trace >= level then log1 st "Now checking" m x;
-   match x with
+let rec b_validate err f st m y =
+   if !G.ct >= level then log1 st "Now checking" m y;
+   match y with
    | B.Sort _         -> f ()
    | B.LRef (_, i)    ->
       begin match BR.get m i with
          | B.Abst _
         | B.Abbr _ -> f ()
         | B.Void   -> 
-           error1 err "reference to excluded variable" m x
+           error1 err "reference to excluded variable" m y
       end
    | B.GRef (_, uri)  ->
       begin match BE.get_entity uri with
          | _, _, _, E.Abst _
         | _, _, _, E.Abbr _ -> f ()
         | _, _, _, E.Void   ->
-            error1 err "reference to unknown entry" m x
+            error1 err "reference to unknown entry" m y
       end
    | B.Bind (a, b, t) ->
       let f () = b_validate err f st (BR.push m a b) t in
@@ -89,8 +90,8 @@ let rec b_validate err f st m x =
          | B.Abbr v         -> validate err f st m v
          | B.Void           -> f ()
       end
-   | B.Appl (_, v, t)        ->
-      let f () = assert_applicability err f st m v t in
+   | B.Appl (_, x, v, t)    ->
+      let f () = assert_applicability err f st m v t in
       let f () = b_validate err f st m t in
       validate err f st m v
    | B.Cast (_, u, t)        ->
@@ -100,4 +101,4 @@ let rec b_validate err f st m x =
 
 (* Interface functions ******************************************************)
 
-and validate err f st m x = b_validate err f st m x
+and validate err f st m t = b_validate err f st m t
index ede703d6d787a958ab576c5b89d44470f301d7c4..1ad6cf28cae6b5522bbb37cc33ba6c720d6e1c3c 100644 (file)
@@ -85,18 +85,18 @@ let rec generated st h i =
    let k, n = resolve_key_with_default st default k in 
    if n.s then generated st h i else begin
       if n <> default then KH.replace st k default;
-      if !G.trace >= level then pp_table st; default
+      if !G.ct >= level then pp_table st; default
    end
 
 let assert_finite st n j =
-   if !G.trace >= level then warn (Printf.sprintf "ASSERT FINITE %u" j);
+   if !G.ct >= level then warn (Printf.sprintf "ASSERT FINITE %u" j);
    let rec aux (k, n) j = match n.v with    
       | Fin i when i = j -> true
       | Fin i            ->
          Printf.printf "binder %s is %u but must be %u\n" (P.string_of_mark k) i j; true (**)
       | Inf              ->
          Printf.printf "binder %s is infinite but must be %u\n" (P.string_of_mark k) j; true (**)
-      | Unk              -> n.v <- Fin j; if !G.trace >= level then pp_table st; true
+      | Unk              -> n.v <- Fin j; if !G.ct >= level then pp_table st; true
       | Ref (k, i)       -> n.v <- Fin j; aux (resolve_key st k) (i+j) 
    in
    let k, n = resolve_layer st n in
@@ -106,12 +106,12 @@ let assert_finite st n j =
       aux (k, n) j
 
 let assert_infinite st n =
-   if !G.trace >= level then warn "ASSERT INFINITE";
+   if !G.ct >= level then warn "ASSERT INFINITE";
    let rec aux (k, n) = match n.v with
       | Inf        -> true
       | Fin i      -> 
          Printf.printf "binder %s is %u but must be infinite\n" (P.string_of_mark k) i; true (**)
-      | Unk        -> n.v <- Inf; if !G.trace >= level then pp_table st; true
+      | Unk        -> n.v <- Inf; if !G.ct >= level then pp_table st; true
       | Ref (k, _) -> n.v <- Inf; aux (resolve_key st k) 
    in
    aux (resolve_layer st n)
@@ -132,19 +132,19 @@ let one = finite 1
 let two = finite 2
 
 let rec unknown st =
-   if !G.trace >= level then warn "UNKNOWN";
+   if !G.ct >= level then warn "UNKNOWN";
    let default = empty () in
    let k = P.new_mark () in
    let k, n = resolve_key_with_default st default k in
    if n.s then match n.v with
       | Inf
       | Fin _ -> n
-      | Unk   -> if !G.trace >= level then pp_table st; cell true (Ref (k, 0))
+      | Unk   -> if !G.ct >= level then pp_table st; cell true (Ref (k, 0))
       | Ref _ -> assert false
    else unknown st
  
 let minus st n j =
-   if !G.trace >= level then warn (Printf.sprintf "MINUS %u" j);
+   if !G.ct >= level then warn (Printf.sprintf "MINUS %u" j);
    let rec aux k n j = match n.v with
       | Inf              -> cell false n.v
       | Fin i when i > j -> cell false (Fin (i - j))
@@ -163,14 +163,14 @@ let to_string st n =
    string_of_value k n.v
 
 let assert_not_zero st n =
-   if !G.trace >= level then warn "ASSERT NOT ZERO";
+   if !G.ct >= level then warn "ASSERT NOT ZERO";
    let k, n = resolve_layer st n in
    match n.b, n.v with
       | true, _                -> n.b
 (*      | _   , Fin i when i = 0 ->   
          Printf.printf "^Pi reduction on binder %s\n" (P.string_of_mark k); false *) (**)
 (*      if n.s && n.v = Fin 1 then Printf.printf "Pi reduction on binder %s\n" (P.string_of_mark k); *)      
-      | _                      -> n.b <- true; if !G.trace >= level then pp_table st; n.b
+      | _                      -> n.b <- true; if !G.ct >= level then pp_table st; n.b
 
 let assert_zero st n = assert_finite st n 0
 
@@ -186,9 +186,9 @@ let assert_equal st n1 n2 =
          | Ref _ -> assert false
       else false
    in begin
-   if !G.trace >= level then warn "ASSERT EQUAL";
+   if !G.ct >= level then warn "ASSERT EQUAL";
    if b && k1 <> P.null_mark && k2 <> P.null_mark then begin
-      n1.v <- Ref (k2, 0); if !G.trace >= level then pp_table st
+      n1.v <- Ref (k2, 0); if !G.ct >= level then pp_table st
    end; b end
 
 let is_not_zero st n  =
index 77a7e2c25682610faec295684a2e33c2cb606e5d..ffef0796ee9292150124e438027f16fe467a00ac 100644 (file)
@@ -20,7 +20,8 @@ type kernel = V4 | V3 | V0
 type manager = Quiet
              | Coq
              | Matita
-             | ELPI
+             | ELPI1
+             | ELPI2
 
 (* interface functions ******************************************************)
 
@@ -30,6 +31,8 @@ let stage = ref 3            (* stage *)
 
 let trace = ref 0            (* trace level *)
 
+let ct = ref 0               (* current trace level *)
+
 let summary = ref false      (* log summary information *)
 
 let xdir = ref ""            (* directory for XML output *)
@@ -62,6 +65,15 @@ let preamble = ref ""        (* preamble file for manager *)
 
 let alpha = ref ""           (* prefix of numeric identifiers *)
 
+let first = ref 0            (* begin trace here *)
+
+let last = ref max_int       (* end trace here *) 
+
+let extended = ref false     (* extended applications *) 
+
+let set_current_trace n =
+   ct := if !first <= n && n <= !last then !trace else 0
+
 let kernel_id () = 
    let id = match !kernel with
       | V4 -> "Environment"
@@ -69,7 +81,8 @@ let kernel_id () =
       | V0 -> "Environment_V0"
    in
    let si = if !si then "_si" else "" in
-   id ^ si
+   let ext = if !extended then "_x" else "" in
+   id ^ si ^ ext
 
 let get_baseuri () =
    String.concat "/" ["ld:"; kernel_id (); !cover; "" ]
@@ -79,8 +92,8 @@ let get_mk_uri () =
    fun s -> KF.concat bu (s ^ ".ld")
 
 let clear () =
-   stage := 3; trace := 0; summary := false; 
-   xdir := ""; kernel := V3; si := false; cover := ""; 
+   stage := 3; trace := 0; summary := false; first := 0; last := max_int;
+   xdir := ""; kernel := V3; si := false; extended := false; cover := ""; 
    expand := false; indexes := false; icm := 0; unquote := false;
    debug_parser := false; debug_lexer := false;
    manager_dir := ""; manager := Quiet
index d84012c2f1d706876fbcf8c8e1a6e63be3f0eb6d..94bf217daec407fd56619e2b11d0dc834fde7626 100644 (file)
@@ -43,11 +43,13 @@ let add
    ?(beta=0) ?(theta=0) ?(epsilon=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) 
    ?(upsilon=0) ?(lrt=0) ?(grt=0) ?(e=0) ?(x=0) ()
 =
- if beta > 0 then L.warn level (KP.sprintf "BETA %u" beta);
- if ldelta > 0 then L.warn level (KP.sprintf "EXP %u" ldelta);
- if gdelta > 0 then L.warn level (KP.sprintf "EXP %u" gdelta);
- if lrt > 0 then L.warn level (KP.sprintf "EXP %u" lrt);
- if grt > 0 then L.warn level (KP.sprintf "EXP %u" grt); 
+   if !G.ct >= level then begin
+      if beta > 0 then L.warn level (KP.sprintf "BETA %u" beta);
+      if ldelta > 0 then L.warn level (KP.sprintf "EXP %u" ldelta);
+      if gdelta > 0 then L.warn level (KP.sprintf "EXP %u" gdelta);
+      if lrt > 0 then L.warn level (KP.sprintf "EXP %u" lrt);
+      if grt > 0 then L.warn level (KP.sprintf "EXP %u" grt); 
+   end;
 reductions := {
    beta = !reductions.beta + beta;
    zeta = !reductions.zeta + zeta;
index ae1a8122238451477aeab5040f9838c380aa52bf..ea3ec54bfc4b101799e1b59ca9316ddfe010f598 100644 (file)
@@ -20,22 +20,22 @@ type uri = E.uri
 type id = E.id
 type attrs = E.node_attrs
 
-type bind = Abst of bool * N.layer * term (* x-reduced?, layer, type *)
-          | Abbr of term                  (* body *)
-          | Void                          (* *)
-
-and term = TSort of attrs * int           (* attrs, hierarchy index *)
-         | TLRef of attrs * int           (* attrs, position indexe *)
-         | TGRef of attrs * uri           (* attrs, reference *)
-         | TCast of attrs * term * term   (* attrs, domain, element *)
-         | TAppl of attrs * term * term   (* attrs, argument, function *)
-        | TBind of attrs * bind * term   (* attrs, binder, scope *)
-        | TProj of attrs * lenv * term   (* attrs, closure, member *)
-
-and lenv = ESort                          (* top *)
-         | EBind of lenv * attrs * bind   (* environment, attrs, binder *)
-         | EAppl of lenv * attrs * term   (* environment, attrs, argument *)
-         | EProj of lenv * attrs * lenv   (* environment, attrs, closure *) 
+type bind = Abst of bool * N.layer * term       (* x-reduced?, layer, type *)
+          | Abbr of term                        (* body *)
+          | Void                                (* *)
+
+and term = TSort of attrs * int                 (* attrs, hierarchy index *)
+         | TLRef of attrs * int                 (* attrs, position indexe *)
+         | TGRef of attrs * uri                 (* attrs, reference *)
+         | TCast of attrs * term * term         (* attrs, domain, element *)
+         | TAppl of attrs * bool * term * term  (* attrs, extended?, argument, function *)
+        | TBind of attrs * bind * term         (* attrs, binder, scope *)
+        | TProj of attrs * lenv * term         (* attrs, closure, member *)
+
+and lenv = ESort                                (* top *)
+         | EBind of lenv * attrs * bind         (* environment, attrs, binder *)
+         | EAppl of lenv * attrs * bool * term  (* environment, attrs, extended?, argument *)
+         | EProj of lenv * attrs * lenv         (* environment, attrs, closure *)
 
 type entity = term E.entity
 
@@ -45,43 +45,43 @@ let empty_lenv = ESort
 
 let push_bind f a b lenv = f (EBind (lenv, a, b))
 
-let push_appl f a t lenv = f (EAppl (lenv, a, t))
+let push_appl f a x t lenv = f (EAppl (lenv, a, x, t))
 
 let push_proj f a e lenv = f (EProj (lenv, a, e))
 
 let add_bind f a b t = f (TBind (a, b, t))
 
-let add_appl f a v t = f (TAppl (a, v, t))
+let add_appl f a x v t = f (TAppl (a, x, v, t))
 
 let add_proj f a e t = f (TProj (a, e, t))
 
 let rec shift f c t = match c with
-   | ESort           -> f t
-   | EBind (e, a, b) -> add_bind (shift f e) a b t
-   | EAppl (e, a, v) -> add_appl (shift f e) a v t
-   | EProj (e, a, d) -> add_proj (shift f e) a d t
+   | ESort              -> f t
+   | EBind (e, a, b)    -> add_bind (shift f e) a b t
+   | EAppl (e, a, x, v) -> add_appl (shift f e) a x v t
+   | EProj (e, a, d)    -> add_proj (shift f e) a d t
 
 let rec append f c = function
-   | ESort           -> f c
-   | EBind (e, a, b) -> append (push_bind f a b) c e
-   | EAppl (e, a, t) -> append (push_appl f a t) c e
-   | EProj (e, a, d) -> append (push_proj f a d) c e
+   | ESort              -> f c
+   | EBind (e, a, b)    -> append (push_bind f a b) c e
+   | EAppl (e, a, x, t) -> append (push_appl f a x t) c e
+   | EProj (e, a, d)    -> append (push_proj f a d) c e
 
 let resolve_lref err f id lenv =
    let rec aux i = function
-     | ESort             -> err ()
-     | EAppl (tl, _, _)  -> aux i tl
-     | EBind (tl, a, _)  ->
+     | ESort                -> err ()
+     | EAppl (tl, _, _, _)  -> aux i tl
+     | EBind (tl, a, _)     ->
         let f id0 _ = if id0 = id then f a i else aux (succ i) tl in
         let err () = aux (succ i) tl in
         E.name err f a
-     | EProj (tl, _, d)  -> append (aux i) tl d
+     | EProj (tl, _, d)     -> append (aux i) tl d
    in
    aux 0 lenv
 
 let rec get_name err f i = function
    | ESort                      -> err i
-   | EAppl (tl, _, _)           -> get_name err f i tl
+   | EAppl (tl, _, _, _)        -> get_name err f i tl
    | EBind (_, a, _) when i = 0 -> 
       let err () = err i in
       E.name err f a
@@ -94,7 +94,7 @@ let rec get e i = match e with
    | ESort                      -> ESort, E.empty_node, Void
    | EBind (e, a, b) when i = 0 -> e, a, b
    | EBind (e, _, _)            -> get e (pred i)
-   | EAppl (e, _, _)            -> get e i
+   | EAppl (e, _, _, _)         -> get e i
    | EProj (e, _, d)            -> get (append C.start e d) i
 
 let rec sub_list_strict f e l = match e, l with
@@ -108,19 +108,19 @@ let rec fold_names f map x = function
    | _                                      -> assert false
 
 let rec mem err f e b = match e with
-   | ESort           -> err ()
-   | EBind (e, a, _) ->
+   | ESort              -> err ()
+   | EBind (e, a, _)    ->
       if a.E.n_name = b.E.n_name then f () else mem err f e b
-   | EAppl (e, _, _) -> mem err f e b
-   | EProj (e, _, d) -> 
+   | EAppl (e, _, _, _) -> mem err f e b
+   | EProj (e, _, d)    -> 
       let err () = mem err f e b in mem err f d b
 
 let replace f n0 e =
    let rec aux f = function
       | ESort                        -> f ESort
-      | EBind (e, a, Abst (x, n, w)) -> aux (push_bind f a (Abst (x, n0, w))) e
+      | EBind (e, a, Abst (r, n, w)) -> aux (push_bind f a (Abst (r, n0, w))) e
       | EBind (e, a, b)              -> aux (push_bind f a b) e
-      | EAppl (e, a, v)              -> aux (push_appl f a v) e
+      | EAppl (e, a, x, v)           -> aux (push_appl f a x v) e
       | EProj (e, a, d)              -> let f d = aux (push_proj f a d) e in aux f d
 
    in
index dc5d78ce1f8f8dcb9f47d0aac9390fd7c2f7bf2d..95c3e8801a41ead8dd99d758b8603ec4b803b05c 100644 (file)
@@ -48,33 +48,33 @@ let initial_counters = {
 }
 
 let rec count_term f c e = function
-   | D.TSort _          -> 
+   | D.TSort _            -> 
       f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
-   | D.TLRef (_, i)     -> 
+   | D.TLRef (_, i)       -> 
       begin match D.get e i with
         | _, _, D.Abbr _ ->
            f {c with tlrefs = succ c.tlrefs; xnodes = succ c.xnodes}
         | _              ->
            f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes}
       end      
-   | D.TGRef (_, u)     -> 
+   | D.TGRef (_, u)       -> 
       let c =    
         if C.list_mem ~eq:U.eq u c.uris
         then {c with nodes = succ c.nodes}
         else {c with xnodes = succ c.xnodes}
       in
       f {c with tgrefs = succ c.tgrefs}
-   | D.TCast (_, v, t)  -> 
+   | D.TCast (_, v, t)    -> 
       let c = {c with tcasts = succ c.tcasts} in
       let f c = count_term f c e t in
       count_term f c e v
-   | D.TAppl (_, v, t)  -> 
+   | D.TAppl (_, _, v, t) -> 
       let c = {c with tappls = succ c.tappls} in
       let f c = count_term f c e t in
       count_term f c e v
-   | D.TProj (_, d, t)  ->
+   | D.TProj (_, d, t)    ->
       D.shift (count_term f c e) d t
-   | D.TBind (a, b, t)  -> 
+   | D.TBind (a, b, t)    -> 
       let f c e = count_term f c e t in
       count_binder f c e a b
 
@@ -137,22 +137,22 @@ let pp_attrs out a =
 let pp_state out x = if x then out "^"
 
 let rec pp_term out st = function
-   | D.TSort (a, l)    -> pp_attrs out a; out (KP.sprintf "*%u" l)
-   | D.TLRef (a, i   ) -> pp_attrs out a; out (KP.sprintf "#%u" i)
-   | D.TGRef (a, u)    -> pp_attrs out a; out (KP.sprintf "$")
-   | D.TCast (a, u, t) -> pp_attrs out a; out "<"; pp_term out st u; out ">."; pp_term out st t
-   | D.TAppl (a, u, t) -> pp_attrs out a; out "("; pp_term out st u; out ")."; pp_term out st t
-   | D.TBind (a, u, t) -> pp_attrs out a; pp_bind out st u; out "."; pp_term out st t
-   | D.TProj (a, u, t) -> pp_attrs out a; out "{"; pp_lenv out st u; out "}."; pp_term out st t
+   | D.TSort (a, l)       -> pp_attrs out a; out (KP.sprintf "*%u" l)
+   | D.TLRef (a, i   )    -> pp_attrs out a; out (KP.sprintf "#%u" i)
+   | D.TGRef (a, u)       -> pp_attrs out a; out (KP.sprintf "$")
+   | D.TCast (a, u, t)    -> pp_attrs out a; out "<"; pp_term out st u; out ">."; pp_term out st t
+   | D.TAppl (a, _, u, t) -> pp_attrs out a; out "("; pp_term out st u; out ")."; pp_term out st t
+   | D.TBind (a, u, t)    -> pp_attrs out a; pp_bind out st u; out "."; pp_term out st t
+   | D.TProj (a, u, t)    -> pp_attrs out a; out "{"; pp_lenv out st u; out "}."; pp_term out st t
 
 and pp_bind out st = function
-   | D.Abst (x, n, u) ->
-      out "[:"; pp_term out st u; out "]"; pp_state out x; out (N.to_string st n); out " "  
+   | D.Abst (r, n, u) ->
+      out "[:"; pp_term out st u; out "]"; pp_state out r; out (N.to_string st n); out " "  
    | D.Abbr u         -> out "[="; pp_term out st u; out "] ";
    | D.Void           -> out "[] "
 
 and pp_lenv out st = function
-   | D.ESort           -> ()
-   | D.EBind (u, a, t) -> pp_lenv out st u; pp_attrs out a; pp_bind out st t
-   | D.EAppl (u, a, t) -> pp_lenv out st u; out "("; pp_term out st t; out ") "
-   | D.EProj (u, a, t) -> pp_lenv out st u; out "{"; pp_lenv out st t; out "} "
+   | D.ESort              -> ()
+   | D.EBind (u, a, t)    -> pp_lenv out st u; pp_attrs out a; pp_bind out st t
+   | D.EAppl (u, a, _, t) -> pp_lenv out st u; out "("; pp_term out st t; out ") "
+   | D.EProj (u, a, t)    -> pp_lenv out st u; out "{"; pp_lenv out st t; out "} "
index 974145812ceba879cfa95be60dacedb198ffc11b..b2d0c99e1630aa54641e6cbeb1561e41ebb573ca 100644 (file)
@@ -25,6 +25,7 @@ type status = {
    path  : T.id list;      (* current section path *)
    line  : int;            (* line number *)
    sort  : int;            (* first default sort index *)
+   ext   : bool;           (* extended applications *) 
    mk_uri: G.uri_generator (* uri generator *) 
 }
 
@@ -80,7 +81,7 @@ let rec xlate_term f st lenv = function
       let f _ uu = xlate_term (f uu) st lenv t in
       xlate_term f st lenv u
    | T.Appl (v, t)    ->
-      let f vv a tt = f a (D.TAppl (a, vv, tt)) in
+      let f vv a tt = f a (D.TAppl (a, st.ext, vv, tt)) in
       let f _ vv = xlate_term (f vv) st lenv t in
       xlate_term f st lenv v
    | T.Proj (bs, t)   ->
@@ -89,7 +90,7 @@ let rec xlate_term f st lenv = function
       C.list_fold_left f (xlate_bind st) (lenv, D.empty_lenv) bs
    | T.Inst (t, vs)   ->
       let map f v e =
-         let f _ vv = D.push_appl f E.empty_node vv e in
+         let f _ vv = D.push_appl f E.empty_node st.ext vv e in
          xlate_term f st lenv v
       in
       let f e a tt = f a (D.TProj (a, e, tt)) in
@@ -171,7 +172,7 @@ let xlate_entity err f gen st = function
 
 let initial_status () =
    KH.clear henv; {
-   path = []; line = 1; sort = 0; mk_uri = G.get_mk_uri ()
+   path = []; line = 1; sort = 0; ext = false; mk_uri = G.get_mk_uri ()
 }
 
 let refresh_status st = {st with
index 3ce7bbc7026252f29724ea52559cafa3288d3218..984933290764364f3ecd8d71f088efcbeead5f00 100644 (file)
@@ -236,7 +236,7 @@ let process_2 st entity =
      | Some (export_entity, _) -> manager st export_entity entity
 
 let process_1 st entity = 
-   if !G.trace >= 3 then pp_progress entity;
+   if !G.ct >= 3 then pp_progress entity;
    let st = if !G.summary then count_entity st entity else st in
    if !export && !G.stage = 1 then export_entity st entity;
    if !G.stage >= 2 then process_2 st (xlate_entity st entity) else st 
@@ -313,10 +313,11 @@ let main =
       if !G.trace >= 2 then begin preprocess := true; G.summary := true end 
    in
    let set_manager s = match KS.lowercase s with
-      | "v8"   -> G.manager := G.Coq
-      | "ma2"  -> G.manager := G.Matita
-      | "elpi" -> G.manager := G.ELPI
-      | s      -> L.warn level (KP.sprintf "Unknown manager: %s" s) 
+      | "v8"    -> G.manager := G.Coq
+      | "ma2"   -> G.manager := G.Matita
+      | "elpi1" -> G.manager := G.ELPI1
+      | "elpi2" -> G.manager := G.ELPI2
+      | s       -> L.warn level (KP.sprintf "Unknown manager: %s" s) 
    in
    let clear_options () =
       export := false; preprocess := false;
@@ -335,7 +336,8 @@ let main =
       begin match !G.manager with
          | G.Coq    -> st := {!st with mst = Some (BA.open_out base_name)}
          | G.Matita -> st := {!st with mst = Some (BG.open_out base_name)}
-         | G.ELPI   -> st := {!st with mst = Some (BP.open_out base_name)}
+         | G.ELPI1  -> st := {!st with mst = Some (BP.open_out_1 base_name)}
+         | G.ELPI2  -> st := {!st with mst = Some (BP.open_out_2 base_name)}
          | G.Quiet  -> ()
       end;
       P.clear_marks ();
@@ -357,12 +359,12 @@ let main =
       if !G.trace >= 1 then Y.utime_stamp "at exit"
    in
    let help = 
-      "Usage: helena [ -LPVXdgilopqtx1 | -Ts <number> | -MO <dir> | -c <file> | -ahkmr <string> ]* [ <file> ]*\n\n" ^
+      "Usage: helena [ -LPVXdgilnopqtx1 | -Ts <number> | -MO <dir> | -c <file> | -ahkmr <string> | -be <age> ]* [ <file> ]*\n\n" ^
       "Trace levels: 0 just errors (default), 1 time stamps, 2 processed files, 3 processed objects,\n" ^
       "              4 typing information, 5 conversion information, 6 reduction information,\n" ^
       "              7 level disambiguation\n\n" ^
       "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n\n" ^
-      "Supported manages: \"ma2\" (Grafite NG), \"v8\" (Gallina 8), \"elpi\" (lambda-Prolog)\n" 
+      "Supported manages: \"ma2\" (Grafite NG), \"v8\" (Gallina 8), \"elpi1\" \"elpi2\" (lambda-Prolog)\n" 
    in
    let help_L = " show lexer debug information" in 
    let help_M = "<dir>  set location of output directory (manager) to <dir> (default: current directory)" in
@@ -373,20 +375,23 @@ let main =
    let help_X = " clear options" in
    
    let help_a = "<string>  set prefix of numeric identifiers (default: empty)" in
+   let help_b = "<age>  begin trace at this global constant (default: first)" in
    let help_c = "<file>  set preamble to this file (default: empty)" in
    let help_d = " show summary information (requires trace >= 2)" in
+   let help_e = "<age>  end trace at this global constant (default: last)" in
    let help_g = " always expand global definitions" in
    let help_h = "<string>  set type hierarchy (default: \"Z1\")" in
    let help_i = " show local references by index" in
    let help_k = "<string>  set kernel version (default: \"V3\")" in
-   let help_l = " disambiguate binders level (Automath)" in
+   let help_l = " disambiguate binders layer (Automath)" in
    let help_m = "<string>  export kernel entities for this manager (see above, default: no manager)" in
+   let help_n = " use extended (i.e. native) applications (Automath)" in
    let help_o = " activate sort inclusion (default: false)" in
    let help_p = " preprocess source (Automath)" in
    let help_q = " disable quotation of identifiers" in
    let help_r = "<string>  set initial segment of URI hierarchy (default: empty)" in
    let help_s = "<number>  set translation stage (see above)" in
-   let help_t = " type check [version 1]" in
+   let help_t = " type check (version 1)" in
    let help_x = " export kernel entities (XML)" in
    
    let help_1 = " parse files with streaming policy" in
@@ -400,14 +405,17 @@ let main =
       ("-V", Arg.Unit print_version, help_V);
       ("-X", Arg.Unit clear_options, help_X);
       ("-a", Arg.String ((:=) G.alpha), help_a);
+      ("-b", Arg.Int ((:=) G.first), help_b);
       ("-c", Arg.String ((:=) G.preamble), help_c);
       ("-d", Arg.Unit set_summary, help_d);
+      ("-e", Arg.Int ((:=) G.last), help_e);
       ("-g", Arg.Set G.expand, help_g);
       ("-h", Arg.String set_hierarchy, help_h);
       ("-i", Arg.Set G.indexes, help_i);
       ("-k", Arg.String set_kernel, help_k);
       ("-l", Arg.Set G.cc, help_l);
       ("-m", Arg.String set_manager, help_m);      
+      ("-n", Arg.Set G.extended, help_n);
       ("-o", Arg.Set G.si, help_o);
       ("-p", Arg.Unit set_preprocess, help_p);
       ("-q", Arg.Set G.unquote, help_q);      
index f04930851035d2d323499eef96a046e0477a5f2d..b5e3b9b40b7a16058ba1a63a4559847bdf002591 100644 (file)
@@ -27,9 +27,9 @@ let lenv_iter map_bind map_appl map_proj st e lenv out tab =
 (* NOTE: the inner binders are alpha-converted first *)
          let a = R.alpha D.mem e a in
          map_bind st e a b out tab; D.EBind (e, a, b)
-      | D.EAppl (e, a, v) ->
+      | D.EAppl (e, a, x, v) ->
          let e = aux e in
-         map_appl st e a v out tab; D.EAppl (e, a, v)
+         map_appl st e a x v out tab; D.EAppl (e, a, x, v)
       | D.EProj (e, a, d) ->
          let e = aux e in
          map_proj st e a d out tab; D.EProj (e, a, d)
@@ -61,9 +61,9 @@ let rec exp_term st e t out tab = match t with
       let attrs = [] in
       XL.tag XL.cast attrs ~contents:(exp_term st e u) out tab;
       exp_term st e t out tab
-   | D.TAppl (a, v, t)    ->
+   | D.TAppl (a, x, v, t) ->
       let attrs = [] in
-      XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab;
+      XL.tag (XL.appl x) attrs ~contents:(exp_term st e v) out tab;
       exp_term st e t out tab
    | D.TProj (a, lenv, t) ->
       let attrs = [] in
@@ -75,9 +75,9 @@ let rec exp_term st e t out tab = match t with
       exp_bind st e a b out tab; 
       exp_term st (D.push_bind C.start a b e) t out tab 
 
-and exp_appl st e a v out tab =
+and exp_appl st e a v out tab =
    let attrs = [] in
-   XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab;
+   XL.tag (XL.appl x) attrs ~contents:(exp_term st e v) out tab;
 
 and exp_bind st e a b out tab = match b with
    | D.Abst (_, n, w) ->
index 584dc776a7b8d4a0d533c1b69a1ebce7e2f01414..3c77fe68bc3edb36620323035601e17ef76725a1 100644 (file)
@@ -75,7 +75,7 @@ let gref = "GRef"
 
 let cast = "Cast"
 
-let appl = "Appl"
+let appl x = if x then "Appx" else "Appr"
 
 let proj = "Proj"
 
index ed7901f57789de19c5b87a3f825d2cc531871020..4ac5dc913413a9ab0c9f20bfec7c8bb2c2bbffe0 100644 (file)
@@ -27,7 +27,7 @@ val gref: string
 
 val cast: string
 
-val appl: string
+val appl: bool -> string
 
 val proj: string