ported to CicAst

diff --git a/helm/ocaml/cic_disambiguation/.depend b/helm/ocaml/cic_disambiguation/.depend
index 1f34686b2783378f2832e56eaadf63c0fe8f245c..b34b115f41b512cbacc5286dfe5d1df22368dc46 100644 (file)
--- a/helm/ocaml/cic_disambiguation/.depend
+++ b/helm/ocaml/cic_disambiguation/.depend
@@ -1,32 +1,25 @@
 disambiguateChoices.cmi: disambiguateTypes.cmi 
-cicTextualParser2Pp.cmi: cicTextualParser2Ast.cmi 
-cicTextualParser2.cmi: cicTextualParser2Ast.cmi disambiguateTypes.cmi 
-disambiguate.cmi: cicTextualParser2Ast.cmi disambiguateTypes.cmi 
+cicTextualParser2.cmi: disambiguateTypes.cmi 
+disambiguate.cmi: disambiguateTypes.cmi 
 disambiguateTypes.cmo: disambiguateTypes.cmi 
 disambiguateTypes.cmx: disambiguateTypes.cmi 
 disambiguateChoices.cmo: disambiguateTypes.cmi disambiguateChoices.cmi 
 disambiguateChoices.cmx: disambiguateTypes.cmx disambiguateChoices.cmi 
-cicTextualParser2Pp.cmo: cicTextualParser2Ast.cmi cicTextualParser2Pp.cmi 
-cicTextualParser2Pp.cmx: cicTextualParser2Ast.cmi cicTextualParser2Pp.cmi 
 macro.cmo: macro.cmi 
 macro.cmx: macro.cmi 
 cicTextualLexer2.cmo: macro.cmi cicTextualLexer2.cmi 
 cicTextualLexer2.cmx: macro.cmx cicTextualLexer2.cmi 
-cicTextualParser2.cmo: cicTextualLexer2.cmi cicTextualParser2Ast.cmi \
-    disambiguateChoices.cmi disambiguateTypes.cmi cicTextualParser2.cmi 
-cicTextualParser2.cmx: cicTextualLexer2.cmx cicTextualParser2Ast.cmi \
-    disambiguateChoices.cmx disambiguateTypes.cmx cicTextualParser2.cmi 
-disambiguate.cmo: cicTextualParser2.cmi cicTextualParser2Ast.cmi \
-    disambiguateChoices.cmi disambiguateTypes.cmi disambiguate.cmi 
-disambiguate.cmx: cicTextualParser2.cmx cicTextualParser2Ast.cmi \
-    disambiguateChoices.cmx disambiguateTypes.cmx disambiguate.cmi 
-logic_notation.cmo: cicTextualParser2.cmi cicTextualParser2Ast.cmi \
-    disambiguateChoices.cmi 
-logic_notation.cmx: cicTextualParser2.cmx cicTextualParser2Ast.cmi \
-    disambiguateChoices.cmx 
-arit_notation.cmo: cicTextualParser2.cmi cicTextualParser2Ast.cmi \
-    disambiguateChoices.cmi 
-arit_notation.cmx: cicTextualParser2.cmx cicTextualParser2Ast.cmi \
-    disambiguateChoices.cmx 
+cicTextualParser2.cmo: cicTextualLexer2.cmi disambiguateChoices.cmi \
+    disambiguateTypes.cmi cicTextualParser2.cmi 
+cicTextualParser2.cmx: cicTextualLexer2.cmx disambiguateChoices.cmx \
+    disambiguateTypes.cmx cicTextualParser2.cmi 
+disambiguate.cmo: cicTextualParser2.cmi disambiguateChoices.cmi \
+    disambiguateTypes.cmi disambiguate.cmi 
+disambiguate.cmx: cicTextualParser2.cmx disambiguateChoices.cmx \
+    disambiguateTypes.cmx disambiguate.cmi 
+logic_notation.cmo: cicTextualParser2.cmi disambiguateChoices.cmi 
+logic_notation.cmx: cicTextualParser2.cmx disambiguateChoices.cmx 
+arit_notation.cmo: cicTextualParser2.cmi disambiguateChoices.cmi 
+arit_notation.cmx: cicTextualParser2.cmx disambiguateChoices.cmx 
 tex_notation.cmo: cicTextualParser2.cmi 
 tex_notation.cmx: cicTextualParser2.cmx 

diff --git a/helm/ocaml/cic_disambiguation/Makefile b/helm/ocaml/cic_disambiguation/Makefile
index a3d6297e303b8861d8459f0f11f19368a247726f..ec24a4f4d6610ae3a9ba43d471b4b06b2bd9c07c 100644 (file)
--- a/helm/ocaml/cic_disambiguation/Makefile
+++ b/helm/ocaml/cic_disambiguation/Makefile
@@ -1,11 +1,12 @@
 
 PACKAGE = cic_textual_parser2
-REQUIRES = ulex pxp helm-tactics helm-logger helm-cic_unification camlp4.gramlib
+REQUIRES = \
+       helm-tactics helm-logger helm-cic_unification helm-cic_transformations \
+       ulex pxp camlp4.gramlib
 NOTATIONS = logic arit tex
 INTERFACE_FILES = \
        disambiguateTypes.mli \
        disambiguateChoices.mli \
-       cicTextualParser2Pp.mli \
        macro.mli \
        cicTextualLexer2.mli \
        cicTextualParser2.mli \

