From 296b163c8a2b09a6f87cbab15c2016de92fc8e70 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 2 Dec 2003 17:11:10 +0000 Subject: [PATCH] sort CProp added --- helm/Makefile | 3 +- helm/gTopLevel/.depend | 11 +++++--- helm/gTopLevel/Makefile | 10 +------ helm/gTopLevel/gTopLevel.ml | 4 +-- helm/gTopLevel/termViewer.ml | 4 ++- helm/ocaml/cic/cic.ml | 1 + helm/ocaml/cic_omdoc/cic2acic.ml | 9 +++--- helm/ocaml/cic_omdoc/doubleTypeInference.ml | 2 +- helm/ocaml/cic_proof_checking/cicPp.ml | 7 +++-- .../cic_proof_checking/cicTypeChecker.ml | 18 ++++++++---- .../cic_textual_parser/cicTextualLexer.mll | 1 + .../cic_textual_parser/cicTextualParser.mly | 9 +++--- helm/ocaml/cic_transformations/cic2Xml.ml | 7 +++-- .../content_expressions.ml | 7 +++-- helm/ocaml/cic_unification/cicRefine.ml | 2 +- .../ocaml/mathql_generator/cGSearchPattern.ml | 1 + helm/ocaml/mathql_generator/mQGTypes.ml | 1 + helm/ocaml/mathql_generator/mQGUtil.ml | 28 +++++++++++-------- .../ocaml/mathql_interpreter/mQueryTLexer.mll | 1 + helm/ocaml/tactics/equalityTactics.ml | 1 + helm/ocaml/tactics/primitiveTactics.ml | 1 + helm/ocaml/tactics/proofEngineHelpers.ml | 1 + .../texCicTextualLexer.mll | 1 + .../texCicTextualParser.mly | 9 +++--- 24 files changed, 81 insertions(+), 58 deletions(-) diff --git a/helm/Makefile b/helm/Makefile index 0b925d515..721a89621 100644 --- a/helm/Makefile +++ b/helm/Makefile @@ -1,5 +1,4 @@ -DIRS = ocaml gTopLevel searchEngine mathql_test -# hbugs +DIRS = ocaml hbugs gTopLevel searchEngine mathql_test DIRS_BYTE = $(patsubst %,%.byte,$(DIRS)) DIRS_OPT = $(patsubst %,%.opt,$(DIRS)) diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index 6da67a4a5..e7f7c2d1d 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -1,6 +1,7 @@ termEditor.cmi: disambiguate.cmi texTermEditor.cmi: disambiguate.cmi invokeTactics.cmi: termEditor.cmi termViewer.cmi +hbugs.cmi: invokeTactics.cmi proofEngine.cmo: proofEngine.cmi proofEngine.cmx: proofEngine.cmi logicalOperations.cmo: proofEngine.cmi logicalOperations.cmi @@ -19,7 +20,9 @@ invokeTactics.cmo: logicalOperations.cmi proofEngine.cmi termEditor.cmi \ termViewer.cmi invokeTactics.cmi invokeTactics.cmx: logicalOperations.cmx proofEngine.cmx termEditor.cmx \ termViewer.cmx invokeTactics.cmi -gTopLevel.cmo: invokeTactics.cmi logicalOperations.cmi proofEngine.cmi \ - termEditor.cmi termViewer.cmi texTermEditor.cmi -gTopLevel.cmx: invokeTactics.cmx logicalOperations.cmx proofEngine.cmx \ - termEditor.cmx termViewer.cmx texTermEditor.cmx +hbugs.cmo: invokeTactics.cmi proofEngine.cmi hbugs.cmi +hbugs.cmx: invokeTactics.cmx proofEngine.cmx hbugs.cmi +gTopLevel.cmo: hbugs.cmi invokeTactics.cmi logicalOperations.cmi \ + proofEngine.cmi termEditor.cmi termViewer.cmi texTermEditor.cmi +gTopLevel.cmx: hbugs.cmx invokeTactics.cmx logicalOperations.cmx \ + proofEngine.cmx termEditor.cmx termViewer.cmx texTermEditor.cmx diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index 9c9aaea62..7ce96c052 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -2,7 +2,7 @@ BIN_DIR = /usr/local/bin REQUIRES = lablgtkmathview helm-cic_textual_parser helm-tex_cic_textual_parser \ helm-cic_proof_checking helm-xml gdome2-xslt helm-cic_unification \ helm-mathql helm-mathql_interpreter helm-mathql_generator \ - helm-tactics threads hbugs-client mathml-editor \ + helm-tactics threads hbugs-client mathml-editor \ helm-cic_transformations PREDICATES = "gnome,init,glade" OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o @@ -77,11 +77,3 @@ uninstall: ifneq ($(MAKECMDGOALS), depend) include .depend endif - - - - - - - - diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 88d819fde..8aec9d350 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -672,7 +672,7 @@ module InvokeTacticsCallbacks = end ;; module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);; - +(* (* Just to initialize the Hbugs module *) module Ignore = Hbugs.Initialize (InvokeTactics');; Hbugs.set_describe_hint_callback (fun hint -> @@ -682,7 +682,7 @@ Hbugs.set_describe_hint_callback (fun hint -> check_window outputhtml [term] | _ -> ()) ;; - +*) let dummy_uri = "/dummy.con" (** load an unfinished proof from filesystem *) diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml index b782237d0..e105d5f0e 100644 --- a/helm/gTopLevel/termViewer.ml +++ b/helm/gTopLevel/termViewer.ml @@ -113,8 +113,10 @@ class sequent_viewer obj = ApplyStylesheets.mml_of_cic_sequent metasenv sequent in self#load_doc ~dom:sequent_mml ; +(* Misc.domImpl#saveDocumentToFile ~name:"/tmp/pippo" ~doc:sequent_mml () ; - current_infos <- +*) + current_infos <- Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses) end ;; diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml index 6d58e6164..cb2af219b 100644 --- a/helm/ocaml/cic/cic.ml +++ b/helm/ocaml/cic/cic.ml @@ -51,6 +51,7 @@ and sort = Prop | Set | Type + | CProp and name = Name of string | Anonymous diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml index d934e83bf..aa0183dad 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.ml +++ b/helm/ocaml/cic_omdoc/cic2acic.ml @@ -100,10 +100,11 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts (*CSC: computed again and again. *) let string_of_sort t = match CicReduction.whd context t with - C.Sort C.Prop -> "Prop" - | C.Sort C.Set -> "Set" - | C.Sort C.Type -> "Type" - | _ -> assert false + C.Sort C.Prop -> "Prop" + | C.Sort C.Set -> "Set" + | C.Sort C.Type -> "Type" + | C.Sort C.CProp -> "CProp" + | _ -> assert false in let ainnertypes,innertype,innersort,expected_available = (*CSC: Here we need the algorithm for Coscoy's double type-inference *) diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml index 03227ef9b..f51c00c74 100644 --- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml +++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml @@ -647,7 +647,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in match (t1', t2') with (C.Sort s1, C.Sort s2) - when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *) + when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *) C.Sort s2 | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *) | (_,_) -> diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml index 11ed4418c..a8d9eaa0b 100644 --- a/helm/ocaml/cic_proof_checking/cicPp.ml +++ b/helm/ocaml/cic_proof_checking/cicPp.ml @@ -83,9 +83,10 @@ let rec pp t l = "]" | C.Sort s -> (match s with - C.Prop -> "Prop" - | C.Set -> "Set" - | C.Type -> "Type" + C.Prop -> "Prop" + | C.Set -> "Set" + | C.Type -> "Type" + | C.CProp -> "CProp" ) | C.Implicit -> "?" | C.Prod (b,s,t) -> diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 62dc951aa..7521f0f90 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -1185,6 +1185,7 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2 | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true | (C.Sort C.Prop, C.Sort C.Set) + | (C.Sort C.Prop, C.Sort C.CProp) | (C.Sort C.Prop, C.Sort C.Type) when need_dummy -> (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *) (match CicEnvironment.get_obj uri with @@ -1198,8 +1199,13 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))) ) | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true + | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true - | (C.Sort C.Set, C.Sort C.Type) when need_dummy -> + | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true + | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true + | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true + | ((C.Sort C.Set, C.Sort C.Type) | (C.Sort C.CProp, C.Sort C.Type)) + when need_dummy -> (match CicEnvironment.get_obj uri with C.InductiveDefinition (itl,_,paramsno) -> let tys = @@ -1220,7 +1226,7 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = res && (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with C.Sort C.Prop -> true - | C.Sort C.Set -> + | (C.Sort C.Set | C.Sort C.CProp) -> (match CicEnvironment.get_obj uri with C.InductiveDefinition (itl,_,_) -> let (_,_,_,cl) = List.nth itl i in @@ -1233,13 +1239,15 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = ) | _ -> false ) - | (C.Sort C.Set, C.Prod (name,so,ta)) when not need_dummy -> + | ((C.Sort C.Set, C.Prod (name,so,ta)) | (C.Sort C.CProp, C.Prod (name,so,ta))) + when not need_dummy -> let res = CicReduction.are_convertible context so ind in res && (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with C.Sort C.Prop | C.Sort C.Set -> true + | C.Sort C.CProp -> true | C.Sort C.Type -> (match CicEnvironment.get_obj uri with C.InductiveDefinition (itl,_,paramsno) -> @@ -1647,7 +1655,7 @@ in if not res then prerr_endline ("#### " ^ CicPp.ppterm (type_of_aux context p) let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in match (t1', t2') with (C.Sort s1, C.Sort s2) - when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *) + when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *) C.Sort s2 | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *) | (_,_) -> @@ -1728,7 +1736,7 @@ and is_small context paramsno c = C.Prod (n,so,de) -> (*CSC: [] is an empty metasenv. Is it correct? *) let s = type_of_aux' [] context so in - (s = C.Sort C.Prop || s = C.Sort C.Set) && + (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) && is_small_aux ((Some (n,(C.Decl so)))::context) de | _ -> true (*CSC: we trust the type-checker *) in diff --git a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll index 6db492ee1..613645bc4 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll +++ b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll @@ -74,6 +74,7 @@ rule token = | "Set" { SET } | "Prop" { PROP } | "Type" { TYPE } + | "CProp" { CPROP } | ident { ID (L.lexeme lexbuf) } | conuri { CONURI (U.uri_of_string ("cic:" ^ L.lexeme lexbuf)) } | varuri { VARURI (U.uri_of_string ("cic:" ^ L.lexeme lexbuf)) } diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly index 08d85a595..84e0f0ee5 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly +++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly @@ -155,7 +155,7 @@ %token VARURI %token INDTYURI %token INDCONURI -%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT NONE +%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CPROP CAST IMPLICIT NONE %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF %right ARROW %start main @@ -286,9 +286,10 @@ expr2: } | IMPLICIT { mk_implicit () } - | SET { [], function _ -> Sort Set } - | PROP { [], function _ -> Sort Prop } - | TYPE { [], function _ -> Sort Type } + | SET { [], function _ -> Sort Set } + | PROP { [], function _ -> Sort Prop } + | TYPE { [], function _ -> Sort Type } + | CPROP { [], function _ -> Sort CProp } | LPAREN expr CAST expr RPAREN { let dom1,mk_expr1 = $2 in let dom2,mk_expr2 = $4 in diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml index d945cc82f..7594ffef1 100644 --- a/helm/ocaml/cic_transformations/cic2Xml.ml +++ b/helm/ocaml/cic_transformations/cic2Xml.ml @@ -72,9 +72,10 @@ let print_term ~ids_to_inner_sorts = | C.ASort (id,s) -> let string_of_sort = function - C.Prop -> "Prop" - | C.Set -> "Set" - | C.Type -> "Type" + C.Prop -> "Prop" + | C.Set -> "Set" + | C.Type -> "Type" + | C.CProp -> "CProp" in X.xml_empty "SORT" [None,"value",(string_of_sort s) ; None,"id",id] | C.AImplicit _ -> raise NotImplemented diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml index 2ff989da1..b913bf0de 100644 --- a/helm/ocaml/cic_transformations/content_expressions.ml +++ b/helm/ocaml/cic_transformations/content_expressions.ml @@ -303,9 +303,10 @@ Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rdiv.con" let string_of_sort = function - Cic.Prop -> "Prop" - | Cic.Set -> "Set" - | Cic.Type -> "Type" + Cic.Prop -> "Prop" + | Cic.Set -> "Set" + | Cic.Type -> "Type" + | Cic.CProp -> "Type" ;; let get_constructors uri i = diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 881c72bfd..ba79ce922 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -290,7 +290,7 @@ and type_of_aux' metasenv context t = let t2'' = CicReduction.whd ((Some (name,C.Decl s))::context) t2' in match (t1'', t2'') with (C.Sort s1, C.Sort s2) - when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *) + when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *) C.Sort s2,subst',metasenv' | (C.Sort s1, C.Sort s2) -> (*CSC manca la gestione degli universi!!! *) diff --git a/helm/ocaml/mathql_generator/cGSearchPattern.ml b/helm/ocaml/mathql_generator/cGSearchPattern.ml index 77f3b488c..a56d65959 100644 --- a/helm/ocaml/mathql_generator/cGSearchPattern.ml +++ b/helm/ocaml/mathql_generator/cGSearchPattern.ml @@ -96,6 +96,7 @@ let get_constraints term = Cic.Prop -> T.Prop | Cic.Set -> T.Set | Cic.Type -> T.Type + | Cic.CProp -> T.CProp in [],[],[!!kind,s'] | _ -> [],[],[]) diff --git a/helm/ocaml/mathql_generator/mQGTypes.ml b/helm/ocaml/mathql_generator/mQGTypes.ml index 2dacfe14c..a210aa68f 100644 --- a/helm/ocaml/mathql_generator/mQGTypes.ml +++ b/helm/ocaml/mathql_generator/mQGTypes.ml @@ -39,6 +39,7 @@ type depth = int type sort = Set | Prop | Type + | CProp type spec = MustObj of uri list * position list * depth list | MustSort of sort list * position list * depth list diff --git a/helm/ocaml/mathql_generator/mQGUtil.ml b/helm/ocaml/mathql_generator/mQGUtil.ml index 36dd0653c..e30742649 100644 --- a/helm/ocaml/mathql_generator/mQGUtil.ml +++ b/helm/ocaml/mathql_generator/mQGUtil.ml @@ -40,9 +40,10 @@ let string_of_position p = | T.InBody -> ns ^ "InBody" let string_of_sort = function - | T.Set -> "Set" - | T.Prop -> "Prop" - | T.Type -> "Type" + | T.Set -> "Set" + | T.Prop -> "Prop" + | T.Type -> "Type" + | T.CProp -> "CProp" let string_of_depth = string_of_int @@ -54,9 +55,10 @@ let mathql_of_position = function | T.InBody -> "$IB" let mathql_of_sort = function - | T.Set -> "$SET" - | T.Prop -> "$PROP" - | T.Type -> "$TYPE" + | T.Set -> "$SET" + | T.Prop -> "$PROP" + | T.Type -> "$TYPE" + | T.CProp -> "$CPROP" let mathql_of_depth = string_of_int @@ -92,9 +94,10 @@ let position_of_mathql = function | _ -> raise Parsing.Parse_error let sort_of_mathql = function - | "$SET" -> T.Set - | "$PROP" -> T.Prop - | "$TYPE" -> T.Type + | "$SET" -> T.Set + | "$PROP" -> T.Prop + | "$TYPE" -> T.Type + | "$CPROP" -> T.CProp | _ -> raise Parsing.Parse_error let depth_of_mathql s = @@ -120,9 +123,10 @@ let text_of_depth pos no_depth_text = match pos with | _ -> no_depth_text let text_of_sort = function - | T.Set -> "Set" - | T.Prop -> "Prop" - | T.Type -> "Type" + | T.Set -> "Set" + | T.Prop -> "Prop" + | T.Type -> "Type" + | T.CProp -> "CProp" let is_main_position = function | `MainHypothesis _ diff --git a/helm/ocaml/mathql_interpreter/mQueryTLexer.mll b/helm/ocaml/mathql_interpreter/mQueryTLexer.mll index abccb4626..ca51751f0 100644 --- a/helm/ocaml/mathql_interpreter/mQueryTLexer.mll +++ b/helm/ocaml/mathql_interpreter/mQueryTLexer.mll @@ -123,6 +123,7 @@ and result_token = parse | SPC { result_token lexbuf } | "(*" { comm_token lexbuf; result_token lexbuf } | '"' { STR (qstr string_token lexbuf) } + | '/' { out "SL"; SL } | '{' { LC } | '}' { RC } | ',' { CM } diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index 1c2a7d37f..a66328220 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -164,6 +164,7 @@ let replace_tac ~what ~with_what ~status:((proof, goal) as status) = match CicTypeChecker.type_of_aux' metasenv context wty with C.Sort C.Set -> "cic:/Coq/Init/Logic/eq.ind" | C.Sort C.Type + | C.Sort C.CProp | C.Sort C.Prop -> "cic:/Coq/Init/Logic_Type/eqT.ind" | _ -> assert false in diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index 8dfdd66c4..b060e009e 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -420,6 +420,7 @@ let elim_tac ~term ~status:(proof, goal) = match T.type_of_aux' metasenv context ty with C.Sort C.Prop -> "_ind" | C.Sort C.Set -> "_rec" + | C.Sort C.CProp -> "_rec" | C.Sort C.Type -> "_rect" | _ -> assert false in diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index ac5850ca2..79304211d 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -36,6 +36,7 @@ let mk_fresh_name context name ~typ = (try (match CicTypeChecker.type_of_aux' [] context typ with C.Sort C.Prop -> "H" + | C.Sort C.CProp -> "H" | C.Sort C.Set -> "x" | _ -> "H" ) diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll index f6eda1ac8..5ab17fa80 100644 --- a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll +++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll @@ -81,6 +81,7 @@ rule token = | "\\Set" { SET } | "\\Prop" { PROP } | "\\Type" { TYPE } + | "\\CProp" { CPROP } | ident { ID (unquote (L.lexeme lexbuf)) } | conuri { CONURI (U.uri_of_string ("cic:" ^ (unquote (L.lexeme lexbuf)))) } diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly index 500565823..f6f557947 100644 --- a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly +++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly @@ -156,7 +156,7 @@ %token VARURI %token INDTYURI %token INDCONURI -%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT NONE +%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CPROP CAST IMPLICIT NONE %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF %token DOLLAR %token RPLUS RMINUS RTIMES RDIV @@ -473,9 +473,10 @@ expr2: } | IMPLICIT { mk_implicit () } - | SET { [], function _ -> Sort Set } - | PROP { [], function _ -> Sort Prop } - | TYPE { [], function _ -> Sort Type } + | SET { [], function _ -> Sort Set } + | PROP { [], function _ -> Sort Prop } + | TYPE { [], function _ -> Sort Type } + | CPROP { [], function _ -> Sort CProp } | LPAREN expr CAST expr RPAREN { let dom1,mk_expr1 = $2 in let dom2,mk_expr2 = $4 in -- 2.39.2