From 8004125685a99b6c0f2f95fd7f3fa09a4f5c9094 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 23 Jan 2004 17:05:20 +0000 Subject: [PATCH] renamed modules so that they are more consistent with other cic modules --- helm/gTopLevel/chosenTermEditor.mli | 2 +- helm/gTopLevel/disambiguatingParser.ml | 6 +- helm/gTopLevel/disambiguatingParser.mli | 2 +- helm/gTopLevel/script.sh | 1 - helm/gTopLevel/termEditor.ml | 2 +- helm/gTopLevel/termEditor.mli | 2 +- helm/ocaml/cic_disambiguation/.depend | 42 +++++++------ helm/ocaml/cic_disambiguation/Makefile | 26 +++++--- .../ocaml/cic_disambiguation/arit_notation.ml | 4 +- .../{lexer.ml => cicTextualLexer2.ml} | 0 .../{lexer.mli => cicTextualLexer2.mli} | 0 .../{parser.ml => cicTextualParser2.ml} | 30 +++++----- .../{parser.mli => cicTextualParser2.mli} | 8 +-- .../{ast.mli => cicTextualParser2Ast.mli} | 0 .../{pp.ml => cicTextualParser2Pp.ml} | 2 +- .../{pp.mli => cicTextualParser2Pp.mli} | 2 +- helm/ocaml/cic_disambiguation/disambiguate.ml | 60 +++++++++---------- .../ocaml/cic_disambiguation/disambiguate.mli | 4 +- ...mbiguate_types.ml => disambiguateTypes.ml} | 0 ...iguate_types.mli => disambiguateTypes.mli} | 0 .../cic_disambiguation/logic_notation.ml | 4 +- helm/ocaml/cic_disambiguation/tests/eq.txt | 1 + 22 files changed, 107 insertions(+), 91 deletions(-) rename helm/ocaml/cic_disambiguation/{lexer.ml => cicTextualLexer2.ml} (100%) rename helm/ocaml/cic_disambiguation/{lexer.mli => cicTextualLexer2.mli} (100%) rename helm/ocaml/cic_disambiguation/{parser.ml => cicTextualParser2.ml} (82%) rename helm/ocaml/cic_disambiguation/{parser.mli => cicTextualParser2.mli} (80%) rename helm/ocaml/cic_disambiguation/{ast.mli => cicTextualParser2Ast.mli} (100%) rename helm/ocaml/cic_disambiguation/{pp.ml => cicTextualParser2Pp.ml} (99%) rename helm/ocaml/cic_disambiguation/{pp.mli => cicTextualParser2Pp.mli} (95%) rename helm/ocaml/cic_disambiguation/{disambiguate_types.ml => disambiguateTypes.ml} (100%) rename helm/ocaml/cic_disambiguation/{disambiguate_types.mli => disambiguateTypes.mli} (100%) create mode 100644 helm/ocaml/cic_disambiguation/tests/eq.txt diff --git a/helm/gTopLevel/chosenTermEditor.mli b/helm/gTopLevel/chosenTermEditor.mli index ebd9a95e6..1cc4f5606 100644 --- a/helm/gTopLevel/chosenTermEditor.mli +++ b/helm/gTopLevel/chosenTermEditor.mli @@ -11,7 +11,7 @@ class type term_editor = end module Make : - functor (C : Disambiguate_types.Callbacks) -> + functor (C : DisambiguateTypes.Callbacks) -> sig val term_editor : MQIConn.handle -> diff --git a/helm/gTopLevel/disambiguatingParser.ml b/helm/gTopLevel/disambiguatingParser.ml index 8ce12c045..580e09bb2 100644 --- a/helm/gTopLevel/disambiguatingParser.ml +++ b/helm/gTopLevel/disambiguatingParser.ml @@ -25,13 +25,13 @@ exception NoWellTypedInterpretation -module EnvironmentP3 = Disambiguate_types.EnvironmentP3 +module EnvironmentP3 = DisambiguateTypes.EnvironmentP3 -module Make (C : Disambiguate_types.Callbacks) = +module Make (C : DisambiguateTypes.Callbacks) = struct let disambiguate_term mqi_handle context metasenv term_as_string environment = let module Disambiguate' = Disambiguate.Make (C) in - let term = Parser.parse_term (Stream.of_string term_as_string) in + let term = CicTextualParser2.parse_term (Stream.of_string term_as_string) in Disambiguate'.disambiguate_term mqi_handle context metasenv term environment end diff --git a/helm/gTopLevel/disambiguatingParser.mli b/helm/gTopLevel/disambiguatingParser.mli index 397799548..5ddf68377 100644 --- a/helm/gTopLevel/disambiguatingParser.mli +++ b/helm/gTopLevel/disambiguatingParser.mli @@ -33,7 +33,7 @@ module EnvironmentP3 : val of_string : string -> t end -module Make (C : Disambiguate_types.Callbacks) : +module Make (C : DisambiguateTypes.Callbacks) : sig val disambiguate_term : MQIConn.handle -> diff --git a/helm/gTopLevel/script.sh b/helm/gTopLevel/script.sh index 5592e25d8..848103c32 100755 --- a/helm/gTopLevel/script.sh +++ b/helm/gTopLevel/script.sh @@ -11,7 +11,6 @@ export GTOPLEVEL_INNERTYPESFILE=/public/helm_library/innertypes export GTOPLEVEL_CONSTANTTYPEFILE=/public/helm_library/constanttype export GTOPLEVEL_ENVIRONMENTFILE=/public/helm_library/environment export MATHQL_DB_MAP=/home/zack/helm/mathql_db_map.txt -export POSTGRESQL_CONNECTION_STRING="dbname=mowgli" export HELM_TMP_DIR=/tmp unset http_proxy diff --git a/helm/gTopLevel/termEditor.ml b/helm/gTopLevel/termEditor.ml index 668bf1502..db637554f 100644 --- a/helm/gTopLevel/termEditor.ml +++ b/helm/gTopLevel/termEditor.ml @@ -51,7 +51,7 @@ class type term_editor = method environment : DisambiguatingParser.EnvironmentP3.t ref end -module Make(C:Disambiguate_types.Callbacks) = +module Make(C:DisambiguateTypes.Callbacks) = struct module Disambiguate' = DisambiguatingParser.Make(C);; diff --git a/helm/gTopLevel/termEditor.mli b/helm/gTopLevel/termEditor.mli index 67b076505..b3fb94937 100644 --- a/helm/gTopLevel/termEditor.mli +++ b/helm/gTopLevel/termEditor.mli @@ -36,7 +36,7 @@ class type term_editor = method environment : DisambiguatingParser.EnvironmentP3.t ref end -module Make (C : Disambiguate_types.Callbacks) : +module Make (C : DisambiguateTypes.Callbacks) : sig val term_editor : MQIConn.handle -> diff --git a/helm/ocaml/cic_disambiguation/.depend b/helm/ocaml/cic_disambiguation/.depend index 00cb03a9a..0342a9b11 100644 --- a/helm/ocaml/cic_disambiguation/.depend +++ b/helm/ocaml/cic_disambiguation/.depend @@ -1,19 +1,27 @@ -pp.cmi: ast.cmi -disambiguate.cmi: ast.cmi disambiguate_types.cmi -parser.cmi: ast.cmi -disambiguate_types.cmo: disambiguate_types.cmi -disambiguate_types.cmx: disambiguate_types.cmi -pp.cmo: ast.cmi pp.cmi -pp.cmx: ast.cmi pp.cmi +cicTextualParser2Pp.cmi: cicTextualParser2Ast.cmi +disambiguate.cmi: cicTextualParser2Ast.cmi disambiguateTypes.cmi +cicTextualParser2.cmi: cicTextualParser2Ast.cmi +disambiguateTypes.cmo: disambiguateTypes.cmi +disambiguateTypes.cmx: disambiguateTypes.cmi +cicTextualParser2Pp.cmo: cicTextualParser2Ast.cmi cicTextualParser2Pp.cmi +cicTextualParser2Pp.cmx: cicTextualParser2Ast.cmi cicTextualParser2Pp.cmi macro.cmo: macro.cmi macro.cmx: macro.cmi -lexer.cmo: macro.cmi lexer.cmi -lexer.cmx: macro.cmx lexer.cmi -parser.cmo: ast.cmi lexer.cmi parser.cmi -parser.cmx: ast.cmi lexer.cmx parser.cmi -disambiguate.cmo: ast.cmi disambiguate_types.cmi parser.cmi disambiguate.cmi -disambiguate.cmx: ast.cmi disambiguate_types.cmx parser.cmx disambiguate.cmi -logic_notation.cmo: ast.cmi disambiguate.cmi parser.cmi -logic_notation.cmx: ast.cmi disambiguate.cmx parser.cmx -arit_notation.cmo: ast.cmi disambiguate.cmi parser.cmi -arit_notation.cmx: ast.cmi disambiguate.cmx parser.cmx +cicTextualLexer2.cmo: macro.cmi cicTextualLexer2.cmi +cicTextualLexer2.cmx: macro.cmx cicTextualLexer2.cmi +cicTextualParser2.cmo: cicTextualLexer2.cmi cicTextualParser2Ast.cmi \ + cicTextualParser2.cmi +cicTextualParser2.cmx: cicTextualLexer2.cmx cicTextualParser2Ast.cmi \ + cicTextualParser2.cmi +disambiguate.cmo: cicTextualParser2.cmi cicTextualParser2Ast.cmi \ + disambiguateTypes.cmi disambiguate.cmi +disambiguate.cmx: cicTextualParser2.cmx cicTextualParser2Ast.cmi \ + disambiguateTypes.cmx disambiguate.cmi +logic_notation.cmo: cicTextualParser2.cmi cicTextualParser2Ast.cmi \ + disambiguate.cmi +logic_notation.cmx: cicTextualParser2.cmx cicTextualParser2Ast.cmi \ + disambiguate.cmx +arit_notation.cmo: cicTextualParser2.cmi cicTextualParser2Ast.cmi \ + disambiguate.cmi +arit_notation.cmx: cicTextualParser2.cmx cicTextualParser2Ast.cmi \ + disambiguate.cmx diff --git a/helm/ocaml/cic_disambiguation/Makefile b/helm/ocaml/cic_disambiguation/Makefile index 3a0ae7b80..abfcd4da9 100644 --- a/helm/ocaml/cic_disambiguation/Makefile +++ b/helm/ocaml/cic_disambiguation/Makefile @@ -5,11 +5,19 @@ REQUIRES = \ camlp4.gramlib NOTATIONS = logic arit INTERFACE_FILES = \ - ast.mli pp.mli macro.mli lexer.mli disambiguate.mli parser.mli \ - disambiguate_types.mli + cicTextualParser2Ast.mli \ + cicTextualParser2Pp.mli \ + macro.mli \ + cicTextualLexer2.mli \ + disambiguate.mli \ + cicTextualParser2.mli \ + disambiguateTypes.mli IMPLEMENTATION_FILES = \ - disambiguate_types.ml \ - pp.ml macro.ml lexer.ml parser.ml \ + disambiguateTypes.ml \ + cicTextualParser2Pp.ml \ + macro.ml \ + cicTextualLexer2.ml \ + cicTextualParser2.ml \ disambiguate.ml \ $(patsubst %,%_notation.ml,$(NOTATIONS)) \ @@ -21,12 +29,12 @@ PA_P4_OPTS = q_MLast.cmo pa_extend.cmo all: -lexer.cmo: lexer.ml +cicTextualLexer2.cmo: cicTextualLexer2.ml $(OCAMLC) -pp "camlp4o $(LEXER_P4_OPTS)" -c $< -parser.cmo: parser.ml macro.cmo pa_unicode_macro.cmo +cicTextualParser2.cmo: cicTextualParser2.ml macro.cmo pa_unicode_macro.cmo $(OCAMLC) -pp "camlp4o $(PARSER_P4_OPTS)" -c $< -%_notation.cmo: %_notation.ml parser.cmo +%_notation.cmo: %_notation.ml cicTextualParser2.cmo $(OCAMLC) -pp "camlp4o $(PARSER_P4_OPTS)" -c $< pa_unicode_macro.cmo: pa_unicode_macro.ml macro.cmo @@ -57,8 +65,8 @@ include ../Makefile.common depend: macro.cmi macro.cmo pa_unicode_macro.cmi pa_unicode_macro.cmo $(OCAMLDEP) -pp "camlp4o $(PARSER_P4_OPTS) $(LEXER_P4_OPTS)" $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) > .depend -disambiguate_types.cmi: disambiguate_types.mli +disambiguateTypes.cmi: disambiguateTypes.mli $(OCAMLC) -c -rectypes $< -disambiguate_types.cmo: disambiguate_types.ml disambiguate_types.cmi +disambiguateTypes.cmo: disambiguateTypes.ml disambiguateTypes.cmi $(OCAMLC) -c -rectypes $< diff --git a/helm/ocaml/cic_disambiguation/arit_notation.ml b/helm/ocaml/cic_disambiguation/arit_notation.ml index b4aaf3398..f0f8d52bc 100644 --- a/helm/ocaml/cic_disambiguation/arit_notation.ml +++ b/helm/ocaml/cic_disambiguation/arit_notation.ml @@ -23,8 +23,8 @@ * http://helm.cs.unibo.it/ *) -open Ast -open Parser +open CicTextualParser2Ast +open CicTextualParser2 (* let i = ref max_int diff --git a/helm/ocaml/cic_disambiguation/lexer.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml similarity index 100% rename from helm/ocaml/cic_disambiguation/lexer.ml rename to helm/ocaml/cic_disambiguation/cicTextualLexer2.ml diff --git a/helm/ocaml/cic_disambiguation/lexer.mli b/helm/ocaml/cic_disambiguation/cicTextualLexer2.mli similarity index 100% rename from helm/ocaml/cic_disambiguation/lexer.mli rename to helm/ocaml/cic_disambiguation/cicTextualLexer2.mli diff --git a/helm/ocaml/cic_disambiguation/parser.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml similarity index 82% rename from helm/ocaml/cic_disambiguation/parser.ml rename to helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 8b53c3aac..d60e56378 100644 --- a/helm/ocaml/cic_disambiguation/parser.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -35,13 +35,13 @@ open Printf exception Parse_error of string -let grammar = Grammar.gcreate Lexer.lex +let grammar = Grammar.gcreate CicTextualLexer2.lex let term = Grammar.Entry.create grammar "term" (* let tactic = Grammar.Entry.create grammar "tactic" *) (* let tactical = Grammar.Entry.create grammar "tactical" *) -let return_term loc term = Ast.LocatedTerm (loc, term) +let return_term loc term = CicTextualParser2Ast.LocatedTerm (loc, term) (* let return_term loc term = term *) let fail (x, y) msg = @@ -72,8 +72,8 @@ EXTEND substs ] -> (match subst with - | Some l -> Ast.Ident (s, l) - | None -> Ast.Ident (s, [])) + | Some l -> CicTextualParser2Ast.Ident (s, l) + | None -> CicTextualParser2Ast.Ident (s, [])) ] ]; name: [ (* as substituted_name with no explicit substitution *) @@ -86,11 +86,11 @@ EXTEND term: [ "arrow" RIGHTA [ t1 = term; SYMBOL <:unicode>; t2 = term -> - return_term loc (Ast.Binder (`Pi, Cic.Anonymous, Some t1, t2)) + return_term loc (CicTextualParser2Ast.Binder (`Pi, Cic.Anonymous, Some t1, t2)) ] | "eq" LEFTA [ t1 = term; SYMBOL "="; t2 = term -> - return_term loc (Ast.Appl_symbol ("eq", 0, [t1; t2])) + return_term loc (CicTextualParser2Ast.Appl_symbol ("eq", 0, [t1; t2])) ] | "add" LEFTA [ (* nothing here by default *) ] | "mult" LEFTA [ (* nothing here by default *) ] @@ -103,19 +103,19 @@ EXTEND SYMBOL "."; body = term -> let binder = List.fold_right - (fun var body -> Ast.Binder (b, Cic.Name var, typ, body)) + (fun var body -> CicTextualParser2Ast.Binder (b, Cic.Name var, typ, body)) vars body in return_term loc binder | sort_kind = [ "Prop" -> `Prop | "Set" -> `Set | "Type" -> `Type | "CProp" -> `CProp ] -> - Ast.Sort sort_kind + CicTextualParser2Ast.Sort sort_kind | n = substituted_name -> return_term loc n | LPAREN "("; head = term; args = LIST1 term; RPAREN ")" -> - return_term loc (Ast.Appl (head :: args)) - | i = NUM -> return_term loc (Ast.Num (i, 0)) -(* | i = NUM -> return_term loc (Ast.Num (i, Random.int max_int)) *) + return_term loc (CicTextualParser2Ast.Appl (head :: args)) + | i = NUM -> return_term loc (CicTextualParser2Ast.Num (i, 0)) +(* | i = NUM -> return_term loc (CicTextualParser2Ast.Num (i, Random.int max_int)) *) | m = META; substs = [ LPAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; RPAREN "]" -> @@ -127,12 +127,12 @@ EXTEND with Failure "int_of_string" -> fail loc ("Invalid meta variable number: " ^ m) in - return_term loc (Ast.Meta (index, substs)) + return_term loc (CicTextualParser2Ast.Meta (index, substs)) (* actually "in" and "and" are _not_ keywords. Parsing works anyway * since applications are required to be bound by parens *) | "let"; name = IDENT; SYMBOL <:unicode> (* ≝ *); t1 = term; IDENT "in"; t2 = term -> - return_term loc (Ast.LetIn (name, t1, t2)) + return_term loc (CicTextualParser2Ast.LetIn (name, t1, t2)) | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; defs = LIST1 [ name = IDENT; @@ -144,7 +144,7 @@ EXTEND (name, t1, typ, (match index with None -> 1 | Some i -> i)) ] SEP (IDENT "and"); IDENT "in"; body = term -> - return_term loc (Ast.LetRec (ind_kind, defs, body)) + return_term loc (CicTextualParser2Ast.LetRec (ind_kind, defs, body)) | outtyp = OPT [ LPAREN "["; typ = term; RPAREN "]" -> typ ]; "match"; t = term; SYMBOL ":"; indty = IDENT; @@ -154,7 +154,7 @@ EXTEND p = pattern; SYMBOL <:unicode> (* ⇒ *); t = term -> (p, t) ] SEP SYMBOL "|"; RPAREN "]" -> - return_term loc (Ast.Case (t, indty, outtyp, patterns)) + return_term loc (CicTextualParser2Ast.Case (t, indty, outtyp, patterns)) | LPAREN "("; t = term; RPAREN ")" -> return_term loc t ] ]; diff --git a/helm/ocaml/cic_disambiguation/parser.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli similarity index 80% rename from helm/ocaml/cic_disambiguation/parser.mli rename to helm/ocaml/cic_disambiguation/cicTextualParser2.mli index 7f855a459..0d600cc20 100644 --- a/helm/ocaml/cic_disambiguation/parser.mli +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli @@ -27,14 +27,14 @@ exception Parse_error of string (** {2 Parsing functions} *) -val parse_term: char Stream.t -> Ast.term +val parse_term: char Stream.t -> CicTextualParser2Ast.term (** {2 Grammar extensions} *) -val term: Ast.term Grammar.Entry.e +val term: CicTextualParser2Ast.term Grammar.Entry.e -val return_term: Ast.location -> Ast.term -> Ast.term +val return_term: CicTextualParser2Ast.location -> CicTextualParser2Ast.term -> CicTextualParser2Ast.term (** raise a parse error *) -val fail: Ast.location -> string -> 'a +val fail: CicTextualParser2Ast.location -> string -> 'a diff --git a/helm/ocaml/cic_disambiguation/ast.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2Ast.mli similarity index 100% rename from helm/ocaml/cic_disambiguation/ast.mli rename to helm/ocaml/cic_disambiguation/cicTextualParser2Ast.mli diff --git a/helm/ocaml/cic_disambiguation/pp.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.ml similarity index 99% rename from helm/ocaml/cic_disambiguation/pp.ml rename to helm/ocaml/cic_disambiguation/cicTextualParser2Pp.ml index 081a7ab19..83da77244 100644 --- a/helm/ocaml/cic_disambiguation/pp.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.ml @@ -23,7 +23,7 @@ * http://helm.cs.unibo.it/ *) -open Ast +open CicTextualParser2Ast open Printf let pp_binder = function diff --git a/helm/ocaml/cic_disambiguation/pp.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.mli similarity index 95% rename from helm/ocaml/cic_disambiguation/pp.mli rename to helm/ocaml/cic_disambiguation/cicTextualParser2Pp.mli index 44fa63323..555e3272c 100644 --- a/helm/ocaml/cic_disambiguation/pp.mli +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.mli @@ -23,4 +23,4 @@ * http://helm.cs.unibo.it/ *) -val pp_term: Ast.term -> string +val pp_term: CicTextualParser2Ast.term -> string 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) = diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli index 94690373a..cbc7a54ac 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate.mli @@ -23,7 +23,7 @@ * http://helm.cs.unibo.it/ *) -open Disambiguate_types +open DisambiguateTypes (** {2 Choice registration interface} *) @@ -47,7 +47,7 @@ module Make (C : Callbacks) : MQIConn.handle -> Cic.context -> Cic.metasenv -> - Ast.term -> + CicTextualParser2Ast.term -> aliases:environment -> (* previous interpretation status *) environment * (* new interpretation status *) Cic.metasenv * (* new metasenv *) diff --git a/helm/ocaml/cic_disambiguation/disambiguate_types.ml b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml similarity index 100% rename from helm/ocaml/cic_disambiguation/disambiguate_types.ml rename to helm/ocaml/cic_disambiguation/disambiguateTypes.ml diff --git a/helm/ocaml/cic_disambiguation/disambiguate_types.mli b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli similarity index 100% rename from helm/ocaml/cic_disambiguation/disambiguate_types.mli rename to helm/ocaml/cic_disambiguation/disambiguateTypes.mli diff --git a/helm/ocaml/cic_disambiguation/logic_notation.ml b/helm/ocaml/cic_disambiguation/logic_notation.ml index 2f404be83..011462f81 100644 --- a/helm/ocaml/cic_disambiguation/logic_notation.ml +++ b/helm/ocaml/cic_disambiguation/logic_notation.ml @@ -23,8 +23,8 @@ * http://helm.cs.unibo.it/ *) -open Ast -open Parser +open CicTextualParser2Ast +open CicTextualParser2 EXTEND term: LEVEL "add" diff --git a/helm/ocaml/cic_disambiguation/tests/eq.txt b/helm/ocaml/cic_disambiguation/tests/eq.txt new file mode 100644 index 000000000..6a826fc71 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/tests/eq.txt @@ -0,0 +1 @@ +\forall n. \forall m. n + m = n -- 2.39.2