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
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)
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 $<
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 $@ $<
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 $<
+
+(* 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
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
| 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
| 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, <pattern,action> list *)
+ | Case of term * string * term option * (case_pattern * term) list
+ (* what to match,
inductive type, out type, <pattern,action> 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
--- /dev/null
+(* 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 <description, term> *)
+ 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
+
--- /dev/null
+(* 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
+
--- /dev/null
+(* 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
+
--- /dev/null
+(* 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
+
+(* 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
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 _ =
+(* 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
+(* 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
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
+(* 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
+(* 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
+(* 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
+(* 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
+(* 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 "<NEW_TEXTUAL_PARSER>";
+ prerr_endline s;
+ prerr_endline "</NEW_TEXTUAL_PARSER>"
+ end
let grammar = Grammar.gcreate Lexer.lex
(* 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;
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 *)
| 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<to>>; 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<def>> (* ≝ *); 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
(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<Rightarrow>> (* ⇒*); t = term -> (p, t)
+ p = pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *); 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
]
];
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
+*)
+
--- /dev/null
+(* 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)
+*)
+
+(* 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
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) ->
(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)
+(* 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
+(* 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 () =
+(* 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
projects / helm.git / commitdiff