X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=e64087cf6f3ad61ab81f478be9be57b7658f92dd;hb=67b9632f9a2e5331cb3c7b03908acf6392911007;hp=0e2b590796dc9dcc9ae6f9d0c4dc0760ca8fc06e;hpb=49bb3bff65173f6f443b66d2d3120d8d9843144e;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 0e2b59079..e64087cf6 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -25,7 +25,7 @@
 
 open Printf
 
-open Disambiguate_types
+open DisambiguateTypes
 open UriManager
 
 exception Invalid_choice
@@ -96,12 +96,12 @@ let find_in_environment name context =
 
 let interpretate ~context ~env ast =
   let rec aux loc context = function
-    | Ast.LocatedTerm (loc, term) -> aux loc context term
-    | Ast.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
-    | Ast.Appl_symbol (symb, i, args) ->
+    | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term
+    | CicTextualParser2Ast.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
+    | CicTextualParser2Ast.Appl_symbol (symb, i, args) ->
         let cic_args = List.map (aux loc context) args in
         resolve env (Symbol (symb, i)) ~args:cic_args ()
-    | Ast.Binder (binder_kind, var, typ, body) ->
+    | CicTextualParser2Ast.Binder (binder_kind, var, typ, body) ->
         let cic_type = aux_option loc context typ in
         let cic_body = aux loc (var :: context) body in
         (match binder_kind with
@@ -110,7 +110,7 @@ let interpretate ~context ~env ast =
         | `Exists ->
             resolve env (Symbol ("exists", 0))
               ~args:[ cic_type; Cic.Lambda (var, cic_type, cic_body) ] ())
-    | Ast.Case (term, indty_ident, outtype, branches) ->
+    | CicTextualParser2Ast.Case (term, indty_ident, outtype, branches) ->
         let cic_term = aux loc context term in
         let cic_outtype = aux_option loc context outtype in
         let do_branch (pat, term) =
@@ -132,12 +132,12 @@ let interpretate ~context ~env ast =
         in
         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
           (List.map do_branch branches))
-    | Ast.LetIn (var, def, body) ->
+    | CicTextualParser2Ast.LetIn (var, def, body) ->
         let cic_def = aux loc context def in
         let name = Cic.Name var in
         let cic_body = aux loc (name :: context) body in
         Cic.LetIn (name, cic_def, cic_body)
-    | Ast.LetRec (kind, defs, body) ->
+    | CicTextualParser2Ast.LetRec (kind, defs, body) ->
         let context' =
           List.fold_left (fun acc (var, _, _, _) -> Cic.Name var :: acc)
             context defs
@@ -169,48 +169,48 @@ let interpretate ~context ~env ast =
                 Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
         in
         List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
-    | Ast.Ident (name, subst) ->
+    | CicTextualParser2Ast.Ident (name, subst) ->
         (* TODO hanlde explicit substitutions *)
         (try
           let index = find_in_environment name context in
           if subst <> [] then
-            Parser.fail loc "Explicit substitutions not allowed here";
+            CicTextualParser2.fail loc "Explicit substitutions not allowed here";
           Cic.Rel index
         with Not_found -> resolve env (Id name) ())
-    | Ast.Num (num, i) -> resolve env (Num i) ~num ()
-    | Ast.Meta (index, subst) ->
+    | CicTextualParser2Ast.Num (num, i) -> resolve env (Num i) ~num ()
+    | CicTextualParser2Ast.Meta (index, subst) ->
         let cic_subst =
           List.map
             (function None -> None | Some term -> Some (aux loc context term))
             subst
         in
         Cic.Meta (index, cic_subst)
-    | Ast.Sort `Prop -> Cic.Sort Cic.Prop
-    | Ast.Sort `Set -> Cic.Sort Cic.Set
-    | Ast.Sort `Type -> Cic.Sort Cic.Type
-    | Ast.Sort `CProp -> Cic.Sort Cic.CProp
+    | CicTextualParser2Ast.Sort `Prop -> Cic.Sort Cic.Prop
+    | CicTextualParser2Ast.Sort `Set -> Cic.Sort Cic.Set
+    | CicTextualParser2Ast.Sort `Type -> Cic.Sort Cic.Type
+    | CicTextualParser2Ast.Sort `CProp -> Cic.Sort Cic.CProp
   and aux_option loc context = function
     | None -> Cic.Implicit
     | Some term -> aux loc context term
   in
   match ast with
-  | Ast.LocatedTerm (loc, term) -> aux loc context term
+  | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term
   | _ -> assert false
 
 let domain_of_term ~context ast =
   let rec aux loc context = function
-    | Ast.LocatedTerm (_, term) -> aux loc context term
-    | Ast.Appl terms ->
+    | CicTextualParser2Ast.LocatedTerm (_, term) -> aux loc context term
+    | CicTextualParser2Ast.Appl terms ->
         List.fold_left (fun dom term -> Domain.union dom (aux loc context term))
           Domain.empty terms
-    | Ast.Appl_symbol (symb, i, args) ->
+    | CicTextualParser2Ast.Appl_symbol (symb, i, args) ->
         List.fold_left (fun dom term -> Domain.union dom (aux loc context term))
           (Domain.singleton (Symbol (symb, i))) args
-    | Ast.Binder (_, var, typ, body) ->
+    | CicTextualParser2Ast.Binder (_, var, typ, body) ->
         let type_dom = aux_option loc context typ in
         let body_dom = aux loc (var :: context) body in
         Domain.union type_dom body_dom
-    | Ast.Case (term, indty_ident, outtype, branches) ->
+    | CicTextualParser2Ast.Case (term, indty_ident, outtype, branches) ->
         let term_dom = aux loc context term in
         let outtype_dom = aux_option loc context outtype in
         let do_branch (pat, term) =
@@ -228,11 +228,11 @@ let domain_of_term ~context ast =
         in
         Domain.add (Id indty_ident)
           (Domain.union outtype_dom (Domain.union term_dom branches_dom))
-    | Ast.LetIn (var, body, where) ->
+    | CicTextualParser2Ast.LetIn (var, body, where) ->
         let body_dom = aux loc context body in
         let where_dom = aux loc (Cic.Name var :: context) where in
         Domain.union body_dom where_dom
-    | Ast.LetRec (kind, defs, where) ->
+    | CicTextualParser2Ast.LetRec (kind, defs, where) ->
         let context' =
           List.fold_left (fun acc (var, _, _, _) -> Cic.Name var :: acc)
             context defs
@@ -245,26 +245,26 @@ let domain_of_term ~context ast =
             Domain.empty defs
         in
         Domain.union where_dom defs_dom
-    | Ast.Ident (name, subst) ->
+    | CicTextualParser2Ast.Ident (name, subst) ->
         (* TODO hanlde explicit substitutions *)
         (try
           let index = find_in_environment name context in
           if subst <> [] then
-            Parser.fail loc "Explicit substitutions not allowed here";
+            CicTextualParser2.fail loc "Explicit substitutions not allowed here";
           Domain.empty
         with Not_found -> Domain.singleton (Id name))
-    | Ast.Num (num, i) -> Domain.singleton (Num i)
-    | Ast.Meta (index, local_context) ->
+    | CicTextualParser2Ast.Num (num, i) -> Domain.singleton (Num i)
+    | CicTextualParser2Ast.Meta (index, local_context) ->
         List.fold_left
           (fun dom term -> Domain.union dom (aux_option loc context term))
             Domain.empty local_context
-    | Ast.Sort _ -> Domain.empty
+    | CicTextualParser2Ast.Sort _ -> Domain.empty
   and aux_option loc context = function
     | None -> Domain.empty
     | Some t -> aux loc context t
   in
   match ast with
-  | Ast.LocatedTerm (loc, term) -> aux loc context term
+  | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term
   | _ -> assert false
 
 module Make (C: Callbacks) =