From aba014724c9ad08f80944ec3021c9fa3826dca4a Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 14 Jan 2004 17:54:33 +0000 Subject: [PATCH] still a working copy, now towards a cleaner implementation ... --- helm/ocaml/cic_disambiguation/.depend | 16 +- helm/ocaml/cic_disambiguation/Makefile | 26 +- .../ocaml/cic_disambiguation/arit_notation.ml | 37 +- helm/ocaml/cic_disambiguation/ast.mli | 16 +- helm/ocaml/cic_disambiguation/disambiguate.ml | 414 ++++++++++++++++++ .../ocaml/cic_disambiguation/disambiguate.mli | 60 +++ .../cic_disambiguation/disambiguate_struct.ml | 48 ++ .../cic_disambiguation/disambiguate_types.mli | 36 ++ helm/ocaml/cic_disambiguation/lexer.ml | 26 +- helm/ocaml/cic_disambiguation/lexer.mli | 24 + .../cic_disambiguation/logic_notation.ml | 33 +- helm/ocaml/cic_disambiguation/macro.ml | 24 + helm/ocaml/cic_disambiguation/macro.mli | 24 + helm/ocaml/cic_disambiguation/make_table.ml | 24 + .../cic_disambiguation/pa_unicode_macro.ml | 24 + helm/ocaml/cic_disambiguation/parser.ml | 298 ++++++++++++- helm/ocaml/cic_disambiguation/parser.mli | 46 ++ helm/ocaml/cic_disambiguation/pp.ml | 49 ++- helm/ocaml/cic_disambiguation/pp.mli | 25 ++ helm/ocaml/cic_disambiguation/test_lexer.ml | 25 ++ helm/ocaml/cic_disambiguation/test_parser.ml | 25 ++ 21 files changed, 1247 insertions(+), 53 deletions(-) create mode 100644 helm/ocaml/cic_disambiguation/disambiguate.ml create mode 100644 helm/ocaml/cic_disambiguation/disambiguate.mli create mode 100644 helm/ocaml/cic_disambiguation/disambiguate_struct.ml create mode 100644 helm/ocaml/cic_disambiguation/disambiguate_types.mli create mode 100644 helm/ocaml/cic_disambiguation/parser.mli diff --git a/helm/ocaml/cic_disambiguation/.depend b/helm/ocaml/cic_disambiguation/.depend index 16d57692a..90354741c 100644 --- a/helm/ocaml/cic_disambiguation/.depend +++ b/helm/ocaml/cic_disambiguation/.depend @@ -1,9 +1,21 @@ pp.cmi: ast.cmi +disambiguate.cmi: ast.cmi disambiguate_struct.cmo disambiguate_types.cmi +parser.cmi: ast.cmi pp.cmo: ast.cmi pp.cmi pp.cmx: ast.cmi pp.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.cmx: ast.cmi lexer.cmx +disambiguate_struct.cmo: disambiguate_types.cmi +disambiguate_struct.cmx: disambiguate_types.cmi +parser.cmo: ast.cmi lexer.cmi parser.cmi +parser.cmx: ast.cmi lexer.cmx parser.cmi +disambiguate.cmo: ast.cmi disambiguate_struct.cmo disambiguate_types.cmi \ + parser.cmi disambiguate.cmi +disambiguate.cmx: ast.cmi disambiguate_struct.cmx disambiguate_types.cmi \ + parser.cmx disambiguate.cmi +logic_notation.cmo: ast.cmi parser.cmi +logic_notation.cmx: ast.cmi parser.cmx +arit_notation.cmo: ast.cmi parser.cmi +arit_notation.cmx: ast.cmi parser.cmx diff --git a/helm/ocaml/cic_disambiguation/Makefile b/helm/ocaml/cic_disambiguation/Makefile index 4827da666..11da72469 100644 --- a/helm/ocaml/cic_disambiguation/Makefile +++ b/helm/ocaml/cic_disambiguation/Makefile @@ -1,11 +1,16 @@ PACKAGE = cic_textual_parser2 -REQUIRES = ulex camlp4 pxp -INTERFACE_FILES = ast.mli pp.mli macro.mli lexer.mli +REQUIRES = \ + ulex pxp helm-tactics helm-cic helm-logger helm-cic_unification \ + camlp4.gramlib NOTATIONS = logic arit +INTERFACE_FILES = \ + ast.mli pp.mli macro.mli lexer.mli disambiguate.mli parser.mli \ + disambiguate_types.mli IMPLEMENTATION_FILES = \ - pp.ml macro.ml lexer.ml parser.ml \ - $(patsubst %,%_notation.ml,$(NOTATIONS)) + pp.ml macro.ml lexer.ml disambiguate_struct.ml parser.ml \ + disambiguate.ml \ + $(patsubst %,%_notation.ml,$(NOTATIONS)) \ ULEXDIR := $(shell ocamlfind query ulex) @@ -13,7 +18,7 @@ LEXER_P4_OPTS = -I $(ULEXDIR) pa_ulex.cma PARSER_P4_OPTS = pa_extend.cmo ./macro.cmo ./pa_unicode_macro.cmo PA_P4_OPTS = q_MLast.cmo pa_extend.cmo -include ../Makefile.common +all: lexer.cmo: lexer.ml $(OCAMLC) -pp "camlp4o $(LEXER_P4_OPTS)" -c $< @@ -26,7 +31,7 @@ parser.cmo: parser.ml macro.cmo pa_unicode_macro.cmo pa_unicode_macro.cmo: pa_unicode_macro.ml macro.cmo $(OCAMLC) -pp "camlp4o $(PA_P4_OPTS)" -c $< -LOCAL_LINKOPTS = -linkpkg gramlib.cma $(PACKAGE).cma +LOCAL_LINKOPTS = -linkpkg $(PACKAGE).cma test: test_lexer test_parser test_lexer: test_lexer.ml $(PACKAGE).cma $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< @@ -45,3 +50,12 @@ distclean: extra_clean extra_clean: rm -f test_lexer test_parser make_table +include ../Makefile.common + +.PHONY: depend +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 + $(OCAMLC) -c -rectypes $< + diff --git a/helm/ocaml/cic_disambiguation/arit_notation.ml b/helm/ocaml/cic_disambiguation/arit_notation.ml index 522021f5f..998688cbe 100644 --- a/helm/ocaml/cic_disambiguation/arit_notation.ml +++ b/helm/ocaml/cic_disambiguation/arit_notation.ml @@ -1,3 +1,28 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + open Ast open Parser @@ -5,23 +30,21 @@ EXTEND term: LEVEL "add" [ [ t1 = term; SYMBOL "+"; t2 = term -> - return_term loc (Appl [Ident ("plus", []); t1; t2]) + return_term loc (Appl_symbol ("plus", [t1; t2])) | t1 = term; SYMBOL "-"; t2 = term -> - return_term loc (Appl [Ident ("minus", []); t1; t2]) + return_term loc (Appl_symbol ("minus", [t1; t2])) ] ]; term: LEVEL "mult" [ [ t1 = term; SYMBOL "*"; t2 = term -> - return_term loc (Appl [Ident ("times", []); t1; t2]) + return_term loc (Appl_symbol ("times", [t1; t2])) | t1 = term; SYMBOL "/"; t2 = term -> - return_term loc (Appl [Ident ("div", []); t1; t2]) + return_term loc (Appl_symbol ("div", [t1; t2])) ] ]; term: LEVEL "inv" [ - [ SYMBOL "-"; t = term -> - return_term loc (Appl [Ident ("uminus", []); t]) - ] + [ SYMBOL "-"; t = term -> return_term loc (Appl_symbol ("uminus", [t])) ] ]; END diff --git a/helm/ocaml/cic_disambiguation/ast.mli b/helm/ocaml/cic_disambiguation/ast.mli index d579ccdd3..19f4bd6bd 100644 --- a/helm/ocaml/cic_disambiguation/ast.mli +++ b/helm/ocaml/cic_disambiguation/ast.mli @@ -60,6 +60,8 @@ type 'tactic tactical = | Try of 'tactic tactical (* try a tactical and mask failures *) type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ] +type induction_kind = [ `Inductive | `CoInductive ] +type sort_kind = [ `Prop | `Set | `Type | `CProp ] type case_pattern = string list @@ -67,16 +69,18 @@ type term = | LocatedTerm of location * term | Appl of term list - | Binder of binder_kind * string * term option * term + | Appl_symbol of string * term list + | Binder of binder_kind * Cic.name * term option * term (* kind, name, type, body *) - | Case of term * term option * (case_pattern * term) list - (* what to match, case type, list *) + | Case of term * string * term option * (case_pattern * term) list + (* what to match, inductive type, out type, list *) | LetIn of string * term * term (* name, body, where *) - | LetRec of (string * term * term option * int) list * term + | LetRec of induction_kind * (string * term * term option * int) list * term (* (name, body, type, decreasing argument) list, where *) | Ident of string * subst list - | Meta of string * meta_subst list - | Int of int + | Meta of int * meta_subst list + | Num of string + | Sort of sort_kind and meta_subst = term option and subst = string * term diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml new file mode 100644 index 000000000..827bbe2d4 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -0,0 +1,414 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +open Disambiguate_struct +open Disambiguate_types + +let debug = true +let debug_print = if debug then prerr_endline else ignore + +type interpretation_domain = Domain.t +type domain_and_interpretation = interpretation_domain * interpretation + +let string_of_interpretation_domain_item = function + | Id s -> "ID " ^ s + | Symbol (s, i) -> "SYMBOL " ^ s ^ " " ^ string_of_int i + | Num (s, i) -> "NUM " ^ s ^ " " ^ string_of_int i + +let descr_of_domain_item = function + | Id s -> s + | Symbol (s, _) -> s + | Num (s, _) -> s + +let rec build_natural = + function + | 0 -> HelmLibraryObjects.Datatypes.zero + | n -> Cic.Appl [ HelmLibraryObjects.Datatypes.succ; (build_natural (n - 1)) ] + +exception Invalid_choice + +let symbol_choices: (string, interpretation_codomain_item list) Hashtbl.t = Hashtbl.create 1023 +let _ = + Hashtbl.add symbol_choices "eq" + [ ("Leibnitz's equality", + (fun interp args -> + let t1, t2 = + match args with + | [t1; t2] -> t1, t2 + | _ -> raise Invalid_choice + in + Cic.Appl [ + Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); + Cic.Implicit; t1; t2 + ])) ] +(* +let add_symbol_choice = Hashtbl.add symbol_choices +let add_symbol_choices symbol = List.iter (add_symbol_choice symbol) +*) +let num_choices = + ref [ + "natural number", + (fun num -> + let num = int_of_string num in + assert (num >= 0); + build_natural num) + ] + +let add_num_choice choice = + num_choices := choice :: !num_choices + +type test_result = + | Ok of Cic.term * Cic.metasenv + | Ko + | Uncertain + +let refine metasenv context term = + let metasenv, term = CicMkImplicit.expand_implicits metasenv context term in + try + let term', _, _, metasenv' = CicRefine.type_of_aux' metasenv context term in + Ok (term', metasenv') + with + | CicRefine.MutCaseFixAndCofixRefineNotImplemented -> + (* TODO remove this case as soon as refine is fully implemented *) + (try + let term' = CicTypeChecker.type_of_aux' metasenv context term in + Ok (term',metasenv) + with _ -> Ko) + | CicRefine.Uncertain _ -> + debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ; + Uncertain + | _ -> + debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ; + Ko + +open Printf + +open UriManager + +let indtyuri_of_uri uri = + let index_sharp = String.index uri '#' in + let index_num = index_sharp + 3 in + (UriManager.uri_of_string (String.sub uri 0 index_sharp), + int_of_string(String.sub uri index_num (String.length uri - index_num)) - 1) + +let indconuri_of_uri uri = + let index_sharp = String.index uri '#' in + let index_div = String.rindex uri '/' in + let index_con = index_div + 1 in + (UriManager.uri_of_string (String.sub uri 0 index_sharp), + int_of_string + (String.sub uri (index_sharp + 3) (index_div - index_sharp - 3)) - 1, + int_of_string + (String.sub uri index_con (String.length uri - index_con))) + + (* TODO move it to Cic *) +let term_of_uri uri = + try + (* Constant *) + (* TODO explicit substitutions? *) + let len = String.length uri in + if String.sub uri (len - 4) 4 = ".con" then + Cic.Const (uri_of_string uri, []) + else if String.sub uri (len - 4) 4 = ".var" then + Cic.Var (uri_of_string uri, []) + else + (try + (* Inductive Type *) + let uri',typeno = indtyuri_of_uri uri in + Cic.MutInd (uri', typeno, []) + with + | UriManager.IllFormedUri _ | Failure _ | Invalid_argument _ -> + (* Constructor of an Inductive Type *) + let uri',typeno,consno = indconuri_of_uri uri in + Cic.MutConstruct (uri', typeno, consno, [])) + with + | Invalid_argument _ -> raise (UriManager.IllFormedUri uri) + +module Make (C: Callbacks) = + struct + exception NoWellTypedInterpretation + + let choices_of_id mqi_handle id = + let query = MQueryGenerator.locate id in + let result = MQueryInterpreter.execute mqi_handle query in + let uris = + List.map + (function uri,_ -> + MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri + ) result in + C.output_html (`Msg (`T "Locate query:")); + MQueryUtil.text_of_query + (fun s -> C.output_html ~append_NL:false (`Msg (`T s))) + "" query; + C.output_html (`Msg (`T "Result:")); + MQueryUtil.text_of_result + (fun s -> C.output_html (`Msg (`T s))) "" result; + let uris' = + match uris with + | [] -> + [UriManager.string_of_uri (C.input_or_locate_uri + ~title:("URI matching \"" ^ id ^ "\" unknown."))] + | [uri] -> [uri] + | _ -> + C.interactive_user_uri_choice ~selection_mode:`MULTIPLE + ~ok:"Try every selection." ~enable_button_for_non_vars:true + ~title:"Ambiguous input." ~id + ~msg: ("Ambiguous input \"" ^ id ^ + "\". Please, choose one or more interpretations:") + uris + in + List.map (fun uri -> (uri, term_of_uri uri)) uris' + + let disambiguate_input + mqi_handle context metasenv parser_dom parser_mk_term + (current_dom, current_interpretation) + = + debug_print "NEW DISAMBIGUATE INPUT"; + let todo_dom = Domain.diff parser_dom current_dom in + (* (1) for each item in todo_dom we get the associated list of choices *) + let id_choices = Hashtbl.create 1023 in + let _ = + Domain.iter + (function + | Id id -> + (* pairs *) + let choices = choices_of_id mqi_handle id in + debug_print (sprintf + "CHOICES_OF_ID di %s ha restituito %d scelte" + id (List.length choices)); + Hashtbl.add id_choices id choices + | _ -> assert false) + (Domain.filter (function Id _ -> true | _ -> false) todo_dom) + in + (* (2) lookup function for any item (Id/Symbol/Num) *) + let lookup_choices item = + try + (match item with + | Id id -> + let choices = Hashtbl.find id_choices id in + List.map (fun (descr, term) -> (descr, fun _ _ -> term)) choices + | Symbol (symb, _) -> Hashtbl.find symbol_choices symb + | Num (num, _) -> + List.map + (fun (descr, f) -> (descr, let term = f num in fun _ _ -> term)) + !num_choices) + with Not_found -> assert false + in + (* (3) test an interpretation filling with meta uninterpreted identifiers + *) + let test_interpretation current_interpretation todo_dom = + let filled_interpretation = + Domain.fold + (fun item' interpretation -> + fun item -> + if item = item' then + "Implicit", fun _ _ -> Cic.Implicit + else + interpretation item) + todo_dom current_interpretation + in + let term' = parser_mk_term filled_interpretation in + refine metasenv context term' + in + (* (4) build all possible interpretations *) + let rec aux current_interpretation todo_dom = + if Domain.is_empty todo_dom then + match test_interpretation current_interpretation Domain.empty with + | Ok (term, metasenv) -> [ current_interpretation, term, metasenv ] + | Ko | Uncertain -> [] + else + let item = Domain.choose todo_dom in + debug_print (sprintf "CHOOSED ITEM: %s" + (string_of_interpretation_domain_item item)); + let remaining_dom = Domain.remove item todo_dom in + let choices = lookup_choices item in + let rec filter = function + | [] -> [] + | codomain_item :: tl -> + let new_interpretation = + fun item' -> + if item' = item then + codomain_item + else + current_interpretation item' + in + (match test_interpretation new_interpretation remaining_dom with + | Ok (term, metasenv) -> + (if Domain.is_empty remaining_dom then + [ new_interpretation, term, metasenv ] + else + aux new_interpretation remaining_dom) + @ filter tl + | Uncertain -> + (if Domain.is_empty remaining_dom then + [] + else + aux new_interpretation remaining_dom) + @ filter tl + | Ko -> filter tl) + in + filter choices + in + let (choosed_interpretation, choosed_term, choosed_metasenv) = + match aux current_interpretation todo_dom with + | [] -> raise NoWellTypedInterpretation + | [ x ] -> + debug_print "UNA SOLA SCELTA"; + x + | l -> + debug_print "PIU' SCELTE"; + let choices = + List.map + (fun (interpretation, _, _) -> + List.map + (fun domain_item -> + let description = fst (interpretation domain_item) in +(* + match interpretation domain_item with + | None -> assert false + | Some (descr, _) -> descr + in +*) + (descr_of_domain_item domain_item, description)) + (Domain.elements parser_dom)) + l + in + let choosed = C.interactive_interpretation_choice choices in + List.nth l choosed + in + (Domain.union current_dom todo_dom, choosed_interpretation), + choosed_metasenv, choosed_term + + end + +let apply_interp (interp: interpretation) item = snd (interp item) + +let interpretate ~context ~interp 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, args) -> + let cic_args = List.map (aux loc context) args in + apply_interp interp (Symbol (symb, 0)) interp cic_args + | Ast.Binder (binder_kind, var, typ, body) -> + let cic_type = aux_option loc context typ in + let cic_body = aux loc (Some var :: context) body in + (match binder_kind with + | `Lambda -> Cic.Lambda (var, cic_type, cic_body) + | `Pi | `Forall -> Cic.Prod (var, cic_type, cic_body) + | `Exists -> + apply_interp interp (Symbol ("exists", 0)) interp + [ cic_type; Cic.Lambda (var, cic_type, cic_body) ]) + | Ast.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) = + let rec do_branch' context = function + | [] -> aux loc context term + | hd :: tl -> + let cic_body = do_branch' (Some (Cic.Name hd) :: context) tl in + Cic.Lambda (Cic.Name hd, Cic.Implicit, cic_body) + in + match pat with + | _ :: tl -> (* ignoring constructor *) do_branch' context tl + | [] -> assert false + in + let (indtype_uri, indtype_no) = + match apply_interp interp (Id indty_ident) interp [] with + | Cic.MutInd (uri, tyno, _) -> uri, tyno + | _ -> Parser.fail loc ("Not an inductive type: " ^ indty_ident) + in + Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term, + (List.map do_branch branches)) + | Ast.LetIn (var, def, body) -> + let cic_def = aux loc context def in + let name = Cic.Name var in + let cic_body = aux loc (Some name :: context) body in + Cic.LetIn (name, cic_def, cic_body) + | Ast.LetRec (kind, defs, body) -> + let context' = + List.fold_left (fun acc (var, _, _, _) -> Some (Cic.Name var) :: acc) + context defs + in + let cic_body = aux loc context' body in + let inductiveFuns = + List.map + (fun (var, body, typ, decr_idx) -> + let cic_body = aux loc context' body in + let cic_type = aux_option loc context typ in + (var, decr_idx, cic_type, cic_body)) + defs + in + let counter = ref 0 in + let build_term funs = + (* this is the body of the fold_right function below. Rationale: Fix + * and CoFix cases differs only in an additional index in the + * indcutiveFun list, see Cic.term *) + match kind with + | `Inductive -> + (fun (var, _, _, _) cic -> + incr counter; + Cic.LetIn (Cic.Name var, Cic.Fix (!counter, funs), cic)) + | `CoInductive -> + let funs = + List.map (fun (name, _, typ, body) -> (name, typ, body)) funs + in + (fun (var, _, _, _) cic -> + Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic)) + in + List.fold_right (build_term inductiveFuns) inductiveFuns cic_body + | Ast.Ident (name, subst) -> + let rec find acc e = function + | [] -> raise Not_found + | Some (Cic.Name hd) :: tl when e = hd -> acc + | _ :: tl -> find (acc + 1) e tl + in + (try + let index = find 1 name context in + if subst <> [] then + Parser.fail loc "Explicit substitutions not allowed here"; + Cic.Rel index + with Not_found -> + apply_interp interp (Id name) interp []) + | Ast.Num num -> apply_interp interp (Num (num, 0)) interp [] + | Ast.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 + 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 + | _ -> assert false + diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli new file mode 100644 index 000000000..7093b1c9f --- /dev/null +++ b/helm/ocaml/cic_disambiguation/disambiguate.mli @@ -0,0 +1,60 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +open Disambiguate_struct +open Disambiguate_types + +type interpretation_domain = Domain.t +type domain_and_interpretation = interpretation_domain * interpretation + +(* +val add_symbol_choice: + string -> string * interpretation_codomain_item -> unit +val add_symbol_choices: + string -> (string * interpretation_codomain_item) list -> unit + +val add_num_choice: string * interpretation_codomain_item -> unit +*) + +module Make (C : Callbacks) : + sig + exception NoWellTypedInterpretation + + val disambiguate_input : + MQIConn.handle -> Cic.context -> Cic.metasenv -> + interpretation_domain -> (* items occuring in parser output *) + (interpretation -> Cic.term) -> (* parser output *) + domain_and_interpretation -> (* current interpretation status *) + domain_and_interpretation * Cic.metasenv * Cic.term + (* new interpretstaion status, new metasenv, disambiguated term *) + end + + (* TODO move to CicSomething *) +val term_of_uri: string -> Cic.term + +val interpretate: + context: Cic.name option list -> interp: interpretation -> Ast.term -> + Cic.term + diff --git a/helm/ocaml/cic_disambiguation/disambiguate_struct.ml b/helm/ocaml/cic_disambiguation/disambiguate_struct.ml new file mode 100644 index 000000000..3e477e154 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/disambiguate_struct.ml @@ -0,0 +1,48 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +open Disambiguate_types + +module OrderedDomain = + struct + type t = interpretation_domain_item + let compare = Pervasives.compare + end + +module Domain = Set.Make(OrderedDomain) + +module type Callbacks = + sig + val output_html : ?append_NL:bool -> Ui_logger.html_msg -> unit + val interactive_user_uri_choice : + selection_mode:[`SINGLE | `MULTIPLE] -> + ?ok:string -> + ?enable_button_for_non_vars:bool -> + title:string -> msg:string -> id:string -> string list -> string list + val interactive_interpretation_choice : + (string * string) list list -> int + val input_or_locate_uri : title:string -> UriManager.uri + end + diff --git a/helm/ocaml/cic_disambiguation/disambiguate_types.mli b/helm/ocaml/cic_disambiguation/disambiguate_types.mli new file mode 100644 index 000000000..fc6b0e742 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/disambiguate_types.mli @@ -0,0 +1,36 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +type interpretation_domain_item = + | Id of string (* literal *) + | Symbol of string * int (* literal, instance num *) + | Num of string * int (* literal, instance num *) + +and interpretation_codomain_item = + string * (* description *) + (interpretation -> Cic.term list -> Cic.term) + +and interpretation = interpretation_domain_item -> interpretation_codomain_item + diff --git a/helm/ocaml/cic_disambiguation/lexer.ml b/helm/ocaml/cic_disambiguation/lexer.ml index 79003792b..10f0667f3 100644 --- a/helm/ocaml/cic_disambiguation/lexer.ml +++ b/helm/ocaml/cic_disambiguation/lexer.ml @@ -1,3 +1,27 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) exception Error of int * int * string @@ -12,7 +36,7 @@ let regexp symbol = [^ 'a' - 'z' 'A' - 'Z' '0' - '9' ' ' '\t' '\n' ] let regexp tex_token = '\\' alpha+ let regexp lparen = [ '(' '[' '{' ] let regexp rparen = [ ')' ']' '}' ] -let regexp meta = '?' (alpha | num)+ +let regexp meta = '?' num let keywords = Hashtbl.create 17 let _ = diff --git a/helm/ocaml/cic_disambiguation/lexer.mli b/helm/ocaml/cic_disambiguation/lexer.mli index f8fe7c955..f4cbaa1cb 100644 --- a/helm/ocaml/cic_disambiguation/lexer.mli +++ b/helm/ocaml/cic_disambiguation/lexer.mli @@ -1,3 +1,27 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) exception Error of int * int * string diff --git a/helm/ocaml/cic_disambiguation/logic_notation.ml b/helm/ocaml/cic_disambiguation/logic_notation.ml index 35ce4b90c..f23098f96 100644 --- a/helm/ocaml/cic_disambiguation/logic_notation.ml +++ b/helm/ocaml/cic_disambiguation/logic_notation.ml @@ -1,3 +1,28 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + open Ast open Parser @@ -5,19 +30,17 @@ EXTEND term: LEVEL "add" [ [ t1 = term; SYMBOL "∨"; t2 = term -> - return_term loc (Appl [Ident ("or", []); t1; t2]) + return_term loc (Appl_symbol ("or", [t1; t2])) ] ]; term: LEVEL "mult" [ [ t1 = term; SYMBOL "∧"; t2 = term -> - return_term loc (Appl [Ident ("and", []); t1; t2]) + return_term loc (Appl_symbol ("and", [t1; t2])) ] ]; term: LEVEL "inv" [ - [ SYMBOL "¬"; t = term -> - return_term loc (Appl [Ident ("not", []); t]) - ] + [ SYMBOL "¬"; t = term -> return_term loc (Appl_symbol ("not", [t])) ] ]; END diff --git a/helm/ocaml/cic_disambiguation/macro.ml b/helm/ocaml/cic_disambiguation/macro.ml index fd93aa9ae..a3e3cbf25 100644 --- a/helm/ocaml/cic_disambiguation/macro.ml +++ b/helm/ocaml/cic_disambiguation/macro.ml @@ -1,3 +1,27 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) exception Macro_not_found of string exception Utf8_not_found of string diff --git a/helm/ocaml/cic_disambiguation/macro.mli b/helm/ocaml/cic_disambiguation/macro.mli index 5f8cf5994..39613d0df 100644 --- a/helm/ocaml/cic_disambiguation/macro.mli +++ b/helm/ocaml/cic_disambiguation/macro.mli @@ -1,3 +1,27 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) exception Macro_not_found of string exception Utf8_not_found of string diff --git a/helm/ocaml/cic_disambiguation/make_table.ml b/helm/ocaml/cic_disambiguation/make_table.ml index 770fe2b05..50780759d 100644 --- a/helm/ocaml/cic_disambiguation/make_table.ml +++ b/helm/ocaml/cic_disambiguation/make_table.ml @@ -1,3 +1,27 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) open Printf open Pxp_types diff --git a/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml b/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml index 044f8ae02..afc9f63af 100644 --- a/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml +++ b/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml @@ -1,3 +1,27 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) let debug = false let debug_print = if debug then prerr_endline else ignore diff --git a/helm/ocaml/cic_disambiguation/parser.ml b/helm/ocaml/cic_disambiguation/parser.ml index 0ee41ab2a..13f9fc42d 100644 --- a/helm/ocaml/cic_disambiguation/parser.ml +++ b/helm/ocaml/cic_disambiguation/parser.ml @@ -1,5 +1,35 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) -open Ast +let debug = true +let debug_print s = + if debug then begin + prerr_endline ""; + prerr_endline s; + prerr_endline "" + end let grammar = Grammar.gcreate Lexer.lex @@ -7,7 +37,11 @@ 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 = LocatedTerm (loc, term) +let return_term loc term = Ast.LocatedTerm (loc, term) +(* let return_term loc term = term *) + +let fail (x, y) msg = + failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg) EXTEND GLOBAL: term; @@ -34,8 +68,8 @@ EXTEND substs ] -> (match subst with - | Some l -> Ident (s, l) - | None -> Ident (s, [])) + | Some l -> Ast.Ident (s, l) + | None -> Ast.Ident (s, [])) ] ]; name: [ (* as substituted_name with no explicit substitution *) @@ -46,35 +80,55 @@ EXTEND | LPAREN "("; names = LIST1 name; RPAREN ")" -> names ] ]; term: - [ "add" LEFTA [ (* nothing here by default *) ] - | "mult" LEFTA [ (* nothing here by default *) ] - | "inv" NONA [ (* nothing here by default *) ] + [ "arrow" RIGHTA + [ t1 = term; SYMBOL <:unicode>; t2 = term -> + return_term loc (Ast.Binder (`Pi, Cic.Anonymous, Some t1, t2)) + ] + | "eq" LEFTA + [ t1 = term; SYMBOL "="; t2 = term -> + return_term loc (Ast.Appl_symbol ("eq", [t1; t2])) + ] + | "add" LEFTA [ (* nothing here by default *) ] + | "mult" LEFTA [ (* nothing here by default *) ] + | "inv" NONA [ (* nothing here by default *) ] | "simple" NONA [ b = binder; vars = LIST1 IDENT SEP SYMBOL ","; typ = OPT [ SYMBOL ":"; t = term -> t ]; SYMBOL "."; body = term -> let binder = - List.fold_right (fun var body -> Binder (b, var, typ, body)) + List.fold_right + (fun var body -> Ast.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 | n = substituted_name -> return_term loc n | LPAREN "("; head = term; args = LIST1 term; RPAREN ")" -> - return_term loc (Appl (head :: args)) - | i = INT -> return_term loc (Int (int_of_string i)) + return_term loc (Ast.Appl (head :: args)) + | i = INT -> return_term loc (Ast.Num i) | m = META; substs = [ LPAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; RPAREN "]" -> substs ] -> - return_term loc (Meta (m, substs)) + let index = + try + int_of_string (String.sub m 1 (String.length m - 1)) + with Failure "int_of_string" -> + fail loc ("Invalid meta variable number: " ^ m) + in + return_term loc (Ast.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 (LetIn (name, t1, t2)) - | "let"; "rec"; defs = LIST1 [ + return_term loc (Ast.LetIn (name, t1, t2)) + | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; + defs = LIST1 [ name = IDENT; index = OPT [ LPAREN "("; index = INT; RPAREN ")" -> int_of_string index @@ -84,15 +138,17 @@ EXTEND (name, t1, typ, (match index with None -> 1 | Some i -> i)) ] SEP (IDENT "and"); IDENT "in"; body = term -> - return_term loc (LetRec (defs, body)) - | typ = OPT [ LPAREN "["; typ = term; RPAREN "]" -> typ ]; - "match"; t = term; "with"; + return_term loc (Ast.LetRec (ind_kind, defs, body)) + | outtyp = OPT [ LPAREN "["; typ = term; RPAREN "]" -> typ ]; + "match"; t = term; + SYMBOL ":"; indty = IDENT; + "with"; LPAREN "["; patterns = LIST0 [ - p = pattern; SYMBOL <:unicode> (* ⇒*); t = term -> (p, t) + p = pattern; SYMBOL <:unicode> (* ⇒ *); t = term -> (p, t) ] SEP SYMBOL "|"; RPAREN "]" -> - return_term loc (Case (t, typ, patterns)) + return_term loc (Ast.Case (t, indty, outtyp, patterns)) | LPAREN "("; t = term; RPAREN ")" -> return_term loc t ] ]; @@ -100,3 +156,209 @@ END let parse_term = Grammar.Entry.parse term +(* +open Disambiguate_struct +open ProofEngineHelpers + +exception UnknownIdentifier of string +exception InductiveTypeExpected + +let list_of_domain dom = Domain.fold (fun s acc -> s :: acc) dom [] +let apply_interp (interp: interpretation) item = snd (interp item) + +let pre_disambiguate ~context ast = + let rec aux loc context = function + | Ast.LocatedTerm (loc, term) -> aux loc context term + | Ast.Appl terms -> + let (dom, funs) = + List.fold_left + (fun (dom, funs) term -> + let (dom', f) = aux loc context term in + (Domain.union dom dom', f :: funs)) + (Domain.empty, []) + terms + in + let f interp = + Cic.Appl (List.map (fun f -> f interp) (List.rev funs)) + in + (dom, f) + | Ast.Appl_symbol (symb, args) -> + let (dom, funs) = + List.fold_left + (fun (dom, funs) term -> + let (dom', f) = aux loc context term in + (Domain.union dom dom', f :: funs)) + (Domain.empty, []) + args + in + (Domain.add (Symbol (symb, 0)) dom, + (fun interp -> + apply_interp interp (Symbol (symb, 0)) interp + (List.map (fun f -> f interp) funs))) + | Ast.Binder (binder_kind, var, typ, body) -> + let (type_dom, type_f) = + match typ with + | Some t -> aux loc context t + | None -> (Domain.empty, (fun _ -> Cic.Implicit)) + in + let (dom', body_f) = aux loc (Some var :: context) body in + let dom'' = Domain.union dom' type_dom in + (dom'', + match binder_kind with + | `Lambda -> + (fun interp -> + Cic.Lambda (var, type_f interp, body_f interp)) + | `Pi | `Forall -> + (fun interp -> + Cic.Prod (var, type_f interp, body_f interp)) + | `Exists -> + (fun interp -> + let typ = type_f interp in + Cic.Appl + [ apply_interp interp (Id "ex") interp []; + typ; + (Cic.Lambda (var, typ, body_f interp)) ])) + | Ast.Case (term, indty_ident, outtype, branches) -> + let (term_dom, term_f) = aux loc context term in + let (outtype_dom, outtype_f) = + match outtype with + | Some typ -> aux loc context typ + | None -> (Domain.empty, (fun _ -> Cic.Implicit)) + in + let do_branch (pat, term) = + let rec do_branch' context = function + | [] -> aux loc context term + | hd :: tl -> + let (dom, f) = do_branch' (Some (Cic.Name hd) :: context) tl in + (dom, + (fun interp -> + Cic.Lambda (Cic.Name hd, Cic.Implicit, f interp))) + in + match pat with + | _ :: tl -> (* ignoring constructor *) + do_branch' context tl + | [] -> assert false + in + let (branches_dom, branches_f) = + List.fold_right + (fun branch (dom, f) -> + let (dom', f') = do_branch branch in + Domain.union dom dom', (fun interp -> f' interp :: f interp)) + branches + (Domain.empty, (fun _ -> [])) + in + (Domain.union outtype_dom (Domain.union term_dom branches_dom), + (fun interp -> + let (indtype_uri, indtype_no) = + match apply_interp interp (Id indty_ident) interp [] with + | Cic.MutInd (uri, tyno, _) -> uri, tyno + | _ -> assert false + in + Cic.MutCase (indtype_uri, indtype_no, outtype_f interp, + term_f interp, branches_f interp))) + | Ast.LetIn (var, body, where) -> + let (body_dom, body_f) = aux loc context body in + let (where_dom, where_f) = aux loc context where in + (Domain.union body_dom where_dom, + fun interp -> Cic.LetIn (Cic.Name var, body_f interp, where_f interp)) + | Ast.LetRec (kind, defs, where) -> + let context' = + List.fold_left (fun acc (var, _, _, _) -> Some (Cic.Name var) :: acc) + context defs + in + let (where_dom, where_f) = aux loc context' where in + let inductiveFuns = + List.map + (fun (var, body, typ, decr_idx) -> + let body_dom, body_f = aux loc context' body in + let typ_dom, typ_f = + match typ with + | None -> (Domain.empty, (fun _ -> Cic.Implicit)) + | Some typ -> aux loc context' typ + in + (Domain.union body_dom typ_dom, + (fun interp -> + (var, decr_idx, typ_f interp, body_f interp)))) + defs + in + let dom = + List.fold_left (fun acc (dom, _) -> Domain.union acc dom) + where_dom inductiveFuns + in + let inductiveFuns interp = + List.map (fun (_, g) -> g interp) inductiveFuns + in + let build_term counter funs = + (* this is the body of the fold_right function below. Rationale: Fix + * and CoFix cases differs only in an additional index in the + * indcutiveFun list, see Cic.term *) + match kind with + | `Inductive -> + (fun (var, _, _, _) cic -> + incr counter; + Cic.LetIn (Cic.Name var, Cic.Fix (!counter, funs), cic)) + | `CoInductive -> + let funs = + List.map (fun (name, _, typ, body) -> (name, typ, body)) funs + in + (fun (var, _, _, _) cic -> + Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic)) + in + (dom, + (fun interp -> + let counter = ref 0 in + let funs = inductiveFuns interp in + List.fold_right (build_term counter funs) funs (where_f interp))) + | Ast.Ident (name, subst) -> + (* TODO hanlde explicit substitutions *) + let rec find acc e = function + | [] -> raise Not_found + | Some (Cic.Name hd) :: tl when e = hd -> acc + | _ :: tl -> find (acc + 1) e tl + in + (try + let index = find 1 name context in + if subst <> [] then + fail loc "Explicit substitutions not allowed here"; + (Domain.empty, fun _ -> Cic.Rel index) + with Not_found -> + (Domain.singleton (Id name), + (fun interp -> apply_interp interp (Id name) interp []))) + | Ast.Num num -> + (* TODO check to see if num can be removed from the domain *) + (Domain.singleton (Num (num, 0)), + (fun interp -> apply_interp interp (Num (num, 0)) interp [])) + | Ast.Meta (index, subst) -> + let (dom, funs) = + List.fold_left + (fun (dom, funs) term -> + match term with + | None -> (dom, (fun _ -> None) :: funs) + | Some term -> + let (dom', f) = aux loc context term in + (Domain.union dom dom', + (fun interp -> Some (f interp)) :: funs)) + (Domain.empty, []) + subst + in + let f interp = + Cic.Meta (index, List.map (fun f -> f interp) (List.rev funs)) + in + (dom, f) + | Ast.Sort `Prop -> Domain.empty, fun _ -> Cic.Sort Cic.Prop + | Ast.Sort `Set -> Domain.empty, fun _ -> Cic.Sort Cic.Set + | Ast.Sort `Type -> Domain.empty, fun _ -> Cic.Sort Cic.Type + | Ast.Sort `CProp -> Domain.empty, fun _ -> Cic.Sort Cic.CProp + in + match ast with + | Ast.LocatedTerm (loc, term) -> + let (dom, f) = aux loc context term in + dom, f + | _ -> assert false + +let main ~context char_stream = + let term_ast = parse_term char_stream in + debug_print (Pp.pp_term term_ast); + pre_disambiguate ~context term_ast +*) + diff --git a/helm/ocaml/cic_disambiguation/parser.mli b/helm/ocaml/cic_disambiguation/parser.mli new file mode 100644 index 000000000..2a70d5091 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/parser.mli @@ -0,0 +1,46 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(** {2 Parsing functions} *) + +val parse_term: char Stream.t -> Ast.term + +(** {2 Grammar extensions} *) + +val term: Ast.term Grammar.Entry.e + +val return_term: Ast.location -> Ast.term -> Ast.term + + (** raise a parse error *) +val fail: Ast.location -> string -> 'a + +(* +open Disambiguate_types + +val main: + context:Cic.name option list -> char Stream.t -> + Domain.t * (interpretation -> Cic.term) +*) + diff --git a/helm/ocaml/cic_disambiguation/pp.ml b/helm/ocaml/cic_disambiguation/pp.ml index 6ee9cf39a..c4b04351c 100644 --- a/helm/ocaml/cic_disambiguation/pp.ml +++ b/helm/ocaml/cic_disambiguation/pp.ml @@ -1,3 +1,27 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) open Ast open Printf @@ -10,21 +34,26 @@ let pp_binder = function let rec pp_term = function | LocatedTerm ((p_begin, p_end), term) -> - sprintf "[%d,%d]%s" p_begin p_end (pp_term term) +(* sprintf "[%d,%d]%s" p_begin p_end (pp_term term) *) + pp_term term | Appl terms -> sprintf "(%s)" (String.concat " " (List.map pp_term terms)) + | Appl_symbol (symbol, terms) -> + sprintf "(%s %s)" symbol (String.concat " " (List.map pp_term terms)) | Binder (kind, var, typ, body) -> - sprintf "\\%s %s%s.%s" (pp_binder kind) var + sprintf "\\%s %s%s.%s" (pp_binder kind) + (match var with Cic.Anonymous -> "_" | Cic.Name s -> s) (match typ with None -> "" | Some typ -> ": " ^ pp_term typ) (pp_term body) - | Case (term, typ, patterns) -> + | Case (term, indtype, typ, patterns) -> sprintf "%smatch %s with %s" (match typ with None -> "" | Some t -> sprintf "<%s>" (pp_term t)) (pp_term term) (pp_patterns patterns) | LetIn (name, t1, t2) -> sprintf "let %s = %s in %s" name (pp_term t1) (pp_term t2) - | LetRec (definitions, term) -> - sprintf "let rec %s in %s" + | LetRec (kind, definitions, term) -> + sprintf "let %s %s in %s" + (match kind with `Inductive -> "rec" | `CoInductive -> "corec") (String.concat " and " (List.map (fun (name, body, typ, index) -> @@ -35,11 +64,15 @@ let rec pp_term = function (pp_term term) | Ident (name, []) -> name | Ident (name, substs) -> sprintf "%s[%s]" name (pp_substs substs) - | Meta (name, substs) -> - sprintf "%s[%s]" name + | Meta (index, substs) -> + sprintf "%d[%s]" index (String.concat "; " (List.map (function None -> "_" | Some term -> pp_term term) substs)) - | Int num -> string_of_int num + | Num num -> num + | Sort `Set -> "Set" + | Sort `Prop -> "Prop" + | Sort `Type -> "Type" + | Sort `CProp -> "CProp" and pp_subst (name, term) = sprintf "%s := %s" name (pp_term term) and pp_substs substs = String.concat "; " (List.map pp_subst substs) diff --git a/helm/ocaml/cic_disambiguation/pp.mli b/helm/ocaml/cic_disambiguation/pp.mli index 078517c56..44fa63323 100644 --- a/helm/ocaml/cic_disambiguation/pp.mli +++ b/helm/ocaml/cic_disambiguation/pp.mli @@ -1 +1,26 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + val pp_term: Ast.term -> string diff --git a/helm/ocaml/cic_disambiguation/test_lexer.ml b/helm/ocaml/cic_disambiguation/test_lexer.ml index 8667953c3..bff5cde99 100644 --- a/helm/ocaml/cic_disambiguation/test_lexer.ml +++ b/helm/ocaml/cic_disambiguation/test_lexer.ml @@ -1,3 +1,28 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + let ic = open_in Sys.argv.(1) in let token_stream = fst (Lexer.lex.Token.tok_func (Stream.of_channel ic)) in let rec dump () = diff --git a/helm/ocaml/cic_disambiguation/test_parser.ml b/helm/ocaml/cic_disambiguation/test_parser.ml index 41634cbb3..fdab36ef3 100644 --- a/helm/ocaml/cic_disambiguation/test_parser.ml +++ b/helm/ocaml/cic_disambiguation/test_parser.ml @@ -1,3 +1,28 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + try let ic = open_in Sys.argv.(1) in let term = Parser.parse_term (Stream.of_channel ic) in -- 2.39.2