- dual_rg: renamed to complete_rg [as suggested in the ToCL documentation]

[helm.git] / helm / software / lambda-delta / toplevel / top.ml

diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml
index 6f7d60e9ca93d35051916c2442bb46bf3424f851..12e639c5636da1e1fa389544a3ff91f1d44bf17b 100644 (file)
--- a/helm/software/lambda-delta/toplevel/top.ml
+++ b/helm/software/lambda-delta/toplevel/top.ml
@@ -20,12 +20,12 @@ module Y    = Entity
 module X    = Library
 module AP   = AutProcess
 module AO   = AutOutput
-module DA   = DrgAut
+module DA   = CrgAut
 module MA   = MetaAut
 module MO   = MetaOutput
 module ML   = MetaLibrary
-module DO   = DrgOutput
-module DBrg = DrgBrg
+module DO   = CrgOutput
+module DBrg = CrgBrg
 module MBrg = MetaBrg
 module BrgO = BrgOutput
 module BrgR = BrgReduction
@@ -76,7 +76,7 @@ type kernel = Brg | Bag
 
 type kernel_entity = BrgEntity  of Brg.entity
                    | BagEntity  of Bag.entity
-                  | DrgEntity  of Drg.entity
+                  | CrgEntity  of Crg.entity
                   | MetaEntity of Meta.entity
 
 let kernel = ref Brg
@@ -86,8 +86,8 @@ let print_counters st = match !kernel with
    | Bag -> BagO.print_counters C.start st.bagc
 
 let xlate f st entity = match !kernel, entity with
-   | Brg, DrgEntity e  -> 
-      let f e = f st (BrgEntity e) in Y.xlate f DBrg.brg_of_drg e
+   | Brg, CrgEntity e  -> 
+      let f e = f st (BrgEntity e) in Y.xlate f DBrg.brg_of_crg e
    | Brg, MetaEntity e -> 
       let f e = f st (BrgEntity e) in Y.xlate f MBrg.brg_of_meta e
    | Bag, MetaEntity e -> 
@@ -102,7 +102,7 @@ let pp_progress e =
       Y.mark err f a
    in
    match e with
-      | DrgEntity e -> Y.common f e
+      | CrgEntity e -> Y.common f e
       | BrgEntity e -> Y.common f e
       | BagEntity e -> Y.common f e      
       | MetaEntity e -> Y.common f e
@@ -114,7 +114,7 @@ let count_entity st = function
    | _            -> st
 
 let export_entity si g moch = function
-   | DrgEntity e  -> X.export_entity DO.export_term si g e
+   | CrgEntity e  -> X.export_entity DO.export_term si g e
    | BrgEntity e  -> X.export_entity BrgO.export_term si g e
    | MetaEntity e ->
       begin match moch with
@@ -125,12 +125,12 @@ let export_entity si g moch = function
 
 let type_check f st si g k =
    let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in
-   let ok _ (a, u, _) = f st a u in
+   let ok _ _ = f 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
-      | DrgEntity (a, u, _)
-      | MetaEntity (a, u, _) -> f st a u
+      | BrgEntity entity -> BrgU.type_check brg_err ok ~si g entity
+      | BagEntity entity -> BagU.type_check ok ~si g entity
+      | CrgEntity _
+      | MetaEntity _     -> f st
 
 (****************************************************************************)
 
@@ -146,7 +146,7 @@ let export = ref false
 let graph = ref (H.graph_of_string C.err C.start "Z2")
 let old = ref false
 
-let process_3 f st a u =
+let process_3 f st =
    f st
 
 let process_2 f st entity =
@@ -166,9 +166,9 @@ let process_0 f st entity =
       let frr mst = f {st with mst = mst} in
       let h mst e = process_1 f {st with mst = mst} (MetaEntity e) in
       let err dst = f {st with dst = dst} in
-      let g dst e = process_1 f {st with dst = dst} (DrgEntity e) in
+      let g dst e = process_1 f {st with dst = dst} (CrgEntity e) in
       if !old then MA.meta_of_aut frr h st.mst entity else 
-      DA.drg_of_aut err g st.dst entity
+      DA.crg_of_aut err g st.dst entity
    in
    let st = {st with ac = count AO.count_entity st.ac entity} in 
    if !preprocess then process_entity f st entity else f st entity
@@ -219,7 +219,7 @@ try
       if !L.level > 0 then T.utime_stamp "parsed";
       O.clear_reductions ();
       let mk_uri =
-         if !stage < 2 then Drg.mk_uri else
+         if !stage < 2 then Crg.mk_uri else
         match !kernel with
            | Brg -> Brg.mk_uri
            | Bag -> Bag.mk_uri
@@ -255,7 +255,7 @@ try
    let help_j = " show URI of processed kernel objects" in
    let help_k = "<string>  set kernel version (default: brg)" in
    let help_m = " output intermediate representation (HAL)" in
-   let help_o = " use old abstract language instead of drg" in   
+   let help_o = " use old abstract language instead of crg" in   
    let help_p = " preprocess Automath source" in
    let help_r = " disable initial segment of URI hierarchy" in
    let help_s = "<number>  set translation stage (see above)" in