X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=d5f427c4f92f039367f722eceb4abf3bb0ce6b68;hb=0aaed6f96b856d1181a3cd1f2ef3ea4a91990771;hp=634e8e291bcd2f38871290ac657f180588fd5e89;hpb=d645b8bf30064e94ee9777d793854eebc921dfe0;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 634e8e291..d5f427c4f 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -23,7 +23,7 @@ * http://helm.cs.unibo.it/ *) -let debug = true +let debug = false let debug_print s = if debug then begin prerr_endline ""; @@ -35,10 +35,16 @@ let debug_print s = * thus be interpreted differently than others *) let use_fresh_num_instances = false + (** does the lexer return COMMENT tokens? *) +let return_comments = false + open Printf + open DisambiguateTypes -exception Parse_error of string +exception Parse_error of Token.flocation * string + +let cic_lexer = CicTextualLexer2.cic_lexer ~comments:return_comments () let fresh_num_instance = let n = ref 0 in @@ -47,11 +53,11 @@ let fresh_num_instance = else (fun () -> 0) -let choice_of_uri (uri: string) = - let cic = HelmLibraryObjects.term_of_uri (UriManager.uri_of_string uri) in - (uri, (fun _ _ _ -> cic)) +let choice_of_uri uri = + let term = CicUtil.term_of_uri uri in + (uri, (fun _ _ _ -> term)) -let grammar = Grammar.gcreate CicTextualLexer2.cic_lexer +let grammar = Grammar.gcreate cic_lexer let term = Grammar.Entry.create grammar "term" let term0 = Grammar.Entry.create grammar "term0" @@ -59,11 +65,12 @@ let tactic = Grammar.Entry.create grammar "tactic" let tactical = Grammar.Entry.create grammar "tactical" let tactical0 = Grammar.Entry.create grammar "tactical0" let command = Grammar.Entry.create grammar "command" +let script = Grammar.Entry.create grammar "script" let return_term loc term = CicAst.AttributedTerm (`Loc loc, term) let return_tactic loc tactic = TacticAst.LocatedTactic (loc, tactic) let return_tactical loc tactical = TacticAst.LocatedTactical (loc, tactical) -let return_command loc cmd = cmd +let return_command loc cmd = cmd (* TODO ZACK FIXME uhm ... why we drop loc? *) let fail floc msg = let (x, y) = CicAst.loc_of_floc floc in @@ -73,20 +80,35 @@ let name_of_string = function | "_" -> Cic.Anonymous | s -> Cic.Name s +let string_of_name = function + | Cic.Anonymous -> "_" + | Cic.Name s -> s + let int_opt = function | None -> None | Some lexeme -> Some (int_of_string lexeme) + (** the uri of an inductive type (a ".ind" uri) is not meaningful without an + * xpointer. Still, it's likely that an user who wrote "cic:/blabla/foo.ind" + * actually meant "cic:/blabla/foo.ind#xpointer(1/1)", i.e. the first inductive + * type in a block of mutual inductive types. + * + * This function performs the expansion foo.ind -> foo#xpointer..., if needed + *) +let ind_expansion uri = + let len = String.length uri in + if len >= 4 && String.sub uri (len - 4) 4 = ".ind" then + uri ^ "#xpointer(1/1)" + else + uri + EXTEND - GLOBAL: term term0 tactic tactical tactical0 command; + GLOBAL: term term0 tactic tactical tactical0 command script; int: [ [ num = NUM -> try int_of_string num - with Failure _ -> - let (x, y) = CicAst.loc_of_floc loc in - raise (Parse_error (sprintf - "integer literal expected at characters %d-%d" x y)) + with Failure _ -> raise (Parse_error (loc, "integer literal expected")) ] ]; meta_subst: [ @@ -107,13 +129,12 @@ EXTEND ]; typed_name: [ [ PAREN "("; i = IDENT; SYMBOL ":"; typ = term; PAREN ")" -> - (name_of_string i, Some typ) - | i = IDENT -> (name_of_string i, None) + (Cic.Name i, Some typ) + | i = IDENT -> (Cic.Name i, None) ] ]; - substituted_name: [ (* a subs.name is an explicit substitution subject *) - [ s = IDENT; - subst = OPT [ + subst: [ + [ subst = OPT [ SYMBOL "\\subst"; (* to avoid catching frequent "a [1]" cases *) PAREN "["; substs = LIST1 [ @@ -121,8 +142,12 @@ EXTEND ] SEP SYMBOL ";"; PAREN "]" -> substs - ] -> - CicAst.Ident (s, subst) + ] -> subst + ] + ]; + substituted_name: [ (* a subs.name is an explicit substitution subject *) + [ s = IDENT; subst = subst -> CicAst.Ident (s, subst) + | s = URI; subst = subst -> CicAst.Uri (ind_expansion s, subst) ] ]; name: [ (* as substituted_name with no explicit substitution *) @@ -134,36 +159,82 @@ EXTEND (head, vars) ] ]; + let_defs:[ + [ defs = LIST1 [ + name = IDENT; + args = LIST1 [ + PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":"; + ty = term; PAREN ")" -> + (names, ty) + ]; + index_name = OPT [ IDENT "on"; idx = IDENT -> idx ]; + ty = OPT [ SYMBOL ":" ; t = term -> t ]; + SYMBOL <:unicode> (* ≝ *); + t1 = term -> + let rec list_of_binder binder ty final_term = function + | [] -> final_term + | name::tl -> + CicAst.Binder (binder, (Cic.Name name, Some ty), + list_of_binder binder ty final_term tl) + in + let rec binder_of_arg_list binder final_term = function + | [] -> final_term + | (l,ty)::tl -> + list_of_binder binder ty + (binder_of_arg_list binder final_term tl) l + in + let t1' = binder_of_arg_list `Lambda t1 args in + let ty' = + match ty with + | None -> None + | Some ty -> Some (binder_of_arg_list `Pi ty args) + in + let rec get_position_of name n = function + | [] -> (None,n) + | nam::tl -> + if nam = name then + (Some n,n) + else + (get_position_of name (n+1) tl) + in + let rec find_arg name n = function + | [] -> (fail loc (sprintf "Argument %s not found" name)) + | (l,_)::tl -> + let (got,len) = get_position_of name 0 l in + (match got with + | None -> (find_arg name (n+len) tl) + | Some where -> n + where) + in + let index = + (match index_name with + | None -> 0 + | (Some name) -> find_arg name 0 args) + in + ((Cic.Name name,ty'), t1', index) + ] SEP "and" -> defs + ]]; + constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ]; term0: [ [ t = term; EOI -> return_term loc t ] ]; term: [ "letin" NONA [ "let"; var = typed_name; - SYMBOL "="; (* SYMBOL <:unicode> (* ≝ *); *) + SYMBOL <:unicode> (* ≝ *); t1 = term; "in"; t2 = term -> return_term loc (CicAst.LetIn (var, t1, t2)) | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; - defs = LIST1 [ - var = typed_name; - index = OPT [ PAREN "("; index = NUM; PAREN ")" -> - int_of_string index - ]; - SYMBOL "="; (* SYMBOL <:unicode> (* ≝ *); *) - t1 = term -> - (var, t1, (match index with None -> 0 | Some i -> i)) - ] SEP "and"; - "in"; body = term -> + defs = let_defs; "in"; body = term -> return_term loc (CicAst.LetRec (ind_kind, defs, body)) ] | "binder" RIGHTA [ b = binder; (vars, typ) = - [ vars = LIST1 IDENT; + [ vars = LIST1 IDENT SEP SYMBOL ","; typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ) - | PAREN "("; vars = LIST1 IDENT; + | PAREN "("; vars = LIST1 IDENT SEP SYMBOL ","; typ = OPT [ SYMBOL ":"; t = term -> t ]; PAREN ")" -> (vars, typ) ]; - SYMBOL ","; body = term -> + SYMBOL "."; body = term -> let binder = List.fold_right (fun var body -> @@ -218,7 +289,8 @@ EXTEND "with"; PAREN "["; patterns = LIST0 [ - lhs = pattern; SYMBOL <:unicode> (* ⇒ *); rhs = term -> + lhs = pattern; SYMBOL <:unicode> (* ⇒ *); rhs = term + -> ((lhs: CicAst.case_pattern), rhs) ] SEP SYMBOL "|"; PAREN "]" -> @@ -240,9 +312,9 @@ EXTEND [ PAREN "["; idents = LIST1 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ] ]; reduction_kind: [ - [ "reduce" -> `Reduce - | "simpl" -> `Simpl - | "whd" -> `Whd ] + [ [ IDENT "reduce" | IDENT "Reduce" ] -> `Reduce + | [ IDENT "simplify" | IDENT "Simplify" ] -> `Simpl + | [ IDENT "whd" | IDENT "Whd" ] -> `Whd ] ]; tactic: [ [ [ IDENT "absurd" | IDENT "Absurd" ]; t = tactic_term -> @@ -251,6 +323,7 @@ EXTEND return_tactic loc (TacticAst.Apply t) | [ IDENT "assumption" | IDENT "Assumption" ] -> return_tactic loc TacticAst.Assumption + | [ IDENT "auto" | IDENT "Auto" ] -> return_tactic loc TacticAst.Auto | [ IDENT "change" | IDENT "Change" ]; t1 = tactic_term; "with"; t2 = tactic_term; where = tactic_where -> @@ -281,6 +354,7 @@ EXTEND return_tactic loc (TacticAst.Fold (kind, t)) | [ IDENT "fourier" | IDENT "Fourier" ] -> return_tactic loc TacticAst.Fourier + | [ IDENT "hint" | IDENT "Hint" ] -> return_tactic loc TacticAst.Hint | [ IDENT "injection" | IDENT "Injection" ]; ident = IDENT -> return_tactic loc (TacticAst.Injection ident) | [ IDENT "intros" | IDENT "Intros" ]; @@ -289,12 +363,25 @@ EXTEND let idents = match idents with None -> [] | Some idents -> idents in return_tactic loc (TacticAst.Intros (num, idents)) | [ IDENT "intro" | IDENT "Intro" ] -> - return_tactic loc (TacticAst.Intros (Some 1, [])) + return_tactic loc (TacticAst.Intros (None, [])) | [ IDENT "left" | IDENT "Left" ] -> return_tactic loc TacticAst.Left | [ "let" | "Let" ]; t = tactic_term; "in"; where = IDENT -> return_tactic loc (TacticAst.LetIn (t, where)) - (* TODO Reduce *) + | kind = reduction_kind; + pat = OPT [ + "in"; pat = [ IDENT "goal" -> `Goal | IDENT "hyp" -> `Everywhere ] -> + pat + ]; + terms = LIST0 term SEP SYMBOL "," -> + let tac = + (match (pat, terms) with + | None, [] -> TacticAst.Reduce (kind, None) + | None, terms -> TacticAst.Reduce (kind, Some (terms, `Goal)) + | Some pat, [] -> TacticAst.Reduce (kind, Some ([], pat)) + | Some pat, terms -> TacticAst.Reduce (kind, Some (terms, pat))) + in + return_tactic loc tac | [ IDENT "reflexivity" | IDENT "Reflexivity" ] -> return_tactic loc TacticAst.Reflexivity | [ IDENT "replace" | IDENT "Replace" ]; @@ -312,13 +399,15 @@ EXTEND return_tactic loc (TacticAst.Transitivity t) ] ]; - tactical0: [ [ t = tactical; SYMBOL "." -> t ] ]; + tactical0: [ [ t = tactical; SYMBOL "." -> return_tactical loc t ] ]; tactical: [ "command" NONA [ cmd = command -> return_tactical loc (TacticAst.Command cmd) ] | "sequence" LEFTA [ tactics = LIST1 NEXT SEP SYMBOL ";" -> - return_tactical loc (TacticAst.Seq tactics) + (match tactics with + | [tactic] -> tactic + | _ -> return_tactical loc (TacticAst.Seq tactics)) ] | "then" NONA [ tac = tactical; @@ -351,17 +440,77 @@ EXTEND | [ IDENT "theorem" | IDENT "Theorem" ] -> `Theorem ] ]; + inductive_spec: [ [ + fst_name = IDENT; params = LIST0 [ + PAREN "("; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":"; + typ = term; PAREN ")" -> (names, typ) ]; + SYMBOL ":"; fst_typ = term; SYMBOL <:unicode>; OPT SYMBOL "|"; + fst_constructors = LIST0 constructor SEP SYMBOL "|"; + tl = OPT [ "with"; + types = LIST1 [ + name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode>; + OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" -> + (name, true, typ, constructors) ] SEP "with" -> types + ] -> + let params = + List.fold_right + (fun (names, typ) acc -> + (List.map (fun name -> (name, typ)) names) @ acc) + params [] + in + let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in + let tl_ind_types = match tl with None -> [] | Some types -> types in + let ind_types = fst_ind_type :: tl_ind_types in + (params, ind_types) + ] ]; + print_kind: [ + [ [ IDENT "Env" | IDENT "env" | IDENT "Environment" | IDENT "environment" ] + -> `Env + | [ IDENT "Coer" | IDENT "coer" | IDENT "Coercions" | IDENT "coercions" ] + -> `Coer + ] ]; + command: [ [ [ IDENT "abort" | IDENT "Abort" ] -> return_command loc TacticAst.Abort | [ IDENT "proof" | IDENT "Proof" ] -> return_command loc TacticAst.Proof | [ IDENT "quit" | IDENT "Quit" ] -> return_command loc TacticAst.Quit | [ IDENT "qed" | IDENT "Qed" ] -> return_command loc (TacticAst.Qed None) + | [ IDENT "print" | IDENT "Print" ]; + print_kind = print_kind -> + return_command loc (TacticAst.Print print_kind) | [ IDENT "save" | IDENT "Save" ]; name = IDENT -> return_command loc (TacticAst.Qed (Some name)) | flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> return_command loc (TacticAst.Theorem (flavour, name, typ, body)) + | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; + defs = let_defs -> + let name,ty = + match defs with + | ((Cic.Name name,Some ty),_,_) :: _ -> name,ty + | ((Cic.Name name,None),_,_) :: _ -> + fail loc ("No type given for " ^ name) + | _ -> assert false + in + let body = CicAst.Ident (name,None) in + TacticAst.Theorem(`Definition, Some name, ty, + Some (CicAst.LetRec (ind_kind, defs, body))) + + | [ IDENT "inductive" | IDENT "Inductive" ]; spec = inductive_spec -> + let (params, ind_types) = spec in + return_command loc (TacticAst.Inductive (params, ind_types)) + | [ IDENT "coinductive" | IDENT "CoInductive" ]; spec = inductive_spec -> + let (params, ind_types) = spec in + let ind_types = (* set inductive flags to false (coinductive) *) + List.map (fun (name, _, term, ctors) -> (name, false, term, ctors)) + ind_types + in + return_command loc (TacticAst.Inductive (params, ind_types)) + | [ IDENT "coercion" | IDENT "Coercion" ] ; name = IDENT -> + return_command loc (TacticAst.Coercion (CicAst.Ident (name,Some []))) + | [ IDENT "coercion" | IDENT "Coercion" ] ; name = URI -> + return_command loc (TacticAst.Coercion (CicAst.Uri (name,Some []))) | [ IDENT "goal" | IDENT "Goal" ]; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> return_command loc (TacticAst.Theorem (`Goal, None, typ, body)) @@ -369,26 +518,43 @@ EXTEND return_command loc (TacticAst.Undo (int_opt steps)) | [ IDENT "redo" | IDENT "Redo" ]; steps = OPT NUM -> return_command loc (TacticAst.Redo (int_opt steps)) + | [ IDENT "baseuri" | IDENT "Baseuri" ]; uri = OPT QSTRING -> + return_command loc (TacticAst.Baseuri uri) + | [ IDENT "basedir" | IDENT "Basedir" ]; uri = OPT QSTRING -> + return_command loc (TacticAst.Basedir uri) | [ IDENT "check" | IDENT "Check" ]; t = term -> return_command loc (TacticAst.Check t) +(* + | [ IDENT "alias" | IDENT "Alias" ]; spec = alias_spec -> + return_command loc (TacticAst.Alias spec) +*) ] ]; + script_entry: [ + [ cmd = tactical0 -> Command cmd +(* | s = COMMENT -> Comment (loc, s) *) + ] + ]; + script: [ [ entries = LIST0 script_entry; EOI -> (loc, entries) ] ]; END let exc_located_wrapper f = try - Lazy.force f - with Stdpp.Exc_located (floc, exn) -> - let (x, y) = CicAst.loc_of_floc floc in - raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y - (Printexc.to_string exn))) + f () + with + | Stdpp.Exc_located (floc, Stream.Error msg) -> + raise (Parse_error (floc, msg)) + | Stdpp.Exc_located (floc, exn) -> + raise (Parse_error (floc, (Printexc.to_string exn))) let parse_term stream = - exc_located_wrapper (lazy (Grammar.Entry.parse term0 stream)) + exc_located_wrapper (fun () -> (Grammar.Entry.parse term0 stream)) let parse_tactic stream = - exc_located_wrapper (lazy (Grammar.Entry.parse tactic stream)) + exc_located_wrapper (fun () -> (Grammar.Entry.parse tactic stream)) let parse_tactical stream = - exc_located_wrapper (lazy (Grammar.Entry.parse tactical0 stream)) + exc_located_wrapper (fun () -> (Grammar.Entry.parse tactical0 stream)) +let parse_script stream = + exc_located_wrapper (fun () -> (Grammar.Entry.parse script stream)) (**/**) @@ -400,7 +566,7 @@ module EnvironmentP3 = let empty = "" - let aliases_grammar = Grammar.gcreate CicTextualLexer2.cic_lexer + let aliases_grammar = Grammar.gcreate cic_lexer let aliases = Grammar.Entry.create aliases_grammar "aliases" let to_string env = @@ -454,12 +620,8 @@ module EnvironmentP3 = if s = empty then Environment.empty else - try - Grammar.Entry.parse aliases (Stream.of_string s) - with Stdpp.Exc_located (floc, exn) -> - let (x, y) = CicAst.loc_of_floc floc in - raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y - (Printexc.to_string exn))) + exc_located_wrapper + (fun () -> Grammar.Entry.parse aliases (Stream.of_string s)) end (* vim:set encoding=utf8: *)