X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fcic_textual_parser%2FcicTextualParser.mly;fp=helm%2Focaml%2Fcic_textual_parser%2FcicTextualParser.mly;h=0000000000000000000000000000000000000000;hp=08d85a595a2b03c358f07586ffdd4eb86ab5c30a;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
deleted file mode 100644
index 08d85a595..000000000
--- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly
+++ /dev/null
@@ -1,512 +0,0 @@
-/* Copyright (C) 2000, 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://cs.unibo.it/helm/.
- */
-
-%{
- open Cic;;
- module U = UriManager;;
-
- exception InvalidSuffix of string;;
- exception InductiveTypeURIExpected;;
- exception UnknownIdentifier of string;;
- exception ExplicitNamedSubstitutionAppliedToRel;;
- exception TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable;;
- 
- (* merge removing duplicates of two lists free of duplicates *)
- let union dom1 dom2 =
-  let rec filter =
-   function
-      [] -> []
-    | he::tl ->
-       if List.mem he dom1 then filter tl else he::(filter tl)
-  in
-   dom1 @ (filter dom2)
- ;;
-
- let get_index_in_list e =
-  let rec aux i =
-   function
-      [] -> raise Not_found
-    | (Some he)::_ when he = e -> i
-    | _::tl -> aux (i+1) tl
-  in
-   aux 1
- ;;
-
- (* 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)
- ;;
-
- let deoptionize_exp_named_subst =
-  function
-     None -> [], (function _ -> [])
-   | Some (dom,mk_exp_named_subst) -> dom,mk_exp_named_subst
- ;;
-
- let term_of_con_uri uri exp_named_subst =
-  Const (uri,exp_named_subst)
- ;;
-
- let term_of_var_uri uri exp_named_subst =
-  Var (uri,exp_named_subst)
- ;;
-
- let term_of_indty_uri (uri,tyno) exp_named_subst =
-  MutInd (uri, tyno, exp_named_subst)
- ;;
-
- let term_of_indcon_uri (uri,tyno,consno) exp_named_subst =
-  MutConstruct (uri, tyno, consno, exp_named_subst)
- ;;
-
- let term_of_uri uri =
-  match uri with
-     CicTextualParser0.ConUri uri ->
-      term_of_con_uri uri
-   | CicTextualParser0.VarUri uri ->
-      term_of_var_uri uri
-   | CicTextualParser0.IndTyUri (uri,tyno) ->
-      term_of_indty_uri (uri,tyno) 
-   | CicTextualParser0.IndConUri (uri,tyno,consno) ->
-      term_of_indcon_uri (uri,tyno,consno)
- ;;
-
- let var_uri_of_id id interp =
-  let module CTP0 = CicTextualParser0 in
-   match interp (CicTextualParser0.Id id) with
-      None -> raise (UnknownIdentifier id)
-    | Some (CTP0.Uri (CTP0.VarUri uri)) -> uri
-    | Some _ -> raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable
- ;;
-
- let indty_uri_of_id id interp =
-  let module CTP0 = CicTextualParser0 in
-   match interp (CicTextualParser0.Id id) with
-      None -> raise (UnknownIdentifier id)
-    | Some (CTP0.Uri (CTP0.IndTyUri (uri,tyno))) -> (uri,tyno)
-    | Some _ -> raise InductiveTypeURIExpected
- ;;
-
- let mk_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 ;
-     [], function _ -> Meta (newmeta+2,irl)
- ;;
-%}
-%token <string> ID
-%token <int> META
-%token <int> NUM
-%token <UriManager.uri> CONURI
-%token <UriManager.uri> VARURI
-%token <UriManager.uri * int> INDTYURI
-%token <UriManager.uri * int * int> INDCONURI
-%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 <CicTextualParser0.interpretation_domain_item list * (CicTextualParser0.interpretation -> Cic.term)> main
-%%
-main:
- | EOF { raise CicTextualParser0.Eof } /* FG: was never raised */
- | expr EOF { $1 }
- | expr SEMICOLON { $1 } /*  FG: to read several terms in a row
-                          *  Do we need to clear some static variables? 
-			  */
-;
-expr2:
-   CONURI exp_named_subst
-   { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
-      dom, function interp -> term_of_con_uri $1 (mk_exp_named_subst interp)
-   }
- | VARURI exp_named_subst
-   { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
-      dom, function interp -> term_of_var_uri $1 (mk_exp_named_subst interp)
-   }
- | INDTYURI exp_named_subst
-   { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
-      dom, function interp -> term_of_indty_uri $1 (mk_exp_named_subst interp)
-   }
- | INDCONURI exp_named_subst
-   { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
-      dom, function interp -> term_of_indcon_uri $1 (mk_exp_named_subst interp)
-   }
- | ID exp_named_subst
-   { try
-      let res =
-       Rel (get_index_in_list (Name $1) !CicTextualParser0.binders)
-      in
-       (match $2 with
-           None -> ([], function _ -> res)
-         | Some _ -> raise (ExplicitNamedSubstitutionAppliedToRel)
-       )
-     with
-      Not_found ->
-       let dom1,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
-        let dom = union dom1 [CicTextualParser0.Id $1] in
-         dom,
-          function interp ->
-           match interp (CicTextualParser0.Id $1) with
-	      None  -> raise (UnknownIdentifier $1)
-	    | Some (CicTextualParser0.Uri uri) ->
-               term_of_uri uri (mk_exp_named_subst interp)
-            | Some CicTextualParser0.Implicit ->
-               (*CSC: not very clean; to maximize code reusage *)
-               snd (mk_implicit ()) ""
-            | Some (CicTextualParser0.Term mk_term) ->
-               (mk_term interp)
-   }
- | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
-    { let dom1,mk_expr1 = $3 in
-      let dom2,mk_expr2 = $7 in
-      let dom3,mk_expr3 = $10 in
-       let dom = (union  dom1 (union dom2 dom3)) in
-        dom,
-        function interp ->
-         MutCase
-          (fst $5,snd $5,(mk_expr2 interp),(mk_expr1 interp),(mk_expr3 interp))
-    }
- | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY
-    { let dom1,mk_expr1 = $3 in
-      let dom2,mk_expr2 = $7 in
-      let dom3,mk_expr3 = $10 in
-       let dom = union [CicTextualParser0.Id $5] (union dom1 (union dom2 dom3)) in
-        dom,
-        function interp ->
-         let uri,typeno = indty_uri_of_id $5 interp in
-          MutCase
-           (uri,typeno,(mk_expr2 interp),(mk_expr1 interp),
-             (mk_expr3 interp))
-    }
- | fixheader LCURLY exprseplist RCURLY
-    { let dom1,foo,ids_and_indexes,mk_types = $1 in
-      let dom2,mk_exprseplist = $3 in
-       let dom = union dom1 dom2 in
-        for i = 1 to List.length ids_and_indexes do
-         CicTextualParser0.binders := List.tl !CicTextualParser0.binders
-        done ;
-        dom,
-         function interp ->
-          let types = mk_types interp in
-          let fixfunsbodies = (mk_exprseplist interp) in
-           let idx =
-            let rec find idx =
-             function
-                [] -> raise Not_found
-              | (name,_)::_  when name = foo -> idx
-              | _::tl -> find (idx+1) tl
-            in
-             find 0 ids_and_indexes
-           in
-            let fixfuns =
-             List.map2 (fun ((name,recindex),ty) bo -> (name,recindex,ty,bo))
-              (List.combine ids_and_indexes types) fixfunsbodies
-            in
-             Fix (idx,fixfuns)
-    }
- | cofixheader LCURLY exprseplist RCURLY
-    { let dom1,foo,ids,mk_types = $1 in
-      let dom2,mk_exprseplist = $3 in
-       let dom = union dom1 dom2 in
-        dom,
-         function interp ->
-          let types = mk_types interp in
-          let fixfunsbodies = (mk_exprseplist interp) in
-           let idx =
-            let rec find idx =
-             function
-                [] -> raise Not_found
-              | name::_  when name = foo -> idx
-              | _::tl -> find (idx+1) tl
-            in
-             find 0 ids
-           in
-            let fixfuns =
-             List.map2 (fun (name,ty) bo -> (name,ty,bo))
-              (List.combine ids types) fixfunsbodies
-            in
-             for i = 1 to List.length fixfuns do
-              CicTextualParser0.binders := List.tl !CicTextualParser0.binders
-             done ;
-             CoFix (idx,fixfuns)
-    }
- | IMPLICIT
-    { mk_implicit () }
- | SET  { [], function _ -> Sort Set }
- | PROP { [], function _ -> Sort Prop }
- | TYPE { [], function _ -> Sort Type }
- | LPAREN expr CAST expr RPAREN
-    { let dom1,mk_expr1 = $2 in
-      let dom2,mk_expr2 = $4 in
-       let dom = union dom1 dom2 in
-        dom, function interp -> Cast ((mk_expr1 interp),(mk_expr2 interp))
-    }
- | META LBRACKET substitutionlist RBRACKET
-    { let dom,mk_substitutionlist = $3 in
-       dom, function interp -> Meta ($1, mk_substitutionlist interp)
-    } 
- | LPAREN expr exprlist RPAREN
-    { let length,dom2,mk_exprlist = $3 in
-       match length with
-          0 -> $2
-        | _ ->
-          let dom1,mk_expr1 = $2 in
-           let dom = union dom1 dom2 in
-            dom,
-             function interp ->
-              Appl ((mk_expr1 interp)::(mk_exprlist interp))
-    }
-;
-exp_named_subst :
-    { None }
- | LCURLY named_substs RCURLY
-    { Some $2 }
-;
-named_substs :
-   VARURI LETIN expr2
-    { let dom,mk_expr = $3 in
-       dom, function interp -> [$1, mk_expr interp] }
- | ID LETIN expr2
-    { let dom1,mk_expr = $3 in
-       let dom = union [CicTextualParser0.Id $1] dom1 in
-        dom, function interp -> [var_uri_of_id $1 interp, mk_expr interp] }
- | VARURI LETIN expr2 SEMICOLON named_substs
-    { let dom1,mk_expr = $3 in
-      let dom2,mk_named_substs = $5 in
-       let dom = union dom1 dom2 in
-        dom, function interp -> ($1, mk_expr interp)::(mk_named_substs interp)
-    }
- | ID LETIN expr2 SEMICOLON named_substs
-    { let dom1,mk_expr = $3 in
-      let dom2,mk_named_substs = $5 in
-       let dom = union [CicTextualParser0.Id $1] (union dom1 dom2) in
-        dom,
-         function interp ->
-          (var_uri_of_id $1 interp, mk_expr interp)::(mk_named_substs interp)
-    }
-;
-expr :
-   pihead expr
-    { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
-      let dom1,mk_expr1 = snd $1 in
-      let dom2,mk_expr2 = $2 in
-       let dom = union dom1 dom2 in
-        dom, function interp -> Prod (fst $1, mk_expr1 interp, mk_expr2 interp)
-    }
- | lambdahead expr
-    { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
-      let dom1,mk_expr1 = snd $1 in
-      let dom2,mk_expr2 = $2 in
-       let dom = union dom1 dom2 in
-        dom,function interp -> Lambda (fst $1, mk_expr1 interp, mk_expr2 interp)
-    }
- | letinhead expr
-    { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
-      let dom1,mk_expr1 = snd $1 in
-      let dom2,mk_expr2 = $2 in
-       let dom = union dom1 dom2 in
-        dom, function interp -> LetIn (fst $1, mk_expr1 interp, mk_expr2 interp)
-    }
- | expr2
-    { $1 }
-;
-fixheader:
-   FIX ID LCURLY fixfunsdecl RCURLY
-    { let dom,ids_and_indexes,mk_types = $4 in
-       let bs =
-        List.rev_map (function (name,_) -> Some (Name name)) ids_and_indexes
-       in
-        CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
-        dom, $2, ids_and_indexes, mk_types
-    }
-;
-fixfunsdecl:
-   ID LPAREN NUM RPAREN COLON expr
-    { let dom,mk_expr = $6 in
-       dom, [$1,$3], function interp -> [mk_expr interp]
-    }
- | ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl
-    { let dom1,mk_expr = $6 in
-      let dom2,ids_and_indexes,mk_types = $8 in
-       let dom = union dom1 dom2 in
-        dom, ($1,$3)::ids_and_indexes,
-         function interp -> (mk_expr interp)::(mk_types interp)
-    }
-;
-cofixheader:
-   COFIX ID LCURLY cofixfunsdecl RCURLY
-    { let dom,ids,mk_types = $4 in
-       let bs =
-        List.rev_map (function name -> Some (Name name)) ids
-       in
-        CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
-        dom, $2, ids, mk_types
-    }
-;
-cofixfunsdecl:
-   ID COLON expr
-    { let dom,mk_expr = $3 in
-       dom, [$1], function interp -> [mk_expr interp]
-    }
- | ID COLON expr SEMICOLON cofixfunsdecl
-    { let dom1,mk_expr = $3 in
-      let dom2,ids,mk_types = $5 in
-       let dom = union dom1 dom2 in
-        dom, $1::ids,
-         function interp -> (mk_expr interp)::(mk_types interp)
-    }
-;
-pihead:
-   PROD ID COLON expr DOT
-    { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
-      let dom,mk_expr = $4 in
-       Cic.Name $2, (dom, function interp -> mk_expr interp)
-    }
- | expr2 ARROW
-   { CicTextualParser0.binders := (Some Anonymous)::!CicTextualParser0.binders ;
-     let dom,mk_expr = $1 in
-      Anonymous, (dom, function interp -> mk_expr interp)
-   }
- | PROD ID DOT
-    { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
-      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)
-          ] @ !CicTextualParser0.metasenv ;
-         Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl))
-    }
-;
-lambdahead:
-   LAMBDA ID COLON expr DOT
-    { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
-      let dom,mk_expr = $4 in
-       Cic.Name $2, (dom, function interp -> mk_expr interp)
-    }
- | LAMBDA ID DOT
-    { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
-      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)
-          ] @ !CicTextualParser0.metasenv ;
-         Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl))
-    }
-;
-letinhead:
-  LAMBDA ID LETIN expr DOT
-   { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
-     let dom,mk_expr = $4 in
-      Cic.Name $2, (dom, function interp -> mk_expr interp)
-   }
-;
-branches:
-    { [], function _ -> [] }
- | expr SEMICOLON branches
-    { let dom1,mk_expr = $1 in
-      let dom2,mk_branches = $3 in
-       let dom = union dom1 dom2 in
-        dom, function interp -> (mk_expr interp)::(mk_branches interp)
-    }
- | expr
-    { let dom,mk_expr = $1 in
-       dom, function interp -> [mk_expr interp]
-    }
-;
-exprlist:
-    
-    { 0, [], function _ -> [] }
- | expr exprlist
-    { let dom1,mk_expr = $1 in
-      let length,dom2,mk_exprlist = $2 in
-       let dom = union dom1 dom2 in
-        length+1, dom, function interp -> (mk_expr interp)::(mk_exprlist interp)
-    }
-;
-exprseplist:
-   expr
-    { let dom,mk_expr = $1 in
-       dom, function interp -> [mk_expr interp]
-    }
- | expr SEMICOLON exprseplist
-    { let dom1,mk_expr = $1 in
-      let dom2,mk_exprseplist = $3 in
-       let dom = union dom1 dom2 in
-        dom, function interp -> (mk_expr interp)::(mk_exprseplist interp)
-    }
-;
-substitutionlist:
-    { [], function _ -> [] }
- | expr SEMICOLON substitutionlist
-    { let dom1,mk_expr = $1 in
-      let dom2,mk_substitutionlist = $3 in
-       let dom = union dom1 dom2 in
-        dom,
-         function interp ->(Some (mk_expr interp))::(mk_substitutionlist interp)
-    }
- | NONE SEMICOLON substitutionlist
-    { let dom,mk_exprsubstitutionlist = $3 in
-       dom, function interp -> None::(mk_exprsubstitutionlist interp)
-    }