From 358d1d55044347255aacb8daf03de0dbb18bc668 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 19 Jan 2004 11:43:03 +0000 Subject: [PATCH] snapshot, almost working TODO: - domain processing order - notation generation --- helm/ocaml/cic_disambiguation/.depend | 20 +- helm/ocaml/cic_disambiguation/Makefile | 5 +- .../ocaml/cic_disambiguation/arit_notation.ml | 44 +- helm/ocaml/cic_disambiguation/ast.mli | 6 +- helm/ocaml/cic_disambiguation/disambiguate.ml | 487 ++++++++++-------- .../ocaml/cic_disambiguation/disambiguate.mli | 53 +- .../cic_disambiguation/disambiguate_struct.ml | 48 -- .../cic_disambiguation/disambiguate_types.ml | 47 ++ .../cic_disambiguation/disambiguate_types.mli | 30 +- helm/ocaml/cic_disambiguation/lexer.ml | 82 ++- .../cic_disambiguation/logic_notation.ml | 26 +- .../cic_disambiguation/pa_unicode_macro.ml | 2 +- helm/ocaml/cic_disambiguation/parser.ml | 212 +------- helm/ocaml/cic_disambiguation/parser.mli | 8 - helm/ocaml/cic_disambiguation/pp.ml | 4 +- helm/ocaml/cic_disambiguation/test_lexer.ml | 6 +- helm/ocaml/cic_disambiguation/test_parser.ml | 6 +- helm/ocaml/cic_disambiguation/tests/match.txt | 18 + 18 files changed, 532 insertions(+), 572 deletions(-) delete mode 100644 helm/ocaml/cic_disambiguation/disambiguate_struct.ml create mode 100644 helm/ocaml/cic_disambiguation/disambiguate_types.ml create mode 100644 helm/ocaml/cic_disambiguation/tests/match.txt diff --git a/helm/ocaml/cic_disambiguation/.depend b/helm/ocaml/cic_disambiguation/.depend index 90354741c..00cb03a9a 100644 --- a/helm/ocaml/cic_disambiguation/.depend +++ b/helm/ocaml/cic_disambiguation/.depend @@ -1,21 +1,19 @@ pp.cmi: ast.cmi -disambiguate.cmi: ast.cmi disambiguate_struct.cmo disambiguate_types.cmi +disambiguate.cmi: ast.cmi disambiguate_types.cmi parser.cmi: ast.cmi +disambiguate_types.cmo: disambiguate_types.cmi +disambiguate_types.cmx: disambiguate_types.cmi pp.cmo: ast.cmi pp.cmi pp.cmx: ast.cmi pp.cmi macro.cmo: macro.cmi macro.cmx: macro.cmi lexer.cmo: macro.cmi lexer.cmi lexer.cmx: macro.cmx lexer.cmi -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 +disambiguate.cmo: ast.cmi disambiguate_types.cmi parser.cmi disambiguate.cmi +disambiguate.cmx: ast.cmi disambiguate_types.cmx parser.cmx disambiguate.cmi +logic_notation.cmo: ast.cmi disambiguate.cmi parser.cmi +logic_notation.cmx: ast.cmi disambiguate.cmx parser.cmx +arit_notation.cmo: ast.cmi disambiguate.cmi parser.cmi +arit_notation.cmx: ast.cmi disambiguate.cmx parser.cmx diff --git a/helm/ocaml/cic_disambiguation/Makefile b/helm/ocaml/cic_disambiguation/Makefile index 11da72469..3a0ae7b80 100644 --- a/helm/ocaml/cic_disambiguation/Makefile +++ b/helm/ocaml/cic_disambiguation/Makefile @@ -8,7 +8,8 @@ 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 disambiguate_struct.ml parser.ml \ + disambiguate_types.ml \ + pp.ml macro.ml lexer.ml parser.ml \ disambiguate.ml \ $(patsubst %,%_notation.ml,$(NOTATIONS)) \ @@ -58,4 +59,6 @@ depend: macro.cmi macro.cmo pa_unicode_macro.cmi pa_unicode_macro.cmo disambiguate_types.cmi: disambiguate_types.mli $(OCAMLC) -c -rectypes $< +disambiguate_types.cmo: disambiguate_types.ml disambiguate_types.cmi + $(OCAMLC) -c -rectypes $< diff --git a/helm/ocaml/cic_disambiguation/arit_notation.ml b/helm/ocaml/cic_disambiguation/arit_notation.ml index 998688cbe..b4aaf3398 100644 --- a/helm/ocaml/cic_disambiguation/arit_notation.ml +++ b/helm/ocaml/cic_disambiguation/arit_notation.ml @@ -26,25 +26,59 @@ open Ast open Parser +(* +let i = ref max_int +let get_i () = decr i; !i +*) + EXTEND term: LEVEL "add" [ [ t1 = term; SYMBOL "+"; t2 = term -> - return_term loc (Appl_symbol ("plus", [t1; t2])) + return_term loc (Appl_symbol ("plus", 0, [t1; t2])) | t1 = term; SYMBOL "-"; t2 = term -> - return_term loc (Appl_symbol ("minus", [t1; t2])) + return_term loc (Appl_symbol ("minus", 0, [t1; t2])) ] ]; term: LEVEL "mult" [ [ t1 = term; SYMBOL "*"; t2 = term -> - return_term loc (Appl_symbol ("times", [t1; t2])) + return_term loc (Appl_symbol ("times", 0, [t1; t2])) | t1 = term; SYMBOL "/"; t2 = term -> - return_term loc (Appl_symbol ("div", [t1; t2])) + return_term loc (Appl_symbol ("div", 0, [t1; t2])) ] ]; term: LEVEL "inv" [ - [ SYMBOL "-"; t = term -> return_term loc (Appl_symbol ("uminus", [t])) ] + [ SYMBOL "-"; t = term -> + return_term loc (Appl_symbol ("uminus", 0, [t])) + ] ]; END + +let _ = + Disambiguate.add_num_choice + ("natural number", + (fun _ num _ -> HelmLibraryObjects.build_nat (int_of_string num))); + Disambiguate.add_num_choice + ("real number", + (fun _ num _ -> HelmLibraryObjects.build_real (int_of_string num))); + Disambiguate.add_symbol_choice "plus" + ("natural plus", + (fun env _ args -> + let t1, t2 = + match args with + | [t1; t2] -> t1, t2 + | _ -> raise Disambiguate.Invalid_choice + in + Cic.Appl [ HelmLibraryObjects.Peano.plus; t1; t2 ])); + Disambiguate.add_symbol_choice "plus" + ("real plus", + (fun env _ args -> + let t1, t2 = + match args with + | [t1; t2] -> t1, t2 + | _ -> raise Disambiguate.Invalid_choice + in + Cic.Appl [ HelmLibraryObjects.Reals.rplus; t1; t2 ])); + diff --git a/helm/ocaml/cic_disambiguation/ast.mli b/helm/ocaml/cic_disambiguation/ast.mli index 19f4bd6bd..b7267ee57 100644 --- a/helm/ocaml/cic_disambiguation/ast.mli +++ b/helm/ocaml/cic_disambiguation/ast.mli @@ -69,7 +69,7 @@ type term = | LocatedTerm of location * term | Appl of term list - | Appl_symbol of string * term list + | Appl_symbol of string * int * term list (* literal, args, instance *) | Binder of binder_kind * Cic.name * term option * term (* kind, name, type, body *) | Case of term * string * term option * (case_pattern * term) list @@ -77,9 +77,9 @@ type term = | LetIn of string * term * term (* name, body, where *) | LetRec of induction_kind * (string * term * term option * int) list * term (* (name, body, type, decreasing argument) list, where *) - | Ident of string * subst list + | Ident of string * subst list (* literal, substitutions *) | Meta of int * meta_subst list - | Num of string + | Num of string * int (* literal, instance *) | Sort of sort_kind and meta_subst = term option diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 827bbe2d4..aa3fe97ee 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -23,61 +23,34 @@ * http://helm.cs.unibo.it/ *) -open Disambiguate_struct open Disambiguate_types -let debug = true -let debug_print = if debug then prerr_endline else ignore +exception Invalid_choice +exception No_choices of domain_item +exception NoWellTypedInterpretation -type interpretation_domain = Domain.t -type domain_and_interpretation = interpretation_domain * interpretation + (** raised when an environment is not enough informative to decide *) +exception Try_again -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 debug = true +let debug_print = if debug then prerr_endline else ignore 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 + | Num i -> string_of_int i -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 symbol_choices = Hashtbl.create 1023 +let num_choices = ref [] -let add_num_choice choice = - num_choices := choice :: !num_choices +let add_symbol_choice symbol codomain_item = + let current_choices = + try + Hashtbl.find symbol_choices symbol + with Not_found -> [] + in + Hashtbl.replace symbol_choices symbol (codomain_item :: current_choices) +let add_num_choice choice = num_choices := choice :: !num_choices type test_result = | Ok of Cic.term * Cic.metasenv @@ -93,9 +66,11 @@ let refine metasenv context term = | CicRefine.MutCaseFixAndCofixRefineNotImplemented -> (* TODO remove this case as soon as refine is fully implemented *) (try + debug_print (Printf.sprintf "TYPE CHECKER %s" (CicPp.ppterm term)); let term' = CicTypeChecker.type_of_aux' metasenv context term in Ok (term',metasenv) - with _ -> Ko) +(* with _ -> Ko) *) + with _ -> Uncertain) | CicRefine.Uncertain _ -> debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ; Uncertain @@ -146,181 +121,33 @@ let term_of_uri uri = 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 resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () = + snd (Environment.find item env) env num args -let apply_interp (interp: interpretation) item = snd (interp item) +let find_in_environment name context = + let rec aux acc = function + | [] -> raise Not_found + | Cic.Name hd :: tl when hd = name -> acc + | _ :: tl -> aux (acc + 1) tl + in + aux 1 context -let interpretate ~context ~interp ast = +let interpretate ~context ~env ast = let rec aux loc context = function | Ast.LocatedTerm (loc, term) -> aux loc context term | Ast.Appl terms -> Cic.Appl (List.map (aux loc context) terms) - | Ast.Appl_symbol (symb, args) -> + | Ast.Appl_symbol (symb, i, args) -> let cic_args = List.map (aux loc context) args in - apply_interp interp (Symbol (symb, 0)) interp cic_args + resolve env (Symbol (symb, i)) ~args: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 + let cic_body = aux loc (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) ]) + resolve env (Symbol ("exists", 0)) + ~args:[ 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 @@ -328,7 +155,7 @@ let interpretate ~context ~interp ast = let rec do_branch' context = function | [] -> aux loc context term | hd :: tl -> - let cic_body = do_branch' (Some (Cic.Name hd) :: context) tl in + let cic_body = do_branch' (Cic.Name hd :: context) tl in Cic.Lambda (Cic.Name hd, Cic.Implicit, cic_body) in match pat with @@ -336,8 +163,9 @@ let interpretate ~context ~interp ast = | [] -> assert false in let (indtype_uri, indtype_no) = - match apply_interp interp (Id indty_ident) interp [] with + match resolve env (Id indty_ident) () with | Cic.MutInd (uri, tyno, _) -> uri, tyno + | Cic.Implicit -> raise Try_again | _ -> Parser.fail loc ("Not an inductive type: " ^ indty_ident) in Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term, @@ -345,11 +173,11 @@ let interpretate ~context ~interp ast = | 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 + let cic_body = aux loc (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) + List.fold_left (fun acc (var, _, _, _) -> Cic.Name var :: acc) context defs in let cic_body = aux loc context' body in @@ -380,19 +208,14 @@ let interpretate ~context ~interp ast = 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 + (* TODO hanlde explicit substitutions *) (try - let index = find 1 name context in + let index = find_in_environment 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 [] + with Not_found -> resolve env (Id name) ()) + | Ast.Num (num, i) -> resolve env (Num i) ~num () | Ast.Meta (index, subst) -> let cic_subst = List.map @@ -412,3 +235,223 @@ let interpretate ~context ~interp ast = | Ast.LocatedTerm (loc, term) -> aux loc context term | _ -> assert false +let domain_of_term ~context ast = + let rec aux loc context = function + | Ast.LocatedTerm (_, term) -> aux loc context term + | Ast.Appl terms -> + List.fold_left (fun dom term -> Domain.union dom (aux loc context term)) + Domain.empty terms + | Ast.Appl_symbol (symb, i, args) -> + List.fold_left (fun dom term -> Domain.union dom (aux loc context term)) + (Domain.singleton (Symbol (symb, i))) args + | Ast.Binder (_, var, typ, body) -> + let type_dom = aux_option loc context typ in + let body_dom = aux loc (var :: context) body in + Domain.union type_dom body_dom + | Ast.Case (term, indty_ident, outtype, branches) -> + let term_dom = aux loc context term in + let outtype_dom = aux_option loc context outtype in + let do_branch (pat, term) = + match pat with + | _ :: tl -> + aux loc + (List.fold_left (fun acc var -> (Cic.Name var) :: acc) + context tl) + term + | [] -> assert false + in + let branches_dom = + List.fold_left (fun dom branch -> Domain.union dom (do_branch branch)) + Domain.empty branches + in + Domain.add (Id indty_ident) + (Domain.union outtype_dom (Domain.union term_dom branches_dom)) + | Ast.LetIn (var, body, where) -> + let body_dom = aux loc context body in + let where_dom = aux loc (Cic.Name var :: context) where in + Domain.union body_dom where_dom + | Ast.LetRec (kind, defs, where) -> + let context' = + List.fold_left (fun acc (var, _, _, _) -> Cic.Name var :: acc) + context defs + in + let where_dom = aux loc context' where in + let defs_dom = + List.fold_left + (fun dom (_, body, typ, _) -> + Domain.union (aux loc context' body) (aux_option loc context typ)) + Domain.empty defs + in + Domain.union where_dom defs_dom + | Ast.Ident (name, subst) -> + (* TODO hanlde explicit substitutions *) + (try + let index = find_in_environment name context in + if subst <> [] then + Parser.fail loc "Explicit substitutions not allowed here"; + Domain.empty + with Not_found -> Domain.singleton (Id name)) + | Ast.Num (num, i) -> Domain.singleton (Num i) + | Ast.Meta (index, local_context) -> + List.fold_left + (fun dom term -> Domain.union dom (aux_option loc context term)) + Domain.empty local_context + | Ast.Sort _ -> Domain.empty + and aux_option loc context = function + | None -> Domain.empty + | Some t -> aux loc context t + in + match ast with + | Ast.LocatedTerm (loc, term) -> aux loc context term + | _ -> assert false + +module Make (C: Callbacks) = + struct + 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, let term = term_of_uri uri in fun _ _ _ -> term)) + uris' + + let disambiguate_term mqi_handle context metasenv term ~aliases:current_env + = + let current_dom = (* TODO temporary, remove ASAP *) + Environment.fold (fun item _ dom -> Domain.add item dom) + current_env Domain.empty + in + debug_print "NEW DISAMBIGUATE INPUT"; + let disambiguate_context = (* cic context -> disambiguate context *) + List.map + (function None -> Cic.Anonymous | Some (name, _) -> name) + context + in + let term_dom = domain_of_term ~context:disambiguate_context term in + debug_print (sprintf "DISAMBIGUATION DOMAIN: %s" + (string_of_domain term_dom)); + let todo_dom = Domain.diff term_dom current_dom in + (* (2) lookup function for any item (Id/Symbol/Num) *) + let lookup_choices = + let id_choices = Hashtbl.create 1023 in + fun item -> + let choices = + match item with + | Id id -> + (try + Hashtbl.find id_choices id + with Not_found -> + let choices = choices_of_id mqi_handle id in + Hashtbl.add id_choices id choices; + choices) + | Symbol (symb, _) -> + (try Hashtbl.find symbol_choices symb with Not_found -> []) + | Num instance -> !num_choices + in + if choices = [] then raise (No_choices item); + choices + in + (* (3) test an interpretation filling with meta uninterpreted identifiers + *) + let test_env current_env todo_dom = + let filled_env = + Domain.fold + (fun item env -> + Environment.add item ("Implicit", fun _ _ _ -> Cic.Implicit) env) + todo_dom current_env + in + try + let cic_term = + interpretate ~context:disambiguate_context ~env:filled_env term + in + debug_print + (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm cic_term)); + refine metasenv context cic_term + with + | Try_again -> Uncertain + | Invalid_choice -> Ko + in + (* (4) build all possible interpretations *) + let rec aux current_env todo_dom = + if Domain.is_empty todo_dom then + match test_env current_env Domain.empty with + | Ok (term, metasenv) -> [ current_env, term, metasenv ] + | Ko | Uncertain -> [] + else + let item = Domain.choose todo_dom in + let remaining_dom = Domain.remove item todo_dom in + debug_print (sprintf "CHOOSED ITEM: %s" (string_of_domain_item item)); + let choices = lookup_choices item in + let rec filter = function + | [] -> [] + | codomain_item :: tl -> + let new_env = Environment.add item codomain_item current_env in + (match test_env new_env remaining_dom with + | Ok (term, metasenv) -> + (if Domain.is_empty remaining_dom then + [ new_env, term, metasenv ] + else + aux new_env remaining_dom) + @ filter tl + | Uncertain -> + (if Domain.is_empty remaining_dom then + [] + else + aux new_env remaining_dom) + @ filter tl + | Ko -> filter tl) + in + filter choices + in + let (choosed_env, choosed_term, choosed_metasenv) = + match aux current_env todo_dom with + | [] -> raise NoWellTypedInterpretation + | [ x ] -> + debug_print "UNA SOLA SCELTA"; + x + | l -> + debug_print (sprintf "PIU' SCELTE (%d)" (List.length l)); + let choices = + List.map + (fun (env, _, _) -> + List.map + (fun domain_item -> + let description = + fst (Environment.find domain_item env) + in + (descr_of_domain_item domain_item, description)) + (Domain.elements term_dom)) + l + in + let choosed = C.interactive_interpretation_choice choices in + List.nth l choosed + in + (choosed_env, choosed_metasenv, choosed_term) + + end + diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli index 7093b1c9f..5f797ab5d 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate.mli @@ -23,38 +23,37 @@ * http://helm.cs.unibo.it/ *) -open Disambiguate_struct open Disambiguate_types -type interpretation_domain = Domain.t -type domain_and_interpretation = interpretation_domain * interpretation + (* TODO move to CicSomething *) +val term_of_uri: string -> Cic.term -(* -val add_symbol_choice: - string -> string * interpretation_codomain_item -> unit -val add_symbol_choices: - string -> (string * interpretation_codomain_item) list -> unit +(** {2 Choice registration interface} *) -val add_num_choice: string * interpretation_codomain_item -> unit -*) + (** to be raised when a choice is invalid due to some given parameter (e.g. + * wrong number of Cic.term arguments received) *) +exception Invalid_choice -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 + (** register a new symbol choice *) +val add_symbol_choice: string -> codomain_item -> unit - (* TODO move to CicSomething *) -val term_of_uri: string -> Cic.term + (** register a new number choice *) +val add_num_choice: codomain_item -> unit + +(** {2 Disambiguation interface} *) -val interpretate: - context: Cic.name option list -> interp: interpretation -> Ast.term -> - Cic.term +exception NoWellTypedInterpretation + +module Make (C : Callbacks) : + sig + val disambiguate_term : + MQIConn.handle -> + Cic.context -> + Cic.metasenv -> + Ast.term -> + aliases:environment -> (* previous interpretation status *) + environment * (* new interpretation status *) + Cic.metasenv * (* new metasenv *) + Cic.term (* disambiguated term *) + end diff --git a/helm/ocaml/cic_disambiguation/disambiguate_struct.ml b/helm/ocaml/cic_disambiguation/disambiguate_struct.ml deleted file mode 100644 index 3e477e154..000000000 --- a/helm/ocaml/cic_disambiguation/disambiguate_struct.ml +++ /dev/null @@ -1,48 +0,0 @@ -(* 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.ml b/helm/ocaml/cic_disambiguation/disambiguate_types.ml new file mode 100644 index 000000000..545099da1 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/disambiguate_types.ml @@ -0,0 +1,47 @@ + +type domain_item = + | Id of string (* literal *) + | Symbol of string * int (* literal, instance num *) + | Num of int (* instance num *) + +module OrderedDomain = + struct + type t = domain_item + let compare = Pervasives.compare + end + +module Domain = Set.Make (OrderedDomain) +module Environment = Map.Make (OrderedDomain) + +type codomain_item = + string * (* description *) + (environment -> string -> Cic.term list -> Cic.term) + (* environment, literal number, arguments as needed *) + +and environment = codomain_item Environment.t + +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 + +let string_of_domain_item = function + | Id s -> Printf.sprintf "ID(%s)" s + | Symbol (s, i) -> Printf.sprintf "SYMBOL(%s,%d)" s i + | Num i -> Printf.sprintf "NUM(instance %d)" i + +let string_of_domain dom = + let buf = Buffer.create 1024 in + Domain.iter + (fun item -> Buffer.add_string buf (string_of_domain_item item ^ "; ")) + dom; + Buffer.contents buf + diff --git a/helm/ocaml/cic_disambiguation/disambiguate_types.mli b/helm/ocaml/cic_disambiguation/disambiguate_types.mli index fc6b0e742..525a7e33f 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate_types.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate_types.mli @@ -23,14 +23,34 @@ * http://helm.cs.unibo.it/ *) -type interpretation_domain_item = +type domain_item = | Id of string (* literal *) | Symbol of string * int (* literal, instance num *) - | Num of string * int (* literal, instance num *) + | Num of int (* instance num *) -and interpretation_codomain_item = +module Domain: Set.S with type elt = domain_item +module Environment: Map.S with type key = domain_item + +type codomain_item = string * (* description *) - (interpretation -> Cic.term list -> Cic.term) + (environment -> string -> Cic.term list -> Cic.term) + (* environment, literal number, arguments as needed *) + +and environment = codomain_item Environment.t + +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 -and interpretation = interpretation_domain_item -> interpretation_codomain_item +val string_of_domain_item: domain_item -> string +val string_of_domain: Domain.t -> string diff --git a/helm/ocaml/cic_disambiguation/lexer.ml b/helm/ocaml/cic_disambiguation/lexer.ml index 10f0667f3..5363d2180 100644 --- a/helm/ocaml/cic_disambiguation/lexer.ml +++ b/helm/ocaml/cic_disambiguation/lexer.ml @@ -25,18 +25,24 @@ exception Error of int * int * string +exception Not_an_extended_ident + let regexp alpha = [ 'a' - 'z' 'A' - 'Z' ] let regexp digit = [ '0' - '9' ] let regexp blank = [ ' ' '\t' '\n' ] let regexp blanks = blank+ let regexp num = digit+ -let regexp ident = alpha (alpha | num)* -let regexp symbol = [^ 'a' - 'z' 'A' - 'Z' '0' - '9' ' ' '\t' '\n' ] let regexp tex_token = '\\' alpha+ +let regexp symbol = [^ 'a' - 'z' 'A' - 'Z' '0' - '9' ' ' '\t' '\n' ] +let regexp ident_cont = alpha | num | '_' +let regexp ident_cont' = ident_cont | tex_token +let regexp ident = (alpha ident_cont*) | ('_' ident_cont+) +let regexp ident' = ((alpha | tex_token) ident_cont'*) | ('_' ident_cont'+) let regexp lparen = [ '(' '[' '{' ] let regexp rparen = [ ')' ']' '}' ] let regexp meta = '?' num +(* let regexp catchall = .* *) let keywords = Hashtbl.create 17 let _ = @@ -50,29 +56,57 @@ let error_at_end lexbuf msg = let return lexbuf token = (token, Ulexing.loc lexbuf) +(* +let parse_ext_ident ident = + let len = String.length ident in + let buf = Buffer.create len in + let in_tex_token = ref false in + let tex_token = Buffer.create 10 in + try + for i = 0 to len - 1 do + match ident.[i] with + | '\' when not !in_tex_token -> + if i < len - 1 && + in_tex_token := true + done + with Invalid_argument -> assert false + +let rec token' = lexer + | ident' -> + (try + let ident = parse_ext_ident (Ulexing.utf8_lexeme lexbuf) in + return lexbuf ("IDENT'", ident) + with Not_an_extended_ident -> + Ulexing.rollback lexbuf; + token lexbuf) + | _ -> + Ulexing.rollback lexbuf; + token lexbuf + +and token = lexer +*) let rec token = lexer -| blanks -> token lexbuf -| ident -> - let lexeme = Ulexing.utf8_lexeme lexbuf in - (try - return lexbuf (Hashtbl.find keywords lexeme) - with Not_found -> - return lexbuf ("IDENT", lexeme)) -| num -> return lexbuf ("INT", Ulexing.utf8_lexeme lexbuf) -| lparen -> return lexbuf ("LPAREN", Ulexing.utf8_lexeme lexbuf) -| rparen -> return lexbuf ("RPAREN", Ulexing.utf8_lexeme lexbuf) -| meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf) -| symbol -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf) -| tex_token -> - let macro = - Ulexing.utf8_sub_lexeme lexbuf 1 (Ulexing.lexeme_length lexbuf - 1) - in - (try - return lexbuf ("SYMBOL", Macro.expand macro) - with Macro.Macro_not_found _ -> - return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)) -| eof -> return lexbuf ("EOI", "") -| _ -> error lexbuf "Invalid character" + | blanks -> token lexbuf + | ident -> + let lexeme = Ulexing.utf8_lexeme lexbuf in + (try + return lexbuf (Hashtbl.find keywords lexeme) + with Not_found -> return lexbuf ("IDENT", lexeme)) + | num -> return lexbuf ("NUM", Ulexing.utf8_lexeme lexbuf) + | lparen -> return lexbuf ("LPAREN", Ulexing.utf8_lexeme lexbuf) + | rparen -> return lexbuf ("RPAREN", Ulexing.utf8_lexeme lexbuf) + | meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf) + | symbol -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf) + | tex_token -> + let macro = + Ulexing.utf8_sub_lexeme lexbuf 1 (Ulexing.lexeme_length lexbuf - 1) + in + (try + return lexbuf ("SYMBOL", Macro.expand macro) + with Macro.Macro_not_found _ -> + return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)) + | eof -> return lexbuf ("EOI", "") + | _ -> error lexbuf "Invalid character" let tok_func stream = let lexbuf = Ulexing.from_utf8_stream stream in diff --git a/helm/ocaml/cic_disambiguation/logic_notation.ml b/helm/ocaml/cic_disambiguation/logic_notation.ml index f23098f96..2f404be83 100644 --- a/helm/ocaml/cic_disambiguation/logic_notation.ml +++ b/helm/ocaml/cic_disambiguation/logic_notation.ml @@ -29,18 +29,34 @@ open Parser EXTEND term: LEVEL "add" [ - [ t1 = term; SYMBOL "∨"; t2 = term -> - return_term loc (Appl_symbol ("or", [t1; t2])) + [ t1 = term; SYMBOL <:unicode> (* ∨ *); t2 = term -> + return_term loc (Appl_symbol ("or", 0, [t1; t2])) ] ]; term: LEVEL "mult" [ - [ t1 = term; SYMBOL "∧"; t2 = term -> - return_term loc (Appl_symbol ("and", [t1; t2])) + [ t1 = term; SYMBOL <:unicode> (* ∧ *); t2 = term -> + return_term loc (Appl_symbol ("and", 0, [t1; t2])) ] ]; term: LEVEL "inv" [ - [ SYMBOL "¬"; t = term -> return_term loc (Appl_symbol ("not", [t])) ] + [ SYMBOL <:unicode> (* ¬ *); t = term -> + return_term loc (Appl_symbol ("not", 0, [t])) ] ]; END + +let _ = + Disambiguate.add_symbol_choice "eq" + ("leibnitz's equality", + (fun interp _ args -> + let t1, t2 = + match args with + | [t1; t2] -> t1, t2 + | _ -> raise Disambiguate.Invalid_choice + in + Cic.Appl [ + Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); + Cic.Implicit; t1; t2 + ])) + diff --git a/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml b/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml index afc9f63af..b1a9153ca 100644 --- a/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml +++ b/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml @@ -24,7 +24,7 @@ *) let debug = false -let debug_print = if debug then prerr_endline else ignore +let debug_print s = if debug then prerr_endline s let loc = (0, 0) diff --git a/helm/ocaml/cic_disambiguation/parser.ml b/helm/ocaml/cic_disambiguation/parser.ml index 13f9fc42d..1621b3ccc 100644 --- a/helm/ocaml/cic_disambiguation/parser.ml +++ b/helm/ocaml/cic_disambiguation/parser.ml @@ -86,13 +86,14 @@ EXTEND ] | "eq" LEFTA [ t1 = term; SYMBOL "="; t2 = term -> - return_term loc (Ast.Appl_symbol ("eq", [t1; t2])) + return_term loc (Ast.Appl_symbol ("eq", 0, [t1; t2])) ] | "add" LEFTA [ (* nothing here by default *) ] | "mult" LEFTA [ (* nothing here by default *) ] | "inv" NONA [ (* nothing here by default *) ] | "simple" NONA [ + (* TODO handle "_" *) b = binder; vars = LIST1 IDENT SEP SYMBOL ","; typ = OPT [ SYMBOL ":"; t = term -> t ]; SYMBOL "."; body = term -> @@ -109,7 +110,8 @@ EXTEND | n = substituted_name -> return_term loc n | LPAREN "("; head = term; args = LIST1 term; RPAREN ")" -> return_term loc (Ast.Appl (head :: args)) - | i = INT -> return_term loc (Ast.Num i) + | i = NUM -> return_term loc (Ast.Num (i, 0)) +(* | i = NUM -> return_term loc (Ast.Num (i, Random.int max_int)) *) | m = META; substs = [ LPAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; RPAREN "]" -> @@ -156,209 +158,3 @@ 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 index 2a70d5091..661d0c36b 100644 --- a/helm/ocaml/cic_disambiguation/parser.mli +++ b/helm/ocaml/cic_disambiguation/parser.mli @@ -36,11 +36,3 @@ 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 c4b04351c..081a7ab19 100644 --- a/helm/ocaml/cic_disambiguation/pp.ml +++ b/helm/ocaml/cic_disambiguation/pp.ml @@ -38,7 +38,7 @@ let rec pp_term = function pp_term term | Appl terms -> sprintf "(%s)" (String.concat " " (List.map pp_term terms)) - | Appl_symbol (symbol, 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) @@ -68,7 +68,7 @@ let rec pp_term = function sprintf "%d[%s]" index (String.concat "; " (List.map (function None -> "_" | Some term -> pp_term term) substs)) - | Num num -> num + | Num (num, _) -> num | Sort `Set -> "Set" | Sort `Prop -> "Prop" | Sort `Type -> "Type" diff --git a/helm/ocaml/cic_disambiguation/test_lexer.ml b/helm/ocaml/cic_disambiguation/test_lexer.ml index bff5cde99..2c4335749 100644 --- a/helm/ocaml/cic_disambiguation/test_lexer.ml +++ b/helm/ocaml/cic_disambiguation/test_lexer.ml @@ -23,7 +23,11 @@ * http://helm.cs.unibo.it/ *) -let ic = open_in Sys.argv.(1) in +let ic = + try + open_in Sys.argv.(1) + with Invalid_argument _ -> stdin +in let token_stream = fst (Lexer.lex.Token.tok_func (Stream.of_channel ic)) in let rec dump () = let (a,b) = Stream.next token_stream in diff --git a/helm/ocaml/cic_disambiguation/test_parser.ml b/helm/ocaml/cic_disambiguation/test_parser.ml index fdab36ef3..0f6b2d162 100644 --- a/helm/ocaml/cic_disambiguation/test_parser.ml +++ b/helm/ocaml/cic_disambiguation/test_parser.ml @@ -24,7 +24,11 @@ *) try - let ic = open_in Sys.argv.(1) in + let ic = + (try + open_in Sys.argv.(1) + with Invalid_argument _ -> stdin) + in let term = Parser.parse_term (Stream.of_channel ic) in close_in ic; print_endline (Pp.pp_term term) diff --git a/helm/ocaml/cic_disambiguation/tests/match.txt b/helm/ocaml/cic_disambiguation/tests/match.txt new file mode 100644 index 000000000..0003a0c23 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/tests/match.txt @@ -0,0 +1,18 @@ +[nat] +match true:bool with +[ true \Rightarrow O +| false \Rightarrow (S O) +] + +[nat] +match O:nat with +[ O \Rightarrow O +| (S x) \Rightarrow (S (S x)) +] + +[nat] +match nil:list with +[ nil \Rightarrow nil +| (cons x y) \Rightarrow (cons x y) +] + -- 2.39.2