-(* Copyright (C) 2000, HELM Team.
+/* Copyright (C) 2000, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
*
* For details, see the HELM World-Wide-Web page,
* http://cs.unibo.it/helm/.
- *)
+ */
%{
open Cic;;
exception InvalidSuffix of string;;
exception InductiveTypeURIExpected;;
+ exception UnknownIdentifier of string;;
let uri_of_id_map = Hashtbl.create 53;;
let rec aux i =
function
[] -> raise Not_found
- | he::_ when he = e -> i
+ | (Some he)::_ when he = e -> i
| _::tl -> aux (i+1) tl
in
aux 1
let get_cookingno uri =
UriManager.relative_depth !CicTextualParser0.current_uri uri 0
;;
-
+
+ (* Returns the first meta whose number is above the *)
+ (* number of the higher meta. *)
+ (*CSC: cut&pasted from proofEngine.ml *)
+ let new_meta () =
+ let rec aux =
+ function
+ None,[] -> 1
+ | Some n,[] -> n
+ | None,(n,_,_)::tl -> aux (Some n,tl)
+ | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
+ in
+ 1 + aux (None,!CicTextualParser0.metasenv)
+ ;;
+
+ (* identity_relocation_list_for_metavariable i canonical_context *)
+ (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
+ (* where n = List.length [canonical_context] *)
+ (*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
+ (*CSC: cut&pasted from proofEngine.ml *)
+ let identity_relocation_list_for_metavariable canonical_context =
+ let canonical_context_length = List.length canonical_context in
+ let rec aux =
+ function
+ (_,[]) -> []
+ | (n,None::tl) -> None::(aux ((n+1),tl))
+ | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
+ in
+ aux (1,canonical_context)
+ ;;
+
%}
%token <string> ID
%token <int> META
%token <UriManager.uri * int> INDTYURI
%token <UriManager.uri * int * int> INDCONURI
%token ALIAS
-%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT
-%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW EOF
+%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT NONE
+%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
+%right ARROW
%start main
%type <Cic.term option> main
%%
| alias { None }
| EOF { raise CicTextualParser0.Eof }
;
-expr:
+expr2:
CONURI
{ let uri = UriManager.string_of_uri $1 in
let suff = (String.sub uri (String.length uri - 3) 3) in
Rel (get_index_in_list (Name $1) !CicTextualParser0.binders)
with
Not_found ->
- Hashtbl.find uri_of_id_map $1
+ try
+ Hashtbl.find uri_of_id_map $1
+ with
+ Not_found ->
+ match ! CicTextualParser0.locate_object $1 with
+ | None -> raise (UnknownIdentifier $1)
+ | Some term -> Hashtbl.add uri_of_id_map $1 term; term
}
| CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
{ let cookingno = get_cookingno (fst $5) in
done ;
CoFix (idx,cofixfuns)
}
- | IMPLICIT { Implicit }
+ | IMPLICIT
+ { let newmeta = new_meta () in
+ let new_canonical_context = [] in
+ let irl =
+ identity_relocation_list_for_metavariable new_canonical_context
+ in
+ CicTextualParser0.metasenv :=
+ [newmeta, new_canonical_context, Sort Type ;
+ newmeta+1, new_canonical_context, Meta (newmeta,irl);
+ newmeta+2, new_canonical_context, Meta (newmeta+1,irl)
+ ] @ !CicTextualParser0.metasenv ;
+ Meta (newmeta+2,irl)
+ }
| SET { Sort Set }
| PROP { Sort Prop }
| TYPE { Sort Type }
| LPAREN expr CAST expr RPAREN { Cast ($2,$4) }
- | META { Meta $1 }
+ | META LBRACKET substitutionlist RBRACKET { Meta ($1, $3) }
| LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) }
- | pihead expr
+;
+expr :
+ pihead expr
{ CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
Prod (fst $1, snd $1,$2) }
- | lambdahead expr
+ | lambdahead expr
{ CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
Lambda (fst $1, snd $1,$2) }
- | letinhead expr
+ | letinhead expr
{ CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
LetIn (fst $1, snd $1,$2) }
+ | expr2
+ { $1 }
;
fixheader:
FIX ID LCURLY fixfunsdecl RCURLY
- { let bs = List.rev_map (function (name,_,_) -> Name name) $4 in
+ { let bs = List.rev_map (function (name,_,_) -> Some (Name name)) $4 in
CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
$2,$4
}
;
cofixheader:
COFIX ID LCURLY cofixfunsdecl RCURLY
- { let bs = List.rev_map (function (name,_) -> Name name) $4 in
+ { let bs = List.rev_map (function (name,_) -> Some (Name name)) $4 in
CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
$2,$4
}
;
pihead:
PROD ID COLON expr DOT
- { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ;
+ { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
(Cic.Name $2, $4) }
- | expr ARROW
- { CicTextualParser0.binders := Anonimous::!CicTextualParser0.binders ;
+ | expr2 ARROW
+ { CicTextualParser0.binders := (Some Anonimous)::!CicTextualParser0.binders ;
(Anonimous, $1) }
| LPAREN expr RPAREN ARROW
- { CicTextualParser0.binders := Anonimous::!CicTextualParser0.binders ;
+ { CicTextualParser0.binders := (Some Anonimous)::!CicTextualParser0.binders ;
(Anonimous, $2) }
;
lambdahead:
LAMBDA ID COLON expr DOT
- { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ;
+ { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
(Cic.Name $2, $4) }
;
letinhead:
LAMBDA ID LETIN expr DOT
- { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ;
+ { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
(Cic.Name $2, $4) }
;
branches:
expr { [$1] }
| expr SEMICOLON exprseplist { $1::$3 }
;
+substitutionlist:
+ { [] }
+ | expr SEMICOLON substitutionlist { (Some $1)::$3 }
+ | NONE SEMICOLON substitutionlist { None::$3 }
+;
alias:
ALIAS ID CONURI
{ let cookingno = get_cookingno $3 in
Hashtbl.add uri_of_id_map $2
(Cic.MutConstruct (uri, cookingno, indno ,consno))
}
+
+
+
projects / helm.git / blobdiff