X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=4bfc7c4457ba7ea6f9be44469e1811bf071052d9;hb=394bf3a0ca050cf97b1f318363e2e353f67141ad;hp=00b4c4418cf7847d82b8dcee13dfb1c6b00e97d3;hpb=ebc6741574ced219ad51e912b947c96e1d470772;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 00b4c4418..4bfc7c445 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,12 +35,17 @@ 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 Token.flocation * string +let cic_lexer = CicTextualLexer2.cic_lexer ~comments:return_comments () + let fresh_num_instance = let n = ref 0 in if use_fresh_num_instances then @@ -52,7 +57,7 @@ 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" @@ -75,6 +80,10 @@ 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) @@ -120,8 +129,8 @@ 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) ] ]; subst: [ @@ -150,25 +159,70 @@ 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 @@ -235,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 "]" -> @@ -392,7 +447,7 @@ EXTEND tl = OPT [ "with"; types = LIST1 [ name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode>; - OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" -> + OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" -> (name, true, typ, constructors) ] SEP "with" -> types ] -> let params = @@ -406,17 +461,40 @@ EXTEND 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)) @@ -427,6 +505,10 @@ EXTEND 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)) @@ -436,6 +518,8 @@ EXTEND 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) (* @@ -446,7 +530,7 @@ EXTEND ]; script_entry: [ [ cmd = tactical0 -> Command cmd - | s = COMMENT -> Comment (loc, s) +(* | s = COMMENT -> Comment (loc, s) *) ] ]; script: [ [ entries = LIST0 script_entry; EOI -> (loc, entries) ] ]; @@ -480,7 +564,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 =