From: Stefano Zacchiroli Date: Wed, 4 Feb 2004 09:43:15 +0000 (+0000) Subject: ported to CicAst X-Git-Tag: V_0_2_3~78 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0d853dfc19b683f5d37741df405a2db721f7221a;p=helm.git ported to CicAst --- diff --git a/helm/ocaml/cic_disambiguation/.depend b/helm/ocaml/cic_disambiguation/.depend index 1f34686b2..b34b115f4 100644 --- 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 a3d6297e3..ec24a4f4d 100644 --- 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 e4c700d0a..53de39449 100644 --- 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 545099da1..648286ec2 100644 --- 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 525a7e33f..059ecf388 100644 --- 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 85c5be3ea..a19361b32 100644 --- 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> (* ∨ *); 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> (* ∧ *); 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> (* ¬ *); t = term -> - return_term loc (Appl_symbol ("not", 0, [t])) ] + return_term loc (CicAst.Appl [CicAst.Symbol ("not", 0); t]) + ] ]; END