From: Stefano Zacchiroli Date: Mon, 18 Jul 2005 12:16:21 +0000 (+0000) Subject: merged cic_notation with disambiguation: good luck! X-Git-Tag: V_0_7_2~201 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e20f3963028a966fc93ba0d611c4aa8341d20e2c;p=helm.git merged cic_notation with disambiguation: good luck! --- diff --git a/helm/ocaml/cic_disambiguation/.depend b/helm/ocaml/cic_disambiguation/.depend index e70fbb34f..c83a3c6ae 100644 --- a/helm/ocaml/cic_disambiguation/.depend +++ b/helm/ocaml/cic_disambiguation/.depend @@ -1,23 +1,15 @@ +disambiguatePp.cmi: disambiguateTypes.cmi disambiguateChoices.cmi: disambiguateTypes.cmi -cicTextualParser2.cmi: disambiguateTypes.cmi disambiguate.cmi: disambiguateTypes.cmi disambiguateTypes.cmo: disambiguateTypes.cmi disambiguateTypes.cmx: disambiguateTypes.cmi +disambiguatePp.cmo: disambiguateTypes.cmi disambiguatePp.cmi +disambiguatePp.cmx: disambiguateTypes.cmx disambiguatePp.cmi disambiguateChoices.cmo: disambiguateTypes.cmi disambiguateChoices.cmi disambiguateChoices.cmx: disambiguateTypes.cmx disambiguateChoices.cmi -cicTextualLexer2.cmo: cicTextualLexer2.cmi -cicTextualLexer2.cmx: cicTextualLexer2.cmi -cicTextualParser2.cmo: disambiguateTypes.cmi disambiguateChoices.cmi \ - cicTextualLexer2.cmi cicTextualParser2.cmi -cicTextualParser2.cmx: disambiguateTypes.cmx disambiguateChoices.cmx \ - cicTextualLexer2.cmx cicTextualParser2.cmi disambiguate.cmo: disambiguateTypes.cmi disambiguateChoices.cmi \ - cicTextualParser2.cmi disambiguate.cmi + disambiguate.cmi disambiguate.cmx: disambiguateTypes.cmx disambiguateChoices.cmx \ - cicTextualParser2.cmx disambiguate.cmi -logic_notation.cmo: disambiguateChoices.cmi cicTextualParser2.cmi -logic_notation.cmx: disambiguateChoices.cmx cicTextualParser2.cmx -arit_notation.cmo: disambiguateChoices.cmi cicTextualParser2.cmi -arit_notation.cmx: disambiguateChoices.cmx cicTextualParser2.cmx -tex_notation.cmo: cicTextualParser2.cmi -tex_notation.cmx: cicTextualParser2.cmx + disambiguate.cmi +arit_notation.cmo: disambiguateTypes.cmi disambiguateChoices.cmi +arit_notation.cmx: disambiguateTypes.cmx disambiguateChoices.cmx diff --git a/helm/ocaml/cic_disambiguation/Makefile b/helm/ocaml/cic_disambiguation/Makefile index 94ea279bd..b995f537d 100644 --- a/helm/ocaml/cic_disambiguation/Makefile +++ b/helm/ocaml/cic_disambiguation/Makefile @@ -1,43 +1,20 @@ PACKAGE = cic_textual_parser2 REQUIRES = \ - helm-tactics helm-logger helm-cic_unification helm-cic_transformations \ + helm-tactics helm-logger helm-cic_unification helm-cic_notation \ helm-utf8_macros \ ulex -NOTATIONS = logic arit tex -# NOTATIONS = logic arit -INTERFACE_FILES = \ - disambiguateTypes.mli \ - disambiguateChoices.mli \ - cicTextualLexer2.mli \ - cicTextualParser2.mli \ +NOTATIONS = arit +INTERFACE_FILES = \ + disambiguateTypes.mli \ + disambiguatePp.mli \ + disambiguateChoices.mli \ disambiguate.mli IMPLEMENTATION_FILES = \ $(patsubst %.mli, %.ml, $(INTERFACE_FILES)) \ $(patsubst %,%_notation.ml,$(NOTATIONS)) -all: test_lexer test_parser - -cicTextualLexer2.cmo: cicTextualLexer2.ml - $(OCAMLC_P4) -c $< -cicTextualParser2.cmo: cicTextualParser2.ml - $(OCAMLC_P4) -c $< -cicTextualLexer2.cmx: cicTextualLexer2.ml - $(OCAMLOPT_P4) -c $< -cicTextualParser2.cmx: cicTextualParser2.ml - $(OCAMLOPT_P4) -c $< - -%_notation.cmo: %_notation.ml - $(OCAMLC_P4) -c $< -%_notation.cmx: %_notation.ml - $(OCAMLOPT_P4) -c $< - -LOCAL_LINKOPTS = -package helm-cic_textual_parser2 -linkpkg -test: test_lexer test_parser -test_lexer: test_lexer.ml $(PACKAGE).cma - $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< -test_parser: test_parser.ml $(PACKAGE).cma - $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< +all: clean: extra_clean distclean: extra_clean diff --git a/helm/ocaml/cic_disambiguation/arit_notation.ml b/helm/ocaml/cic_disambiguation/arit_notation.ml index 780fed363..7ce0ec0a0 100644 --- a/helm/ocaml/cic_disambiguation/arit_notation.ml +++ b/helm/ocaml/cic_disambiguation/arit_notation.ml @@ -23,53 +23,6 @@ * http://helm.cs.unibo.it/ *) -open CicTextualParser2 - -EXTEND - term: LEVEL "add" - [ - [ t1 = term; SYMBOL "+"; t2 = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("plus", 0); t1; t2]) - | t1 = term; SYMBOL "-"; t2 = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("minus", 0); t1; t2]) - ] - ]; - term: LEVEL "mult" - [ - [ t1 = term; SYMBOL "*"; t2 = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("times", 0); t1; t2]) - | t1 = term; SYMBOL "/"; t2 = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("divide", 0); t1; t2]) - ] - ]; - term: LEVEL "power" - [ - [ t1 = term; SYMBOL "^"; t2 = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("power", 0); t1; t2]) - ] - ]; - term: LEVEL "inv" - [ - [ SYMBOL "-"; t = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("uminus", 0); t]) - ] - ]; - term: LEVEL "relop" - [ - [ t1 = term; SYMBOL <:unicode> (* ≤ *); t2 = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("leq", 0); t1; t2]) - | t1 = term; SYMBOL <:unicode> (* ≥ *); t2 = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("geq", 0); t1; t2]) - | t1 = term; SYMBOL "<"; t2 = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("lt", 0); t1; t2]) - | t1 = term; SYMBOL ">"; t2 = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("gt", 0); t1; t2]) - | t1 = term; SYMBOL <:unicode> (* ≠ *); t2 = term -> - return_term loc (CicAst.Appl [CicAst.Symbol ("neq", 0); t1; t2]) - ] - ]; -END - let _ = let const s = Cic.Const (s, []) in let mutind s = Cic.MutInd (s, 0, []) in @@ -85,7 +38,7 @@ let _ = (fun _ num _ -> let num = int_of_string num in if num = 0 then - raise DisambiguateChoices.Invalid_choice + raise DisambiguateTypes.Invalid_choice else HelmLibraryObjects.build_bin_pos num)); DisambiguateChoices.add_num_choice @@ -99,72 +52,5 @@ let _ = HelmLibraryObjects.BinInt.zpos; HelmLibraryObjects.build_bin_pos num ] else - assert false)); - - DisambiguateChoices.add_binary_op "plus" "natural plus" - HelmLibraryObjects.Peano.plus; - DisambiguateChoices.add_binary_op "plus" "real plus" - HelmLibraryObjects.Reals.rplus; - DisambiguateChoices.add_binary_op "plus" "binary integer plus" - HelmLibraryObjects.BinInt.zplus; - DisambiguateChoices.add_binary_op "plus" "binary positive plus" - HelmLibraryObjects.BinPos.pplus; - DisambiguateChoices.add_binary_op "minus" "natural minus" - (const HelmLibraryObjects.Peano.minus_URI); - DisambiguateChoices.add_binary_op "minus" "real minus" - (const HelmLibraryObjects.Reals.rminus_URI); - DisambiguateChoices.add_binary_op "minus" "binary integer minus" - HelmLibraryObjects.BinInt.zminus; - DisambiguateChoices.add_binary_op "minus" "binary positive minus" - HelmLibraryObjects.BinPos.pminus; - DisambiguateChoices.add_binary_op "times" "natural times" - (const HelmLibraryObjects.Peano.mult_URI); - DisambiguateChoices.add_binary_op "times" "real times" - (const HelmLibraryObjects.Reals.rmult_URI); - DisambiguateChoices.add_binary_op "times" "binary positive times" - HelmLibraryObjects.BinPos.pmult; - DisambiguateChoices.add_binary_op "times" "binary integer times" - HelmLibraryObjects.BinInt.zmult; - DisambiguateChoices.add_binary_op "power" "real power" - (const HelmLibraryObjects.Reals.pow_URI); - DisambiguateChoices.add_binary_op "power" "integer power" - (const HelmLibraryObjects.BinInt.zpower_URI); - DisambiguateChoices.add_binary_op "divide" "real divide" - (const HelmLibraryObjects.Reals.rdiv_URI); - DisambiguateChoices.add_unary_op "uminus" "real unary minus" - (const HelmLibraryObjects.Reals.ropp_URI); - DisambiguateChoices.add_unary_op "uminus" "binary integer negative sign" - (HelmLibraryObjects.BinInt.zneg); - DisambiguateChoices.add_unary_op "uminus" "binary integer unary minus" - (HelmLibraryObjects.BinInt.zopp); - - DisambiguateChoices.add_binary_op "leq" "natural 'less or equal to'" - (mutind HelmLibraryObjects.Peano.le_URI); - DisambiguateChoices.add_binary_op "leq" "real 'less or equal to'" - (const HelmLibraryObjects.Reals.rle_URI); - DisambiguateChoices.add_binary_op "geq" "natural 'greater or equal to'" - (const HelmLibraryObjects.Peano.ge_URI); - DisambiguateChoices.add_binary_op "geq" "real 'greater or equal to'" - (const HelmLibraryObjects.Reals.rge_URI); - DisambiguateChoices.add_binary_op "lt" "natural 'less than'" - (const HelmLibraryObjects.Peano.lt_URI); - DisambiguateChoices.add_binary_op "lt" "real 'less than'" - (const HelmLibraryObjects.Reals.rlt_URI); - DisambiguateChoices.add_binary_op "gt" "natural 'greater than'" - (const HelmLibraryObjects.Peano.gt_URI); - DisambiguateChoices.add_binary_op "gt" "real 'greater than'" - (const HelmLibraryObjects.Reals.rgt_URI); - DisambiguateChoices.add_symbol_choice "neq" - ("not equal to (leibnitz)", - (fun env _ args -> - let t1, t2 = - match args with - | [t1; t2] -> t1, t2 - | _ -> raise DisambiguateChoices.Invalid_choice - in - Cic.Appl [ const HelmLibraryObjects.Logic.not_URI; - Cic.Appl [ - Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); - Cic.Implicit (Some `Type); t1; t2 ] ])); + assert false)) -(* vim:set encoding=utf8: *) diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 6848338c3..026f9ebd1 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -47,6 +47,16 @@ let domain_size = ref 0 let choices_avg = ref 0. *) +let floc_of_loc (loc_begin, loc_end) = + let floc_begin = + { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1; + Lexing.pos_cnum = loc_begin } + in + let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in + (floc_begin, floc_end) + +let dummy_floc = floc_of_loc (-1, -1) + let descr_of_domain_item = function | Id s -> s | Symbol (s, _) -> s @@ -100,7 +110,7 @@ let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () = (DisambiguateTypes.string_of_domain_item item)) (* TODO move it to Cic *) -let find_in_environment name context = +let find_in_environment name (context: Cic.name list) = let rec aux acc = function | [] -> raise Not_found | Cic.Name hd :: tl when hd = name -> acc @@ -108,39 +118,42 @@ let find_in_environment name context = in aux 1 context -let interpretate_term ~context ~env ~uri ~is_path ast = +let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = assert (uri = None); - let rec aux loc context = function - | CicAst.AttributedTerm (`Loc loc, term) -> + let rec aux loc (context: Cic.name list) = function + | CicNotationPt.AttributedTerm (`Loc loc, term) -> aux loc context term - | CicAst.AttributedTerm (_, term) -> aux loc context term - | CicAst.Appl (CicAst.Symbol (symb, i) :: args) -> + | CicNotationPt.AttributedTerm (_, term) -> aux loc context term + | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) -> let cic_args = List.map (aux loc context) args in resolve env (Symbol (symb, i)) ~args:cic_args () - | CicAst.Appl terms -> Cic.Appl (List.map (aux loc context) terms) - | CicAst.Binder (binder_kind, (var, typ), body) -> + | CicNotationPt.Appl terms -> Cic.Appl (List.map (aux loc context) terms) + | CicNotationPt.Binder (binder_kind, (var, typ), body) -> let cic_type = aux_option loc context (Some `Type) typ in - let cic_body = aux loc (var :: context) body in + let cic_name = CicNotationUtil.cic_name_of_name var in + let cic_body = aux loc (cic_name :: context) body in (match binder_kind with - | `Lambda -> Cic.Lambda (var, cic_type, cic_body) - | `Pi | `Forall -> Cic.Prod (var, cic_type, cic_body) + | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body) + | `Pi + | `Forall -> Cic.Prod (cic_name, cic_type, cic_body) | `Exists -> resolve env (Symbol ("exists", 0)) - ~args:[ cic_type; Cic.Lambda (var, cic_type, cic_body) ] ()) - | CicAst.Case (term, indty_ident, outtype, branches) -> + ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ()) + | CicNotationPt.Case (term, indty_ident, outtype, branches) -> let cic_term = aux loc context term in let cic_outtype = aux_option loc context None outtype in let do_branch ((head, args), term) = let rec do_branch' context = function | [] -> aux loc context term | (name, typ) :: tl -> - let cic_body = do_branch' (name :: context) tl in + let cic_name = CicNotationUtil.cic_name_of_name name in + let cic_body = do_branch' (cic_name :: context) tl in let typ = match typ with | None -> Cic.Implicit (Some `Type) | Some typ -> aux loc context typ in - Cic.Lambda (name, typ, cic_body) + Cic.Lambda (cic_name, typ, cic_body) in do_branch' context args in @@ -150,33 +163,40 @@ let interpretate_term ~context ~env ~uri ~is_path ast = (match resolve env (Id indty_ident) () with | Cic.MutInd (uri, tyno, _) -> (uri, tyno) | Cic.Implicit _ -> raise Try_again - | _ -> raise DisambiguateChoices.Invalid_choice) + | _ -> raise Invalid_choice) | None -> let fst_constructor = match branches with | ((head, _), _) :: _ -> head - | [] -> raise DisambiguateChoices.Invalid_choice + | [] -> raise Invalid_choice in (match resolve env (Id fst_constructor) () with | Cic.MutConstruct (indtype_uri, indtype_no, _, _) -> (indtype_uri, indtype_no) | Cic.Implicit _ -> raise Try_again - | _ -> raise DisambiguateChoices.Invalid_choice) + | _ -> raise Invalid_choice) in Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term, (List.map do_branch branches)) - | CicAst.LetIn ((name, typ), def, body) -> + | CicNotationPt.Cast (t1, t2) -> + let cic_t1 = aux loc context t1 in + let cic_t2 = aux loc context t2 in + Cic.Cast (cic_t1, cic_t2) + | CicNotationPt.LetIn ((name, typ), def, body) -> let cic_def = aux loc context def in + let cic_name = CicNotationUtil.cic_name_of_name name in let cic_def = match typ with | None -> cic_def | Some t -> Cic.Cast (cic_def, aux loc context t) in - let cic_body = aux loc (name :: context) body in - Cic.LetIn (name, cic_def, cic_body) - | CicAst.LetRec (kind, defs, body) -> + let cic_body = aux loc (cic_name :: context) body in + Cic.LetIn (cic_name, cic_def, cic_body) + | CicNotationPt.LetRec (kind, defs, body) -> let context' = - List.fold_left (fun acc ((name, _), _, _) -> name :: acc) + List.fold_left + (fun acc ((name, _), _, _) -> + CicNotationUtil.cic_name_of_name name :: acc) context defs in let cic_body = aux loc context' body in @@ -186,9 +206,9 @@ let interpretate_term ~context ~env ~uri ~is_path ast = let cic_body = aux loc context' body in let cic_type = aux_option loc context (Some `Type) typ in let name = - match name with + match CicNotationUtil.cic_name_of_name name with | Cic.Anonymous -> - CicTextualParser2.fail loc + CicNotationPt.fail loc "Recursive functions cannot be anonymous" | Cic.Name name -> name in @@ -214,17 +234,16 @@ let interpretate_term ~context ~env ~uri ~is_path ast = Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic)) in List.fold_right (build_term inductiveFuns) inductiveFuns cic_body - | CicAst.Ident _ - | CicAst.Uri _ when is_path -> raise PathNotWellFormed - | CicAst.Ident (name, subst) - | CicAst.Uri (name, subst) as ast -> - let is_uri = function CicAst.Uri _ -> true | _ -> false in + | CicNotationPt.Ident _ + | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed + | CicNotationPt.Ident (name, subst) + | CicNotationPt.Uri (name, subst) as ast -> + let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in (try if is_uri ast then raise Not_found;(* don't search the env for URIs *) let index = find_in_environment name context in if subst <> None then - CicTextualParser2.fail loc - "Explicit substitutions not allowed here"; + CicNotationPt.fail loc "Explicit substitutions not allowed here"; Cic.Rel index with Not_found -> let cic = @@ -232,7 +251,7 @@ let interpretate_term ~context ~env ~uri ~is_path ast = try CicUtil.term_of_uri (UriManager.uri_of_string name) with UriManager.IllFormedUri _ -> - CicTextualParser2.fail loc "Ill formed URI" + CicNotationPt.fail loc "Ill formed URI" else resolve env (Id name) () in @@ -247,7 +266,7 @@ let interpretate_term ~context ~env ~uri ~is_path ast = (try List.assoc s ids_to_uris, aux loc context term with Not_found -> - raise DisambiguateChoices.Invalid_choice)) + raise Invalid_choice)) subst | None -> List.map (fun uri -> uri, Cic.Implicit None) uris) in @@ -286,38 +305,39 @@ let interpretate_term ~context ~env ~uri ~is_path ast = (CicPp.ppterm t) (String.concat "; " (List.map - (fun (s, term) -> s ^ " := " ^ CicAstPp.pp_term term) + (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term) subst))); *) t | _ -> - raise DisambiguateChoices.Invalid_choice + raise Invalid_choice with CicEnvironment.CircularDependency _ -> - raise DisambiguateChoices.Invalid_choice)) - | CicAst.Implicit -> Cic.Implicit None - | CicAst.UserInput -> Cic.Implicit (Some `Hole) - | CicAst.Num (num, i) -> resolve env (Num i) ~num () - | CicAst.Meta (index, subst) -> + raise Invalid_choice)) + | CicNotationPt.Implicit -> Cic.Implicit None + | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole) + | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num () + | CicNotationPt.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) - | CicAst.Sort `Prop -> Cic.Sort Cic.Prop - | CicAst.Sort `Set -> Cic.Sort Cic.Set - | CicAst.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *) - | CicAst.Sort `CProp -> Cic.Sort Cic.CProp - | CicAst.Symbol (symbol, instance) -> + | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop + | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set + | CicNotationPt.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *) + | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp + | CicNotationPt.Symbol (symbol, instance) -> resolve env (Symbol (symbol, instance)) () - and aux_option loc context annotation = function + | _ -> assert false (* god bless Bologna *) + and aux_option loc (context: Cic.name list) annotation = function | None -> Cic.Implicit annotation | Some term -> aux loc context term in match ast with - | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term - | term -> aux CicAst.dummy_floc context term + | CicNotationPt.AttributedTerm (`Loc loc, term) -> aux loc context term + | term -> aux dummy_floc context term let interpretate_path ~context ~env path = interpretate_term ~context ~env ~uri:None ~is_path:true path @@ -326,13 +346,13 @@ let interpretate_obj ~context ~env ~uri ~is_path obj = assert (context = []); assert (is_path = false); match obj with - | TacticAst.Inductive (params,tyl) -> + | GrafiteAst.Inductive (params,tyl) -> let uri = match uri with Some uri -> uri | None -> assert false in let context,params = let context,res = List.fold_left (fun (context,res) (name,t) -> - (Cic.Name name)::context, + Cic.Name name :: context, (name, interpretate_term context env None false t)::res ) ([],[]) params in @@ -374,13 +394,13 @@ let interpretate_obj ~context ~env ~uri ~is_path obj = ) tyl in Cic.InductiveDefinition (tyl,[],List.length params,[]) - | TacticAst.Record (params,name,ty,fields) -> + | GrafiteAst.Record (params,name,ty,fields) -> let uri = match uri with Some uri -> uri | None -> assert false in let context,params = let context,res = List.fold_left (fun (context,res) (name,t) -> - (Cic.Name name)::context, + (Cic.Name name :: context), (name, interpretate_term context env None false t)::res ) ([],[]) params in @@ -393,7 +413,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj = snd ( List.fold_left (fun (context,res) (name,ty) -> - let context' = (Cic.Name name)::context in + let context' = Cic.Name name :: context in context',(name,interpretate_term context env None false ty)::res ) (context,[]) fields) in let concl = @@ -412,7 +432,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj = let field_names = List.map fst fields in Cic.InductiveDefinition (tyl,[],List.length params,[`Class (`Record field_names)]) - | TacticAst.Theorem (flavour, name, ty, bo) -> + | GrafiteAst.Theorem (flavour, name, ty, bo) -> let attrs = [`Flavour flavour] in let ty' = interpretate_term [] env None false ty in (match bo with @@ -448,23 +468,27 @@ let rev_uniq = (* "aux" keeps domain in reverse order and doesn't care about duplicates. * Domain item more in deep in the list will be processed first. *) -let rec domain_rev_of_term ?(loc = CicAst.dummy_floc) context = function - | CicAst.AttributedTerm (`Loc loc, term) -> +let rec domain_rev_of_term ?(loc = dummy_floc) context = function + | CicNotationPt.AttributedTerm (`Loc loc, term) -> domain_rev_of_term ~loc context term - | CicAst.AttributedTerm (_, term) -> domain_rev_of_term ~loc context term - | CicAst.Appl terms -> + | CicNotationPt.AttributedTerm (_, term) -> + domain_rev_of_term ~loc context term + | CicNotationPt.Appl terms -> List.fold_left (fun dom term -> domain_rev_of_term ~loc context term @ dom) [] terms - | CicAst.Binder (kind, (var, typ), body) -> + | CicNotationPt.Binder (kind, (var, typ), body) -> let kind_dom = match kind with | `Exists -> [ Symbol ("exists", 0) ] | _ -> [] in let type_dom = domain_rev_of_term_option loc context typ in - let body_dom = domain_rev_of_term ~loc (var :: context) body in + let body_dom = + domain_rev_of_term ~loc + (CicNotationUtil.cic_name_of_name var :: context) body + in body_dom @ type_dom @ kind_dom - | CicAst.Case (term, indty_ident, outtype, branches) -> + | CicNotationPt.Case (term, indty_ident, outtype, branches) -> let term_dom = domain_rev_of_term ~loc context term in let outtype_dom = domain_rev_of_term_option loc context outtype in let get_first_constructor = function @@ -475,7 +499,7 @@ let rec domain_rev_of_term ?(loc = CicAst.dummy_floc) context = function let (term_context, args_domain) = List.fold_left (fun (cont, dom) (name, typ) -> - (name :: cont, + (CicNotationUtil.cic_name_of_name name :: cont, (match typ with | None -> dom | Some typ -> domain_rev_of_term ~loc cont typ @ dom))) @@ -490,14 +514,23 @@ let rec domain_rev_of_term ?(loc = CicAst.dummy_floc) context = function (match indty_ident with | None -> get_first_constructor branches | Some ident -> [ Id ident ]) - | CicAst.LetIn ((var, typ), body, where) -> + | CicNotationPt.Cast (term, ty) -> + let term_dom = domain_rev_of_term ~loc context term in + let ty_dom = domain_rev_of_term ~loc context ty in + ty_dom @ term_dom + | CicNotationPt.LetIn ((var, typ), body, where) -> let body_dom = domain_rev_of_term ~loc context body in let type_dom = domain_rev_of_term_option loc context typ in - let where_dom = domain_rev_of_term ~loc (var :: context) where in + let where_dom = + domain_rev_of_term ~loc + (CicNotationUtil.cic_name_of_name var :: context) where + in where_dom @ type_dom @ body_dom - | CicAst.LetRec (kind, defs, where) -> + | CicNotationPt.LetRec (kind, defs, where) -> let context' = - List.fold_left (fun acc ((var, typ), _, _) -> var :: acc) + List.fold_left + (fun acc ((var, typ), _, _) -> + CicNotationUtil.cic_name_of_name var :: acc) context defs in let where_dom = domain_rev_of_term ~loc context' where in @@ -509,12 +542,11 @@ let rec domain_rev_of_term ?(loc = CicAst.dummy_floc) context = function [] defs in where_dom @ defs_dom - | CicAst.Ident (name, subst) -> + | CicNotationPt.Ident (name, subst) -> (try let index = find_in_environment name context in if subst <> None then - CicTextualParser2.fail loc - "Explicit substitutions not allowed here" + CicNotationPt.fail loc "Explicit substitutions not allowed here" else [] with Not_found -> @@ -526,16 +558,20 @@ let rec domain_rev_of_term ?(loc = CicAst.dummy_floc) context = function let dom' = domain_rev_of_term ~loc context term in dom' @ dom) [Id name] subst)) - | CicAst.Uri _ -> [] - | CicAst.Implicit -> [] - | CicAst.Num (num, i) -> [ Num i ] - | CicAst.Meta (index, local_context) -> + | CicNotationPt.Uri _ -> [] + | CicNotationPt.Implicit -> [] + | CicNotationPt.Num (num, i) -> [ Num i ] + | CicNotationPt.Meta (index, local_context) -> List.fold_left (fun dom term -> domain_rev_of_term_option loc context term @ dom) [] local_context - | CicAst.Sort _ -> [] - | CicAst.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ] - | CicAst.UserInput -> assert false + | CicNotationPt.Sort _ -> [] + | CicNotationPt.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ] + | CicNotationPt.UserInput + | CicNotationPt.Literal _ + | CicNotationPt.Layout _ + | CicNotationPt.Magic _ + | CicNotationPt.Variable _ -> assert false and domain_rev_of_term_option loc context = function | None -> [] @@ -548,12 +584,12 @@ let domain_of_obj ~context ast = assert (context = []); let domain_rev = match ast with - | TacticAst.Theorem (_,_,ty,bo) -> + | GrafiteAst.Theorem (_,_,ty,bo) -> (match bo with None -> [] | Some bo -> domain_rev_of_term [] bo) @ domain_of_term [] ty - | TacticAst.Inductive (params,tyl) -> + | GrafiteAst.Inductive (params,tyl) -> let dom = List.flatten ( List.rev_map @@ -573,7 +609,7 @@ let domain_of_obj ~context ast = not ( List.exists (fun (name',_) -> name = Id name') params || List.exists (fun (name',_,_,_) -> name = Id name') tyl) ) dom - | TacticAst.Record (params,_,ty,fields) -> + | GrafiteAst.Record (params,_,ty,fields) -> let dom = List.flatten (List.rev_map (fun (_,ty) -> domain_rev_of_term [] ty) fields) in @@ -608,7 +644,7 @@ sig metasenv:Cic.metasenv -> ?initial_ugraph:CicUniv.universe_graph -> aliases:environment -> (* previous interpretation status *) - CicAst.term -> + CicNotationPt.term -> (environment * (* new interpretation status *) Cic.metasenv * (* new metasenv *) Cic.term* @@ -618,7 +654,7 @@ sig dbd:Mysql.dbd -> aliases:environment -> (* previous interpretation status *) uri:UriManager.uri option -> (* required only for inductive types *) - TacticAst.obj -> + GrafiteAst.obj -> (environment * (* new interpretation status *) Cic.metasenv * (* new metasenv *) Cic.obj * @@ -688,7 +724,10 @@ module Make (C: Callbacks) = let choices = choices_of_id dbd id in Hashtbl.add id_choices id choices; choices) - | Symbol (symb, _) -> DisambiguateChoices.lookup_symbol_choices symb + | Symbol (symb, _) -> + List.map DisambiguateChoices.mk_choice + (CicNotationRew.lookup_interpretations symb) +(* DisambiguateChoices.lookup_symbol_choices symb *) | Num instance -> DisambiguateChoices.lookup_num_choices () in if choices = [] then raise (No_choices item); @@ -741,8 +780,8 @@ module Make (C: Callbacks) = let k,ugraph1 = refine_thing metasenv context uri cic_thing ugraph in (k , ugraph1 ) with - | Try_again -> Uncertain,ugraph - | DisambiguateChoices.Invalid_choice -> Ko,ugraph + | Try_again -> Uncertain, ugraph + | Invalid_choice -> Ko, ugraph in (* (4) build all possible interpretations *) let rec aux current_env todo_dom base_univ = @@ -822,12 +861,12 @@ module Make (C: Callbacks) = ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases term = disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases - ~uri:None ~pp_thing:CicAstPp.pp_term ~domain_of_thing:domain_of_term + ~uri:None ~pp_thing:CicNotationPp.pp_term ~domain_of_thing:domain_of_term ~interpretate_thing:interpretate_term ~refine_thing:refine_term term let disambiguate_obj ~dbd ~aliases ~uri obj = disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~uri - ~pp_thing:TacticAstPp.pp_obj ~domain_of_thing:domain_of_obj + ~pp_thing:GrafiteAstPp.pp_obj ~domain_of_thing:domain_of_obj ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj obj end @@ -845,9 +884,10 @@ struct let input_or_locate_uri ~(title:string) ?id = raise Exit end module Disambiguator = Make (Callbacks) - let disambiguate_string ~dbd ?(context=[]) ?(metasenv=[]) ?initial_ugraph - ?(aliases=DisambiguateTypes.Environment.empty) term = - let ast = CicTextualParser2.parse_term (Stream.of_string term) in + let disambiguate_string ~dbd ?(context = []) ?(metasenv = []) ?initial_ugraph + ?(aliases = DisambiguateTypes.Environment.empty) term + = + let ast = CicNotationParser.parse_level2_ast (Stream.of_string term) in try Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast ?initial_ugraph ~aliases diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli index ca33fa422..6f74c23c0 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate.mli @@ -29,9 +29,9 @@ exception NoWellTypedInterpretation exception PathNotWellFormed val interpretate_path : - context:Cic.name list -> env:DisambiguateTypes.environment -> CicAst.term -> - Cic.term - + context:Cic.name list -> env:DisambiguateTypes.environment -> + DisambiguateTypes.term -> + Cic.term module type Disambiguator = sig @@ -41,7 +41,7 @@ sig metasenv:Cic.metasenv -> ?initial_ugraph:CicUniv.universe_graph -> aliases:DisambiguateTypes.environment ->(* previous interpretation status *) - CicAst.term -> + DisambiguateTypes.term -> (DisambiguateTypes.environment * (* new interpretation status *) Cic.metasenv * (* new metasenv *) Cic.term * @@ -51,7 +51,7 @@ sig dbd:Mysql.dbd -> aliases:DisambiguateTypes.environment ->(* previous interpretation status *) uri:UriManager.uri option -> (* required only for inductive types *) - TacticAst.obj -> + GrafiteAst.obj -> (DisambiguateTypes.environment * (* new interpretation status *) Cic.metasenv * (* new metasenv *) Cic.obj * @@ -79,3 +79,6 @@ sig Cic.term * CicUniv.universe_graph) list (* disambiguated term *) end + +val dummy_floc: Lexing.position * Lexing.position + diff --git a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml index 368bc2f45..9f3c554c6 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml +++ b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml @@ -30,69 +30,38 @@ open DisambiguateTypes exception Invalid_choice exception Choice_not_found of string -let symbol_choices = Hashtbl.create 1023 let num_choices = ref [] -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_binary_op symbol dsc appl_head = - add_symbol_choice symbol - (dsc, - (fun env _ args -> - let t1, t2 = - match args with - | [t1; t2] -> t1, t2 - | _ -> raise Invalid_choice - in - Cic.Appl [ appl_head; t1; t2 ])) - -let add_unary_op symbol dsc appl_head = - add_symbol_choice symbol - (dsc, - (fun env _ args -> - let t = match args with [t] -> t | _ -> raise Invalid_choice in - Cic.Appl [ appl_head; t ])) - let add_num_choice choice = num_choices := choice :: !num_choices -let lookup_symbol_choices symbol = - try - Hashtbl.find symbol_choices symbol - with Not_found -> [] - -let lookup_num_choices () = !num_choices - let has_description dsc = (fun x -> fst x = dsc) -let lookup_symbol_by_dsc symb dsc = - try - List.find (has_description dsc) (Hashtbl.find symbol_choices symb) - with Not_found -> - raise (Choice_not_found (sprintf "Symbol %s, dsc %s" symb dsc)) +let lookup_num_choices () = !num_choices let lookup_num_by_dsc dsc = try List.find (has_description dsc) !num_choices with Not_found -> raise (Choice_not_found ("Num with dsc " ^ dsc)) - (** initial table contents *) - -let _ = - add_binary_op "exists" "exists" - (Cic.MutInd (HelmLibraryObjects.Logic.ex_URI, 0, [])); - add_symbol_choice "cast" - ("type cast", - (fun env _ args -> - let t1, t2 = - match args with - | [t1; t2] -> t1, t2 - | _ -> raise Invalid_choice - in - Cic.Cast (t1, t2))); +let mk_choice (dsc, args, appl_pattern) = + dsc, + (fun env _ cic_args -> + let env' = + let names = + List.map (function CicNotationPt.IdentArg (_, name) -> name) args + in + try + List.combine names cic_args + with Invalid_argument _ -> raise Invalid_choice + in + CicNotationFwd.instantiate_appl_pattern env' appl_pattern) + +let lookup_symbol_by_dsc symbol dsc = + try + mk_choice + (List.find + (fun (dsc', _, _) -> dsc = dsc') + (CicNotationRew.lookup_interpretations symbol)) + with CicNotationRew.Interpretation_not_found | Not_found -> + raise (Choice_not_found (sprintf "Symbol %s, dsc %s" symbol dsc)) diff --git a/helm/ocaml/cic_disambiguation/disambiguateChoices.mli b/helm/ocaml/cic_disambiguation/disambiguateChoices.mli index 87d731e27..74dfaaa58 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateChoices.mli +++ b/helm/ocaml/cic_disambiguation/disambiguateChoices.mli @@ -27,44 +27,27 @@ open DisambiguateTypes (** {2 Choice registration low-level interface} *) - (** 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 - (** raised by lookup_XXXX below *) exception Choice_not_found of string - (** register a new symbol choice *) -val add_symbol_choice: string -> codomain_item -> unit - (** register a new number choice *) val add_num_choice: codomain_item -> unit -(** {2 Choice registration high-level interface} *) - - (** @param symbol - * @param description - * @param term cic application head *) -val add_binary_op: string -> string -> Cic.term -> unit - - (** @param symbol - * @param description - * @param term cic application head *) -val add_unary_op: string -> string -> Cic.term -> unit - (** {2 Choices lookup} * for user defined aliases *) - (** @param symbol symbol as per AST *) -val lookup_symbol_choices: string -> codomain_item list - val lookup_num_choices: unit -> codomain_item list + (** @param dsc description (1st component of codomain_item) *) +val lookup_num_by_dsc: string -> codomain_item + (** @param symbol symbol as per AST * @param dsc description (1st component of codomain_item) *) val lookup_symbol_by_dsc: string -> string -> codomain_item - (** @param dsc description (1st component of codomain_item) *) -val lookup_num_by_dsc: string -> codomain_item +val mk_choice: + string * CicNotationPt.argument_pattern list * + CicNotationPt.cic_appl_pattern -> + codomain_item diff --git a/helm/ocaml/cic_disambiguation/disambiguatePp.ml b/helm/ocaml/cic_disambiguation/disambiguatePp.ml new file mode 100644 index 000000000..1d36df44d --- /dev/null +++ b/helm/ocaml/cic_disambiguation/disambiguatePp.ml @@ -0,0 +1,47 @@ +(* Copyright (C) 2005, 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 DisambiguateTypes + +let pp_environment env = + let aliases = + Environment.fold + (fun domain_item (dsc, _) acc -> + let s = + match domain_item with + | Id id -> + GrafiteAstPp.pp_alias (GrafiteAst.Ident_alias (id, dsc)) ^ "." + | Symbol (symb, i) -> + GrafiteAstPp.pp_alias (GrafiteAst.Symbol_alias (symb, i, dsc)) + ^ "." + | Num i -> + GrafiteAstPp.pp_alias (GrafiteAst.Number_alias (i, dsc)) ^ "." + in + s :: acc) + env [] + in + String.concat "\n" (List.sort compare aliases) ^ + (if aliases = [] then "" else "\n") + diff --git a/helm/ocaml/cic_disambiguation/disambiguatePp.mli b/helm/ocaml/cic_disambiguation/disambiguatePp.mli new file mode 100644 index 000000000..985ba32fc --- /dev/null +++ b/helm/ocaml/cic_disambiguation/disambiguatePp.mli @@ -0,0 +1,27 @@ +(* Copyright (C) 2005, 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_environment: DisambiguateTypes.environment -> string + diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml index 64fcdb5a8..c30316769 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml @@ -23,16 +23,20 @@ * http://helm.cs.unibo.it/ *) -type term = CicAst.term -type tactic = (term, string) TacticAst.tactic -type tactical = (term, string) TacticAst.tactical -type script_entry = Command of tactical | Comment of CicAst.location * string -type script = CicAst.location * script_entry list +type term = CicNotationPt.term +type tactic = (term, string) GrafiteAst.tactic +type tactical = (term, string) GrafiteAst.tactical +type script_entry = + | Command of tactical + | Comment of CicNotationPt.location * string +type script = CicNotationPt.location * script_entry list type domain_item = - | Id of string (* literal *) - | Symbol of string * int (* literal, instance num *) - | Num of int (* instance num *) + | Id of string (* literal *) + | Symbol of string * int (* literal, instance num *) + | Num of int (* instance num *) + +exception Invalid_choice module OrderedDomain = struct diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli index 89d529015..084ce0122 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli @@ -31,6 +31,10 @@ type domain_item = (* module Domain: Set.S with type elt = domain_item *) module Environment: Map.S with type key = domain_item + (** 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 + type codomain_item = string * (* description *) (environment -> string -> Cic.term list -> Cic.term) @@ -65,14 +69,14 @@ val string_of_domain: domain_item list -> string (** {3 type shortands} *) -type term = CicAst.term -type tactic = (term, string) TacticAst.tactic -type tactical = (term, string) TacticAst.tactical +type term = CicNotationPt.term +type tactic = (term, string) GrafiteAst.tactic +type tactical = (term, string) GrafiteAst.tactical type script_entry = | Command of tactical - | Comment of CicAst.location * string -type script = CicAst.location * script_entry list + | Comment of CicNotationPt.location * string +type script = CicNotationPt.location * script_entry list val empty_environment: environment diff --git a/helm/ocaml/cic_notation/.depend b/helm/ocaml/cic_notation/.depend index 00d1f6fed..c08c2bf91 100644 --- a/helm/ocaml/cic_notation/.depend +++ b/helm/ocaml/cic_notation/.depend @@ -1,17 +1,19 @@ -cicNotationUtil.cmi: grafiteAst.cmo cicNotationPt.cmo +cicNotationUtil.cmi: cicNotationPt.cmo cicNotationTag.cmi: cicNotationPt.cmo cicNotationEnv.cmi: cicNotationPt.cmo cicNotationPp.cmi: cicNotationPt.cmo cicNotationEnv.cmi -cicNotationMatcher.cmi: grafiteAst.cmo cicNotationPt.cmo cicNotationEnv.cmi +grafiteAstPp.cmi: grafiteAst.cmo cicNotationPt.cmo +cicNotationMatcher.cmi: cicNotationPt.cmo cicNotationEnv.cmi cicNotationFwd.cmi: cicNotationPt.cmo cicNotationEnv.cmi +cicNotationRew.cmi: cicNotationPt.cmo cicNotationParser.cmi: cicNotationPt.cmo cicNotationEnv.cmi grafiteParser.cmi: grafiteAst.cmo cicNotationPt.cmo -cicNotationRew.cmi: grafiteAst.cmo cicNotationPt.cmo cicNotationPres.cmi: cicNotationPt.cmo +cicNotation.cmi: grafiteAst.cmo grafiteAst.cmo: cicNotationPt.cmo grafiteAst.cmx: cicNotationPt.cmx -cicNotationUtil.cmo: grafiteAst.cmo cicNotationPt.cmo cicNotationUtil.cmi -cicNotationUtil.cmx: grafiteAst.cmx cicNotationPt.cmx cicNotationUtil.cmi +cicNotationUtil.cmo: cicNotationPt.cmo cicNotationUtil.cmi +cicNotationUtil.cmx: cicNotationPt.cmx cicNotationUtil.cmi cicNotationTag.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationTag.cmi cicNotationTag.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationTag.cmi cicNotationLexer.cmo: cicNotationLexer.cmi @@ -20,16 +22,22 @@ cicNotationEnv.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationEnv.cmi cicNotationEnv.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationEnv.cmi cicNotationPp.cmo: cicNotationPt.cmo cicNotationEnv.cmi cicNotationPp.cmi cicNotationPp.cmx: cicNotationPt.cmx cicNotationEnv.cmx cicNotationPp.cmi -cicNotationMatcher.cmo: grafiteAst.cmo cicNotationUtil.cmi cicNotationTag.cmi \ +grafiteAstPp.cmo: grafiteAst.cmo cicNotationPp.cmi grafiteAstPp.cmi +grafiteAstPp.cmx: grafiteAst.cmx cicNotationPp.cmx grafiteAstPp.cmi +cicNotationMatcher.cmo: cicNotationUtil.cmi cicNotationTag.cmi \ cicNotationPt.cmo cicNotationPp.cmi cicNotationEnv.cmi \ cicNotationMatcher.cmi -cicNotationMatcher.cmx: grafiteAst.cmx cicNotationUtil.cmx cicNotationTag.cmx \ +cicNotationMatcher.cmx: cicNotationUtil.cmx cicNotationTag.cmx \ cicNotationPt.cmx cicNotationPp.cmx cicNotationEnv.cmx \ cicNotationMatcher.cmi cicNotationFwd.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationEnv.cmi \ cicNotationFwd.cmi cicNotationFwd.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationEnv.cmx \ cicNotationFwd.cmi +cicNotationRew.cmo: cicNotationUtil.cmi cicNotationPt.cmo \ + cicNotationMatcher.cmi cicNotationEnv.cmi cicNotationRew.cmi +cicNotationRew.cmx: cicNotationUtil.cmx cicNotationPt.cmx \ + cicNotationMatcher.cmx cicNotationEnv.cmx cicNotationRew.cmi cicNotationParser.cmo: cicNotationUtil.cmi cicNotationPt.cmo \ cicNotationPp.cmi cicNotationLexer.cmi cicNotationEnv.cmi \ cicNotationParser.cmi @@ -40,13 +48,11 @@ grafiteParser.cmo: grafiteAst.cmo cicNotationPt.cmo cicNotationParser.cmi \ grafiteParser.cmi grafiteParser.cmx: grafiteAst.cmx cicNotationPt.cmx cicNotationParser.cmx \ grafiteParser.cmi -cicNotationRew.cmo: grafiteAst.cmo cicNotationUtil.cmi cicNotationPt.cmo \ - cicNotationParser.cmi cicNotationMatcher.cmi cicNotationEnv.cmi \ - cicNotationRew.cmi -cicNotationRew.cmx: grafiteAst.cmx cicNotationUtil.cmx cicNotationPt.cmx \ - cicNotationParser.cmx cicNotationMatcher.cmx cicNotationEnv.cmx \ - cicNotationRew.cmi cicNotationPres.cmo: cicNotationUtil.cmi cicNotationPt.cmo \ cicNotationPres.cmi cicNotationPp.cmi cicNotationPres.cmi cicNotationPres.cmx: cicNotationUtil.cmx cicNotationPt.cmx \ cicNotationPres.cmx cicNotationPp.cmx cicNotationPres.cmi +cicNotation.cmo: grafiteParser.cmi grafiteAst.cmo cicNotationRew.cmi \ + cicNotationParser.cmi cicNotationFwd.cmi cicNotation.cmi +cicNotation.cmx: grafiteParser.cmx grafiteAst.cmx cicNotationRew.cmx \ + cicNotationParser.cmx cicNotationFwd.cmx cicNotation.cmi diff --git a/helm/ocaml/cic_notation/Makefile b/helm/ocaml/cic_notation/Makefile index 38859414d..d54e0a5f3 100644 --- a/helm/ocaml/cic_notation/Makefile +++ b/helm/ocaml/cic_notation/Makefile @@ -15,12 +15,14 @@ INTERFACE_FILES = \ cicNotationLexer.mli \ cicNotationEnv.mli \ cicNotationPp.mli \ + grafiteAstPp.mli \ cicNotationMatcher.mli \ cicNotationFwd.mli \ + cicNotationRew.mli \ cicNotationParser.mli \ grafiteParser.mli \ - cicNotationRew.mli \ cicNotationPres.mli \ + cicNotation.mli \ $(NULL) IMPLEMENTATION_FILES = \ cicNotationPt.ml \ diff --git a/helm/ocaml/cic_notation/TODO b/helm/ocaml/cic_notation/TODO index 73a2a49a6..7ba1c4f75 100644 --- a/helm/ocaml/cic_notation/TODO +++ b/helm/ocaml/cic_notation/TODO @@ -1,27 +1,33 @@ TODO -* implementare trasformazione 1 => 0 * gestione priorita'/associativita' - triplicare livelli nella grammatica? * implementare type-checker per le trasformazioni * prestazioni trasformazioni 3 => 2 e 2 => 1 * magic per gestione degli array? * gestione speciale dei numeri -* sintassi concreta / prelexing +* sintassi concreta - studiare/implementare sintassi con ... per i magic fold * integrazione - - porting della disambiguazione al nuovo ast - - apportare all'ast le modifiche di CicAst (case, cast non come annotazione, - tipi opzionali nel let rec e nelle definizioni) + - portare le trasformazioni al nuovo ast + - salvare la notazione nei file .moo + - togliere file non piu' utilizzati (caterva di cvs remove) DONE +* implementare trasformazione 1 => 0 * implementare istanziazione dei magic a livello 1 (2 => 1) * implementare compilazione dei default in 2 => 1 - -> Tue, 07 Jun 2005 17:17:36 +0200 zack * annotazioni nel livello 1 generato * problema con pattern overlapping per i magic al livello 2 * gestione greedyness dei magic in 2 => 1 * href multipli +* integrazione + - apportare all'ast le modifiche di CicAst (case, cast non come annotazione, + tipi opzionali nel let rec e nelle definizioni) +* integrazione + - porting della disambiguazione al nuovo ast + - refactoring: unico punto di accesso allo stato imperativo della notazione + - gestire cast diff --git a/helm/ocaml/cic_notation/cicNotation.ml b/helm/ocaml/cic_notation/cicNotation.ml new file mode 100644 index 000000000..87eb9980e --- /dev/null +++ b/helm/ocaml/cic_notation/cicNotation.ml @@ -0,0 +1,64 @@ +(* Copyright (C) 2005, 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 GrafiteAst + +type notation_id = + | RuleId of CicNotationParser.rule_id + | InterpretationId of CicNotationRew.interpretation_id + | PrettyPrinterId of CicNotationRew.pretty_printer_id + +let process_notation st = + match st with + | Notation (loc, l1, associativity, precedence, l2) -> + let rule_id = + CicNotationParser.extend l1 ?precedence ?associativity + (fun env loc -> CicNotationFwd.instantiate_level2 env l2) + in + let pp_id = + CicNotationRew.add_pretty_printer ?precedence ?associativity l2 l1 + in + st, [ RuleId rule_id; PrettyPrinterId pp_id ] + | Interpretation (loc, dsc, l2, l3) -> + let interp_id = CicNotationRew.add_interpretation dsc l2 l3 in + st, [ InterpretationId interp_id ] + | st -> st, [] + +let remove_notation = function + | RuleId id -> CicNotationParser.delete id + | PrettyPrinterId id -> CicNotationRew.remove_pretty_printer id + | InterpretationId id -> CicNotationRew.remove_interpretation id + +let load_notation fname = + let ic = open_in fname in + let istream = Stream.of_channel ic in + try + while true do + match GrafiteParser.parse_statement istream with + | Executable (_, Command (_, cmd)) -> ignore (process_notation cmd) + | _ -> () + done + with End_of_file -> close_in ic + diff --git a/helm/ocaml/cic_notation/cicNotation.mli b/helm/ocaml/cic_notation/cicNotation.mli new file mode 100644 index 000000000..082f08b05 --- /dev/null +++ b/helm/ocaml/cic_notation/cicNotation.mli @@ -0,0 +1,35 @@ +(* Copyright (C) 2005, 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 notation_id + +val process_notation: + ('a, 'b) GrafiteAst.command -> ('a, 'b) GrafiteAst.command * notation_id list + +val remove_notation: notation_id -> unit + +(** @param fname file from which load notation *) +val load_notation: string -> unit + diff --git a/helm/ocaml/cic_notation/cicNotationFwd.ml b/helm/ocaml/cic_notation/cicNotationFwd.ml index 8e955c0b1..93a4c684d 100644 --- a/helm/ocaml/cic_notation/cicNotationFwd.ml +++ b/helm/ocaml/cic_notation/cicNotationFwd.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +open Printf + open CicNotationEnv open CicNotationPt @@ -246,3 +248,18 @@ let instantiate_level2 env term = in aux env term +let instantiate_appl_pattern env appl_pattern = + let lookup name = + try List.assoc name env + with Not_found -> + prerr_endline (sprintf "Name %s not found" name); + assert false + in + let rec aux = function + | UriPattern uri -> CicUtil.term_of_uri uri + | ImplicitPattern -> Cic.Implicit None + | VarPattern name -> lookup name + | ApplPattern terms -> Cic.Appl (List.map aux terms) + in + aux appl_pattern + diff --git a/helm/ocaml/cic_notation/cicNotationFwd.mli b/helm/ocaml/cic_notation/cicNotationFwd.mli index 0cb0a8669..4a5d89f98 100644 --- a/helm/ocaml/cic_notation/cicNotationFwd.mli +++ b/helm/ocaml/cic_notation/cicNotationFwd.mli @@ -28,3 +28,9 @@ val instantiate_level2: CicNotationEnv.t -> CicNotationPt.term -> CicNotationPt.term + (** @param env environment from argument_pattern to cic terms + * @param pat cic_appl_pattern *) +val instantiate_appl_pattern: + (string * Cic.term) list -> CicNotationPt.cic_appl_pattern -> + Cic.term + diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml index b5cd026d6..9897412b9 100644 --- a/helm/ocaml/cic_notation/cicNotationLexer.ml +++ b/helm/ocaml/cic_notation/cicNotationLexer.ml @@ -94,8 +94,8 @@ let _ = (* TODO ZACK: keyword list almost cut and paste from cicTextualLexer2.ml, to * be reviewed *) List.iter (fun k -> Hashtbl.add level2_ast_keywords k ()) - [ "Prop"; "Type"; "Set"; "let"; "rec"; "corec"; "match"; "with"; "in"; - "and"; "on" ] + [ "Prop"; "Type"; "Set"; "let"; "rec"; "corec"; "using"; "match"; "with"; + "in"; "and"; "to"; "as"; "on"; "names" ] let add_level2_ast_keyword k = Hashtbl.add level2_ast_keywords k () let remove_level2_ast_keyword k = Hashtbl.remove level2_ast_keywords k @@ -217,7 +217,8 @@ let rec level2_ast_token = lexer | uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf) | qstring -> return lexbuf ("QSTRING", remove_quotes (Ulexing.utf8_lexeme lexbuf)) - | csymbol -> return lexbuf ("CSYMBOL", Ulexing.utf8_lexeme lexbuf) + | csymbol -> + return lexbuf ("CSYMBOL", remove_left_quote (Ulexing.utf8_lexeme lexbuf)) | "${" -> read_unparsed_group "UNPARSED_META" lexbuf | "@{" -> read_unparsed_group "UNPARSED_AST" lexbuf | '(' -> return lexbuf ("LPAREN", "") diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml index 2ae4fd00e..91937ed34 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.ml +++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml @@ -373,19 +373,20 @@ struct Hashtbl.hash mask, tl let mask_of_appl_pattern = function - | GrafiteAst.UriPattern uri -> Uri uri, [] - | GrafiteAst.VarPattern _ -> Blob, [] - | GrafiteAst.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl + | Pt.UriPattern uri -> Uri uri, [] + | Pt.ImplicitPattern + | Pt.VarPattern _ -> Blob, [] + | Pt.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl let tag_of_pattern p = let mask, pl = mask_of_appl_pattern p in Hashtbl.hash mask, pl - type pattern_t = GrafiteAst.cic_appl_pattern + type pattern_t = Pt.cic_appl_pattern type term_t = Cic.annterm let classify = function - | GrafiteAst.VarPattern _ -> Variable + | Pt.VarPattern _ -> Variable | _ -> Constructor end @@ -399,7 +400,8 @@ struct List.map2 (fun p t -> match p with - | GrafiteAst.VarPattern name -> name, t + | Pt.ImplicitPattern -> Util.fresh_name (), t + | Pt.VarPattern name -> name, t | _ -> assert false) pl matched_terms in diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.mli b/helm/ocaml/cic_notation/cicNotationMatcher.mli index 3846bf528..4a9d4a275 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.mli +++ b/helm/ocaml/cic_notation/cicNotationMatcher.mli @@ -54,7 +54,7 @@ end module Matcher32: sig val compiler : - (GrafiteAst.cic_appl_pattern * int) list -> + (CicNotationPt.cic_appl_pattern * int) list -> (Cic.annterm -> ((string * Cic.annterm) list * int) option) end diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index e52baffdd..c9a5fbafb 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -40,16 +40,6 @@ let min_precedence = 0 let max_precedence = 100 let default_precedence = 50 -let let_in_prec = 10 -let binder_prec = 20 -let apply_prec = 70 -let simple_prec = 90 - -let let_in_assoc = Gramext.NonA -let binder_assoc = Gramext.RightA -let apply_assoc = Gramext.LeftA -let simple_assoc = Gramext.NonA - let level1_pattern = Grammar.Entry.create level1_pattern_grammar "level1_pattern" let level2_ast = Grammar.Entry.create level2_ast_grammar "level2_ast" @@ -59,10 +49,6 @@ let level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta" let return_term loc term = () -let fail floc msg = - let (x, y) = loc_of_floc floc in - failwith (sprintf "Error at characters %d - %d: %s" x y msg) - let int_of_string s = try Pervasives.int_of_string s @@ -578,7 +564,7 @@ EXTEND SYMBOL "]" -> return_term loc (Case (t, indty_ident, outtyp, patterns)) | LPAREN; p1 = term; SYMBOL ":"; p2 = term; RPAREN -> - return_term loc (Appl [ Symbol ("cast", 0); p1; p2 ]) + return_term loc (Cast (p1, p2)) | LPAREN; p = term; RPAREN -> p | blob = UNPARSED_META -> !parse_level2_meta_ref (Stream.of_string blob) ] diff --git a/helm/ocaml/cic_notation/cicNotationParser.mli b/helm/ocaml/cic_notation/cicNotationParser.mli index 2819f4d9d..083d442eb 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.mli +++ b/helm/ocaml/cic_notation/cicNotationParser.mli @@ -48,18 +48,6 @@ val extend: val delete: rule_id -> unit -(** {2 Standard precedences} *) - -val let_in_prec: int -val binder_prec: int -val apply_prec: int -val simple_prec: int - -val let_in_assoc: Gramext.g_assoc -val binder_assoc: Gramext.g_assoc -val apply_assoc: Gramext.g_assoc -val simple_assoc: Gramext.g_assoc - (** {2 Grammar entries} * needed by grafite parser *) diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml index fcb42fd18..f98b51067 100644 --- a/helm/ocaml/cic_notation/cicNotationPp.ml +++ b/helm/ocaml/cic_notation/cicNotationPp.ml @@ -62,6 +62,7 @@ let rec pp_term = function sprintf "%smatch %s with %s" (match typ with None -> "" | Some t -> sprintf "<%s>" (pp_term t)) (pp_term term) (pp_patterns patterns) + | Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term t1) (pp_term t2) | LetIn (var, t1, t2) -> sprintf "let %s = %s in %s" (pp_capture_variable var) (pp_term t1) (pp_term t2) diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml index 56272ebed..ba31a3705 100644 --- a/helm/ocaml/cic_notation/cicNotationPt.ml +++ b/helm/ocaml/cic_notation/cicNotationPt.ml @@ -35,6 +35,9 @@ type location = Lexing.position * Lexing.position let loc_of_floc = function | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } -> (loc_begin, loc_end) +let fail floc msg = + let (x, y) = loc_of_floc floc in + failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg) type term_attribute = [ `Loc of location (* source file location *) @@ -60,6 +63,7 @@ type term = | Binder of binder_kind * capture_variable * term (* kind, name, body *) | Case of term * string option * term option * (case_pattern * term) list (* what to match, inductive type, out type, list *) + | Cast of term * term | LetIn of capture_variable * term * term (* name, body, where *) | LetRec of induction_kind * (capture_variable * term * int) list * term (* (name, body, decreasing argument) list, where *) @@ -136,3 +140,24 @@ and pattern_variable = (* level 2 variables *) | FreshVar of string +type argument_pattern = + | IdentArg of int * string (* eta-depth, name *) + +type cic_appl_pattern = + | UriPattern of UriManager.uri + | VarPattern of string + | ImplicitPattern + | ApplPattern of cic_appl_pattern list + +(** {2 Standard precedences} *) + +let let_in_prec = 10 +let binder_prec = 20 +let apply_prec = 70 +let simple_prec = 90 + +let let_in_assoc = Gramext.NonA +let binder_assoc = Gramext.RightA +let apply_assoc = Gramext.LeftA +let simple_assoc = Gramext.NonA + diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 15947f3f2..91b40fbee 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -32,8 +32,10 @@ type pretty_printer_id = pattern_id let default_prec = 50 let default_assoc = Gramext.NonA +module Ast = CicNotationPt + type term_info = - { sort: (Cic.id, CicNotationPt.sort_kind) Hashtbl.t; + { sort: (Cic.id, Ast.sort_kind) Hashtbl.t; uri: (Cic.id, string) Hashtbl.t; } @@ -62,15 +64,6 @@ let constructor_of_inductive_type uri i j = fst (List.nth (constructors_of_inductive_type uri i) (j-1)) with Not_found -> assert false) -module Ast = CicNotationPt -module Parser = CicNotationParser - -let string_of_name = function - | Cic.Name s -> s - | Cic.Anonymous -> "_" - -let ident_of_name n = Ast.Ident (string_of_name n, None) - let idref id t = Ast.AttributedTerm (`IdRef id, t) let resolve_binder = function @@ -92,7 +85,7 @@ let pp_ast0 t k = in let rec aux = function | Ast.Appl ts -> - Ast.AttributedTerm (`Level (Parser.apply_prec, Parser.apply_assoc), + Ast.AttributedTerm (`Level (Ast.apply_prec, Ast.apply_assoc), Ast.Layout (Ast.Box ((Ast.HOV, true, true), (CicNotationUtil.dress @@ -100,14 +93,14 @@ let pp_ast0 t k = (List.map k ts))))) | Ast.Binder (`Forall, (Ast.Ident ("_", _), ty), body) | Ast.Binder (`Pi, (Ast.Ident ("_", _), ty), body) -> - Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc), + Ast.AttributedTerm (`Level (Ast.binder_prec, Ast.binder_assoc), Ast.Layout (Ast.Box ((Ast.HV, false, true), [ aux_ty ty; Ast.Layout Ast.Break; binder_symbol "\\to"; k body]))) | Ast.Binder (binder_kind, (id, ty), body) -> - Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc), + Ast.AttributedTerm (`Level (Ast.binder_prec, Ast.binder_assoc), Ast.Layout (Ast.Box ((Ast.HV, false, true), [ binder_symbol (resolve_binder binder_kind); k id; @@ -164,13 +157,15 @@ let ast_of_acic0 term_info acic k = | `Set | `Type -> `Pi | `Prop | `CProp -> `Forall in - idref id (Ast.Binder (binder_kind, (ident_of_name n, Some (k s)), k t)) - | Cic.ACast (id,v,t) -> - idref id (Ast.Appl [idref id (Ast.Symbol ("cast", 0)); k v; k t]) + idref id (Ast.Binder (binder_kind, + (CicNotationUtil.name_of_cic_name n, Some (k s)), k t)) + | Cic.ACast (id,v,t) -> idref id (Ast.Cast (k v, k t)) | Cic.ALambda (id,n,s,t) -> - idref id (Ast.Binder (`Lambda, (ident_of_name n, Some (k s)), k t)) + idref id (Ast.Binder (`Lambda, + (CicNotationUtil.name_of_cic_name n, Some (k s)), k t)) | Cic.ALetIn (id,n,s,t) -> - idref id (Ast.LetIn ((ident_of_name n, None), k s, k t)) + idref id (Ast.LetIn ((CicNotationUtil.name_of_cic_name n, None), + k s, k t)) | Cic.AAppl (aid,args) -> idref aid (Ast.Appl (List.map k args)) | Cic.AConst (id,uri,substs) -> register_uri id (UriManager.string_of_uri uri); @@ -196,7 +191,7 @@ let ast_of_acic0 term_info acic k = match (ty, pat) with | Cic.Prod (_, _, t), Cic.ALambda (_, name, s, t') -> let (cv, rhs) = eat_branch t t' in - (ident_of_name name, Some (k s)) :: cv, rhs + (CicNotationUtil.name_of_cic_name name, Some (k s)) :: cv, rhs | _, _ -> [], k pat in let patterns = @@ -243,6 +238,7 @@ let ast_of_acic0 term_info acic k = let level1_patterns21 = Hashtbl.create 211 let level2_patterns32 = Hashtbl.create 211 +let interpretations = Hashtbl.create 211 (* symb -> id list ref *) let compiled21 = ref None let compiled32 = ref None @@ -296,7 +292,7 @@ let instantiate21 env (* precedence associativity *) l1 = let sep = match sep_opt with | None -> [] - | Some l -> [ CicNotationPt.Literal l ] + | Some l -> [ Ast.Literal l ] in let rec instantiate_list acc = function | [] -> List.rev acc @@ -367,7 +363,7 @@ let rec pp_ast1 term = let instantiate32 term_info env symbol args = let rec instantiate_arg = function - | GrafiteAst.IdentArg (n, name) -> + | Ast.IdentArg (n, name) -> let t = (try List.assoc name env with Not_found -> assert false) in let rec count_lambda = function | Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body @@ -393,7 +389,7 @@ let rec ast_of_acic1 term_info annterm = let env' = List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) env in - let symbol, args, uris = + let _, symbol, args, _, uris = try Hashtbl.find level2_patterns32 pid with Not_found -> assert false @@ -422,14 +418,34 @@ let fresh_id = incr counter; !counter -let add_interpretation (symbol, args) appl_pattern = +let add_interpretation dsc (symbol, args) appl_pattern = let id = fresh_id () in let uris = CicNotationUtil.find_appl_pattern_uris appl_pattern in - Hashtbl.add level2_patterns32 id (symbol, args, uris); + Hashtbl.add level2_patterns32 id (dsc, symbol, args, appl_pattern, uris); pattern32_matrix := (appl_pattern, id) :: !pattern32_matrix; load_patterns32 !pattern32_matrix; + (try + let ids = Hashtbl.find interpretations symbol in + ids := id :: !ids + with Not_found -> Hashtbl.add interpretations symbol (ref [id])); id +exception Interpretation_not_found +exception Pretty_printer_not_found + +let lookup_interpretations symbol = + try + List.map + (fun id -> + let (dsc, _, args, appl_pattern, _) = + try + Hashtbl.find level2_patterns32 id + with Not_found -> assert false + in + dsc, args, appl_pattern) + !(Hashtbl.find interpretations symbol) + with Not_found -> raise Interpretation_not_found + let add_pretty_printer ?(precedence = default_prec) ?(associativity = default_assoc) l2 l1 = @@ -440,11 +456,11 @@ let add_pretty_printer load_patterns21 !pattern21_matrix; id -exception Interpretation_not_found -exception Pretty_printer_not_found - let remove_interpretation id = (try + let _, symbol, _, _, _ = Hashtbl.find level2_patterns32 id in + let ids = Hashtbl.find interpretations symbol in + ids := List.filter ((<>) id) !ids; Hashtbl.remove level2_patterns32 id; with Not_found -> raise Interpretation_not_found); pattern32_matrix := List.filter (fun (_, id') -> id <> id') !pattern32_matrix; diff --git a/helm/ocaml/cic_notation/cicNotationRew.mli b/helm/ocaml/cic_notation/cicNotationRew.mli index 7c2415a73..105f3ffba 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.mli +++ b/helm/ocaml/cic_notation/cicNotationRew.mli @@ -39,10 +39,17 @@ type interpretation_id type pretty_printer_id val add_interpretation: - string * GrafiteAst.argument_pattern list -> (* level 2 pattern *) - GrafiteAst.cic_appl_pattern -> (* level 3 pattern *) + string -> (* id / description *) + string * CicNotationPt.argument_pattern list -> (* symbol, level 2 pattern *) + CicNotationPt.cic_appl_pattern -> (* level 3 pattern *) interpretation_id + (** @raise Interpretation_not_found *) +val lookup_interpretations: + string -> (* symbol *) + (string * CicNotationPt.argument_pattern list * + CicNotationPt.cic_appl_pattern) list + val add_pretty_printer: ?precedence:int -> ?associativity:Gramext.g_assoc -> diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml index 4dbc83f9e..4489344f5 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.ml +++ b/helm/ocaml/cic_notation/cicNotationUtil.ml @@ -25,13 +25,6 @@ open CicNotationPt - (* TODO ensure that names generated by fresh_var do not clash with user's *) -let fresh_name = - let index = ref ~-1 in - fun () -> - incr index; - "fresh" ^ string_of_int !index - (* let meta_names_of term = *) (* let rec names = ref [] in *) (* let add_name n = *) @@ -105,6 +98,7 @@ let visit_ast ?(special_k = fun _ -> assert false) k = Binder (kind, aux_capture_variable var, k body) | Case (term, indtype, typ, patterns) -> Case (k term, indtype, aux_opt typ, aux_patterns patterns) + | Cast (t1, t2) -> Cast (k t1, k t2) | LetIn (var, t1, t2) -> LetIn (aux_capture_variable var, k t1, k t2) | LetRec (kind, definitions, term) -> let definitions = @@ -350,13 +344,14 @@ let dress sauce = let find_appl_pattern_uris ap = let rec aux acc = function - | GrafiteAst.UriPattern uri -> + | UriPattern uri -> (try ignore (List.find (fun uri' -> UriManager.eq uri uri') acc); acc with Not_found -> uri :: acc) - | GrafiteAst.VarPattern _ -> acc - | GrafiteAst.ApplPattern apl -> List.fold_left aux acc apl + | ImplicitPattern + | VarPattern _ -> acc + | ApplPattern apl -> List.fold_left aux acc apl in aux [] ap @@ -365,3 +360,24 @@ let rec find_branch = Magic (If (_, Magic Fail, t)) -> find_branch t | Magic (If (_, t, _)) -> find_branch t | t -> t + +let cic_name_of_name = function + | CicNotationPt.Ident ("_", None) -> Cic.Anonymous + | CicNotationPt.Ident (name, None) -> Cic.Name name + | _ -> assert false + +let name_of_cic_name = function + | Cic.Name s -> CicNotationPt.Ident (s, None) + | Cic.Anonymous -> CicNotationPt.Ident ("_", None) + +let fresh_index = ref ~-1 + +type notation_id = int + +let fresh_id () = + incr fresh_index; + !fresh_index + + (* TODO ensure that names generated by fresh_var do not clash with user's *) +let fresh_name () = "fresh" ^ string_of_int (fresh_id ()) + diff --git a/helm/ocaml/cic_notation/cicNotationUtil.mli b/helm/ocaml/cic_notation/cicNotationUtil.mli index 6661245af..d11f1917e 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.mli +++ b/helm/ocaml/cic_notation/cicNotationUtil.mli @@ -55,7 +55,18 @@ val boxify: CicNotationPt.term list -> CicNotationPt.term val group: CicNotationPt.term list -> CicNotationPt.term val ungroup: CicNotationPt.term list -> CicNotationPt.term list -val find_appl_pattern_uris: GrafiteAst.cic_appl_pattern -> UriManager.uri list +val find_appl_pattern_uris: + CicNotationPt.cic_appl_pattern -> UriManager.uri list val find_branch: CicNotationPt.term -> CicNotationPt.term + +val cic_name_of_name: CicNotationPt.term -> Cic.name +val name_of_cic_name: Cic.name -> CicNotationPt.term + + (** Notation id handling *) + +type notation_id + +val fresh_id: unit -> notation_id + diff --git a/helm/ocaml/cic_notation/doc/core_notation.ma b/helm/ocaml/cic_notation/doc/core_notation.ma deleted file mode 100644 index bb62bd372..000000000 --- a/helm/ocaml/cic_notation/doc/core_notation.ma +++ /dev/null @@ -1,72 +0,0 @@ -notation "hvbox(a break \to b)" - right associative with precedence 20 -for @{ \forall $_:$a.$b }. - -notation "hvbox(a break = b)" - non associative with precedence 45 -for @{ 'eq $a $b }. - -notation "hvbox(a break \leq b)" - non associative with precedence 45 -for @{ 'leq $a $b }. - -notation "hvbox(a break \geq b)" - non associative with precedence 45 -for @{ 'geq $a $b }. - -notation "hvbox(a break \lt b)" - non associative with precedence 45 -for @{ 'lt $a $b }. - -notation "hvbox(a break \gt b)" - non associative with precedence 45 -for @{ 'gt $a $b }. - -notation "hvbox(a break \neq b)" - non associative with precedence 45 -for @{ 'neq $a $b }. - -notation "hvbox(a break + b)" - left associative with precedence 50 -for @{ 'plus $a $b }. - -notation "hvbox(a break - b)" - left associative with precedence 50 -for @{ 'minus $a $b }. - -notation "hvbox(a break * b)" - left associative with precedence 55 -for @{ 'times $a $b }. - -notation "hvbox(a break / b)" - left associative with precedence 55 -for @{ 'divide $a $b }. - -notation "\frac a b" - non associative with precedence 90 -for @{ 'divide $a $b }. - -notation "a \over b" - non associative with precedence 55 -for @{ 'divide $a $b }. - -notation "- a" - non associative with precedence 60 -for @{ 'uminus $a }. - -notation "\sqrt a" - non associative with precedence 60 -for @{ 'sqrt $a }. - -notation "hvbox(a break \lor b)" - left associative with precedence 30 -for @{ 'or $a $b }. - -notation "hvbox(a break \land b)" - left associative with precedence 35 -for @{ 'or $a $b }. - -notation "hvbox(a break \lnot b)" - left associative with precedence 40 -for @{ 'or $a $b }. - diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml index 5117fd493..e845e5755 100644 --- a/helm/ocaml/cic_notation/grafiteAst.ml +++ b/helm/ocaml/cic_notation/grafiteAst.ml @@ -120,14 +120,6 @@ type obj = (string * CicNotationPt.term) list * string * CicNotationPt.term * (string * CicNotationPt.term) list -type argument_pattern = - | IdentArg of int * string (* eta-depth, name *) - -type cic_appl_pattern = - | UriPattern of UriManager.uri - | VarPattern of string - | ApplPattern of cic_appl_pattern list - type ('term,'obj) command = | Default of loc * string * UriManager.uri list | Include of loc * string @@ -141,9 +133,13 @@ type ('term,'obj) command = | Alias of loc * alias_spec (** parameters, name, type, fields *) | Obj of loc * 'obj - | Notation of loc * 'term * Gramext.g_assoc option * int option * 'term + | Notation of loc * CicNotationPt.term * Gramext.g_assoc option * int option * + CicNotationPt.term (* level 1 pattern, associativity, precedence, level 2 pattern *) - | Interpretation of loc * (string * argument_pattern list) * cic_appl_pattern + | Interpretation of loc * + string * (string * CicNotationPt.argument_pattern list) * + CicNotationPt.cic_appl_pattern + (* description (i.e. id), symbol, arg pattern, appl pattern *) (* DEBUGGING *) | Dump of loc (* dump grammar on stdout *) diff --git a/helm/ocaml/cic_notation/grafiteAstPp.ml b/helm/ocaml/cic_notation/grafiteAstPp.ml new file mode 100644 index 000000000..db7a7253e --- /dev/null +++ b/helm/ocaml/cic_notation/grafiteAstPp.ml @@ -0,0 +1,283 @@ +(* 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 GrafiteAst + +let tactical_terminator = "." +let tactic_terminator = tactical_terminator +let command_terminator = tactical_terminator + +let pp_term_ast term = CicNotationPp.pp_term term +let pp_term_cic term = CicPp.ppterm term + +let pp_idents idents = "[" ^ String.concat "; " idents ^ "]" + +let pp_terms_ast terms = String.concat ", " (List.map pp_term_ast terms) + +let pp_reduction_kind = function + | `Reduce -> "reduce" + | `Simpl -> "simplify" + | `Whd -> "whd" + | `Normalize -> "normalize" + + +let pp_pattern (t, hyp, goal) = + let pp_hyp_pattern l = + String.concat "; " + (List.map (fun (name, p) -> sprintf "%s : %s" name (pp_term_ast p)) l) in + let pp_t t = + match t with + None -> "" + | Some t -> pp_term_ast t + in + pp_t t ^ " in " ^ pp_hyp_pattern hyp ^ " \\vdash " ^ pp_term_ast goal + +let pp_intros_specs = function + | None, [] -> "" + | Some num, [] -> Printf.sprintf " names %i" num + | None, idents -> Printf.sprintf " names %s" (pp_idents idents) + | Some num, idents -> Printf.sprintf " names %i %s" num (pp_idents idents) + +let rec pp_tactic = function + | Absurd (_, term) -> "absurd" ^ pp_term_ast term + | Apply (_, term) -> "apply " ^ pp_term_ast term + | Auto _ -> "auto" + | Assumption _ -> "assumption" + | Change (_, where, with_what) -> + sprintf "change %s with %s" (pp_pattern where) (pp_term_ast with_what) + | Clear (_,id) -> sprintf "clear %s" id + | ClearBody (_,id) -> sprintf "clearbody %s" id + | Compare (_,term) -> "compare " ^ pp_term_ast term + | Constructor (_,n) -> "constructor " ^ string_of_int n + | Contradiction _ -> "contradiction" + | Cut (_, ident, term) -> + "cut " ^ pp_term_ast term ^ + (match ident with None -> "" | Some id -> " as " ^ id) + | DecideEquality _ -> "decide equality" + | Decompose (_, term) -> + sprintf "decompose %s" (pp_term_ast term) + | Discriminate (_, term) -> "discriminate " ^ pp_term_ast term + | Elim (_, term, using, num, idents) -> + sprintf "elim " ^ pp_term_ast term ^ + (match using with None -> "" | Some term -> " using " ^ pp_term_ast term) + ^ pp_intros_specs (num, idents) + | ElimType (_, term, using, num, idents) -> + sprintf "elim type " ^ pp_term_ast term ^ + (match using with None -> "" | Some term -> " using " ^ pp_term_ast term) + ^ pp_intros_specs (num, idents) + | Exact (_, term) -> "exact " ^ pp_term_ast term + | Exists _ -> "exists" + | Fold (_, kind, term, pattern) -> + sprintf "fold %s %s %s" (pp_reduction_kind kind) + (pp_term_ast term) (pp_pattern pattern) + | FwdSimpl (_, hyp, idents) -> + sprintf "fwd %s%s" hyp + (match idents with [] -> "" | idents -> " " ^ pp_idents idents) + | Generalize (_, pattern, ident) -> + sprintf "generalize %s%s" (pp_pattern pattern) + (match ident with None -> "" | Some id -> " as " ^ id) + | Goal (_, n) -> "goal " ^ string_of_int n + | Fail _ -> "fail" + | Fourier _ -> "fourier" + | IdTac _ -> "id" + | Injection (_, term) -> "injection " ^ pp_term_ast term + | Intros (_, None, []) -> "intro" + | Intros (_, num, idents) -> + sprintf "intros%s%s" + (match num with None -> "" | Some num -> " " ^ string_of_int num) + (match idents with [] -> "" | idents -> " " ^ pp_idents idents) + | LApply (_, level_opt, terms, term, ident_opt) -> + sprintf "lapply %s%s%s%s" + (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ") + (pp_term_ast term) + (match terms with [] -> "" | _ -> " to " ^ pp_terms_ast terms) + (match ident_opt with None -> "" | Some ident -> " using " ^ ident) + | Left _ -> "left" + | LetIn (_, term, ident) -> sprintf "let %s in %s" (pp_term_ast term) ident + | Reduce (_, kind, pat) -> + sprintf "%s %s" (pp_reduction_kind kind) (pp_pattern pat) + | Reflexivity _ -> "reflexivity" + | Replace (_, pattern, t) -> + sprintf "replace %s with %s" (pp_pattern pattern) (pp_term_ast t) + | Rewrite (_, pos, t, pattern) -> + sprintf "rewrite %s %s %s" + (if pos = `LeftToRight then ">" else "<") + (pp_term_ast t) + (pp_pattern pattern) + | Right _ -> "right" + | Ring _ -> "ring" + | Split _ -> "split" + | Symmetry _ -> "symmetry" + | Transitivity (_, term) -> "transitivity " ^ pp_term_ast term + +let pp_flavour = function + | `Definition -> "Definition" + | `Fact -> "Fact" + | `Goal -> "Goal" + | `Lemma -> "Lemma" + | `Remark -> "Remark" + | `Theorem -> "Theorem" + | `Variant -> "Variant" + +let pp_search_kind = function + | `Locate -> "locate" + | `Hint -> "hint" + | `Match -> "match" + | `Elim -> "elim" + | `Instance -> "instance" + +let pp_macro pp_term = function + (* Whelp *) + | WInstance (_, term) -> "whelp instance " ^ pp_term term + | WHint (_, t) -> "whelp hint " ^ pp_term t + | WLocate (_, s) -> "whelp locate " ^ s + | WElim (_, t) -> "whelp elim " ^ pp_term t + | WMatch (_, term) -> "whelp match " ^ pp_term term + (* real macros *) +(* | Abort _ -> "Abort" *) + | Check (_, term) -> sprintf "Check %s" (pp_term term) + | Hint _ -> "hint" +(* | Redo (_, None) -> "Redo" + | Redo (_, Some n) -> sprintf "Redo %d" n *) + | Search_pat (_, kind, pat) -> + sprintf "search %s \"%s\"" (pp_search_kind kind) pat + | Search_term (_, kind, term) -> + sprintf "search %s %s" (pp_search_kind kind) (pp_term term) +(* | Undo (_, None) -> "Undo" + | Undo (_, Some n) -> sprintf "Undo %d" n *) + | Print (_, name) -> sprintf "Print \"%s\"" name + | Quit _ -> "Quit" + +let pp_macro_ast = pp_macro pp_term_ast +let pp_macro_cic = pp_macro pp_term_cic + +let pp_alias = function + | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"" id uri + | Symbol_alias (symb, instance, desc) -> + sprintf "alias symbol \"%s\" (instance %d) = \"%s\"" + symb instance desc + | Number_alias (instance,desc) -> + sprintf "alias num (instance %d) = \"%s\"" instance desc + +let pp_params = function + | [] -> "" + | params -> + " " ^ + String.concat " " + (List.map + (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term_ast typ)) + params) + +let pp_fields fields = + (if fields <> [] then "\n" else "") ^ + String.concat ";\n" + (List.map (fun (name,ty) -> " " ^ name ^ ": " ^ pp_term_ast ty) fields) + +let pp_obj = function + | Inductive (params, types) -> + let pp_constructors constructors = + String.concat "\n" + (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term_ast typ)) + constructors) + in + let pp_type (name, _, typ, constructors) = + sprintf "\nwith %s: %s \\def\n%s" name (pp_term_ast typ) + (pp_constructors constructors) + in + (match types with + | [] -> assert false + | (name, inductive, typ, constructors) :: tl -> + let fst_typ_pp = + sprintf "%sinductive %s%s: %s \\def\n%s" + (if inductive then "" else "co") name (pp_params params) + (pp_term_ast typ) (pp_constructors constructors) + in + fst_typ_pp ^ String.concat "" (List.map pp_type tl)) + | Theorem (flavour, name, typ, body) -> + sprintf "%s %s: %s %s" + (pp_flavour flavour) + name + (pp_term_ast typ) + (match body with + | None -> "" + | Some body -> "\\def " ^ pp_term_ast body) + | Record (params,name,ty,fields) -> + "record " ^ name ^ " " ^ pp_params params ^ " \\def {" ^ + pp_fields fields ^ "}" + +let pp_command = function + | Include (_,path) -> "include " ^ path + | Qed _ -> "qed" + | Drop _ -> "drop" + | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value + | Coercion (_,term) -> sprintf "coercion %s" (pp_term_ast term) + | Alias (_,s) -> pp_alias s + | Obj (_,obj) -> pp_obj obj + | Default (_,what,uris) -> + sprintf "default \"%s\" %s" what + (String.concat " " (List.map UriManager.string_of_uri uris)) + +let rec pp_tactical = function + | Tactic (_, tac) -> pp_tactic tac + | Do (_, count, tac) -> sprintf "do %d %s" count (pp_tactical tac) + | Repeat (_, tac) -> "repeat " ^ pp_tactical tac + | Seq (_, tacs) -> pp_tacticals ~sep:"; " tacs + | Then (_, tac, tacs) -> + sprintf "%s; [%s]" (pp_tactical tac) (pp_tacticals ~sep:" | " tacs) + | First (_, tacs) -> sprintf "tries [%s]" (pp_tacticals ~sep:" | " tacs) + | Try (_, tac) -> "try " ^ pp_tactical tac + | Solve (_, tac) -> sprintf "solve [%s]" (pp_tacticals ~sep:" | " tac) + +and pp_tacticals ~sep tacs = + String.concat sep (List.map pp_tactical tacs) + +let pp_tactical tac = pp_tactical tac ^ tactical_terminator +let pp_tactic tac = pp_tactic tac ^ tactic_terminator +let pp_command tac = pp_command tac ^ command_terminator + +let pp_executable = function + | Macro (_,x) -> pp_macro_ast x + | Tactical (_,x) -> pp_tactical x + | Command (_,x) -> pp_command x + +let pp_comment = function + | Note (_,str) -> sprintf "(* %s *)" str + | Code (_,code) -> sprintf "(** %s. **)" (pp_executable code) + +let pp_statement = function + | Executable (_, ex) -> pp_executable ex + | Comment (_, c) -> pp_comment c + +let pp_cic_command = function + | Include (_,path) -> "include " ^ path + | Qed _ -> "qed" + | Drop _ -> "drop" + | Coercion (_,term) -> sprintf "coercion %s" (CicPp.ppterm term) + | Set (_, _, _) + | Alias (_,_) + | Default (_,_,_) + | Obj (_,_) -> assert false (* not implemented *) diff --git a/helm/ocaml/cic_notation/grafiteAstPp.mli b/helm/ocaml/cic_notation/grafiteAstPp.mli new file mode 100644 index 000000000..9268ea25b --- /dev/null +++ b/helm/ocaml/cic_notation/grafiteAstPp.mli @@ -0,0 +1,39 @@ +(* 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_tactic: (CicNotationPt.term, string) GrafiteAst.tactic -> string +val pp_obj: GrafiteAst.obj -> string +val pp_command: (CicNotationPt.term,GrafiteAst.obj) GrafiteAst.command -> string +val pp_macro: ('a -> string) -> 'a GrafiteAst.macro -> string +val pp_comment: (CicNotationPt.term,GrafiteAst.obj,string) GrafiteAst.comment -> string +val pp_executable: (CicNotationPt.term,GrafiteAst.obj,string) GrafiteAst.code -> string +val pp_statement: (CicNotationPt.term,GrafiteAst.obj,string) GrafiteAst.statement -> string +val pp_macro_ast: CicNotationPt.term GrafiteAst.macro -> string +val pp_macro_cic: Cic.term GrafiteAst.macro -> string +val pp_tactical: (CicNotationPt.term, string) GrafiteAst.tactical -> string +val pp_alias: GrafiteAst.alias_spec -> string + +val pp_cic_command: (Cic.term,Cic.obj) GrafiteAst.command -> string + diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml index 41c3fd054..8bd5cc04e 100644 --- a/helm/ocaml/cic_notation/grafiteParser.ml +++ b/helm/ocaml/cic_notation/grafiteParser.ml @@ -29,10 +29,9 @@ let grammar = CicNotationParser.level2_ast_grammar let term = CicNotationParser.term let statement = Grammar.Entry.create grammar "statement" -let statements = Grammar.Entry.create grammar "statements" EXTEND - GLOBAL: term statement statements; + GLOBAL: term statement; arg: [ [ LPAREN; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":"; ty = term; RPAREN -> names,ty @@ -338,10 +337,10 @@ EXTEND ] ]; argument: [ - [ id = IDENT -> GrafiteAst.IdentArg (0, id) + [ id = IDENT -> CicNotationPt.IdentArg (0, id) | l = LIST1 [ SYMBOL <:unicode> (* η *) -> () ] SEP SYMBOL "."; SYMBOL "."; id = IDENT -> - GrafiteAst.IdentArg (List.length l, id) + CicNotationPt.IdentArg (List.length l, id) ] ]; associativity: [ @@ -367,13 +366,14 @@ EXTEND ] ]; level3_term: [ - [ u = URI -> GrafiteAst.UriPattern (UriManager.uri_of_string u) - | id = IDENT -> GrafiteAst.VarPattern id + [ u = URI -> CicNotationPt.UriPattern (UriManager.uri_of_string u) + | id = IDENT -> CicNotationPt.VarPattern id + | SYMBOL "_" -> CicNotationPt.ImplicitPattern | LPAREN; terms = LIST1 SELF; RPAREN -> (match terms with | [] -> assert false | [term] -> term - | terms -> GrafiteAst.ApplPattern terms) + | terms -> CicNotationPt.ApplPattern terms) ] ]; interpretation: [ @@ -435,11 +435,13 @@ EXTEND GrafiteAst.Default (loc,what,uris) | IDENT "notation"; (l1, assoc, prec, l2) = notation -> GrafiteAst.Notation (loc, l1, assoc, prec, l2) - | IDENT "interpretation"; (symbol, args, l3) = interpretation -> - GrafiteAst.Interpretation (loc, (symbol, args), l3) + | IDENT "interpretation"; id = QSTRING; + (symbol, args, l3) = interpretation -> + GrafiteAst.Interpretation (loc, id, (symbol, args), l3) | IDENT "dump" -> GrafiteAst.Dump loc - | IDENT "render"; u = URI -> GrafiteAst.Render (loc, UriManager.uri_of_string u) + | IDENT "render"; u = URI -> + GrafiteAst.Render (loc, UriManager.uri_of_string u) ]]; executable: [ [ cmd = command; SYMBOL "." -> GrafiteAst.Command (loc, cmd) @@ -457,18 +459,16 @@ EXTEND statement: [ [ ex = executable -> GrafiteAst.Executable (loc,ex) | com = comment -> GrafiteAst.Comment (loc, com) + | EOI -> raise End_of_file ] ]; - statements: [ - [ l = LIST0 statement ; EOI -> l - ] - ]; END let exc_located_wrapper f = try f () with + | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file | Stdpp.Exc_located (floc, Stream.Error msg) -> raise (CicNotationParser.Parse_error (floc, msg)) | Stdpp.Exc_located (floc, exn) -> @@ -476,6 +476,4 @@ let exc_located_wrapper f = let parse_statement stream = exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream)) -let parse_statements stream = - exc_located_wrapper (fun () -> (Grammar.Entry.parse statements stream)) diff --git a/helm/ocaml/cic_notation/grafiteParser.mli b/helm/ocaml/cic_notation/grafiteParser.mli index e769a5bfb..ccea04836 100644 --- a/helm/ocaml/cic_notation/grafiteParser.mli +++ b/helm/ocaml/cic_notation/grafiteParser.mli @@ -23,10 +23,8 @@ * http://helm.cs.unibo.it/ *) + (** @raise End_of_file *) val parse_statement: - char Stream.t -> (CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement - -val parse_statements: char Stream.t -> - (CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement list + (CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index 22d5c09ff..df94eaa6f 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -91,10 +91,10 @@ let process_stream ?(ignore_exn = false) istream = "extending pretty printer took %f)\n") (time2 -. time1) (time4 -. time3); flush stdout - | G.Executable (_, G.Command (_, G.Interpretation (_, l2, l3))) -> + | G.Executable (_, G.Command (_, G.Interpretation (_, id, l2, l3))) -> prerr_endline "Adding interpretation ..."; flush stdout; let time1 = Unix.gettimeofday () in - ignore (CicNotationRew.add_interpretation l2 l3); + ignore (CicNotationRew.add_interpretation id l2 l3); let time2 = Unix.gettimeofday () in printf "done (patterns compilation took %f seconds)\n" (time2 -. time1); diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml index 70036146e..76be244ad 100644 --- a/helm/ocaml/cic_transformations/acic2Ast.ml +++ b/helm/ocaml/cic_transformations/acic2Ast.ml @@ -83,8 +83,7 @@ let ast_of_acic ids_to_inner_sorts acic = | `Prop | `CProp -> `Forall in idref id (Ast.Binder (binder_kind, (n, Some (aux s)), aux t)) - | Cic.ACast (id,v,t) -> - idref id (Ast.Appl [idref id (Ast.Symbol ("cast", 0)); aux v; aux t]) + | Cic.ACast (id,v,t) -> idref id (Ast.Cast (aux v, aux t)) | Cic.ALambda (id,n,s,t) -> idref id (Ast.Binder (`Lambda, (n, Some (aux s)), aux t)) | Cic.ALetIn (id,n,s,t) -> idref id (Ast.LetIn ((n, None), aux s, aux t)) diff --git a/helm/ocaml/cic_transformations/cicAst.ml b/helm/ocaml/cic_transformations/cicAst.ml index 3f14ebf73..45fcc8820 100644 --- a/helm/ocaml/cic_transformations/cicAst.ml +++ b/helm/ocaml/cic_transformations/cicAst.ml @@ -65,6 +65,7 @@ type term = | Appl of term list | Binder of binder_kind * capture_variable * term | Case of term * string option * term option * (case_pattern * term) list + | Cast of term * term | LetIn of capture_variable * term * term | LetRec of induction_kind * (capture_variable * term * int) list * term | Ident of string * subst list option diff --git a/helm/ocaml/cic_transformations/cicAst.mli b/helm/ocaml/cic_transformations/cicAst.mli index 7815a1765..97cda2e47 100644 --- a/helm/ocaml/cic_transformations/cicAst.mli +++ b/helm/ocaml/cic_transformations/cicAst.mli @@ -55,6 +55,7 @@ type term = | Binder of binder_kind * capture_variable * term (* kind, name, body *) | Case of term * string option * term option * (case_pattern * term) list (* what to match, inductive type, out type, list *) + | Cast of term * term | LetIn of capture_variable * term * term (* name, body, where *) | LetRec of induction_kind * (capture_variable * term * int) list * term (* (name, body, decreasing argument) list, where *)