when sort inclusion is enabled, we can produce conversion constraints in xml

[helm.git] / helm / software / lambda-delta / src / complete_rg / crgTxt.ml

diff --git a/helm/software/lambda-delta/src/complete_rg/crgTxt.ml b/helm/software/lambda-delta/src/complete_rg/crgTxt.ml
index 34727aff9a28e00ea756f2eaab3aba2cbe803045..141b467bbeb2d6a8a6bcd574e61ffaa2b3ff4c51 100644 (file)
--- a/helm/software/lambda-delta/src/complete_rg/crgTxt.ml
+++ b/helm/software/lambda-delta/src/complete_rg/crgTxt.ml
@@ -12,8 +12,8 @@
 module U  = NUri
 module H  = Hierarchy
 module C  = Cps
-module O  = Options
-module Y  = Entity
+module G  = Options
+module E  = Entity
 module T  = Txt
 module TT = TxtTxt
 module D  = Crg
@@ -22,7 +22,7 @@ type status = {
    path  : T.id list;      (* current section path *)
    line  : int;            (* line number *)
    sort  : int;            (* first default sort index *)
-   mk_uri: O.uri_generator (* uri generator *) 
+   mk_uri: G.uri_generator (* uri generator *) 
 }
 
 let henv_size = 7000 (* hash tables initial size *)
@@ -31,9 +31,9 @@ let henv = Hashtbl.create henv_size (* optimized global environment *)
 
 (* Internal functions *******************************************************)
 
-let name_of_id ?(r=true) id = Y.Name (id, r)
+let name_of_id ?(r=true) id = E.Name (id, r)
 
-let mk_lref f i j k = f (D.TLRef ([Y.Apix k], i, j))
+let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j))
 
 let mk_gref f uri = f (D.TGRef ([], uri))
 
@@ -49,27 +49,27 @@ let resolve_gref err f st id =
 
 let rec xlate_term f st lenv = function
    | T.Inst _
-   | T.Impl _       -> assert false
-   | T.Sort h       -> 
+   | T.Impl _         -> assert false
+   | T.Sort h         -> 
       f (D.TSort ([], h))
-   | T.NSrt id      -> 
+   | T.NSrt id        -> 
       let f h = f (D.TSort ([], h)) in
       H.sort_of_string C.err f id
-   | T.LRef (i, j)  ->    
+   | T.LRef (i, j)    ->    
       D.get_index C.err (mk_lref f i j) i j lenv
-   | T.NRef id      ->
+   | T.NRef id        ->
       let err () = resolve_gref C.err (mk_gref f) st id in
       D.resolve_lref err (mk_lref f) id lenv
-   | T.Cast (u, t)  ->
+   | T.Cast (u, t)    ->
       let f uu tt = f (D.TCast ([], uu, tt)) in
       let f uu = xlate_term (f uu) st lenv t in
       xlate_term f st lenv u
-   | T.Appl (vs, t) ->
+   | T.Appl (vs, t)   ->
       let map f = xlate_term f st lenv in
       let f vvs tt = f (D.TAppl ([], vvs, tt)) in
       let f vvs = xlate_term (f vvs) st lenv t in
       C.list_map f map vs
-   | T.Bind (b, t)  ->
+   | T.Bind (n, b, t) ->
       let abst_map (lenv, a, wws) (id, r, w) = 
          let attr = name_of_id ~r id in
         let ww = xlate_term C.start st lenv w in
@@ -86,9 +86,9 @@ let rec xlate_term f st lenv = function
       in
       let lenv, aa, bb = match b with
          | T.Abst xws ->
-           let lenv = D.push_bind C.start lenv [] (D.Abst []) in
+           let lenv = D.push_bind C.start lenv [] (D.Abst (n, [])) in
            let lenv, aa, wws = List.fold_left abst_map (lenv, [], []) xws in
-           lenv, aa, D.Abst wws
+           lenv, aa, D.Abst (n, wws)
          | T.Abbr xvs ->
            let lenv = D.push_bind C.start lenv [] (D.Abbr []) in
            let lenv, aa, vvs = List.fold_left abbr_map (lenv, [], []) xvs in
@@ -104,11 +104,12 @@ let rec xlate_term f st lenv = function
 let xlate_term f st lenv t =
    TT.contract (xlate_term f st lenv) t
 
-let mk_contents tt = function
-   | T.Decl -> [], Y.Abst tt
-   | T.Ax   -> [], Y.Abst tt
-   | T.Def  -> [], Y.Abbr tt
-   | T.Th   -> [], Y.Abbr tt
+let mk_contents n tt = function
+   | T.Decl -> [], E.Abst (n, tt)
+   | T.Ax   -> [], E.Abst (n, tt)
+   | T.Cong -> [], E.Abst (n, tt)   
+   | T.Def  -> [], E.Abbr tt
+   | T.Th   -> [], E.Abbr tt
 
 let xlate_entity err f gen st = function
    | T.Require _                  ->
@@ -130,31 +131,31 @@ let xlate_entity err f gen st = function
          {st with sort = H.set_sorts ix [s]}
       in
       err (List.fold_left map st sorts)
-   | T.Graph id                   ->
+   | T.Graph id                      ->
       assert (H.set_graph id); err st
-   | T.Entity (kind, id, meta, t) ->
+   | T.Entity (kind, n, id, meta, t) ->
       let uri = uri_of_id st id st.path in
       Hashtbl.add henv id uri;
       let tt = xlate_term C.start st D.empty_lenv t in
 (*
       print_newline (); CrgOutput.pp_term print_string tt;
 *)
-      let a, b = mk_contents tt kind in 
-      let a = if meta <> "" then Y.Meta meta :: a else a in
-      let entity = Y.Mark st.line :: a, uri, b in
+      let a, b = mk_contents n tt kind in 
+      let a = if meta <> "" then E.Meta meta :: a else a in
+      let entity = E.Mark st.line :: a, uri, b in
       f {st with line = succ st.line} entity
-   | T.Generate _                 ->
+   | T.Generate _                   ->
       err st
 
 (* Interface functions ******************************************************)
 
 let initial_status () =
    Hashtbl.clear henv; {
-   path = []; line = 1; sort = 0; mk_uri = O.get_mk_uri ()
+   path = []; line = 1; sort = 0; mk_uri = G.get_mk_uri ()
 }
 
 let refresh_status st = {st with
-   mk_uri = O.get_mk_uri ()
+   mk_uri = G.get_mk_uri ()
 }
 
 let crg_of_txt = xlate_entity