X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=2d03762aecccd1bcdfa99f6be0170a97cf622070;hb=63ed9d3148199584ae8b238f018e0f9883768ada;hp=088d1b69d690562e4ce74281f3109cccdee259d0;hpb=14724f9aab44f1b150a5509743a43cb6693d493e;p=helm.git diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml index 088d1b69d..2d03762ae 100644 --- a/helm/software/components/content_pres/cicNotationParser.ml +++ b/helm/software/components/content_pres/cicNotationParser.ml @@ -57,11 +57,20 @@ let int_of_string s = (** {2 Grammar extension} *) +let level_of precedence = + if precedence < min_precedence || precedence > max_precedence then + raise (Level_not_found precedence); + string_of_int precedence ^ "N" + let gram_symbol s = Gramext.Stoken ("SYMBOL", s) let gram_ident s = Gramext.Stoken ("IDENT", s) let gram_number s = Gramext.Stoken ("NUMBER", s) let gram_keyword s = Gramext.Stoken ("", s) -let gram_term = Gramext.Sself +let gram_term = function + | None -> Gramext.Sself + | Some (precedence) -> + Gramext.Snterml (Grammar.Entry.obj (term: 'a Grammar.Entry.e),level_of precedence) +;; let gram_of_literal = function @@ -80,10 +89,10 @@ let make_action action bindings = [] -> Gramext.action (fun (loc: Ast.location) -> action vl loc) | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl) (* LUCA: DEFCON 3 BEGIN *) - | Binding (name, Env.TermType) :: tl -> + | Binding (name, Env.TermType l) :: tl -> Gramext.action (fun (v:Ast.term) -> - aux ((name, (Env.TermType, Env.TermValue v))::vl) tl) + aux ((name, (Env.TermType l, Env.TermValue v))::vl) tl) | Binding (name, Env.StringType) :: tl -> Gramext.action (fun (v:string) -> @@ -165,20 +174,6 @@ let extract_term_production pattern = | Ast.List0 (p, _) | Ast.List1 (p, _) -> let p_bindings, p_atoms, p_names, p_action = inner_pattern p in -(* let env0 = List.map list_binding_of_name p_names in - let grow_env_entry env n v = - List.map - (function - | (n', (ty, ListValue vl)) as entry -> - if n' = n then n', (ty, ListValue (v :: vl)) else entry - | _ -> assert false) - env - in - let grow_env env_i env = - List.fold_left - (fun env (n, (_, v)) -> grow_env_entry env n v) - env env_i - in *) let action (env_list : CicNotationEnv.t list) (loc : Ast.location) = CicNotationEnv.coalesce_env p_names env_list in @@ -198,7 +193,8 @@ let extract_term_production pattern = and aux_variable = function | Ast.NumVar s -> [Binding (s, Env.NumType), gram_number ""] - | Ast.TermVar s -> [Binding (s, Env.TermType), gram_term] + | Ast.TermVar (s,level) -> + [Binding (s, Env.TermType level), gram_term level] | Ast.IdentVar s -> [Binding (s, Env.StringType), gram_ident ""] | Ast.Ascription (p, s) -> assert false (* TODO *) | Ast.FreshVar _ -> assert false @@ -213,34 +209,90 @@ let extract_term_production pattern = in aux pattern -let level_of precedence associativity = - if precedence < min_precedence || precedence > max_precedence then - raise (Level_not_found precedence); - let assoc_string = - match associativity with - | Gramext.NonA -> "N" - | Gramext.LeftA -> "L" - | Gramext.RightA -> "R" - in - string_of_int precedence ^ assoc_string - -type rule_id = Token.t Gramext.g_symbol list +type rule_id = Grammar.token Gramext.g_symbol list (* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *) let owned_keywords = Hashtbl.create 23 -let extend level1_pattern ~precedence ~associativity action = +type checked_l1_pattern = CL1P of CicNotationPt.term * int + +let check_l1_pattern level1_pattern level associativity = + let variables = ref 0 in + let symbols = ref 0 in + let rec aux = function + | Ast.AttributedTerm (att, t) -> Ast.AttributedTerm (att,aux t) + | Ast.Literal _ as l -> incr symbols; l + | Ast.Layout l -> Ast.Layout (aux_layout l) + | Ast.Magic m -> Ast.Magic (aux_magic m) + | Ast.Variable v -> Ast.Variable (aux_variable v) + | t -> assert false + and aux_layout = function + | Ast.Sub (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Sub (p1, p2) + | Ast.Sup (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Sup (p1, p2) + | Ast.Below (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Below (p1, p2) + | Ast.Above (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Above (p1, p2) + | Ast.Frac (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Frac (p1, p2) + | Ast.Atop (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Atop (p1, p2) + | Ast.Over (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Over (p1, p2) + | Ast.Root (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Root (p1, p2) + | Ast.Sqrt p -> Ast.Sqrt (aux p) + | Ast.Break as t -> t + | Ast.Box (b, pl) -> Ast.Box(b, List.map aux pl) + | Ast.Group pl -> Ast.Group (List.map aux pl) + and aux_magic magic = + match magic with + | Ast.Opt p -> Ast.Opt (aux p) + | Ast.List0 (p, x) -> Ast.List0 (aux p, x) + | Ast.List1 (p, x) -> Ast.List1 (aux p, x) + | _ -> assert false + and aux_variable = + function + | Ast.NumVar _ as t -> t + | Ast.TermVar (s,None) when associativity <> Gramext.NonA -> + incr variables; + if !variables > 2 then + raise (Parse_error ("Exactly 2 variables must be specified in an "^ + "associative notation")); + (match !variables, associativity with + | 1,Gramext.LeftA -> Ast.TermVar (s, None) (*Ast.TermVar (s, Some + (level-1)) *) + | 1,Gramext.RightA -> Ast.TermVar (s, None) + | 2,Gramext.LeftA ->Ast.TermVar (s, None) + | 2,Gramext.RightA -> Ast.TermVar (s, Some (level-1)) + | _ -> assert false) + | Ast.TermVar (s,Some _) when associativity <> Gramext.NonA -> + raise (Parse_error ("Variables can not be declared with a " ^ + "precedence in an associative notation")) + (* avoid camlp5 divergence due to non-Sself recursion at the same level *) + | Ast.TermVar (s,Some l) when l <= level && !variables=0 && !symbols=0 -> + raise (Parse_error ("Left recursive rule with precedence not greater " ^ + "than " ^ string_of_int level ^ " is not allowed to avoid divergence")) + | Ast.TermVar _ as t -> incr variables; t + | Ast.IdentVar _ as t -> t + | Ast.Ascription _ -> assert false (* TODO *) + | Ast.FreshVar _ -> assert false + in + if associativity <> Gramext.NonA && level = min_precedence then + raise (Parse_error ("You can not specify an associative notation " ^ + "at level "^string_of_int min_precedence ^ "; increase it")); + let cp = CL1P (aux level1_pattern, level) in + if !variables <> 2 && associativity <> Gramext.NonA then + raise (Parse_error ("Exactly 2 variables must be specified in an "^ + "associative notation")); + cp +;; + +let extend (CL1P (level1_pattern,precedence)) action = let p_bindings, p_atoms = List.split (extract_term_production level1_pattern) in - let level = level_of precedence associativity in -(* let p_names = flatten_opt p_bindings in *) + let level = level_of precedence in let _ = Grammar.extend [ Grammar.Entry.obj (term: 'a Grammar.Entry.e), Some (Gramext.Level level), [ None, - Some associativity, + Some (*Gramext.NonA*) Gramext.NonA, [ p_atoms, (make_action (fun (env: CicNotationEnv.t) (loc: Ast.location) -> @@ -300,9 +352,7 @@ let _ = | i when i < first -> acc | i -> aux - ((Some (string_of_int i ^ "N"), Some Gramext.NonA, dummy_prod) - :: (Some (string_of_int i ^ "L"), Some Gramext.LeftA, dummy_prod) - :: (Some (string_of_int i ^ "R"), Some Gramext.RightA, dummy_prod) + ((Some (string_of_int i ^ "N"), Some (*Gramext.NonA*)Gramext.NonA, dummy_prod) :: acc) (i - 1) in @@ -335,7 +385,8 @@ EXTEND ] ]; l1_pattern_variable: [ - [ "term"; id = IDENT -> Ast.TermVar id + [ "term"; precedence = NUMBER; id = IDENT -> + Ast.TermVar (id, Some (int_of_string precedence)) | "number"; id = IDENT -> Ast.NumVar id | "ident"; id = IDENT -> Ast.IdentVar id ] @@ -375,7 +426,7 @@ EXTEND return_term loc (CicNotationUtil.group p) ] | "simple" NONA - [ i = IDENT -> return_term loc (Ast.Variable (Ast.TermVar i)) + [ i = IDENT -> return_term loc (Ast.Variable (Ast.TermVar (i,None))) | m = l1_magic_pattern -> return_term loc (Ast.Magic m) | v = l1_pattern_variable -> return_term loc (Ast.Variable v) | l = literal -> return_term loc (Ast.Literal l) @@ -388,12 +439,13 @@ EXTEND EXTEND GLOBAL: level2_meta; l2_variable: [ - [ "term"; id = IDENT -> Ast.TermVar id + [ "term"; precedence = NUMBER; id = IDENT -> + Ast.TermVar (id,Some (int_of_string precedence)) | "number"; id = IDENT -> Ast.NumVar id | "ident"; id = IDENT -> Ast.IdentVar id | "fresh"; id = IDENT -> Ast.FreshVar id - | "anonymous" -> Ast.TermVar "_" - | id = IDENT -> Ast.TermVar id + | "anonymous" -> Ast.TermVar ("_",None) + | id = IDENT -> Ast.TermVar (id,None) ] ]; l2_magic: [ @@ -427,7 +479,7 @@ EXTEND [ "Prop" -> `Prop | "Set" -> `Set | "Type" -> `Type (CicUniv.fresh ()) - | "CProp" -> `CProp + | "CProp" -> `CProp (CicUniv.fresh ()) ] ]; explicit_subst: [ @@ -452,12 +504,17 @@ EXTEND id, Some typ | arg = single_arg -> arg, None | SYMBOL "_" -> Ast.Ident ("_", None), None + | LPAREN; SYMBOL "_"; SYMBOL ":"; typ = term; RPAREN -> + Ast.Ident ("_", None), Some typ ] ]; match_pattern: [ - [ id = IDENT -> id, None, [] + [ id = IDENT -> Ast.Pattern (id, None, []) | LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN -> - id, None, vars + Ast.Pattern (id, None, vars) + | id = IDENT; vars = LIST1 possibly_typed_name -> + Ast.Pattern (id, None, vars) + | SYMBOL "_" -> Ast.Wildcard ] ]; binder: [ @@ -476,7 +533,7 @@ EXTEND let meta = !parse_level2_meta_ref (Ulexing.from_utf8_string blob) in match meta with | Ast.Variable (Ast.FreshVar _) -> [meta], None - | Ast.Variable (Ast.TermVar "_") -> [Ast.Ident ("_", None)], None + | Ast.Variable (Ast.TermVar ("_",_)) -> [Ast.Ident ("_", None)], None | _ -> failwith "Invalid bound name." ] ]; @@ -487,15 +544,10 @@ EXTEND match meta with | Ast.Variable (Ast.FreshVar _) | Ast.Variable (Ast.IdentVar _) -> meta - | Ast.Variable (Ast.TermVar "_") -> Ast.Ident ("_", None) + | Ast.Variable (Ast.TermVar ("_",_)) -> Ast.Ident ("_", None) | _ -> failwith "Invalid index name." ] ]; - induction_kind: [ - [ "rec" -> `Inductive - | "corec" -> `CoInductive - ] - ]; let_defs: [ [ defs = LIST1 [ name = single_arg; @@ -549,27 +601,31 @@ EXTEND | vars = protected_binder_vars -> vars ] ]; - term: LEVEL "10N" [ (* let in *) + term: LEVEL "10N" + [ [ "let"; var = possibly_typed_name; SYMBOL <:unicode> (* ≝ *); p1 = term; "in"; p2 = term -> return_term loc (Ast.LetIn (var, p1, p2)) - | "let"; k = induction_kind; defs = let_defs; "in"; + | LETCOREC; defs = let_defs; "in"; + body = term -> + return_term loc (Ast.LetRec (`CoInductive, defs, body)) + | LETREC; defs = let_defs; "in"; body = term -> - return_term loc (Ast.LetRec (k, defs, body)) + return_term loc (Ast.LetRec (`Inductive, defs, body)) ] ]; - term: LEVEL "20R" (* binder *) + term: LEVEL "20N" [ - [ b = binder; (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term -> + [ b = binder; (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19N" -> return_term loc (fold_cluster b vars typ body) | SYMBOL <:unicode> (* ∃ *); - (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term -> + (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19N"-> return_term loc (fold_exists vars typ body) ] ]; - term: LEVEL "70L" (* apply *) + term: LEVEL "70N" [ - [ p1 = term; p2 = term -> + [ p1 = term; p2 = term LEVEL "71N" -> let rec aux = function | Ast.Appl (hd :: tl) | Ast.AttributedTerm (_, Ast.Appl (hd :: tl)) -> @@ -579,7 +635,7 @@ EXTEND return_term loc (Ast.Appl (aux p1 @ [p2])) ] ]; - term: LEVEL "90N" (* simple *) + term: LEVEL "90N" [ [ id = IDENT -> return_term loc (Ast.Ident (id, None)) | id = IDENT; s = explicit_subst ->