diff --git a/helm/ocaml/cic_disambiguation/arit_notation.ml b/helm/ocaml/cic_disambiguation/arit_notation.ml
index e4c700d0a6fede6338256ae9a6b12d51ccbeeb93..53de39449b24de7af95169348594d5ae18a66c8c 100644 (file)
--- a/helm/ocaml/cic_disambiguation/arit_notation.ml
+++ b/helm/ocaml/cic_disambiguation/arit_notation.ml
@@ -23,35 +23,29 @@
  * http://helm.cs.unibo.it/
  *)
 
-open CicTextualParser2Ast
 open CicTextualParser2
 
-(*
-let i = ref max_int
-let get_i () = decr i; !i
-*)
-
 EXTEND
   term: LEVEL "add"
     [
       [ t1 = term; SYMBOL "+"; t2 = term ->
-          return_term loc (Appl_symbol ("plus", 0, [t1; t2]))
+          return_term loc (CicAst.Appl [CicAst.Symbol ("plus", 0); t1; t2])
       | t1 = term; SYMBOL "-"; t2 = term ->
-          return_term loc (Appl_symbol ("minus", 0, [t1; t2]))
+          return_term loc (CicAst.Appl [CicAst.Symbol ("minus", 0); t1; t2])
       ]
     ];
   term: LEVEL "mult"
     [
       [ t1 = term; SYMBOL "*"; t2 = term ->
-          return_term loc (Appl_symbol ("times", 0, [t1; t2]))
+          return_term loc (CicAst.Appl [CicAst.Symbol ("times", 0); t1; t2])
       | t1 = term; SYMBOL "/"; t2 = term ->
-          return_term loc (Appl_symbol ("div", 0, [t1; t2]))
+          return_term loc (CicAst.Appl [CicAst.Symbol ("div", 0); t1; t2])
       ]
     ];
   term: LEVEL "inv"
     [
       [ SYMBOL "-"; t = term ->
-        return_term loc (Appl_symbol ("uminus", 0, [t]))
+        return_term loc (CicAst.Appl [CicAst.Symbol ("uminus", 0); t])
       ]
     ];
 END

diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml
index 545099da1ee362c73cf348ed4ee40df41d8f0f6b..648286ec2c7a5428d5e7f1a0a70173ed5329e9d1 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml
@@ -10,7 +10,7 @@ module OrderedDomain =
     let compare = Pervasives.compare
   end
 
-module Domain = Set.Make (OrderedDomain)
+(* module Domain = Set.Make (OrderedDomain) *)
 module Environment = Map.Make (OrderedDomain)
 
 type codomain_item =
@@ -38,10 +38,14 @@ let string_of_domain_item = function
   | Symbol (s, i) -> Printf.sprintf "SYMBOL(%s,%d)" s i
   | Num i -> Printf.sprintf "NUM(instance %d)" i
 
+let string_of_domain dom =
+  String.concat "; " (List.map string_of_domain_item dom)
+(*
 let string_of_domain dom =
   let buf = Buffer.create 1024 in
   Domain.iter
     (fun item -> Buffer.add_string buf (string_of_domain_item item ^ "; "))
     dom;
   Buffer.contents buf
+*)
 

diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli
index 525a7e33f8a1f1bb044d4e00190e7b0f6d0b25f5..059ecf38838320aeae9ba1aa9145cb4edd0c74a5 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli
@@ -28,7 +28,7 @@ type domain_item =
  | Symbol of string * int     (* literal, instance num *)
  | Num of int                 (* instance num *)
 
-module Domain:      Set.S with type elt = domain_item
+(* module Domain:      Set.S with type elt = domain_item *)
 module Environment: Map.S with type key = domain_item
 
 type codomain_item =
@@ -52,5 +52,5 @@ module type Callbacks =
   end
 
 val string_of_domain_item: domain_item -> string
-val string_of_domain: Domain.t -> string
+val string_of_domain: domain_item list -> string
 

diff --git a/helm/ocaml/cic_disambiguation/logic_notation.ml b/helm/ocaml/cic_disambiguation/logic_notation.ml
index 85c5be3ea324fefc82d004eb7d7b03c62388855a..a19361b32e7264717b96e5f5fc185353d50fff99 100644 (file)
--- a/helm/ocaml/cic_disambiguation/logic_notation.ml
+++ b/helm/ocaml/cic_disambiguation/logic_notation.ml
@@ -23,26 +23,26 @@
  * http://helm.cs.unibo.it/
  *)
 
-open CicTextualParser2Ast
 open CicTextualParser2
 
 EXTEND
   term: LEVEL "add"
     [
       [ t1 = term; SYMBOL <:unicode<lor>> (* ∨ *); t2 = term ->
-          return_term loc (Appl_symbol ("or", 0, [t1; t2]))
+          return_term loc (CicAst.Appl [CicAst.Symbol ("or", 0); t1; t2])
       ]
     ];
   term: LEVEL "mult"
     [
       [ t1 = term; SYMBOL <:unicode<land>> (* ∧ *); t2 = term ->
-        return_term loc (Appl_symbol ("and", 0, [t1; t2]))
+        return_term loc (CicAst.Appl [CicAst.Symbol ("and", 0); t1; t2])
       ]
     ];
   term: LEVEL "inv"
     [
       [ SYMBOL <:unicode<lnot>> (* ¬ *); t = term ->
-        return_term loc (Appl_symbol ("not", 0, [t])) ]
+        return_term loc (CicAst.Appl [CicAst.Symbol ("not", 0); t])
+      ]
     ];
 END